---

Step * 1 2 1 1 1 of Lemma permutation-generators3

.....assertion..... 
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
⊢ ∀L:(ℕn × ℕn) List. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} .  (P[f] ⇒ P[f o compose-flips(L)])
BY
{ ((Assert ∀L:(ℕn × ℕn) List. (compose-flips(L) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ) BY
          (Auto THEN MemTypeCD THEN Auto))
   THEN (Assert ∀L:(ℕn × ℕn) List. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} .  (f o compose-flips(L) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} )\000C BY
               (ParallelLast
                THEN Auto
                THEN (GenConclTerm ⌜compose-flips(L)⌝ ⋅ THEN Auto)
                THEN DSetVars 
                THEN MemTypeCD
                THEN EAuto 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
9. ∀L:(ℕn × ℕn) List. (compose-flips(L) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} )
10. ∀L:(ℕn × ℕn) List. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} .  (f o compose-flips(L) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} )
⊢ ∀L:(ℕn × ℕn) List. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} .  (P[f] ⇒ P[f o compose-flips(L)])

---

Latex:

---

Latex:
.....assertion..... 
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]
8.  flips  :  (\mBbbN{}n  \mtimes{}  \mBbbN{}n)  List
\mvdash{}  \mforall{}L:(\mBbbN{}n  \mtimes{}  \mBbbN{}n)  List.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .    (P[f]  {}\mRightarrow{}  P[f  o  compose-flips(L)])


By

---

Latex:
((Assert  \mforall{}L:(\mBbbN{}n  \mtimes{}  \mBbbN{}n)  List.  (compose-flips(L)  \mmember{}  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  )  BY
                (Auto  THEN  MemTypeCD  THEN  Auto))
  THEN  (Assert  \mforall{}L:(\mBbbN{}n  \mtimes{}  \mBbbN{}n)  List.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .
                                (f  o  compose-flips(L)  \mmember{}  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  )  BY
                          (ParallelLast
                            THEN  Auto
                            THEN  (GenConclTerm  \mkleeneopen{}compose-flips(L)\mkleeneclose{}  \mcdot{}  THEN  Auto)
                            THEN  DSetVars 
                            THEN  MemTypeCD
                            THEN  EAuto  1))
  )

---

Home Index