---

Step * 1 1 1 of Lemma latest-val-cases


1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. e : E@i
6. #(X es e) = 1 ∈ ℤ
7. single-valued-bag(X es e;T)
⊢ True
⇐⇒ (True ∧ (only(X es e) = only(X es e) ∈ T)) ∨ (((↑e ∈b (X)') ∧ (¬True)) ∧ (only(X es e) = only((X)' es e) ∈ T))
BY
{ Auto }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [T]  :  Type
4.  X  :  EClass(T)@i'
5.  e  :  E@i
6.  \#(X  es  e)  =  1
7.  single-valued-bag(X  es  e;T)
\mvdash{}  True
\mLeftarrow{}{}\mRightarrow{}  (True  \mwedge{}  (only(X  es  e)  =  only(X  es  e)))
        \mvee{}  (((\muparrow{}e  \mmember{}\msubb{}  (X)')  \mwedge{}  (\mneg{}True))  \mwedge{}  (only(X  es  e)  =  only((X)'  es  e)))


By

---

Latex:
Auto

---

Home Index