---

Step * 1 1 2 of Lemma app_perm_wf


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)
BY
{ (RewriteWith [4; 5; 7; 8] ``app_permf_id app_permf_comp`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  p  :  Perm(\mBbbN{}m)
4.  (p.b  o  p.f)  =  Id\{\mBbbN{}m\}
5.  (p.f  o  p.b)  =  Id\{\mBbbN{}m\}
6.  q  :  Perm(\mBbbN{}n)
7.  (q.b  o  q.f)  =  Id\{\mBbbN{}n\}
8.  (q.f  o  q.b)  =  Id\{\mBbbN{}n\}
\mvdash{}  (app\_permf(m;n;p.f;q.f)  o  app\_permf(m;n;p.b;q.b))  =  Id\{\mBbbN{}m  +  n\}


By

---

Latex:
(RewriteWith  [4;  5;  7;  8]  ``app\_permf\_id  app\_permf\_comp``  0  THEN  Auto)

---

Home Index