---

Step * 1 1 1 2 1 1 of Lemma rec-value-evalall


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. (if x is inl then eval y = λ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 
                              ⊥ 
                              outl(x) in
                     inl y
    else if x is inr then eval y = λ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 
                                   ⊥ 
                                   outr(x) in
                          inr y 
         else x)↓
6. (x)↓
7. ∀a,b:Base.  (if x is a pair then a otherwise b ~ b)
8. x ~ inl outl(x)
⊢ x ∈ rec-value()
BY
{ (HypSubstAll (-1)
   THEN HasValueD (-4)
   THEN (SubsumeC ⌜atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + rec-value())⌝⋅
         THEN Try (Complete (Auto))
         )
   THEN InstLemma `rec-value-ext` []
   THEN D -1
   THEN Hypothesis) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}x:Base
          ((\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\^{}j  -  1 
              \mbot{} 
              x)\mdownarrow{}
          {}\mRightarrow{}  (x  \mmember{}  rec-value()))
4.  x  :  Base@i
5.  (if  x  is  inl  then  eval  y  =  \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\^{}j  -  1 
                                                            \mbot{} 
                                                            outl(x)  in
                                          inl  y
        else  if  x  is  inr  then  eval  y  =  \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
                                                                                                                  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 
                                                                      \mbot{} 
                                                                      outr(x)  in
                                                    inr  y 
                  else  x)\mdownarrow{}
6.  (x)\mdownarrow{}
7.  \mforall{}a,b:Base.    (if  x  is  a  pair  then  a  otherwise  b  \msim{}  b)
8.  x  \msim{}  inl  outl(x)
\mvdash{}  x  \mmember{}  rec-value()


By

---

Latex:
(HypSubstAll  (-1)
  THEN  HasValueD  (-4)
  THEN  (SubsumeC  \mkleeneopen{}atomic-values()  \mcup{}  (rec-value()  \mtimes{}  rec-value())  \mcup{}  (rec-value()  +  rec-value())\mkleeneclose{}\mcdot{}
              THEN  Try  (Complete  (Auto))
              )
  THEN  InstLemma  `rec-value-ext`  []
  THEN  D  -1
  THEN  Hypothesis)

---

Home Index