---

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


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. (if a @ b is a pair then let a,b = a @ b 
                            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 a @ b 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(a @ b) in
                                   inl y
              else if a @ b 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(a @ b) in
                                        inr y 
                   else a @ b)↓@i
7. (a @ b)↓
⊢ a ∈ Base List
BY
{ (Unfold `append` (-1) THEN RecUnfold `list_ind` (-1)⋅ THEN HasValueD (-1) THEN HVimplies2 (-2) [1]) }

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. (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 
              ⊥ 
              (fst(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 
              ⊥ 
              ((snd(a)) @ b) in
      <a', b'>)↓@i
7. 0 ≤ 0
8. 0 ≤ 0
9. a ~ <fst(a), snd(a)>
⊢ <fst(a), snd(a)> ∈ Base List

2
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. (if a @ b is a pair then let a,b = a @ b 
                            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 a @ b 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(a @ b) in
                                   inl y
              else if a @ b 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(a @ b) in
                                        inr y 
                   else a @ b)↓@i
7. (if a = Ax then b otherwise ⊥)↓
8. (a)↓
9. ∀a@0,b:Top.  (if a is a pair then a@0 otherwise b ~ b)
⊢ a ∈ Base List

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `append`  (-1)  THEN  RecUnfold  `list\_ind`  (-1)\mcdot{}  THEN  HasValueD  (-1)  THEN  HVimplies2  (-2)  [1])

---

Home Index