Step
*
1
2
2
1
1
1
of Lemma
hdf-parallel-bind-halt-eq
.....equality.....
1. A : Type
2. B : Type
3. C : Type
4. valueall-type(B)
5. valueall-type(C)
6. u : A@i
7. v : A List@i
8. ∀X1,X2:hdataflow(A;B). ∀X:B ─→ hdataflow(A;C). ∀hdfs1,hdfs2:bag(hdataflow(A;C)).
hdf-halted(X1 (hdfs1) >>= X || X2 (hdfs2) >>= X*(v)) = hdf-halted(X1 || X2 (hdfs1 + hdfs2) >>= X*(v))@i
9. X1 : hdataflow(A;B)@i
10. X2 : hdataflow(A;B)@i
11. X : B ─→ hdataflow(A;C)@i
12. hdfs1 : bag(hdataflow(A;C))@i
13. hdfs2 : bag(hdataflow(A;C))@i
14. ¬((↑hdf-halted(X1 (hdfs1) >>= X)) ∧ (↑hdf-halted(X2 (hdfs2) >>= X)))
15. v2 : hdataflow(A;C)@i
16. v3 : bag(C)@i
17. fst(X1(u)) ([y∈bag-map(λP.(fst(P(u)));hdfs1 + bag-map(X;snd(X1(u))))|¬bhdf-halted(y)]) >>= X = v2 ∈ hdataflow(A;C)
18. ∪p∈bag-map(λP.P(u);hdfs1 + bag-map(X;snd(X1(u)))).snd(p) = v3 ∈ bag(C)
19. v5 : hdataflow(A;C)@i
20. v6 : bag(C)@i
21. fst(X2(u)) ([y∈bag-map(λP.(fst(P(u)));hdfs2 + bag-map(X;snd(X2(u))))|¬bhdf-halted(y)]) >>= X = v5 ∈ hdataflow(A;C)
22. ∪p∈bag-map(λP.P(u);hdfs2 + bag-map(X;snd(X2(u)))).snd(p) = v6 ∈ bag(C)
⊢ [y∈bag-map(λP.(fst(P(u)));(hdfs1 + hdfs2) + bag-map(X;(snd(X1(u))) + (snd(X2(u)))))|¬bhdf-halted(y)]
= ([y∈bag-map(λP.(fst(P(u)));hdfs1 + bag-map(X;snd(X1(u))))|¬bhdf-halted(y)]
+ [y∈bag-map(λP.(fst(P(u)));hdfs2 + bag-map(X;snd(X2(u))))|¬bhdf-halted(y)])
∈ bag(hdataflow(A;C))
BY
{ InstLemma `bag-filter-append` [] }
1
1. A : Type
2. B : Type
3. C : Type
4. valueall-type(B)
5. valueall-type(C)
6. u : A@i
7. v : A List@i
8. ∀X1,X2:hdataflow(A;B). ∀X:B ─→ hdataflow(A;C). ∀hdfs1,hdfs2:bag(hdataflow(A;C)).
hdf-halted(X1 (hdfs1) >>= X || X2 (hdfs2) >>= X*(v)) = hdf-halted(X1 || X2 (hdfs1 + hdfs2) >>= X*(v))@i
9. X1 : hdataflow(A;B)@i
10. X2 : hdataflow(A;B)@i
11. X : B ─→ hdataflow(A;C)@i
12. hdfs1 : bag(hdataflow(A;C))@i
13. hdfs2 : bag(hdataflow(A;C))@i
14. ¬((↑hdf-halted(X1 (hdfs1) >>= X)) ∧ (↑hdf-halted(X2 (hdfs2) >>= X)))
15. v2 : hdataflow(A;C)@i
16. v3 : bag(C)@i
17. fst(X1(u)) ([y∈bag-map(λP.(fst(P(u)));hdfs1 + bag-map(X;snd(X1(u))))|¬bhdf-halted(y)]) >>= X = v2 ∈ hdataflow(A;C)
18. ∪p∈bag-map(λP.P(u);hdfs1 + bag-map(X;snd(X1(u)))).snd(p) = v3 ∈ bag(C)
19. v5 : hdataflow(A;C)@i
20. v6 : bag(C)@i
21. fst(X2(u)) ([y∈bag-map(λP.(fst(P(u)));hdfs2 + bag-map(X;snd(X2(u))))|¬bhdf-halted(y)]) >>= X = v5 ∈ hdataflow(A;C)
22. ∪p∈bag-map(λP.P(u);hdfs2 + bag-map(X;snd(X2(u)))).snd(p) = v6 ∈ bag(C)
23. ∀[p,as,bs:Top]. ([x∈as + bs|p[x]] ~ [x∈as|p[x]] + [x∈bs|p[x]])
⊢ [y∈bag-map(λP.(fst(P(u)));(hdfs1 + hdfs2) + bag-map(X;(snd(X1(u))) + (snd(X2(u)))))|¬bhdf-halted(y)]
= ([y∈bag-map(λP.(fst(P(u)));hdfs1 + bag-map(X;snd(X1(u))))|¬bhdf-halted(y)]
+ [y∈bag-map(λP.(fst(P(u)));hdfs2 + bag-map(X;snd(X2(u))))|¬bhdf-halted(y)])
∈ bag(hdataflow(A;C))
Latex:
Latex:
.....equality.....
1. A : Type
2. B : Type
3. C : Type
4. valueall-type(B)
5. valueall-type(C)
6. u : A@i
7. v : A List@i
8. \mforall{}X1,X2:hdataflow(A;B). \mforall{}X:B {}\mrightarrow{} hdataflow(A;C). \mforall{}hdfs1,hdfs2:bag(hdataflow(A;C)).
hdf-halted(X1 (hdfs1) >>= X || X2 (hdfs2) >>= X*(v)) = hdf-halted(X1 || X2 (hdfs1 + hdfs2) >>= \000CX*(v))@i
9. X1 : hdataflow(A;B)@i
10. X2 : hdataflow(A;B)@i
11. X : B {}\mrightarrow{} hdataflow(A;C)@i
12. hdfs1 : bag(hdataflow(A;C))@i
13. hdfs2 : bag(hdataflow(A;C))@i
14. \mneg{}((\muparrow{}hdf-halted(X1 (hdfs1) >>= X)) \mwedge{} (\muparrow{}hdf-halted(X2 (hdfs2) >>= X)))
15. v2 : hdataflow(A;C)@i
16. v3 : bag(C)@i
17. fst(X1(u)) ([y\mmember{}bag-map(\mlambda{}P.(fst(P(u)));hdfs1 + bag-map(X;snd(X1(u))))|\mneg{}\msubb{}hdf-halted(y)]) >>= X = v\000C2
18. \mcup{}p\mmember{}bag-map(\mlambda{}P.P(u);hdfs1 + bag-map(X;snd(X1(u)))).snd(p) = v3
19. v5 : hdataflow(A;C)@i
20. v6 : bag(C)@i
21. fst(X2(u)) ([y\mmember{}bag-map(\mlambda{}P.(fst(P(u)));hdfs2 + bag-map(X;snd(X2(u))))|\mneg{}\msubb{}hdf-halted(y)]) >>= X = v\000C5
22. \mcup{}p\mmember{}bag-map(\mlambda{}P.P(u);hdfs2 + bag-map(X;snd(X2(u)))).snd(p) = v6
\mvdash{} [y\mmember{}bag-map(\mlambda{}P.(fst(P(u)));(hdfs1 + hdfs2) + bag-map(X;(snd(X1(u))) + (snd(X2(u)))))|
\mneg{}\msubb{}hdf-halted(y)]
= ([y\mmember{}bag-map(\mlambda{}P.(fst(P(u)));hdfs1 + bag-map(X;snd(X1(u))))|\mneg{}\msubb{}hdf-halted(y)]
+ [y\mmember{}bag-map(\mlambda{}P.(fst(P(u)));hdfs2 + bag-map(X;snd(X2(u))))|\mneg{}\msubb{}hdf-halted(y)])
By
Latex:
InstLemma `bag-filter-append` []
Home
Index