proposition: Theorem doTripletRestrictInv : forall (S1 S2 : State) (t : triplet) (L : list rNat), incl (ResTriplet t) L -> doTripletP (restrictState S1 L) t S2 -> exists S3 : State, doTripletP S1 t S3 /\ eqState S3 (unionState (restrictState S2 L) S1).
proof: Proof. intros S1 S2 t L H' H'0. elim (doTripletCongruentEx (restrictState S1 L) S2 S1 t); [ intros S4 E; Elimc E; intros H'4 H'5 | idtac ]; auto with stalmarck. elim (doTripletEqCompEx (unionState S1 (restrictState S1 L)) S4 S1 t); [ intros S5 E; Elimc E; intros H'8 H'9 | idtac | idtac ]; auto with stalmarck. exists S5; split; auto with stalmarck. apply eqStateTrans with (S2 := S4); auto with stalmarck. apply eqStateTrans with (S2 := unionState S1 S2); auto with stalmarck. apply eqStateTrans with (S2 := unionState S1 (restrictState S2 L)); auto with stalmarck. apply unionStateEq; auto with stalmarck. apply restrictDoTripletComp with (S1 := S1) (t := t); auto with stalmarck. red in |- *; split; auto with stalmarck. apply unionStateMin; auto with stalmarck. apply restrictStateIncl; auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)