---

Step * of Lemma class-output-support-no_repeats

∀[Info,T: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.  (e2 ↓∈ bg ⇒ e1 ↓∈ bg ⇒ (¬(e1 <loc e2)))))
BY
{ (UnivCD THENA Auto) }

1
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))

---

Latex:


\mforall{}[Info,T: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.    (e2  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  e1  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2)))))


By

(UnivCD  THENA  Auto)

---

Home Index