---

{ [Info,T:Type]. [f:T  ]. [es:EO+(Info)]. [lb:]. [X:EClass(T)].
  [e:E(X)]. [n:].
    uiff((maximum f[v]  lb with v from X)(e)  n;([e':E(X)]
                                                     f[X(e')]  n 
                                                     supposing e' loc e )
     (lb  n)) }

{ Proof }

---

Definitions occuring in Statement :  imax-class: (maximum f[v]  lb with v from X),  es-E-interface: E(X),  eclass-val: X(e),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-le: e loc e' ,  uiff: uiff(P;Q),  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  le: A  B,  and: P  Q,  function: x:A  B[x],  int: ,  universe: Type
Definitions :  so_lambda: x.t[x],  member: t  T,  prop: ,  and: P  Q,  iff: P  Q,  rev_implies: P  Q,  so_apply: x[s],  implies: P  Q,  all: x:A. B[x],  es-E-interface: E(X),  subtype: S  T
Lemmas :  es-interface-predecessors_wf,  event-ordering+_inc,  es-loc_wf,  Id_wf,  es-E-interface_wf,  l_member-settype

---

\mforall{}[Info,T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[es:EO+(Info)].  \mforall{}[lb:\mBbbZ{}].  \mforall{}[X:EClass(T)].  \mforall{}[e:E(X)].  \mforall{}[n:\mBbbZ{}].
    uiff((maximum  f[v]  \mgeq{}  lb  with  v  from  X)(e)  \mleq{}  n;(\mforall{}[e':E(X)].  f[X(e')]  \mleq{}  n  supposing  e'  \mleq{}loc  e  )
    \mwedge{}  (lb  \mleq{}  n))


Date html generated: 2011_08_16-PM-05_19_59
Last ObjectModification: 2011_06_20-AM-01_21_12

Home Index