Nuprl Definition : pcw-path
A full path through a co-W type is an infinite sequence of steps
such that each successive step agrees with the previous step.⋅
Path == {path:ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b])| ∀i:ℕ. StepRel(path i;path (i + 1))}
Definitions occuring in Statement :
pcw-steprel: StepRel(s1;s2),
pcw-step: pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]),
nat: ℕ,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
pcw-step: pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]),
all: ∀x:A. B[x],
nat: ℕ,
pcw-steprel: StepRel(s1;s2),
apply: f a,
add: n + m,
natural_number: $n
FDL editor aliases :
pcw-path
Latex:
Path ==
\{path:\mBbbN{} {}\mrightarrow{} pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b])| \mforall{}i:\mBbbN{}. StepRel(path i;path (i + 1))\}
Date html generated:
2016_07_08-PM-04_47_43
Last ObjectModification:
2015_09_22-PM-05_47_02
Theory : co-recursion
Home
Index