Step
*
2
3
of Lemma
evalall-append-nil
1. j : ℤ
2. 0 < j
3. ∀l:Base
((fix((λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(l @ []))↓
⇒ (λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x^j - 1
⊥
(l @ []))↓
⇒ (l ≤ fix((λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr
eval y = evalall outr(x) in
inr y
else x))
(l @ [])))
4. l : Base@i
5. (fix((λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(inr outr(l @ []) ))↓@i
6. (eval y = λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x^j - 1
⊥
outr(l @ []) in
inr y )↓@i
7. 0 ≤ 0
8. ∀a,b:Top. (b ~ b)
9. ∀a,b:Top. (b ~ b)
10. l @ [] ~ inr outr(l @ [])
⊢ l ≤ eval y = fix((λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall
outr(x) in
inr y
else x))
outr(l @ []) in
inr y
BY
{ ((InstLemma `ispair-or-isaxiom-append-nil` [⌜l⌝]⋅ THENA (Auto THEN HypSubst (-1) 0 THEN Auto))
THEN HypSubst (-2) (-1)
THEN Reduce (-1)
THEN D (-1)
THEN Auto)⋅ }
Latex:
Latex:
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}l:Base
((fix((\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(l @ []))\mdownarrow{}
{}\mRightarrow{} (\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x\^{}j - 1
\mbot{}
(l @ []))\mdownarrow{}
{}\mRightarrow{} (l \mleq{} fix((\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(l @ [])))
4. l : Base@i
5. (fix((\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(inr outr(l @ []) ))\mdownarrow{}@i
6. (eval y = \mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x\^{}j - 1
\mbot{}
outr(l @ []) in
inr y )\mdownarrow{}@i
7. 0 \mleq{} 0
8. \mforall{}a,b:Top. (b \msim{} b)
9. \mforall{}a,b:Top. (b \msim{} b)
10. l @ [] \msim{} inr outr(l @ [])
\mvdash{} l \mleq{} eval y = fix((\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
outr(l @ []) in
inr y
By
Latex:
((InstLemma `ispair-or-isaxiom-append-nil` [\mkleeneopen{}l\mkleeneclose{}]\mcdot{} THENA (Auto THEN HypSubst (-1) 0 THEN Auto))
THEN HypSubst (-2) (-1)
THEN Reduce (-1)
THEN D (-1)
THEN Auto)\mcdot{}
Home
Index