---

Step * 1 1 of Lemma app_perm_wf


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))
BY
{ (OnCls [6; 4; 0] D) }

1
1. m : ℕ
2. n : ℕ
3. p : Perm(ℕm)
4. (p.b o p.f) = Id{ℕm} ∈ (ℕm ⟶ ℕm)
5. (p.f o p.b) = Id{ℕm} ∈ (ℕm ⟶ ℕm)
6. q : Perm(ℕn)
7. (q.b o q.f) = Id{ℕn} ∈ (ℕn ⟶ ℕn)
8. (q.f o q.b) = Id{ℕn} ∈ (ℕn ⟶ ℕn)
⊢ (app_permf(m;n;p.b;q.b) o app_permf(m;n;p.f;q.f)) = Id{ℕm + n} ∈ (ℕm + n ⟶ ℕm + n)

2
1. m : ℕ
2. n : ℕ
3. p : Perm(ℕm)
4. (p.b o p.f) = Id{ℕm} ∈ (ℕm ⟶ ℕm)
5. (p.f o p.b) = Id{ℕm} ∈ (ℕm ⟶ ℕm)
6. q : Perm(ℕn)
7. (q.b o q.f) = Id{ℕn} ∈ (ℕn ⟶ ℕn)
8. (q.f o q.b) = Id{ℕn} ∈ (ℕn ⟶ ℕn)
⊢ (app_permf(m;n;p.f;q.f) o app_permf(m;n;p.b;q.b)) = Id{ℕm + n} ∈ (ℕm + n ⟶ ℕm + n)

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  p  :  Perm(\mBbbN{}m)
4.  InvFuns(\mBbbN{}m;\mBbbN{}m;p.f;p.b)
5.  q  :  Perm(\mBbbN{}n)
6.  InvFuns(\mBbbN{}n;\mBbbN{}n;q.f;q.b)
\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:
(OnCls  [6;  4;  0]  D)

---

Home Index