---

retrace(es;Q;X) ==
  (e,e':E.  ((Q e e')  ((e  X)  (e'  X))))
   (e,e':E(X).  ((Q e e')  (e = e')  (Q e' e)))
   (e':E
       L:E List
        ((e:E. ((e  L)  Q e e'))
         (e1,e2:E.  (e1 before e2  L  (Q e1 e2)))))

---

Definitions :  assert: b,  in-eclass: e  X,  es-E-interface: E(X),  or: P  Q,  equal: s = t,  exists: x:A. B[x],  list: type List,  and: P  Q,  iff: P  Q,  l_member: (x  l),  all: x:A. B[x],  implies: P  Q,  l_before: x before y  l,  es-E: E,  apply: f a
FDL editor aliases :  retrace

---

retrace(es;Q;X)  ==
    (\mforall{}e,e':E.    ((Q  e  e')  {}\mRightarrow{}  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\muparrow{}e'  \mmember{}\msubb{}  X))))
    \mwedge{}  (\mforall{}e,e':E(X).    ((Q  e  e')  \mvee{}  (e  =  e')  \mvee{}  (Q  e'  e)))
    \mwedge{}  (\mforall{}e':E
              \mexists{}L:E  List.  ((\mforall{}e:E.  ((e  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  Q  e  e'))  \mwedge{}  (\mforall{}e1,e2:E.    (e1  before  e2  \mmember{}  L  {}\mRightarrow{}  (Q  e1  e2)))))


Date html generated: 2010_08_27-PM-03_23_02
Last ObjectModification: 2010_04_14-PM-01_23_52

Home Index