---

Step * of Lemma nc-p-s-commute

∀[I:fset(ℕ)]. ∀[i,j:ℕ]. ∀[z:Point(dM(I))].  ((i/z) ⋅ s = s ⋅ (i/z) ∈ I+j ⟶ I+i)
BY
{ (Auto
   THEN Unfold `names-hom` 0
   THEN (FunExt THENA Auto)
   THEN RepUR ``nh-comp dma-lift-compose`` 0
   THEN Fold `dM` 0
   THEN Fold `dM-lift` 0
   THEN RW (SubC (TryC (AddrC [2;1] UnfoldTopAbC))) 0
   THEN Reduce 0
   THEN Try (QuickAuto)
   THEN (Assert (i/z) ∈ I+j ⟶ I+i+j BY
               ((Assert ⌜(i/z) ∈ I+j ⟶ I+j+i⌝⋅ THENA Auto) THEN InferEqualType THEN Auto))
   THEN AutoSplit) }

1
1. I : fset(ℕ)
2. i : ℕ
3. j : ℕ
4. z : Point(dM(I))
5. x : names(I+i)
6. (i/z) ∈ I+j ⟶ I+i+j
7. x = i ∈ ℤ
⊢ (dM-lift(I+j;I;s) z) = (dM-lift(I+j;I+i+j;(i/z)) <x>) ∈ Point(dM(I+j))

2
1. I : fset(ℕ)
2. i : ℕ
3. j : ℕ
4. z : Point(dM(I))
5. x : names(I+i)
6. x ≠ i
7. (i/z) ∈ I+j ⟶ I+i+j
⊢ (dM-lift(I+j;I;s) <x>) = (dM-lift(I+j;I+i+j;(i/z)) <x>) ∈ Point(dM(I+j))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i,j:\mBbbN{}].  \mforall{}[z:Point(dM(I))].    ((i/z)  \mcdot{}  s  =  s  \mcdot{}  (i/z))


By

---

Latex:
(Auto
  THEN  Unfold  `names-hom`  0
  THEN  (FunExt  THENA  Auto)
  THEN  RepUR  ``nh-comp  dma-lift-compose``  0
  THEN  Fold  `dM`  0
  THEN  Fold  `dM-lift`  0
  THEN  RW  (SubC  (TryC  (AddrC  [2;1]  UnfoldTopAbC)))  0
  THEN  Reduce  0
  THEN  Try  (QuickAuto)
  THEN  (Assert  (i/z)  \mmember{}  I+j  {}\mrightarrow{}  I+i+j  BY
                          ((Assert  \mkleeneopen{}(i/z)  \mmember{}  I+j  {}\mrightarrow{}  I+j+i\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  InferEqualType  THEN  Auto))
  THEN  AutoSplit)

---

Home Index