---

Step * 2 1 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. ys1 = {} ∈ bag(hdataflow(A;C))
15. ↑hdf-halted(X)
16. ys1 = {} ∈ bag(hdataflow(A;C))
17. ↑hdf-halted(X)
⊢ (snd(hdf-halt()(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))) ∈ bag(\000CC)
BY
{ Subst ⌈snd(hdf-halt()(a)) ~ {}⌉ 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)
⊢ snd(hdf-halt()(a)) ~ {}

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(fst(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)(u))*(v)(a))) ∈ bag(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.  ys1  =  \{\}
15.  \muparrow{}hdf-halted(X)
16.  ys1  =  \{\}
17.  \muparrow{}hdf-halted(X)
\mvdash{}  (snd(hdf-halt()(a)))  =  (snd(fst(mk-hdf(p,a.simple-bind-nxt(Y;  p;  a);p.let  X,ys  =  p  in  ff;<X,  ys2>)\000C(u))*(v)(a)))


By

Subst  \mkleeneopen{}snd(hdf-halt()(a))  \msim{}  \{\}\mkleeneclose{}  0\mcdot{}

---

Home Index