---

Step * of Lemma permutation-generators2

∀n:ℕ
  ∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ]
    (P[λx.x]
    ⇒ ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[f o (0, 1)]) supposing 1 < n
    ⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[f o rot(n)]))
    ⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . P[f]))
BY
{ (InstLemma `permutation-generators` []
   THEN ParallelLast'
   THEN (Assert λx.x ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  BY
               Auto)
   THEN (D 0 THENA Auto)
   THEN (SimpleInstHyp ⌜λ2f.P[inv(f)]⌝ (-3)⋅ THENA Auto)
   THEN Try ((ReduceSOAps (-1) THEN Reduce (-1)))
   THEN Thin (-4)
   THEN ReduceSOAps 0
   THEN ParallelLast) }

1
.....antecedent..... 
1. n : ℕ
2. λx.x ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
3. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
4. P (λx.x)
⊢ P inv(λx.x)

2
1. n : ℕ
2. λx.x ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
3. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
4. P (λx.x)
5. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ((P inv(f)) ⇒ (P inv((0, 1) o f))) supposing 1 < n
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ((P inv(f)) ⇒ (P inv(rot(n) o f))))
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P inv(f)))
⊢ ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ((P f) ⇒ (P (f o (0, 1)))) supposing 1 < n
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ((P f) ⇒ (P (f o rot(n)))))
⇒ (∀f:{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[f  o  (0,  1)])  supposing  1  <  n
        {}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  (P[f]  {}\mRightarrow{}  P[f  o  rot(n)]))
        {}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  P[f]))


By

---

Latex:
(InstLemma  `permutation-generators`  []
  THEN  ParallelLast'
  THEN  (Assert  \mlambda{}x.x  \mmember{}  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}    BY
                          Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (SimpleInstHyp  \mkleeneopen{}\mlambda{}\msubtwo{}f.P[inv(f)]\mkleeneclose{}  (-3)\mcdot{}  THENA  Auto)
  THEN  Try  ((ReduceSOAps  (-1)  THEN  Reduce  (-1)))
  THEN  Thin  (-4)
  THEN  ReduceSOAps  0
  THEN  ParallelLast)

---

Home Index