proposition: Lemma stateAssignedProp1 : forall (S : State) (L : list triplet), stateAssignedOn S L -> forall a b : rZ, In a (varTriplets L) -> In b (varTriplets L) -> eqStateRz S a b \/ eqStateRz S a (rZComp b).
proof: Proof. unfold stateAssignedOn in |- *; intros S L H a b Ha Hb. elim (H a Ha); elim (H b Hb); intros H1 H2. left; apply eqStateRzTrans with (b := rZTrue); auto with stalmarck. right; apply eqStateRzTrans with (b := rZTrue); auto with stalmarck. cut (rZTrue = rZComp rZFalse); [ intros T; rewrite T | simpl in |- * ]; auto with stalmarck. right; apply eqStateRzTrans with (b := rZFalse); auto with stalmarck. cut (rZFalse = rZComp rZTrue); [ intros T; rewrite T | simpl in |- * ]; auto with stalmarck. left; apply eqStateRzTrans with (b := rZFalse); auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux) Stalmarck(makeTriplet)