---

Step * of Lemma l-ind-sqequal-list_ind

∀[L,x,F:Top].  (l-ind(L;x;h,t,r.F[h;t;r]) ~ rec-case(L) of [] => x | h::t => r.F[h;t;r])
BY
{ (MutualFixpointInduction1 `L'
   THEN Reduce 0
   THEN RW (AddrC [2] RecUnfoldTopAbC) 0
   THEN UseCbvSqle
   THEN Try (Complete (RepeatFor 2 (HVimplies2 0 [1])))
   THEN RepeatFor 2 (HVimplies2 0 [2])
   THEN (RWO  "-2 -1" 0 THENA Auto)) }

1
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] ≤ ⊥

---

Latex:

---

Latex:
\mforall{}[L,x,F:Top].    (l-ind(L;x;h,t,r.F[h;t;r])  \msim{}  rec-case(L)  of  []  =>  x  |  h::t  =>  r.F[h;t;r])


By

---

Latex:
(MutualFixpointInduction1  `L'
  THEN  Reduce  0
  THEN  RW  (AddrC  [2]  RecUnfoldTopAbC)  0
  THEN  UseCbvSqle
  THEN  Try  (Complete  (RepeatFor  2  (HVimplies2  0  [1])))
  THEN  RepeatFor  2  (HVimplies2  0  [2])
  THEN  (RWO    "-2  -1"  0  THENA  Auto))

---

Home Index