---

[e1;e2]~([a,b].p[a; b])*[a,b].q[a; b] ==
  m:
   f:m  {e:E| loc(e) = loc(e1)} 
    ((((f 0) = e1)  f (m - 1) loc e2 )
     ((i:m - 1. (f i <loc f (i + 1)))  (i:m - 1. p[f i; pred(f (i + 1))]))
     q[f (m - 1); e2])

---

Definitions :  nat_plus: ,  exists: x:A. B[x],  function: x:A  B[x],  set: {x:A| B[x]} ,  Id: Id,  es-loc: loc(e),  equal: s = t,  es-E: E,  es-le: e loc e' ,  and: P  Q,  es-locl: (e <loc e'),  all: x:A. B[x],  int_seg: {i..j},  es-pred: pred(e),  add: n + m,  apply: f a,  subtract: n - m,  natural_number: $n
FDL editor aliases :  es-pstar-q

---

[e1;e2]\msim{}([a,b].p[a;  b])*[a,b].q[a;  b]  ==
    \mexists{}m:\mBbbN{}\msupplus{}
      \mexists{}f:\mBbbN{}m  {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\} 
        ((((f  0)  =  e1)  \mwedge{}  f  (m  -  1)  \mleq{}loc  e2  )
        \mwedge{}  ((\mforall{}i:\mBbbN{}m  -  1.  (f  i  <loc  f  (i  +  1)))  \mwedge{}  (\mforall{}i:\mBbbN{}m  -  1.  p[f  i;  pred(f  (i  +  1))]))
        \mwedge{}  q[f  (m  -  1);  e2])


Date html generated: 2010_08_27-AM-09_32_56
Last ObjectModification: 2009_12_16-AM-01_12_25

Home Index