---

Step * of Lemma nc-e'-lemma4

No Annotations
∀[I,J:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[j:{j:ℕ| ¬j ∈ J} ]. ∀[g:J ⟶ I]. ∀[k:{i1:ℕ| ¬i1 ∈ I+i} ]. ∀[l:{i:ℕ| ¬i ∈ J+j} ].
  ((i0) ⋅ s ⋅ g,i=j,k=l = g,i=j ⋅ (j0) ⋅ s ∈ J+j+l ⟶ I+i)
BY
{ (Intros
   THEN Unfold `names-hom` 0
   THEN (FunExt THENA Auto)
   THEN (RWW "nh-comp-sq" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN ((Assert I ⊆ I+i+k BY EAuto 2) THEN (Assert J ⊆ J+j+l BY EAuto 2))
   THEN (RW (AddrC [2;2;2] (UnfoldC `nc-0`)) 0 THEN Reduce 0)
   THEN RW (AddrC [3;2;2] (UnfoldC `nc-e\'`)) 0
   THEN Reduce 0
   THEN (BoolCase ⌜(x =z i)⌝⋅ THENA Auto)
   THEN (ThinVar `x' ORELSE (FLemma `not-added-name` [-3] THENA Auto))) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. i : {i:ℕ| ¬i ∈ I} 
4. j : {j:ℕ| ¬j ∈ J} 
5. g : J ⟶ I
6. k : {i1:ℕ| ¬i1 ∈ I+i} 
7. l : {i:ℕ| ¬i ∈ J+j} 
8. I ⊆ I+i+k
9. J ⊆ J+j+l
⊢ (dM-lift(J+j+l;I+i+k;g,i=j,k=l) (dM-lift(I+i+k;I;s) {}))
= (dM-lift(J+j+l;J;s) (dM-lift(J;J+j;(j0)) <j>))
∈ Point(dM(J+j+l))

2
1. I : fset(ℕ)
2. J : fset(ℕ)
3. i : {i:ℕ| ¬i ∈ I} 
4. j : {j:ℕ| ¬j ∈ J} 
5. g : J ⟶ I
6. k : {i1:ℕ| ¬i1 ∈ I+i} 
7. l : {i:ℕ| ¬i ∈ J+j} 
8. x : names(I+i)
9. x ≠ i
10. I ⊆ I+i+k
11. J ⊆ J+j+l
12. x ∈ names(I)
⊢ (dM-lift(J+j+l;I+i+k;g,i=j,k=l) (dM-lift(I+i+k;I;s) <x>))
= (dM-lift(J+j+l;J;s) (dM-lift(J;J+j;(j0)) (g x)))
∈ Point(dM(J+j+l))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].  \mforall{}[j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\}  ].  \mforall{}[g:J  {}\mrightarrow{}  I].  \mforall{}[k:\{i1:\mBbbN{}|  \mneg{}i1  \mmember{}  I+i\}  ].
\mforall{}[l:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  J+j\}  ].
    ((i0)  \mcdot{}  s  \mcdot{}  g,i=j,k=l  =  g,i=j  \mcdot{}  (j0)  \mcdot{}  s)


By

---

Latex:
(Intros
  THEN  Unfold  `names-hom`  0
  THEN  (FunExt  THENA  Auto)
  THEN  (RWW  "nh-comp-sq"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  ((Assert  I  \msubseteq{}  I+i+k  BY  EAuto  2)  THEN  (Assert  J  \msubseteq{}  J+j+l  BY  EAuto  2))
  THEN  (RW  (AddrC  [2;2;2]  (UnfoldC  `nc-0`))  0  THEN  Reduce  0)
  THEN  RW  (AddrC  [3;2;2]  (UnfoldC  `nc-e\mbackslash{}'`))  0
  THEN  Reduce  0
  THEN  (BoolCase  \mkleeneopen{}(x  =\msubz{}  i)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (ThinVar  `x'  ORELSE  (FLemma  `not-added-name`  [-3]  THENA  Auto)))

---

Home Index