---

Step * 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. X : hdataflow(A;B)@i
7. ys2 : bag(hdataflow(A;C))@i
8. a : A@i
9. {} = [y∈ys2|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))
10. ↑hdf-halted(X)
⊢ (snd(hdf-halt()(a)))
= (snd(hdf-run(λa.let s1,b = simple-bind-nxt(Y; <X, ys2>; a) 
                  in <mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;s1), b>)(a)))
∈ bag(C)
BY
{ (MoveToConcl (-1) THEN (HDataflowHD 6 THENA Auto) THEN RepUR ``hdf-ap hdf-run hdf-halted hdf-halt`` 0 THEN Auto) }

1
1. A : Type
2. B : Type
3. C : Type
4. Y : B ─→ hdataflow(A;C)
5. valueall-type(C)
6. ys2 : bag(hdataflow(A;C))@i
7. a : A@i
8. {} = [y∈ys2|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))
9. y : Unit@i
10. True@i
⊢ {}
= (snd(let s1,b = simple-bind-nxt(Y; <inr y , ys2>; a) 
       in <mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;s1), b>))
∈ bag(C)

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  Y  :  B  {}\mrightarrow{}  hdataflow(A;C)
5.  valueall-type(C)
6.  X  :  hdataflow(A;B)@i
7.  ys2  :  bag(hdataflow(A;C))@i
8.  a  :  A@i
9.  \{\}  =  [y\mmember{}ys2|\mneg{}\msubb{}hdf-halted(y)]
10.  \muparrow{}hdf-halted(X)
\mvdash{}  (snd(hdf-halt()(a)))
=  (snd(hdf-run(\mlambda{}a.let  s1,b  =  simple-bind-nxt(Y;  <X,  ys2>  a) 
                                    in  <mk-hdf(p,a.simple-bind-nxt(Y;  p;  a);p.let  X,ys  =  p  in  ff;s1),  b>)(a)))


By

(MoveToConcl  (-1)
  THEN  (HDataflowHD  6  THENA  Auto)
  THEN  RepUR  ``hdf-ap  hdf-run  hdf-halted  hdf-halt``  0
  THEN  Auto)

---

Home Index