{ 
[V:Type]. [L:ts-reachable(consensus-ts3(V))]. [v:V].
[v':V]. v' = v supposing (CONSIDERING[v'] 
L) 
(COMMITED[v'] L)
supposing (CONSIDERING[v] L) (COMMITED[v] L) }
{ Proof }
Definitions occuring in Statement :
consensus-ts3: consensus-ts3(T),
cs-commited: COMMITED[v],
cs-considering: CONSIDERING[v],
consensus-state3: consensus-state3(T),
uimplies: b supposing a,
uall: [x:A]. B[x],
or: P Q,
universe: Type,
equal: s = t,
l_member: (x l),
ts-reachable: ts-reachable(ts)
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
member: t T,
or: P Q,
prop: 
,
all: x:A. B[x],
consensus-ts3: consensus-ts3(T),
ts-init: ts-init(ts),
so_lambda: 
x.t[x],
pi1: fst(t),
pi2: snd(t),
implies: P 
Q,
infix_ap: x f y,
top: Top,
subtype: S 
T,
guard: {T},
iff: P 
Q,
and: P 
Q,
rev_implies: P Q,
l_member: (x l),
int_seg: {i..j
},
not: 
A,
exists: 
x:A. B[x],
cand: A c B,
le: A 
B,
lelt: i j < k,
false: False,
squash: 
T,
true: True,
nat: 
,
outl: outl(x),
assert: 
b,
isl: isl(x),
btrue: tt,
ifthenelse: if b then t else f fi ,
ts-reachable: ts-reachable(ts),
ts-type: ts-type(ts),
so_apply: x[s],
ts-rel: ts-rel(ts),
decidable: Dec(P),
sq_type: SQType(T),
consensus-state3: consensus-state3(T),
cs-commited: COMMITED[v],
cs-considering: CONSIDERING[v]
Lemmas :
ts-reachable_wf,
consensus-ts3_wf,
ts-type_wf,
l_member_wf,
consensus-state3_wf,
cs-considering_wf,
cs-commited_wf,
ts-reachable-induction,
sq_stable__all,
sq_stable__equal,
ts-rel_wf,
nil_member,
length_wf_nat,
top_wf,
nat_wf,
member_wf,
cs-initial_wf,
consensus-state3-unequal,
iff_transitivity,
member_append,
or_functionality_wrt_iff,
member_singleton,
consensus-ts3-invariant0,
le_wf,
select_wf,
squash_wf,
length_wf1,
int_seg_wf,
decidable__equal_int,
iff_weakening_uiff,
cs-considering-equal,
decidable__lt,
int_seg_properties,
cs-commited-equal,
subtype_base_sq,
int_subtype_base,
true_wf,
bool_wf,
outl_wf,
assert_wf,
isl_wf
\mforall{}[V:Type]. \mforall{}[L:ts-reachable(consensus-ts3(V))]. \mforall{}[v:V].
\mforall{}[v':V]. v' = v supposing (CONSIDERING[v'] \mmember{} L) \mvee{} (COMMITED[v'] \mmember{} L)
supposing (CONSIDERING[v] \mmember{} L) \mvee{} (COMMITED[v] \mmember{} L)
Date html generated:
2011_08_16-AM-09_56_35
Last ObjectModification:
2011_06_18-AM-08_56_11
Home
Index