Step
*
1
1
1
1
1
2
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. (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)
BY
{ (((RWO "-1" 0 THENA Auto) THEN Thin (-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 ⊥ (inl outl(x)))↓
8. (eval y = F^j - 1 ⊥ outl(x) in
inl y)↓
9. 0 ≤ 0
10. x ~ inl outl(x)
⊢ (eval y = fix(F) outl(x) in inl y)↓ ∧ (eval y = fix(F) outl(x) in inl y ~ inl outl(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 inr then eval y = F^j - 1 ⊥ outr(x) in
inr y
else x)↓
9. (x)↓
10. ∀a,b:Top. (if x is inl then a else b ~ b)
⊢ (if x is inr then eval y = fix(F) outr(x) in
inr y
else x)↓
∧ (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. (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{}
9. (x)\mdownarrow{}
10. \mforall{}a,b:Top. (if x is a pair then a otherwise b \msim{} b)
\mvdash{} (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{} (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:
(((RWO "-1" 0 THENA Auto) THEN Thin (-1)) THEN HVimplies2 (-2) [1])
Home
Index