---

Step * 2 of Lemma is-list-map


1. j : ℤ
2. 0 < j
3. ∀t,f:Base.
     (λis-list,t. eval u = t in if u is a pair then is-list (snd(u)) otherwise if u = Ax then tt otherwise ⊥^j - 1 ⊥ t 
      ≤ is-list(map(f;t)))
4. t : Base
5. f : Base
⊢ (λx.((λis-list,t. eval u = t in if u is a pair then is-list (snd(u)) otherwise if u = Ax then tt otherwise ⊥) 
       (λis-list,t. eval u = t in if u is a pair then is-list (snd(u)) otherwise if u = Ax then tt otherwise ⊥^j - 1 x))\000C) 
  ⊥ 
  t ≤ is-list(map(f;t))
BY
{ (RW (SubC (TryC (RecUnfoldC `is-list`))) 0
   THEN (Unfold `map` 0 THEN RecUnfold `list_ind` 0)
   THEN Reduce 0
   THEN RW (SubC (LiftC true)) 0
   THEN UseCbvSqle
   THEN HVimplies2 0 [1]
   THEN Try (((RWO  "-1" 0 THENA Auto) THEN HVimplies2 0 [1]))
   THEN Fold `map` 0
   THEN RepUR ``cons`` 0
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}t,f:Base.
          (\mlambda{}is-list,t.  eval  u  =  t  in
                                    if  u  is  a  pair  then  is-list  (snd(u))  otherwise  if  u  =  Ax  then  tt  otherwise  \mbot{}\^{}j  -  1\000C 
            \mbot{} 
            t  \mleq{}  is-list(map(f;t)))
4.  t  :  Base
5.  f  :  Base
\mvdash{}  (\mlambda{}x.((\mlambda{}is-list,t.  eval  u  =  t  in
                                        if  u  is  a  pair  then  is-list  (snd(u))  otherwise  if  u  =  Ax  then  tt  otherwise  \mbot{}) 
              (\mlambda{}is-list,t.  eval  u  =  t  in
                                        if  u  is  a  pair  then  is-list  (snd(u))  otherwise  if  u  =  Ax  then  tt  otherwise  \mbot{}\^{}j  -\000C  1 
                x))) 
    \mbot{} 
    t  \mleq{}  is-list(map(f;t))


By

---

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

---

Home Index