---

Step * 1 2 1 1 1 1 of Lemma tl_perm_wf


1. n : ℕ+
2. p : Perm(ℕn)
3. x : ℕ+n
4. (p.b x) = 0 ∈ ℤ
5. (p.b 0) = 0 ∈ ℕn
⊢ False
BY
{ TACTIC:(((AssertAtHyp 5 (p.b x) = 0 ∈ ℕn THENM Thin 4) THENM RWN 3 (RevHypC 4) 5) THENA Auto) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  p  :  Perm(\mBbbN{}n)
3.  x  :  \mBbbN{}\msupplus{}n
4.  (p.b  x)  =  0
5.  (p.b  0)  =  0
\mvdash{}  False


By

---

Latex:
TACTIC:(((AssertAtHyp  5  (p.b  x)  =  0  THENM  Thin  4)  THENM  RWN  3  (RevHypC  4)  5)  THENA  Auto)

---

Home Index