---

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


1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. j : {j:ℕ| ¬j ∈ I+i} 
4. x : names(I+i)
5. (m(i;j) ⋅ (j1) i) = (j1) i ∧ (j1) j ∈ Point(dM(I+i))
6. ¬(x = i ∈ ℤ)
7. x ∈ names(I)
⊢ (m(i;j) ⋅ (j1) x) = (1 x) ∈ Point(dM(I+i))
BY
{ (RepUR ``nh-comp nc-1 nh-id dma-lift-compose`` 0
   THEN Fold `dM` 0
   THEN Fold `dM-lift` 0
   THEN (Subst' {{}} ~ 1 0 THENA Auto)
   THEN RepUR ``nc-m`` 0
   THEN (OReduce 0 THENA Auto)
   THEN (RWO "dM-lift-inc" 0 THENW Auto)
   THEN (Trivial ORELSE Reduce 0)) }

1
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. j : {j:ℕ| ¬j ∈ I+i} 
4. x : names(I+i)
5. (m(i;j) ⋅ (j1) i) = (j1) i ∧ (j1) j ∈ Point(dM(I+i))
6. ¬(x = i ∈ ℤ)
7. x ∈ names(I)
⊢ if (x =z j) then 1 else <x> fi  = <x> ∈ Point(dM(I+i))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  I+i\} 
4.  x  :  names(I+i)
5.  (m(i;j)  \mcdot{}  (j1)  i)  =  (j1)  i  \mwedge{}  (j1)  j
6.  \mneg{}(x  =  i)
7.  x  \mmember{}  names(I)
\mvdash{}  (m(i;j)  \mcdot{}  (j1)  x)  =  (1  x)


By

---

Latex:
(RepUR  ``nh-comp  nc-1  nh-id  dma-lift-compose``  0
  THEN  Fold  `dM`  0
  THEN  Fold  `dM-lift`  0
  THEN  (Subst'  \{\{\}\}  \msim{}  1  0  THENA  Auto)
  THEN  RepUR  ``nc-m``  0
  THEN  (OReduce  0  THENA  Auto)
  THEN  (RWO  "dM-lift-inc"  0  THENW  Auto)
  THEN  (Trivial  ORELSE  Reduce  0))

---

Home Index