---

Step * of Lemma latest-val-val

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[T:Type]
      ∀X:EClass(T). ∀e:E.
        ∃e':E
         (e' ≤loc e  ∧ (↑e' ∈b X) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑e'' ∈b X))) ∧ ((X)-(e) = X(e') ∈ T)) 
        supposing ↑e ∈b (X)-
BY
{ ((UnivCD THENA Auto) THEN (RWO "latest-val-cases" (-1) THENM D -1) THEN Auto) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. e : E@i
6. ↑e ∈b (X)'
7. ¬↑e ∈b X
8. (X)-(e) = (X)'(e) ∈ T
⊢ ∃e':E. (e' ≤loc e  ∧ (↑e' ∈b X) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑e'' ∈b X))) ∧ ((X)-(e) = X(e') ∈ T))

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[T:Type]
            \mforall{}X:EClass(T).  \mforall{}e:E.
                \mexists{}e':E
                  (e'  \mleq{}loc  e 
                  \mwedge{}  (\muparrow{}e'  \mmember{}\msubb{}  X)
                  \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}e''  \mmember{}\msubb{}  X)))
                  \mwedge{}  ((X)\msupminus{}(e)  =  X(e'))) 
                supposing  \muparrow{}e  \mmember{}\msubb{}  (X)\msupminus{}


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "latest-val-cases"  (-1)  THENM  D  -1)  THEN  Auto)

---

Home Index