---

Step * 1 of Lemma app_perm_wf


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))
BY
{ ((OnHyps [3; 4] UnfoldTopAb THEN OnMHyps [4; 3] AddProperties) THENA Auto) }

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

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  p  :  Sym(m)
4.  q  :  Sym(n)
\mvdash{}  InvFuns(\mBbbN{}m  +  n;\mBbbN{}m  +  n;app\_permf(m;n;p.f;q.f);app\_permf(m;n;p.b;q.b))


By

---

Latex:
((OnHyps  [3;  4]  UnfoldTopAb  THEN  OnMHyps  [4;  3]  AddProperties)  THENA  Auto)

---

Home Index