---

Step * 1 2 of Lemma order-messages_wf


1. allhdrs : Name List
2. f : hdr:Name ─→ Type
3. locs : Id List
4. hdrs : Name List
5. mcmp : hdr:Name ─→ comparison(f hdr)
6. (∀h∈allhdrs.valueall-type(f h))
7. (∀h∈hdrs.∀x,y:f h.  (((mcmp h x y) = 0 ∈ ℤ) ⇒ (x = y ∈ (f h))))
8. b : bag(Interface(to locs, with allhdrs))@i
9. single-valued-bag([mi∈b|¬bmsg-header(mi.msg) ∈b hdrs)];Interface)@i
10. x : Interface(to locs, with allhdrs)@i
11. x ↓∈ b@i
12. y : Interface(to locs, with allhdrs)@i
13. y ↓∈ b@i
14. (interface-cmp(mcmp;locs;allhdrs) x y) = 0 ∈ ℤ@i
15. (x.delay = y.delay ∈ ℤ)
∧ (x.dst = y.dst ∈ Id)
∧ msg-authentic(x.msg) = msg-authentic(y.msg)
∧ (msg-header(x.msg) = msg-header(y.msg) ∈ Name)
∧ ((mcmp msg-header(x.msg) msg-body(x.msg) msg-body(y.msg)) = 0 ∈ ℤ)
16. ¬(msg-header(x.msg) ∈ hdrs)
⊢ x = y ∈ Interface(to locs, with allhdrs)
BY
{ ((InstLemma `bag-member-subtype` [⌈Interface(to locs, with allhdrs)⌉;⌈Interface⌉]⋅ THENA Auto)
   THEN OnMaybeHyp 9 (\h. (Unfold `single-valued-bag` h
                           THEN ((InstHyp [⌈x⌉;⌈y⌉] h⋅ THENM (DVar `x'⋅ THEN EqTypeCD THEN Auto))
                                 THENA (Auto THEN BagMemberD 0 THEN Auto)
                                 )
                           ))
   ) }

---

Latex:

---

Latex:

1.  allhdrs  :  Name  List
2.  f  :  hdr:Name  {}\mrightarrow{}  Type
3.  locs  :  Id  List
4.  hdrs  :  Name  List
5.  mcmp  :  hdr:Name  {}\mrightarrow{}  comparison(f  hdr)
6.  (\mforall{}h\mmember{}allhdrs.valueall-type(f  h))
7.  (\mforall{}h\mmember{}hdrs.\mforall{}x,y:f  h.    (((mcmp  h  x  y)  =  0)  {}\mRightarrow{}  (x  =  y)))
8.  b  :  bag(Interface(to  locs,  with  allhdrs))@i
9.  single-valued-bag([mi\mmember{}b|\mneg{}\msubb{}msg-header(mi.msg)  \mmember{}\msubb{}  hdrs)];Interface)@i
10.  x  :  Interface(to  locs,  with  allhdrs)@i
11.  x  \mdownarrow{}\mmember{}  b@i
12.  y  :  Interface(to  locs,  with  allhdrs)@i
13.  y  \mdownarrow{}\mmember{}  b@i
14.  (interface-cmp(mcmp;locs;allhdrs)  x  y)  =  0@i
15.  (x.delay  =  y.delay)
\mwedge{}  (x.dst  =  y.dst)
\mwedge{}  msg-authentic(x.msg)  =  msg-authentic(y.msg)
\mwedge{}  (msg-header(x.msg)  =  msg-header(y.msg))
\mwedge{}  ((mcmp  msg-header(x.msg)  msg-body(x.msg)  msg-body(y.msg))  =  0)
16.  \mneg{}(msg-header(x.msg)  \mmember{}  hdrs)
\mvdash{}  x  =  y


By

---

Latex:
((InstLemma  `bag-member-subtype`  [\mkleeneopen{}Interface(to  locs,  with  allhdrs)\mkleeneclose{};\mkleeneopen{}Interface\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  OnMaybeHyp  9  (\mbackslash{}h.  (Unfold  `single-valued-bag`  h
                                                  THEN  ((InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  h\mcdot{}  THENM  (DVar  `x'\mcdot{}  THEN  EqTypeCD  THEN  Auto))
                                                              THENA  (Auto  THEN  BagMemberD  0  THEN  Auto)
                                                              )
                                                  ))
  )

---

Home Index