proposition: Lemma check_symopp_bvor_length3: forall bs1 bs2 bsres n, check_symopp bs1 bs2 bsres (BO_BVor (N.of_nat n)) = true -> (length bs1 = n)%nat -> (length bsres = n)%nat.
proof: Proof. intros bs1 bs2 bsres. revert bs1 bs2. induction bsres as [ | xbsres xsbsres IHbsres ]. - intros. case bs1 in *. simpl in H. case bs2 in *. easy. now contradict H. case bs2 in *. simpl in H. now contradict H. simpl in H. now contradict H. - intros. case bs1 in *. simpl in H. case bs2 in *. now contradict H. now contradict H. simpl in H. case bs2 in *. now contradict H. case (Lit.is_pos xbsres) in *. case (t_form .[ Lit.blit xbsres] ) in *; try now contradict H. case (PArray.length a =? 2) in *. case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in *. specialize (IHbsres bs1 bs2 (n-1)%nat). simpl in H0. assert (length bs1 = (n-1)%nat). { lia. } cut ( (BO_BVor (N.of_nat n - 1)) = (BO_BVor (N.of_nat (n - 1)))). intros. revert H. rewrite H2. intros. specialize (IHbsres H H1). simpl. rewrite IHbsres. lia. simpl. cut ((N.of_nat n - 1)%N = (N.of_nat (n - 1))). intros. now rewrite H2. case n. now simpl. intros. lia. now contradict H. now contradict H. now contradict 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