Step
*
1
1
1
of Lemma
l-last-is-last
1. l : Base@i
2. u : Base@i
3. v : Base@i
4. j : ℕ
5. 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
⊥
l
⊥
⊢ exception(u; v) ≤ last(l)
BY
{ TACTIC:((Assert ⌜∀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 ⊥^j
⊥
l
d)
⇒ (↓(exception(u; v) ≤ last(l)) ∨ ((l ~ []) ∧ (exception(u; v) ≤ d))))⌝⋅
THENM ((InstHyp [⌜l⌝;⌜⊥⌝] (-1)⋅ THENA Auto)
THEN SquashConcl
THEN RepeatFor 2 (D -1)
THEN Try ((D -1 THEN FLemma `exception-not-bottom_1` [-1] THEN Auto))
THEN Auto)
)
THEN All Thin
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 RW (AddrC [2] (LiftC true)) (-1)
THEN ExceptionCases (-1)
THEN Try (((CallByValueReduce (-2) THENA Trivial) THEN HVimplies2 (-2) [1;1]))
THEN Try ((HVimplies2 (-3) [1;1]
THEN (Complete (((D 0 THEN OrRight) THEN RepUR ``nil it`` 0 THEN Auto))
ORELSE ((Subst' ⊥ d ~ ⊥ -4 THENA Auto) THEN FLemma `exception-not-bottom` [-4] THEN 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. 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))
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) ≤ 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))
Latex:
Latex:
1. l : Base@i
2. u : Base@i
3. v : Base@i
4. j : \mBbbN{}
5. 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
\mbot{}
l
\mbot{}
\mvdash{} exception(u; v) \mleq{} last(l)
By
Latex:
TACTIC:((Assert \mkleeneopen{}\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\000C}$ t h)
otherwise if v = Ax then \mlambda{}x.x otherwise \mbot{}\^{}j
\mbot{}
l
d)
{}\mRightarrow{} (\mdownarrow{}(exception(u; v) \mleq{} last(l)) \mvee{} ((l \msim{} []) \mwedge{} (exception(u; v) \mleq{} d))))\mkleeneclose{}\mcdot{}
THENM ((InstHyp [\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}\mbot{}\mkleeneclose{}] (-1)\mcdot{} THENA Auto)
THEN SquashConcl
THEN RepeatFor 2 (D -1)
THEN Try ((D -1 THEN FLemma `exception-not-bottom\_1` [-1] THEN Auto))
THEN Auto)
)
THEN All Thin
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 RW (AddrC [2] (LiftC true)) (-1)
THEN ExceptionCases (-1)
THEN Try (((CallByValueReduce (-2) THENA Trivial) THEN HVimplies2 (-2) [1;1]))
THEN Try ((HVimplies2 (-3) [1;1]
THEN (Complete (((D 0 THEN OrRight) THEN RepUR ``nil it`` 0 THEN Auto))
ORELSE ((Subst' \mbot{} d \msim{} \mbot{} -4 THENA Auto)
THEN FLemma `exception-not-bottom` [-4]
THEN Auto)
)
)))
Home
Index