proposition: Theorem restricMonotone : forall (S1 S2 : State) (L1 L2 : list rNat), inclState S1 S2 -> incl L1 L2 -> inclState (restrictState S1 L1) (restrictState S2 L2).
proof: Proof. intros S1 S2 L1 L2 H' H'0. apply inclStateIn; auto with stalmarck. intros a b H'1. unfold restrictState in H'1; generalize H'1; clear H'1. case (eqStateRzContrDec S1); auto with stalmarck. intros H'1 H'2; unfold restrictState in |- *. case (eqStateRzContrDec S2); auto with stalmarck. intros H'3; case H'3; auto with stalmarck. intros H'1 H'2. apply restrictStateComp; auto with stalmarck. red in H'0. apply H'0. apply stripInRzIn1 with (L1 := stripRz S1); auto with stalmarck. apply prodRzInL with (b := b) (L2 := stripInRz L1 (stripRz S1)); auto with stalmarck. apply stripRzDecProp1 with (S1 := S1); auto with stalmarck. red in H'0. apply H'0. apply stripInRzIn1 with (L1 := stripRz S1); auto with stalmarck. apply prodRzInR with (a := a) (L1 := stripInRz L1 (stripRz S1)); auto with stalmarck. apply stripRzDecProp1 with (S1 := S1); auto with stalmarck. apply eqStateIncl with (S1 := S1); auto with stalmarck. apply eqStateIncl with (S1 := restrictState S1 L1); auto with stalmarck. apply restrictStateIncl; auto with stalmarck. unfold restrictState in |- *; case (eqStateRzContrDec S1); auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)