proposition: Theorem RestrictAddEq1 : forall (S : State) (L : list rNat) (a b : rZ), In (valRz a) L -> In (valRz b) L -> In zero L -> inclState (addEq (a, b) (restrictState S L)) (restrictState (addEq (a, b) S) L).
proof: Proof. intros S L a b H' H'0 H'1. apply inclStateIn; auto with stalmarck. simpl in |- *; auto with stalmarck. intros a0 b0 H'2; Elimc H'2; intros H'2; auto with stalmarck. inversion H'2; auto with stalmarck. rewrite <- H0; auto with stalmarck. rewrite <- H1; auto with stalmarck. apply restrictStateComp; auto with stalmarck. apply restrictStateComp; auto with stalmarck. generalize H'2; unfold restrictState in |- *. case (eqStateRzContrDec S); simpl in |- *; auto with stalmarck. intros H'3 H'4; Elimc H'4; intros H'4; auto with stalmarck; inversion H'4; auto with stalmarck. intros H'3 H'4. apply stripInRzIn1 with (L1 := stripRz S); auto with stalmarck. apply prodRzInL with (b := b0) (L2 := stripInRz L (stripRz S)); auto with stalmarck. apply stripRzDecProp1 with (S1 := S); auto with stalmarck. generalize H'2; unfold restrictState in |- *. case (eqStateRzContrDec S); simpl in |- *; auto with stalmarck. intros H'3 H'4; Elimc H'4; intros H'4; auto with stalmarck; inversion H'4; auto with stalmarck. intros H'3 H'4. apply stripInRzIn1 with (L1 := stripRz S); auto with stalmarck. apply prodRzInR with (a := a0) (L1 := stripInRz L (stripRz S)); auto with stalmarck. apply stripRzDecProp1 with (S1 := S); auto with stalmarck. apply eqStateIncl with (S1 := S); auto with stalmarck. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateIncl. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)