---

Step * 1 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))
⊢ exception(u; v) ≤ last([fst(l) / (snd(l))])
BY
{ TACTIC:(DupHyp (-1) THEN Unfold `last` -1 THEN RecUnfold `select` (-1) THEN ExceptionCases (-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))
12. exception(u; v) ≤ let x,y = snd(l) 
                      in if (||snd(l)|| - 1) < (1)  then x  else eval m = ||snd(l)|| - 1 - 1 in y[m]
13. is-exception(let x,y = snd(l) 
                 in if (||snd(l)|| - 1) < (1)  then x  else eval m = ||snd(l)|| - 1 - 1 in y[m])
14. snd(l) ∈ Top × Top
⊢ 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. exception(u; v) ≤ last(snd(l))
12. exception(u; v) ≤ let x,y = snd(l) 
                      in if (||snd(l)|| - 1) < (1)  then x  else eval m = ||snd(l)|| - 1 - 1 in y[m]
13. is-exception(let x,y = snd(l) 
                 in if (||snd(l)|| - 1) < (1)  then x  else eval m = ||snd(l)|| - 1 - 1 in y[m])
14. is-exception(snd(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))
\mvdash{}  exception(u;  v)  \mleq{}  last([fst(l)  /  (snd(l))])


By

---

Latex:
TACTIC:(DupHyp  (-1)  THEN  Unfold  `last`  -1  THEN  RecUnfold  `select`  (-1)  THEN  ExceptionCases  (-1))

---

Home Index