{ 
[V:Type]. [A:Id List]. [W:{a:Id| (a 
A)} List List]. [a:{a:Id| (a A)} \000C].
ts-stable-rel(consensus-ts4(V;A;W);x,y.Estimate(x;a) 
Estimate(y;a)) }
{ Proof }
Definitions occuring in Statement :
consensus-ts4: consensus-ts4(V;A;W),
cs-estimate: Estimate(s;a),
fpf-sub: f g,
Id: Id,
uall: [x:A]. B[x],
set: {x:A| B[x]} ,
list: type List,
int: 
,
universe: Type,
l_member: (x l),
int-deq: IntDeq,
ts-stable-rel: ts-stable-rel(ts;x,y.R[x; y])
Definitions :
transition-system: transition-system{i:l},
tag-by: z
T,
rev_implies: P 
Q,
or: P 
Q,
iff: P 
Q,
record+: record+,
record: record(x.T[x]),
fset: FSet{T},
isect2: T1 
T2,
b-union: A 
B,
union: left + right,
top: Top,
fpf-cap: f(x)?z,
fpf: a:A fp-> B[a],
deq: EqDecider(T),
spread: spread def,
pi1: fst(t),
cs-estimate: Estimate(s;a),
int-deq: IntDeq,
fpf-empty: 
,
consensus-state4: ConsensusState,
pair: <a, b>,
strong-subtype: strong-subtype(A;B),
exists: 
x:A. B[x],
le: A 
B,
ge: i 
j ,
not: 
A,
less_than: a < b,
uimplies: b supposing a,
and: P 
Q,
uiff: uiff(P;Q),
subtype_rel: A r B,
so_lambda: 
x y.t[x; y],
int: ,
so_lambda: x.t[x],
ts-rel: ts-rel(ts),
rel_star: R^*,
apply: f a,
infix_ap: x f y,
consensus-ts4: consensus-ts4(V;A;W),
ts-type: ts-type(ts),
lambda: x.A[x],
void: Void,
false: False,
true: True,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
assert: 
b,
product: x:A B[x],
cand: A c B,
fpf-sub: f g,
implies: P Q,
ts-stable-rel: ts-stable-rel(ts;x,y.R[x; y]),
prop: 
,
isect: x:A. B[x],
all: x:A. B[x],
function: x:A 
B[x],
uall: [x:A]. B[x],
set: {x:A| B[x]} ,
l_member: (x l),
Id: Id,
list: type List,
universe: Type,
member: t T,
equal: s = t,
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic,
cs-precondition: state s may consider v in inning i,
consensus-rel: CR[x,y],
rel_implies: R1 => R2,
fpf-join: f 
g,
trans: Trans(T;x,y.E[x; y]),
refl: Refl(T;x,y.E[x; y]),
IdLnk: IdLnk,
Knd: Knd,
MaName: MaName,
l_disjoint: l_disjoint(T;l1;l2),
consensus-state3: consensus-state3(T),
decidable: Dec(P),
add: n + m,
cs-inning: Inning(s;a),
guard: {T},
atom: Atom,
atom: Atom$n,
sq_type: SQType(T),
natural_number: $n,
fpf-domain: fpf-domain(f),
fpf-single: x : v,
bool: 
Lemmas :
product_subtype_base,
list_subtype_base,
int_subtype_base,
fpf-sub-join-left2,
fpf-single_wf,
cs-inning_wf,
subtype_base_sq,
atom2_subtype_base,
decidable__equal_Id,
fpf-sub_transitivity,
ts-transitive-stable,
refl_wf,
assert_wf,
fpf-sub_weakening,
trans_wf,
rel_implies_wf,
consensus-rel_wf,
ts-rel_wf,
consensus-ts4_wf,
fpf-sub_wf,
ts-type_wf,
rel_star_wf,
ts-stable-rel_wf,
fpf-sub_witness,
Id_wf,
l_member_wf,
consensus-state4_wf,
int-deq_wf,
cs-estimate_wf,
member_wf,
subtype_rel_wf,
fpf_wf
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[W:\{a:Id| (a \mmember{} A)\} List List]. \mforall{}[a:\{a:Id| (a \mmember{} A)\} ].
ts-stable-rel(consensus-ts4(V;A;W);x,y.Estimate(x;a) \msubseteq{} Estimate(y;a))
Date html generated:
2011_08_16-AM-09_58_22
Last ObjectModification:
2011_06_18-AM-08_57_08
Home
Index