---

Step * of Lemma simple-loc-comb-1-concat-es-sv

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[F:Id ─→ A ─→ bag(Top)]. ∀[X:EClass(A)].
  es-sv-class(es;F@(Loc, X)) supposing (∀i:Id. ∀a:A.  (#(F i a) ≤ 1)) ∧ es-sv-class(es;X)
BY
{ ((UnivCD THENA MaAuto)
   THEN RepUR ``es-sv-class simple-loc-comb-1 simple-loc-comb concat-lifting-loc-1`` 0
   THEN RepUR ``concat-lifting1-loc concat-lifting-loc concat-lifting concat-lifting-list`` 0
   THEN Auto
   THEN RepeatFor 2 ((RecUnfold `lifting-gen-list-rev` 0 THEN Reduce 0))
   THEN Unfold `es-sv-class` (-2)
   THEN (InstHyp [⌈e⌉] (-2)⋅ THENA Auto)
   THEN (Assert ⌈(#(X es e) = 0 ∈ ℤ) ∨ (#(X es e) = 1 ∈ ℤ)⌉⋅ THENA Auto')
   THEN D (-1)) }

1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. F : Id ─→ A ─→ bag(Top)
5. X : EClass(A)
6. ∀i:Id. ∀a:A.  (#(F i a) ≤ 1)
7. ∀e:E. (#(X es e) ≤ 1)
8. e : E@i
9. #(X es e) ≤ 1
10. #(X es e) = 0 ∈ ℤ
⊢ #(bag-union(∪x∈X es e.{F loc(e) x})) ≤ 1

2
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. F : Id ─→ A ─→ bag(Top)
5. X : EClass(A)
6. ∀i:Id. ∀a:A.  (#(F i a) ≤ 1)
7. ∀e:E. (#(X es e) ≤ 1)
8. e : E@i
9. #(X es e) ≤ 1
10. #(X es e) = 1 ∈ ℤ
⊢ #(bag-union(∪x∈X es e.{F loc(e) x})) ≤ 1

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[F:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  bag(Top)].  \mforall{}[X:EClass(A)].
    es-sv-class(es;F@(Loc,  X))  supposing  (\mforall{}i:Id.  \mforall{}a:A.    (\#(F  i  a)  \mleq{}  1))  \mwedge{}  es-sv-class(es;X)


By

---

Latex:
((UnivCD  THENA  MaAuto)
  THEN  RepUR  ``es-sv-class  simple-loc-comb-1  simple-loc-comb  concat-lifting-loc-1``  0
  THEN  RepUR  ``concat-lifting1-loc  concat-lifting-loc  concat-lifting  concat-lifting-list``  0
  THEN  Auto
  THEN  RepeatFor  2  ((RecUnfold  `lifting-gen-list-rev`  0  THEN  Reduce  0))
  THEN  Unfold  `es-sv-class`  (-2)
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(\#(X  es  e)  =  0)  \mvee{}  (\#(X  es  e)  =  1)\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  D  (-1))

---

Home Index