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. 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