Step * of Lemma length-is-colength

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

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

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