proposition: Lemma prop_main: forall bs1 bs2 bsres, check_mult bs1 bs2 bsres = true -> map interp_carry (bblast_bvmult bs1 bs2 (Datatypes.length (map (Lit.interp rho) bs1))) = map (Lit.interp rho) bsres.
proof: Proof. intros. unfold check_mult in H. case_eq (Nat.eqb (Datatypes.length bs1) (Datatypes.length bs2)). intros. rewrite H0 in H. apply prop_eq_carry_lit2 in H. rewrite map_length. now rewrite H. intros. rewrite H0 in H. now contradict H. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance