---

state-machine-spec{i:l}(Info;es;C;R;F;I;O) ==
  X:EClass(C)
   Q:E  E  
    B:retrace(es;Q;X)
     (I:e,e'.(e <loc e') e.I(e)  X:Q
      X:Q e.(F map(e'.X(e');(retracer(B) e) @ [e]))  O:e,e'.
                                                               ((loc(e)
                                                               = loc(e'))
                                                                (e <loc e')))

---

Definitions :  eclass: EClass(A[eo; e]),  function: x:A  B[x],  es-E: E,  prop: ,  exists: x:A. B[x],  retrace: retrace(es;Q;X),  and: P  Q,  Q-R-glued: Ia:Qa f  Ib:Rb,  map: map(f;as),  eclass-val: X(e),  append: as @ bs,  apply: f a,  retracer: retracer(p),  cons: [car / cdr],  nil: [],  lambda: x.A[x],  implies: P  Q,  equal: s = t,  Id: Id,  es-loc: loc(e),  es-locl: (e <loc e')
FDL editor aliases :  state-machine-spec

---

state-machine-spec\{i:l\}(Info;es;C;R;F;I;O)  ==
    \mexists{}X:EClass(C)
      \mexists{}Q:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
        \mexists{}B:retrace(es;Q;X)
          (I:\mlambda{}e,e'.(e  <loc  e')  \mrightarrow{}{}\mlambda{}e.I(e){}\mrightarrow{}    X:Q
          \mwedge{}  X:Q  \mrightarrow{}{}\mlambda{}e.(F  map(\mlambda{}e'.X(e');(retracer(B)  e)  @  [e])){}\mrightarrow{}    O:\mlambda{}e,e'.
                                                                                                                              ((loc(e)  =  loc(e'))  {}\mRightarrow{}  (e  <loc  e')))


Date html generated: 2010_08_27-PM-03_23_18
Last ObjectModification: 2010_04_14-PM-01_31_53

Home Index