Nuprl Lemma : es-propagation-rule_wf

[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[f:Id ─→ A ─→ B]. ∀[g:A ─→ (Id List)]. ∀[es:EO+(Info)].
  (X =f Y@g ∈ ℙ)


Proof




Definitions occuring in Statement :  es-propagation-rule: =f B@g eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) Id: Id list: List uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  exists_wf es-E-interface_wf es-interface-subtype_rel2 es-E_wf event-ordering+_subtype top_wf list_wf all_wf not_wf equal_wf l_disjoint_wf l_all_wf2 l_member_wf es-causl_wf eclass-val_wf assert_elim in-eclass_wf subtype_base_sq bool_wf bool_subtype_base es-loc_wf l_exists_wf event-ordering+_wf Id_wf eclass_wf

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B].  \mforall{}[g:A  {}\mrightarrow{}  (Id  List)].
\mforall{}[es:EO+(Info)].
    (X  {}f\mRightarrow{}  Y@g  \mmember{}  \mBbbP{})



Date html generated: 2015_07_21-PM-03_29_17
Last ObjectModification: 2015_01_27-PM-06_41_34

Home Index