{ 
[V:Type]
L:ts-reachable(consensus-ts3(V)). i:
||L||.
j:||L||. (L[j] = INITIAL) 
(L[j] = WITHDRAWN) supposing i < j
supposing L[i] = INITIAL }
{ Proof }
Definitions occuring in Statement :
consensus-ts3: consensus-ts3(T),
cs-withdrawn: WITHDRAWN,
cs-initial: INITIAL,
consensus-state3: consensus-state3(T),
select: l[i],
length: ||as||,
int_seg: {i..j
},
uimplies: b supposing a,
uall: [x:A]. B[x],
all: x:A. B[x],
or: P Q,
less_than: a < b,
natural_number: $n,
universe: Type,
equal: s = t,
ts-reachable: ts-reachable(ts)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
consensus-ts3: consensus-ts3(T),
int_seg: {i..j},
uimplies: b supposing a,
or: P Q,
and: P 
Q,
not: 
A,
member: t 
T,
prop: 
,
implies: P 
Q,
ts-init: ts-init(ts),
guard: {T},
so_lambda: 
x.t[x],
pi1: fst(t),
pi2: snd(t),
lelt: i 
j < k,
le: A B,
false: False,
top: Top,
subtype: S 
T,
infix_ap: x f y,
squash: 
T,
true: True,
length: ||as||,
rev_implies: P 
Q,
iff: P Q,
ycomb: Y,
select: l[i],
ifthenelse: if b then t else f fi ,
le_int: i z j,
bnot: 
b,
lt_int: i <z j,
bfalse: ff,
btrue: tt,
ts-reachable: ts-reachable(ts),
so_apply: x[s],
ts-rel: ts-rel(ts),
exists: 
x:A. B[x],
nat: ,
ts-type: ts-type(ts),
decidable: Dec(P),
sq_type: SQType(T)
Lemmas :
consensus-state3-unequal,
ts-reachable-induction,
consensus-ts3_wf,
consensus-state3_wf,
select_wf,
length_wf2,
cs-withdrawn_wf,
int_seg_wf,
length_wf_nat,
top_wf,
nat_wf,
cs-initial_wf,
decidable__equal_cs-initial,
length_wf1,
le_wf,
ts-reachable_wf,
ts-type_wf,
sq_stable__all,
sq_stable__uall,
sq_stable_from_decidable,
decidable__or,
decidable__equal_cs-withdrawn,
ts-rel_wf,
squash_wf,
not_wf,
member_wf,
append_wf,
decidable__equal_int,
select_append_back,
subtype_base_sq,
int_subtype_base,
length_append,
select_append_front,
true_wf
\mforall{}[V:Type]
\mforall{}L:ts-reachable(consensus-ts3(V)). \mforall{}i:\mBbbN{}||L||.
\mforall{}j:\mBbbN{}||L||. (L[j] = INITIAL) \mvee{} (L[j] = WITHDRAWN) supposing i < j supposing L[i] = INITIAL
Date html generated:
2011_08_16-AM-09_56_24
Last ObjectModification:
2011_06_18-AM-08_56_07
Home
Index