consensus-rel-add-knowledge-step(V;A;W;x1;x2;y1;y2;a) ==
(Inning(y1;a) = Inning(x1;a))
(Estimate(y1;a) = Estimate(x1;a))
(
b:{a:Id| (a 
A)}
i:
((i 
Inning(x1;b))
(((
j:. ((j < i) 
(
j dom(Estimate(x1;b)))))
(Knowledge(y2;a) = b : <i, inr 
> 
Knowledge(x2;a)))
(j:
((j < i)
(j dom(Estimate(x1;b)))
(k:. ((j < k) (k < i) (k dom(Estimate(x1;b)))))
(Knowledge(y2;a)
= b : <i, inl <j, Estimate(x1;b)(j)> > Knowledge(x2;a)))))))
Definitions :
set: {x:A| B[x]} ,
l_member: (x l),
le: A B,
cs-inning: Inning(s;a),
or: P Q,
inr: inr x ,
it: ,
exists: x:A. B[x],
and: P Q,
all: x:A. B[x],
implies: P Q,
less_than: a < b,
not: A,
assert: b,
fpf-dom: x dom(f),
equal: s = t,
fpf: a:A fp-> B[a],
Id: Id,
union: left + right,
product: x:A 
B[x],
int: ,
top: Top,
fpf-join: f g,
id-deq: IdDeq,
fpf-single: x : v,
inl: inl x ,
pair: <a, b>,
fpf-ap: f(x),
cs-estimate: Estimate(s;a),
int-deq: IntDeq,
cs-knowledge: Knowledge(x;a)
FDL editor aliases :
consensus-rel-add-knowledge-step
consensus-rel-add-knowledge-step(V;A;W;x1;x2;y1;y2;a) ==
(Inning(y1;a) = Inning(x1;a))
\mwedge{} (Estimate(y1;a) = Estimate(x1;a))
\mwedge{} (\mexists{}b:\{a:Id| (a \mmember{} A)\}
\mexists{}i:\mBbbZ{}
((i \mleq{} Inning(x1;b))
\mwedge{} (((\mforall{}j:\mBbbZ{}. ((j < i) {}\mRightarrow{} (\mneg{}\muparrow{}j \mmember{} dom(Estimate(x1;b)))))
\mwedge{} (Knowledge(y2;a) = b : <i, inr \mcdot{} > \moplus{} Knowledge(x2;a)))
\mvee{} (\mexists{}j:\mBbbZ{}
((j < i)
\mwedge{} (\muparrow{}j \mmember{} dom(Estimate(x1;b)))
\mwedge{} (\mforall{}k:\mBbbZ{}. ((j < k) {}\mRightarrow{} (k < i) {}\mRightarrow{} (\mneg{}\muparrow{}k \mmember{} dom(Estimate(x1;b)))))
\mwedge{} (Knowledge(y2;a) = b : <i, inl <j, Estimate(x1;b)(j)> > \moplus{} Knowledge(x2;a)))))))
Date html generated:
2010_08_27-AM-12_53_58
Last ObjectModification:
2009_12_23-PM-03_28_47
Home
Index