---

Step * of Lemma evalall-append-implies-list-base

∀[a,b:Base].  a ∈ Base List supposing (evalall(a @ b))↓
BY
{ (Auto
   THEN Unfold `evalall` (-1)
   THEN Compactness (-1)
   THEN Unhide
   THEN Thin (-3)
   THEN MoveToConcl (-3)
   THEN MoveToConcl (-2)
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN Auto
   THEN BotDiv) }

1
1. j : ℤ
2. 0 < j
3. ∀a,b: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 
       ⊥ 
       (a @ b))↓
     ⇒ (a ∈ Base List))
4. a : Base@i
5. b : Base@i
6. (λ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 
    ⊥ 
    (a @ b))↓@i
⊢ a ∈ Base List

---

Latex:

---

Latex:
\mforall{}[a,b:Base].    a  \mmember{}  Base  List  supposing  (evalall(a  @  b))\mdownarrow{}


By

---

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

---

Home Index