proposition: Theorem CompInterR : forall (S : State) (a b : rZ), eqState S (interState (addEq (a, b) S) (addEq (a, rZComp b) S)).
proof: Proof. red in |- *; split; auto with stalmarck. red in |- *. intros i j H'. cut (eqStateRz (addEq (a, b) S) i j); [ intros Eq1 | apply (interMemInL (addEq (a, b) S) (addEq (a, rZComp b) S) i j) ]; auto with stalmarck. cut (eqStateRz (addEq (a, rZComp b) S) i j); [ intros Eq2 | apply (interMemInR (addEq (a, b) S) (addEq (a, rZComp b) S) i j) ]; auto with stalmarck. clear H'. cut (eqConstrState ((a, b) :: S) i j); [ intros EqC1; inversion EqC1 | auto with stalmarck ]. auto with stalmarck. cut (eqConstrState ((a, rZComp b) :: S) i j); [ intros EqC2; inversion EqC2 | auto with stalmarck ]. auto with stalmarck. apply eqStateContr with (p := j) (q := b); auto with stalmarck. apply eqStateContr with (p := a) (q := b); auto with stalmarck. apply eqStateRzTrans with (b := j); auto with stalmarck. apply eqStateRzTrans with (b := i); auto with stalmarck. apply eqStateContr with (p := i) (q := a); auto with stalmarck. apply eqStateContr with (p := a) (q := b); auto with stalmarck. apply eqStateRzTrans with (b := i); auto with stalmarck. rewrite <- (rZCompInv b); auto with stalmarck. apply eqStateRzTrans with (b := rZComp j); auto with stalmarck. apply eqStateRzTrans with (b := a); auto with stalmarck. apply eqStateRzTrans with (b := b); auto with stalmarck. rewrite <- (rZCompInv b); auto with stalmarck. cut (eqConstrState ((a, rZComp b) :: S) i j); [ intros EqC2; inversion EqC2 | auto with stalmarck ]. auto with stalmarck. apply eqStateContr with (p := a) (q := b); auto with stalmarck. apply eqStateRzTrans with (b := i); auto with stalmarck. apply eqStateRzTrans with (b := j); auto with stalmarck. apply eqStateContr with (p := i) (q := b); auto with stalmarck. apply eqStateContr with (p := a) (q := b); auto with stalmarck. apply eqStateRzTrans with (b := j); auto with stalmarck. rewrite <- (rZCompInv b); auto with stalmarck. apply eqStateRzTrans with (b := rZComp i); auto with stalmarck. apply eqStateContr with (p := j) (q := a); auto with stalmarck. apply eqStateRzTrans with (b := a); auto with stalmarck. apply eqStateRzTrans with (b := b); auto with stalmarck. rewrite <- (rZCompInv b); auto with stalmarck. cut (eqConstrState ((a, rZComp b) :: S) i j); [ intros EqC2; inversion EqC2 | auto with stalmarck ]. auto with stalmarck. apply eqStateContr with (p := i) (q := a); auto with stalmarck. apply eqStateContr with (p := a) (q := b); auto with stalmarck. apply eqStateRzTrans with (b := rZComp i); auto with stalmarck. apply eqStateRzTrans with (b := j); auto with stalmarck. apply eqStateContr with (p := j) (q := b); auto with stalmarck. rewrite <- (rZCompInv b); auto with stalmarck. apply eqStateContr with (p := a) (q := b); auto with stalmarck. apply eqStateRzTrans with (b := rZComp j); auto with stalmarck. apply eqStateRzTrans with (b := rZComp i); auto with stalmarck. apply eqStateRzTrans with (b := rZComp a); auto with stalmarck. apply eqStateRzTrans with (b := rZComp b); auto with stalmarck. cut (eqConstrState ((a, rZComp b) :: S) i j); [ intros EqC2; inversion EqC2 | auto with stalmarck ]. auto with stalmarck. apply eqStateContr with (p := a) (q := b); auto with stalmarck. apply eqStateRzTrans with (b := rZComp j); auto with stalmarck. apply eqStateRzTrans with (b := i); auto with stalmarck. apply eqStateContr with (p := j) (q := a); auto with stalmarck. apply eqStateContr with (p := a) (q := b); auto with stalmarck. apply eqStateRzTrans with (b := rZComp i); auto with stalmarck. apply eqStateRzTrans with (b := rZComp j); auto with stalmarck. apply eqStateContr with (p := i) (q := b); auto with stalmarck. rewrite <- (rZCompInv b); auto with stalmarck. apply eqStateRzTrans with (b := rZComp a); auto with stalmarck. apply eqStateRzTrans with (b := rZComp b); auto with stalmarck. cut (eqConstrState ((a, rZComp b) :: S) i j); [ intros EqC2; inversion EqC2 | auto with stalmarck ]. auto with stalmarck. apply eqStateRzTrans with (b := a); auto with stalmarck. apply eqStateRzTrans with (b := rZComp b); auto with stalmarck. apply eqStateRzTrans with (b := rZComp b); auto with stalmarck. apply eqStateRzTrans with (b := a); auto with stalmarck. apply eqStateRzTrans with (b := rZComp a); auto with stalmarck. apply eqStateRzTrans with (b := b); auto with stalmarck. rewrite <- (rZCompInv b); auto with stalmarck. apply eqStateRzTrans with (b := b); auto with stalmarck. rewrite <- (rZCompInv b); auto with stalmarck. apply eqStateRzTrans with (b := rZComp a); auto with stalmarck. apply eqStateContr with (p := a) (q := b); auto with stalmarck. rewrite <- (rZCompInv b); auto with stalmarck. Qed.
imports: Coq(List)