---

Step * 1 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. ∀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)
BY
{ (SimpEqPairs
   THEN (RevHypSubst' (-1) 0 THENA Auto)
   THEN (Subst ⌈(snd((x a))) = (snd(pr i*(L)(a))) ∈ bag(A)⌉ 0⋅
         THENA (Auto THEN (HypSubst' (-6) 0 THENA Auto) THEN RepUR ``hdf-ap`` 0 THEN Auto)
         )
   THEN (InstLemma `list2extended-eo` [⌈Info⌉;⌈L @ [a]⌉;⌈i⌉]⋅
         THENA (Auto
                THEN MemTypeCD
                THEN Auto
                THEN RWO "length-append" 0
                THEN Reduce 0
                THEN Auto
                THEN RW assert_pushdownC 0
                THEN Auto')
         )
   THEN ExRepD
   THEN RepUR ``es-le-before`` (-1)
   THEN (RWO "map_append_sq" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN (InstLemma `general-append-cancellation` [⌈Info⌉;⌈L⌉;⌈map(λe.info(e);before(e))⌉;⌈[a]⌉;⌈[info(e)]⌉]⋅
         THENA (Auto THEN Reduce 0 THEN OrRight THEN Auto)
         )
   THEN RepD
   THEN (Assert ⌈a = info(e) ∈ Info⌉⋅ THENA Auto)
   THEN HypSubst' (-3) 0
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN RevHypSubst' (-5) 0
   THEN RWO "5<" 0
   THEN Auto
   THEN RepUR ``class-ap`` 0
   THEN BLemma `single-valued-classrel-all-implies-bag`
   THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  X  :  EClass(A)@i'
4.  pr  :  Id  {}\mrightarrow{}  hdataflow(Info;A)@i'
5.  \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
12.  z1  :  hdataflow(Info;A)@i
13.  z2  :  bag(A)@i
14.  (x  a)  =  <z1,  z2>@i
\mvdash{}  single-valued-bag(z2;A)


By

---

Latex:
(SimpEqPairs
  THEN  (RevHypSubst'  (-1)  0  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}(snd((x  a)))  =  (snd(pr  i*(L)(a)))\mkleeneclose{}  0\mcdot{}
              THENA  (Auto  THEN  (HypSubst'  (-6)  0  THENA  Auto)  THEN  RepUR  ``hdf-ap``  0  THEN  Auto)
              )
  THEN  (InstLemma  `list2extended-eo`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}L  @  [a]\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  RWO  "length-append"  0
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  RW  assert\_pushdownC  0
                            THEN  Auto')
              )
  THEN  ExRepD
  THEN  RepUR  ``es-le-before``  (-1)
  THEN  (RWO  "map\_append\_sq"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  (InstLemma  `general-append-cancellation`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}map(\mlambda{}e.info(e);before(e))\mkleeneclose{};\mkleeneopen{}[a]\mkleeneclose{};
              \mkleeneopen{}[info(e)]\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Reduce  0  THEN  OrRight  THEN  Auto)
              )
  THEN  RepD
  THEN  (Assert  \mkleeneopen{}a  =  info(e)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-3)  0
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  RevHypSubst'  (-5)  0
  THEN  RWO  "5<"  0
  THEN  Auto
  THEN  RepUR  ``class-ap``  0
  THEN  BLemma  `single-valued-classrel-all-implies-bag`
  THEN  Auto)

---

Home Index