Nuprl Definition : consensus-rel-add-knowledge-step
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) ∈ i:ℤ fp-> V)
∧ (∃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) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))
∨ (∃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) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))\000C)))
Definitions occuring in Statement :
cs-knowledge: Knowledge(x;a),
cs-estimate: Estimate(s;a),
cs-inning: Inning(s;a),
fpf-single: x : v,
fpf-join: f ⊕ g,
fpf-ap: f(x),
fpf-dom: x ∈ dom(f),
fpf: a:A fp-> B[a],
id-deq: IdDeq,
Id: Id,
int-deq: IntDeq,
l_member: (x ∈ l),
assert: ↑b,
less_than: a < b,
it: ⋅,
top: Top,
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
pair: <a, b>,
product: x:A × B[x],
inr: inr x ,
inl: inl x,
union: left + right,
int: ℤ,
equal: s = t ∈ T
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:
2015_07_17-AM-11_40_36
Last ObjectModification:
2012_02_25-AM-11_46_18
Home
Index