---

Step * 1 of Lemma rec-bind-nxt_wf


1. A : Type
2. B : Type
3. C : Type
4. X : C ─→ hdataflow(A;B)
5. Y : C ─→ hdataflow(A;C)
6. p1 : bag(hdataflow(A;B))
7. p2 : bag(hdataflow(A;C))
8. a : A
9. valueall-type(C)
10. valueall-type(B)
11. Z : bag(hdataflow(A;C) × bag(C))@i
12. bag-map(λp.p(a);p2) = Z ∈ bag(hdataflow(A;C) × bag(C))@i
13. V : bag(hdataflow(A;B) × bag(B))@i
14. bag-map(λp.p(a);p1 + bag-map(X;∪x∈Z.snd(x))) = V ∈ bag(hdataflow(A;B) × bag(B))@i
15. W : bag(hdataflow(A;C))@i
16. bag-map(λx.(fst(Y x(a)));∪x∈Z.snd(x)) = W ∈ bag(hdataflow(A;C))@i
⊢ <<bag-mapfilter(λx.(fst(x));λx.isl(fst(x));V), bag-mapfilter(λx.(fst(x));λx.isl(fst(x));Z) + [p∈W|isl(p)]>
  , ∪x∈V.snd(x)
  > ∈ bag(hdataflow(A;B)) × bag(hdataflow(A;C)) × bag(B)
BY
{ (Fold `hdf-running` 0 THEN Auto) }

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  X  :  C  {}\mrightarrow{}  hdataflow(A;B)
5.  Y  :  C  {}\mrightarrow{}  hdataflow(A;C)
6.  p1  :  bag(hdataflow(A;B))
7.  p2  :  bag(hdataflow(A;C))
8.  a  :  A
9.  valueall-type(C)
10.  valueall-type(B)
11.  Z  :  bag(hdataflow(A;C)  \mtimes{}  bag(C))@i
12.  bag-map(\mlambda{}p.p(a);p2)  =  Z@i
13.  V  :  bag(hdataflow(A;B)  \mtimes{}  bag(B))@i
14.  bag-map(\mlambda{}p.p(a);p1  +  bag-map(X;\mcup{}x\mmember{}Z.snd(x)))  =  V@i
15.  W  :  bag(hdataflow(A;C))@i
16.  bag-map(\mlambda{}x.(fst(Y  x(a)));\mcup{}x\mmember{}Z.snd(x))  =  W@i
\mvdash{}  <<bag-mapfilter(\mlambda{}x.(fst(x));\mlambda{}x.isl(fst(x));V)
      ,  bag-mapfilter(\mlambda{}x.(fst(x));\mlambda{}x.isl(fst(x));Z)  +  [p\mmember{}W|isl(p)]
      >
    ,  \mcup{}x\mmember{}V.snd(x)
    >  \mmember{}  bag(hdataflow(A;B))  \mtimes{}  bag(hdataflow(A;C))  \mtimes{}  bag(B)


By

(Fold  `hdf-running`  0  THEN  Auto)

---

Home Index