proposition: Lemma check_symopp_bvand: forall bs1 bs2 bsres N, let n := length bsres in (length bs1 = n)%nat -> (length bs2 = n)%nat -> check_symopp bs1 bs2 bsres (BO_BVand N) = true -> (List.map (Lit.interp rho) bsres) = (RAWBITVECTOR_LIST.map2 andb (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). intros. rewrite H2 in H1. simpl. rewrite afold_left_and. case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold forallb. rewrite H3. case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? 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. unfold Var.interp. now rewrite andb_true_r. intros. rewrite H4 in H1. simpl in *. case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H5 & H6). rewrite eqb_spec in H5, H6. rewrite H5, H6. rewrite andb_true_r. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite andb_comm. intros. rewrite H5 in H1. now contradict H1. intros. rewrite H3 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 i0 Heq; rewrite Heq in H1; now contradict H1). try (intros i Heq; rewrite Heq 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). intros. contradict H3. discriminate. intros. contradict H3. discriminate. intros. contradict H3. discriminate. 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). intros. rewrite H2 in H1. simpl. rewrite afold_left_and. case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold forallb. rewrite H3. case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? 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. unfold Var.interp. now rewrite andb_true_r. intros H4. rewrite H4 in H1. simpl in *. case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. rewrite andb_true_r. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite andb_comm. intros. rewrite H5 in H1. now contradict H1. intros. rewrite H3 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 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). 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). 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). intros. contradict H3. discriminate. intros. contradict H3. discriminate. intros. contradict H3. discriminate. 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). intros. rewrite H2 in H1. simpl. rewrite afold_left_and. case_eq (PArray.length a =? 2). intros. rewrite H3 in H1. rewrite eqb_spec in H3. apply to_list_two in H3. unfold forallb. rewrite H3. case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? 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. unfold Var.interp. now rewrite andb_true_r. intros. rewrite H4 in H1. simpl in *. case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5. rewrite andb_true_iff in H5. destruct H5 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. rewrite andb_true_r. unfold Lit.interp. rewrite Heq1, Heq2. unfold Var.interp. now rewrite andb_comm. intros. rewrite H5 in H1. now contradict H1. intros. rewrite H3 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 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). 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). intros. 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). intros. contradict H3. discriminate. intros. contradict H3. discriminate. intros. contradict H3. discriminate. 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). intros. rewrite H3 in H1. simpl. rewrite afold_left_and. case_eq (PArray.length a =? 2). intros H5. rewrite H5 in H1. rewrite eqb_spec in H5. apply to_list_two in H5. unfold forallb. rewrite H5. case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H6. rewrite andb_true_iff in H6. destruct H6 as (H6 & H7). rewrite eqb_spec in H6, H7. rewrite H6, H7. unfold Lit.interp. rewrite Heq1, H2. unfold Var.interp. now rewrite andb_true_r. intros H6. rewrite H6 in H1. simpl in *. case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H7. rewrite andb_true_iff in H7. destruct H7 as (H7 & H8). rewrite eqb_spec in H7, H8. rewrite H7, H8. rewrite andb_true_r. unfold Lit.interp. rewrite Heq1, H2. unfold Var.interp. now rewrite andb_comm. intros. rewrite H4 in H1. now contradict H1. intros. rewrite H4 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 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). 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_and 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