---

Step * 1 of Lemma class-output-support-no_repeats


1. Info : Type
2. T : Type
3. es : EO+(Info)
4. bg : bag(E)
5. ∀e1,e2:E.  (e2 ↓∈ bg ⇒ e1 ↓∈ bg ⇒ (¬(e1 <loc e2)))
6. bag-no-repeats(E;bg)
⊢ bag-no-repeats(E;class-output-support(es;bg))
BY
{ (Unfold `class-output-support` 0
   THEN Unfold `bag-no-repeats` (-1)
   THEN D (-1)
   THEN (Unhide THENA Auto)
   THEN ExRepD
   THEN (RevHypSubst' (-2) 0 THENA Auto)
   THEN (RevHypSubst' (-2) (-4) THENA Auto)
   THEN ThinVar `bg'
   THEN Unfold `bag-no-repeats` 0
   THEN D 0
   THEN (InstConcl [⌈concat(map(λe.≤loc(e);L))⌉]⋅
         THENA (Auto
                THEN (InstLemma `bag-combine_wf` [⌈E⌉;⌈E⌉;⌈L⌉;⌈λe.≤loc(e)⌉]⋅ THENA Auto)
                THEN RepUR ``so_apply`` (-1)
                THEN Auto)
         )
   THEN RepUR ``bag-combine bag-union bag-map`` 0
   THEN Auto
   THEN Thin (-1))⋅ }

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

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  es  :  EO+(Info)
4.  bg  :  bag(E)
5.  \mforall{}e1,e2:E.    (e2  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  e1  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2)))
6.  bag-no-repeats(E;bg)
\mvdash{}  bag-no-repeats(E;class-output-support(es;bg))


By

(Unfold  `class-output-support`  0
  THEN  Unfold  `bag-no-repeats`  (-1)
  THEN  D  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  ExRepD
  THEN  (RevHypSubst'  (-2)  0  THENA  Auto)
  THEN  (RevHypSubst'  (-2)  (-4)  THENA  Auto)
  THEN  ThinVar  `bg'
  THEN  Unfold  `bag-no-repeats`  0
  THEN  D  0
  THEN  (InstConcl  [\mkleeneopen{}concat(map(\mlambda{}e.\mleq{}loc(e);L))\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  (InstLemma  `bag-combine\_wf`  [\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}\mlambda{}e.\mleq{}loc(e)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  RepUR  ``so\_apply``  (-1)
                            THEN  Auto)
              )
  THEN  RepUR  ``bag-combine  bag-union  bag-map``  0
  THEN  Auto
  THEN  Thin  (-1))\mcdot{}

---

Home Index