---

Step * of Lemma nc-e'-s-lemma1

∀[I,J:fset(ℕ)]. ∀[i,z:ℕ]. ∀[g:J ⟶ I]. ∀[j,k:ℕ].  g,i=z ⋅ s = s ⋅ g,j=k,i=z ∈ J+z+k ⟶ I+i supposing ¬j ∈ I
BY
{ (Auto
   THEN Unfold `names-hom` 0
   THEN (FunExt THENA Auto)
   THEN (RWW "nh-comp-sq" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN RW (SubC (TryC (AddrC [2;1] UnfoldTopAbC))) 0
   THEN Reduce 0
   THEN AutoSplit
   THEN ((FLemma `not-added-name` [-1] THENA Auto) ORELSE HypSubst' (-1) 0)
   THEN (RWO "dM-lift-inc" 0 THENA Auto)) }

1
.....wf..... 
1. I : fset(ℕ)
2. J : fset(ℕ)
3. i : ℕ
4. z : ℕ
5. g : J ⟶ I
6. j : ℕ
7. k : ℕ
8. ¬j ∈ I
9. x : names(I+i)
10. x = i ∈ ℤ
⊢ g,j=k,i=z ∈ J+k+z ⟶ I+i+j

2
1. I : fset(ℕ)
2. J : fset(ℕ)
3. i : ℕ
4. z : ℕ
5. g : J ⟶ I
6. j : ℕ
7. k : ℕ
8. ¬j ∈ I
9. x : names(I+i)
10. x = i ∈ ℤ
⊢ (s z) = (g,j=k,i=z i) ∈ Point(dM(J+z+k))

3
.....wf..... 
1. I : fset(ℕ)
2. J : fset(ℕ)
3. i : ℕ
4. z : ℕ
5. g : J ⟶ I
6. j : ℕ
7. k : ℕ
8. ¬j ∈ I
9. x : names(I+i)
10. x ≠ i
11. x ∈ names(I)
⊢ g,j=k,i=z ∈ J+k+z ⟶ I+i+j

4
1. I : fset(ℕ)
2. J : fset(ℕ)
3. i : ℕ
4. z : ℕ
5. g : J ⟶ I
6. j : ℕ
7. k : ℕ
8. ¬j ∈ I
9. x : names(I+i)
10. x ≠ i
11. x ∈ names(I)
⊢ (dM-lift(J+z+k;J+z;s) (g x)) = (g,j=k,i=z x) ∈ Point(dM(J+z+k))

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[i,z:\mBbbN{}].  \mforall{}[g:J  {}\mrightarrow{}  I].  \mforall{}[j,k:\mBbbN{}].    g,i=z  \mcdot{}  s  =  s  \mcdot{}  g,j=k,i=z  supposing  \mneg{}j  \mmember{}  I


By

---

Latex:
(Auto
  THEN  Unfold  `names-hom`  0
  THEN  (FunExt  THENA  Auto)
  THEN  (RWW  "nh-comp-sq"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  RW  (SubC  (TryC  (AddrC  [2;1]  UnfoldTopAbC)))  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  ((FLemma  `not-added-name`  [-1]  THENA  Auto)  ORELSE  HypSubst'  (-1)  0)
  THEN  (RWO  "dM-lift-inc"  0  THENA  Auto))

---

Home Index