Step
*
1
1
2
of Lemma
evalall-append-implies-list-base
1. j : ℤ
2. 0 < j
3. ∀a,b:Base.
((λ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
⊥
(a @ b))↓
⇒ (a ∈ Base List))
4. a : Base@i
5. b : Base@i
6. (if a @ b is a pair then let a,b = a @ b
in eval a' = λ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
⊥
a in
eval b' = λ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
⊥
b in
<a', b'>
otherwise if a @ b is inl then 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
⊥
outl(a @ b) in
inl y
else if a @ b is inr then 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(a @ b) in
inr y
else a @ b)↓@i
7. (if a = Ax then b otherwise ⊥)↓
8. (a)↓
9. ∀a@0,b:Top. (if a is a pair then a@0 otherwise b ~ b)
⊢ a ∈ Base List
BY
{ (HVimplies2 (-3) [1] THEN BotDiv) }
Latex:
Latex:
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}a,b:Base.
((\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
eval y = evalall outr(x) in
inr y
else x\^{}j - 1
\mbot{}
(a @ b))\mdownarrow{}
{}\mRightarrow{} (a \mmember{} Base List))
4. a : Base@i
5. b : Base@i
6. (if a @ b is a pair then let a,b = a @ b
in eval a' = \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
eval y = evalall outr(x) in
inr y
else x\^{}j - 1
\mbot{}
a in
eval b' = \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
eval y = evalall outr(x) in
inr y
else x\^{}j - 1
\mbot{}
b in
<a', b'>
otherwise if a @ b is inl
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{}
outl(a @ b) in
inl y
else if a @ b is inr
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(a @ b) in
inr y
else a @ b)\mdownarrow{}@i
7. (if a = Ax then b otherwise \mbot{})\mdownarrow{}
8. (a)\mdownarrow{}
9. \mforall{}a@0,b:Top. (if a is a pair then a@0 otherwise b \msim{} b)
\mvdash{} a \mmember{} Base List
By
Latex:
(HVimplies2 (-3) [1] THEN BotDiv)
Home
Index