Nuprl Lemma : cut-order_transitivity

[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:sys-antecedent(es;X)]. ∀[a,b,c:E(X)].
  (a ≤(X;f) c) supposing (b ≤(X;f) and 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) uimplies: supposing a uall: [x:A]. B[x] top: Top universe: Type
Lemmas :  cut-order_witness cut-order_wf es-E-interface_wf sys-antecedent_wf eclass_wf top_wf es-E_wf event-ordering+_subtype event-ordering+_wf cut-subset-cut fset-singleton_wf f-singleton-subset es-eq_wf-interface cut-of_wf es-cut_wf

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



Date html generated: 2015_07_21-PM-04_05_16
Last ObjectModification: 2015_01_27-PM-05_47_09

Home Index