---

Step * 2 1 2 1 2 1 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)
⊢ ∀L:A List. ∀a:A. ∀ys:bag({x:hdataflow(A;C)| ↑hdf-halted(x)} ).
    ({} = (snd(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<hdf-halt(), ys>)*(L)(a))) ∈ bag(C))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN RecUnfold `mk-hdf` 0
   THEN RepUR ``hdf-ap hdf-run`` 0
   THEN Try (Fold `hdf-ap` 0)
   THEN (RepUR ``simple-bind-nxt`` 0
         THEN Fold `simple-bind-nxt` 0
         THEN (Assert λP.P(a) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C)) BY
                     Auto)
         THEN Try ((Assert λP.P(u) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C)) BY Auto))
         THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto)⋅)
         THEN Reduce 0
         THEN Try (BHyp -5 ))⋅) }

1
1. A : Type
2. B : Type
3. C : Type
4. Y : B ⟶ hdataflow(A;C)
5. valueall-type(C)
6. a : A@i
7. ys : bag({x:hdataflow(A;C)| ↑hdf-halted(x)} )@i
8. λP.P(a) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C))
⊢ {} = ⋃yb∈bag-map(λP.P(a);ys + {}).snd(yb) ∈ bag(C)

2
.....wf..... 
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. ∀a:A. ∀ys:bag({x:hdataflow(A;C)| ↑hdf-halted(x)} ).
     ({} = (snd(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<hdf-halt(), ys>)*(v)(a))) ∈ bag(C))@i
9. a : A@i
10. ys : bag({x:hdataflow(A;C)| ↑hdf-halted(x)} )@i
11. λP.P(a) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C))
12. λP.P(u) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C))
⊢ a ∈ A

3
.....wf..... 
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. ∀a:A. ∀ys:bag({x:hdataflow(A;C)| ↑hdf-halted(x)} ).
     ({} = (snd(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<hdf-halt(), ys>)*(v)(a))) ∈ bag(C))@i
9. a : A@i
10. ys : bag({x:hdataflow(A;C)| ↑hdf-halted(x)} )@i
11. λP.P(a) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C))
12. λP.P(u) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C))
⊢ bag-map(λyb.(fst(yb));bag-map(λP.P(u);ys + {})) ∈ bag({x:hdataflow(A;C)| ↑hdf-halted(x)} )

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  Y  :  B  {}\mrightarrow{}  hdataflow(A;C)
5.  valueall-type(C)
\mvdash{}  \mforall{}L:A  List.  \mforall{}a:A.  \mforall{}ys:bag(\{x:hdataflow(A;C)|  \muparrow{}hdf-halted(x)\}  ).
        (\{\}  =  (snd(mk-hdf(p,a.simple-bind-nxt(Y;  p;  a);p.let  X,ys  =  p  in  ff;<hdf-halt(),  ys>)*(L)(a))))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  RecUnfold  `mk-hdf`  0
  THEN  RepUR  ``hdf-ap  hdf-run``  0
  THEN  Try  (Fold  `hdf-ap`  0)
  THEN  (RepUR  ``simple-bind-nxt``  0
              THEN  Fold  `simple-bind-nxt`  0
              THEN  (Assert  \mlambda{}P.P(a)  \mmember{}  hdataflow(A;C)  {}\mrightarrow{}  (hdataflow(A;C)  \mtimes{}  bag(C))  BY
                                      Auto)
              THEN  Try  ((Assert  \mlambda{}P.P(u)  \mmember{}  hdataflow(A;C)  {}\mrightarrow{}  (hdataflow(A;C)  \mtimes{}  bag(C))  BY  Auto))
              THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto)\mcdot{})
              THEN  Reduce  0
              THEN  Try  (BHyp  -5  ))\mcdot{})

---

Home Index