---

Step * 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
⊢ hdf-single-valued(inl x;A;B ─→ B)
⇒ (let X',fs = x a 
    in let b' ←─ if bag-null(fs) then X2 else sv-bag-only(fs) X2 fi 
       in <<X', b'>, {b'}> ∈ {X:hdataflow(A;B ─→ B)| hdf-single-valued(X;A;B ─→ B)}  × B × bag(B))
BY
{ (Fold `hdf-run` 0
   THEN (D 0 THENA Auto)
   THEN Unfold `hdf-single-valued` (-1)
   THEN (InstHyp [⌈[]⌉] (-1)⋅ THENA Auto)
   THEN RepUR ``hdf-run`` (-1)
   THEN (InstHyp [⌈a⌉] (-1)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenApply (-3) THENA Auto)
   THEN DVar `z'
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN (BoolCase ⌈bag-null(z2)⌉⋅ THENA Auto)) }

1
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)

2
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)

---

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
\mvdash{}  hdf-single-valued(inl  x;A;B  {}\mrightarrow{}  B)
{}\mRightarrow{}  (let  X',fs  =  x  a 
        in  let  b'  \mleftarrow{}{}  if  bag-null(fs)  then  X2  else  sv-bag-only(fs)  X2  fi 
              in  <<X',  b'>,  \{b'\}>  \mmember{}  \{X:hdataflow(A;B  {}\mrightarrow{}  B)|  hdf-single-valued(X;A;B  {}\mrightarrow{}  B)\}    \mtimes{}  B  \mtimes{}  bag(B))


By

(Fold  `hdf-run`  0
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `hdf-single-valued`  (-1)
  THEN  (InstHyp  [\mkleeneopen{}[]\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  RepUR  ``hdf-run``  (-1)
  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenApply  (-3)  THENA  Auto)
  THEN  DVar  `z'
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}bag-null(z2)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index