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)))
(
(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)))
Definitions :
Id: Id,
union: left + right,
product: x:A 
B[x],
top: Top,
not: A,
l_member: (x l),
fpf-domain: fpf-domain(f),
exists: x:A. B[x],
and: P Q,
cs-knowledge-precondition: may consider v in inning i based on knowledge (s),
cs-knowledge: Knowledge(x;a),
equal: s = t,
fpf: a:A fp-> B[a],
int: 
,
fpf-join: f g,
int-deq: IntDeq,
cs-estimate: Estimate(s;a),
fpf-single: x : v,
cs-inning: Inning(s;a)
FDL editor aliases :
consensus-rel-knowledge-archive-step
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:
2010_08_27-AM-12_53_51
Last ObjectModification:
2009_12_23-PM-03_28_42
Home
Index