Step
*
2
2
2
1
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. u : A@i
7. v : A List@i
8. ∀X:hdataflow(A;B). ∀ys1,ys2:bag(hdataflow(A;C)). ∀a:A.
((ys1 = [y∈ys2|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C)))
⇒ ((snd(mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) ∧b hdf-halted(X);<X, ys1>)*(v)(a))) = (snd(mk-hd\000Cf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)*(v)(a))) ∈ bag(C)))@i
9. X : hdataflow(A;B)@i
10. ys1 : bag(hdataflow(A;C))@i
11. ys2 : bag(hdataflow(A;C))@i
12. a : A@i
13. ys1 = [y∈ys2|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))@i
14. (¬(ys1 = {} ∈ bag(hdataflow(A;C)))) ∨ (¬↑hdf-halted(X))
15. v2 : hdataflow(A;B)@i
16. v3 : bag(B)@i
17. X(u) = <v2, v3> ∈ (hdataflow(A;B) × bag(B))@i
18. λP.P(u) ∈ hdataflow(A;C) ─→ (hdataflow(A;C) × bag(C))
19. [y∈bag-map(λyb.(fst(yb));bag-map(λP.P(u);ys1 + bag-map(Y;v3)))|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))
⊢ [y∈bag-map(λyb.(fst(yb));bag-map(λP.P(u);ys1 + bag-map(Y;v3)))|¬bhdf-halted(y)]
= [y∈bag-map(λyb.(fst(yb));bag-map(λP.P(u);ys2 + bag-map(Y;v3)))|¬bhdf-halted(y)]
∈ bag(hdataflow(A;C))
BY
{ ((RWW "bag-map-append bag-filter-append" 0 THENA Auto)⋅ THEN 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. u : A@i
7. v : A List@i
8. ∀X:hdataflow(A;B). ∀ys1,ys2:bag(hdataflow(A;C)). ∀a:A.
((ys1 = [y∈ys2|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C)))
⇒ ((snd(mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) ∧b hdf-halted(X);<X, ys1>)*(v)(a))) = (snd(mk-hd\000Cf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)*(v)(a))) ∈ bag(C)))@i
9. X : hdataflow(A;B)@i
10. ys1 : bag(hdataflow(A;C))@i
11. ys2 : bag(hdataflow(A;C))@i
12. a : A@i
13. ys1 = [y∈ys2|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))@i
14. (¬(ys1 = {} ∈ bag(hdataflow(A;C)))) ∨ (¬↑hdf-halted(X))
15. v2 : hdataflow(A;B)@i
16. v3 : bag(B)@i
17. X(u) = <v2, v3> ∈ (hdataflow(A;B) × bag(B))@i
18. λP.P(u) ∈ hdataflow(A;C) ─→ (hdataflow(A;C) × bag(C))
19. [y∈bag-map(λyb.(fst(yb));bag-map(λP.P(u);ys1 + bag-map(Y;v3)))|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))
⊢ [y∈bag-map(λyb.(fst(yb));bag-map(λP.P(u);ys1))|¬bhdf-halted(y)]
= [y∈bag-map(λyb.(fst(yb));bag-map(λP.P(u);ys2))|¬bhdf-halted(y)]
∈ bag(hdataflow(A;C))
Latex:
1. A : Type
2. B : Type
3. C : Type
4. Y : B {}\mrightarrow{} hdataflow(A;C)
5. valueall-type(C)
6. u : A@i
7. v : A List@i
8. \mforall{}X:hdataflow(A;B). \mforall{}ys1,ys2:bag(hdataflow(A;C)). \mforall{}a:A.
((ys1 = [y\mmember{}ys2|\mneg{}\msubb{}hdf-halted(y)])
{}\mRightarrow{} ((snd(mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) \mwedge{}\msubb{} hdf-halted(X);<X, ys1>)*(\000Cv)(a))) = (snd(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)*(v)(a)))))@i
9. X : hdataflow(A;B)@i
10. ys1 : bag(hdataflow(A;C))@i
11. ys2 : bag(hdataflow(A;C))@i
12. a : A@i
13. ys1 = [y\mmember{}ys2|\mneg{}\msubb{}hdf-halted(y)]@i
14. (\mneg{}(ys1 = \{\})) \mvee{} (\mneg{}\muparrow{}hdf-halted(X))
15. v2 : hdataflow(A;B)@i
16. v3 : bag(B)@i
17. X(u) = <v2, v3>@i
18. \mlambda{}P.P(u) \mmember{} hdataflow(A;C) {}\mrightarrow{} (hdataflow(A;C) \mtimes{} bag(C))
19. [y\mmember{}bag-map(\mlambda{}yb.(fst(yb));bag-map(\mlambda{}P.P(u);ys1 + bag-map(Y;v3)))|\mneg{}\msubb{}hdf-halted(y)]
\mmember{} bag(hdataflow(A;C))
\mvdash{} [y\mmember{}bag-map(\mlambda{}yb.(fst(yb));bag-map(\mlambda{}P.P(u);ys1 + bag-map(Y;v3)))|\mneg{}\msubb{}hdf-halted(y)]
= [y\mmember{}bag-map(\mlambda{}yb.(fst(yb));bag-map(\mlambda{}P.P(u);ys2 + bag-map(Y;v3)))|\mneg{}\msubb{}hdf-halted(y)]
By
((RWW "bag-map-append bag-filter-append" 0 THENA Auto)\mcdot{} THEN EqCD THEN Auto)
Home
Index