proposition: Lemma check_symopp_or: forall ibs1 ibs2 xbs1 ybs2 ibsres zbsres N, check_symopp (ibs1 :: xbs1) (ibs2 :: ybs2) (ibsres :: zbsres) (BO_BVor N) = true -> check_symopp xbs1 ybs2 zbsres (BO_BVor (N-1)) = true.
proof: Proof. intros. induction N. simpl. simpl in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). case (PArray.length a =? 2) in H. case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2) || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H. exact H. now contradict H. now contradict H. now contradict H. unfold check_symopp in H. case (Lit.is_pos ibsres) in H. case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy). case (PArray.length a =? 2) in H. case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2) || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H. apply H. 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