---

Step * of Lemma nc-e-comp-e'

∀[I,K:fset(ℕ)]. ∀[f:K ⟶ I]. ∀[z,z1,v:ℕ].  f,z=v = e(z;z1) ⋅ f,z1=v ∈ K+v ⟶ I+z supposing ¬z1 ∈ I
BY
{ (Auto
   THEN Unfold `names-hom` 0
   THEN (FunExt THENA Auto)
   THEN RepUR ``nh-comp dma-lift-compose`` 0
   THEN Fold `dM` 0
   THEN Fold `dM-lift` 0
   THEN RepUR ``nc-e`` 0
   THEN AutoSplit
   THEN Try ((FLemma `not-added-name` [-1] THENA Auto))
   THEN (RWO "dM-lift-inc" 0 THENA Auto)
   THEN RepUR ``nc-e\'`` 0
   THEN RepeatFor 2 (AutoSplit)) }

1
1. I : fset(ℕ)
2. K : fset(ℕ)
3. f : K ⟶ I
4. z : ℕ
5. z1 : ℕ
6. v : ℕ
7. ¬z1 ∈ I
8. x : names(I+z)
9. x ≠ z
10. x ≠ z
11. x ∈ names(I)
12. x = z1 ∈ ℤ
⊢ (f x) = <v> ∈ Point(dM(K+v))

---

Latex:

---

Latex:
\mforall{}[I,K:fset(\mBbbN{})].  \mforall{}[f:K  {}\mrightarrow{}  I].  \mforall{}[z,z1,v:\mBbbN{}].    f,z=v  =  e(z;z1)  \mcdot{}  f,z1=v  supposing  \mneg{}z1  \mmember{}  I


By

---

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

---

Home Index