consensus-ts2(T) ==
<consensus-state2(T)
, AMBIVALENT
, 
x,y.
(((x = AMBIVALENT) 
(
v:T. (y = PREDECIDED[v])))
(v:T. ((x = PREDECIDED[v]) ((y = Decided[v]) (y = AMBIVALENT)))))
, x.v:T. (x = Decided[v])>
Definitions :
pair: <a, b>,
and: P Q,
cs-predecided: PREDECIDED[v],
or: P Q,
cs-ambivalent: AMBIVALENT,
lambda: x.A[x],
exists: x:A. B[x],
equal: s = t,
consensus-state2: consensus-state2(T),
cs-decided: Decided[v]
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:
2010_08_27-AM-12_26_56
Last ObjectModification:
2009_12_23-PM-03_21_04
Home
Index