---

Step * of Lemma is-or-latest

∀[Info,A,B:Type].  ∀es:EO+(Info). ∀X:EClass(A). ∀Y:EClass(B). ∀e:E.  (↑e ∈b (X |- Y) ⇐⇒ (↑e ∈b X) ∨ (↑e ∈b Y))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `es-or-latest` 0
   THEN (RWW "es-is-interface-union is-latest-pair" 0 THENA Auto)
   THEN AutoBoolCase ⌜e ∈b X⌝⋅
   THEN AutoBoolCase ⌜e ∈b Y⌝⋅) }

1
1. [Info] : Type
2. [A] : Type
3. [B] : Type
4. es : EO+(Info)@i'
5. X : EClass(A)@i'
6. Y : EClass(B)@i'
7. e : E@i
8. ¬↑e ∈b Y
9. ¬↑e ∈b X
⊢ ((False ∧ (False ∨ (↑e ∈b Prior(Y)))) ∨ (False ∧ (False ∨ (↑e ∈b Prior(X))))) ∨ False ∨ False ⇐⇒ False ∨ False

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(A).  \mforall{}Y:EClass(B).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  (X  |\msupminus{}  Y)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}e  \mmember{}\msubb{}  X)  \mvee{}  (\muparrow{}e  \mmember{}\msubb{}  Y))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `es-or-latest`  0
  THEN  (RWW  "es-is-interface-union  is-latest-pair"  0  THENA  Auto)
  THEN  AutoBoolCase  \mkleeneopen{}e  \mmember{}\msubb{}  X\mkleeneclose{}\mcdot{}
  THEN  AutoBoolCase  \mkleeneopen{}e  \mmember{}\msubb{}  Y\mkleeneclose{}\mcdot{})

---

Home Index