---

Step * of Lemma class-output-support-no-repeats

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[bg:bag(E)].
  (bag-no-repeats(E;class-output-support(es;bg))) supposing 
     (bag-no-repeats(E;bg) and 
     (∀e1,e2:E.  (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2)))))
BY
{ ((UnivCD THENA Auto)
   THEN (BagToList 3 THENA Auto)
   THEN All (RepUR ``bag-no-repeats``)
   THEN SquashExRepD
   THEN (RevHypSubst' (-2) 0 THENA Auto)
   THEN (RevHypSubst' (-2) (-4) THENA Auto)
   THEN ThinVar `bg'
   THEN RepUR ``class-output-support bag-combine bag-union bag-map`` 0
   THEN D 0
   THEN (InstConcl [⌈concat(map(λe.≤loc(e);L))⌉]⋅ THENA Auto)
   THEN Auto
   THEN Auto) }

1
1. Info : Type
2. es : EO+(Info)
3. L : E List
4. no_repeats(E;L)
5. ∀e1,e2:E.  (e1 ↓∈ L ⇒ e2 ↓∈ L ⇒ (¬(e1 <loc e2)))
6. concat(map(λe.≤loc(e);L)) = concat(map(λe.≤loc(e);L)) ∈ bag(E)
⊢ no_repeats(E;concat(map(λe.≤loc(e);L)))

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[bg:bag(E)].
    (bag-no-repeats(E;class-output-support(es;bg)))  supposing 
          (bag-no-repeats(E;bg)  and 
          (\mforall{}e1,e2:E.    (e1  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  e2  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2)))))


By

((UnivCD  THENA  Auto)
  THEN  (BagToList  3  THENA  Auto)
  THEN  All  (RepUR  ``bag-no-repeats``)
  THEN  SquashExRepD
  THEN  (RevHypSubst'  (-2)  0  THENA  Auto)
  THEN  (RevHypSubst'  (-2)  (-4)  THENA  Auto)
  THEN  ThinVar  `bg'
  THEN  RepUR  ``class-output-support  bag-combine  bag-union  bag-map``  0
  THEN  D  0
  THEN  (InstConcl  [\mkleeneopen{}concat(map(\mlambda{}e.\mleq{}loc(e);L))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Auto
  THEN  Auto)

---

Home Index