---

single-thread-generator{i:l}(es;P;R) ==
  (e:E. Dec(P[e]))
   (e,e':E.  Dec(R e' e))
   R => x,y.(x < y)
   (e,e':E.  ((P[e]  (R e' e))  P[e']))
   (m,m':E.
       (P[m]
        P[m']
        (e:E. ((e R m)  (P[e])))
        (e:E. ((e R m')  (P[e])))
        (m = m')))
   (a,b,e:E.  (((R e a)  (R e b))  ((P[e]  P[a])  P[b])  (a = b)))

---

Definitions :  decidable: Dec(P),  rel_implies: R1 => R2,  lambda: x.A[x],  es-causl: (e < e'),  infix_ap: x f y,  not: A,  all: x:A. B[x],  apply: f a,  implies: P  Q,  and: P  Q,  so_apply: x[s],  equal: s = t,  es-E: E
FDL editor aliases :  single-thread-generator

---

single-thread-generator\{i:l\}(es;P;R)  ==
    (\mforall{}e:E.  Dec(P[e]))
    \mwedge{}  (\mforall{}e,e':E.    Dec(R  e'  e))
    \mwedge{}  R  =>  \mlambda{}x,y.(x  <  y)
    \mwedge{}  (\mforall{}e,e':E.    ((P[e]  \mwedge{}  (R  e'  e))  {}\mRightarrow{}  P[e']))
    \mwedge{}  (\mforall{}m,m':E.
              (P[m]  {}\mRightarrow{}  P[m']  {}\mRightarrow{}  (\mforall{}e:E.  ((e  R  m)  {}\mRightarrow{}  (\mneg{}P[e])))  {}\mRightarrow{}  (\mforall{}e:E.  ((e  R  m')  {}\mRightarrow{}  (\mneg{}P[e])))  {}\mRightarrow{}  (m  =  m')))
    \mwedge{}  (\mforall{}a,b,e:E.    (((R  e  a)  \mwedge{}  (R  e  b))  {}\mRightarrow{}  ((P[e]  \mwedge{}  P[a])  \mwedge{}  P[b])  {}\mRightarrow{}  (a  =  b)))


Date html generated: 2010_08_27-AM-09_46_50
Last ObjectModification: 2009_12_17-PM-10_57_06

Home Index