---

Step * 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. is-exception(λ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 - 1 
                ⊥ 
                (snd(l)) 
                (fst(l)))
10. 0 ≤ 0
11. l ~ <fst(l), snd(l)>
⊢ ↓(exception(u; v) ≤ last(<fst(l), snd(l)>)) ∨ ((<fst(l), snd(l)> ~ []) ∧ (exception(u; v) ≤ d))
BY
{ TACTIC:(Thin (-3) THEN (FHyp 5 [-3] THENA Auto) THEN ParallelLast THEN (OrLeft THENA Auto)) }

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))) ∨ ((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.  is-exception(\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)))
10.  0  \mleq{}  0
11.  l  \msim{}  <fst(l),  snd(l)>
\mvdash{}  \mdownarrow{}(exception(u;  v)  \mleq{}  last(<fst(l),  snd(l)>))  \mvee{}  ((<fst(l),  snd(l)>  \msim{}  [])  \mwedge{}  (exception(u;  v)  \mleq{}  d))


By

---

Latex:
TACTIC:(Thin  (-3)  THEN  (FHyp  5  [-3]  THENA  Auto)  THEN  ParallelLast  THEN  (OrLeft  THENA  Auto))

---

Home Index