---

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

.....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)
BY
{ (RepUR ``bag-filter empty-bag`` 0 THEN Fold `empty-bag` 0 THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  f  :  Name  {}\mrightarrow{}  Type
2.  hdrs  :  Name  List
3.  X  :  \{X:hdataflow(Message(f);\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Message(f))| 
                hdf-invariant(Message(f);b.single-valued-bag([x\mmember{}b|\mneg{}\msubb{}msg-header(snd(snd(x)))  \mmember{}\msubb{}  hdrs)];
                                                                              Interface);X)\}  @i
4.  m  :  Message(f)@i
\mvdash{}  single-valued-bag([x\mmember{}\{\}|\mneg{}\msubb{}msg-header(snd(snd(x)))  \mmember{}\msubb{}  hdrs)];Interface)


By

---

Latex:
(RepUR  ``bag-filter  empty-bag``  0  THEN  Fold  `empty-bag`  0  THEN  Auto)

---

Home Index