---

Step * 1 2 1 of Lemma permutation-generators3


1. n : ℕ
2. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f] ⇒ P[f o (i, j)] supposing i < j
5. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
6. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
7. P[f1]
⊢ P[f1 o rot(n)]
BY
{ (((InstLemma `rotate-as-flips` [⌜n⌝]⋅ THENA Auto) THEN ExRepD)
   THEN (Assert rot(n) = compose-flips(flips) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  BY
               (EqTypeCD THEN Auto))
   THEN (ApFunToHypEquands `Z' ⌜f1 o Z⌝ ⌜{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⌝ (-1)⋅
         THENA (Auto THEN DSetVars THEN MemTypeCD THEN EAuto 1)
         )
   THEN (RWO "-1" 0 THENA Auto)
   THEN RepeatFor 3 (Thin (-1))) }

1
1. n : ℕ
2. [P] : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f] ⇒ P[f o (i, j)] supposing i < j
5. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
6. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
7. P[f1]
8. flips : (ℕn × ℕn) List
⊢ P[f1 o compose-flips(flips)]

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  [P]  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}    {}\mrightarrow{}  \mBbbP{}
3.  P[\mlambda{}x.x]
4.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  \mforall{}i,j:\mBbbN{}n.    P[f]  {}\mRightarrow{}  P[f  o  (i,  j)]  supposing  i  <  j
5.  f  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
6.  f1  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
7.  P[f1]
\mvdash{}  P[f1  o  rot(n)]


By

---

Latex:
(((InstLemma  `rotate-as-flips`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (Assert  rot(n)  =  compose-flips(flips)  BY
                          (EqTypeCD  THEN  Auto))
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}f1  o  Z\mkleeneclose{}  \mkleeneopen{}\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  \mkleeneclose{}  (-1)\mcdot{}
              THENA  (Auto  THEN  DSetVars  THEN  MemTypeCD  THEN  EAuto  1)
              )
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  RepeatFor  3  (Thin  (-1)))

---

Home Index