---

Step * 1 2 1 of Lemma tl_perm_wf

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

1
.....truecase..... 
1. n : ℕ+
2. p : Perm(ℕn)
3. x : ℕ+n
4. (p.b x) = 0 ∈ ℤ
⊢ p.b 0 ∈ ℕ+n

2
.....truecase..... 
1. n : ℕ+
2. p : Perm(ℕn)
3. x : ℕ+n
4. ¬((p.b x) = 0 ∈ ℤ)
5. (p.b x) = (p.b 0) ∈ ℤ
⊢ 0 ∈ ℕ+n

3
.....falsecase..... 
1. n : ℕ+
2. p : Perm(ℕn)
3. x : ℕ+n
4. ¬((p.b x) = 0 ∈ ℤ)
5. ¬((p.b x) = (p.b 0) ∈ ℤ)
⊢ p.b x ∈ ℕ+n

---

Latex:

---

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


By

---

Latex:
(Unfold  `swap`  0  THEN  AbReduce  0  THEN  (SplitOnConclITEs  THENA  Auto))

---

Home Index