---

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

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[F:A ─→ B]. ∀[X:EClass(A)].
  es-sv-class(es;lifting-1(F)|X|) supposing es-sv-class(es;X)
BY
{ ((UnivCD THENA MaAuto)
   THEN All (Unfold `es-sv-class`)
   THEN Auto
   THEN (InstHyp [⌈e⌉] (-2)⋅ THENA Auto)
   THEN RepUR ``simple-comb-1 simple-comb lifting-1 lifting1 lifting-gen-rev`` 0
   THEN RepeatFor 2 ((RecUnfold `lifting-gen-list-rev` 0⋅ THEN Reduce 0))
   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 : A ─→ B
6. X : EClass(A)
7. ∀e:E. (#(X es e) ≤ 1)
8. e : E@i
9. #(X es e) ≤ 1
10. #(X es e) = 0 ∈ ℤ
⊢ #(∪x∈X es e.{F x}) ≤ 1

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

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:Type].  \mforall{}[F:A  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].
    es-sv-class(es;lifting-1(F)|X|)  supposing  es-sv-class(es;X)


By

---

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

---

Home Index