---

Step * 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∈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 ∈ ℤ)
⊢ x = y ∈ Interface(to locs, with allhdrs)
BY
{ (Decide ⌈(msg-header(x.msg) ∈ hdrs)⌉⋅ THENA 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∈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)

2
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)

---

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)
\mvdash{}  x  =  y


By

---

Latex:
(Decide  \mkleeneopen{}(msg-header(x.msg)  \mmember{}  hdrs)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index