Nuprl Lemma : member-local-simulation-inputs

f:Name ⟶ Type
  ∀[Info:Type]
    ∀es:EO+(Message(f)). ∀hdr:Name. ∀locs:bag(Id).
      ∀e:E. ∀v:Id × Info.
        ((v ∈ local-simulation-inputs(es;e;hdr;locs))
        ⇐⇒ ∃e':E
             (e' ≤loc 
             ∧ (msg-header(info(e')) hdr ∈ Name)
             ∧ fst(v) ↓∈ locs
             ∧ (v msg-body(info(e')) ∈ (Id × Info)))) 
      supposing hdr encodes Id × Info


Proof




Definitions occuring in Statement :  local-simulation-inputs: local-simulation-inputs(es;e;hdr;locs) encodes-msg-type: hdr encodes T msg-body: msg-body(msg) msg-header: msg-header(m) Message: Message(f) es-info: info(e) event-ordering+: EO+(Info) es-le: e ≤loc e'  es-E: E Id: Id name: Name l_member: (x ∈ l) uimplies: supposing a uall: [x:A]. B[x] pi1: fst(t) all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q function: x:A ⟶ B[x] product: x:A × B[x] universe: Type equal: t ∈ T bag-member: x ↓∈ bs bag: bag(T)
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T encodes-msg-type: hdr encodes T subtype_rel: A ⊆B local-simulation-inputs: local-simulation-inputs(es;e;hdr;locs) prop: guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] top: Top cand: c∧ B iff: ⇐⇒ Q and: P ∧ Q implies:  Q msg-type: msg-type(msg;f) name: Name sq_type: SQType(T) rev_implies:  Q exists: x:A. B[x] sq_stable: SqStable(P) squash: T pi1: fst(t) true: True

Latex:
\mforall{}f:Name  {}\mrightarrow{}  Type
    \mforall{}[Info:Type]
        \mforall{}es:EO+(Message(f)).  \mforall{}hdr:Name.  \mforall{}locs:bag(Id).
            \mforall{}e:E.  \mforall{}v:Id  \mtimes{}  Info.
                ((v  \mmember{}  local-simulation-inputs(es;e;hdr;locs))
                \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E
                          (e'  \mleq{}loc  e 
                          \mwedge{}  (msg-header(info(e'))  =  hdr)
                          \mwedge{}  fst(v)  \mdownarrow{}\mmember{}  locs
                          \mwedge{}  (v  =  msg-body(info(e'))))) 
            supposing  hdr  encodes  Id  \mtimes{}  Info



Date html generated: 2016_05_17-AM-08_53_17
Last ObjectModification: 2016_01_17-PM-08_34_14

Theory : messages


Home Index