Step
*
1
1
1
1
1
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. (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
⊥
(fst(x)) 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
⊥
(snd(x)) in
<a', b'>)↓
6. (x)↓
7. x ~ <fst(x), snd(x)>
⊢ x ∈ rec-value()
BY
{ (HypSubst' (-1) 0 THEN SubsumeC ⌜atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + rec-value())⌝⋅) }
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. (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
⊥
(fst(x)) 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
⊥
(snd(x)) in
<a', b'>)↓
6. (x)↓
7. x ~ <fst(x), snd(x)>
⊢ <fst(x), snd(x)> ∈ atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + 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. (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
⊥
(fst(x)) 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
⊥
(snd(x)) in
<a', b'>)↓
6. (x)↓
7. x ~ <fst(x), snd(x)>
8. <fst(x), snd(x)> = <fst(x), snd(x)> ∈ (atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + rec-value()))
⊢ (atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + rec-value())) ⊆r 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. (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 then eval y = evalall outr(x) in
inr y
else x\^{}j - 1
\mbot{}
(fst(x)) 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 then eval y = evalall outr(x) in
inr y
else x\^{}j - 1
\mbot{}
(snd(x)) in
<a', b'>)\mdownarrow{}
6. (x)\mdownarrow{}
7. x \msim{} <fst(x), snd(x)>
\mvdash{} x \mmember{} rec-value()
By
Latex:
(HypSubst' (-1) 0
THEN SubsumeC \mkleeneopen{}atomic-values() \mcup{} (rec-value() \mtimes{} rec-value()) \mcup{} (rec-value() + rec-value())\mkleeneclose{}\mcdot{}
)
Home
Index