---

Step * 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. (λ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()
BY
{ ((RWO "fun_exp_unroll_1" (-1) THENA Auto) THEN Reduce (-1) THEN HasValueD (-1)⋅ THEN CallByValueReduceOn ⌜x⌝ (-2)⋅) }

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. (if x is a pair then let a,b = x 
                        in eval a' = λ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 
                                     ⊥ 
                                     a in
                           eval b' = λ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 
                                     ⊥ 
                                     b in
                             <a', b'>
    otherwise 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)↓
⊢ x ∈ rec-value()

---

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.  (\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\^{}j 
        \mbot{} 
        x)\mdownarrow{}
\mvdash{}  x  \mmember{}  rec-value()


By

---

Latex:
((RWO  "fun\_exp\_unroll\_1"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  HasValueD  (-1)\mcdot{}
  THEN  CallByValueReduceOn  \mkleeneopen{}x\mkleeneclose{}  (-2)\mcdot{})

---

Home Index