Nuprl Lemma : consensus-ts4-passed-stable
[V:Type]. [A:Id List]. [W:{a:Id| (a 
A)} List List]. [a:{a:Id| (a A)} ]. [i:
].
ts-stable(consensus-ts4(V;A;W);s.by state s, a passed inning i without archiving a value)
Proof not projected
Definitions occuring in Statement :
cs-passed: by state s, a passed inning i without archiving a value,
consensus-ts4: consensus-ts4(V;A;W),
Id: Id,
uall: [x:A]. B[x],
set: {x:A| B[x]} ,
list: type List,
int: ,
universe: Type,
l_member: (x l),
ts-stable: ts-stable(ts;x.P[x])
Definitions :
so_lambda: 
x.t[x],
consensus-state4: ConsensusState,
prop: 
,
false: False,
not: 
A,
and: P 
Q,
infix_ap: x f y,
implies: P 
Q,
all: x:A. B[x],
member: t T,
cs-passed: by state s, a passed inning i without archiving a value,
ts-stable: ts-stable(ts;x.P[x]),
uall: [x:A]. B[x],
pi2: snd(t),
pi1: fst(t),
ts-rel: ts-rel(ts),
ts-type: ts-type(ts),
consensus-ts4: consensus-ts4(V;A;W),
true: True,
squash: 
T,
cand: A c B,
Id: Id,
top: Top,
or: P 
Q,
so_apply: x[s],
uimplies: b supposing a,
exists: 
x:A. B[x],
consensus-rel: CR[x,y],
decidable: Dec(P),
guard: {T},
sq_type: SQType(T),
uiff: uiff(P;Q),
iff: P 
Q,
rev_implies: P Q,
fpf-single: x : v,
fpf-domain: fpf-domain(f)
Lemmas :
ts-type_wf,
cs-passed_wf,
consensus-ts4_wf,
ts-rel_wf,
subtype_top,
strong-subtype-self,
subtype-fpf3,
subtype_rel_simple_product,
subtype_rel_self,
fpf_wf,
Id_wf,
subtype_rel_dep_function,
top_wf,
cs-estimate_wf,
fpf-domain_wf,
l_member_wf,
consensus-state4_wf,
consensus-rel_wf,
decidable__equal_Id,
equal_wf,
member_wf,
fpf-trivial-subtype-top,
not_wf,
cs-inning_wf,
less_than_wf,
and_wf,
atom2_subtype_base,
subtype_base_sq,
member_singleton,
int-deq_wf,
fpf-domain-join,
fpf-single_wf,
or_wf,
subtype-top,
subtype-fpf2,
not_functionality_wrt_iff
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[W:\{a:Id| (a \mmember{} A)\} List List]. \mforall{}[a:\{a:Id| (a \mmember{} A)\} ]. \mforall{}[i:\mBbbZ{}].
ts-stable(consensus-ts4(V;A;W);s.by state s, a passed inning i without archiving a value)
Date html generated:
2012_01_23-PM-12_03_44
Last ObjectModification:
2011_12_12-PM-06_56_34
Home
Index