---

Step * 1 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
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)
BY
{ (((Assert ∀es:EO+(Message(f)). ∀e:E.
              (X(e) = (snd(P loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(Interface)) BY
           (DVar `P' THEN Auto))
    THEN (InstHyp [⌈list-eo(L @ [m];a)⌉;⌈||L||⌉] (-1)⋅ THENA (Try (BLemma `list-eo-E`) THEN Auto))
    THEN Thin (-2))
   THEN OnMaybeHyp 4 (\h. (Unfold `single-valued-class-except` h
                           THEN (InstHyp [⌈list-eo(L @ [m];a)⌉;⌈||L||⌉] h⋅ THENA (Try (BLemma `list-eo-E`) THEN Auto))
                           ))
   ) }

1
1. [f] : Name ─→ Type
2. [hdrs] : Name List
3. [X] : EClass(Interface)
4. ∀es:EO+(Message(f)). ∀e:E.  single-valued-bag([v∈X(e)|¬bmsg-header(snd(snd(v))) ∈b hdrs)];Interface)@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
14. X(||L||) = (snd(P loc(||L||)*(map(λx.info(x);before(||L||)))(info(||L||)))) ∈ bag(Interface)
15. single-valued-bag([v∈X(||L||)|¬bmsg-header(snd(snd(v))) ∈b hdrs)];Interface)
⊢ 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
7.  L  :  Message(f)  List@i
8.  x  :  Message(f)  {}\mrightarrow{}  (hdataflow(Message(f);Interface)  \mtimes{}  bag(Interface))@i
9.  P  a*(L)  =  hdf-run(x)@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>@i
\mvdash{}  single-valued-bag([x\mmember{}v2|\mneg{}\msubb{}msg-header(snd(snd(x)))  \mmember{}\msubb{}  hdrs)];Interface)


By

---

Latex:
(((Assert  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.
                        (X(e)  =  (snd(P  loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e)))))  BY
                  (DVar  `P'  THEN  Auto))
    THEN  (InstHyp  [\mkleeneopen{}list-eo(L  @  [m];a)\mkleeneclose{};\mkleeneopen{}||L||\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Try  (BLemma  `list-eo-E`)  THEN  Auto))
    THEN  Thin  (-2))
  THEN  OnMaybeHyp  4  (\mbackslash{}h.  (Unfold  `single-valued-class-except`  h
                                                  THEN  (InstHyp  [\mkleeneopen{}list-eo(L  @  [m];a)\mkleeneclose{};\mkleeneopen{}||L||\mkleeneclose{}]  h\mcdot{}
                                                              THENA  (Try  (BLemma  `list-eo-E`)  THEN  Auto)
                                                              )
                                                  ))
  )

---

Home Index