---

Step * of Lemma evalall-sqequal

∀[x:Base]. evalall(x) ~ x supposing (evalall(x))↓
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN Unfold `evalall` (-1)
          THEN Compactness 2
          THEN Unfold `evalall` 0
          THEN MoveToConcl (-1)
          THEN (GenConcl ⌜(λ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)
                          = F
                          ∈ Base⌝⋅
                THENA Auto
                )
          THEN (D 0 THENA Auto)
          THEN UseWitness ⌜Ax⌝⋅
          THEN Unfold `member` 0
          THEN Refine_axiomSqEquality
          THEN (Assert ⌜∀j:ℕ. ∀x:Base.  ((F^j ⊥ x)↓ ⇒ ((fix(F) x)↓ ∧ (fix(F) x ~ x)))⌝⋅
          THENM (InstHyp [⌜j⌝;⌜x⌝] (-1)⋅ THEN Auto)
          )
          THEN ThinVar `x'
          THEN ThinVar `j') }

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
⊢ ∀j:ℕ. ∀x:Base.  ((F^j ⊥ x)↓ ⇒ ((fix(F) x)↓ ∧ (fix(F) x ~ x)))

---

Latex:

---

Latex:
\mforall{}[x:Base].  evalall(x)  \msim{}  x  supposing  (evalall(x))\mdownarrow{}


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  Unfold  `evalall`  (-1)
                THEN  Compactness  2
                THEN  Unfold  `evalall`  0
                THEN  MoveToConcl  (-1)
                THEN  (GenConcl  \mkleeneopen{}(\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\mkleeneclose{}\mcdot{}
                            THENA  Auto
                            )
                THEN  (D  0  THENA  Auto)
                THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
                THEN  Unfold  `member`  0
                THEN  Refine\_axiomSqEquality
                THEN  (Assert  \mkleeneopen{}\mforall{}j:\mBbbN{}.  \mforall{}x:Base.    ((F\^{}j  \mbot{}  x)\mdownarrow{}  {}\mRightarrow{}  ((fix(F)  x)\mdownarrow{}  \mwedge{}  (fix(F)  x  \msim{}  x)))\mkleeneclose{}\mcdot{}
                THENM  (InstHyp  [\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
                )
                THEN  ThinVar  `x'
                THEN  ThinVar  `j')

---

Home Index