Nuprl Definition : consensus-ts4
consensus-ts4(V;A;W) ==
<ConsensusState
, λa.<-1, ⊗>
, λx,y. CR[x,y]
, λx.∃v:V. ∀a:{a:Id| (a ∈ A)} . ((Inning(x;a) = 0 ∈ ℤ) ∧ (Estimate(x;a) = 0 : v ∈ i:ℤ fp-> V))>
Definitions occuring in Statement :
consensus-rel: CR[x,y],
cs-estimate: Estimate(s;a),
cs-inning: Inning(s;a),
consensus-state4: ConsensusState,
fpf-single: x : v,
fpf-empty: ⊗,
fpf: a:A fp-> B[a],
Id: Id,
l_member: (x ∈ l),
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>,
minus: -n,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
consensus-ts4
Latex:
consensus-ts4(V;A;W) ==
<ConsensusState
, \mlambda{}a.<-1, \motimes{}>
, \mlambda{}x,y. CR[x,y]
, \mlambda{}x.\mexists{}v:V. \mforall{}a:\{a:Id| (a \mmember{} A)\} . ((Inning(x;a) = 0) \mwedge{} (Estimate(x;a) = 0 : v))>
Date html generated:
2016_05_16-AM-11_56_28
Last ObjectModification:
2012_02_25-AM-11_42_21
Theory : event-ordering
Home
Index