---

EventsWithState ==
  E:Type
   eq:EqDecider(E)
   pred?:E  (?E)
   info:E  (Id  Id + (IdLnk  E  Id))
   oaxioms:EOrderAxioms(E;pred?;info)
   T:Id  Id  Type
   V:Id  Id  Type
   M:IdLnk  Id  Type
   init:i:Id  EState(T i)
   Trans:i:Id
           k:Knd
           kindcase(k;a.V i a;l,t.M l t)
           EState(T i)
           EState(T i)
   val:e:E  kindcase(kind(e);a.V loc(e) a;l,t.M l t)
   Send:i:Id
          k:Knd
          kindcase(k;a.V i a;l,t.M l t)
          x:Id  (T i x)
          (Msg(M) List)
   Choose:i:Id  a:Id    x:Id  (T i x)  (?V i a)
   time:E  
   va:val-axiom(E;V;M;info;pred?;
       init;Trans;
       Choose;Send;val;time)
   Top

---

Definitions :  deq: EqDecider(T),  IdLnk: IdLnk,  universe: Type,  Knd: Knd,  kindcase: kindcase(k;a.f[a];l,t.g[l; t]),  list: type List,  Msg: Msg(M),  nat: ,  Id: Id,  union: left + right,  apply: f a,  unit: Unit,  function: x:A  B[x],  rationals: ,  product: x:A  B[x],  top: Top
FDL editor aliases :  EState

---

EventsWithState  ==
    E:Type
    \mtimes{}  eq:EqDecider(E)
    \mtimes{}  pred?:E  {}\mrightarrow{}  (?E)
    \mtimes{}  info:E  {}\mrightarrow{}  (Id  \mtimes{}  Id  +  (IdLnk  \mtimes{}  E  \mtimes{}  Id))
    \mtimes{}  oaxioms:EOrderAxioms(E;pred?;info)
    \mtimes{}  T:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type
    \mtimes{}  V:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type
    \mtimes{}  M:IdLnk  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type
    \mtimes{}  init:i:Id  {}\mrightarrow{}  EState(T  i)
    \mtimes{}  Trans:i:Id  {}\mrightarrow{}  k:Knd  {}\mrightarrow{}  kindcase(k;a.V  i  a;l,t.M  l  t)  {}\mrightarrow{}  EState(T  i)  {}\mrightarrow{}  EState(T  i)
    \mtimes{}  val:e:E  {}\mrightarrow{}  kindcase(kind(e);a.V  loc(e)  a;l,t.M  l  t)
    \mtimes{}  Send:i:Id  {}\mrightarrow{}  k:Knd  {}\mrightarrow{}  kindcase(k;a.V  i  a;l,t.M  l  t)  {}\mrightarrow{}  x:Id  {}\mrightarrow{}  (T  i  x)  {}\mrightarrow{}  (Msg(M)  List)
    \mtimes{}  Choose:i:Id  {}\mrightarrow{}  a:Id  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  x:Id  {}\mrightarrow{}  (T  i  x)  {}\mrightarrow{}  (?V  i  a)
    \mtimes{}  time:E  {}\mrightarrow{}  \mBbbQ{}
    \mtimes{}  va:val-axiom(E;V;M;info;pred?;
              init;Trans;
              Choose;Send;val;time)
    \mtimes{}  Top


Date html generated: 2010_08_27-AM-01_08_03
Last ObjectModification: 2009_12_16-AM-12_36_02

Home Index