---

Step * 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. ↑e ∈b X
⊢ 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
{ (RepUR ``in-eclass`` -1
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN (Assert single-valued-bag(X es e;T) BY
               (BLemma `single-valued-bag-if-le1` THEN Auto))) }

1
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))

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [T]  :  Type
4.  X  :  EClass(T)@i'
5.  e  :  E@i
6.  \muparrow{}e  \mmember{}\msubb{}  X
\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:
(RepUR  ``in-eclass``  -1
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  (Assert  single-valued-bag(X  es  e;T)  BY
                          (BLemma  `single-valued-bag-if-le1`  THEN  Auto)))

---

Home Index