Nuprl Definition : param-W
For each parameter ⌜par ∈ P⌝, the corresponding type
in the parameterized family of W-types is the subtype of the
corresponding parameterized co-inductive family of co-W types
containing those trees, w, such that every path starting at w
is barred. ⋅
pW == λpar.{w:pco-W par| ∀path:Path. (StepAgree(path 0;par;w) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))}
Definitions occuring in Statement :
pcw-pp-barred: Barred(pp),
pcw-partial: pcw-partial(path;n),
pcw-path: Path,
pcw-step-agree: StepAgree(s;p1;w),
param-co-W: pco-W,
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
set: {x:A| B[x]} ,
param-co-W: pco-W,
all: ∀x:A. B[x],
pcw-path: Path,
implies: P ⇒ Q,
pcw-step-agree: StepAgree(s;p1;w),
apply: f a,
natural_number: $n,
squash: ↓T,
exists: ∃x:A. B[x],
nat: ℕ,
pcw-pp-barred: Barred(pp),
pcw-partial: pcw-partial(path;n)
FDL editor aliases :
param-W
Latex:
pW ==
\mlambda{}par.\{w:pco-W par| \mforall{}path:Path. (StepAgree(path 0;par;w) {}\mRightarrow{} (\mdownarrow{}\mexists{}n:\mBbbN{}. Barred(pcw-partial(path;n))))\}
Date html generated:
2016_07_08-PM-04_47_46
Last ObjectModification:
2015_09_22-PM-05_47_10
Theory : co-recursion
Home
Index