{ 
[V:Type]. [A:Id List]. [t:
]. [f:V List 
V].
[L:consensus-rcv(V;A) List]. [n:
]. [v:V].
[L1:consensus-rcv(V;A) List]
[v1:V]. (
archive-condition(V;A;t;f;n;v1;L1)) supposing L1 < L
supposing archive-condition(V;A;t;f;n;v;L) }
{ Proof }
Definitions occuring in Statement :
archive-condition: archive-condition(V;A;t;f;n;v;L),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
nat_plus: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
not: A,
function: x:A B[x],
list: type List,
int: ,
universe: Type,
proper-iseg: L1 < L2
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
not: A,
member: t 
T,
implies: P 
Q,
false: False,
prop: 
,
all: x:A. B[x],
subtype: S 
T
Lemmas :
archive-condition_wf,
nat_plus_inc,
proper-iseg_wf,
consensus-rcv_wf,
nat_plus_wf,
Id_wf,
archive-condition-innings
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[t:\mBbbN{}\msupplus{}]. \mforall{}[f:V List {}\mrightarrow{} V]. \mforall{}[L:consensus-rcv(V;A) List]. \mforall{}[n:\mBbbZ{}]. \mforall{}[v:V].
\mforall{}[L1:consensus-rcv(V;A) List]. \mforall{}[v1:V]. (\mneg{}archive-condition(V;A;t;f;n;v1;L1)) supposing L1 < L
supposing archive-condition(V;A;t;f;n;v;L)
Date html generated:
2011_08_16-AM-10_13_46
Last ObjectModification:
2011_06_18-AM-09_06_17
Home
Index