---

Step * 2 1 1 of Lemma tl_perm_wf


1. n : ℕ+
2. p : Perm(ℕn)
3. tl_perm(p) ∈ Perm(ℕn)
⊢ (tl_perm(p).b o tl_perm(p).f) = Id{ℕ+n} ∈ (ℕ+n ⟶ ℕ+n)
BY
{ ((RepUnfolds ``tidentity identity compose`` 0 THEN MemCD) THENA Auto) }

1
.....subterm..... T:t
1:n
1. n : ℕ+
2. p : Perm(ℕn)
3. tl_perm(p) ∈ Perm(ℕn)
4. x : ℕ+n
⊢ (tl_perm(p).b (tl_perm(p).f x)) = x ∈ ℕ+n

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  p  :  Perm(\mBbbN{}n)
3.  tl\_perm(p)  \mmember{}  Perm(\mBbbN{}n)
\mvdash{}  (tl\_perm(p).b  o  tl\_perm(p).f)  =  Id\{\mBbbN{}\msupplus{}n\}


By

---

Latex:
((RepUnfolds  ``tidentity  identity  compose``  0  THEN  MemCD)  THENA  Auto)

---

Home Index