---

Step * 2 of Lemma first-iseg


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)))))
BY
{ xxx(((FLemma `last_lemma` [(-2)]) THENA Auto)
      THEN ExRepD
      THEN AssertBY ⌜Dec(∃zs:T List. (zs ≤ L' ∧ P[zs]))⌝
         (BLemma `decidable-exists-iseg` THEN Auto)⋅
      THEN (D (-1)))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]
9. L' : T List
10. L = (L' @ [last(L)]) ∈ (T List)
11. ∃zs:T List. (zs ≤ L' ∧ P[zs])
⊢ ∃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]
9. L' : T List
10. L = (L' @ [last(L)]) ∈ (T List)
11. ¬(∃zs:T List. (zs ≤ L' ∧ P[zs]))
⊢ ∃L':T List. (L' ≤ L ∧ P[L'] ∧ (∀L'':T List. (L'' ≤ L' ⇒ P[L''] ⇒ (L'' = L' ∈ (T List)))))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}L:T  List.  Dec(P[L])
4.  n  :  \mBbbN{}
5.  L  :  T  List
6.  \mforall{}L1:T  List
          (||L1||  <  ||L||
          {}\mRightarrow{}  P[L1]
          {}\mRightarrow{}  (\mexists{}L':T  List.  (L'  \mleq{}  L1  \mwedge{}  P[L']  \mwedge{}  (\mforall{}L'':T  List.  (L''  \mleq{}  L'  {}\mRightarrow{}  P[L'']  {}\mRightarrow{}  (L''  =  L'))))))
7.  \mneg{}\muparrow{}null(L)
8.  P[L]
\mvdash{}  \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(((FLemma  `last\_lemma`  [(-2)])  THENA  Auto)
        THEN  ExRepD
        THEN  AssertBY  \mkleeneopen{}Dec(\mexists{}zs:T  List.  (zs  \mleq{}  L'  \mwedge{}  P[zs]))\mkleeneclose{}
              (BLemma  `decidable-exists-iseg`  THEN  Auto)\mcdot{}
        THEN  (D  (-1)))xxx

---

Home Index