---

Step * of Lemma event-has_functionality

∀s:SES. (ActionsDisjoint ⇒ (∀es:EO+(Info). ∀x,y:E.  (same-action(x;y) ⇒ (∀a:Atom1. ((x has a) ⇒ (y has a))))))
BY
{ (Auto
   THEN Unfold `same-action` -3
   THEN Unfold `ses-disjoint` 2
   THEN (((InstHyp [⌜es⌝] 2⋅ THENM (Thin 2 THEN D -1)) THEN Auto)⋅
         THEN ((InstHyp [⌜x⌝] (-1)⋅ THENM InstHyp [⌜y⌝] (-2)⋅ THENM Thin (-3)) THENA Auto)
         THEN SplitOrHyps
         THEN Auto
         THEN ThinTrivial
         THEN Eliminate ⌜f x⌝⋅
         THEN Eliminate ⌜f y⌝⋅
         THEN Try ((DupHyp 9
                    THEN RepUR ``event-has class-value-has`` -1
                    THEN RepUR ``event-has class-value-has`` 0
                    THEN SplitOrHyps
                    THEN ExRepD
                    THEN (ThinTrivial⋅ THEN Try ((Assert ⌜False⌝⋅ THEN CompleteAuto)))
                    THEN (SelectBy 6 THENA Auto)⋅
                    THEN D 0
                    THEN Try ((NthHypEq (-1) THEN EqCD))
                    THEN Complete (Auto))⋅))⋅) }

---

Latex:

---

Latex:
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}x,y:E.    (same-action(x;y)  {}\mRightarrow{}  (\mforall{}a:Atom1.  ((x  has  a)  {}\mRightarrow{}  (y  has  a))))))


By

---

Latex:
(Auto
  THEN  Unfold  `same-action`  -3
  THEN  Unfold  `ses-disjoint`  2
  THEN  (((InstHyp  [\mkleeneopen{}es\mkleeneclose{}]  2\mcdot{}  THENM  (Thin  2  THEN  D  -1))  THEN  Auto)\mcdot{}
              THEN  ((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENM  InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  (-2)\mcdot{}  THENM  Thin  (-3))  THENA  Auto)
              THEN  SplitOrHyps
              THEN  Auto
              THEN  ThinTrivial
              THEN  Eliminate  \mkleeneopen{}f  x\mkleeneclose{}\mcdot{}
              THEN  Eliminate  \mkleeneopen{}f  y\mkleeneclose{}\mcdot{}
              THEN  Try  ((DupHyp  9
                                    THEN  RepUR  ``event-has  class-value-has``  -1
                                    THEN  RepUR  ``event-has  class-value-has``  0
                                    THEN  SplitOrHyps
                                    THEN  ExRepD
                                    THEN  (ThinTrivial\mcdot{}  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  CompleteAuto)))
                                    THEN  (SelectBy  6  THENA  Auto)\mcdot{}
                                    THEN  D  0
                                    THEN  Try  ((NthHypEq  (-1)  THEN  EqCD))
                                    THEN  Complete  (Auto))\mcdot{}))\mcdot{})

---

Home Index