---

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


1. l : Base
2. u : Base
3. v : Base
4. j : ℕ
5. exception(u; v) ≤ λselect,n,L. let x,y = L in if (n) < (1)  then x  else eval m = n - 1 in select m y^j ⊥ (||l|| - 1)\000C l
⊢ exception(u; v) ≤ l-last(l)
BY
{ TACTIC:((MoveToConcl 1 THEN NatInd (-1))
          THEN Reduce 0
          THEN Strictness
          THEN (UnivCD THENA Auto)
          THEN Try ((FLemma `exception-not-bottom_1` [-1] THEN Auto))
          THEN (RWO "fun_exp_unroll_1" (-1) THENA Auto)
          THEN Reduce (-1)
          THEN ExceptionCases (-1)) }

1
1. u : Base
2. v : Base
3. j : ℤ
4. 0 < j
5. ∀l:Base
     ((exception(u; v) ≤ λselect,n,L. let x,y = L in if (n) < (1)  then x  else eval m = n - 1 in select m y^j - 1 ⊥ (||\000Cl|| - 1) l)
     ⇒ (exception(u; v) ≤ l-last(l)))
6. l : Base
7. exception(u; v) ≤ let x,y = l 
                     in if (||l|| - 1) < (1)
                           then x
                           else eval m = ||l|| - 1 - 1 in
                                λselect,n,L. let x,y = L in if (n) < (1)  then x  else eval m = n - 1 in select m y^j - \000C1 ⊥ m y
8. is-exception(let x,y = l 
                in if (||l|| - 1) < (1)
                      then x
                      else eval m = ||l|| - 1 - 1 in
                           λselect,n,L. let x,y = L in if (n) < (1)  then x  else eval m = n - 1 in select m y^j - 1 ⊥ m\000C y)
9. l ∈ Top × Top
⊢ exception(u; v) ≤ l-last(l)

2
1. u : Base
2. v : Base
3. j : ℤ
4. 0 < j
5. ∀l:Base
     ((exception(u; v) ≤ λselect,n,L. let x,y = L in if (n) < (1)  then x  else eval m = n - 1 in select m y^j - 1 ⊥ (||\000Cl|| - 1) l)
     ⇒ (exception(u; v) ≤ l-last(l)))
6. l : Base
7. exception(u; v) ≤ let x,y = l 
                     in if (||l|| - 1) < (1)
                           then x
                           else eval m = ||l|| - 1 - 1 in
                                λselect,n,L. let x,y = L in if (n) < (1)  then x  else eval m = n - 1 in select m y^j - \000C1 ⊥ m y
8. is-exception(let x,y = l 
                in if (||l|| - 1) < (1)
                      then x
                      else eval m = ||l|| - 1 - 1 in
                           λselect,n,L. let x,y = L in if (n) < (1)  then x  else eval m = n - 1 in select m y^j - 1 ⊥ m\000C y)
9. is-exception(l)
⊢ exception(u; v) ≤ l-last(l)

---

Latex:

---

Latex:

1.  l  :  Base
2.  u  :  Base
3.  v  :  Base
4.  j  :  \mBbbN{}
5.  exception(u;  v)  \mleq{}  \mlambda{}select,n,L.  let  x,y  =  L 
                                                                    in  if  (n)  <  (1)    then  x    else  eval  m  =  n  -  1  in  select  m  y\^{}j 
                                          \mbot{} 
                                          (||l||  -  1) 
                                          l
\mvdash{}  exception(u;  v)  \mleq{}  l-last(l)


By

---

Latex:
TACTIC:((MoveToConcl  1  THEN  NatInd  (-1))
                THEN  Reduce  0
                THEN  Strictness
                THEN  (UnivCD  THENA  Auto)
                THEN  Try  ((FLemma  `exception-not-bottom\_1`  [-1]  THEN  Auto))
                THEN  (RWO  "fun\_exp\_unroll\_1"  (-1)  THENA  Auto)
                THEN  Reduce  (-1)
                THEN  ExceptionCases  (-1))

---

Home Index