---

Step * 2 1 of Lemma evalall-append-sqle


1. j : ℤ
2. 0 < j
3. ∀a,b:Base.
     (evalall(λlist_ind,L. eval v = L in
                           if v is a pair then let a,as' = v 
                                               in [a / (list_ind as')] otherwise if v = Ax then b otherwise ⊥^j - 1 
              ⊥ 
              a) ≤ eval u = evalall(a) in
                   eval v = evalall(b) in
                     evalall(u @ v))
4. a : Base
5. b : Base
6. 0 ≤ 0
7. ∀a@0,b:Top.  (b ~ b)
8. a ~ Ax
⊢ eval v = b in
  if v is a pair then let a,b = v 
                      in eval a' = evalall(a) in
                         eval b' = evalall(b) in
                           <a', b'> otherwise if v is inl then eval y = evalall(outl(v)) in
                                                               inl y
                                              else if v is inr then eval y = evalall(outr(v)) in
                                                                    inr y 
                                                   else v ≤ eval v = evalall(b) in
                                                            evalall(v)
BY
{ TACTIC:Subst' eval v = b in
                if v is a pair then let a,b = v 
                                    in eval a' = evalall(a) in
                                       eval b' = evalall(b) in
                                         <a', b'> otherwise if v is inl then eval y = evalall(outl(v)) in
                                                                             inl y
                                                            else if v is inr then eval y = evalall(outr(v)) in
                                                                                  inr y 
                                                                 else v ~ evalall(b) 0 }

1
.....equality..... 
1. j : ℤ
2. 0 < j
3. ∀a,b:Base.
     (evalall(λlist_ind,L. eval v = L in
                           if v is a pair then let a,as' = v 
                                               in [a / (list_ind as')] otherwise if v = Ax then b otherwise ⊥^j - 1 
              ⊥ 
              a) ≤ eval u = evalall(a) in
                   eval v = evalall(b) in
                     evalall(u @ v))
4. a : Base
5. b : Base
6. 0 ≤ 0
7. ∀a@0,b:Top.  (b ~ b)
8. a ~ Ax
⊢ eval v = b in
  if v is a pair then let a,b = v 
                      in eval a' = evalall(a) in
                         eval b' = evalall(b) in
                           <a', b'> otherwise if v is inl then eval y = evalall(outl(v)) in
                                                               inl y
                                              else if v is inr then eval y = evalall(outr(v)) in
                                                                    inr y 
                                                   else v ~ evalall(b)

2
1. j : ℤ
2. 0 < j
3. ∀a,b:Base.
     (evalall(λlist_ind,L. eval v = L in
                           if v is a pair then let a,as' = v 
                                               in [a / (list_ind as')] otherwise if v = Ax then b otherwise ⊥^j - 1 
              ⊥ 
              a) ≤ eval u = evalall(a) in
                   eval v = evalall(b) in
                     evalall(u @ v))
4. a : Base
5. b : Base
6. 0 ≤ 0
7. ∀a@0,b:Top.  (b ~ b)
8. a ~ Ax
⊢ evalall(b) ≤ eval v = evalall(b) in
               evalall(v)

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}a,b:Base.
          (evalall(\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                    if  v  is  a  pair  then  let  a,as'  =  v 
                                                                                            in  [a  /  (list$_{ind}$  as')]
                                                    otherwise  if  v  =  Ax  then  b  otherwise  \mbot{}\^{}j  -  1 
                            \mbot{} 
                            a)  \mleq{}  eval  u  =  evalall(a)  in
                                      eval  v  =  evalall(b)  in
                                          evalall(u  @  v))
4.  a  :  Base
5.  b  :  Base
6.  0  \mleq{}  0
7.  \mforall{}a@0,b:Top.    (b  \msim{}  b)
8.  a  \msim{}  Ax
\mvdash{}  eval  v  =  b  in
    if  v  is  a  pair  then  let  a,b  =  v 
                                            in  eval  a'  =  evalall(a)  in
                                                  eval  b'  =  evalall(b)  in
                                                      <a',  b'>  otherwise  if  v  is  inl  then  eval  y  =  evalall(outl(v))  in
                                                                                                                              inl  y
                                                                                            else  if  v  is  inr  then  eval  y  =  evalall(outr(v))  in
                                                                                                                                        inr  y 
                                                                                                      else  v  \mleq{}  eval  v  =  evalall(b)  in
                                                                                                                        evalall(v)


By

---

Latex:
TACTIC:Subst'  eval  v  =  b  in
                            if  v  is  a  pair  then  let  a,b  =  v 
                                                                    in  eval  a'  =  evalall(a)  in
                                                                          eval  b'  =  evalall(b)  in
                                                                              <a',  b'>
                            otherwise  if  v  is  inl  then  eval  y  =  evalall(outl(v))  in
                                                                                  inl  y
                                                else  if  v  is  inr  then  eval  y  =  evalall(outr(v))  in
                                                                                            inr  y 
                                                          else  v  \msim{}  evalall(b)  0

---

Home Index