---

Step * 1 of Lemma list-if-has-value-rev-append


1. j : ℤ
2. 0 < j
3. ∀as,bs:Base.
     ((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)↓
     ⇒ (λ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 
         ⊥ 
         bs 
         as)↓
     ⇒ (as ∈ Base List))
4. as : Base@i
5. bs : Base@i
6. (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 
    <fst(as), snd(as)>)↓@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) / bs] 
    (snd(as)))↓@i
8. 0 ≤ 0
9. as ~ <fst(as), snd(as)>
⊢ <fst(as), snd(as)> ∈ Base List
BY
{ ((Fold `cons` 0 THEN Auto)
   THEN InstHyp [⌜snd(as)⌝;⌜[fst(as) / bs]⌝] 3⋅
   THEN Auto
   THEN RW UnrollLoopsC (-4)
   THEN Reduce (-4)
   THEN Auto) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}as,bs:Base.
          ((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)\mdownarrow{}
          {}\mRightarrow{}  (\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{} 
                  bs 
                  as)\mdownarrow{}
          {}\mRightarrow{}  (as  \mmember{}  Base  List))
4.  as  :  Base@i
5.  bs  :  Base@i
6.  (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 
        <fst(as),  snd(as)>)\mdownarrow{}@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)  /  bs] 
        (snd(as)))\mdownarrow{}@i
8.  0  \mleq{}  0
9.  as  \msim{}  <fst(as),  snd(as)>
\mvdash{}  <fst(as),  snd(as)>  \mmember{}  Base  List


By

---

Latex:
((Fold  `cons`  0  THEN  Auto)
  THEN  InstHyp  [\mkleeneopen{}snd(as)\mkleeneclose{};\mkleeneopen{}[fst(as)  /  bs]\mkleeneclose{}]  3\mcdot{}
  THEN  Auto
  THEN  RW  UnrollLoopsC  (-4)
  THEN  Reduce  (-4)
  THEN  Auto)

---

Home Index