Step
*
1
of Lemma
rotate-by-injection
1. n : ℕ
2. i : ℕ
⊢ Inj(ℕn;ℕn;rot(n)^i)
BY
{ (BLemma `fun_exp-injection` THEN Auto) }
Latex:
Latex:
1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}
\mvdash{}  Inj(\mBbbN{}n;\mBbbN{}n;rot(n)\^{}i)
By
Latex:
(BLemma  `fun\_exp-injection`  THEN  Auto)
Home
Index