---

Step * 2 2 1 2 1 1 of Lemma first-iseg

.....subterm..... T:t
2:n
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]))
12. L ≤ L
13. P[L]
14. L'' : T List
15. l : T List
16. 0 < ||l||
17. L'' = (L' @ l) ∈ (T List)
18. l ≤ [last(L)]
19. P[L'']
⊢ l = [last(L)] ∈ (T List)
BY
{ xxx(((DVar `l'
        THEN All Reduce
        THEN Auto
        THEN (RWO "cons_iseg" (-2))
        THEN Auto
        THEN EqCD
        THEN Auto
        THEN (RWO "iseg_nil" (-2)))
       THENA Auto
       )
      THEN (RW assert_pushdownC (-2))
      THEN Auto)xxx }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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]
9.  L'  :  T  List
10.  L  =  (L'  @  [last(L)])
11.  \mneg{}(\mexists{}zs:T  List.  (zs  \mleq{}  L'  \mwedge{}  P[zs]))
12.  L  \mleq{}  L
13.  P[L]
14.  L''  :  T  List
15.  l  :  T  List
16.  0  <  ||l||
17.  L''  =  (L'  @  l)
18.  l  \mleq{}  [last(L)]
19.  P[L'']
\mvdash{}  l  =  [last(L)]


By

---

Latex:
xxx(((DVar  `l'
            THEN  All  Reduce
            THEN  Auto
            THEN  (RWO  "cons\_iseg"  (-2))
            THEN  Auto
            THEN  EqCD
            THEN  Auto
            THEN  (RWO  "iseg\_nil"  (-2)))
          THENA  Auto
          )
        THEN  (RW  assert\_pushdownC  (-2))
        THEN  Auto)xxx

---

Home Index