---

Step * of Lemma iterate-hdf-bind-simple

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ⟶ hdataflow(A;C)].
  ∀[L:A List]. ∀[a:A].  ((snd(X >>= Y*(L)(a))) = (snd(simple-hdf-bind(X;Y)*(L)(a))) ∈ bag(C)) supposing valueall-type(C)
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN Unfolds ``hdf-bind simple-hdf-bind`` 0
   THEN Assert ⌜∀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>)*(L)(a)))\000C = (snd(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)*(L)(a))) ∈ bag(C)))⌝⋅
   THEN Try ((RWO "band_commutes" 0 THEN Auto THEN BHyp (-2) THEN Auto THEN Reduce 0 THEN Auto))
   THEN MoveToConcl (-4)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN Try ((DoSubsume THEN Complete (Auto))⋅)) }

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
⊢ (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)

2
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
⊢ (snd(fst(mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) ∧b hdf-halted(X);<X, ys1>)(u))*(v)(a))) = (snd(fst(\000Cmk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)(u))*(v)(a))) ∈ bag(C)

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:B  {}\mrightarrow{}  hdataflow(A;C)].
    \mforall{}[L:A  List].  \mforall{}[a:A].    ((snd(X  >>=  Y*(L)(a)))  =  (snd(simple-hdf-bind(X;Y)*(L)(a)))) 
    supposing  valueall-type(C)


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  Unfolds  ``hdf-bind  simple-hdf-bind``  0
  THEN  Assert  \mkleeneopen{}\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>)*(L)\000C(a)))
                                      =  (snd(mk-hdf(p,a.simple-bind-nxt(Y;  p;  a);p.let  X,ys  =  p 
                                                                                                                                in  ff;<X,  ys2>)*(L)(a)))))\mkleeneclose{}\mcdot{}
  THEN  Try  ((RWO  "band\_commutes"  0  THEN  Auto  THEN  BHyp  (-2)  THEN  Auto  THEN  Reduce  0  THEN  Auto))
  THEN  MoveToConcl  (-4)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Complete  (Auto))\mcdot{}))

---

Home Index