---

Step * 1 2 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. ¬(z2 = {} ∈ bag(B ─→ B))
15. (x a) = <z1, z2> ∈ (hdataflow(A;B ─→ B) × bag(B ─→ B))@i
16. single-valued-bag(z2;B ─→ B)@i
⊢ let b' ←─ sv-bag-only(z2) X2
  in <<z1, b'>, {b'}> ∈ {X:hdataflow(A;B ─→ B)| hdf-single-valued(X;A;B ─→ B)}  × B × bag(B)
BY
{ ((Assert ⌈0 < #(z2)⌉⋅
    THENA (SupposeNot
           THEN (Assert ⌈#(z2) = 0 ∈ ℤ⌉⋅ THENA Auto')
           THEN FLemma `bag-size-is-zero` [-1]
           THEN Auto
           THEN D (-6)
           THEN RWO "-1" 0
           THEN Auto)
    )
   THEN (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]⌉] (-9)⋅ 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.  \mneg{}(z2  =  \{\})
15.  (x  a)  =  <z1,  z2>@i
16.  single-valued-bag(z2;B  {}\mrightarrow{}  B)@i
\mvdash{}  let  b'  \mleftarrow{}{}  sv-bag-only(z2)  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

((Assert  \mkleeneopen{}0  <  \#(z2)\mkleeneclose{}\mcdot{}
    THENA  (SupposeNot
                  THEN  (Assert  \mkleeneopen{}\#(z2)  =  0\mkleeneclose{}\mcdot{}  THENA  Auto')
                  THEN  FLemma  `bag-size-is-zero`  [-1]
                  THEN  Auto
                  THEN  D  (-6)
                  THEN  RWO  "-1"  0
                  THEN  Auto)
    )
  THEN  (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{}]  (-9)\mcdot{}  THENA  Auto)
  THEN  RepUR  ``hdf-run  hdf-ap``  (-1)
  THEN  Trivial)

---

Home Index