---

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


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)
BY
{ ((GenApply (-3) THENA Auto)
   THEN DVar `z'
   THEN Reduce 0
   THEN Auto
   THEN Unhide
   THEN Try (Complete ((Unfold `single-valued-bag` 0 THEN Auto)))) }

1
1. Info : Type
2. A : Type
3. X : EClass(A)@i'
4. pr : Id ─→ hdataflow(Info;A)@i'
5. ∀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
12. z1 : hdataflow(Info;A)@i
13. z2 : bag(A)@i
14. (x a) = <z1, z2> ∈ (hdataflow(Info;A) × bag(A))@i
⊢ single-valued-bag(z2;A)

---

Latex:

---

Latex:

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


By

---

Latex:
((GenApply  (-3)  THENA  Auto)
  THEN  DVar  `z'
  THEN  Reduce  0
  THEN  Auto
  THEN  Unhide
  THEN  Try  (Complete  ((Unfold  `single-valued-bag`  0  THEN  Auto))))

---

Home Index