Theory permutes

⊢ ∀p. evenperm p ⇔ EVEN (@n. swapseq n p)

⊢ ∀f. inverse f = (λy. @x. f x = y)

⊢ ∀p. permutation p ⇔ ∃n. swapseq n p

⊢ ∀p s. p permutes s ⇔ (∀x. x ∉ s ⇒ p x = x) ∧ ∀y. ∃!x. p x = y

⊢ ∀i j k. swap (i,j) k = if k = i then j else if k = j then i else k

⊢ ∀s. FINITE s ⇒ CARD {p | p permutes s} = FACT (CARD s)

⊢ ∀p q.
    permutation p ∧ permutation q ⇒
    (evenperm (p ∘ q) ⇔ (evenperm p ⇔ evenperm q))

⊢ evenperm I ⇔ T

⊢ ∀p. permutation p ⇒ (evenperm (inverse p) ⇔ evenperm p)

⊢ ∀a b. evenperm (swap (a,b)) ⇔ a = b

⊢ ∀n p b. swapseq n p ∧ (EVEN n ⇔ b) ⇒ (evenperm p ⇔ b)

⊢ ∀s. FINITE s ⇒ FINITE {p | p permutes s}

⊢ ∀n p a b.
    swapseq n p ∧ a ≠ b ∧ (swap (a,b) ∘ p) a = a ⇒
    n ≠ 0 ∧ swapseq (n − 1) (swap (a,b) ∘ p)

⊢ ∀s n. s HAS_SIZE n ⇒ {p | p permutes s} HAS_SIZE FACT n

⊢ ∀s q. q permutes s ⇒ {q ∘ p | p permutes s} = {p | p permutes s}

⊢ ∀s q. q permutes s ⇒ {p ∘ q | p permutes s} = {p | p permutes s}

⊢ ∀s. {inverse p | p permutes s} = {p | p permutes s}

⊢ ∀f. (∀x y. f x = f y ⇒ x = y) ⇔ ∀x. inverse f (f x) = x

⊢ ∀f. (∀x y. f x = f y ⇒ x = y) ⇔ inverse f ∘ f = I

⊢ inverse I = I

⊢ ∀a b. inverse (swap (a,b)) = swap (a,b)

⊢ ∀f g. f ∘ g = I ∧ g ∘ f = I ⇒ inverse f = g

⊢ ∀p. permutation p ⇔ (∀y. ∃!x. p x = y) ∧ FINITE {x | p x ≠ x}

⊢ ∀p. permutation p ⇒ ∀y. ∃!x. p x = y

⊢ ∀p q. permutation p ∧ permutation q ⇒ permutation (p ∘ q)

⊢ (∀p q. permutation p ⇒ (permutation (p ∘ q) ⇔ permutation q)) ∧
  ∀p q. permutation q ⇒ (permutation (p ∘ q) ⇔ permutation p)

⊢ (∀p a b. permutation (swap (a,b) ∘ p) ⇔ permutation p) ∧
  ∀p a b. permutation (p ∘ swap (a,b)) ⇔ permutation p

⊢ ∀p. permutation p ⇒ FINITE {x | p x ≠ x}

⊢ permutation I

⊢ ∀p. permutation p ⇒ permutation (inverse p)

⊢ ∀p q.
    permutation p ∧ permutation q ⇒ inverse (p ∘ q) = inverse q ∘ inverse p

⊢ ∀p. permutation p ⇒ inverse p ∘ p = I ∧ p ∘ inverse p = I

⊢ ∀s p.
    FINITE s ∧ (∀y. ∃!x. p x = y) ∧ (∀x. x ∉ s ⇒ p x = x) ⇒ permutation p

⊢ ∀p. permutation p ⇔ ∃s. FINITE s ∧ p permutes s

⊢ ∀a b. permutation (swap (a,b))

⊢ ∀p q s x. p permutes s ∧ q permutes s ⇒ q ∘ p permutes s

⊢ ∀p. p permutes ∅ ⇔ p = I

⊢ ∀s p.
    FINITE s ⇒
    (p permutes s ⇔
     (∀x. x ∉ s ⇒ p x = x) ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
     ∀x y. x ∈ s ∧ y ∈ s ∧ p x = p y ⇒ x = y)

⊢ ∀s p.
    FINITE s ⇒
    (p permutes s ⇔
     (∀x. x ∉ s ⇒ p x = x) ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
     ∀y. y ∈ s ⇒ ∃x. x ∈ s ∧ p x = y)

⊢ ∀s. I permutes s

⊢ ∀p s. p permutes s ⇒ IMAGE p s = s

⊢ ∀P s.
    FINITE s ∧ P I ∧
    (∀a b p. a ∈ s ∧ b ∈ s ∧ P p ∧ permutation p ⇒ P (swap (a,b) ∘ p)) ⇒
    ∀p. p permutes s ⇒ P p

⊢ ∀p s. p permutes s ⇒ ∀x y. p x = p y ⇔ x = y

⊢ {p | p permutes a INSERT s} =
  IMAGE (λ(b,p). swap (a,b) ∘ p)
    {(b,p) | b ∈ a INSERT s ∧ p ∈ {p | p permutes s}}

⊢ ∀p a s. p permutes a INSERT s ⇒ swap (a,p a) ∘ p permutes s

⊢ ∀p s. p permutes s ⇒ inverse p permutes s

⊢ ∀p s. p permutes s ⇒ (∀x. p (inverse p x) = x) ∧ ∀x. inverse p (p x) = x

⊢ ∀p s. p permutes s ⇒ p ∘ inverse p = I ∧ inverse p ∘ p = I

⊢ ∀p s. p permutes s ⇒ ∀x y. inverse p y = x ⇔ p x = y

⊢ ∀p s. p permutes s ⇒ inverse (inverse p) = p

⊢ ∀p n i. p permutes count n ∧ i ∈ count n ⇒ p i < n

⊢ ∀p s x. p permutes s ⇒ (p x ∈ s ⇔ x ∈ s)

⊢ ∀p s. p permutes s ∧ (∀i. i ∈ s ⇒ i ≤ p i) ⇒ p = I

⊢ ∀p s. p permutes s ∧ (∀i. i ∈ s ⇒ p i ≤ i) ⇒ p = I

⊢ ∀p a. p permutes {a} ⇔ p = I

⊢ ∀p s t. p permutes s ∧ s ⊆ t ⇒ p permutes t

⊢ ∀p s t. p permutes s ∧ (∀x. x ∈ s DIFF t ⇒ p x = x) ⇒ p permutes t

⊢ ∀p s. p permutes s ⇒ ∀y. ∃x. p x = y

⊢ ∀a b s. a ∈ s ∧ b ∈ s ⇒ swap (a,b) permutes s

⊢ ∀p. p permutes 𝕌(:α) ⇔ ∀y. ∃!x. p x = y

⊢ ∀f. (∀y. ∃x. f x = y) ⇔ ∀y. f (inverse f y) = y

⊢ ∀f. (∀y. ∃x. f x = y) ⇔ f ∘ inverse f = I

⊢ ∀n p m q. swapseq n p ∧ swapseq m q ⇒ swapseq (n + m) (p ∘ q)

⊢ ∀n p a b. swapseq n p ∧ a ≠ b ⇒ swapseq (SUC n) (p ∘ swap (a,b))

⊢ ∀m n p. swapseq m p ∧ swapseq n p ⇒ (EVEN m ⇔ EVEN n)

⊢ swapseq 0 I

⊢ ∀n. swapseq n I ⇒ EVEN n

⊢ ∀n p. swapseq n p ⇒ swapseq n (inverse p)

⊢ ∀n p. swapseq n p ⇒ ∃q. swapseq n q ∧ p ∘ q = I ∧ q ∘ p = I

⊢ ∀a b. swapseq (if a = b then 0 else 1) (swap (a,b))

⊢ ∀a b c. a ≠ c ∧ b ≠ c ⇒ swap (a,b) ∘ swap (a,c) = swap (b,c) ∘ swap (a,b)

⊢ ∀a b c. a ≠ b ∧ a ≠ c ⇒ swap (a,c) ∘ swap (b,c) = swap (b,c) ∘ swap (a,b)

⊢ ∀a b x y. x = swap (a,b) y ⇔ y = swap (a,b) x

⊢ ∀a b c d.
    a ≠ b ∧ c ≠ d ⇒
    swap (a,b) ∘ swap (c,d) = I ∨
    ∃x y z.
      x ≠ a ∧ y ≠ a ∧ z ≠ a ∧ x ≠ y ∧
      swap (a,b) ∘ swap (c,d) = swap (x,y) ∘ swap (a,z)

⊢ ∀a b. swap (a,b) ∘ swap (a,b) = I

⊢ ∀a b c d.
    a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ⇒
    swap (a,b) ∘ swap (c,d) = swap (c,d) ∘ swap (a,b)

⊢ ∀a. swap (a,a) = I

⊢ ∀a b. swap (a,b) = swap (b,a)

⊢ ∀f. (∀y. ∃x. f x = y) ∧ (∀x y. f x = f y ⇒ x = y) ⇒
      inverse f = LINV f 𝕌(:α)

⊢ ∀f s. f permutes s ⇔ f PERMUTES s ∧ ∀x. x ∉ s ⇒ f x = x

⊢ ∀f. f permutes 𝕌(:α) ⇔ f PERMUTES 𝕌(:α)

⊢ ∀f s. f permutes s ⇒ f PERMUTES s

⊢ ∀a0 a1.
    swapseq a0 a1 ⇔
    a0 = 0 ∧ a1 = I ∨
    ∃a b p n. a0 = SUC n ∧ a1 = swap (a,b) ∘ p ∧ swapseq n p ∧ a ≠ b

⊢ ∀swapseq'.
    swapseq' 0 I ∧
    (∀a b p n. swapseq' n p ∧ a ≠ b ⇒ swapseq' (SUC n) (swap (a,b) ∘ p)) ⇒
    ∀a0 a1. swapseq a0 a1 ⇒ swapseq' a0 a1

⊢ swapseq 0 I ∧
  ∀a b p n. swapseq n p ∧ a ≠ b ⇒ swapseq (SUC n) (swap (a,b) ∘ p)

⊢ ∀swapseq'.
    swapseq' 0 I ∧
    (∀a b p n.
       swapseq n p ∧ swapseq' n p ∧ a ≠ b ⇒
       swapseq' (SUC n) (swap (a,b) ∘ p)) ⇒
    ∀a0 a1. swapseq a0 a1 ⇒ swapseq' a0 a1