---

EventsWithValues ==
  E:Type
   eq:EqDecider(E)
   pred?:E  (?E)
   info:E  (Id  Id + (IdLnk  E  Id))
   oaxioms:EOrderAxioms(E;pred?;info)
   T:Id  Id  Type
   when:x:Id  e:E  (T loc(e) x)
   after:x:Id  e:E  (T loc(e) x)
   saxiom:e:E. ((first(e))  (x:Id. ((when x e) = (after x pred(e)))))
   V:Knd  Id  Type
   val:e:E  (V kind(e) loc(e))
   Top

---

Definitions :  deq: EqDecider(T),  unit: Unit,  union: left + right,  IdLnk: IdLnk,  implies: P  Q,  not: A,  assert: b,  all: x:A. B[x],  equal: s = t,  Knd: Knd,  Id: Id,  universe: Type,  product: x:A  B[x],  function: x:A  B[x],  apply: f a,  top: Top
FDL editor aliases :  EVal

---

EventsWithValues  ==
    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{}  when:x:Id  {}\mrightarrow{}  e:E  {}\mrightarrow{}  (T  loc(e)  x)
    \mtimes{}  after:x:Id  {}\mrightarrow{}  e:E  {}\mrightarrow{}  (T  loc(e)  x)
    \mtimes{}  saxiom:\mforall{}e:E.  ((\mneg{}\muparrow{}first(e))  {}\mRightarrow{}  (\mforall{}x:Id.  ((when  x  e)  =  (after  x  pred(e)))))
    \mtimes{}  V:Knd  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type
    \mtimes{}  val:e:E  {}\mrightarrow{}  (V  kind(e)  loc(e))
    \mtimes{}  Top


Date html generated: 2010_08_27-AM-01_08_07
Last ObjectModification: 2009_12_16-AM-12_38_00

Home Index