---

Step * of Lemma nc-se'-p

∀[J:fset(ℕ)]. ∀[k,z:ℕ]. ∀[n:{n:ℕ| ¬n ∈ J} ].  (s,z=n ⋅ (n/<k>) = e(z;k) ∈ J+k ⟶ J+z)
BY
{ (Auto
   THEN (RWO "nh-comp-sq" 0 THENA Auto)
   THEN Unfold `names-hom` 0
   THEN (FunExt THENA Auto)
   THEN RepUR ``compose`` 0
   THEN RepUR ``nc-e\' nc-e nc-s`` 0
   THEN AutoSplit
   THEN Try ((FLemma `not-added-name` [-1] THENA Auto))
   THEN RWO "dM-lift-inc" 0
   THEN Auto) }

1
1. J : fset(ℕ)
2. k : ℕ
3. z : ℕ
4. n : {n:ℕ| ¬n ∈ J} 
5. x : names(J+z)
6. x = z ∈ ℤ
⊢ ((n/<k>) n) = <k> ∈ Point(dM(J+k))

2
.....wf..... 
1. J : fset(ℕ)
2. k : ℕ
3. z : ℕ
4. n : {n:ℕ| ¬n ∈ J} 
5. x : names(J+z)
6. x ≠ z
7. x ∈ names(J)
⊢ x ∈ names(J+k+n)

3
1. J : fset(ℕ)
2. k : ℕ
3. z : ℕ
4. n : {n:ℕ| ¬n ∈ J} 
5. x : names(J+z)
6. x ≠ z
7. x ∈ names(J)
⊢ ((n/<k>) x) = <x> ∈ Point(dM(J+k))

---

Latex:

---

Latex:
\mforall{}[J:fset(\mBbbN{})].  \mforall{}[k,z:\mBbbN{}].  \mforall{}[n:\{n:\mBbbN{}|  \mneg{}n  \mmember{}  J\}  ].    (s,z=n  \mcdot{}  (n/<k>)  =  e(z;k))


By

---

Latex:
(Auto
  THEN  (RWO  "nh-comp-sq"  0  THENA  Auto)
  THEN  Unfold  `names-hom`  0
  THEN  (FunExt  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  RepUR  ``nc-e\mbackslash{}'  nc-e  nc-s``  0
  THEN  AutoSplit
  THEN  Try  ((FLemma  `not-added-name`  [-1]  THENA  Auto))
  THEN  RWO  "dM-lift-inc"  0
  THEN  Auto)

---

Home Index