proposition: Lemma check_add_bvadd_length: forall bs1 bs2 bsres c, let n := length bsres in check_add bs1 bs2 bsres c = true -> (length bs1 = n)%nat /\ (length bs2 = n)%nat .
proof: Proof. intros. revert bs1 bs2 c H. induction bsres as [ | r rbsres ]. intros. simpl in H. case bs1 in *. simpl in H. case bs2 in *. simpl in *. easy. easy. case bs2 in *. simpl in *. easy. simpl in *. easy. intros. case bs1 in *. case bs2 in *. simpl in *. easy. simpl in *. easy. case bs2 in *. simpl in *. easy. set (n' := length rbsres). fold n' in n, IHrbsres, H. simpl in IHrbsres. simpl in H. case (Lit.is_pos r) in H. case (t_form .[ Lit.blit r]) in H; try easy. case (Lit.is_pos i1) in H. case (t_form .[ Lit.blit i1]) in H; try now contradict H. rewrite andb_true_iff in H. destruct H. specialize (IHrbsres bs1 bs2 ((Cor (Cand (Clit i) (Clit i0)) (Cand (Cxor (Clit i) (Clit i0)) c))) H0). simpl. simpl in n. split; apply f_equal. easy. easy. easy. easy. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance