Nuprl Lemma : consensus-ts4-estimate-rel
∀[V:Type]. ∀[A:Id List]. ∀[W:{a:Id| (a ∈ A)} List List]. ∀[a:{a:Id| (a ∈ A)} ].
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,
int-deq: IntDeq,
l_member: (x ∈ l),
list: T List,
uall: ∀[x:A]. B[x],
set: {x:A| B[x]} ,
int: ℤ,
universe: Type,
ts-stable-rel: ts-stable-rel(ts;x,y.R[x; y])
Lemmas :
cs-estimate_wf,
int-deq_wf,
fpf-sub_transitivity,
decidable__equal_Id,
atom2_subtype_base,
Id_wf,
subtype_base_sq,
fpf-sub_weakening,
fpf-sub_wf,
fpf-sub-reflexive,
fpf-single_wf,
fpf-sub-join-left2
\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:
2015_07_17-AM-11_26_44
Last ObjectModification:
2015_07_16-AM-09_51_06
Home
Index