archive-condition(V;A;t;f;n;v;L) ==
L':consensus-rcv(V;A) List
r:consensus-rcv(V;A)
((L = (L' @ [r]))
(((L' = [])
(((r = Init[v]) (n = 0))
((0 
n) (a:{a:Id| (a 
A)} . (r = Vote[a;n;v])))))
(((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]))
((((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))))))
Definitions :
append: as @ bs,
cons: [car / cdr],
list: type List,
nil: [],
cs-initial-rcv: Init[v],
int: 
,
less_than: a < b,
assert: b,
null: null(as),
filter: filter(P;l),
lambda: x.A[x],
rcvd-inning-gt: i <z inning(r),
or: P Q,
exists: x:A. B[x],
set: {x:A| B[x]} ,
l_member: (x l),
Id: Id,
consensus-rcv: consensus-rcv(V;A),
cs-rcv-vote: Vote[a;i;v],
and: P Q,
le: A B,
add: n + m,
multiply: n * m,
length: ||as||,
equal: s = t,
apply: f a,
values-for-distinct: values-for-distinct(eq;L),
id-deq: IdDeq,
votes-from-inning: votes-from-inning(i;L),
subtract: n - m,
natural_number: $n
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:
2010_08_27-AM-12_57_15
Last ObjectModification:
2009_12_23-PM-03_32_26
Home
Index