---

Step * 1 1 1 of Lemma tl_perm_wf

.....subterm..... T:t
1:n
1. n : ℕ+
2. p : Perm(ℕn)
3. x : ℕ+n
⊢ p.f (swap(0;p.b 0) x) ∈ ℕ+n
BY
{ (Unfold `swap` 0 THEN AbReduce 0) }

1
1. n : ℕ+
2. p : Perm(ℕn)
3. x : ℕ+n
⊢ p.f if (x =z 0) then p.b 0 if (x =z p.b 0) then 0 else x fi  ∈ ℕ+n

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  n  :  \mBbbN{}\msupplus{}
2.  p  :  Perm(\mBbbN{}n)
3.  x  :  \mBbbN{}\msupplus{}n
\mvdash{}  p.f  (swap(0;p.b  0)  x)  \mmember{}  \mBbbN{}\msupplus{}n


By

---

Latex:
(Unfold  `swap`  0  THEN  AbReduce  0)

---

Home Index