proposition: Lemma check_bvmult_length: forall bs1 bs2, let bsres0 := bblast_bvmult bs1 bs2 (length bs1) in length bs1 = length bs2 -> length bs1 = length bsres0.
proof: Proof. intros. unfold bblast_bvmult in bsres0. case_eq (length bs1). intros. unfold bsres0. rewrite H0. specialize (@prop_and_with_bit2 bs1 (nth 0 bs2 Lit._false)). intros. now rewrite H1. intros. unfold bsres0. rewrite H0. case n in *. simpl. rewrite prop_and_with_bit2. auto. rewrite prop_mult_step3. rewrite prop_and_with_bit2. auto. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance