Nuprl Definition : consensus-rel-knowledge-step
consensus-rel-knowledge-step(V;A;W;x1;x2;y1;y2;a) ==
(∀b:{a:Id| (a ∈ A)}
((¬(b = a ∈ Id))
⇒ ((Inning(y1;b) = Inning(x1;b) ∈ ℤ)
∧ (Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V)
∧ (Knowledge(y2;b) = Knowledge(x2;b) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))))
∧ (consensus-rel-knowledge-inning-step(V;A;W;x1;x2;y1;y2;a)
∨ consensus-rel-knowledge-archive-step(V;A;W;x1;x2;y1;y2;a)
∨ consensus-rel-add-knowledge-step(V;A;W;x1;x2;y1;y2;a))
Definitions occuring in Statement :
consensus-rel-add-knowledge-step: consensus-rel-add-knowledge-step(V;A;W;x1;x2;y1;y2;a),
consensus-rel-knowledge-archive-step: consensus-rel-knowledge-archive-step(V;A;W;x1;x2;y1;y2;a),
consensus-rel-knowledge-inning-step: consensus-rel-knowledge-inning-step(V;A;W;x1;x2;y1;y2;a),
cs-knowledge: Knowledge(x;a),
cs-estimate: Estimate(s;a),
cs-inning: Inning(s;a),
fpf: a:A fp-> B[a],
Id: Id,
l_member: (x ∈ l),
top: Top,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
product: x:A × B[x],
union: left + right,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
consensus-rel-knowledge-step
Latex:
consensus-rel-knowledge-step(V;A;W;x1;x2;y1;y2;a) ==
(\mforall{}b:\{a:Id| (a \mmember{} A)\}
((\mneg{}(b = a))
{}\mRightarrow{} ((Inning(y1;b) = Inning(x1;b))
\mwedge{} (Estimate(y1;b) = Estimate(x1;b))
\mwedge{} (Knowledge(y2;b) = Knowledge(x2;b)))))
\mwedge{} (consensus-rel-knowledge-inning-step(V;A;W;x1;x2;y1;y2;a)
\mvee{} consensus-rel-knowledge-archive-step(V;A;W;x1;x2;y1;y2;a)
\mvee{} consensus-rel-add-knowledge-step(V;A;W;x1;x2;y1;y2;a))
Date html generated:
2016_05_16-PM-00_21_49
Last ObjectModification:
2012_02_25-AM-11_46_24
Theory : event-ordering
Home
Index