### Nuprl Lemma : consensus-ts4-inning-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.Inning(x;a) ≤ Inning(y;a))`

Proof

Definitions occuring in Statement :  consensus-ts4: `consensus-ts4(V;A;W)` cs-inning: `Inning(s;a)` Id: `Id` l_member: `(x ∈ l)` list: `T List` uall: `∀[x:A]. B[x]` le: `A ≤ B` set: `{x:A| B[x]} ` universe: `Type` ts-stable-rel: `ts-stable-rel(ts;x,y.R[x; y])`
Lemmas :  less_than_wf cs-inning_wf infix_ap_wf ts-type_wf consensus-ts4_wf rel_star_wf ts-rel_wf set_wf l_member_wf list_wf Id_wf ts-transitive-stable le_wf le_weakening consensus-state4_wf le_transitivity consensus-rel_wf decidable__equal_Id atom2_subtype_base subtype_base_sq
\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.Inning(x;a)  \mleq{}  Inning(y;a))

Date html generated: 2015_07_17-AM-11_26_38
Last ObjectModification: 2015_07_16-AM-09_51_10

Home Index