Step
*
1
1
of Lemma
evalall-append-sqle
1. j : ℤ
2. 0 < j
3. ∀a,b:Base.
(evalall(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then b otherwise ⊥^j - 1
⊥
a) ≤ eval u = evalall(a) in
eval v = evalall(b) in
evalall(u @ v))
4. a : Base
5. b : Base
6. 0 ≤ 0
7. a ~ <fst(a), snd(a)>
8. (evalall(fst(a)))↓
9. evalall(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then snd(a) otherwise ⊥^j - 1
⊥
b) ≤ eval u = evalall(b) in
eval v = evalall(snd(a)) in
evalall(u @ v)
⊢ eval b' = evalall(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then b otherwise ⊥^j - \000C1
⊥
(snd(a))) in
<evalall(fst(a)), b'> ≤ eval u = eval b' = evalall(snd(a)) in
<evalall(fst(a)), b'> in
eval v = evalall(b) in
evalall(u @ v)
BY
{ TACTIC:((Assert ⌜eval b' = evalall(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then b
otherwise ⊥^j - \000C1
⊥
(snd(a))) in
<evalall(fst(a)), b'> ≤ eval b' = eval u = evalall(snd(a)) in
eval v = evalall(b) in
evalall(u @ v) in
<evalall(fst(a)), b'>⌝⋅
THENA Auto
)
THEN SqLeTrans (-1)
THEN Try (NthHyp (-1))) }
1
1. j : ℤ
2. 0 < j
3. ∀a,b:Base.
(evalall(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then b otherwise ⊥^j - 1
⊥
a) ≤ eval u = evalall(a) in
eval v = evalall(b) in
evalall(u @ v))
4. a : Base
5. b : Base
6. 0 ≤ 0
7. a ~ <fst(a), snd(a)>
8. (evalall(fst(a)))↓
9. evalall(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then snd(a) otherwise ⊥^j - 1
⊥
b) ≤ eval u = evalall(b) in
eval v = evalall(snd(a)) in
evalall(u @ v)
10. eval b' = evalall(λlist_ind,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list_ind as')] otherwise if v = Ax then b otherwise ⊥^j \000C- 1
⊥
(snd(a))) in
<evalall(fst(a)), b'> ≤ eval b' = eval u = evalall(snd(a)) in
eval v = evalall(b) in
evalall(u @ v) in
<evalall(fst(a)), b'>
⊢ eval b' = eval u = evalall(snd(a)) in
eval v = evalall(b) in
evalall(u @ v) in
<evalall(fst(a)), b'> ≤ eval u = eval b' = evalall(snd(a)) in
<evalall(fst(a)), b'> in
eval v = evalall(b) in
evalall(u @ v)
Latex:
Latex:
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}a,b:Base.
(evalall(\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list$_{ind}$ as')]
otherwise if v = Ax then b otherwise \mbot{}\^{}j - 1
\mbot{}
a) \mleq{} eval u = evalall(a) in
eval v = evalall(b) in
evalall(u @ v))
4. a : Base
5. b : Base
6. 0 \mleq{} 0
7. a \msim{} <fst(a), snd(a)>
8. (evalall(fst(a)))\mdownarrow{}
9. evalall(\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list$_{ind}$ as')]
otherwise if v = Ax then snd(a) otherwise \mbot{}\^{}j - 1
\mbot{}
b) \mleq{} eval u = evalall(b) in
eval v = evalall(snd(a)) in
evalall(u @ v)
\mvdash{} eval b' = evalall(\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list$_{ind}$ as')]
otherwise if v = Ax then b otherwise \mbot{}\^{}j - 1
\mbot{}
(snd(a))) in
<evalall(fst(a)), b'> \mleq{} eval u = eval b' = evalall(snd(a)) in
<evalall(fst(a)), b'> in
eval v = evalall(b) in
evalall(u @ v)
By
Latex:
TACTIC:((Assert \mkleeneopen{}eval b' = evalall(\mlambda{}list$_{ind}$,L. eval v = L in
if v is a pair then let a,as' = v
in [a / (list$_{ind\mbackslash{}f\000Cf7d$ as')]
otherwise if v = Ax then b otherwise \mbot{}\^{}j - 1
\mbot{}
(snd(a))) in
<evalall(fst(a)), b'> \mleq{} eval b' = eval u = evalall(snd(a)) in
eval v = evalall(b) in
evalall(u @ v) in
<evalall(fst(a)), b'>\mkleeneclose{}\mcdot{}
THENA Auto
)
THEN SqLeTrans (-1)
THEN Try (NthHyp (-1)))
Home
Index