proposition: Lemma resolve_correct : forall rho c1 c2, interp rho c1 -> interp rho c2 -> interp rho (resolve c1 c2).
proof: Proof. induction c1;simpl;try discriminate. destruct c2;simpl;try discriminate. intros Hc1 Hc2. generalize (compare_spec' a i);destruct (a ?= i);intros;subst;simpl. destruct (Lit.interp rho i);simpl in *;auto. generalize (Lit.lxor_neg a i);destruct (a lxor i =? 1);intros. rewrite or_correct. rewrite H0, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho i). simpl in Hc1;rewrite Hc1;trivial. simpl in Hc2;rewrite Hc2, orb_true_r;trivial. simpl;destruct (Lit.interp rho a);simpl;auto. generalize (Lit.lxor_neg a i);destruct (a lxor i =? 1);intros. rewrite or_correct. rewrite H0, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho i). simpl in Hc1;rewrite Hc1;trivial. simpl in Hc2;rewrite Hc2, orb_true_r;trivial. simpl;destruct (Lit.interp rho i);simpl;auto using resolve_aux_correct. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring