---

Step * of Lemma length-is-colength

∀[t:Top]. (||t|| ~ colength(t))
BY
{ TACTIC:(RepUR ``length colength list_ind`` 0 THEN MutualFixpointInduction1 `t') }

1
1. j : ℤ
2. 0 < j
3. ∀t:Base
     (λlist_ind,L. eval v = L in
                   if v is a pair then let a,b = v 
                                       in (list_ind b) + 1 otherwise if v = Ax then 0 otherwise ⊥^j - 1 
      ⊥ 
      t ≤ fix((λcolength,L. if L = Ax then 0 otherwise let a,b = L in 1 + (colength b))) t)
4. t : Base
⊢ (λx.((λlist_ind,L. eval v = L in
                     if v is a pair then let a,b = v 
                                         in (list_ind b) + 1 otherwise if v = Ax then 0 otherwise ⊥) 
       (λlist_ind,L. eval v = L in
                     if v is a pair then let a,b = v 
                                         in (list_ind b) + 1 otherwise if v = Ax then 0 otherwise ⊥^j - 1 
        x))) 
  ⊥ 
  t ≤ fix((λcolength,L. if L = Ax then 0 otherwise let a,b = L in 1 + (colength b))) t

2
1. j : ℤ
2. 0 < j
3. ∀t:Base
     (λcolength,L. if L = Ax then 0 otherwise let a,b = L in 1 + (colength b)^j - 1 ⊥ t ≤ fix((λlist_ind,L. eval v = L i\000Cn
                                                                                                 if v is a pair
                                                                                                 then let a,b = v 
                                                                                                      in (list_ind b)
                                                                                                         + 1
                                                                                                 otherwise if v = Ax
                                                                                                           then 0
                                                                                                           otherwise ⊥))\000C 
                                                                               t)
4. t : Base
⊢ (λx.((λcolength,L. if L = Ax then 0 otherwise let a,b = L in 1 + (colength b)) 
       (λcolength,L. if L = Ax then 0 otherwise let a,b = L in 1 + (colength b)^j - 1 x))) 
  ⊥ 
  t ≤ fix((λlist_ind,L. eval v = L in
                        if v is a pair then let a,b = v 
                                            in (list_ind b) + 1 otherwise if v = Ax then 0 otherwise ⊥)) 
      t

---

Latex:

---

Latex:
\mforall{}[t:Top].  (||t||  \msim{}  colength(t))


By

---

Latex:
TACTIC:(RepUR  ``length  colength  list\_ind``  0  THEN  MutualFixpointInduction1  `t')

---

Home Index