---

{ [Info,A,T:Type].
    [es:EO+(Info)]. [X:EClass(T  A)]. [e:E].
      MaxFst(X)(e) ~ accum_list(p1,e.if fst(p1) <z fst(X(e))
      then X(e)
      else p1
      fi ;e.X(e);(X)(e)) 
      supposing e  MaxFst(X) 
    supposing T r  }

{ Proof }

---

Definitions occuring in Statement :  max-fst-class: MaxFst(X),  es-interface-predecessors: (X)(e),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  subtype_rel: A r B,  lt_int: i <z j,  assert: b,  ifthenelse: if b then t else f fi ,  uimplies: b supposing a,  uall: [x:A]. B[x],  pi1: fst(t),  product: x:A  B[x],  int: ,  universe: Type,  sqequal: s ~ t,  accum_list: accum_list(a,x.f[a; x];x.base[x];L)
Definitions :  max-fst-class: MaxFst(X),  member: t  T,  so_lambda: x.t[x],  top: Top,  all: x:A. B[x],  subtype: S  T,  so_lambda: x y.t[x; y],  uall: [x:A]. B[x],  uimplies: b supposing a,  so_apply: x[s],  so_apply: x[s1;s2]
Lemmas :  max-f-class-val,  pi1_wf_top,  assert_wf,  in-eclass_wf,  max-fst-class_wf,  es-interface-subtype_rel2,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  top_wf,  eclass_wf

---

\mforall{}[Info,A,T:Type].
    \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(T  \mtimes{}  A)].  \mforall{}[e:E].
        MaxFst(X)(e)  \msim{}  accum\_list(p1,e.if  fst(p1)  <z  fst(X(e))  then  X(e)  else  p1  fi  ;e.X(e);\mleq{}(X)(e)) 
        supposing  \muparrow{}e  \mmember{}\msubb{}  MaxFst(X) 
    supposing  T  \msubseteq{}r  \mBbbZ{}


Date html generated: 2011_08_16-PM-04_37_46
Last ObjectModification: 2011_06_20-AM-01_00_19

Home Index