---

Step * 1 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. 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)
BY
{ ((Assert λP.P(a) ∈ hdataflow(A;C) ─→ (hdataflow(A;C) × bag(C)) BY
          Auto)
   THEN RW (AddrC [3;1;1] (UnfoldC `simple-bind-nxt`)) 0
   THEN RepUR ``hdf-ap`` 0
   THEN Fold `hdf-ap` 0
   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. 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
11. λP.P(a) ∈ hdataflow(A;C) ─→ (hdataflow(A;C) × bag(C))
⊢ {} = ∪yb∈bag-map(λP.P(a);ys2 + {}).snd(yb) ∈ bag(C)

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  Y  :  B  {}\mrightarrow{}  hdataflow(A;C)
5.  valueall-type(C)
6.  ys2  :  bag(hdataflow(A;C))@i
7.  a  :  A@i
8.  \{\}  =  [y\mmember{}ys2|\mneg{}\msubb{}hdf-halted(y)]
9.  y  :  Unit@i
10.  True@i
\mvdash{}  \{\}
=  (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>))


By

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

---

Home Index