{ 
[V:Type]
x:consensus-state2(V)
((x = AMBIVALENT) 
(
v:V. ((x = PREDECIDED[v]) (x = Decided[v])))) }
{ Proof }
Definitions occuring in Statement :
cs-predecided: PREDECIDED[v],
cs-ambivalent: AMBIVALENT,
consensus-state2: consensus-state2(T),
cs-decided: Decided[v],
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
or: P Q,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
or: P Q,
exists: x:A. B[x],
guard: {T},
member: t 
T,
prop: 
,
top: Top,
consensus-state2: consensus-state2(T),
cs-ambivalent: AMBIVALENT,
cs-predecided: PREDECIDED[v],
cs-decided: Decided[v]
Lemmas :
cs-decided_wf2,
consensus-state2_wf,
cs-predecided_wf,
cs-ambivalent_wf,
equal-top
\mforall{}[V:Type]
\mforall{}x:consensus-state2(V). ((x = AMBIVALENT) \mvee{} (\mexists{}v:V. ((x = PREDECIDED[v]) \mvee{} (x = Decided[v]))))
Date html generated:
2011_08_16-AM-09_54_43
Last ObjectModification:
2011_06_18-AM-08_54_36
Home
Index