---

Step * of Lemma hdf-state-single-val_wf

∀[A,B:Type]. ∀[X:hdataflow(A;B ─→ B)]. ∀[b:B].
  (hdf-state-single-val(X;b) ∈ hdataflow(A;B)) supposing (hdf-single-valued(X;A;B ─→ B) and valueall-type(B))
BY
{ (Auto
   THEN Unfold `hdf-state-single-val` 0
   THEN Using [`S',⌈{X:hdataflow(A;B ─→ B)| hdf-single-valued(X;A;B ─→ B)}  × B⌉] MemCD⋅
   THEN Try (QuickAuto)
   THEN DVar `Xb'
   THEN Reduce 0
   THEN DVarSets
   THEN RepUR ``hdf-ap`` 0
   THEN MoveToConcl (-3)
   THEN HDataflowHD (-3)
   THEN Reduce 0
   THEN Try (QuickAuto)) }

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

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. y : Unit@i
⊢ hdf-single-valued(inr y ;A;B ─→ B) ⇒ (let b' ←─ X2 in <<inr ⋅ , b'>, {b'}> ∈ {X:hdataflow(A;B ─→ B)| hdf-single-value\000Cd(X;A;B ─→ B)}  × B × bag(B))

---

Latex:


\mforall{}[A,B:Type].  \mforall{}[X:hdataflow(A;B  {}\mrightarrow{}  B)].  \mforall{}[b:B].
    (hdf-state-single-val(X;b)  \mmember{}  hdataflow(A;B))  supposing 
          (hdf-single-valued(X;A;B  {}\mrightarrow{}  B)  and 
          valueall-type(B))


By

(Auto
  THEN  Unfold  `hdf-state-single-val`  0
  THEN  Using  [`S',\mkleeneopen{}\{X:hdataflow(A;B  {}\mrightarrow{}  B)|  hdf-single-valued(X;A;B  {}\mrightarrow{}  B)\}    \mtimes{}  B\mkleeneclose{}]  MemCD\mcdot{}
  THEN  Try  (QuickAuto)
  THEN  DVar  `Xb'
  THEN  Reduce  0
  THEN  DVarSets
  THEN  RepUR  ``hdf-ap``  0
  THEN  MoveToConcl  (-3)
  THEN  HDataflowHD  (-3)
  THEN  Reduce  0
  THEN  Try  (QuickAuto))

---

Home Index