---

Step * 1 of Lemma interface-cmp_wf

.....wf..... 
1. f : Name ─→ Type
2. locs : Id List
3. hdrs : Name List
4. mcmp : hdr:Name ─→ comparison(f hdr)
5. list-index-cmp(IdDeq;locs;λmi.mi.dst) ∈ comparison(Interface(to locs, with hdrs))
6. list-index-cmp(NameDeq;hdrs;λmi.msg-header(mi.msg)) ∈ comparison(Interface(to locs, with hdrs))
⊢ compare-fun(message-cmp(hdrs;mcmp);λmi.mi.msg) ∈ comparison(Interface(to locs, with hdrs))
BY
{ (Using [`B',⌈{m:Message(f)| (msg-header(m) ∈ hdrs)} ⌉] MemCD⋅ THEN Auto THEN D -1 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  f  :  Name  {}\mrightarrow{}  Type
2.  locs  :  Id  List
3.  hdrs  :  Name  List
4.  mcmp  :  hdr:Name  {}\mrightarrow{}  comparison(f  hdr)
5.  list-index-cmp(IdDeq;locs;\mlambda{}mi.mi.dst)  \mmember{}  comparison(Interface(to  locs,  with  hdrs))
6.  list-index-cmp(NameDeq;hdrs;\mlambda{}mi.msg-header(mi.msg))  \mmember{}  comparison(Interface(to  locs,  with  hdrs))
\mvdash{}  compare-fun(message-cmp(hdrs;mcmp);\mlambda{}mi.mi.msg)  \mmember{}  comparison(Interface(to  locs,  with  hdrs))


By

---

Latex:
(Using  [`B',\mkleeneopen{}\{m:Message(f)|  (msg-header(m)  \mmember{}  hdrs)\}  \mkleeneclose{}]  MemCD\mcdot{}  THEN  Auto  THEN  D  -1  THEN  Auto)

---

Home Index