---

Step * 1 1 1 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 ~ <fst(a), snd(a)>
8. (evalall(fst(a)))↓
9. 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 snd(a) otherwise ⊥^j - 1 
           ⊥ 
           b) ≤ eval u = evalall(b) in
                eval v = evalall(snd(a)) in
                  evalall(u @ v)
10. eval b' = 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 \000C- 1 
                      ⊥ 
                      (snd(a))) in
    <evalall(fst(a)), b'> ≤ eval b' = eval u = evalall(snd(a)) in
                                      eval v = evalall(b) in
                                        evalall(u @ v) in
                            <evalall(fst(a)), b'>
11. (evalall(snd(a)))↓
12. (evalall(b))↓
⊢ eval b' = evalall(evalall(snd(a)) @ evalall(b)) in
  <evalall(fst(a)), b'> ≤ evalall([evalall(fst(a)) / (evalall(snd(a)) @ evalall(b))])
BY
{ ((RW (AddrC [2] RecUnfoldTopAbC) 0 THEN Reduce 0)
   THEN (Subst' evalall(fst(a)) ~ fst(a) 0 THENA (BLemma `evalall-sqequal` THEN Auto))
   THEN (CallByValueReduceOn ⌜evalall(fst(a))⌝ 0⋅ THENA Auto)
   THEN (Subst' evalall(fst(a)) ~ fst(a) 0 THENA (BLemma `evalall-sqequal` THEN Auto))
   THEN Auto) }

---

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.  a  \msim{}  <fst(a),  snd(a)>
8.  (evalall(fst(a)))\mdownarrow{}
9.  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  snd(a)  otherwise  \mbot{}\^{}j  -  1 
                      \mbot{} 
                      b)  \mleq{}  eval  u  =  evalall(b)  in
                                eval  v  =  evalall(snd(a))  in
                                    evalall(u  @  v)
10.  eval  b'  =  evalall(\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                                    if  v  is  a  pair  then  let  a,as'  =  v 
                                                                                                            in  [a  /  (list$_{ind}$  as')\000C]
                                                                    otherwise  if  v  =  Ax  then  b  otherwise  \mbot{}\^{}j  -  1 
                                            \mbot{} 
                                            (snd(a)))  in
        <evalall(fst(a)),  b'>  \mleq{}  eval  b'  =  eval  u  =  evalall(snd(a))  in
                                                                            eval  v  =  evalall(b)  in
                                                                                evalall(u  @  v)  in
                                                        <evalall(fst(a)),  b'>
11.  (evalall(snd(a)))\mdownarrow{}
12.  (evalall(b))\mdownarrow{}
\mvdash{}  eval  b'  =  evalall(evalall(snd(a))  @  evalall(b))  in
    <evalall(fst(a)),  b'>  \mleq{}  evalall([evalall(fst(a))  /  (evalall(snd(a))  @  evalall(b))])


By

---

Latex:
((RW  (AddrC  [2]  RecUnfoldTopAbC)  0  THEN  Reduce  0)
  THEN  (Subst'  evalall(fst(a))  \msim{}  fst(a)  0  THENA  (BLemma  `evalall-sqequal`  THEN  Auto))
  THEN  (CallByValueReduceOn  \mkleeneopen{}evalall(fst(a))\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst'  evalall(fst(a))  \msim{}  fst(a)  0  THENA  (BLemma  `evalall-sqequal`  THEN  Auto))
  THEN  Auto)

---

Home Index