proposition: Theorem stateAssignedDoTriplet : forall (S : State) (L : list triplet), stateAssignedOn S L -> forall t : triplet, In t L -> exists u : rZ * rZ, match u with | (a, b) => inTriplets a L /\ inTriplets b L end /\ doTripletP S t (addEq u S).
proof: Proof. unfold stateAssignedOn in |- *; intros S L H t; case t; intros b p q r Ht. cut (inTriplets p L); [ intros Hp | apply inTripletsIn with (2 := Ht) ]; simpl in |- *; auto with stalmarck. cut (inTriplets r L); [ intros Hr | apply inTripletsIn with (2 := Ht) ]; simpl in |- *; auto with stalmarck. cut (inTriplets (rZComp r) L); [ intros Hr2 | apply inTripletsIn with (2 := Ht) ]; simpl in |- *; auto with stalmarck. cut (inTriplets rZFalse L); [ intros Hz | apply inTripletsFalse ]; auto with stalmarck. elim (H q); [ intros Hq; case b | intros Hq; case b | apply varTripletTriplet2 with (1 := Ht) ]; auto with stalmarck. exists (p, r); simpl in |- *; split; [ split | apply doTripletAndPqT ]; auto with stalmarck. exists (p, r); simpl in |- *; split; [ split | apply doTripletEqPqT ]; auto with stalmarck. exists (p, rZFalse); simpl in |- *; split; [ split | apply doTripletAndPqF ]; auto with stalmarck. exists (p, rZComp r); simpl in |- *; split; [ split | apply doTripletEqPqF ]; auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux) Stalmarck(makeTriplet)