---

Step * of Lemma prior-or-latest

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  ((X |- Y))' = ((X)' | (Y)') ∈ EClass(one_or_both(A;B)) supposing Singlevalued(X) ∧ Singlevalued(Y)
BY
{ Auto
THEN (Assert ∀es:EO+(Info). ∀e:E.  (↑e ∈b ((X |- Y))' ⇐⇒ ↑e ∈b ((X)' | (Y)')) BY
            RWW "is-prior-val is-or-latest is-interface-or" 0
            THEN Auto
            THEN ExRepD
            THEN SplitOrHyps
            THEN ExRepD
            THEN Try (InstConcl [⌜e'⌝]⋅ THEN Auto)
            THEN Try (OrLeft THEN Complete (Auto))
            THEN Try (OrRight THEN Complete (Auto))) }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. Singlevalued(Y)
8. ∀es:EO+(Info). ∀e:E.  (↑e ∈b ((X |- Y))' ⇐⇒ ↑e ∈b ((X)' | (Y)'))
⊢ ((X |- Y))' = ((X)' | (Y)') ∈ EClass(one_or_both(A;B))

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    ((X  |\msupminus{}  Y))'  =  ((X)'  |  (Y)')  supposing  Singlevalued(X)  \mwedge{}  Singlevalued(Y)


By

---

Latex:
Auto
THEN  (Assert  \mforall{}es:EO+(Info).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  ((X  |\msupminus{}  Y))'  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  ((X)'  |  (Y)'))  BY
                        RWW  "is-prior-val  is-or-latest  is-interface-or"  0
                        THEN  Auto
                        THEN  ExRepD
                        THEN  SplitOrHyps
                        THEN  ExRepD
                        THEN  Try  (InstConcl  [\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}  THEN  Auto)
                        THEN  Try  (OrLeft  THEN  Complete  (Auto))
                        THEN  Try  (OrRight  THEN  Complete  (Auto)))

---

Home Index