---

Step * 1 2 1 1 1 of Lemma iterate-hdf-bind-simple

.....subterm..... T:t
1:n
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
11. (¬(ys1 = {} ∈ bag(hdataflow(A;C)))) ∨ (¬↑hdf-halted(X))
12. v1 : hdataflow(A;B)@i
13. v2 : bag(B)@i
14. X(a) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
15. λP.P(a) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C))
16. ∀[ba,bb:bag(hdataflow(A;C) × bag(C))]. ∀[f:(hdataflow(A;C) × bag(C)) ⟶ bag(C)].
      (⋃x∈ba + bb.f[x] = (⋃x∈ba.f[x] + ⋃x∈bb.f[x]) ∈ bag(C))
⊢ ⋃yb∈bag-map(λP.P(a);ys1).snd(yb) = ⋃yb∈bag-map(λP.P(a);ys2).snd(yb) ∈ bag(C)
BY
{ ((InstLemma `bag-filter-split` [⌜hdataflow(A;C)⌝;⌜λ2y.hdf-halted(y)⌝;⌜ys2⌝]⋅ THENA Auto)
   THEN (RevHypSubst (-1) 0 THENA Auto)
   THEN (RWO "bag-map-append" 0 THENA Auto)
   THEN RWO "-2" 0
   THEN Auto
   THEN Subst ⌜⋃yb∈bag-map(λP.P(a);[x∈ys2|hdf-halted(x)]).snd(yb) ~ {}⌝ 0⋅
   THEN Try ((Reduce 0 THEN EqCD THEN Auto))) }

1
.....equality..... 
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
11. (¬(ys1 = {} ∈ bag(hdataflow(A;C)))) ∨ (¬↑hdf-halted(X))
12. v1 : hdataflow(A;B)@i
13. v2 : bag(B)@i
14. X(a) = <v1, v2> ∈ (hdataflow(A;B) × bag(B))@i
15. λP.P(a) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C))
16. ∀[ba,bb:bag(hdataflow(A;C) × bag(C))]. ∀[f:(hdataflow(A;C) × bag(C)) ⟶ bag(C)].
      (⋃x∈ba + bb.f[x] = (⋃x∈ba.f[x] + ⋃x∈bb.f[x]) ∈ bag(C))
17. ([x∈ys2|hdf-halted(x)] + [x∈ys2|¬bhdf-halted(x)]) = ys2 ∈ bag(hdataflow(A;C))
⊢ ⋃yb∈bag-map(λP.P(a);[x∈ys2|hdf-halted(x)]).snd(yb) ~ {}

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  Y  :  B  {}\mrightarrow{}  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\mmember{}ys2|\mneg{}\msubb{}hdf-halted(y)]@i
11.  (\mneg{}(ys1  =  \{\}))  \mvee{}  (\mneg{}\muparrow{}hdf-halted(X))
12.  v1  :  hdataflow(A;B)@i
13.  v2  :  bag(B)@i
14.  X(a)  =  <v1,  v2>@i
15.  \mlambda{}P.P(a)  \mmember{}  hdataflow(A;C)  {}\mrightarrow{}  (hdataflow(A;C)  \mtimes{}  bag(C))
16.  \mforall{}[ba,bb:bag(hdataflow(A;C)  \mtimes{}  bag(C))].  \mforall{}[f:(hdataflow(A;C)  \mtimes{}  bag(C))  {}\mrightarrow{}  bag(C)].
            (\mcup{}x\mmember{}ba  +  bb.f[x]  =  (\mcup{}x\mmember{}ba.f[x]  +  \mcup{}x\mmember{}bb.f[x]))
\mvdash{}  \mcup{}yb\mmember{}bag-map(\mlambda{}P.P(a);ys1).snd(yb)  =  \mcup{}yb\mmember{}bag-map(\mlambda{}P.P(a);ys2).snd(yb)


By

---

Latex:
((InstLemma  `bag-filter-split`  [\mkleeneopen{}hdataflow(A;C)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}y.hdf-halted(y)\mkleeneclose{};\mkleeneopen{}ys2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RevHypSubst  (-1)  0  THENA  Auto)
  THEN  (RWO  "bag-map-append"  0  THENA  Auto)
  THEN  RWO  "-2"  0
  THEN  Auto
  THEN  Subst  \mkleeneopen{}\mcup{}yb\mmember{}bag-map(\mlambda{}P.P(a);[x\mmember{}ys2|hdf-halted(x)]).snd(yb)  \msim{}  \{\}\mkleeneclose{}  0\mcdot{}
  THEN  Try  ((Reduce  0  THEN  EqCD  THEN  Auto)))

---

Home Index