---

Step * 2 1 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)
⊢ if (x =z j) then 1 else <x> fi  = <x> ∈ Point(dM(I+i))
BY
{ AutoSplit }

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)
8. x = j ∈ ℤ
⊢ 1 = <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{}  if  (x  =\msubz{}  j)  then  1  else  <x>  fi    =  <x>


By

---

Latex:
AutoSplit

---

Home Index