---

Step * 1 1 1 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
11. λP.P(a) ∈ hdataflow(A;C) ─→ (hdataflow(A;C) × bag(C))
⊢ {} = ∪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 (Assert [y∈ys2|¬bhdf-halted(y)] = {} ∈ bag(hdataflow(A;C)) BY
               Auto)
   THEN (FLemma `equal-empty-bag` [-1] THENA Auto)
   THEN HypSubst' (-1) 0
   THEN RepeatFor 2 (Thin (-1))
   THEN (RWO "bag-append-empty" 0 THENA Auto))⋅ }

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))
12. ([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) ∈ 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
11.  \mlambda{}P.P(a)  \mmember{}  hdataflow(A;C)  {}\mrightarrow{}  (hdataflow(A;C)  \mtimes{}  bag(C))
\mvdash{}  \{\}  =  \mcup{}yb\mmember{}bag-map(\mlambda{}P.P(a);ys2).snd(yb)


By

((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  (Assert  [y\mmember{}ys2|\mneg{}\msubb{}hdf-halted(y)]  =  \{\}  BY
                          Auto)
  THEN  (FLemma  `equal-empty-bag`  [-1]  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  (RWO  "bag-append-empty"  0  THENA  Auto))\mcdot{}

---

Home Index