---

Step * of Lemma flip-conjugation1

∀[n:ℕ]. ∀[k:ℕn - 1]. ∀[j:ℕk].  ((j, k + 1) = ((k, k + 1) o ((j, k) o (k, k + 1))) ∈ (ℕn ⟶ ℕn))
BY
{ ((Auto THEN BLemma `flip-conjugation`) THEN Auto THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[k:\mBbbN{}n  -  1].  \mforall{}[j:\mBbbN{}k].    ((j,  k  +  1)  =  ((k,  k  +  1)  o  ((j,  k)  o  (k,  k  +  1))))


By

---

Latex:
((Auto  THEN  BLemma  `flip-conjugation`)  THEN  Auto  THEN  Auto')

---

Home Index