---

Step * 1 of Lemma evalall-sqequal


1. F : Base
2. (λ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)
= F
∈ Base
⊢ ∀j:ℕ. ∀x:Base.  ((F^j ⊥ x)↓ ⇒ ((fix(F) x)↓ ∧ (fix(F) x ~ x)))
BY
{ (InductionOnNat THEN Reduce 0 THEN Strictness THEN (UnivCD THENA Auto) THEN BotDiv) }

1
1. F : Base
2. (λ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)
= F
∈ Base
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)↓
⊢ (fix(F) x)↓ ∧ (fix(F) x ~ x)

---

Latex:

---

Latex:

1.  F  :  Base
2.  (\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)
=  F
\mvdash{}  \mforall{}j:\mBbbN{}.  \mforall{}x:Base.    ((F\^{}j  \mbot{}  x)\mdownarrow{}  {}\mRightarrow{}  ((fix(F)  x)\mdownarrow{}  \mwedge{}  (fix(F)  x  \msim{}  x)))


By

---

Latex:
(InductionOnNat  THEN  Reduce  0  THEN  Strictness  THEN  (UnivCD  THENA  Auto)  THEN  BotDiv)

---

Home Index