---

Step * 1 1 of Lemma nc-e'-lemma3


1. I : fset(ℕ)
2. i : ℕ
3. ¬i ∈ I
4. J : fset(ℕ)
5. g : J ⟶ I
6. j : ℕ
7. ¬j ∈ J
8. x : names(I)
⊢ (dM-lift(J+j;I+i;λx.if (x =z i) then <j> else g x fi ) <x>) = (dM-lift(J+j;J;λx.<x>) (g x)) ∈ Point(dM(J+j))
BY
{ (RWO "dM-lift-inc" 0 THEN Try (Complete (Auto))) }

1
1. I : fset(ℕ)
2. i : ℕ
3. ¬i ∈ I
4. J : fset(ℕ)
5. g : J ⟶ I
6. j : ℕ
7. ¬j ∈ J
8. x : names(I)
⊢ ((λx.if (x =z i) then <j> else g x fi ) x) = (dM-lift(J+j;J;λx.<x>) (g x)) ∈ Point(dM(J+j))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
3.  \mneg{}i  \mmember{}  I
4.  J  :  fset(\mBbbN{})
5.  g  :  J  {}\mrightarrow{}  I
6.  j  :  \mBbbN{}
7.  \mneg{}j  \mmember{}  J
8.  x  :  names(I)
\mvdash{}  (dM-lift(J+j;I+i;\mlambda{}x.if  (x  =\msubz{}  i)  then  <j>  else  g  x  fi  )  <x>)  =  (dM-lift(J+j;J;\mlambda{}x.<x>)  (g  x))


By

---

Latex:
(RWO  "dM-lift-inc"  0  THEN  Try  (Complete  (Auto)))

---

Home Index