---

Step * of Lemma msg-body-cmp_wf

∀[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
  ∀a:{x:Message(f)| (msg-header(x) ∈ hdrs)} 
    (msg-body-cmp(mcmp) ∈ comparison({b:{m:Message(f)| (msg-header(m) ∈ hdrs)} | 
                                      (list-index-cmp(NameDeq;hdrs;λm.msg-header(m)) a b) = 0 ∈ ℤ} ))
BY
{ (Intros
   THEN (Unhide THEN Unfold `msg-body-cmp` 0)
   THEN SubsumeC ⌜comparison({m:Message(f)| msg-header(m) = msg-header(a) ∈ Name} )⌝⋅) }

1
1. f : Name ⟶ Type
2. hdrs : Name List
3. mcmp : hdr:Name ⟶ comparison(f hdr)
4. a : {x:Message(f)| (msg-header(x) ∈ hdrs)} @i
⊢ λm1,m2. (mcmp msg-header(m1) msg-body(m1) msg-body(m2)) ∈ comparison({m:Message(f)| msg-header(m) = msg-header(a) ∈ Na\000Cme} )

2
1. f : Name ⟶ Type
2. hdrs : Name List
3. mcmp : hdr:Name ⟶ comparison(f hdr)
4. a : {x:Message(f)| (msg-header(x) ∈ hdrs)} @i
5. (λm1,m2. (mcmp msg-header(m1) msg-body(m1) msg-body(m2)))
= (λm1,m2. (mcmp msg-header(m1) msg-body(m1) msg-body(m2)))
∈ comparison({m:Message(f)| msg-header(m) = msg-header(a) ∈ Name} )
⊢ comparison({m:Message(f)| msg-header(m) = msg-header(a) ∈ Name} ) ⊆r comparison({b:{m:Message(f)| (msg-header(m) ∈ hdr\000Cs)} | 
                                                                         (list-index-cmp(NameDeq;hdrs;λm.msg-header(m)) 
                                                                          a 
                                                                          b)
                                                                         = 0
                                                                         ∈ ℤ} )

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdrs:Name  List].  \mforall{}[mcmp:hdr:Name  {}\mrightarrow{}  comparison(f  hdr)].
    \mforall{}a:\{x:Message(f)|  (msg-header(x)  \mmember{}  hdrs)\} 
        (msg-body-cmp(mcmp)  \mmember{}  comparison(\{b:\{m:Message(f)|  (msg-header(m)  \mmember{}  hdrs)\}  | 
                                                                            (list-index-cmp(NameDeq;hdrs;\mlambda{}m.msg-header(m))  a  b)  =  0\}  ))


By

---

Latex:
(Intros
  THEN  (Unhide  THEN  Unfold  `msg-body-cmp`  0)
  THEN  SubsumeC  \mkleeneopen{}comparison(\{m:Message(f)|  msg-header(m)  =  msg-header(a)\}  )\mkleeneclose{}\mcdot{})

---

Home Index