---

Step * of Lemma perm_induction_a

∀n:ℕ. ∀Q:Sym(n) ⟶ ℙ.
  (Q[id_perm()] ⇒ (∀p:Sym(n). (Q[p] ⇒ (∀i:{1..n-}. Q[txpose_perm(i;0) O p]))) ⇒ {∀p:Sym(n). Q[p]})
BY
{ ((UnivCD THENA Auto) THEN BLemma `perm_induction` THEN Auto) }

1
1. n : ℕ@i
2. Q : Sym(n) ⟶ ℙ@i'
3. Q[id_perm()]@i
4. ∀p:Sym(n). (Q[p] ⇒ (∀i:{1..n-}. Q[txpose_perm(i;0) O p]))@i
5. p : Sym(n)@i
6. Q[p]@i
7. i : ℕn@i
8. j : ℕn@i
⊢ Q[txpose_perm(i
                ;j)
     O p]

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}Q:Sym(n)  {}\mrightarrow{}  \mBbbP{}.
    (Q[id\_perm()]
    {}\mRightarrow{}  (\mforall{}p:Sym(n).  (Q[p]  {}\mRightarrow{}  (\mforall{}i:\{1..n\msupminus{}\}.  Q[txpose\_perm(i;0)  O  p])))
    {}\mRightarrow{}  \{\mforall{}p:Sym(n).  Q[p]\})


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  BLemma  `perm\_induction`  THEN  Auto)

---

Home Index