Nuprl Definition : consensus-ts2
consensus-ts2(T) ==
<consensus-state2(T)
, AMBIVALENT
, λx,y. (((x = AMBIVALENT ∈ consensus-state2(T)) ∧ (∃v:T. (y = PREDECIDED[v] ∈ consensus-state2(T))))
∨ (∃v:T
((x = PREDECIDED[v] ∈ consensus-state2(T))
∧ ((y = Decided[v] ∈ consensus-state2(T)) ∨ (y = AMBIVALENT ∈ consensus-state2(T))))))
, λx.∃v:T. (x = Decided[v] ∈ consensus-state2(T))>
Definitions occuring in Statement :
cs-predecided: PREDECIDED[v],
cs-ambivalent: AMBIVALENT,
consensus-state2: consensus-state2(T),
cs-decided: Decided[v],
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
lambda: λx.A[x],
pair: <a, b>,
equal: s = t ∈ T
FDL editor aliases :
consensus-ts2
consensus-ts2(T) ==
<consensus-state2(T)
, AMBIVALENT
, \mlambda{}x,y. (((x = AMBIVALENT) \mwedge{} (\mexists{}v:T. (y = PREDECIDED[v])))
\mvee{} (\mexists{}v:T. ((x = PREDECIDED[v]) \mwedge{} ((y = Decided[v]) \mvee{} (y = AMBIVALENT)))))
, \mlambda{}x.\mexists{}v:T. (x = Decided[v])>
Date html generated:
2015_07_17-AM-11_21_52
Last ObjectModification:
2012_02_25-AM-11_39_53
Home
Index