---

Step * of Lemma order-messages_wf

∀[allhdrs:Name List]. ∀[f:hdr:Name ─→ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ─→ comparison(f hdr)].
  order-messages(mcmp;locs;allhdrs) ∈ {b:bag(Interface(to locs, with allhdrs))| 
                                       single-valued-bag([mi∈b|¬bmsg-header(mi.msg) ∈b hdrs)];Interface)}  ─→ (Interface\000C(to locs, with allhdrs) List) 
  supposing (∀h∈allhdrs.valueall-type(f h)) ∧ (∀h∈hdrs.∀x,y:f h.  (((mcmp h x y) = 0 ∈ ℤ) ⇒ (x = y ∈ (f h))))
BY
{ (Auto
   THEN Unfold `order-messages` 0
   THEN (MemCD THENA Auto)
   THEN D -1
   THEN Auto
   THEN DSetVars
   THEN (FLemma `interface-cmp-zero` [-1] 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 ∈ ℤ)
⊢ x = y ∈ Interface(to locs, with allhdrs)

---

Latex:

---

Latex:
\mforall{}[allhdrs:Name  List].  \mforall{}[f:hdr:Name  {}\mrightarrow{}  Type].  \mforall{}[locs:Id  List].  \mforall{}[hdrs:Name  List].
\mforall{}[mcmp:hdr:Name  {}\mrightarrow{}  comparison(f  hdr)].
    order-messages(mcmp;locs;allhdrs)  \mmember{}  \{b:bag(Interface(to  locs,  with  allhdrs))| 
                                                                              single-valued-bag([mi\mmember{}b|\mneg{}\msubb{}msg-header(mi.msg)  \mmember{}\msubb{}  hdrs)];
                                                                                      Interface)\}    {}\mrightarrow{}  (Interface(to  locs,  with  allhdrs)  List) 
    supposing  (\mforall{}h\mmember{}allhdrs.valueall-type(f  h))  \mwedge{}  (\mforall{}h\mmember{}hdrs.\mforall{}x,y:f  h.    (((mcmp  h  x  y)  =  0)  {}\mRightarrow{}  (x  =  y)))


By

---

Latex:
(Auto
  THEN  Unfold  `order-messages`  0
  THEN  (MemCD  THENA  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  DSetVars
  THEN  (FLemma  `interface-cmp-zero`  [-1]  THENA  Auto))

---

Home Index