---

Step * 1 of Lemma is-list-map


1. j : ℤ
2. 0 < j
3. ∀t,f:Base.
     (is-list(λlist_ind,L. eval v = L in
                           if v is a pair then let h,t = v 
                                               in [f h / (list_ind t)] otherwise if v = Ax then [] otherwise ⊥^j - 1 
              ⊥ 
              t) ≤ is-list(t))
4. t : Base
5. f : Base
⊢ is-list((λx.((λlist_ind,L. eval v = L in
                             if v is a pair then let h,t = v 
                                                 in [f h / (list_ind t)] otherwise if v = Ax then [] otherwise ⊥) 
               (λlist_ind,L. eval v = L in
                             if v is a pair then let h,t = v 
                                                 in [f h / (list_ind t)] otherwise if v = Ax then [] otherwise ⊥^j - 1 
                x))) 
          ⊥ 
          t) ≤ is-list(t)
BY
{ (RW (SubC (RecUnfoldC `is-list`)) 0
   THEN Reduce 0
   THEN RW (SubC (LiftC true)) 0
   THEN UseCbvSqle
   THEN HVimplies2 0 [2]
   THEN Try (((RWO  "-1" 0 THENA Auto) THEN HVimplies2 0 [2]))
   THEN (RepUR ``cons`` 0 THEN Fold `cons` 0)
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}t,f:Base.
          (is-list(\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                    if  v  is  a  pair  then  let  h,t  =  v 
                                                                                            in  [f  h  /  (list$_{ind}$  t)]
                                                    otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1 
                            \mbot{} 
                            t)  \mleq{}  is-list(t))
4.  t  :  Base
5.  f  :  Base
\mvdash{}  is-list((\mlambda{}x.((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                        if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                in  [f  h  /  (list$_{ind}$  t)]
                                                        otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}) 
                              (\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                                        if  v  is  a  pair  then  let  h,t  =  v 
                                                                                                in  [f  h  /  (list$_{ind}$  t)]
                                                        otherwise  if  v  =  Ax  then  []  otherwise  \mbot{}\^{}j  -  1 
                                x))) 
                    \mbot{} 
                    t)  \mleq{}  is-list(t)


By

---

Latex:
(RW  (SubC  (RecUnfoldC  `is-list`))  0
  THEN  Reduce  0
  THEN  RW  (SubC  (LiftC  true))  0
  THEN  UseCbvSqle
  THEN  HVimplies2  0  [2]
  THEN  Try  (((RWO    "-1"  0  THENA  Auto)  THEN  HVimplies2  0  [2]))
  THEN  (RepUR  ``cons``  0  THEN  Fold  `cons`  0)
  THEN  BackThruSomeHyp)

---

Home Index