---

Step * of Lemma is-list-map

∀[t,f:Top].  (is-list(map(f;t)) ~ is-list(t))
BY
{ xxxMutualFixpointInduction1 `t'xxx }

1
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)

2
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))

---

Latex:

---

Latex:
\mforall{}[t,f:Top].    (is-list(map(f;t))  \msim{}  is-list(t))


By

---

Latex:
xxxMutualFixpointInduction1  `t'xxx

---

Home Index