---

Step * of Lemma hdf-state1-single-val_wf

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

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

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

---

Latex:


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


By

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

---

Home Index