Nuprl Definition : consensus-event-constraint
e@a allowed in state x ==
(∀v:V
((e = Archive(v) ∈ consensus-event(V;A))
⇒ let i,est,knw = consensus-accum-state(A;x a) in
(¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw)))
∧ (∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
((e = consensus-message(b;i;z) ∈ consensus-event(V;A))
⇒ let i',est,knw = consensus-accum-state(A;x b) in
(i ≤ i')
∧ case z
of inl(p) =>
let j,v = p
in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (j < k ⇒ k < i ⇒ (¬↑k ∈ dom(est)))) ∧ (v = est(j) ∈ V)
| inr(a) =>
∀j:ℤ. (j < i ⇒ (¬↑j ∈ dom(est)))))
Definitions occuring in Statement :
consensus-accum-state: consensus-accum-state(A;L),
consensus-message: consensus-message(b;i;z),
archive-event: Archive(v),
consensus-event: consensus-event(V;A),
cs-knowledge-precondition: may consider v in inning i based on knowledge (s),
fpf-ap: f(x),
fpf-domain: fpf-domain(f),
fpf-dom: x ∈ dom(f),
Id: Id,
int-deq: IntDeq,
l_member: (x ∈ l),
int_seg: {i..j-},
nat: ℕ,
assert: ↑b,
less_than: a < b,
spreadn: spread3,
le: A ≤ B,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
unit: Unit,
set: {x:A| B[x]} ,
apply: f a,
spread: spread def,
product: x:A × B[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
union: left + right,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
consensus-event-constraint
e@a allowed in state x ==
(\mforall{}v:V
((e = Archive(v))
{}\mRightarrow{} let i,est,knw = consensus-accum-state(A;x a) in
(\mneg{}(i \mmember{} fpf-domain(est))) \mwedge{} may consider v in inning i based on knowledge (knw)))
\mwedge{} (\mforall{}b:\{a:Id| (a \mmember{} A)\} . \mforall{}i:\mBbbN{}. \mforall{}z:\mBbbN{}i \mtimes{} V?.
((e = consensus-message(b;i;z))
{}\mRightarrow{} let i',est,knw = consensus-accum-state(A;x b) in
(i \mleq{} i')
\mwedge{} case z
of inl(p) =>
let j,v = p
in (\muparrow{}j \mmember{} dom(est)) \mwedge{} (\mforall{}k:\mBbbZ{}. (j < k {}\mRightarrow{} k < i {}\mRightarrow{} (\mneg{}\muparrow{}k \mmember{} dom(est)))) \mwedge{} (v = est(j))
| inr(a) =>
\mforall{}j:\mBbbZ{}. (j < i {}\mRightarrow{} (\mneg{}\muparrow{}j \mmember{} dom(est)))))
Date html generated:
2015_07_17-AM-11_45_20
Last ObjectModification:
2012_02_25-AM-11_48_07
Home
Index