---

Step * 1 of Lemma local-class-single-valued-class-except


1. [f] : Name ─→ Type
2. [hdrs] : Name List
3. [X] : EClass(Interface)
4. single-valued-class-except{i:l}(f;hdrs;X)@i'
5. P : LocalClass(X)@i'
6. a : Id@i
⊢ hdf-single-valued-except(f;hdrs;P a)
BY
{ (D 0
   THEN Auto
   THEN (GenConclAtAddr [1] THENA Auto)
   THEN MoveToConcl (-1)
   THEN (HDataflowHD (-1) THENA Auto)
   THEN Reduce 0
   THEN Try (Fold `hdf-run` 0)
   THEN Auto
   THEN (RW (AddrC [1] (RevLemmaC `hdf-ap-run`)) 0 THENA Auto)
   THEN (GenConclAtAddr [1] THENA Auto)
   THEN D -2
   THEN Reduce 0) }

1
1. [f] : Name ─→ Type
2. [hdrs] : Name List
3. [X] : EClass(Interface)
4. single-valued-class-except{i:l}(f;hdrs;X)@i'
5. P : LocalClass(X)@i'
6. a : Id@i
7. L : Message(f) List@i
8. x : Message(f) ─→ (hdataflow(Message(f);Interface) × bag(Interface))@i
9. P a*(L) = hdf-run(x) ∈ hdataflow(Message(f);Interface)@i
10. m : Message(f)@i
11. v1 : hdataflow(Message(f);Interface)@i
12. v2 : bag(Interface)@i
13. hdf-run(x)(m) = <v1, v2> ∈ (hdataflow(Message(f);Interface) × bag(Interface))@i
⊢ single-valued-bag([x∈v2|¬bmsg-header(snd(snd(x))) ∈b hdrs)];Interface)

---

Latex:

---

Latex:

1.  [f]  :  Name  {}\mrightarrow{}  Type
2.  [hdrs]  :  Name  List
3.  [X]  :  EClass(Interface)
4.  single-valued-class-except\{i:l\}(f;hdrs;X)@i'
5.  P  :  LocalClass(X)@i'
6.  a  :  Id@i
\mvdash{}  hdf-single-valued-except(f;hdrs;P  a)


By

---

Latex:
(D  0
  THEN  Auto
  THEN  (GenConclAtAddr  [1]  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (HDataflowHD  (-1)  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  (Fold  `hdf-run`  0)
  THEN  Auto
  THEN  (RW  (AddrC  [1]  (RevLemmaC  `hdf-ap-run`))  0  THENA  Auto)
  THEN  (GenConclAtAddr  [1]  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0)

---

Home Index