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