---

Step * of Lemma interface-cmp_wf

∀[f:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
  (interface-cmp(mcmp;locs;hdrs) ∈ comparison(Interface(to locs, with hdrs)))
BY
{ (Auto
   THEN (Assert list-index-cmp(IdDeq;locs;λmi.mi.dst) ∈ comparison(Interface(to locs, with hdrs)) BY
               ((InstLemma `list-index-cmp_wf` [⌜Id⌝;⌜IdDeq⌝;⌜locs⌝;⌜Interface(to locs, with hdrs)⌝;⌜λmi.mi.dst⌝]⋅
                 THENA Auto
                 )
                THEN DoSubsume
                THEN Try (Trivial)
                THEN (BLemma `subtype_rel_comparison` THENA Auto)
                THEN Reduce 0
                THEN (D 0 THENA Auto)
                THEN D -1
                THEN MemTypeCD
                THEN Auto))
   THEN (Assert list-index-cmp(NameDeq;hdrs;λmi.msg-header(mi.msg)) ∈ comparison(Interface(to locs, with hdrs)) BY
               ((InstLemma `list-index-cmp_wf` [⌜Name⌝;⌜NameDeq⌝;⌜hdrs⌝;⌜Interface(to locs, with hdrs)⌝;
                 ⌜λmi.msg-header(mi.msg)⌝]⋅
                 THENA Auto
                 )
                THEN DoSubsume
                THEN Try (Trivial)
                THEN (BLemma `subtype_rel_comparison` THENA Auto)
                THEN Reduce 0
                THEN (D 0 THENA Auto)
                THEN D -1
                THEN MemTypeCD
                THEN Auto))
   THEN Unfold `interface-cmp` 0
   THEN BLemma `comparison-seq-simple-wf`
   THEN Try (BLemma `comparison-seq-simple-wf`)
   THEN Try (QuickAuto)) }

1
.....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))

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[locs:Id  List].  \mforall{}[hdrs:Name  List].  \mforall{}[mcmp:hdr:Name  {}\mrightarrow{}  comparison(f  hdr)].
    (interface-cmp(mcmp;locs;hdrs)  \mmember{}  comparison(Interface(to  locs,  with  hdrs)))


By

---

Latex:
(Auto
  THEN  (Assert  list-index-cmp(IdDeq;locs;\mlambda{}mi.mi.dst)  \mmember{}  comparison(Interface(to  locs,  with  hdrs))  BY
                          ((InstLemma  `list-index-cmp\_wf`  [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}IdDeq\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{};\mkleeneopen{}Interface(to  locs,  with  hdrs)\mkleeneclose{};
                              \mkleeneopen{}\mlambda{}mi.mi.dst\mkleeneclose{}]\mcdot{}
                              THENA  Auto
                              )
                            THEN  DoSubsume
                            THEN  Try  (Trivial)
                            THEN  (BLemma  `subtype\_rel\_comparison`  THENA  Auto)
                            THEN  Reduce  0
                            THEN  (D  0  THENA  Auto)
                            THEN  D  -1
                            THEN  MemTypeCD
                            THEN  Auto))
  THEN  (Assert  list-index-cmp(NameDeq;hdrs;\mlambda{}mi.msg-header(mi.msg))
                            \mmember{}  comparison(Interface(to  locs,  with  hdrs))  BY
                          ((InstLemma  `list-index-cmp\_wf`  [\mkleeneopen{}Name\mkleeneclose{};\mkleeneopen{}NameDeq\mkleeneclose{};\mkleeneopen{}hdrs\mkleeneclose{};
                              \mkleeneopen{}Interface(to  locs,  with  hdrs)\mkleeneclose{};\mkleeneopen{}\mlambda{}mi.msg-header(mi.msg)\mkleeneclose{}]\mcdot{}
                              THENA  Auto
                              )
                            THEN  DoSubsume
                            THEN  Try  (Trivial)
                            THEN  (BLemma  `subtype\_rel\_comparison`  THENA  Auto)
                            THEN  Reduce  0
                            THEN  (D  0  THENA  Auto)
                            THEN  D  -1
                            THEN  MemTypeCD
                            THEN  Auto))
  THEN  Unfold  `interface-cmp`  0
  THEN  BLemma  `comparison-seq-simple-wf`
  THEN  Try  (BLemma  `comparison-seq-simple-wf`)
  THEN  Try  (QuickAuto))

---

Home Index