---

{ es:EO
    [P:E  ]. [R:E  E  ].
      ((e:E. Dec(P[e]))
       (e,e':E.  Dec(R e' e))
       R => x,y.(x < y)
       Trans(E;x,y.R x y)
       (e,e':E.
            (P[e]  P[e']  (((e R e')  (e = e'))  (e' R e)))) supposing 
            ((m,m':E.
                (P[m]
                 P[m']
                 (m = m') supposing 
                      ((e:E. ((e R m')  (P[e]))) and 
                      (e:E. ((e R m)  (P[e])))))) and 
            (a,b,e:E.
               ((x,y:E.
                   (x c e
                    y c e
                    P[x]
                    P[y]
                    (((x R y)  (x = y))  (y R x))))
                ((R e a)  (R e b))
                ((P[e]  P[a])  P[b])
                (a = b) supposing 
                     ((z:E. (((R e z)  (R z b)  P[z]))) and 
                     (z:E. (((R e z)  (R z a)  P[z])))))))) }

{ Proof }

---

Definitions occuring in Statement :  es-causle: e c e',  es-causl: (e < e'),  es-E: E,  event_ordering: EO,  trans: Trans(T;x,y.E[x; y]),  decidable: Dec(P),  uimplies: b supposing a,  uall: [x:A]. B[x],  prop: ,  infix_ap: x f y,  so_apply: x[s],  all: x:A. B[x],  not: A,  implies: P  Q,  or: P  Q,  and: P  Q,  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  equal: s = t,  rel_implies: R1 => R2
Definitions :  all: x:A. B[x],  uall: [x:A]. B[x],  prop: ,  implies: P  Q,  decidable: Dec(P),  so_apply: x[s],  uimplies: b supposing a,  or: P  Q,  infix_ap: x f y,  and: P  Q,  not: A,  member: t  T,  exists: x:A. B[x],  so_lambda: x.t[x],  cand: A c B,  guard: {T},  false: False,  nat: ,  le: A  B,  ge: i  j ,  so_lambda: x y.t[x; y],  rel_implies: R1 => R2,  strongwellfounded: SWellFounded(R[x; y]),  so_apply: x[s1;s2],  trans: Trans(T;x,y.E[x; y]),  es-r-immediate-pred: es-r-immediate-pred(es;R;e';e),  rel-immediate: R!,  es-causle: e c e'
Lemmas :  not_wf,  es-causle_wf,  decidable__existse-causl,  decidable__and,  es-causl_wf,  es-causl-swellfnd,  nat_properties,  ge_wf,  nat_wf,  le_wf,  trans_wf,  rel_implies_wf,  decidable_wf,  es-E_wf,  event_ordering_wf,  decidable__es-r-immediate-pred,  not-r-immediate-pred,  es-r-immediate-pred_wf

---

\mforall{}es:EO
    \mforall{}[P:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
        ((\mforall{}e:E.  Dec(P[e]))
        {}\mRightarrow{}  (\mforall{}e,e':E.    Dec(R  e'  e))
        {}\mRightarrow{}  R  =>  \mlambda{}x,y.(x  <  y)
        {}\mRightarrow{}  Trans(E;x,y.R  x  y)
        {}\mRightarrow{}  (\mforall{}e,e':E.    (P[e]  {}\mRightarrow{}  P[e']  {}\mRightarrow{}  (((e  R  e')  \mvee{}  (e  =  e'))  \mvee{}  (e'  R  e))))  supposing 
                    ((\mforall{}m,m':E.
                            (P[m]
                            {}\mRightarrow{}  P[m']
                            {}\mRightarrow{}  (m  =  m')  supposing 
                                        ((\mforall{}e:E.  ((e  R  m')  {}\mRightarrow{}  (\mneg{}P[e])))  and 
                                        (\mforall{}e:E.  ((e  R  m)  {}\mRightarrow{}  (\mneg{}P[e]))))))  and 
                    (\mforall{}a,b,e:E.
                          ((\mforall{}x,y:E.    (x  c\mleq{}  e  {}\mRightarrow{}  y  c\mleq{}  e  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  P[y]  {}\mRightarrow{}  (((x  R  y)  \mvee{}  (x  =  y))  \mvee{}  (y  R  x))))
                          {}\mRightarrow{}  ((R  e  a)  \mwedge{}  (R  e  b))
                          {}\mRightarrow{}  ((P[e]  \mwedge{}  P[a])  \mwedge{}  P[b])
                          {}\mRightarrow{}  (a  =  b)  supposing 
                                      ((\mforall{}z:E.  (\mneg{}((R  e  z)  \mwedge{}  (R  z  b)  \mwedge{}  P[z])))  and 
                                      (\mforall{}z:E.  (\mneg{}((R  e  z)  \mwedge{}  (R  z  a)  \mwedge{}  P[z]))))))))


Date html generated: 2011_08_16-AM-11_17_51
Last ObjectModification: 2011_06_20-AM-00_23_04

Home Index