---

Step * 2 of Lemma length-is-colength


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
BY
{ (Reduce 0⋅
   THEN SqReasoning
   THEN TACTIC:(RW (AddrC [2] (UnrollRecursionC)) 0
                THEN Reduce 0
                THEN (CallByValueReduce 0 THENA Auto)
                THEN HVimplies2 0 [1]
                THEN (HasValueD (-3) ORELSE (ExceptionCases (-3) THEN Try (SameException)))
                THEN (GenConclTerm ⌜t⌝⋅ THENA Auto)
                THEN D -2
                THEN Reduce 0
                THEN SqLeTopToBase
                THEN (RW (AddrC [2] (RevLemmaC `add-commutes`)) 0 THENA Auto)
                THEN SqLeCD
                THEN Try (BackThruSomeHyp)
                THEN Auto)) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}t:Base
          (\mlambda{}colength,L.  if  L  =  Ax  then  0  otherwise  let  a,b  =  L  in  1  +  (colength  b)\^{}j  -  1  \mbot{}  t 
            \mleq{}  fix((\mlambda{}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  \mbot{})) 
                t)
4.  t  :  Base
\mvdash{}  (\mlambda{}x.((\mlambda{}colength,L.  if  L  =  Ax  then  0  otherwise  let  a,b  =  L  in  1  +  (colength  b)) 
              (\mlambda{}colength,L.  if  L  =  Ax  then  0  otherwise  let  a,b  =  L  in  1  +  (colength  b)\^{}j  -  1  x))) 
    \mbot{} 
    t  \mleq{}  fix((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                              if  v  is  a  pair  then  let  a,b  =  v 
                                                                                      in  (list$_{ind}$  b)  +  1  otherwise  if  \000Cv  =  Ax  then  0  otherwise  \mbot{})) 
            t


By

---

Latex:
(Reduce  0\mcdot{}
  THEN  SqReasoning
  THEN  TACTIC:(RW  (AddrC  [2]  (UnrollRecursionC))  0
                            THEN  Reduce  0
                            THEN  (CallByValueReduce  0  THENA  Auto)
                            THEN  HVimplies2  0  [1]
                            THEN  (HasValueD  (-3)  ORELSE  (ExceptionCases  (-3)  THEN  Try  (SameException)))
                            THEN  (GenConclTerm  \mkleeneopen{}t\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  SqLeTopToBase
                            THEN  (RW  (AddrC  [2]  (RevLemmaC  `add-commutes`))  0  THENA  Auto)
                            THEN  SqLeCD
                            THEN  Try  (BackThruSomeHyp)
                            THEN  Auto))

---

Home Index