Nuprl Definition : pcw-steprel

If the "decision" d in step s1 = ⌜<p, w, d>⌝ is ⌜inl b⌝
then the next step s2 = ⌜<p', w', d'>⌝ must
have p' = ⌜C[p; a; b]⌝ and w' = ⌜f b⌝ (where w = ⌜<a, f>⌝).
If the path "ended" at step s1, then later steps are irrelevant
so there is no restriction.⋅

StepRel(s1;s2) ==  let p,w,d = s1 in let a,f = w in case d of inl(b) => StepAgree(s2;C[p; a; b];f b) | inr(x) => True

Definitions occuring in Statement : pcw-step-agree: StepAgree(s;p1;w), spreadn: spread3, true: True, apply: f a, spread: spread def, decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition : spreadn: spread3, spread: spread def, decide: case b of inl(x) => s[x] | inr(y) => t[y], pcw-step-agree: StepAgree(s;p1;w), apply: f a, true: True
FDL editor aliases : pcw-steprel

Latex:
StepRel(s1;s2) == let p,w,d = s1 in let a,f = w in case d of inl(b) => StepAgree(s2;C[p; a; b];f b) | inr(x) => True Date html generated: 2016_07_08-PM-04_47_42 Last ObjectModification: 2015_09_22-PM-05_47_01 Theory : co-recursion Home Index