---

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


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


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