proposition: Theorem RestrictAddEq2 : forall (S : State) (L : list rNat) (a b : rZ), In (valRz a) L -> In (valRz b) L -> In zero L -> inclState (restrictState (addEq (a, b) S) L) (addEq (a, b) (restrictState S L)).
proof: Proof. intros S L a b H' H'0 Eqz; apply inclStateIn; auto with stalmarck. intros a0 b0 H'1. cut (eqConstrState (addEq (a, b) S) a0 b0). cut (In (valRz a0) L); [ intros Ina0L | apply restrictStateInZeroL with (S := addEq (a, b) S) (b := b0) ]; auto with stalmarck. cut (In (valRz b0) L); [ intros Inb0L | apply restrictStateInZeroR with (S := addEq (a, b) S) (a := a0) ]; auto with stalmarck. intros H'2; unfold addEq in H'2; inversion H'2. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateComp; auto with stalmarck. apply eqStateRzTrans with (b := a); auto with stalmarck. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateComp; auto with stalmarck. apply eqStateRzTrans with (b := b); auto with stalmarck. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateComp; auto with stalmarck. apply eqStateRzTrans with (b := b); auto with stalmarck. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateComp; auto with stalmarck. apply eqStateRzTrans with (b := a); auto with stalmarck. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateComp; auto with stalmarck. apply eqStateRzTrans with (b := rZComp a); auto with stalmarck. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateComp; auto with stalmarck; rewrite valRzComp; auto with stalmarck. apply eqStateRzTrans with (b := rZComp b); auto with stalmarck. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateComp; auto with stalmarck; rewrite valRzComp; auto with stalmarck. apply eqStateRzTrans with (b := rZComp b); auto with stalmarck. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateComp; auto with stalmarck; rewrite valRzComp; auto with stalmarck. apply eqStateRzTrans with (b := rZComp a); auto with stalmarck. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateComp; auto with stalmarck; rewrite valRzComp; auto with stalmarck. apply eqStateContr with (p := a) (q := b); auto with stalmarck. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateComp; auto with stalmarck; rewrite valRzComp; auto with stalmarck. apply eqStateRzPImpeqConstrState; auto with stalmarck. apply eqStateIncl with (S1 := restrictState (addEq (a, b) S) L); auto with stalmarck. apply restrictStateIncl; auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)