Step
*
1
1
1
1
1
of Lemma
evalall-sqequal
1. F : Base
2. F ~ λ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
3. j : ℤ
4. 0 < j
5. ∀x:Base. ((F^j - 1 ⊥ x)↓ ⇒ ((fix(F) x)↓ ∧ (fix(F) x ~ x)))
6. x : Base
7. (F^j ⊥ x)↓
8. (eval x = x in
if x is a pair then let a,b = x
in eval a' = F^j - 1 ⊥ a in
eval b' = F^j - 1 ⊥ b in
<a', b'> otherwise if x is inl then eval y = F^j - 1 ⊥ outl(x) in
inl y
else if x is inr then eval y = F^j - 1 ⊥ outr(x) in
inr y
else x)↓
⊢ (eval x = x in
if x is a pair then let a,b = x
in eval a' = fix(F) a in
eval b' = fix(F) b in
<a', b'> otherwise if x is inl then eval y = fix(F) outl(x) in
inl y
else if x is inr then eval y = fix(F) outr(x) in
inr y
else x)↓
∧ (eval x = x in
if x is a pair then let a,b = x
in eval a' = fix(F) a in
eval b' = fix(F) b in
<a', b'> otherwise if x is inl then eval y = fix(F) outl(x) in
inl y
else if x is inr then eval y = fix(F) outr(x) in
inr y
else x ~ x)
BY
{ (HasValueD (-1) THEN HVimplies2 (-2) [1]) }
1
1. F : Base
2. F ~ λ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
3. j : ℤ
4. 0 < j
5. ∀x:Base. ((F^j - 1 ⊥ x)↓ ⇒ ((fix(F) x)↓ ∧ (fix(F) x ~ x)))
6. x : Base
7. (F^j ⊥ <fst(x), snd(x)>)↓
8. (eval a' = F^j - 1 ⊥ (fst(x)) in
eval b' = F^j - 1 ⊥ (snd(x)) in
<a', b'>)↓
9. 0 ≤ 0
10. x ~ <fst(x), snd(x)>
⊢ (eval a' = fix(F) (fst(x)) in
eval b' = fix(F) (snd(x)) in
<a', b'>)↓
∧ (eval a' = fix(F) (fst(x)) in
eval b' = fix(F) (snd(x)) in
<a', b'> ~ <fst(x), snd(x)>)
2
1. F : Base
2. F ~ λ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
3. j : ℤ
4. 0 < j
5. ∀x:Base. ((F^j - 1 ⊥ x)↓ ⇒ ((fix(F) x)↓ ∧ (fix(F) x ~ x)))
6. x : Base
7. (F^j ⊥ x)↓
8. (if x is inl then eval y = F^j - 1 ⊥ outl(x) in
inl y
else if x is inr then eval y = F^j - 1 ⊥ outr(x) in
inr y
else x)↓
9. (x)↓
10. ∀a,b:Top. (if x is a pair then a otherwise b ~ b)
⊢ (if x is inl then eval y = fix(F) outl(x) in
inl y
else if x is inr then eval y = fix(F) outr(x) in
inr y
else x)↓
∧ (if x is a pair then let a,b = x
in eval a' = fix(F) a in
eval b' = fix(F) b in
<a', b'> otherwise if x is inl then eval y = fix(F) outl(x) in
inl y
else if x is inr then eval y = fix(F) outr(x) in
inr y
else x ~ x)
Latex:
Latex:
1. F : Base
2. F \msim{} \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
3. j : \mBbbZ{}
4. 0 < j
5. \mforall{}x:Base. ((F\^{}j - 1 \mbot{} x)\mdownarrow{} {}\mRightarrow{} ((fix(F) x)\mdownarrow{} \mwedge{} (fix(F) x \msim{} x)))
6. x : Base
7. (F\^{}j \mbot{} x)\mdownarrow{}
8. (eval x = x in
if x is a pair then let a,b = x
in eval a' = F\^{}j - 1 \mbot{} a in
eval b' = F\^{}j - 1 \mbot{} b in
<a', b'> otherwise if x is inl then eval y = F\^{}j - 1 \mbot{} outl(x) in
inl y
else if x is inr then eval y = F\^{}j - 1 \mbot{} outr(x) in
inr y
else x)\mdownarrow{}
\mvdash{} (eval x = x in
if x is a pair then let a,b = x
in eval a' = fix(F) a in
eval b' = fix(F) b in
<a', b'> otherwise if x is inl then eval y = fix(F) outl(x) in
inl y
else if x is inr then eval y = fix(F) outr(x) in
inr y
else x)\mdownarrow{}
\mwedge{} (eval x = x in
if x is a pair then let a,b = x
in eval a' = fix(F) a in
eval b' = fix(F) b in
<a', b'> otherwise if x is inl then eval y = fix(F) outl(x) in
inl y
else if x is inr then eval y = fix(F) outr(x) in
inr y
else x \msim{} x)
By
Latex:
(HasValueD (-1) THEN HVimplies2 (-2) [1])
Home
Index