proposition: Lemma check_symopp_bvxor: forall bs1 bs2 bsres N, let n := length bsres in (length bs1 = n)%nat -> (length bs2 = n)%nat -> check_symopp bs1 bs2 bsres (BO_BVxor N) = true -> (List.map (Lit.interp rho) bsres) = (RAWBITVECTOR_LIST.map2 xorb (List.map (Lit.interp rho) bs1) (List.map (Lit.interp rho) bs2)).
proof: Proof. intro bs1. induction bs1 as [ | ibs1 xbs1 IHbs1]. - intros. simpl in *. rewrite <- H0 in H. rewrite <- H in H0. unfold n in H0. symmetry in H0. rewrite empty_list_length in H0. unfold map. now rewrite H0. - intros [ | ibs2 ybs2]. + intros. simpl in *. now contradict H1. + intros [ | ibsres zbsres ]. * intros. simpl in *. now contradict H. * intros. simpl. specialize (IHbs1 ybs2 zbsres (N-1)%N). rewrite IHbs1. rewrite eq_head. unfold Lit.interp, Var.interp. case_eq (Lit.is_pos ibsres); intro Heq0. case_eq (Lit.is_pos ibs1); intro Heq1. case_eq (Lit.is_pos ibs2); intro Heq2. rewrite wf_interp_form; trivial. simpl in H1. rewrite Heq0 in H1. case_eq (t_form .[ Lit.blit ibsres]). try (intros i Heq; rewrite Heq in H1; now contradict H1). try (intros Heq; rewrite Heq in H1; now contradict H1). try (intros Heq; rewrite Heq in H1; now contradict H1). try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). try (intros i Heq; rewrite Heq in H1; now contradict H1). intros. rewrite H2 in H1. simpl. case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. now unfold Var.interp. intros H4. rewrite H4 in H1. simpl in *. case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite xorb_comm. intros. rewrite H3 in H1. now contradict H1. try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). try (intros i i0 i1 Heq; rewrite Heq in H1; now contradict H1). try (intros i l Heq; rewrite Heq in H1; now contradict H1). rewrite wf_interp_form; trivial. simpl in H1. case_eq (t_form .[ Lit.blit ibsres]). rewrite Heq0 in H1. case_eq (t_form .[ Lit.blit ibsres]). try (intros i Heq; rewrite Heq in H1; now contradict H1). try (intros Heq; rewrite Heq in H1; now contradict H1). try (intros Heq; rewrite Heq in H1; now contradict H1). try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). intros. contradict H3. discriminate. intros. contradict H3. discriminate. intros. contradict H3. discriminate. intros. contradict H3. discriminate. rewrite Heq0 in H1. try (intros Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros a Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros a Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros a Heq; rewrite Heq in H1; now contradict H1). intros. rewrite H2 in H1. simpl. case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. now unfold Var.interp. intros H4. rewrite Heq0, H4 in H1. simpl in *. case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite xorb_comm. intros. rewrite H3 in H1. now contradict H1. rewrite Heq0 in H1. try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). try (intros i i0 i1 Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros i l Heq; rewrite Heq in H1; now contradict H1). case_eq (Lit.is_pos ibs2). intro Heq2. rewrite wf_interp_form; trivial. simpl in H1. case_eq (t_form .[ Lit.blit ibsres]). rewrite Heq0 in H1. case_eq (t_form .[ Lit.blit ibsres]). try (intros i Heq; rewrite Heq in H1; now contradict H1). try (intros Heq; rewrite Heq in H1; now contradict H1). try (intros Heq; rewrite Heq in H1; now contradict H1). try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). intros. contradict H3. discriminate. intros. contradict H3. discriminate. intros. contradict H3. discriminate. intros. contradict H3. discriminate. rewrite Heq0 in H1. try (intros Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros a Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros a Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros a Heq; rewrite Heq in H1; now contradict H1). intros. rewrite H2 in H1. simpl. case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. now unfold Var.interp. intros H4. rewrite Heq0, H4 in H1. simpl in *. case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite xorb_comm. intros. rewrite H3 in H1. now contradict H1. rewrite Heq0 in H1. try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). try (intros i i0 i1 Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros i l Heq; rewrite Heq in H1; now contradict H1). intro Heq2. rewrite wf_interp_form; trivial. simpl in H1. case_eq (t_form .[ Lit.blit ibsres]). rewrite Heq0 in H1. case_eq (t_form .[ Lit.blit ibsres]). try (intros i Heq; rewrite Heq in H1; now contradict H1). try (intros Heq; rewrite Heq in H1; now contradict H1). try (intros Heq; rewrite Heq in H1; now contradict H1). try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). try (intros a Heq; rewrite Heq in H1; now contradict H1). intros. contradict H3. discriminate. intros. contradict H3. discriminate. intros. contradict H3. discriminate. intros. contradict H3. discriminate. rewrite Heq0 in H1. try (intros Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros a Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros a Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros a Heq; rewrite Heq in H1; now contradict H1). intros. rewrite H2 in H1. simpl. case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. unfold Lit.interp. rewrite Heq1, Heq2. now unfold Var.interp. intros H4. rewrite Heq0, H4 in H1. simpl in *. case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite xorb_comm. intros. rewrite H3 in H1. now contradict H1. rewrite Heq0 in H1. try (intros i i0 Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros i i0 i1 Heq; rewrite Heq in H1; now contradict H1). rewrite Heq0 in H1. try (intros i l Heq; rewrite Heq in H1; now contradict H1). rewrite wf_interp_form; trivial. simpl in H1. rewrite Heq0 in H1. now contradict H1. now inversion H. now inversion H0. apply (@check_symopp_xor ibs1 ibs2 xbs1 ybs2 ibsres zbsres N). exact H1. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance