---

Step * 1 of Lemma rec-value-evalall


1. x : Base
2. (evalall(x))↓
⊢ x ∈ rec-value()
BY
{ (Unfold `evalall` (-1)
   THEN Compactness (-1)
   THEN Unhide
   THEN Thin (-3)
   THEN MoveToConcl 1
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN Auto
   THEN BotDiv) }

1
1. j : ℤ
2. 0 < j
3. ∀x:Base
     ((λ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^j - 1 
       ⊥ 
       x)↓
     ⇒ (x ∈ rec-value()))
4. x : Base@i
5. (λ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^j 
    ⊥ 
    x)↓
⊢ x ∈ rec-value()

---

Latex:

---

Latex:

1.  x  :  Base
2.  (evalall(x))\mdownarrow{}
\mvdash{}  x  \mmember{}  rec-value()


By

---

Latex:
(Unfold  `evalall`  (-1)
  THEN  Compactness  (-1)
  THEN  Unhide
  THEN  Thin  (-3)
  THEN  MoveToConcl  1
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  Auto
  THEN  BotDiv)

---

Home Index