---

Step * 1 of Lemma length-is-colength


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
BY
{ TACTIC:(Reduce 0⋅
          THEN SqReasoning
          THEN TACTIC:(RW (AddrC [2] (UnrollRecursionC)) 0
                       THEN Reduce 0
                       THEN HVimplies2 0 [1]
                       THEN (RW (AddrC [2] (LemmaC `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{}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  =  A\000Cx  then  0  otherwise  \mbot{}\^{}j  -  1 
            \mbot{} 
            t  \mleq{}  fix((\mlambda{}colength,L.  if  L  =  Ax  then  0  otherwise  let  a,b  =  L  in  1  +  (colength  b)))  t)
4.  t  :  Base
\mvdash{}  (\mlambda{}x.((\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  =\000C  Ax  then  0  otherwise  \mbot{}) 
              (\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  =\000C  Ax  then  0  otherwise  \mbot{}\^{}j  -  1 
                x))) 
    \mbot{} 
    t  \mleq{}  fix((\mlambda{}colength,L.  if  L  =  Ax  then  0  otherwise  let  a,b  =  L  in  1  +  (colength  b)))  t


By

---

Latex:
TACTIC:(Reduce  0\mcdot{}
                THEN  SqReasoning
                THEN  TACTIC:(RW  (AddrC  [2]  (UnrollRecursionC))  0
                                          THEN  Reduce  0
                                          THEN  HVimplies2  0  [1]
                                          THEN  (RW  (AddrC  [2]  (LemmaC  `add-commutes`))  0  THENA  Auto)
                                          THEN  SqLeCD
                                          THEN  Try  (BackThruSomeHyp)
                                          THEN  Auto))

---

Home Index