---

Step * 1 of Lemma l-ind-sqequal-list_ind


1. j : ℤ
2. 0 < j
3. ∀F,x,L:Base.
     (λl-ind,L. eval v = L in if v = Ax then x otherwise let h,t = v in F[h;t;l-ind t]^j - 1 ⊥ L ≤ rec-case(L) of
                                                                                          [] => x
                                                                                          h::t =>
                                                                                           r.F[h;t;r])
4. F : Base
5. x : Base
6. L : Base
7. (L)↓
8. ∀a,b:Top.  (if L is a pair then a otherwise b ~ b)
9. ∀a,b:Top.  (if L = Ax then a otherwise b ~ b)
⊢ let h,t = L 
  in F[h;t;λl-ind,L. eval v = L in if v = Ax then x otherwise let h,t = v in F[h;t;l-ind t]^j - 1 ⊥ t] ≤ ⊥
BY
{ (SqReasoning
   THEN (Assert 0 ~ 1 BY
               (HypSubst' (-1) 8 THEN Reduce 8 THEN InstHyp [⌜0⌝;⌜1⌝] 8⋅ THEN Auto))
   THEN (Assert 0 = 1 ∈ ℤ BY
               HypSubst' (-1) 0)
   THEN Auto) }

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}F,x,L:Base.
          (\mlambda{}l-ind,L.  eval  v  =  L  in  if  v  =  Ax  then  x  otherwise  let  h,t  =  v  in  F[h;t;l-ind  t]\^{}j  -  1  \mbot{}  L 
            \mleq{}  rec-case(L)  of
                []  =>  x
                h::t  =>
                  r.F[h;t;r])
4.  F  :  Base
5.  x  :  Base
6.  L  :  Base
7.  (L)\mdownarrow{}
8.  \mforall{}a,b:Top.    (if  L  is  a  pair  then  a  otherwise  b  \msim{}  b)
9.  \mforall{}a,b:Top.    (if  L  =  Ax  then  a  otherwise  b  \msim{}  b)
\mvdash{}  let  h,t  =  L 
    in  F[h;t;\mlambda{}l-ind,L.  eval  v  =  L  in  if  v  =  Ax  then  x  otherwise  let  h,t  =  v  in  F[h;t;l-ind  t]\^{}j  -  1  \mbot{}  \000Ct]  \mleq{}  \mbot{}


By

---

Latex:
(SqReasoning
  THEN  (Assert  0  \msim{}  1  BY
                          (HypSubst'  (-1)  8  THEN  Reduce  8  THEN  InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]  8\mcdot{}  THEN  Auto))
  THEN  (Assert  0  =  1  BY
                          HypSubst'  (-1)  0)
  THEN  Auto)

---

Home Index