---

Step * of Lemma app_perm_wf

∀m,n:ℕ. ∀p:Sym(m). ∀q:Sym(n).  (app_perm(m;n;p;q) ∈ Sym(m + n))
BY
{ ProveWfLemma }

1
1. m : ℕ
2. n : ℕ
3. p : Sym(m)
4. q : Sym(n)
⊢ InvFuns(ℕm + n;ℕm + n;app_permf(m;n;p.f;q.f);app_permf(m;n;p.b;q.b))

---

Latex:

---

Latex:
\mforall{}m,n:\mBbbN{}.  \mforall{}p:Sym(m).  \mforall{}q:Sym(n).    (app\_perm(m;n;p;q)  \mmember{}  Sym(m  +  n))


By

---

Latex:
ProveWfLemma

---

Home Index