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