Nuprl Lemma : max-f-class-val

[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[f:A ─→ ℤ]. ∀[X:EClass(A)]. ∀[e:E].
  (v from with maximum f[v])(e) accum_list(v,e.if f[v] <f[X(e)] then X(e) else fi ;e.X(e);≤(X)(e)) 
  supposing ↑e ∈b (v from with maximum f[v])


Definitions occuring in Statement :  max-f-class: (v from with maximum f[v]) es-interface-predecessors: (X)(e) eclass-val: X(e) in-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E accum_list: accum_list(a,x.f[a; x];x.base[x];L) assert: b ifthenelse: if then else fi  lt_int: i <j uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] function: x:A ─→ B[x] int: universe: Type sqequal: t
Lemmas :  accum-class-val max-f-class_wf assert_wf in-eclass_wf es-interface-subtype_rel2 es-E_wf event-ordering+_subtype eclass_wf event-ordering+_wf

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].
    (v  from  X  with  maximum  f[v])(e)  \msim{}  accum\_list(v,e.if  f[v]  <z  f[X(e)]
    then  X(e)
    else  v
    fi  ;e.X(e);\mleq{}(X)(e)) 
    supposing  \muparrow{}e  \mmember{}\msubb{}  (v  from  X  with  maximum  f[v])

Date html generated: 2015_07_20-PM-03_50_05
Last ObjectModification: 2015_01_27-PM-10_06_04

Home Index