---

Step * of Lemma single-valued-class-implies-hdf

∀[Info,A:Type].
  ∀X:EClass(A). ∀pr:LocalClass(X).
    (single-valued-classrel-all{i:l}(Info;A;X) ⇒ (∀i:Id. hdf-single-valued(pr i;Info;A)))
BY
{ (Auto
   THEN Unfold `hdf-single-valued` 0
   THEN Auto
   THEN D (-4)
   THEN GenConclAtAddr [1]
   THEN MoveToConcl (-1)
   THEN (HDataflowHD (-1) THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN Try (Complete ((Fold `hdf-run` 0 THEN Auto)))
   THEN Try (Complete ((DVar `y' THEN Fold `it` 0 THEN Fold `hdf-halt` 0 THEN Auto)))) }

1
1. [Info] : Type
2. [A] : Type
3. X : EClass(A)@i'
4. pr : Id ⟶ hdataflow(Info;A)@i'
5. [%2] : ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(pr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A))@i'
6. single-valued-classrel-all{i:l}(Info;A;X)@i'
7. i : Id@i
8. L : Info List@i
9. x : Info ⟶ (hdataflow(Info;A) × bag(A))@i
10. pr i*(L) = (inl x) ∈ hdataflow(Info;A)@i
11. a : Info@i
⊢ let X',b = x a 
  in single-valued-bag(b;A)

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].
    \mforall{}X:EClass(A).  \mforall{}pr:LocalClass(X).
        (single-valued-classrel-all\{i:l\}(Info;A;X)  {}\mRightarrow{}  (\mforall{}i:Id.  hdf-single-valued(pr  i;Info;A)))


By

---

Latex:
(Auto
  THEN  Unfold  `hdf-single-valued`  0
  THEN  Auto
  THEN  D  (-4)
  THEN  GenConclAtAddr  [1]
  THEN  MoveToConcl  (-1)
  THEN  (HDataflowHD  (-1)  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (Complete  ((Fold  `hdf-run`  0  THEN  Auto)))
  THEN  Try  (Complete  ((DVar  `y'  THEN  Fold  `it`  0  THEN  Fold  `hdf-halt`  0  THEN  Auto))))

---

Home Index