---

Step * 1 of Lemma or-latest-val


1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. X : EClass(A)
6. Y : EClass(B)
7. e : E
8. (↑e ∈b X) ∨ (↑e ∈b Y)
9. Singlevalued(X)
10. Singlevalued(Y)
⊢ (X |- Y)(e) = ((X)- | (Y)-)(e) ∈ one_or_both(A;B)
BY
{ (RepUR ``eclass-val es-or-latest es-interface-or es-interface-union`` 0⋅
   THEN (RepUR ``eclass-compose2 eclass-compose4 latest-pair es-latest-val`` 0⋅ THEN RepUR ``oob-apply`` 0)
   THEN Fold `in-eclass` 0
   THEN RepeatFor 2 (AutoSplit)
   THEN Try (Complete ((SplitOrHyps THEN Auto)))) }

1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. X : EClass(A)
6. Y : EClass(B)
7. e : E
8. ¬↑e ∈b Y
9. (↑e ∈b X) ∨ False
10. Singlevalued(X)
11. Singlevalued(Y)
12. ↑e ∈b X
⊢ only(if (#(if e ∈b Prior(Y) then {<only(X es e), only(Prior(Y) es e)>} else {} fi ) =z 1)
then {inl only(if e ∈b Prior(Y) then {<only(X es e), only(Prior(Y) es e)>} else {} fi )}
else {inr (inl only(X es e)) }
fi )
= only(if (#((Y)' es e) =z 1) then {oobboth(<X(e), only((Y)' es e)>)} else {oobleft(X(e))} fi )
∈ one_or_both(A;B)

2
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. X : EClass(A)
6. Y : EClass(B)
7. e : E
8. ¬↑e ∈b X
9. False ∨ (↑e ∈b Y)
10. Singlevalued(X)
11. Singlevalued(Y)
12. ↑e ∈b Y
⊢ only(if (#(if e ∈b Prior(X) then {<only(Prior(X) es e), only(Y es e)>} else {} fi ) =z 1)
then {inl only(if e ∈b Prior(X) then {<only(Prior(X) es e), only(Y es e)>} else {} fi )}
else {inr inr only(Y es e)  }
fi )
= only(if (#((X)' es e) =z 1) then {oobboth(<only((X)' es e), Y(e)>)} else {oobright(Y(e))} fi )
∈ one_or_both(A;B)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  A  :  Type
4.  B  :  Type
5.  X  :  EClass(A)
6.  Y  :  EClass(B)
7.  e  :  E
8.  (\muparrow{}e  \mmember{}\msubb{}  X)  \mvee{}  (\muparrow{}e  \mmember{}\msubb{}  Y)
9.  Singlevalued(X)
10.  Singlevalued(Y)
\mvdash{}  (X  |\msupminus{}  Y)(e)  =  ((X)\msupminus{}  |  (Y)\msupminus{})(e)


By

---

Latex:
(RepUR  ``eclass-val  es-or-latest  es-interface-or  es-interface-union``  0\mcdot{}
  THEN  (RepUR  ``eclass-compose2  eclass-compose4  latest-pair  es-latest-val``  0\mcdot{}
              THEN  RepUR  ``oob-apply``  0
              )
  THEN  Fold  `in-eclass`  0
  THEN  RepeatFor  2  (AutoSplit)
  THEN  Try  (Complete  ((SplitOrHyps  THEN  Auto))))

---

Home Index