---

Step * 1 1 of Lemma hdf-state-single-val_wf


1. A : Type
2. B : Type
3. X : hdataflow(A;B ─→ B)
4. b : B
5. valueall-type(B)
6. hdf-single-valued(X;A;B ─→ B)
7. X2 : B@i
8. a : A@i
9. x : A ─→ (hdataflow(A;B ─→ B) × bag(B ─→ B))@i
10. ∀L:A List. case hdf-run(x)*(L) of inl(P) => ∀a:A. let X',b = P a in single-valued-bag(b;B ─→ B) | inr(z) => True@i
11. ∀a:A. let X',b = x a in single-valued-bag(b;B ─→ B)
12. z1 : hdataflow(A;B ─→ B)@i
13. z2 : bag(B ─→ B)@i
14. (x a) = <z1, z2> ∈ (hdataflow(A;B ─→ B) × bag(B ─→ B))@i
15. single-valued-bag(z2;B ─→ B)@i
16. z2 = {} ∈ bag(B ─→ B)
⊢ let b' ←─ X2
  in <<z1, b'>, {b'}> ∈ {X:hdataflow(A;B ─→ B)| hdf-single-valued(X;A;B ─→ B)}  × B × bag(B)
BY
{ ((CallByValueReduce 0 THENA Auto)
   THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))
   THEN MemTypeCD
   THEN Try (Complete (Auto))
   THEN (Subst ⌈z1 = (fst((x a))) ∈ hdataflow(A;B ─→ B)⌉ 0⋅ THENA Auto)
   THEN Unfold `hdf-single-valued` 0
   THEN Auto
   THEN (InstHyp [⌈[a / L]⌉] (-8)⋅ THENA Auto)
   THEN RepUR ``hdf-run hdf-ap`` (-1)
   THEN Trivial) }

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  X  :  hdataflow(A;B  {}\mrightarrow{}  B)
4.  b  :  B
5.  valueall-type(B)
6.  hdf-single-valued(X;A;B  {}\mrightarrow{}  B)
7.  X2  :  B@i
8.  a  :  A@i
9.  x  :  A  {}\mrightarrow{}  (hdataflow(A;B  {}\mrightarrow{}  B)  \mtimes{}  bag(B  {}\mrightarrow{}  B))@i
10.  \mforall{}L:A  List
            case  hdf-run(x)*(L)
              of  inl(P)  =>
              \mforall{}a:A.  let  X',b  =  P  a  in  single-valued-bag(b;B  {}\mrightarrow{}  B)
              |  inr(z)  =>
              True@i
11.  \mforall{}a:A.  let  X',b  =  x  a  in  single-valued-bag(b;B  {}\mrightarrow{}  B)
12.  z1  :  hdataflow(A;B  {}\mrightarrow{}  B)@i
13.  z2  :  bag(B  {}\mrightarrow{}  B)@i
14.  (x  a)  =  <z1,  z2>@i
15.  single-valued-bag(z2;B  {}\mrightarrow{}  B)@i
16.  z2  =  \{\}
\mvdash{}  let  b'  \mleftarrow{}{}  X2
    in  <<z1,  b'>,  \{b'\}>  \mmember{}  \{X:hdataflow(A;B  {}\mrightarrow{}  B)|  hdf-single-valued(X;A;B  {}\mrightarrow{}  B)\}    \mtimes{}  B  \mtimes{}  bag(B)


By

((CallByValueReduce  0  THENA  Auto)
  THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  MemTypeCD
  THEN  Try  (Complete  (Auto))
  THEN  (Subst  \mkleeneopen{}z1  =  (fst((x  a)))\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Unfold  `hdf-single-valued`  0
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}[a  /  L]\mkleeneclose{}]  (-8)\mcdot{}  THENA  Auto)
  THEN  RepUR  ``hdf-run  hdf-ap``  (-1)
  THEN  Trivial)

---

Home Index