proposition: Lemma check_add_bvadd: forall bs1 bs2 bsres n, (N.of_nat(length bs1) = n)%N -> (N.of_nat(length bs2) = n)%N -> (N.of_nat(length bsres) = n)%N -> check_add bs1 bs2 bsres (Clit Lit._false) = true -> (RAWBITVECTOR_LIST.bv_add (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2) = (map (Lit.interp rho) bsres)).
proof: Proof. intros. pose proof H as H'. pose proof H0 as H0'. pose proof H1 as H1'. rewrite <- H1 in H. apply Nat2N.inj in H. rewrite <- H1 in H0. apply Nat2N.inj in H0. specialize (@check_add_list bs1 bs2 bsres ( (Clit Lit._false)) H H0 H2). intros. unfold RAWBITVECTOR_LIST.bv_add. unfold RAWBITVECTOR_LIST.size, RAWBITVECTOR_LIST.bits. unfold BITVECTOR_LIST.of_bits. rewrite !map_length, H, H0. rewrite N.eqb_refl. assert ( (interp_carry (Clit Lit._false)) = false). { specialize (Lit.interp_false rho wf_rho). intros. unfold is_true in H4. rewrite not_true_iff_false in H4. now unfold interp_carry. } rewrite H4 in H3. unfold RAWBITVECTOR_LIST.add_list. apply H3. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance