### Nuprl Definition : mrecind

`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.`
`    ((∀j:ℕ||mrec-spec(L;lbl;k)||`
`        case mrec-spec(L;lbl;k)[j] of inl(y) => case y of inl(p) => P[<p, t.j>] | inr(p) => (∀u∈t.j.P[<p, u>]) | inr(_) \000C=> True)`
`    `` P[<k, mk-prec(lbl;t)>])`

Definitions occuring in Statement :  mkinds: `mKinds` mrec-spec: `mrec-spec(L;lbl;p)` mk-prec: `mk-prec(lbl;x)` prec-arg-types: `prec-arg-types(lbl,p.a[lbl; p];i;lbl)` select-tuple: `x.n` tuple-type: `tuple-type(L)` l_all: `(∀x∈L.P[x])` select: `L[n]` length: `||as||` int_seg: `{i..j-}` less_than: `a < b` all: `∀x:A. B[x]` implies: `P `` Q` true: `True` set: `{x:A| B[x]} ` pair: `<a, b>` decide: `case b of inl(x) => s[x] | inr(y) => t[y]` natural_number: `\$n` atom: `Atom`
Definitions occuring in definition :  mkinds: `mKinds` set: `{x:A| B[x]} ` atom: `Atom` less_than: `a < b` tuple-type: `tuple-type(L)` prec-arg-types: `prec-arg-types(lbl,p.a[lbl; p];i;lbl)` implies: `P `` Q` all: `∀x:A. B[x]` int_seg: `{i..j-}` natural_number: `\$n` select: `L[n]` decide: `case b of inl(x) => s[x] | inr(y) => t[y]` l_all: `(∀x∈L.P[x])` select-tuple: `x.n` length: `||as||` mrec-spec: `mrec-spec(L;lbl;p)` true: `True` pair: `<a, b>` mk-prec: `mk-prec(lbl;x)`
FDL editor aliases :  mrecind

Latex:
mrecind(L;x.P[x])  ==
\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{}j:\mBbbN{}||mrec-spec(L;lbl;k)||
case  mrec-spec(L;lbl;k)[j]
of  inl(y)  =>
case  y  of  inl(p)  =>  P[<p,  t.j>]  |  inr(p)  =>  (\mforall{}u\mmember{}t.j.P[<p,  u>])
|  inr(\$_{}\$)  =>
True)
{}\mRightarrow{}  P[<k,  mk-prec(lbl;t)>])

Date html generated: 2019_06_20-PM-02_15_54
Last ObjectModification: 2019_02_28-PM-04_51_59

Theory : tuples

Home Index