Step * of Lemma permutation-generators

n:ℕ
  ∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ]
    (P[λx.x]
     ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} (P[f]  P[(0, 1) f]) supposing 1 < n
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} (P[f]  P[rot(n) f]))
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} P[f]))
BY
(Auto THEN Try ((BLemma `compose-injections` THEN Auto)) THEN Auto) }

1
1. : ℕ
2. [P] {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} (P[f]  P[(0, 1) f]) supposing 1 < n
5. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} (P[f]  P[rot(n) f])
6. {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
⊢ P[f]


Latex:


Latex:
\mforall{}n:\mBbbN{}
    \mforall{}[P:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}    {}\mrightarrow{}  \mBbbP{}]
        (P[\mlambda{}x.x]
        {}\mRightarrow{}  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  (P[f]  {}\mRightarrow{}  P[(0,  1)  o  f])  supposing  1  <  n
        {}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  (P[f]  {}\mRightarrow{}  P[rot(n)  o  f]))
        {}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  P[f]))


By


Latex:
(Auto  THEN  Try  ((BLemma  `compose-injections`  THEN  Auto))  THEN  Auto)




Home Index