Nuprl Definition : pcw-step-agree
The first and second parts of the triple s (the parameter p and tree w')
agree with the given parameter p1 and tree w.⋅
StepAgree(s;p1;w) == let p,w',b = s in (p = p1 ∈ P) ∧ (w' = w ∈ (pco-W p1))
Definitions occuring in Statement :
param-co-W: pco-W,
spreadn: spread3,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
spreadn: spread3,
and: P ∧ Q,
equal: s = t ∈ T,
apply: f a,
param-co-W: pco-W
FDL editor aliases :
pcw-step-agree
Latex:
StepAgree(s;p1;w) == let p,w',b = s in (p = p1) \mwedge{} (w' = w)
Date html generated:
2016_07_08-PM-04_47_41
Last ObjectModification:
2015_09_22-PM-05_47_01
Theory : co-recursion
Home
Index