proposition: Lemma DilemmaContradAux : forall (n : nat) (S : State) (L : list triplet) (a b : rZ), validEquation L a b -> eqStateRz S a (rZComp b) -> (forall a : rZ, In a (nthTail n (varTriplets L)) -> eqStateRz S a rZTrue \/ eqStateRz S a rZFalse) -> ex (fun S' : State => stalmarckP S L S' /\ contradictory S').
proof: Proof. simple induction n. simpl in |- *; intros S L a b V Eq H; elim (stateAssignContrad S L H a b V Eq); intros S' HS'. elim HS'; intros HS'1 HS'2; exists S'; auto with stalmarck. intros n' HR S L a b V Eq H. elim (Nat.le_gt_cases (length (varTriplets L)) n'); intros Hn'. apply (HR S L a b); auto with stalmarck. rewrite (nthTailProp3 n' (varTriplets L)); auto with stalmarck. elim (HR (addEq (myNth n' (varTriplets L) rZTrue, rZTrue) S) L a b); auto with stalmarck. intros S1 HS1; elim HS1; intros HS11 HS12. elim (HR (addEq (myNth n' (varTriplets L) rZTrue, rZFalse) S) L a b); auto with stalmarck. intros S2 HS2; elim HS2; intros HS21 HS22. exists (interState S1 S2); split; auto with stalmarck. apply stalmarckPSplit with (a := myNth n' (varTriplets L) rZTrue) (b := rZTrue) (S2 := S1) (S3 := S2); auto with stalmarck. unfold interState in |- *; case (eqStateRzContrDec S1); auto with stalmarck. intros Abs; absurd (forall a b : rZ, eqStateRz S1 a b); auto with stalmarck. intros c d; unfold contradictory in HS12; elim HS12; intros e He; eapply eqStateRzContr; eauto with stalmarck. rewrite (nthTailProp1 n' (varTriplets L)); auto with stalmarck; simpl in |- *; intros c Hc; elim Hc; intros Hc'. rewrite Hc'; right; auto with stalmarck. elim (H c); [ left | right | idtac ]; auto with stalmarck. rewrite (nthTailProp1 n' (varTriplets L)); auto with stalmarck; simpl in |- *; intros c Hc; elim Hc; intros Hc'. rewrite Hc'; left; auto with stalmarck. elim (H c); [ left | right | idtac ]; auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux) Stalmarck(makeTriplet) Coq(Arith)