{ 
[V:Type]
((
(INITIAL = WITHDRAWN))
([v:V]
((((COMMITED[v] = INITIAL)) ((CONSIDERING[v] = INITIAL)))
((COMMITED[v] = WITHDRAWN))
((CONSIDERING[v] = WITHDRAWN))
([v':V]
(((CONSIDERING[v] = COMMITED[v']))
((CONSIDERING[v] = CONSIDERING[v']))
((COMMITED[v] = COMMITED[v']))
supposing (v = v')))))) }
{ Proof }
Definitions occuring in Statement :
cs-commited: COMMITED[v],
cs-considering: CONSIDERING[v],
cs-withdrawn: WITHDRAWN,
cs-initial: INITIAL,
consensus-state3: consensus-state3(T),
uimplies: b supposing a,
uall: [x:A]. B[x],
not: A,
and: P Q,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
and: P Q,
not: A,
uimplies: b supposing a,
member: t 
T,
implies: P 
Q,
false: False,
bfalse: ff,
btrue: tt,
outr: outr(x),
prop: 
,
assert: 
b,
bnot: 
b,
isl: isl(x),
ifthenelse: if b then t else f fi ,
true: True,
outl: outl(x),
consensus-state3: consensus-state3(T),
cs-initial: INITIAL,
cs-withdrawn: WITHDRAWN,
cs-commited: COMMITED[v],
cs-considering: CONSIDERING[v],
bool: 
Lemmas :
bool_wf,
btrue_wf,
outr_wf,
assert_wf,
bnot_wf,
isl_wf,
consensus-state3_wf,
cs-initial_wf,
cs-withdrawn_wf,
cs-commited_wf,
bfalse_wf,
cs-considering_wf,
outl_wf,
not_wf
\mforall{}[V:Type]
((\mneg{}(INITIAL = WITHDRAWN))
\mwedge{} (\mforall{}[v:V]
(((\mneg{}(COMMITED[v] = INITIAL)) \mwedge{} (\mneg{}(CONSIDERING[v] = INITIAL)))
\mwedge{} (\mneg{}(COMMITED[v] = WITHDRAWN))
\mwedge{} (\mneg{}(CONSIDERING[v] = WITHDRAWN))
\mwedge{} (\mforall{}[v':V]
((\mneg{}(CONSIDERING[v] = COMMITED[v']))
\mwedge{} (\mneg{}(CONSIDERING[v] = CONSIDERING[v'])) \mwedge{} (\mneg{}(COMMITED[v] = COMMITED[v']))
supposing \mneg{}(v = v'))))))
Date html generated:
2011_08_16-AM-09_56_07
Last ObjectModification:
2011_06_18-AM-08_55_55
Home
Index