---

Step * 1 2 1 of Lemma iterate-hdf-bind-simple


1. A : Type
2. B : Type
3. C : Type
4. Y : B ─→ hdataflow(A;C)
5. valueall-type(C)
6. X : hdataflow(A;B)@i
7. ys1 : bag(hdataflow(A;C))@i
8. ys2 : bag(hdataflow(A;C))@i
9. a : A@i
10. ys1 = [y∈ys2|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))@i
11. (¬(ys1 = {} ∈ bag(hdataflow(A;C)))) ∨ (¬↑hdf-halted(X))
12. v1 : hdataflow(A;B)@i
13. v2 : bag(B)@i
14. X(a) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
15. λP.P(a) ∈ hdataflow(A;C) ─→ (hdataflow(A;C) × bag(C))
⊢ ∪yb∈bag-map(λP.P(a);ys1 + bag-map(Y;v2)).snd(yb) = ∪yb∈bag-map(λP.P(a);ys2 + bag-map(Y;v2)).snd(yb) ∈ bag(C)
BY
{ ((RWO "bag-map-append" 0 THENA Auto)⋅
   THEN (InstLemma `bag-combine-append-left` [⌈hdataflow(A;C) × bag(C)⌉;⌈C⌉]⋅ THENA Auto)
   THEN RWO "-1" 0
   THEN Auto) }

1
1. A : Type
2. B : Type
3. C : Type
4. Y : B ─→ hdataflow(A;C)
5. valueall-type(C)
6. X : hdataflow(A;B)@i
7. ys1 : bag(hdataflow(A;C))@i
8. ys2 : bag(hdataflow(A;C))@i
9. a : A@i
10. ys1 = [y∈ys2|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))@i
11. (¬(ys1 = {} ∈ bag(hdataflow(A;C)))) ∨ (¬↑hdf-halted(X))
12. v1 : hdataflow(A;B)@i
13. v2 : bag(B)@i
14. X(a) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
15. λP.P(a) ∈ hdataflow(A;C) ─→ (hdataflow(A;C) × bag(C))
16. ∀[ba,bb:bag(hdataflow(A;C) × bag(C))]. ∀[f:(hdataflow(A;C) × bag(C)) ─→ bag(C)].
      (∪x∈ba + bb.f[x] = (∪x∈ba.f[x] + ∪x∈bb.f[x]) ∈ bag(C))
⊢ (∪yb∈bag-map(λP.P(a);ys1).snd(yb) + ∪yb∈bag-map(λP.P(a);bag-map(Y;v2)).snd(yb))
= (∪yb∈bag-map(λP.P(a);ys2).snd(yb) + ∪yb∈bag-map(λP.P(a);bag-map(Y;v2)).snd(yb))
∈ bag(C)

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  Y  :  B  {}\mrightarrow{}  hdataflow(A;C)
5.  valueall-type(C)
6.  X  :  hdataflow(A;B)@i
7.  ys1  :  bag(hdataflow(A;C))@i
8.  ys2  :  bag(hdataflow(A;C))@i
9.  a  :  A@i
10.  ys1  =  [y\mmember{}ys2|\mneg{}\msubb{}hdf-halted(y)]@i
11.  (\mneg{}(ys1  =  \{\}))  \mvee{}  (\mneg{}\muparrow{}hdf-halted(X))
12.  v1  :  hdataflow(A;B)@i
13.  v2  :  bag(B)@i
14.  X(a)  =  <v1,  v2>@i
15.  \mlambda{}P.P(a)  \mmember{}  hdataflow(A;C)  {}\mrightarrow{}  (hdataflow(A;C)  \mtimes{}  bag(C))
\mvdash{}  \mcup{}yb\mmember{}bag-map(\mlambda{}P.P(a);ys1  +  bag-map(Y;v2)).snd(yb)
=  \mcup{}yb\mmember{}bag-map(\mlambda{}P.P(a);ys2  +  bag-map(Y;v2)).snd(yb)


By

((RWO  "bag-map-append"  0  THENA  Auto)\mcdot{}
  THEN  (InstLemma  `bag-combine-append-left`  [\mkleeneopen{}hdataflow(A;C)  \mtimes{}  bag(C)\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index