exp_md: THEORY
 BEGIN


  IMPORTING mul_div_comb

  md_add_lz(lza, lzb: bvec[6], fdiv: bit): [# s: bvec[12], t: bvec[11] #] =
      LET lzaP = fill[1](TRUE) o NOT lza,
          lzbP = fill[1](NOT fdiv) o mux_impl[6](NOT lzb, lzb, fdiv),
		  c1 = fill[6](FALSE) o fill[1](NOT fdiv),
										%%%% this was constant 1, but for the 
						%%% new shift by 1 of the div-significand, we
						%%% compensate here by only incrementing in case of mult 
          cs = carry_save_adder_impl(7, lzaP, lzbP, c1)
        IN (# s := sext_impl[7,12](cs`s),
			  t := sext_impl[8,11](cs`t) #);

  exp_md(ea, eb: bvec[11], lza,lzb: bvec[6], fdiv: bit): bvec[13]
		= LET cslz = md_add_lz(lza, lzb, fdiv),
			  ebP = mux_impl[11](eb, NOT eb, fdiv),
			  cse = carry_save_adder_impl(11, ea, ebP, cslz`t),
			  cses=sext_impl[11,12](cse`s),
			  cs_all = carry_save_adder_impl(12, cses, cse`t, cslz`s),
			  cs_alls=sext_impl[12,13](cs_all`s)
		   IN add_impl[13](cs_alls, cs_all`t, TRUE)`s;

  exp_md_mul: LEMMA FORALL (ea, eb: bvec[11], lza,lzb: bvec[6]):
		bv2int(exp_md(ea, eb, lza, lzb, FALSE)) =
			bv2int(ea) + bv2int(eb) - bv2nat(lza) - bv2nat(lzb);

  exp_md_div: LEMMA FORALL (ea, eb: bvec[11], lza,lzb: bvec[6]):
		bv2int(exp_md(ea, eb, lza, lzb, TRUE)) =
			bv2int(ea) - bv2int(eb) - bv2nat(lza) + bv2nat(lzb) - 1;

 END exp_md