---

Step * 1 1 of Lemma tl_perm_wf

.....subterm..... T:t
1:n
1. n : ℕ+
2. p : Perm(ℕn)
⊢ p.f o txpose_perm(0
                    ;p.b 0).f ∈ ℕ+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
⊢ p.f (swap(0;p.b 0) x) ∈ ℕ+n

---

Latex:

---

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


By

---

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

---

Home Index