---

Step * of Lemma first-iseg

∀[T:Type]. ∀[P:(T List) ⟶ ℙ].
  ((∀L:T List. Dec(P[L]))
  ⇒ (∀L:T List
        (P[L] ⇒ (∃L':T List. (L' ≤ L ∧ P[L'] ∧ (∀L'':T List. (L'' ≤ L' ⇒ P[L''] ⇒ (L'' = L' ∈ (T List)))))))))
BY
{ xxx(RepeatFor 3 ((D 0 THENA Auto)) THEN InductionOnLength THEN Decide ⌜↑null(L)⌝⋅ THEN Auto)xxx }

1
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
4. n : ℕ
5. L : T List
6. ∀L1:T List
     (||L1|| < ||L||
     ⇒ P[L1]
     ⇒ (∃L':T List. (L' ≤ L1 ∧ P[L'] ∧ (∀L'':T List. (L'' ≤ L' ⇒ P[L''] ⇒ (L'' = L' ∈ (T List)))))))
7. ↑null(L)
8. P[L]
⊢ ∃L':T List. (L' ≤ L ∧ P[L'] ∧ (∀L'':T List. (L'' ≤ L' ⇒ P[L''] ⇒ (L'' = L' ∈ (T List)))))

2
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
4. n : ℕ
5. L : T List
6. ∀L1:T List
     (||L1|| < ||L||
     ⇒ P[L1]
     ⇒ (∃L':T List. (L' ≤ L1 ∧ P[L'] ∧ (∀L'':T List. (L'' ≤ L' ⇒ P[L''] ⇒ (L'' = L' ∈ (T List)))))))
7. ¬↑null(L)
8. P[L]
⊢ ∃L':T List. (L' ≤ L ∧ P[L'] ∧ (∀L'':T List. (L'' ≤ L' ⇒ P[L''] ⇒ (L'' = L' ∈ (T List)))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}L:T  List.  Dec(P[L]))
    {}\mRightarrow{}  (\mforall{}L:T  List
                (P[L]
                {}\mRightarrow{}  (\mexists{}L':T  List.  (L'  \mleq{}  L  \mwedge{}  P[L']  \mwedge{}  (\mforall{}L'':T  List.  (L''  \mleq{}  L'  {}\mRightarrow{}  P[L'']  {}\mRightarrow{}  (L''  =  L'))))))))


By

---

Latex:
xxx(RepeatFor  3  ((D  0  THENA  Auto))  THEN  InductionOnLength  THEN  Decide  \mkleeneopen{}\muparrow{}null(L)\mkleeneclose{}\mcdot{}  THEN  Auto)xxx

---

Home Index