Nuprl Definition : consensus-ts1
consensus-ts1(T) ==
<consensus-state1(T)
, UNDECIDED
, λx,y. ((x = UNDECIDED ∈ consensus-state1(T)) ∧ (∃v:T. (y = Decided[v] ∈ consensus-state1(T))))
, λx.∃v:T. (x = Decided[v] ∈ consensus-state1(T))>
Definitions occuring in Statement :
cs-decided: Decided[v],
cs-undecided: UNDECIDED,
consensus-state1: consensus-state1(V),
exists: ∃x:A. B[x],
and: P ∧ Q,
lambda: λx.A[x],
pair: <a, b>,
equal: s = t ∈ T
FDL editor aliases :
consensus-ts1
consensus-ts1(T) ==
<consensus-state1(T)
, UNDECIDED
, \mlambda{}x,y. ((x = UNDECIDED) \mwedge{} (\mexists{}v:T. (y = Decided[v])))
, \mlambda{}x.\mexists{}v:T. (x = Decided[v])>
Date html generated:
2015_07_17-AM-11_21_05
Last ObjectModification:
2012_02_25-AM-11_39_20
Home
Index