Nuprl Lemma : es-class-causal-rel-fail_wf

[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:Id List]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[R:E(X) ─→ A ─→ B ─→ ℙ].
  (∀e,x,y. e∈X(x) c ∃ Y(y) such that
                       R[e;x;y]
                      unless loc(e) ∈ f ∈ ℙ)


Proof




Definitions occuring in Statement :  es-class-causal-rel-fail: es-class-causal-rel-fail es-E-interface: E(X) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) Id: Id list: List uall: [x:A]. B[x] prop: so_apply: x[s1;s2;s3] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  all_wf es-E-interface_wf es-interface-subtype_rel2 es-E_wf event-ordering+_subtype top_wf exists_wf es-causle_wf eclass-val_wf assert_elim in-eclass_wf subtype_base_sq bool_wf bool_subtype_base or_wf l_member_wf es-loc_wf event-ordering+_wf eclass_wf list_wf Id_wf

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[f:Id  List].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[R:E(X)
                                                                                                                                                                          {}\mrightarrow{}  A
                                                                                                                                                                          {}\mrightarrow{}  B
                                                                                                                                                                          {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}e,x,y.  e\mmember{}X(x)  \mLeftarrow{}c\mRightarrow{}  \mexists{}  Y(y)  such  that
                                              R[e;x;y]
                                            unless  loc(e)  \mmember{}  f  \mmember{}  \mBbbP{})



Date html generated: 2015_07_21-PM-04_25_39
Last ObjectModification: 2015_01_27-PM-05_15_28

Home Index