{ 
[V:Type]
A:Id List. t:
. f:V List 
V. n:
. v:V.
(archive-condition(V;A;t;f;n;v;[]) 
False) }
{ Proof }
Definitions occuring in Statement :
archive-condition: archive-condition(V;A;t;f;n;v;L),
Id: Id,
nat: ,
uall: [x:A]. B[x],
all: x:A. B[x],
iff: P Q,
false: False,
function: x:A B[x],
nil: [],
list: type List,
int: ,
universe: Type
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
iff: P Q,
and: P 
Q,
implies: P Q,
rev_implies: P Q,
member: t 
T,
false: False,
archive-condition: archive-condition(V;A;t;f;n;v;L),
exists: 
x:A. B[x],
append: as @ bs,
assert: 
b,
null: null(as),
filter: filter(P;l),
reduce: reduce(f;k;as),
ifthenelse: if b then t else f fi ,
btrue: tt,
prop: 
Lemmas :
archive-condition_wf,
consensus-rcv_wf,
nat_wf,
Id_wf
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}t:\mBbbN{}. \mforall{}f:V List {}\mrightarrow{} V. \mforall{}n:\mBbbZ{}. \mforall{}v:V. (archive-condition(V;A;t;f;n;v;[]) \mLeftarrow{}{}\mRightarrow{} False)
Date html generated:
2011_08_16-AM-10_12_08
Last ObjectModification:
2011_06_18-AM-09_04_31
Home
Index