---

Step * 2 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. 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)))))
BY
{ ((RWO "l_all_iff<" 0 THENA Auto)
   THEN (RWO "l_exists_iff<" 0 THENA Auto)
   THEN (SupposeNot THENA Auto)
   THEN Assert ⌈False⌉⋅
   THEN Auto
   THEN (RWW "not-l_exists not_over_and not-l_all-dec l_exists_or not_over_implies not_over_not" (-1)⋅ THENA Auto)
   THEN (RWO "l_all_iff l_exists_iff" (-1) THENA Auto)) }

1
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
8. ∀e:E(X)
     ((e ∈ [u / v])
     ⇒ (∃e'∈[u / v]. ((e = (X-pred e') ∈ E(X)) ∧ (¬(e' = e ∈ E(X)))) ∨ ((e = (f e') ∈ E(X)) ∧ (¬(e' = e ∈ E(X))))))
⊢ False

---

Latex:

---

Latex:

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.  \mneg{}([u  /  v]  =  \{\})@i
\mvdash{}  \mexists{}e:E(X)
      ((e  \mmember{}  [u  /  v])
      \mwedge{}  (\mforall{}e':E(X).  ((e'  \mmember{}  [u  /  v])  {}\mRightarrow{}  (e  =  (X-pred  e'))  {}\mRightarrow{}  (e'  =  e)))
      \mwedge{}  (\mforall{}e':E(X).  ((e'  \mmember{}  [u  /  v])  {}\mRightarrow{}  (e  =  (f  e'))  {}\mRightarrow{}  (e'  =  e))))


By

---

Latex:
((RWO  "l\_all\_iff<"  0  THENA  Auto)
  THEN  (RWO  "l\_exists\_iff<"  0  THENA  Auto)
  THEN  (SupposeNot  THENA  Auto)
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (RWW  "not-l\_exists  not\_over\_and  not-l\_all-dec  l\_exists\_or  not\_over\_implies  not\_over\_not"  (-1)\mcdot{}
              THENA  Auto
              )
  THEN  (RWO  "l\_all\_iff  l\_exists\_iff"  (-1)  THENA  Auto))

---

Home Index