---

Step * 1 2 1 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))
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)
BY
{ (EqCD THEN Auto)⋅ }

1
.....subterm..... T:t
1:n
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);ys2).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))
16.  \mforall{}[ba,bb:bag(hdataflow(A;C)  \mtimes{}  bag(C))].  \mforall{}[f:(hdataflow(A;C)  \mtimes{}  bag(C))  {}\mrightarrow{}  bag(C)].
            (\mcup{}x\mmember{}ba  +  bb.f[x]  =  (\mcup{}x\mmember{}ba.f[x]  +  \mcup{}x\mmember{}bb.f[x]))
\mvdash{}  (\mcup{}yb\mmember{}bag-map(\mlambda{}P.P(a);ys1).snd(yb)  +  \mcup{}yb\mmember{}bag-map(\mlambda{}P.P(a);bag-map(Y;v2)).snd(yb))
=  (\mcup{}yb\mmember{}bag-map(\mlambda{}P.P(a);ys2).snd(yb)  +  \mcup{}yb\mmember{}bag-map(\mlambda{}P.P(a);bag-map(Y;v2)).snd(yb))


By

(EqCD  THEN  Auto)\mcdot{}

---

Home Index