### 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