---

Step * 1 1 1 1 1 of Lemma l-last-is-last


1. u : Base@i
2. v : Base@i
3. j : ℤ
4. 0 < j
5. ∀l,d:Base.
     ((exception(u; v) ≤ λlist_ind,L. eval v = L in
                                      if v is a pair then let h,t = v 
                                                          in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥\000C^j - 1 
                         ⊥ 
                         l 
                         d)
     ⇒ (↓(exception(u; v) ≤ last(l)) ∨ ((l ~ []) ∧ (exception(u; v) ≤ d))))
6. l : Base@i
7. d : Base@i
8. exception(u; v) ≤ λlist_ind,L. eval v = L in
                                  if v is a pair then let h,t = v 
                                                      in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥^j -\000C 1 
                     ⊥ 
                     (snd(l)) 
                     (fst(l))
9. 0 ≤ 0
10. l ~ <fst(l), snd(l)>
11. (exception(u; v) ≤ last(snd(l))) ∨ ((snd(l) ~ []) ∧ (exception(u; v) ≤ fst(l)))
⊢ exception(u; v) ≤ last(<fst(l), snd(l)>)
BY
{ TACTIC:(Fold `cons` 0 THEN D -1) }

1
1. u : Base@i
2. v : Base@i
3. j : ℤ
4. 0 < j
5. ∀l,d:Base.
     ((exception(u; v) ≤ λlist_ind,L. eval v = L in
                                      if v is a pair then let h,t = v 
                                                          in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥\000C^j - 1 
                         ⊥ 
                         l 
                         d)
     ⇒ (↓(exception(u; v) ≤ last(l)) ∨ ((l ~ []) ∧ (exception(u; v) ≤ d))))
6. l : Base@i
7. d : Base@i
8. exception(u; v) ≤ λlist_ind,L. eval v = L in
                                  if v is a pair then let h,t = v 
                                                      in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥^j -\000C 1 
                     ⊥ 
                     (snd(l)) 
                     (fst(l))
9. 0 ≤ 0
10. l ~ <fst(l), snd(l)>
11. exception(u; v) ≤ last(snd(l))
⊢ exception(u; v) ≤ last([fst(l) / (snd(l))])

2
1. u : Base@i
2. v : Base@i
3. j : ℤ
4. 0 < j
5. ∀l,d:Base.
     ((exception(u; v) ≤ λlist_ind,L. eval v = L in
                                      if v is a pair then let h,t = v 
                                                          in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥\000C^j - 1 
                         ⊥ 
                         l 
                         d)
     ⇒ (↓(exception(u; v) ≤ last(l)) ∨ ((l ~ []) ∧ (exception(u; v) ≤ d))))
6. l : Base@i
7. d : Base@i
8. exception(u; v) ≤ λlist_ind,L. eval v = L in
                                  if v is a pair then let h,t = v 
                                                      in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥^j -\000C 1 
                     ⊥ 
                     (snd(l)) 
                     (fst(l))
9. 0 ≤ 0
10. l ~ <fst(l), snd(l)>
11. (snd(l) ~ []) ∧ (exception(u; v) ≤ fst(l))
⊢ exception(u; v) ≤ last([fst(l) / (snd(l))])

---

Latex:

---

Latex:

1.  u  :  Base@i
2.  v  :  Base@i
3.  j  :  \mBbbZ{}
4.  0  <  j
5.  \mforall{}l,d:Base.
          ((exception(u;  v)  \mleq{}  \mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                                          if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                                  in  \mlambda{}x.(list$_{ind}$  t  h\000C)
                                                                          otherwise  if  v  =  Ax  then  \mlambda{}x.x  otherwise  \mbot{}\^{}j  -  1 
                                                  \mbot{} 
                                                  l 
                                                  d)
          {}\mRightarrow{}  (\mdownarrow{}(exception(u;  v)  \mleq{}  last(l))  \mvee{}  ((l  \msim{}  [])  \mwedge{}  (exception(u;  v)  \mleq{}  d))))
6.  l  :  Base@i
7.  d  :  Base@i
8.  exception(u;  v)  \mleq{}  \mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                                  if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                          in  \mlambda{}x.(list$_{ind}$  t  h)
                                                                  otherwise  if  v  =  Ax  then  \mlambda{}x.x  otherwise  \mbot{}\^{}j  -  1 
                                          \mbot{} 
                                          (snd(l)) 
                                          (fst(l))
9.  0  \mleq{}  0
10.  l  \msim{}  <fst(l),  snd(l)>
11.  (exception(u;  v)  \mleq{}  last(snd(l)))  \mvee{}  ((snd(l)  \msim{}  [])  \mwedge{}  (exception(u;  v)  \mleq{}  fst(l)))
\mvdash{}  exception(u;  v)  \mleq{}  last(<fst(l),  snd(l)>)


By

---

Latex:
TACTIC:(Fold  `cons`  0  THEN  D  -1)

---

Home Index