---

Step * 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
⊢ hdf-single-valued(inl x;A;B)
⇒ (let X',xs = x a 
    in let b' ←─ if bag-null(xs) then X2 else f sv-bag-only(xs) X2 fi 
       in <<X', b'>, {b'}> ∈ {X:hdataflow(A;B)| hdf-single-valued(X;A;B)}  × C × bag(C))
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. 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)

2
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. ¬(z2 = {} ∈ bag(B))
17. (x a) = <z1, z2> ∈ (hdataflow(A;B) × bag(B))@i
18. single-valued-bag(z2;B)@i
⊢ let b' ←─ f sv-bag-only(z2) X2
  in <<z1, b'>, {b'}> ∈ {X:hdataflow(A;B)| hdf-single-valued(X;A;B)}  × C × bag(C)

---

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


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