Nuprl Lemma : archive-condition-append-init
[V:Type]
A:Id List. t:
. f:V List 
V. L:consensus-rcv(V;A) List. n:
. v,v2:V.
(archive-condition(V;A;t;f;n;v;L @ [Init[v2]]) 
{(L = []) 
(n = 0) (v2 = v)})
Proof not projected
Definitions occuring in Statement :
archive-condition: archive-condition(V;A;t;f;n;v;L),
cs-initial-rcv: Init[v],
consensus-rcv: consensus-rcv(V;A),
Id: Id,
append: as @ bs,
nat: ,
uall: [x:A]. B[x],
guard: {T},
all: x:A. B[x],
iff: P Q,
and: P Q,
function: x:A B[x],
cons: [car / cdr],
nil: [],
list: type List,
natural_number: $n,
int: ,
universe: Type,
equal: s = t
Definitions :
cand: A c B,
so_lambda: 
x.t[x],
prop: 
,
member: t 
T,
rev_implies: P Q,
implies: P Q,
or: P 
Q,
exists: 
x:A. B[x],
and: P Q,
archive-condition: archive-condition(V;A;t;f;n;v;L),
iff: P Q,
nat: ,
all: x:A. B[x],
uall: [x:A]. B[x],
ycomb: Y,
top: Top,
guard: {T},
length: ||as||,
true: True,
ifthenelse: if b then t else f fi ,
btrue: tt,
isl: isl(x),
assert: 
b,
outl: outl(x),
subtype: S 
T,
votes-from-inning: votes-from-inning(i;L),
bfalse: ff,
reduce: reduce(f;k;as),
rcv-vote?: rcv-vote?(x),
band: p 
q,
map: map(f;as),
rcvd-inning-eq: inning(r) =
i,
mapfilter: mapfilter(f;P;L),
filter: filter(P;l),
cs-initial-rcv: Init[v],
squash: 
T,
null: null(as),
values-for-distinct: values-for-distinct(eq;L),
remove-repeats: remove-repeats(eq;L),
uimplies: b supposing a,
so_apply: x[s],
tl: tl(l),
hd: hd(l),
decidable: Dec(P),
consensus-rcv: consensus-rcv(V;A),
false: False,
not: 
A,
cs-rcv-vote: Vote[a;i;v],
le: A 
B
Lemmas :
nat_wf,
guard_wf,
rcvd-inning-gt_wf,
filter_wf_top,
null_wf3,
assert_wf,
votes-from-inning_wf,
strong-subtype-self,
strong-subtype-set3,
strong-subtype-deq-subtype,
id-deq_wf,
values-for-distinct_wf,
length_wf,
cs-rcv-vote_wf,
equal_wf,
l_member_wf,
Id_wf,
le_wf,
or_wf,
cs-initial-rcv_wf,
append_wf,
consensus-rcv_wf,
exists_wf,
tl_wf,
ge_wf,
hd_wf,
top_wf,
length_wf_nat,
decidable__equal_int,
general-append-cancellation,
isl_wf,
outl_wf,
append-nil,
rcvd-inning-eq_wf,
mapfilter-append,
true_wf,
squash_wf,
and_wf
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}t:\mBbbN{}. \mforall{}f:V List {}\mrightarrow{} V. \mforall{}L:consensus-rcv(V;A) List. \mforall{}n:\mBbbZ{}. \mforall{}v,v2:V.
(archive-condition(V;A;t;f;n;v;L @ [Init[v2]]) \mLeftarrow{}{}\mRightarrow{} \{(L = []) \mwedge{} (n = 0) \mwedge{} (v2 = v)\})
Date html generated:
2012_01_23-PM-12_07_14
Last ObjectModification:
2011_12_19-PM-04_34_31
Home
Index