Step * 1 1 1 1 1 1 of Lemma tl_perm_wf


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

1
1. : ℕ+
2. Perm(ℕn)
3. : ℕ+n
4. x ≠ 0
5. (p.b 0) x ∈ ℕn
6. (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