Nuprl Lemma : consensus-event-constraint_wf

[V:Type]. ∀[A:Id List]. ∀[a:{a:Id| (a ∈ A)} ]. ∀[W:{a:Id| (a ∈ A)}  List List]. ∀[e:consensus-event(V;A)].
[x:consensus-state6(V;A)].
  (e@a allowed in state x ∈ ℙ)


Proof




Definitions occuring in Statement :  consensus-event-constraint: e@a allowed in state x consensus-state6: consensus-state6(V;A) consensus-event: consensus-event(V;A) Id: Id l_member: (x ∈ l) list: List uall: [x:A]. B[x] prop: member: t ∈ T set: {x:A| B[x]}  universe: Type
Lemmas :  all_wf archive-event_wf consensus-accum-state_wf fpf_wf top_wf not_wf l_member_wf fpf-domain_wf subtype-fpf2 cs-knowledge-precondition_wf nat_wf int_seg_wf unit_wf2 consensus-message_wf int_seg_properties le_wf assert_wf fpf-dom_wf int-deq_wf less_than_wf fpf-ap_wf consensus-state6_wf consensus-event_wf list_wf Id_wf set_wf
\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[a:\{a:Id|  (a  \mmember{}  A)\}  ].  \mforall{}[W:\{a:Id|  (a  \mmember{}  A)\}    List  List].
\mforall{}[e:consensus-event(V;A)].  \mforall{}[x:consensus-state6(V;A)].
    (e@a  allowed  in  state  x  \mmember{}  \mBbbP{})



Date html generated: 2015_07_17-AM-11_45_24
Last ObjectModification: 2015_01_28-AM-01_31_50

Home Index