---

Step * 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. 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
⊢ (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>)(a))) = (snd(mk-hdf(p,a.simpl\000Ce-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)(a))) ∈ bag(C)
BY
{ (RecUnfold `mk-hdf` 0 THEN Reduce 0 THEN (SplitOnConclITE THENA Auto)) }

1
.....truecase..... 
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-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)

2
.....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)

---

Latex:

---

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.  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
\mvdash{}  (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>)(a)))  =  (\000Csnd(mk-hdf(p,a.simple-bind-nxt(Y;  p;  a);p.let  X,ys  =  p  in  ff;<X,  ys2>)(a)))


By

---

Latex:
(RecUnfold  `mk-hdf`  0  THEN  Reduce  0  THEN  (SplitOnConclITE  THENA  Auto))

---

Home Index