---

Step * 1 2 of Lemma iterate-hdf-bind-simple

.....falsecase..... 
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. ys1 : bag(hdataflow(A;C))@i
8. ys2 : bag(hdataflow(A;C))@i
9. a : A@i
10. ys1 = [y∈ys2|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))@i
11. (¬(ys1 = {} ∈ bag(hdataflow(A;C)))) ∨ (¬↑hdf-halted(X))
⊢ (snd(hdf-run(λa.let s1,b = bind-nxt(Y;<X, ys1>;a) 
                  in <mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) ∧b hdf-halted(X);s1), b>)(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
{ (RepUR ``hdf-ap hdf-run`` 0
   THEN (RW (AddrC [3;1;1] (UnfoldC `simple-bind-nxt`)) 0⋅ THEN Reduce 0)
   THEN RW (AddrC [2;1;1] (UnfoldC `bind-nxt`)) 0⋅
   THEN Reduce 0
   THEN GenConclAtAddr [2;1;1;1]
   THEN D -2
   THEN Reduce 0
   THEN (Assert λP.P(a) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C)) BY
               Auto)
   THEN Repeat ((CallByValueReduce 0 THENA Auto))
   THEN Reduce 0) }

1
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. ys1 : bag(hdataflow(A;C))@i
8. ys2 : bag(hdataflow(A;C))@i
9. a : A@i
10. ys1 = [y∈ys2|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))@i
11. (¬(ys1 = {} ∈ bag(hdataflow(A;C)))) ∨ (¬↑hdf-halted(X))
12. v1 : hdataflow(A;B)@i
13. v2 : bag(B)@i
14. X(a) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
15. λP.P(a) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C))
⊢ ⋃yb∈bag-map(λP.P(a);ys1 + bag-map(Y;v2)).snd(yb) = ⋃yb∈bag-map(λP.P(a);ys2 + bag-map(Y;v2)).snd(yb) ∈ bag(C)

---

Latex:

---

Latex:
.....falsecase..... 
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.  ys1  :  bag(hdataflow(A;C))@i
8.  ys2  :  bag(hdataflow(A;C))@i
9.  a  :  A@i
10.  ys1  =  [y\mmember{}ys2|\mneg{}\msubb{}hdf-halted(y)]@i
11.  (\mneg{}(ys1  =  \{\}))  \mvee{}  (\mneg{}\muparrow{}hdf-halted(X))
\mvdash{}  (snd(hdf-run(\mlambda{}a.let  s1,b  =  bind-nxt(Y;<X,  ys1>a) 
                                    in  <mk-hdf(p,a.bind-nxt(Y;p;a);p.let  X,ys  =  p 
                                                                                                      in  bag-null(ys)  \mwedge{}\msubb{}  hdf-halted(X);s1)
                                          ,  b
                                          >)(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

---

Latex:
(RepUR  ``hdf-ap  hdf-run``  0
  THEN  (RW  (AddrC  [3;1;1]  (UnfoldC  `simple-bind-nxt`))  0\mcdot{}  THEN  Reduce  0)
  THEN  RW  (AddrC  [2;1;1]  (UnfoldC  `bind-nxt`))  0\mcdot{}
  THEN  Reduce  0
  THEN  GenConclAtAddr  [2;1;1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  (Assert  \mlambda{}P.P(a)  \mmember{}  hdataflow(A;C)  {}\mrightarrow{}  (hdataflow(A;C)  \mtimes{}  bag(C))  BY
                          Auto)
  THEN  Repeat  ((CallByValueReduce  0  THENA  Auto))
  THEN  Reduce  0)

---

Home Index