proposition: Theorem stateAssignContrad : forall (S : State) (L : list triplet), stateAssignedOn S L -> forall a b : rZ, validEquation L a b -> eqStateRz S a (rZComp b) -> ex (fun S' : State => doTripletsP S L S' /\ contradictory S').
proof: Proof. intros S L H a b Hab1 Hab2. case (eqStateRzContrDec2 S); intros HS. exists S; auto with stalmarck. elim (Realizable2 S HS); intros f Hf; elim Hf; intros Hf1 Hf2. elim (negRealizeTriplets f L); [ intros t Ht; elim Ht; intros Ht1 Ht2 | idtac ]. elim (stateAssignedDoTriplet S L H t Ht1); intros p; case p; intros c d T; elim T; intros T2 HS'; elim T2; intros Hc Hd. exists (addEq (c, d) S); split; auto with stalmarck. apply doTripletsTrans with (t := t) (S2 := addEq (c, d) S); auto with stalmarck. unfold contradictory in |- *; exists d. apply eqStateRzTrans with (b := c); auto with stalmarck. cut (eqStateRz S c (rZComp d)); auto with stalmarck. elim (stateAssignedProp2 S L H c d); auto with stalmarck. intros Hcd. elim (realizeStateEvalEquiv f S (addEq (c, d) S) t); auto with stalmarck; intros Thm1 Thm2. rewrite Ht2 in Thm1; absurd (false = true); [ auto with bool stalmarck| apply Thm1 ]. apply realizeStateAddEq; auto with stalmarck. eapply realizeStateInv; eauto with stalmarck. red in |- *; intros Abs; unfold validEquation in Hab1. lapply (realizeStateInv f S Hf1 a (rZComp b)); auto with stalmarck. rewrite (Hab1 f Abs Hf2); rewrite (rZEvalCompInv b f). case (rZEval f b); auto with bool stalmarck. Qed.
imports: Stalmarck(PolyListAux) Stalmarck(makeTriplet)