Nuprl Definition : deliver-messages

deliver-messages{i:l}(es;X) ==

e:E.

v:Id

Message.
(v

X(e)

let m = snd(v) in
        let hdrs = msg-header(m) in
        let locs = [fst(v)] in

e':E. (e c

e'

m

BaseClass(hdrs;Message)@locs(e')))

Proof not projected

Definitions occuring in Statement : restricted-baseclass: BaseClass(h;T)@locs, msg-header: msg-header(m), Message: Message, classrel: v

X(e), es-causle: e c

e', es-E: E, Id: Id, let: let, pi1: fst(t), pi2: snd(t), all:

x:A. B[x], exists:

x:A. B[x], implies: P

Q, and: P

Q, product: x:A

B[x], cons: [car / cdr], nil: []
FDL editor aliases : deliver-messages

deliver-messages\{i:l\}(es;X) == \mforall{}e:E. \mforall{}v:Id \mtimes{} Message. (v \mmember{} X(e) {}\mRightarrow{} let m = snd(v) in let hdrs = msg-header(m) in let locs = [fst(v)] in \mexists{}e':E. (e c\mleq{} e' \mwedge{} m \mmember{} BaseClass(hdrs;Message)@locs(e'))) Date html generated: 2011_10_20-PM-04_52_03 Last ObjectModification: 2011_06_23-PM-01_07_24 Home Index