---

Step * 1 1 1 2 2 1 2 1 1 2 3 2 of Lemma permutation-generators


1. n : ℕ
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) o f]) supposing 1 < n
5. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[rot(n) o f])
6. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
7. i : ℕn
8. j : ℕn
9. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
10. P[f1]
11. ¬(n = 0 ∈ ℤ)
12. ¬(n = 1 ∈ ℤ)
13. ∀L:𝔹 List. Inj(ℕn;ℕn;reduce(λi,g. (if i then rot(n) else (0, 1) fi  o g);λx.x;L))
14. y : Unit
15. v : 𝔹 List
16. v1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
17. reduce(λi,g. (if i then rot(n) else (0, 1) fi  o g);λx.x;v) = v1 ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
18. P[v1 o f1]
⊢ P[((0, 1) o v1) o f1]
BY
{ ((D 4 THEN Auto)
   THEN (InstHyp [⌜v1 o f1⌝] (-1)⋅ THENA (Auto THEN BLemma `compose-injections` THEN Auto))
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
2:n
1. n : ℕ
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[rot(n) o f])
5. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
6. i : ℕn
7. j : ℕn
8. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
9. P[f1]
10. ¬(n = 0 ∈ ℤ)
11. ¬(n = 1 ∈ ℤ)
12. ∀L:𝔹 List. Inj(ℕn;ℕn;reduce(λi,g. (if i then rot(n) else (0, 1) fi  o g);λx.x;L))
13. y : Unit
14. v : 𝔹 List
15. v1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
16. reduce(λi,g. (if i then rot(n) else (0, 1) fi  o g);λx.x;v) = v1 ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
17. P[v1 o f1]
18. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[(0, 1) o f])
19. P[(0, 1) o (v1 o f1)]
⊢ (((0, 1) o v1) o f1) = ((0, 1) o (v1 o f1)) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 

---

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)\}  .  (P[f]  {}\mRightarrow{}  P[(0,  1)  o  f])  supposing  1  <  n
5.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  (P[f]  {}\mRightarrow{}  P[rot(n)  o  f])
6.  f  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
7.  i  :  \mBbbN{}n
8.  j  :  \mBbbN{}n
9.  f1  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
10.  P[f1]
11.  \mneg{}(n  =  0)
12.  \mneg{}(n  =  1)
13.  \mforall{}L:\mBbbB{}  List.  Inj(\mBbbN{}n;\mBbbN{}n;reduce(\mlambda{}i,g.  (if  i  then  rot(n)  else  (0,  1)  fi    o  g);\mlambda{}x.x;L))
14.  y  :  Unit
15.  v  :  \mBbbB{}  List
16.  v1  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
17.  reduce(\mlambda{}i,g.  (if  i  then  rot(n)  else  (0,  1)  fi    o  g);\mlambda{}x.x;v)  =  v1
18.  P[v1  o  f1]
\mvdash{}  P[((0,  1)  o  v1)  o  f1]


By

---

Latex:
((D  4  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}v1  o  f1\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Auto  THEN  BLemma  `compose-injections`  THEN  Auto))
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto)

---

Home Index