Nuprl Definition : consensus-ts3
consensus-ts3(T) ==
<consensus-state3(T) List
, []
, λx,y. ((y = (x @ [INITIAL]) ∈ (consensus-state3(T) List))
∨ ((||y|| = ||x|| ∈ ℤ)
∧ (∃i:ℕ||x||
((∀j:ℕ||x||. ((¬(j = i ∈ ℤ)) ⇒ (y[j] = x[j] ∈ consensus-state3(T))))
∧ (((x[i] = INITIAL ∈ consensus-state3(T))
∧ ((y[i] = WITHDRAWN ∈ consensus-state3(T))
∨ (∃v:T
((y[i] = CONSIDERING[v] ∈ consensus-state3(T))
∧ (∀j:ℕi
((x[j] = WITHDRAWN ∈ consensus-state3(T))
∨ (x[j] = CONSIDERING[v] ∈ consensus-state3(T))
∨ (x[j] = COMMITED[v] ∈ consensus-state3(T))))))))
∨ (∃v:T
((x[i] = CONSIDERING[v] ∈ consensus-state3(T))
∧ ((y[i] = COMMITED[v] ∈ consensus-state3(T)) ∨ (y[i] = WITHDRAWN ∈ consensus-state3(T))))))))))
, λx.∃v:T. (x = [COMMITED[v]] ∈ (consensus-state3(T) List))>
Definitions occuring in Statement :
cs-commited: COMMITED[v],
cs-considering: CONSIDERING[v],
cs-withdrawn: WITHDRAWN,
cs-initial: INITIAL,
consensus-state3: consensus-state3(T),
select: L[n],
length: ||as||,
append: as @ bs,
cons: [a / b],
nil: [],
list: T List,
int_seg: {i..j-},
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
lambda: λx.A[x],
pair: <a, b>,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
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:
2015_07_17-AM-11_23_49
Last ObjectModification:
2012_02_25-AM-11_41_17
Home
Index