Nuprl Definition : consensus-rel-mod
CR(in ws)[x, y] ==
∃a:{a:Id| (a ∈ A)}
((a ∈ ws)
∧ (∀b:{a:Id| (a ∈ A)}
((¬(b = a ∈ Id)) ⇒ ((Inning(y;b) = Inning(x;b) ∈ ℤ) ∧ (Estimate(y;b) = Estimate(x;b) ∈ i:ℤ fp-> V))))
∧ (((Inning(y;a) = (Inning(x;a) + 1) ∈ ℤ) ∧ (Estimate(y;a) = Estimate(x;a) ∈ i:ℤ fp-> V))
∨ ((Inning(y;a) = Inning(x;a) ∈ ℤ)
∧ (¬(Inning(x;a) ∈ fpf-domain(Estimate(x;a))))
∧ (∃v:V
(state x may consider v in inning Inning(x;a)
∧ (Estimate(y;a) = Estimate(x;a) ⊕ Inning(x;a) : v ∈ i:ℤ fp-> V))))))
Definitions occuring in Statement :
cs-precondition: state s may consider v in inning i,
cs-estimate: Estimate(s;a),
cs-inning: Inning(s;a),
fpf-single: x : v,
fpf-join: f ⊕ g,
fpf-domain: fpf-domain(f),
fpf: a:A fp-> B[a],
Id: Id,
l_member: (x ∈ l),
int-deq: IntDeq,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
consensus-rel-mod
Latex:
CR(in ws)[x, y] ==
\mexists{}a:\{a:Id| (a \mmember{} A)\}
((a \mmember{} ws)
\mwedge{} (\mforall{}b:\{a:Id| (a \mmember{} A)\}
((\mneg{}(b = a)) {}\mRightarrow{} ((Inning(y;b) = Inning(x;b)) \mwedge{} (Estimate(y;b) = Estimate(x;b)))))
\mwedge{} (((Inning(y;a) = (Inning(x;a) + 1)) \mwedge{} (Estimate(y;a) = Estimate(x;a)))
\mvee{} ((Inning(y;a) = Inning(x;a))
\mwedge{} (\mneg{}(Inning(x;a) \mmember{} fpf-domain(Estimate(x;a))))
\mwedge{} (\mexists{}v:V
(state x may consider v in inning Inning(x;a)
\mwedge{} (Estimate(y;a) = Estimate(x;a) \moplus{} Inning(x;a) : v))))))
Date html generated:
2016_05_16-AM-11_56_11
Last ObjectModification:
2012_02_25-AM-11_42_16
Theory : event-ordering
Home
Index