---

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index