---

Step * 2 2 2 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. 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)))) ∨ (¬↑hdf-halted(X))
15. v2 : hdataflow(A;B)@i
16. v3 : bag(B)@i
17. X(u) = <v2, v3> ∈ (hdataflow(A;B) × bag(B))@i
18. λP.P(u) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C))
⊢ (snd(fst(let s1,b = let ybs ⟵ bag-map(λP.P(u);ys1 + bag-map(Y;v3))
                      in let ys' ⟵ [y∈bag-map(λyb.(fst(yb));ybs)|¬bhdf-halted(y)]
                         in let out ⟵ ⋃yb∈ybs.snd(yb)
                            in <<v2, ys'>, out> 
           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>)*(v)(a)))
= (snd(fst(let s1,b = let ybs ⟵ bag-map(λP.P(u);ys2 + bag-map(Y;v3))
                      in let ys' ⟵ bag-map(λyb.(fst(yb));ybs)
                         in let out ⟵ ⋃yb∈ybs.snd(yb)
                            in <<v2, ys'>, out> 
           in <mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;s1), b>)*(v)(a)))
∈ bag(C)
BY
{ ((Assert [y∈bag-map(λyb.(fst(yb));bag-map(λP.P(u);ys1 + bag-map(Y;v3)))|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C)) BY
          (BLemma `bag-filter-wf3` THEN Auto))
   THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
   THEN Reduce 0
   THEN BackThruSomeHyp) }

1
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)))) ∨ (¬↑hdf-halted(X))
15. v2 : hdataflow(A;B)@i
16. v3 : bag(B)@i
17. X(u) = <v2, v3> ∈ (hdataflow(A;B) × bag(B))@i
18. λP.P(u) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C))
19. [y∈bag-map(λyb.(fst(yb));bag-map(λP.P(u);ys1 + bag-map(Y;v3)))|¬bhdf-halted(y)] ∈ bag(hdataflow(A;C))
⊢ [y∈bag-map(λyb.(fst(yb));bag-map(λP.P(u);ys1 + bag-map(Y;v3)))|¬bhdf-halted(y)]
= [y∈bag-map(λyb.(fst(yb));bag-map(λP.P(u);ys2 + bag-map(Y;v3)))|¬bhdf-halted(y)]
∈ bag(hdataflow(A;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.  (\mneg{}(ys1  =  \{\}))  \mvee{}  (\mneg{}\muparrow{}hdf-halted(X))
15.  v2  :  hdataflow(A;B)@i
16.  v3  :  bag(B)@i
17.  X(u)  =  <v2,  v3>@i
18.  \mlambda{}P.P(u)  \mmember{}  hdataflow(A;C)  {}\mrightarrow{}  (hdataflow(A;C)  \mtimes{}  bag(C))
\mvdash{}  (snd(fst(let  s1,b  =  let  ybs  \mleftarrow{}{}  bag-map(\mlambda{}P.P(u);ys1  +  bag-map(Y;v3))
                                            in  let  ys'  \mleftarrow{}{}  [y\mmember{}bag-map(\mlambda{}yb.(fst(yb));ybs)|\mneg{}\msubb{}hdf-halted(y)]
                                                  in  let  out  \mleftarrow{}{}  \mcup{}yb\mmember{}ybs.snd(yb)
                                                        in  <<v2,  ys'>,  out> 
                      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
                            >)*(v)(a)))
=  (snd(fst(let  s1,b  =  let  ybs  \mleftarrow{}{}  bag-map(\mlambda{}P.P(u);ys2  +  bag-map(Y;v3))
                                            in  let  ys'  \mleftarrow{}{}  bag-map(\mlambda{}yb.(fst(yb));ybs)
                                                  in  let  out  \mleftarrow{}{}  \mcup{}yb\mmember{}ybs.snd(yb)
                                                        in  <<v2,  ys'>,  out> 
                      in  <mk-hdf(p,a.simple-bind-nxt(Y;  p;  a);p.let  X,ys  =  p  in  ff;s1),  b>)*(v)(a)))


By

---

Latex:
((Assert  [y\mmember{}bag-map(\mlambda{}yb.(fst(yb));bag-map(\mlambda{}P.P(u);ys1  +  bag-map(Y;v3)))|\mneg{}\msubb{}hdf-halted(y)]
                  \mmember{}  bag(hdataflow(A;C))  BY
                (BLemma  `bag-filter-wf3`  THEN  Auto))
  THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto))
  THEN  Reduce  0
  THEN  BackThruSomeHyp)

---

Home Index