---

Step * 1 of Lemma tl_perm_wf


1. n : ℕ+
2. p : Perm(ℕn)
⊢ tl_perm(p) ∈ perm_sig(ℕ+n)
BY
{ ((RepUnfolds ``tl_perm comp_perm`` 0 THEN MemCD) THENA Auto) }

1
.....subterm..... T:t
1:n
1. n : ℕ+
2. p : Perm(ℕn)
⊢ p.f o txpose_perm(0
                    ;p.b 0).f ∈ ℕ+n ⟶ ℕ+n

2
.....subterm..... T:t
2:n
1. n : ℕ+
2. p : Perm(ℕn)
⊢ txpose_perm(0
              ;p.b 0).b o p.b ∈ ℕ+n ⟶ ℕ+n

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  p  :  Perm(\mBbbN{}n)
\mvdash{}  tl\_perm(p)  \mmember{}  perm\_sig(\mBbbN{}\msupplus{}n)


By

---

Latex:
((RepUnfolds  ``tl\_perm  comp\_perm``  0  THEN  MemCD)  THENA  Auto)

---

Home Index