---

Step * of Lemma perm_induction

∀n:ℕ. ∀Q:Sym(n) ⟶ ℙ.  (Q[id_perm()] ⇒ (∀p:Sym(n). (Q[p] ⇒ (∀i,j:ℕn.  Q[txpose_perm(i;j) O p]))) ⇒ {∀p:Sym(n). Q[p]})
BY
{ ((Unfold `guard` 0 THEN UnivCD) THENA Auto) }

1
1. n : ℕ
2. Q : Sym(n) ⟶ ℙ
3. Q[id_perm()]
4. ∀p:Sym(n). (Q[p] ⇒ (∀i,j:ℕn.  Q[txpose_perm(i;j) O p]))
5. p : Sym(n)
⊢ Q[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,j:\mBbbN{}n.    Q[txpose\_perm(i;j)  O  p])))  {}\mRightarrow{}  \{\mforall{}p:Sym(n).  Q[p]\})


By

---

Latex:
((Unfold  `guard`  0  THEN  UnivCD)  THENA  Auto)

---

Home Index