Nuprl Definition : three-consensus-ts
three-consensus-ts(V;A;t;f) ==
<{a:Id| (a ∈ A)} ─→ (consensus-rcv(V;A) List)
, λa.[]
, λx,y. ∃a:{a:Id| (a ∈ A)}
∃e:consensus-rcv(V;A)
((∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀v:V.
((e = Vote[b;i;v] ∈ consensus-rcv(V;A))
⇒ ((∃L:consensus-rcv(V;A) List. (L ≤ x b ∧ archive-condition(V;A;t;f;i;v;L))) ∧ (¬(e ∈ x a)))))
∧ (∀b:{a:Id| (a ∈ A)} . ((¬(b = a ∈ Id)) ⇒ ((y b) = (x b) ∈ (consensus-rcv(V;A) List))))
∧ ((y a) = ((x a) @ [e]) ∈ (consensus-rcv(V;A) List)))
, λx.∃v:V. ∀a:{a:Id| (a ∈ A)} . ((x a) = [Init[v]] ∈ (consensus-rcv(V;A) List))>
Definitions occuring in Statement :
archive-condition: archive-condition(V;A;t;f;n;v;L),
cs-rcv-vote: Vote[a;i;v],
cs-initial-rcv: Init[v],
consensus-rcv: consensus-rcv(V;A),
Id: Id,
iseg: l1 ≤ l2,
l_member: (x ∈ l),
append: as @ bs,
cons: [a / b],
nil: [],
list: T List,
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
function: x:A ─→ B[x],
pair: <a, b>,
equal: s = t ∈ T
FDL editor aliases :
three-consensus-ts
three-consensus-ts(V;A;t;f) ==
<\{a:Id| (a \mmember{} A)\} {}\mrightarrow{} (consensus-rcv(V;A) List)
, \mlambda{}a.[]
, \mlambda{}x,y. \mexists{}a:\{a:Id| (a \mmember{} A)\}
\mexists{}e:consensus-rcv(V;A)
((\mforall{}b:\{a:Id| (a \mmember{} A)\} . \mforall{}i:\mBbbN{}. \mforall{}v:V.
((e = Vote[b;i;v])
{}\mRightarrow{} ((\mexists{}L:consensus-rcv(V;A) List. (L \mleq{} x b \mwedge{} archive-condition(V;A;t;f;i;v;L)))
\mwedge{} (\mneg{}(e \mmember{} x a)))))
\mwedge{} (\mforall{}b:\{a:Id| (a \mmember{} A)\} . ((\mneg{}(b = a)) {}\mRightarrow{} ((y b) = (x b))))
\mwedge{} ((y a) = ((x a) @ [e])))
, \mlambda{}x.\mexists{}v:V. \mforall{}a:\{a:Id| (a \mmember{} A)\} . ((x a) = [Init[v]])>
Date html generated:
2015_07_17-AM-11_52_11
Last ObjectModification:
2012_02_25-AM-11_51_18
Home
Index