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