Step
*
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. 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. (↑bag-null(ys1)) ∧ (↑hdf-halted(X))
⊢ (snd(fst(mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) ∧b hdf-halted(X);<X, ys1>)(u))*(v)(a))) = (snd(fst(\000Cmk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)(u))*(v)(a))) ∈ bag(C)
BY
{ ((RW assert_pushdownC (-1) THENA Auto)
THEN RW (AddrC [2] (RecUnfoldC `mk-hdf`)) 0
THEN Reduce 0
THEN (SplitOnConclITE THENA Auto)
THEN ((D (-1) THEN Auto) THEN Subst' fst(hdf-halt()(u)) ~ hdf-halt() 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))
15. ↑hdf-halted(X)
16. ys1 = {} ∈ bag(hdataflow(A;C))
17. ↑hdf-halted(X)
⊢ fst(hdf-halt()(u)) ~ hdf-halt()
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))
15. ↑hdf-halted(X)
16. ys1 = {} ∈ bag(hdataflow(A;C))
17. ↑hdf-halted(X)
⊢ (snd(hdf-halt()*(v)(a))) = (snd(fst(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)(u))*(v)(a))) ∈ \000Cbag(C)
Latex:
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. (\muparrow{}bag-null(ys1)) \mwedge{} (\muparrow{}hdf-halted(X))
\mvdash{} (snd(fst(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>)(u))*\000C(v)(a))) = (snd(fst(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)(u))*(v)(a)))
By
Latex:
((RW assert\_pushdownC (-1) THENA Auto)
THEN RW (AddrC [2] (RecUnfoldC `mk-hdf`)) 0
THEN Reduce 0
THEN (SplitOnConclITE THENA Auto)
THEN ((D (-1) THEN Auto) THEN Subst' fst(hdf-halt()(u)) \msim{} hdf-halt() 0)\mcdot{})
Home
Index