Nuprl Definition : consensus-ts5
consensus-ts5(V;A;W) ==
<ConsensusState × Knowledge(ConsensusState)
, <λa.<0, ⊗>, λa.mk_fpf(A;λb.<0, ff>)>
, λx,y. consensus-rel-knowledge(V;A;W;x;y)
, λx.∃v:V
∀a:{a:Id| (a ∈ A)}
((Inning(fst(x);a) = 0 ∈ ℤ)
∧ (Estimate(fst(x);a) = 0 : v ∈ i:ℤ fp-> V)
∧ (Knowledge(snd(x);a) = mk_fpf(A;λb.<0, ff>) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))>
Definitions occuring in Statement :
consensus-rel-knowledge: consensus-rel-knowledge(V;A;W;x;y),
cs-knowledge: Knowledge(x;a),
consensus-state5: Knowledge(ConsensusState),
cs-estimate: Estimate(s;a),
cs-inning: Inning(s;a),
consensus-state4: ConsensusState,
mk_fpf: mk_fpf(L;f),
fpf-single: x : v,
fpf-empty: ⊗,
fpf: a:A fp-> B[a],
Id: Id,
l_member: (x ∈ l),
bfalse: ff,
top: Top,
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
lambda: λx.A[x],
pair: <a, b>,
product: x:A × B[x],
union: left + right,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
consensus-ts5
Latex:
consensus-ts5(V;A;W) ==
<ConsensusState \mtimes{} Knowledge(ConsensusState)
, <\mlambda{}a.ɘ, \motimes{}>, \mlambda{}a.mk\_fpf(A;\mlambda{}b.ɘ, ff>)>
, \mlambda{}x,y. consensus-rel-knowledge(V;A;W;x;y)
, \mlambda{}x.\mexists{}v:V
\mforall{}a:\{a:Id| (a \mmember{} A)\}
((Inning(fst(x);a) = 0)
\mwedge{} (Estimate(fst(x);a) = 0 : v)
\mwedge{} (Knowledge(snd(x);a) = mk\_fpf(A;\mlambda{}b.ɘ, ff>)))>
Date html generated:
2016_05_16-PM-00_22_26
Last ObjectModification:
2012_02_25-AM-11_46_36
Theory : event-ordering
Home
Index