consensus-rel-knowledge-step(V;A;W;x1;x2;y1;y2;a) ==
(
b:{a:Id| (a 
A)}
((
(b = a))
((Inning(y1;b) = Inning(x1;b))
(Estimate(y1;b) = Estimate(x1;b))
(Knowledge(y2;b) = Knowledge(x2;b)))))
(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 :
all: x:A. B[x],
set: {x:A| B[x]} ,
l_member: (x l),
implies: P Q,
not: A,
cs-inning: Inning(s;a),
and: P Q,
cs-estimate: Estimate(s;a),
equal: s = t,
fpf: a:A fp-> B[a],
Id: Id,
union: left + right,
product: x:A 
B[x],
int: 
,
top: Top,
cs-knowledge: Knowledge(x;a),
consensus-rel-knowledge-inning-step: consensus-rel-knowledge-inning-step(V;A;W;x1;x2;y1;y2;a),
or: P Q,
consensus-rel-knowledge-archive-step: consensus-rel-knowledge-archive-step(V;A;W;x1;x2;y1;y2;a),
consensus-rel-add-knowledge-step: consensus-rel-add-knowledge-step(V;A;W;x1;x2;y1;y2;a)
FDL editor aliases :
consensus-rel-knowledge-step
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:
2010_08_27-AM-12_54_04
Last ObjectModification:
2009_12_23-PM-03_28_53
Home
Index