Nuprl Definition : consensus-rel-knowledge-archive-step
consensus-rel-knowledge-archive-step(V;A;W;x1;x2;y1;y2;a) ==
((Inning(y1;a) = Inning(x1;a) ∈ ℤ) ∧ (Knowledge(y2;a) = Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))
∧ (¬(Inning(x1;a) ∈ fpf-domain(Estimate(x1;a))))
∧ (∃v:V
(may consider v in inning Inning(x1;a) based on knowledge (Knowledge(x2;a))
∧ (Estimate(y1;a) = Estimate(x1;a) ⊕ Inning(x1;a) : v ∈ i:ℤ fp-> V)))
Definitions occuring in Statement :
cs-knowledge: Knowledge(x;a),
cs-knowledge-precondition: may consider v in inning i based on knowledge (s),
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,
top: Top,
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q,
product: x:A × B[x],
union: left + right,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
consensus-rel-knowledge-archive-step
Latex:
consensus-rel-knowledge-archive-step(V;A;W;x1;x2;y1;y2;a) ==
((Inning(y1;a) = Inning(x1;a)) \mwedge{} (Knowledge(y2;a) = Knowledge(x2;a)))
\mwedge{} (\mneg{}(Inning(x1;a) \mmember{} fpf-domain(Estimate(x1;a))))
\mwedge{} (\mexists{}v:V
(may consider v in inning Inning(x1;a) based on knowledge (Knowledge(x2;a))
\mwedge{} (Estimate(y1;a) = Estimate(x1;a) \moplus{} Inning(x1;a) : v)))
Date html generated:
2016_05_16-PM-00_21_13
Last ObjectModification:
2012_02_25-AM-11_46_12
Theory : event-ordering
Home
Index