---

Step * 2 of Lemma rev-append-property-top-sqle


1. j : ℤ
2. 0 < j
3. ∀as,bs,cs:Base.
     (λlist_accum,y,L. eval v = L in
                       if v is a pair then let h,t = v 
                                           in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥^j - 1 
      ⊥ 
      (fix((λ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 cs otherwise ⊥)) 
       bs) 
      as ≤ fix((λ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 cs otherwise ⊥)) 
           (fix((λlist_accum,y,L. eval v = L in
                                  if v is a pair then let h,t = v 
                                                      in list_accum [h / y] t otherwise if v = Ax then y otherwise ⊥)) 
            bs 
            as))
4. as : Base@i
5. bs : Base@i
6. cs : Base@i
7. (if as = Ax then fix((λ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 cs otherwise ⊥)) 
                    bs otherwise ⊥)↓
8. (as)↓
9. ∀a,b:Top.  (if as is a pair then a otherwise b ~ b)
⊢ if as = Ax then fix((λ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 cs otherwise ⊥)\000C) 
                  bs otherwise ⊥ ≤ fix((λ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 cs otherwise ⊥)) 
                                   (fix((λlist_accum,y,L. eval v = L in
                                                          if v is a pair then let h,t = v 
                                                                              in list_accum [h / y] t
                                                          otherwise if v = Ax then y otherwise ⊥)) 
                                    bs 
                                    as)
BY
{ (HVimplies2 0 [1] THEN RW (AddrC [2;2] UnrollLoopsC) 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}as,bs,cs:Base.
          (\mlambda{}list$_{accum}$,y,L.  eval  v  =  L  in
                                            if  v  is  a  pair  then  let  h,t  =  v 
                                                                                    in  list$_{accum}$  [h  /  y]  t
                                            otherwise  if  v  =  Ax  then  y  otherwise  \mbot{}\^{}j  -  1 
            \mbot{} 
            (fix((\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  cs  otherwise  \mbot{})) 
              bs) 
            as  \mleq{}  fix((\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  cs  otherwise  \mbot{})) 
                      (fix((\mlambda{}list$_{accum}$,y,L.  eval  v  =  L  in
                                                                  if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                          in  list$_{accum}$  [h  /  y]  t
                                                                  otherwise  if  v  =  Ax  then  y  otherwise  \mbot{})) 
                        bs 
                        as))
4.  as  :  Base@i
5.  bs  :  Base@i
6.  cs  :  Base@i
7.  (if  as  =  Ax  then  fix((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                                          if  v  is  a  pair  then  let  a,as'  =  v 
                                                                                                                  in  [a  /  (list$_{ind}$  a\000Cs')]
                                                                          otherwise  if  v  =  Ax  then  cs  otherwise  \mbot{})) 
                                        bs  otherwise  \mbot{})\mdownarrow{}
8.  (as)\mdownarrow{}
9.  \mforall{}a,b:Top.    (if  as  is  a  pair  then  a  otherwise  b  \msim{}  b)
\mvdash{}  if  as  =  Ax  then  fix((\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  cs  otherwise  \mbot{})) 
                                    bs  otherwise  \mbot{}  \mleq{}  fix((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                                                                        if  v  is  a  pair  then  let  a,as'  =  v 
                                                                                                                                                in  [a  /  (list$_{\000Cind}$  as')]
                                                                                                        otherwise  if  v  =  Ax  then  cs  otherwise  \mbot{})) 
                                                                      (fix((\mlambda{}list$_{accum}$,y,L.  eval  v  =  L  in
                                                                                                                  if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                                                                          in  list$_{a\000Cccum}$  [h  /  y]  t
                                                                                                                  otherwise  if  v  =  Ax  then  y  otherwise  \mbot{})) 
                                                                        bs 
                                                                        as)


By

---

Latex:
(HVimplies2  0  [1]  THEN  RW  (AddrC  [2;2]  UnrollLoopsC)  0  THEN  Reduce  0  THEN  Auto)

---

Home Index