---

Step * of Lemma permutation-sign-flip

No Annotations
∀[n:ℕ]. ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ]. ∀[u,v:ℕn].
  permutation-sign(n;f o (u, v)) = (-permutation-sign(n;f)) ∈ ℤ supposing ¬(u = v ∈ ℤ)
BY
{ (InstLemma `permutation-sign-flip-adjacent` []⋅
   THEN ParallelLast'
   THEN (Assert ⌜∀d:ℕ
                   ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ]. ∀[u,v:ℕn].
                     permutation-sign(n;f o (u, v)) = (-permutation-sign(n;f)) ∈ ℤ 
                     supposing (¬(u = v ∈ ℤ)) ∧ (|u - v| ≤ (d + 1))⌝⋅
   THENM (Auto THEN InstHyp [⌜|u - v|⌝;⌜f⌝;⌜u⌝;⌜v⌝] (-5)⋅ THEN Auto)
   )) }

1
.....assertion..... 
1. [n] : ℕ
2. ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ]. ∀[u:ℕn - 1].  (permutation-sign(n;f o (u, u + 1)) = (-permutation-sign(n;f)) ∈ ℤ)
⊢ ∀d:ℕ
    ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ]. ∀[u,v:ℕn].
      permutation-sign(n;f o (u, v)) = (-permutation-sign(n;f)) ∈ ℤ supposing (¬(u = v ∈ ℤ)) ∧ (|u - v| ≤ (d + 1))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  ].  \mforall{}[u,v:\mBbbN{}n].
    permutation-sign(n;f  o  (u,  v))  =  (-permutation-sign(n;f))  supposing  \mneg{}(u  =  v)


By

---

Latex:
(InstLemma  `permutation-sign-flip-adjacent`  []\mcdot{}
  THEN  ParallelLast'
  THEN  (Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}
                                  \mforall{}[f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  ].  \mforall{}[u,v:\mBbbN{}n].
                                      permutation-sign(n;f  o  (u,  v))  =  (-permutation-sign(n;f)) 
                                      supposing  (\mneg{}(u  =  v))  \mwedge{}  (|u  -  v|  \mleq{}  (d  +  1))\mkleeneclose{}\mcdot{}
  THENM  (Auto  THEN  InstHyp  [\mkleeneopen{}|u  -  v|\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]  (-5)\mcdot{}  THEN  Auto)
  ))

---

Home Index