---

Decide values come from Input values ==
  d:E(Decide). e:E(Input). (e c d  (Decide(d) = Input(e)))

---

Definitions :  all: x:A. B[x],  exists: x:A. B[x],  es-E-interface: E(X),  and: P  Q,  es-causle: e c e',  equal: s = t,  eclass-val: X(e)
FDL editor aliases :  consensus-spec2

---

Decide  values  come  from  Input  values  ==
    \mforall{}d:E(Decide).  \mexists{}e:E(Input).  (e  c\mleq{}  d  \mwedge{}  (Decide(d)  =  Input(e)))


Date html generated: 2010_08_28-AM-11_51_59
Last ObjectModification: 2010_04_16-AM-12_59_41

Home Index