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