---

Step * 1 of Lemma nc-e'-r


1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. J : fset(ℕ)
4. f : J ⟶ I
5. j : {i:ℕ| ¬i ∈ J} 
6. x : names(I+i)
7. x = i ∈ ℤ
⊢ (dM-lift(J+j;I+i;f,i=j) <1-i>) = (dM-lift(J+j;J+j;r_j) <j>) ∈ Point(dM(J+j))
BY
{ (RWO "dM-lift-opp dM-lift-inc" 0
   THEN Auto
   THEN RepUR ``nc-e\' nc-r`` 0
   THEN (Subst' (i =z i) ~ tt 0 THENA Auto)
   THEN (Subst' (j =z j) ~ tt 0 THENA Auto)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  J  :  fset(\mBbbN{})
4.  f  :  J  {}\mrightarrow{}  I
5.  j  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  J\} 
6.  x  :  names(I+i)
7.  x  =  i
\mvdash{}  (dM-lift(J+j;I+i;f,i=j)  ə-i>)  =  (dM-lift(J+j;J+j;r\_j)  <j>)


By

---

Latex:
(RWO  "dM-lift-opp  dM-lift-inc"  0
  THEN  Auto
  THEN  RepUR  ``nc-e\mbackslash{}'  nc-r``  0
  THEN  (Subst'  (i  =\msubz{}  i)  \msim{}  tt  0  THENA  Auto)
  THEN  (Subst'  (j  =\msubz{}  j)  \msim{}  tt  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index