---

Step * 1 1 of Lemma msg-body-cmp_wf


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. λx,y. (mcmp msg-header(a) msg-body(x) msg-body(y)) ∈ comparison({m:Message(f)| msg-header(m) = msg-header(a) ∈ Name} \000C)
⊢ λm1,m2. (mcmp msg-header(m1) msg-body(m1) msg-body(m2)) ∈ comparison({m:Message(f)| msg-header(m) = msg-header(a) ∈ Na\000Cme} )
BY
{ (Assert (λm1,m2. (mcmp msg-header(m1) msg-body(m1) msg-body(m2)))
         = (λx,y. (mcmp msg-header(a) msg-body(x) msg-body(y)))
         ∈ ({m:Message(f)| msg-header(m) = msg-header(a) ∈ Name} 
           ─→ {m:Message(f)| msg-header(m) = msg-header(a) ∈ Name} 
           ─→ ℤ) BY
         ((EqCD THENA Auto) THEN D -1 THEN HypSubst' (-1) 0 THEN Auto)) }

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
5. λx,y. (mcmp msg-header(a) msg-body(x) msg-body(y)) ∈ comparison({m:Message(f)| msg-header(m) = msg-header(a) ∈ Name} \000C)
6. (λm1,m2. (mcmp msg-header(m1) msg-body(m1) msg-body(m2)))
= (λx,y. (mcmp msg-header(a) msg-body(x) msg-body(y)))
∈ ({m:Message(f)| msg-header(m) = msg-header(a) ∈ Name}  ─→ {m:Message(f)| msg-header(m) = msg-header(a) ∈ Name}  ─→ ℤ)
⊢ λm1,m2. (mcmp msg-header(m1) msg-body(m1) msg-body(m2)) ∈ comparison({m:Message(f)| msg-header(m) = msg-header(a) ∈ Na\000Cme} )

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  hdrs  :  Name  List
3.  mcmp  :  hdr:Name  {}\mrightarrow{}  comparison(f  hdr)
4.  a  :  \{x:Message(f)|  (msg-header(x)  \mmember{}  hdrs)\}  @i
5.  \mlambda{}x,y.  (mcmp  msg-header(a)  msg-body(x)  msg-body(y))  \mmember{}  comparison(\{m:Message(f)| 
                                                                                                                                msg-header(m)  =  msg-header(a)\}  )
\mvdash{}  \mlambda{}m1,m2.  (mcmp  msg-header(m1)  msg-body(m1)  msg-body(m2))  \mmember{}  comparison(\{m:Message(f)| 
                                                                                                                                    msg-header(m)  =  msg-header(a)\}  )


By

---

Latex:
(Assert  (\mlambda{}m1,m2.  (mcmp  msg-header(m1)  msg-body(m1)  msg-body(m2)))
              =  (\mlambda{}x,y.  (mcmp  msg-header(a)  msg-body(x)  msg-body(y)))  BY
              ((EqCD  THENA  Auto)  THEN  D  -1  THEN  HypSubst'  (-1)  0  THEN  Auto))

---

Home Index