---

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


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 a*(map(λx.info(x);before(||L||)))(info(||L||)))) ∈ bag(Interface)
15. ||L|| ∈ E
⊢ v2 = (snd(P a*(firstn(||L||;L @ [m]))(L @ [m][||L||]))) ∈ bag(Interface)
BY
{ Subst' firstn(||L||;L @ [m]) ~ L 0 }

1
.....equality..... 
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 a*(map(λx.info(x);before(||L||)))(info(||L||)))) ∈ bag(Interface)
15. ||L|| ∈ E
⊢ firstn(||L||;L @ [m]) ~ L

2
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 a*(map(λx.info(x);before(||L||)))(info(||L||)))) ∈ bag(Interface)
15. ||L|| ∈ E
⊢ v2 = (snd(P a*(L)(L @ [m][||L||]))) ∈ bag(Interface)

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  hdrs  :  Name  List
3.  X  :  EClass(Interface)
4.  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.
          single-valued-bag([v\mmember{}X(e)|\mneg{}\msubb{}msg-header(snd(snd(v)))  \mmember{}\msubb{}  hdrs];Interface)@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
14.  X(||L||)  =  (snd(P  a*(map(\mlambda{}x.info(x);before(||L||)))(info(||L||))))
15.  ||L||  \mmember{}  E
\mvdash{}  v2  =  (snd(P  a*(firstn(||L||;L  @  [m]))(L  @  [m][||L||])))


By

---

Latex:
Subst'  firstn(||L||;L  @  [m])  \msim{}  L  0

---

Home Index