Nuprl Lemma : cut-order_weakening

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


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) uimplies: supposing a uall: [x:A]. B[x] top: Top universe: Type equal: t ∈ T
Lemmas :  cut-of-closed fset-singleton_wf member-fset-singleton es-eq_wf-interface cut-order_witness equal_wf es-E-interface_wf sys-antecedent_wf eclass_wf top_wf es-E_wf event-ordering+_subtype event-ordering+_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  supposing  a  =  b



Date html generated: 2015_07_21-PM-03_59_19
Last ObjectModification: 2015_01_27-PM-05_49_53

Home Index