proposition: Lemma prop_bblast_bvmult: forall a b n, (map interp_carry (bblast_bvmult a b n)) = RAWBITVECTOR_LIST.bvmult_bool (map (Lit.interp rho) a) (map (Lit.interp rho) b) n.
proof: Proof. intros. revert a b. induction n. - intros. simpl. rewrite prop_and_with_bit. rewrite <- map_nth. specialize (Lit.interp_false rho wf_rho). intros. unfold is_true in H. rewrite not_true_iff_false in H. now rewrite H. - intros. simpl. specialize (Lit.interp_false rho wf_rho). intros. unfold is_true in H. rewrite not_true_iff_false in H. case n in *. rewrite prop_and_with_bit; rewrite <- map_nth; now rewrite H. rewrite prop_mult_step; rewrite prop_and_with_bit; rewrite <- map_nth; now rewrite 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