Nuprl Definition : pcw-consistent-steps
pcw-consistent-steps(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];s1;s2) ==
let p,w,d = s1 in
let p',w',d' = s2 in
(p = p' ∈ P) ∧ (w = w' ∈ (pco-W p)) ∧ ((↑isl(d)) ⇒ (d = d' ∈ (B[p; fst(w)]?)))
Definitions occuring in Statement :
param-co-W: pco-W,
assert: ↑b,
isl: isl(x),
spreadn: spread3,
pi1: fst(t),
implies: P ⇒ Q,
and: P ∧ Q,
unit: Unit,
apply: f a,
union: left + right,
equal: s = t ∈ T
Definitions occuring in definition :
spreadn: spread3,
and: P ∧ Q,
apply: f a,
param-co-W: pco-W,
implies: P ⇒ Q,
assert: ↑b,
isl: isl(x),
equal: s = t ∈ T,
union: left + right,
pi1: fst(t),
unit: Unit
FDL editor aliases :
pcw-consistent-steps
Latex:
pcw-consistent-steps(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];s1;s2) ==
let p,w,d = s1 in
let p',w',d' = s2 in
(p = p') \mwedge{} (w = w') \mwedge{} ((\muparrow{}isl(d)) {}\mRightarrow{} (d = d'))
Date html generated:
2016_05_14-AM-06_12_41
Last ObjectModification:
2015_09_22-PM-05_47_02
Theory : co-recursion
Home
Index