---

Step * of Lemma mrec-induction2-ext

∀L:MutualRectypeSpec. ∀[P:mobj(L) ⟶ TYPE]. (mrecind(L;x.P[x]) ⇒ (∀x:mobj(L). P[x]))
BY
{ Extract of Obid: mrec-induction2
  not unfolding  select select-tuple apply-alist atom-deq length
  finishing with (RepUR ``let`` 0 THEN Auto)
  normalizes to:
  
  λL,h,x. let i,x1 = x 
          in letrec r(i)=λx.(h i (fst(x)) (snd(x)) 
                             let L' = case apply-alist(AtomDeq;L;i)
                                       of inl(L2) =>
                                       case apply-alist(AtomDeq;L2;fst(x)) of inl(as) => as | inr(_) => Ax
                                       | inr(_) =>
                                       Ax in
                                 λj.case L'[j]
                                     of inl(x@0) =>
                                     case x@0 of inl(x1) => r x1 snd(x).j | inr(y) => λi@0.(r y snd(x).j[i@0])
                                     | inr(y) =>
                                     Ax) in
              r(i) 
             x1 }

---

Latex:

---

Latex:
\mforall{}L:MutualRectypeSpec.  \mforall{}[P:mobj(L)  {}\mrightarrow{}  TYPE].  (mrecind(L;x.P[x])  {}\mRightarrow{}  (\mforall{}x:mobj(L).  P[x]))


By

---

Latex:
Extract  of  Obid:  mrec-induction2
not  unfolding    select  select-tuple  apply-alist  atom-deq  length
finishing  with  (RepUR  ``let``  0  THEN  Auto)
normalizes  to:

\mlambda{}L,h,x.  let  i,x1  =  x 
                in  letrec  r(i)=\mlambda{}x.(h  i  (fst(x))  (snd(x)) 
                                                      let  L'  =  case  apply-alist(AtomDeq;L;i)
                                                                          of  inl(L2)  =>
                                                                          case  apply-alist(AtomDeq;L2;fst(x))
                                                                            of  inl(as)  =>
                                                                            as
                                                                            |  inr($_{}$)  =>
                                                                            Ax
                                                                          |  inr($_{}$)  =>
                                                                          Ax  in
                                                              \mlambda{}j.case  L'[j]
                                                                      of  inl(x@0)  =>
                                                                      case  x@0
                                                                        of  inl(x1)  =>
                                                                        r  x1  snd(x).j
                                                                        |  inr(y)  =>
                                                                        \mlambda{}i@0.(r  y  snd(x).j[i@0])
                                                                      |  inr(y)  =>
                                                                      Ax)  in
                        r(i) 
                      x1

---

Home Index