Nuprl Definition : archive-condition
archive-condition(V;A;t;f;n;v;L) ==
∃L':consensus-rcv(V;A) List
∃r:consensus-rcv(V;A)
((L = (L' @ [r]) ∈ (consensus-rcv(V;A) List))
∧ (((L' = [] ∈ (consensus-rcv(V;A) List))
∧ (((r = Init[v] ∈ consensus-rcv(V;A)) ∧ (n = 0 ∈ ℤ))
∨ ((0 ≤ n) ∧ (∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n;v] ∈ consensus-rcv(V;A))))))
∨ ((0 < n
∧ (||values-for-distinct(IdDeq;votes-from-inning(n - 1;L'))|| ≤ (2 * t))
∧ (↑null(filter(λr.n - 1 <z inning(r);L'))))
∧ ((∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n;v] ∈ consensus-rcv(V;A)))
∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n - 1;L))||)
∧ ((f values-for-distinct(IdDeq;votes-from-inning(n - 1;L))) = v ∈ V))))))
Definitions occuring in Statement :
votes-from-inning: votes-from-inning(i;L),
rcvd-inning-gt: i <z inning(r),
cs-rcv-vote: Vote[a;i;v],
cs-initial-rcv: Init[v],
consensus-rcv: consensus-rcv(V;A),
id-deq: IdDeq,
Id: Id,
values-for-distinct: values-for-distinct(eq;L),
l_member: (x ∈ l),
filter: filter(P;l),
length: ||as||,
append: as @ bs,
null: null(as),
cons: [a / b],
nil: [],
list: T List,
assert: ↑b,
less_than: a < b,
le: A ≤ B,
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
archive-condition
archive-condition(V;A;t;f;n;v;L) ==
\mexists{}L':consensus-rcv(V;A) List
\mexists{}r:consensus-rcv(V;A)
((L = (L' @ [r]))
\mwedge{} (((L' = [])
\mwedge{} (((r = Init[v]) \mwedge{} (n = 0)) \mvee{} ((0 \mleq{} n) \mwedge{} (\mexists{}a:\{a:Id| (a \mmember{} A)\} . (r = Vote[a;n;v])))))
\mvee{} ((0 < n
\mwedge{} (||values-for-distinct(IdDeq;votes-from-inning(n - 1;L'))|| \mleq{} (2 * t))
\mwedge{} (\muparrow{}null(filter(\mlambda{}r.n - 1 <z inning(r);L'))))
\mwedge{} ((\mexists{}a:\{a:Id| (a \mmember{} A)\} . (r = Vote[a;n;v]))
\mvee{} ((((2 * t) + 1) \mleq{} ||values-for-distinct(IdDeq;votes-from-inning(n - 1;L))||)
\mwedge{} ((f values-for-distinct(IdDeq;votes-from-inning(n - 1;L))) = v))))))
Date html generated:
2015_07_17-AM-11_48_13
Last ObjectModification:
2012_02_25-AM-11_49_42
Home
Index