---

Step * 1 2 of Lemma tl_perm_wf

.....subterm..... T:t
2:n
1. n : ℕ+
2. p : Perm(ℕn)
⊢ txpose_perm(0
              ;p.b 0).b o p.b ∈ ℕ+n ⟶ ℕ+n
BY
{ (((AbReduce 0 THEN Unfold `compose` 0) THEN MemCD) THENA Auto) }

1
.....subterm..... T:t
1:n
1. n : ℕ+
2. p : Perm(ℕn)
3. x : ℕ+n
⊢ swap(0;p.b 0) (p.b x) ∈ ℕ+n

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  n  :  \mBbbN{}\msupplus{}
2.  p  :  Perm(\mBbbN{}n)
\mvdash{}  txpose\_perm(0
                            ;p.b  0).b  o  p.b  \mmember{}  \mBbbN{}\msupplus{}n  {}\mrightarrow{}  \mBbbN{}\msupplus{}n


By

---

Latex:
(((AbReduce  0  THEN  Unfold  `compose`  0)  THEN  MemCD)  THENA  Auto)

---

Home Index