---

Step * 1 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 ⊥ <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)>)
BY
{ (HasValueD (-3)
   THEN HasValueD (-4)
   THEN RepeatFor 2 ((FHyp 5 [-2] THENA Auto))
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Auto) }

---

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{}  <fst(x),  snd(x)>)\mdownarrow{}
8.  (eval  a'  =  F\^{}j  -  1  \mbot{}  (fst(x))  in
        eval  b'  =  F\^{}j  -  1  \mbot{}  (snd(x))  in
            <a',  b'>)\mdownarrow{}
9.  0  \mleq{}  0
10.  x  \msim{}  <fst(x),  snd(x)>
\mvdash{}  (eval  a'  =  fix(F)  (fst(x))  in
      eval  b'  =  fix(F)  (snd(x))  in
          <a',  b'>)\mdownarrow{}
\mwedge{}  (eval  a'  =  fix(F)  (fst(x))  in
      eval  b'  =  fix(F)  (snd(x))  in
          <a',  b'>  \msim{}  <fst(x),  snd(x)>)


By

---

Latex:
(HasValueD  (-3)
  THEN  HasValueD  (-4)
  THEN  RepeatFor  2  ((FHyp  5  [-2]  THENA  Auto))
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Auto)

---

Home Index