---

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

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[F:Id ─→ A ─→ B ─→ bag(Top)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  es-sv-class(es;F@Loc o (Loc,X, Y)) 
  supposing (∀i:Id. ∀a:A. ∀b:B.  (#(F i a b) ≤ 1)) ∧ es-sv-class(es;X) ∧ es-sv-class(es;Y)
BY
{ ((UnivCD THENA MaAuto)
   THEN RepUR ``es-sv-class simple-loc-comb-2 simple-loc-comb concat-lifting-loc-2`` 0
   THEN RepUR ``concat-lifting2-loc concat-lifting-loc concat-lifting concat-lifting-list`` 0
   THEN Auto
   THEN RepeatFor 3 ((RecUnfold `lifting-gen-list-rev` 0 THEN Reduce 0))
   THEN Unfold `es-sv-class` (-3)
   THEN (InstHyp [⌈e⌉] (-3)⋅ 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. B : Type
5. F : Id ─→ A ─→ B ─→ bag(Top)
6. X : EClass(A)
7. Y : EClass(B)
8. ∀i:Id. ∀a:A. ∀b:B.  (#(F i a b) ≤ 1)
9. ∀e:E. (#(X es e) ≤ 1)
10. es-sv-class(es;Y)
11. e : E@i
12. #(X es e) ≤ 1
13. #(X es e) = 0 ∈ ℤ
⊢ #(bag-union(∪x∈X es e.∪x@0∈Y es e.{F loc(e) x x@0})) ≤ 1

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

---

Latex:

---

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


By

---

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

---

Home Index