Nuprl Lemma : cut-order_witness

[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:sys-antecedent(es;X)]. ∀[a,b:E(X)].
  (a ≤(X;f)  (Ax ∈ a ≤(X;f) b))


Proof




Definitions occuring in Statement :  cut-order: a ≤(X;f) b sys-antecedent: sys-antecedent(es;Sys) es-E-interface: E(X) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) uall: [x:A]. B[x] top: Top implies:  Q member: t ∈ T universe: Type axiom: Ax
Lemmas :  fset-member_wf-cut cut-of_wf fset-singleton_wf es-E-interface_wf sys-antecedent_wf eclass_wf top_wf es-E_wf event-ordering+_subtype event-ordering+_wf fset-member_witness es-eq_wf-interface es-cut_wf

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:sys-antecedent(es;X)].  \mforall{}[a,b:E(X)].
    (a  \mleq{}(X;f)  b  {}\mRightarrow{}  (Ax  \mmember{}  a  \mleq{}(X;f)  b))



Date html generated: 2015_07_21-PM-03_58_58
Last ObjectModification: 2015_01_27-PM-05_51_15

Home Index