---

Step * 1 1 2 1 of Lemma mrec-induction2


1. L : MutualRectypeSpec
2. [P] : mobj(L) ⟶ TYPE
3. mrecind(L;x.P[x])
4. ∀k:mKinds. ∀lbl:{lbl:Atom| 0 < ||mrec-spec(L;lbl;k)||} .
   ∀t:tuple-type(prec-arg-types(lbl,p.mrec-spec(L;lbl;p);k;lbl)).
     ((∀z:{z:mobj(L)| z < <k, mk-prec(lbl;t)>} . P[z]) ⇒ P[<k, mk-prec(lbl;t)>])
5. x : mobj(L)
6. x ~ <mobj-kind(x), mk-prec(mobj-label(x);mobj-tuple(x))>
⊢ (∀z:{z:mobj(L)| z < <mobj-kind(x), mk-prec(mobj-label(x);mobj-tuple(x))>} . P[z])
⇒ P[<mobj-kind(x), mk-prec(mobj-label(x);mobj-tuple(x))>]
BY
{ ((D 4 With ⌜mobj-kind(x)⌝  THENA Auto)
   THEN (D -1 With ⌜mobj-label(x)⌝  THENA Auto)
   THEN D -1 With ⌜mobj-tuple(x)⌝ 
   THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  MutualRectypeSpec
2.  [P]  :  mobj(L)  {}\mrightarrow{}  TYPE
3.  mrecind(L;x.P[x])
4.  \mforall{}k:mKinds.  \mforall{}lbl:\{lbl:Atom|  0  <  ||mrec-spec(L;lbl;k)||\}  .
      \mforall{}t:tuple-type(prec-arg-types(lbl,p.mrec-spec(L;lbl;p);k;lbl)).
          ((\mforall{}z:\{z:mobj(L)|  z  <  <k,  mk-prec(lbl;t)>\}  .  P[z])  {}\mRightarrow{}  P[<k,  mk-prec(lbl;t)>])
5.  x  :  mobj(L)
6.  x  \msim{}  <mobj-kind(x),  mk-prec(mobj-label(x);mobj-tuple(x))>
\mvdash{}  (\mforall{}z:\{z:mobj(L)|  z  <  <mobj-kind(x),  mk-prec(mobj-label(x);mobj-tuple(x))>\}  .  P[z])
{}\mRightarrow{}  P[<mobj-kind(x),  mk-prec(mobj-label(x);mobj-tuple(x))>]


By

---

Latex:
((D  4  With  \mkleeneopen{}mobj-kind(x)\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}mobj-label(x)\mkleeneclose{}    THENA  Auto)
  THEN  D  -1  With  \mkleeneopen{}mobj-tuple(x)\mkleeneclose{} 
  THEN  Auto)

---

Home Index