---

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


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) ≤ if (||<fst(l), snd(l)>|| - 1) < (1)
                        then fst(l)
                        else eval m = ||<fst(l), snd(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 ⊥\000C m (snd(l))
8. l ∈ Top × Top
9. ||<fst(l), snd(l)>|| - 1 ∈ ℤ
10. 1 ∈ ℤ
11. (||<fst(l), snd(l)>|| + (-1))↓
12. ||<fst(l), snd(l)>|| ∈ ℤ
13. -1 ∈ ℤ
⊢ exception(u; v) ≤ l-last(<fst(l), snd(l)>)
BY
{ TACTIC:TACTIC:((Decide ⌜||<fst(l), snd(l)>|| - 1 < 1⌝⋅ THENA Auto) THEN (Reduce 7 THENA Auto)) }

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) ≤ fst(l)
8. l ∈ Top × Top
9. ||<fst(l), snd(l)>|| - 1 ∈ ℤ
10. 1 ∈ ℤ
11. (||<fst(l), snd(l)>|| + (-1))↓
12. ||<fst(l), snd(l)>|| ∈ ℤ
13. -1 ∈ ℤ
14. ||<fst(l), snd(l)>|| - 1 < 1
⊢ exception(u; v) ≤ l-last(<fst(l), snd(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) ≤ eval m = ||<fst(l), snd(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 (snd(\000Cl))
8. l ∈ Top × Top
9. ||<fst(l), snd(l)>|| - 1 ∈ ℤ
10. 1 ∈ ℤ
11. (||<fst(l), snd(l)>|| + (-1))↓
12. ||<fst(l), snd(l)>|| ∈ ℤ
13. -1 ∈ ℤ
14. ¬||<fst(l), snd(l)>|| - 1 < 1
⊢ exception(u; v) ≤ l-last(<fst(l), snd(l)>)

---

Latex:

---

Latex:

1.  u  :  Base
2.  v  :  Base
3.  j  :  \mBbbZ{}
4.  0  <  j
5.  \mforall{}l:Base
          ((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  -\000C  1 
                                                  \mbot{} 
                                                  (||l||  -  1) 
                                                  l)
          {}\mRightarrow{}  (exception(u;  v)  \mleq{}  l-last(l)))
6.  l  :  Base
7.  exception(u;  v)  \mleq{}  if  (||<fst(l),  snd(l)>||  -  1)  <  (1)
                                                then  fst(l)
                                                else  eval  m  =  ||<fst(l),  snd(l)>||  -  1  -  1  in
                                                          \mlambda{}select,n,L.  let  x,y  =  L 
                                                                                    in  if  (n)  <  (1)    then  x    else  eval  m  =  n  -  1  in  select  m  y\000C\^{}j  -  1 
                                                          \mbot{} 
                                                          m 
                                                          (snd(l))
8.  l  \mmember{}  Top  \mtimes{}  Top
9.  ||<fst(l),  snd(l)>||  -  1  \mmember{}  \mBbbZ{}
10.  1  \mmember{}  \mBbbZ{}
11.  (||<fst(l),  snd(l)>||  +  (-1))\mdownarrow{}
12.  ||<fst(l),  snd(l)>||  \mmember{}  \mBbbZ{}
13.  -1  \mmember{}  \mBbbZ{}
\mvdash{}  exception(u;  v)  \mleq{}  l-last(<fst(l),  snd(l)>)


By

---

Latex:
TACTIC:TACTIC:((Decide  \mkleeneopen{}||<fst(l),  snd(l)>||  -  1  <  1\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (Reduce  7  THENA  Auto))

---

Home Index