proposition: Theorem doTripletsConftEx : forall (L : list triplet) (S1 S2 S3 : State), doTripletsP S1 L S2 -> doTripletsP S1 L S3 -> exists S4 : State, doTripletsP S2 L S4 /\ doTripletsP S3 L S4.
proof: Proof. intros L S1 S2 S3 H' H'0. elim (doTripletsUnionEx S1 S2 L); [ intros S4 E | idtac ]; auto with stalmarck. elim (doTripletsUnionEx S1 S3 L); [ intros S5 E0 | idtac ]; auto with stalmarck. exists (unionState S5 S2); split; auto with stalmarck. apply doTripletsComp with (S1 := unionState S4 S1) (S2 := unionState S4 S3); auto with stalmarck. apply doTripletCongruent; auto with stalmarck. apply eqStateTrans with (S2 := unionState S5 (unionState S4 S1)); auto with stalmarck. apply eqStateTrans with (S2 := unionState (unionState S5 S4) S1); auto with stalmarck. apply unionStateAssoc; auto with stalmarck. apply eqStateTrans with (S2 := unionState (unionState S4 S5) S1); auto with stalmarck. apply eqStateTrans with (S2 := unionState S4 (unionState S5 S1)); auto with stalmarck. apply eqStateTrans with (S2 := unionState (unionState S4 S5) S1); auto with stalmarck. apply eqStateSym; auto with stalmarck. apply unionStateAssoc; auto with stalmarck. apply doTripletsComp with (S1 := unionState S5 S1) (S2 := unionState S5 S2); auto with stalmarck. apply doTripletCongruent; auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux)