Nuprl Definition : consensus-rel
CR[x,y] ==
∃a:{a:Id| (a ∈ A)}
((∀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,
int-deq: IntDeq,
l_member: (x ∈ l),
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
CR[x,y] ==
\mexists{}a:\{a:Id| (a \mmember{} A)\}
((\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:
2015_07_17-AM-11_26_12
Last ObjectModification:
2012_02_25-AM-11_42_11
Home
Index