Nuprl Lemma : consensus-state4-cases
[V:Type]
A:Id List. s:ConsensusState. a:{a:Id| (a 
A)} . i:
.
(by state s, a passed inning i without archiving a value
in state s, a has not completed inning i
(
v:V. by state s, a archived v in inning i))
Proof not projected
Definitions occuring in Statement :
cs-passed: by state s, a passed inning i without archiving a value,
cs-archived: by state s, a archived v in inning i,
cs-not-completed: in state s, a has not completed inning i,
consensus-state4: ConsensusState,
Id: Id,
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
or: P Q,
set: {x:A| B[x]} ,
list: type List,
int: ,
universe: Type,
l_member: (x l)
Definitions :
prop: 
,
member: t T,
cs-archived: by state s, a archived v in inning i,
cs-not-completed: in state s, a has not completed inning i,
cs-passed: by state s, a passed inning i without archiving a value,
all: x:A. B[x],
uall: [x:A]. B[x],
true: True,
so_lambda: 
x.t[x],
cand: A c
B,
and: P Q,
or: P Q,
exists: x:A. B[x],
consensus-state4: ConsensusState,
guard: {T},
implies: P 
Q,
false: False,
le: A 
B,
not: 
A,
decidable: Dec(P),
uiff: uiff(P;Q),
so_apply: x[s],
uimplies: b supposing a,
rev_implies: P 
Q,
iff: P Q,
fpf-domain: fpf-domain(f)
Lemmas :
consensus-state4_wf,
l_member_wf,
Id_wf,
decidable__equal_int,
decidable__l_member,
subtype-top,
subtype-fpf2,
cs-estimate_wf,
fpf-domain_wf,
not_wf,
cs-inning_wf,
le_wf,
subtype_rel_simple_product,
subtype_rel_self,
fpf_wf,
subtype_rel_function,
top_wf,
member-fpf-dom,
int-deq_wf,
fpf-ap_wf,
decidable__not,
decidable__le,
decidable__cand,
exists_wf,
or_wf,
decidable__lt
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}s:ConsensusState. \mforall{}a:\{a:Id| (a \mmember{} A)\} . \mforall{}i:\mBbbZ{}.
(by state s, a passed inning i without archiving a value
\mvee{} in state s, a has not completed inning i
\mvee{} (\mexists{}v:V. by state s, a archived v in inning i))
Date html generated:
2012_01_23-PM-12_03_36
Last ObjectModification:
2011_12_12-PM-06_56_42
Home
Index