consensus-ts3(T) ==
<consensus-state3(T) List
, []
, 
x,y.
((y = (x @ [INITIAL]))
((||y|| = ||x||)
(
i:
||x||
((
j:||x||. ((
(j = i)) 
(y[j] = x[j])))
(((x[i] = INITIAL)
((y[i] = WITHDRAWN)
(v:T
((y[i] = CONSIDERING[v])
(j:i
((x[j] = WITHDRAWN)
(x[j] = CONSIDERING[v])
(x[j] = COMMITED[v])))))))
(v:T
((x[i] = CONSIDERING[v])
((y[i] = COMMITED[v]) (y[i] = WITHDRAWN)))))))))
, x.v:T. (x = [COMMITED[v]])>
Definitions :
pair: <a, b>,
append: as @ bs,
length: ||as||,
implies: P Q,
not: A,
int: 
,
cs-initial: INITIAL,
all: x:A. B[x],
int_seg: {i..j
},
natural_number: $n,
and: P Q,
cs-considering: CONSIDERING[v],
or: P Q,
select: l[i],
cs-withdrawn: WITHDRAWN,
lambda: x.A[x],
exists: x:A. B[x],
equal: s = t,
list: type List,
consensus-state3: consensus-state3(T),
cons: [car / cdr],
cs-commited: COMMITED[v],
nil: []
FDL editor aliases :
consensus-ts3
consensus-ts3(T) ==
<consensus-state3(T) List
, []
, \mlambda{}x,y.
((y = (x @ [INITIAL]))
\mvee{} ((||y|| = ||x||)
\mwedge{} (\mexists{}i:\mBbbN{}||x||
((\mforall{}j:\mBbbN{}||x||. ((\mneg{}(j = i)) {}\mRightarrow{} (y[j] = x[j])))
\mwedge{} (((x[i] = INITIAL)
\mwedge{} ((y[i] = WITHDRAWN)
\mvee{} (\mexists{}v:T
((y[i] = CONSIDERING[v])
\mwedge{} (\mforall{}j:\mBbbN{}i
((x[j] = WITHDRAWN) \mvee{} (x[j] = CONSIDERING[v]) \mvee{} (x[j] = COMMITED[v])))))))
\mvee{} (\mexists{}v:T. ((x[i] = CONSIDERING[v]) \mwedge{} ((y[i] = COMMITED[v]) \mvee{} (y[i] = WITHDRAWN)))))))))
, \mlambda{}x.\mexists{}v:T. (x = [COMMITED[v]])>
Date html generated:
2010_08_27-AM-12_28_11
Last ObjectModification:
2009_12_23-PM-03_22_57
Home
Index