---

Step * 1 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. (λ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 
    ⊥ 
    [fst(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 ⊥)) 
      bs)] 
    (snd(as)))↓
8. 0 ≤ 0
9. as ~ <fst(as), snd(as)>
⊢ λ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 
  ⊥ 
  [fst(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 ⊥)) 
    bs)] 
  (snd(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 ⊥)\000C) 
               bs 
               <fst(as), snd(as)>)
BY
{ ((InstHyp [⌜snd(as)⌝;⌜[fst(as) / bs]⌝;⌜cs⌝] 3⋅ THENA Auto)
   THEN RW (AddrC [1;1;2] UnrollLoopsC) (-1)
   THEN Reduce (-1)
   THEN RW (AddrC [2;2] UnrollLoopsC) 0
   THEN Reduce 0
   THEN Trivial) }

---

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.  (\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{} 
        [fst(as)  / 
          (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)] 
        (snd(as)))\mdownarrow{}
8.  0  \mleq{}  0
9.  as  \msim{}  <fst(as),  snd(as)>
\mvdash{}  \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\000C  =  Ax  then  y  otherwise  \mbot{}\^{}j  -  1 
    \mbot{} 
    [fst(as)  / 
      (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)] 
    (snd(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\000C]  t
                                                                        otherwise  if  v  =  Ax  then  y  otherwise  \mbot{})) 
                              bs 
                              <fst(as),  snd(as)>)


By

---

Latex:
((InstHyp  [\mkleeneopen{}snd(as)\mkleeneclose{};\mkleeneopen{}[fst(as)  /  bs]\mkleeneclose{};\mkleeneopen{}cs\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  RW  (AddrC  [1;1;2]  UnrollLoopsC)  (-1)
  THEN  Reduce  (-1)
  THEN  RW  (AddrC  [2;2]  UnrollLoopsC)  0
  THEN  Reduce  0
  THEN  Trivial)

---

Home Index