proposition: Lemma check_symopp_bveq: forall bs1 bs2 a4 n, check_symopp bs1 bs2 (to_list a4) (BO_eq (Typ.TBV n)) = true -> RAWBITVECTOR_LIST.beq_list (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2) = forallb (Lit.interp rho) (to_list a4).
proof: Proof. intros. revert bs1 bs2 H. induction (to_list a4) as [ | xa4 xsa4 IHa4]. - intros. case_eq bs1. intros. rewrite H0 in H. case_eq bs2. intros. rewrite H1 in H. simpl. easy. intros. rewrite H1 in H. simpl in H. now contradict H. intros. rewrite H0 in H. simpl in H. case_eq bs2. intros. rewrite H1 in H. now contradict H. intros. rewrite H1 in H. now contradict H. - intros. unfold check_symopp in H. case_eq bs1. intros. rewrite H0 in H. case_eq bs2. intros. rewrite H1 in H. now contradict H. intros. rewrite H1 in H. now contradict H. intros. fold check_symopp in H. case_eq bs2. intros. rewrite H1 in H. simpl in H. rewrite H0 in H. simpl in H. now contradict H. intros. rewrite H0, H1 in H. pose proof H. apply check_symopp_eq' in H2. apply check_symopp_eq in H. specialize (IHa4 l l0 H). simpl. rewrite IHa4. case (forallb (Lit.interp rho) xsa4); [ do 2 rewrite andb_true_r | now do 2 rewrite andb_false_r]. exact H2. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance