---

Step * 1 1 1 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
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. (F (F^j - 1 ⊥) x)↓
9. 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
⊢ (fix(F) x)↓ ∧ (fix(F) x ~ x)
BY
{ (Thin 2
   THEN PromoteHyp (-1) 2
   THEN RW (AddrC [1;1;1] (HypC 2)) (-1)
   THEN Reduce (-1)
   THEN (Subst' fix(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
                                                                                       eval y = evalall outr(x) in
                                                                                       inr y 
                                                                                       else x) 
                         fix(F) 0
         THENA (RevHypSubst 2 0 THEN RW (AddrC [1] UnrollRecursionC) 0 THEN Auto)
         )
   THEN Reduce 0) }

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 ⊥ 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)

---

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
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.  (F  (F\^{}j  -  1  \mbot{})  x)\mdownarrow{}
9.  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
\mvdash{}  (fix(F)  x)\mdownarrow{}  \mwedge{}  (fix(F)  x  \msim{}  x)


By

---

Latex:
(Thin  2
  THEN  PromoteHyp  (-1)  2
  THEN  RW  (AddrC  [1;1;1]  (HypC  2))  (-1)
  THEN  Reduce  (-1)
  THEN  (Subst'  fix(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  then  eval  y  =  evalall  outr(x)  in
                                                                                                                                        inr  y 
                                                                                                      else  x) 
                                              fix(F)  0
              THENA  (RevHypSubst  2  0  THEN  RW  (AddrC  [1]  UnrollRecursionC)  0  THEN  Auto)
              )
  THEN  Reduce  0)

---

Home Index