Step
*
1
1
1
2
1
2
of Lemma
rec-value-evalall
1. j : ℤ
2. 0 < j
3. ∀x: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
⊥
x)↓
⇒ (x ∈ rec-value()))
4. x : Base@i
5. (if x 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(x) in
inl y
else if x 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(x) in
inr y
else x)↓
6. (x)↓
7. ∀a,b:Base. (if x is a pair then a otherwise b ~ b)
8. ∀a,b:Base. (if x is inl then a else b ~ b)
⊢ x ∈ rec-value()
BY
{ (( RWO "-1" (-4)⋅ THENA Complete (Auto)) THEN HasValueImplies2 5 [1]) }
1
1. j : ℤ
2. 0 < j
3. ∀x: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
⊥
x)↓
⇒ (x ∈ rec-value()))
4. x : Base@i
5. (if x 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(x) in
inr y
else x)↓
6. (x)↓
7. ∀a,b:Base. (if x is a pair then a otherwise b ~ b)
8. ∀a,b:Base. (if x is inl then a else b ~ b)
9. x ~ inr outr(x)
⊢ x ∈ rec-value()
2
1. j : ℤ
2. 0 < j
3. ∀x: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
⊥
x)↓
⇒ (x ∈ rec-value()))
4. x : Base@i
5. (if x 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(x) in
inr y
else x)↓
6. (x)↓
7. ∀a,b:Base. (if x is a pair then a otherwise b ~ b)
8. ∀a,b:Base. (if x is inl then a else b ~ b)
9. ∀a,b:Base. (if x is inr then a else b ~ b)
⊢ x ∈ rec-value()
Latex:
Latex:
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}x: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{}
x)\mdownarrow{}
{}\mRightarrow{} (x \mmember{} rec-value()))
4. x : Base@i
5. (if x is inl then 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
eval y = evalall outr(x) in
inr y
else x\^{}j - 1
\mbot{}
outl(x) in
inl y
else if x is inr then 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
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(x) in
inr y
else x)\mdownarrow{}
6. (x)\mdownarrow{}
7. \mforall{}a,b:Base. (if x is a pair then a otherwise b \msim{} b)
8. \mforall{}a,b:Base. (if x is inl then a else b \msim{} b)
\mvdash{} x \mmember{} rec-value()
By
Latex:
(( RWO "-1" (-4)\mcdot{} THENA Complete (Auto)) THEN HasValueImplies2 5 [1])
Home
Index