proposition: Lemma prop_eq_carry_lit: forall c i, eq_carry_lit c i = true -> interp_carry c = (Lit.interp rho i).
proof: Proof. intro c. induction c. - intros. simpl in *. case (Lit.is_pos i0 ) in H; rewrite eqb_spec in H; now rewrite H. - intros. simpl. pose proof IHc1. pose proof IHc2. simpl in H. case_eq ( Lit.is_pos i). intros Hip0. rewrite Hip0 in H. case_eq (t_form .[ Lit.blit i]); intros; rewrite H2 in H; try now contradict H. case_eq (PArray.length a =? 2). intros Hl. rewrite Hl in H. rewrite andb_true_iff in H. specialize (@rho_interp ( Lit.blit i)). rewrite H2 in rho_interp. simpl in rho_interp. rewrite afold_left_and in rho_interp. rewrite eqb_spec in Hl. apply to_list_two in Hl. rewrite Hl in rho_interp. simpl in rho_interp. rewrite andb_true_r in rho_interp. + destruct H. apply H0 in H. apply H1 in H3. rewrite H, H3. unfold Lit.interp at 3. unfold Var.interp. rewrite Hip0. now rewrite rho_interp. + intros. rewrite H3 in H. now contradict H. + intros. rewrite H2 in H. now contradict H. - intros. simpl. pose proof IHc1. pose proof IHc2. simpl in H. case_eq ( Lit.is_pos i). intros Hip0. rewrite Hip0 in H. case_eq (t_form .[ Lit.blit i]); intros; rewrite H2 in H; try now contradict H. rewrite andb_true_iff in H. specialize (@rho_interp ( Lit.blit i)). rewrite H2 in rho_interp. simpl in rho_interp. + destruct H. apply H0 in H. apply H1 in H3. rewrite H, H3. unfold Lit.interp at 3. unfold Var.interp. rewrite Hip0. now rewrite rho_interp. + intros. rewrite H2 in H. now contradict H. - intros. simpl. pose proof IHc1. pose proof IHc2. simpl in H. case_eq ( Lit.is_pos i). intros Hip0. rewrite Hip0 in H. case_eq (t_form .[ Lit.blit i]); intros; rewrite H2 in H; try now contradict H. case_eq (PArray.length a =? 2). intros Hl. rewrite Hl in H. rewrite andb_true_iff in H. specialize (@rho_interp ( Lit.blit i)). rewrite H2 in rho_interp. simpl in rho_interp. rewrite afold_left_or in rho_interp. rewrite eqb_spec in Hl. apply to_list_two in Hl. rewrite Hl in rho_interp. simpl in rho_interp. rewrite orb_false_r in rho_interp. + destruct H. apply H0 in H. apply H1 in H3. rewrite H, H3. unfold Lit.interp at 3. unfold Var.interp. rewrite Hip0. now rewrite rho_interp. + intros. rewrite H3 in H. now contradict H. + intros. rewrite H2 in H. now contradict H. - intros. simpl. pose proof IHc1. pose proof IHc2. simpl in H. case_eq ( Lit.is_pos i). intros Hip0. rewrite Hip0 in H. case_eq (t_form .[ Lit.blit i]); intros; rewrite H2 in H; try now contradict H. rewrite andb_true_iff in H. specialize (@rho_interp ( Lit.blit i)). rewrite H2 in rho_interp. simpl in rho_interp. + destruct H. apply H0 in H. apply H1 in H3. rewrite H, H3. unfold Lit.interp at 3. unfold Var.interp. rewrite Hip0. now rewrite rho_interp. + intros. rewrite H2 in 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