---

Step * 1 1 1 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:Name. ((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 ∈ ℤ
16. x.dst = y.dst ∈ Id
17. msg-authentic(x.msg) = msg-authentic(y.msg)
18. msg-header(x.msg) = msg-header(y.msg) ∈ Name
19. (mcmp msg-header(x.msg) msg-body(x.msg) msg-body(y.msg)) = 0 ∈ ℤ
20. (msg-header(x.msg) ∈ hdrs)
21. msg-body(x.msg) = msg-body(y.msg) ∈ (f msg-header(x.msg))
⊢ x = y ∈ Interface(to locs, with allhdrs)
BY
{ (DVar `x' THEN DVar `y' THEN EqTypeCD THEN Auto) }

1
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:Name. ((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@i
11. (x.dst ∈ locs)@i
12. (msg-header(x.msg) ∈ allhdrs)@i
13. x ↓∈ b@i
14. y : Interface@i
15. (y.dst ∈ locs)@i
16. (msg-header(y.msg) ∈ allhdrs)@i
17. y ↓∈ b@i
18. (interface-cmp(mcmp;locs;allhdrs) x y) = 0 ∈ ℤ@i
19. x.delay = y.delay ∈ ℤ
20. x.dst = y.dst ∈ Id
21. msg-authentic(x.msg) = msg-authentic(y.msg)
22. msg-header(x.msg) = msg-header(y.msg) ∈ Name
23. (mcmp msg-header(x.msg) msg-body(x.msg) msg-body(y.msg)) = 0 ∈ ℤ
24. (msg-header(x.msg) ∈ hdrs)
25. msg-body(x.msg) = msg-body(y.msg) ∈ (f msg-header(x.msg))
⊢ x = y ∈ Interface

---

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:Name.  ((h  \mmember{}  hdrs)  {}\mRightarrow{}  (\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
16.  x.dst  =  y.dst
17.  msg-authentic(x.msg)  =  msg-authentic(y.msg)
18.  msg-header(x.msg)  =  msg-header(y.msg)
19.  (mcmp  msg-header(x.msg)  msg-body(x.msg)  msg-body(y.msg))  =  0
20.  (msg-header(x.msg)  \mmember{}  hdrs)
21.  msg-body(x.msg)  =  msg-body(y.msg)
\mvdash{}  x  =  y


By

---

Latex:
(DVar  `x'  THEN  DVar  `y'  THEN  EqTypeCD  THEN  Auto)

---

Home Index