---

Step * of Lemma cut-list-maximal-exists

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀a:E(X) List.
    ((¬(a = {} ∈ fset(E(X))))
    ⇒ (∃e:E(X)
         ((e ∈ a)
         ∧ (∀e':E(X). ((e' ∈ a) ⇒ (e = (X-pred e') ∈ E(X)) ⇒ (e' = e ∈ E(X))))
         ∧ (∀e':E(X). ((e' ∈ a) ⇒ (e = (f e') ∈ E(X)) ⇒ (e' = e ∈ E(X)))))))
BY
{ (Auto THEN DVar `a') }

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

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. u : E(X)
6. v : E(X) List
7. ¬([u / v] = {} ∈ fset(E(X)))@i
⊢ ∃e:E(X)
   ((e ∈ [u / v])
   ∧ (∀e':E(X). ((e' ∈ [u / v]) ⇒ (e = (X-pred e') ∈ E(X)) ⇒ (e' = e ∈ E(X))))
   ∧ (∀e':E(X). ((e' ∈ [u / v]) ⇒ (e = (f e') ∈ E(X)) ⇒ (e' = e ∈ E(X)))))

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:sys-antecedent(es;X).  \mforall{}a:E(X)  List.
        ((\mneg{}(a  =  \{\}))
        {}\mRightarrow{}  (\mexists{}e:E(X)
                  ((e  \mmember{}  a)
                  \mwedge{}  (\mforall{}e':E(X).  ((e'  \mmember{}  a)  {}\mRightarrow{}  (e  =  (X-pred  e'))  {}\mRightarrow{}  (e'  =  e)))
                  \mwedge{}  (\mforall{}e':E(X).  ((e'  \mmember{}  a)  {}\mRightarrow{}  (e  =  (f  e'))  {}\mRightarrow{}  (e'  =  e))))))


By

---

Latex:
(Auto  THEN  DVar  `a')

---

Home Index