---

y = x after e@a ==
  (b:{a:Id| (a  A)} . (((b = a))  ((y b) = (x b))))
   ((y a) = ((x a) @ [e]))

---

Definitions :  and: P  Q,  all: x:A. B[x],  set: {x:A| B[x]} ,  l_member: (x  l),  implies: P  Q,  not: A,  Id: Id,  equal: s = t,  list: type List,  consensus-event: consensus-event(V;A),  append: as @ bs,  apply: f a,  cons: [car / cdr],  nil: []
FDL editor aliases :  one-consensus-event

---

y  =  x  after  e@a  ==    (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  ((\mneg{}(b  =  a))  {}\mRightarrow{}  ((y  b)  =  (x  b))))  \mwedge{}  ((y  a)  =  ((x  a)  @  [e]))


Date html generated: 2010_08_27-AM-12_55_38
Last ObjectModification: 2009_12_23-PM-03_31_00

Home Index