---

Step * 1 1 of Lemma nc-m-nc-0


1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. j : {j:ℕ| ¬j ∈ I+i} 
4. (j0) i ∧ (j0) j = 0 ∈ Point(dM(I+i))
⊢ m(i;j) ⋅ (j0) = (i0) ⋅ s ∈ I+i ⟶ I+i
BY
{ (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 (Decide x = i ∈ ℤ THENA Auto)
   THEN ((HypSubst' (-1) 0 THEN ThinVar `x')
   ORELSE (Assert ((j0) x) = (s x) ∈ Point(dM(I+i)) BY
                 (RepUR ``nc-0 nc-s`` 0 THEN AutoSplit THEN DVar `j' THEN DVar `x' THEN D 4 THEN Auto))
   )
   THEN RepUR ``nc-0 nc-m`` 0
   THEN (OReduce 0 THENA Auto)
   THEN Try (Fold `nc-0` 0)
   THEN (Subst' {} ~ 0 0 THENA Auto)
   THEN RWO  "dM-lift-0 dM-lift-dMpair dM-lift-inc" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  I+i\} 
4.  (j0)  i  \mwedge{}  (j0)  j  =  0
\mvdash{}  m(i;j)  \mcdot{}  (j0)  =  (i0)  \mcdot{}  s


By

---

Latex:
(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  (Decide  x  =  i  THENA  Auto)
  THEN  ((HypSubst'  (-1)  0  THEN  ThinVar  `x')
  ORELSE  ...
  )
  THEN  RepUR  ``nc-0  nc-m``  0
  THEN  (OReduce  0  THENA  Auto)
  THEN  Try  (Fold  `nc-0`  0)
  THEN  (Subst'  \{\}  \msim{}  0  0  THENA  Auto)
  THEN  RWO    "dM-lift-0  dM-lift-dMpair  dM-lift-inc"  0
  THEN  Auto)

---

Home Index