---

Step * 1 1 2 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)>])
⊢ ∀x:mobj(L). ((∀z:{z:mobj(L)| z < x} . P[z]) ⇒ P[x])
BY
{ ((D 0 THENA Auto)
   THEN (InstLemma  `mobj-sq` [⌜L⌝;⌜x⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN skip{(BHyp 4 THEN Auto)}) }

1
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))>]

---

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)>])
\mvdash{}  \mforall{}x:mobj(L).  ((\mforall{}z:\{z:mobj(L)|  z  <  x\}  .  P[z])  {}\mRightarrow{}  P[x])


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma    `mobj-sq`  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  skip\{(BHyp  4  THEN  Auto)\})

---

Home Index