Nuprl Definition : pcw-step

A step in a path through a parameterized-co-W type
is a triple ⌜<p, w, d>⌝ where ⌜p ∈ P⌝ is the current parameter,
⌜w ∈ pco-W p⌝ is the current "co-tree" (i.e. non-well-founded tree)
and d is a "decision",
When d is ⌜inl b⌝ where b is a member of the domain
of ⌜snd(w)⌝ (i.e. a member of ⌜B[p; fst(w)]⌝)
then the path will continue with a next step.
When d is ⌜inr ⋅ ⌝ then the path ends at this step.⋅

pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]) == p:P × w:pco-W p × (B[p; fst(w)]?)

Definitions occuring in Statement : param-co-W: pco-W, pi1: fst(t), unit: Unit, apply: f a, product: x:A × B[x], union: left + right
Definitions occuring in definition : product: x:A × B[x], apply: f a, param-co-W: pco-W, union: left + right, pi1: fst(t), unit: Unit
FDL editor aliases : pcw-step

Latex:
pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]) == p:P \mtimes{} w:pco-W p \mtimes{} (B[p; fst(w)]?) Date html generated: 2016_07_08-PM-04_47_39 Last ObjectModification: 2015_09_22-PM-05_47_00 Theory : co-recursion Home Index