---

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


1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. j : {j:ℕ| ¬j ∈ I+i} 
⊢ m(i;j) ⋅ (j0) = (i0) ⋅ s ∈ I+i ⟶ I+i
BY
{ (Assert (j0) i ∧ (j0) j = 0 ∈ Point(dM(I+i)) BY
         ((Subst' (j0) j ~ 0 0 THENA (RepUR ``nc-0`` 0 THEN AutoSplit))
          THEN (GenConcl ⌜((j0) i) = z ∈ Point(dM(I+i))⌝⋅ THENW (RepUR ``nc-0`` 0 THEN AutoSplit))
          THEN Try ((All Thin THEN Subst' z ∧ 0 = 0 ∧ z ∈ Point(dM(I+i)) 0 THEN Auto))
          THEN Subst' {} ~ 0 0
          THEN Auto)) }

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  (j0)  i  \mwedge{}  (j0)  j  =  0  BY
              ((Subst'  (j0)  j  \msim{}  0  0  THENA  (RepUR  ``nc-0``  0  THEN  AutoSplit))
                THEN  (GenConcl  \mkleeneopen{}((j0)  i)  =  z\mkleeneclose{}\mcdot{}  THENW  (RepUR  ``nc-0``  0  THEN  AutoSplit))
                THEN  Try  ((All  Thin  THEN  Subst'  z  \mwedge{}  0  =  0  \mwedge{}  z  0  THEN  Auto))
                THEN  Subst'  \{\}  \msim{}  0  0
                THEN  Auto))

---

Home Index