Step
*
2
2
2
1
1
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(λx.(fst(x(u)));ys1)|¬bhdf-halted(y)]
= [y∈bag-map(λx.(fst(x(u)));ys2)|¬bhdf-halted(y)]
∈ bag(hdataflow(A;C))
BY
{ ((InstLemma `bag-filter-split` [⌈hdataflow(A;C)⌉;⌈λ2y.hdf-halted(y)⌉;⌈ys2⌉]⋅ THENA Auto)
THEN (RevHypSubst (-1) 0 THENA (Auto THEN Try ((BLemma `bag-filter-wf3` THEN Auto))))⋅
THEN (RWW "bag-map-append bag-filter-append" 0 THENA Auto)⋅
THEN Subst ⌈[y∈bag-map(λx.(fst(x(u)));[x∈ys2|hdf-halted(x)])|¬bhdf-halted(y)] ~ {}⌉ 0⋅)⋅ }
1
.....equality.....
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))
20. ([x∈ys2|hdf-halted(x)] + [x∈ys2|¬bhdf-halted(x)]) = ys2 ∈ bag(hdataflow(A;C))
⊢ [y∈bag-map(λx.(fst(x(u)));[x∈ys2|hdf-halted(x)])|¬bhdf-halted(y)] ~ {}
2
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))
20. ([x∈ys2|hdf-halted(x)] + [x∈ys2|¬bhdf-halted(x)]) = ys2 ∈ bag(hdataflow(A;C))
⊢ [y∈bag-map(λx.(fst(x(u)));ys1)|¬bhdf-halted(y)]
= ({} + [y∈bag-map(λx.(fst(x(u)));[x∈ys2|¬bhdf-halted(x)])|¬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{}x.(fst(x(u)));ys1)|\mneg{}\msubb{}hdf-halted(y)] = [y\mmember{}bag-map(\mlambda{}x.(fst(x(u)));ys2)|\mneg{}\msubb{}hdf-halted(y)]
By
((InstLemma `bag-filter-split` [\mkleeneopen{}hdataflow(A;C)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}y.hdf-halted(y)\mkleeneclose{};\mkleeneopen{}ys2\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (RevHypSubst (-1) 0 THENA (Auto THEN Try ((BLemma `bag-filter-wf3` THEN Auto))))\mcdot{}
THEN (RWW "bag-map-append bag-filter-append" 0 THENA Auto)\mcdot{}
THEN Subst \mkleeneopen{}[y\mmember{}bag-map(\mlambda{}x.(fst(x(u)));[x\mmember{}ys2|hdf-halted(x)])|\mneg{}\msubb{}hdf-halted(y)] \msim{} \{\}\mkleeneclose{} 0\mcdot{})\mcdot{}
Home
Index