consensus-ts1(T) ==
<consensus-state1(T)
, UNDECIDED
, 
x,y.((x = UNDECIDED) 
(
v:T. (y = Decided[v])))
, x.v:T. (x = Decided[v])>
Definitions :
pair: <a, b>,
and: P Q,
cs-undecided: UNDECIDED,
lambda: x.A[x],
exists: x:A. B[x],
equal: s = t,
consensus-state1: consensus-state1(V),
cs-decided: Decided[v]
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:
2010_08_27-AM-12_26_29
Last ObjectModification:
2009_12_23-PM-03_20_32
Home
Index