---

Step * 1 1 1 2 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) ≤ eval v = l in
                     if v is a pair then let h,t = v 
                                         in λx.(λ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 
                                                ⊥ 
                                                t 
                                                h) otherwise if v = Ax then λx.x otherwise ⊥ 
                     d
9. is-exception(eval v = l in
                if v is a pair then let h,t = v 
                                    in λx.(λ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 
                                           ⊥ 
                                           t 
                                           h) otherwise if v = Ax then λx.x otherwise ⊥ 
                d)
10. is-exception(l)
⊢ ↓(exception(u; v) ≤ last(l)) ∨ ((l ~ []) ∧ (exception(u; v) ≤ d))
BY
{ TACTIC:(D 0
          THEN (OrLeft THENA Auto)
          THEN ExceptionSqequal (-1)
          THEN DupHyp (-6)
          THEN HypSubst' (-2) (-1)
          THEN HypSubst' (-2) 0
          THEN Reduce (-1)
          THEN RW  (SubC (TagC (mk_tag_term 20))) 0
          THEN Auto) }

---

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{}  eval  v  =  l  in
                                          if  v  is  a  pair  then  let  h,t  =  v 
                                                                                  in  \mlambda{}x.(\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                                                                                        if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                                                                                in  \mlambda{}x.(list$\mbackslash{}ff5\000Cf{ind}$  t  h)
                                                                                                                        otherwise  if  v  =  Ax  then  \mlambda{}x.x
                                                                                                                                            otherwise  \mbot{}\^{}j  -  1 
                                                                                                \mbot{} 
                                                                                                t 
                                                                                                h)  otherwise  if  v  =  Ax  then  \mlambda{}x.x  otherwise  \mbot{} 
                                          d
9.  is-exception(eval  v  =  l  in
                                if  v  is  a  pair  then  let  h,t  =  v 
                                                                        in  \mlambda{}x.(\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                                                                              if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                                                                      in  \mlambda{}x.(list$_\mbackslash{}ff7\000Cbind}$  t  h)
                                                                                                              otherwise  if  v  =  Ax  then  \mlambda{}x.x  otherwise  \mbot{}\^{}j  -\000C  1 
                                                                                      \mbot{} 
                                                                                      t 
                                                                                      h)  otherwise  if  v  =  Ax  then  \mlambda{}x.x  otherwise  \mbot{} 
                                d)
10.  is-exception(l)
\mvdash{}  \mdownarrow{}(exception(u;  v)  \mleq{}  last(l))  \mvee{}  ((l  \msim{}  [])  \mwedge{}  (exception(u;  v)  \mleq{}  d))


By

---

Latex:
TACTIC:(D  0
                THEN  (OrLeft  THENA  Auto)
                THEN  ExceptionSqequal  (-1)
                THEN  DupHyp  (-6)
                THEN  HypSubst'  (-2)  (-1)
                THEN  HypSubst'  (-2)  0
                THEN  Reduce  (-1)
                THEN  RW    (SubC  (TagC  (mk\_tag\_term  20)))  0
                THEN  Auto)

---

Home Index