---

Step * 1 of Lemma cut-list-maximal-exists


1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. ¬([] = {} ∈ fset(E(X)))@i
⊢ ∃e:E(X)
   ((e ∈ [])
   ∧ (∀e':E(X). ((e' ∈ []) ⇒ (e = (X-pred e') ∈ E(X)) ⇒ (e' = e ∈ E(X))))
   ∧ (∀e':E(X). ((e' ∈ []) ⇒ (e = (f e') ∈ E(X)) ⇒ (e' = e ∈ E(X)))))
BY
{ ((D (-1) THEN Fold `empty-fset` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  f  :  sys-antecedent(es;X)@i
5.  \mneg{}([]  =  \{\})@i
\mvdash{}  \mexists{}e:E(X)
      ((e  \mmember{}  [])
      \mwedge{}  (\mforall{}e':E(X).  ((e'  \mmember{}  [])  {}\mRightarrow{}  (e  =  (X-pred  e'))  {}\mRightarrow{}  (e'  =  e)))
      \mwedge{}  (\mforall{}e':E(X).  ((e'  \mmember{}  [])  {}\mRightarrow{}  (e  =  (f  e'))  {}\mRightarrow{}  (e'  =  e))))


By

---

Latex:
((D  (-1)  THEN  Fold  `empty-fset`  0)  THEN  Auto)

---

Home Index