---

Step * 1 1 1 1 1 1 of Lemma tl_perm_wf


1. n : ℕ+
2. p : Perm(ℕn)
3. x : ℕ+n
4. x ≠ 0
5. x = (p.b 0) ∈ ℤ
⊢ p.f 0 ∈ ℕ+n
BY
{ (Assert x = (p.b 0) ∈ ℕn  THENM Thin 5  THENM SwapEquands 5  THENM FwdThruLemma `perm_b_to_f` [5] THENA Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  x  =  (p.b  0) 
  THENM  Thin  5 
  THENM  SwapEquands  5 
  THENM  FwdThruLemma  `perm\_b\_to\_f`  [5]
  THENA  Auto
  )

---

Home Index