---

Step * of Lemma hdf-ap-single-valued-except2

∀[f:Name ─→ Type]. ∀[hdrs:Name List].
  ∀X:{X:msg-interface-hdf(f)| hdf-single-valued-except(f;hdrs;X)} . ∀m:Message(f).
    single-valued-bag([x∈snd(X(m))|¬bmsg-header(snd(snd(x))) ∈b hdrs)];Interface)
BY
{ (Auto
   THEN Unfold `hdf-single-valued-except` -2
   THEN Unfold `msg-interface-hdf` -2
   THEN InstLemma `hdf-ap-invariant2` [Message(f);⌈ℤ × Id × Message(f)⌉;
   ⌈λ2b.single-valued-bag([x∈b|¬bmsg-header(snd(snd(x))) ∈b hdrs)];Interface)⌉]⋅
   THEN Auto
   THEN Try ((Unfold `single-valued-bag` 0 THEN Complete (Auto)))) }

1
.....antecedent..... 
1. f : Name ─→ Type
2. hdrs : Name List
3. X : {X:hdataflow(Message(f);ℤ × Id × Message(f))| 
        hdf-invariant(Message(f);b.single-valued-bag([x∈b|¬bmsg-header(snd(snd(x))) ∈b hdrs)];Interface);X)} @i
4. m : Message(f)@i
⊢ single-valued-bag([x∈{}|¬bmsg-header(snd(snd(x))) ∈b hdrs)];Interface)

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdrs:Name  List].
    \mforall{}X:\{X:msg-interface-hdf(f)|  hdf-single-valued-except(f;hdrs;X)\}  .  \mforall{}m:Message(f).
        single-valued-bag([x\mmember{}snd(X(m))|\mneg{}\msubb{}msg-header(snd(snd(x)))  \mmember{}\msubb{}  hdrs)];Interface)


By

---

Latex:
(Auto
  THEN  Unfold  `hdf-single-valued-except`  -2
  THEN  Unfold  `msg-interface-hdf`  -2
  THEN  InstLemma  `hdf-ap-invariant2`  [Message(f);\mkleeneopen{}\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Message(f)\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}b.single-valued-bag([x\mmember{}b|\mneg{}\msubb{}msg-header(snd(snd(x)))  \mmember{}\msubb{}  hdrs)];Interface)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((Unfold  `single-valued-bag`  0  THEN  Complete  (Auto))))

---

Home Index