proposition: Lemma check_symopp_bvor_length2: forall bs1 bs2 bsres N, let n := length bsres in check_symopp bs1 bs2 bsres (BO_BVor N) = true -> (length bs1 = n)%nat /\ (length bs2 = n)%nat .
proof: Proof. intros. revert bs1 bs2 N 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 (PArray.length a =? 2) in H; try easy. case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy. specialize (IHrbsres bs1 bs2 (N - 1)%N H). simpl. simpl in n. fold n' in n. unfold n. split; apply f_equal. 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