proposition: Theorem restrictDoTripletCompAux1 : forall (S1 : State) (L : list rNat) (p q r s : rZ), In (valRz p) L -> In (valRz q) L -> In (valRz r) L -> In (valRz s) L -> In zero L -> eqState (addEq (p, q) (addEq (r, s) (restrictState S1 L))) (restrictState (addEq (p, q) (addEq (r, s) (restrictState S1 L))) L).
proof: Proof. intros S1 L p q r s H' H'0 H'1 H'2 H'3. apply eqStateTrans with (S2 := restrictState (addEq (p, q) (addEq (r, s) S1)) L); auto with stalmarck. apply eqStateTrans with (S2 := addEq (p, q) (restrictState (addEq (r, s) S1) L)); auto with stalmarck. apply eqStateAddEq; auto with stalmarck. apply eqStateSym. apply RestrictAddEq; auto with datatypes stalmarck. apply eqStateSym. apply RestrictAddEq; auto with datatypes stalmarck. apply eqStateTrans with (S2 := restrictState (restrictState (addEq (p, q) (addEq (r, s) S1)) L) L); auto with stalmarck. apply restrictStateInvol; auto with datatypes stalmarck. apply restrictEqComp; auto with stalmarck. apply eqStateTrans with (S2 := addEq (p, q) (restrictState (addEq (r, s) S1) L)); auto with stalmarck. apply RestrictAddEq; auto with datatypes stalmarck. apply eqStateAddEq; auto with stalmarck. apply RestrictAddEq; auto with datatypes stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)