---

Step * 1 of Lemma cycle-as-flips


1. n : ℕ
2. no_repeats(ℕn;[])
⊢ ∃flips:(ℕn × ℕn) List. (cycle([]) = compose-flips(flips) ∈ (ℕn ⟶ ℕn))
BY
{ (InstConcl [⌜[]⌝]⋅ THEN Auto THEN RepUR ``cycle compose-flips`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  no\_repeats(\mBbbN{}n;[])
\mvdash{}  \mexists{}flips:(\mBbbN{}n  \mtimes{}  \mBbbN{}n)  List.  (cycle([])  =  compose-flips(flips))


By

---

Latex:
(InstConcl  [\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  RepUR  ``cycle  compose-flips``  0  THEN  Auto)\mcdot{}

---

Home Index