---

Step * of Lemma hdf-ap-only-headers2

∀[f:Name ⟶ Type]
  ∀hdrs:Name List. ∀X:{X:msg-interface-hdf(f)| hdf-only-headers(f;hdrs;X)} . ∀m:Message(f). ∀mi:Interface.
    (mi ↓∈ snd(X(m)) ⇒ (msg-header(mi.msg) ∈ hdrs))
BY
{ (Unfold `msg-interface-hdf` 0
   THEN Unfold `hdf-only-headers` 0
   THEN Intros
   THEN InstLemma `hdf-ap-invariant2` [⌜Message(f)⌝;⌜ℤ × Id × Message(f)⌝;⌜λ2b.∀mi:Interface
                                                                                 (mi ↓∈ b
                                                                                 ⇒ (msg-header(mi.msg) ∈ hdrs))⌝]⋅
   THEN Auto
   THEN Try (BagMemberD (-1))) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type]
    \mforall{}hdrs:Name  List.  \mforall{}X:\{X:msg-interface-hdf(f)|  hdf-only-headers(f;hdrs;X)\}  .  \mforall{}m:Message(f).
    \mforall{}mi:Interface.
        (mi  \mdownarrow{}\mmember{}  snd(X(m))  {}\mRightarrow{}  (msg-header(mi.msg)  \mmember{}  hdrs))


By

---

Latex:
(Unfold  `msg-interface-hdf`  0
  THEN  Unfold  `hdf-only-headers`  0
  THEN  Intros
  THEN  InstLemma  `hdf-ap-invariant2`  [\mkleeneopen{}Message(f)\mkleeneclose{};\mkleeneopen{}\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Message(f)\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}b.\mforall{}mi:Interface.  (mi  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (msg-header(mi.msg)  \mmember{}  hdrs))\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (BagMemberD  (-1)))

---

Home Index