---

Step * 1 1 of Lemma mrec-induction2

.....antecedent..... 
1. L : MutualRectypeSpec
2. [P] : mobj(L) ⟶ TYPE
3. mrecind(L;x.P[x])
⊢ ∀x:mobj(L). ((∀z:{z:mobj(L)| z < x} . P[z]) ⇒ P[x])
BY
{ Assert ⌜∀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)>])⌝⋅ }

1
.....assertion..... 
1. L : MutualRectypeSpec
2. [P] : mobj(L) ⟶ TYPE
3. mrecind(L;x.P[x])
⊢ ∀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))\000C.
    ((∀z:{z:mobj(L)| z < <k, mk-prec(lbl;t)>} . P[z]) ⇒ P[<k, mk-prec(lbl;t)>])

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

---

Latex:

---

Latex:
.....antecedent..... 
1.  L  :  MutualRectypeSpec
2.  [P]  :  mobj(L)  {}\mrightarrow{}  TYPE
3.  mrecind(L;x.P[x])
\mvdash{}  \mforall{}x:mobj(L).  ((\mforall{}z:\{z:mobj(L)|  z  <  x\}  .  P[z])  {}\mRightarrow{}  P[x])


By

---

Latex:
Assert  \mkleeneopen{}\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)>])\mkleeneclose{}\mcdot{}

---

Home Index