(* ----- Definitions *)

let xor1 = new_definition
  `xor1 (n:num) = if EVEN n then n+1 else n-1`;;
  (* "num" in HOL Light is the type {0,1,2,...}. *)
  (* Could have simply said "xor1 n = ...";
     type-checker will take n:num since EVEN wants num. *)
  (* Warning: If n:num is 0 then n-1 is 0 in HOL Light.
     This definition uses n-1 only for positive n. *)

let involution = new_definition
  `involution (f:A->A) <=> !x. f(f x) = x`;;
  (* "!x" in HOL Light is "for all x of this type".
     Type-checker automatically chooses type of x here
     as A since x is an f input (and an f output). *)

(* Simpler special case of built-in SURJ. *)
let surjection = new_definition
  `surjection (f:A->B) <=> !y. ?x. f x = y`;;
  (* "?x" in HOL Light is "there exists x of this type". *)

(* Simpler special case of built-in INJ. *)
let injection = new_definition
  `injection (f:A->B) <=> !x y. f x = f y ==> x = y`;;

(* Simpler special case of built-in BIJ. *)
let bijection = new_definition
  `bijection (f:A->B) <=> surjection f /\ injection f`;;
  (* /\ in HOL Light is "and". *)

(* Same as "inverse" in permutations.ml. *)
let inverse = new_definition
  `inverse (f:A->B) = \y. @x. f x = y`;;
  (* \y.f(y) in HOL Light is lambda notation
     for the function y|->f(y). *)
  (* @x.P(x) in HOL Light is some x such that P(x).
     Warning: returns an arbitrary element if P(x) is never true. *)

parse_as_infix("pow_num",(24,"left"));;
let pow_num = define
  `((p:A->A) pow_num n) =
    if n = 0 then (I:A->A) else (p o (p pow_num(n-1)))`;;
  (* "I" in HOL Light is the identity map. *)
  (* "define" is like "new_definition" but allows recursion. *)

parse_as_infix("pow_int",(24,"left"));;
let pow_int = new_definition
  `(p:A->A) pow_int (k:int)
    = if (&0 <= k) then (p pow_num(num_of_int k))
      else (inverse p pow_num(num_of_int(--k)))`;;
  (* "&" in HOL Light maps naturals to integers.
     Or to real numbers! Important to declare k as an int. *)
  (* "--k" in HOL Light is the negative of k. *)
  (* "num_of_int k" is @n. &n = k.
     Warning: returns an arbitrary natural if k is negative. *)

let cycle = new_definition
  `cycle (p:A->A) x = { y | ?k:int. y = (p pow_int k)(x) }`;;

let cyclemin = new_definition
  `cyclemin p x = (minimal) (cycle p x)`;;
  (* HOL Light defines minimal only for sets of naturals,
     so this definition forces p:num->num. *)

let partcycle = new_definition
  `partcycle (i:num) (p:A->A) x =
   { y | ?k:num. k < i /\ y = (p pow_num k)(x) }`;;

let part2powcycle = new_definition
  `part2powcycle (i:num) (p:A->A) x = partcycle (2 EXP i) p x`;;

let fastcyclemin = define
  `fastcyclemin i p x =
   if i = 0 then x else
   MIN (fastcyclemin (i-1) p x)
       (fastcyclemin (i-1) p ((p pow_num (2 EXP (i-1))) x))`;;

parse_as_infix("vanishesifonbothsidesof",(12,"right"));;
let vanishesifonbothsidesof = new_definition
  `(p:A->A) vanishesifonbothsidesof (q:A->A) <=> p o q o p = q`;;

let range = new_definition
  `range n = {m:num | m < n}`;;

parse_as_infix("subsetrange",(12,"right"));;
let subsetrange = new_definition
  `(s:num->bool) subsetrange n <=> !x. s x ==> x < n`;;

(* Part of "permutes" from permutations.ml. *)
(* There isn't a type {0,1,...,n-1} in HOL Light;
   easiest way to describe a permutation of {0,1,...,n-1}
   is as a permutation of the integers that fixes {n,n+1,...}. *)
parse_as_infix("fixesge",(12,"right"));;
let fixesge = new_definition
  `(p:num->num) fixesge n <=> !x. x >= n ==> p(x) = x`;;

let xif = new_definition
  `Xif s n = if s(n DIV 2) then xor1 n else n`;;

let XbackXforth = new_definition
  `XbackXforth p = p o xor1 o inverse p o xor1`;;

let firstcontrol = new_definition
  `firstcontrol p j = ODD(cyclemin(XbackXforth p)(2*j))`;;

let lastcontrol = new_definition
  `lastcontrol p k = ODD(Xif (firstcontrol p) (p(2*k)))`;;

let middleperm = new_definition
  `middleperm p = Xif(firstcontrol p) o p o Xif(lastcontrol p)`;;

(* ----- involution *)

let involution_I = prove(
  `involution (I:A->A)`,
  MESON_TAC[I_DEF;involution]);;

let involution_o = prove(
  `!f:A->A. involution f <=> f o f = I`,
  REWRITE_TAC[FUN_EQ_THM;o_THM;I_THM;involution]);;

(* ----- surjection *)

let surjection_ifinvolution = prove(
  `!p:A->A. involution p ==> surjection p`,
  REWRITE_TAC[involution;surjection] THEN
  REPEAT STRIP_TAC THEN
  EXISTS_TAC `(p:A->A)(y)` THEN
  ASM_MESON_TAC[]);;

let surjection_I = prove(
  `surjection (I:A->A)`,
  MESON_TAC[involution_I;surjection_ifinvolution]);;

let surjection_composes = prove(
  `!p:A->B q:B->C. surjection p /\ surjection q ==> surjection(q o p)`,
  REWRITE_TAC[surjection;o_THM] THEN
  MESON_TAC[]);;

(* ----- injection *)

let injection_ifinvolution = prove(
  `!(p:A->A). involution p ==> injection p`,
  REWRITE_TAC[involution;injection] THEN
  MESON_TAC[]);;

let injection_I = prove(
  `injection (I:A->A)`,
  MESON_TAC[involution_I;injection_ifinvolution]);;

let injection_composes = prove(
  `!p:A->B q:B->C. injection p /\ injection q ==> injection(q o p)`,
  REWRITE_TAC[injection] THEN
  REWRITE_TAC[o_THM] THEN
  MESON_TAC[]);;

(* ----- bijection *)

let bijection_ifinvolution = prove(
  `!p:A->A. involution p ==> bijection p`,
  MESON_TAC[surjection_ifinvolution;injection_ifinvolution;bijection]);;

let bijection_I = prove(
  `bijection (I:A->A)`,
  MESON_TAC[involution_I;bijection_ifinvolution]);;

let bijection_composes = prove(
  `!p:A->B q:B->C. bijection p /\ bijection q ==> bijection(q o p)`,
  REWRITE_TAC[bijection] THEN
  MESON_TAC[surjection_composes;injection_composes]);;

let bijection_inverseisinjection = prove(
  `!p:A->B. bijection p ==> injection(inverse p)`,
  REWRITE_TAC[bijection;surjection;injection;inverse] THEN
  MESON_TAC[]);;

let bijection_inverseissurjection = prove(
  `!p:A->B. bijection p ==> surjection(inverse p)`,
  REWRITE_TAC[bijection;surjection;injection;inverse] THEN
  MESON_TAC[]);;

let bijection_inverseisbijection = prove(
  `!p:A->B. bijection p ==> bijection(inverse p)`,
  MESON_TAC[bijection_inverseisinjection;
    bijection_inverseissurjection;bijection]);;

let bijection_inverse_composition1 = prove(
  `!p:A->B x. bijection p ==> p((inverse p)x) = x`,
  REWRITE_TAC[bijection;surjection;injection;inverse] THEN
  MESON_TAC[]);;

let bijection_inverse_composition2 = prove(
  `!p:A->B x. bijection p ==> (inverse p)(p x) = x`,
  REWRITE_TAC[bijection;surjection;injection;inverse] THEN
  MESON_TAC[]);;

let bijection_inverse_composition3 = prove(
  `!p:A->B. bijection p ==> !x. (p o inverse p)x = x`,
  MESON_TAC[bijection_inverse_composition1;o_THM]);;

let bijection_inverse_composition4 = prove(
  `!p:A->B. bijection p ==> !x. (inverse p o p)x = x`,
  MESON_TAC[bijection_inverse_composition2;o_THM]);;

let bijection_inverse_composition5 = prove(
  `!p:A->B. bijection p ==> p o inverse p = I`,
  MESON_TAC[bijection_inverse_composition3;I_THM;EQ_EXT]);;

let bijection_inverse_composition6 = prove(
  `!p:A->B. bijection p ==> inverse p o p = I`,
  MESON_TAC[bijection_inverse_composition4;I_THM;EQ_EXT]);;

let bijection_frominverse = prove(
  `!p:A->B q:B->A. q o p = I /\ p o q = I ==>
                   bijection p /\ q = inverse p`,
  REWRITE_TAC[bijection;surjection;injection;inverse] THEN
  MESON_TAC[I_THM;o_THM;EQ_EXT]);;

let bijection_matchinverse = prove(
  `!p:A->B. bijection p ==> !q:B->A. p o q = I ==> q = inverse p`,
  REWRITE_TAC[bijection;surjection;injection;inverse] THEN
  MESON_TAC[I_THM;o_THM;EQ_EXT]);;

let bijection_matchinverse2 = prove(
  `!p:A->B. bijection p ==> !q:B->A. q o p = I ==> q = inverse p`,
  REWRITE_TAC[bijection;surjection;injection;inverse] THEN
  MESON_TAC[I_THM;o_THM;EQ_EXT]);;

let bijection_inverse_inverse = prove(
  `!p:A->B. bijection p ==> inverse(inverse p) = p`,
  MESON_TAC[bijection_inverse_composition5;
    bijection_inverse_composition6;bijection_frominverse]);;

(* ----- EVEN, ODD *)

let suc_isadd1 = prove(
  `!n. SUC n = n+1`,
  MESON_TAC[ONE;ADD_SUC;ADD_0]);;

let nonzero_sub1add1 = prove(
  `!n. ~(n = 0) ==> (n-1)+1 = n`,
  MESON_TAC[LTE_CASES;LE_1;SUB_ADD]);;

let nonzero_subsuc = prove(
  `!n. ~(n = 0) ==> SUC(n-1) = n`,
  MESON_TAC[nonzero_sub1add1;suc_isadd1]);;

let nonzero_pre_le_suc = prove(
  `!n. ~(n = 0) ==> n-1 <= SUC(n-1)`,
  MESON_TAC[LE_REFL;LE]);;

let pre_le_ifnonzero = prove(
  `!n. ~(n = 0) ==> n-1 <= n`,
  MESON_TAC[nonzero_pre_le_suc;nonzero_subsuc]);;

let pre_le_ifzero = prove(
  `!n. n = 0 ==> n-1 <= n`,
  CONV_TAC ARITH_RULE);;

let pre_le = prove(
  `!n. n-1 <= n`,
  MESON_TAC[pre_le_ifzero;pre_le_ifnonzero]);;

let even_odd_add1 = prove(
  `!n. EVEN n ==> ODD(n+1)`,
  REWRITE_TAC[ODD_ADD;ODD;EVEN;ONE;NOT_ODD]);;

let even_add1_odd = prove(
  `!n. EVEN(n+1) ==> ODD n`,
  MESON_TAC[ONE;NOT_EVEN;EVEN_ADD;EVEN;ODD]);;

let odd_even_sub1 = prove(
  `!n. ODD n ==> EVEN(n-1)`,
  MESON_TAC[EVEN_SUB;ODD;EVEN;NOT_EVEN;ONE;LTE_CASES]);;

let odd_sub1add1 = prove(
  `!n. ODD n ==> (n-1)+1 = n`,
  MESON_TAC[nonzero_sub1add1;ODD]);;

let odd_sub1distinct = prove(
  `!n. ODD n ==> ~(n-1 = n)`,
  GEN_TAC THEN
  ASSUME_TAC(ARITH_RULE `~(n-1 = (n-1)+1)`) THEN
  ASM_MESON_TAC[odd_sub1add1]);;

let odd_isdoubleplus1 = prove(
  `!n. ODD n ==> ?m. n = 2*m+1`,
  MESON_TAC[ODD_EXISTS;suc_isadd1]);;

let sandwich_suc = prove(
  `!m n. m < n /\ n <= SUC m ==> SUC m = n`,
  MESON_TAC[LE_ANTISYM;LE_SUC_LT]);;

let sandwich_add1 = prove(
  `!m n. m < n /\ n <= m+1 ==> m+1 = n`,
  MESON_TAC[sandwich_suc;suc_isadd1]);;

let sandwich_even_add1_odd = prove(
  `!n b. n < 2*b /\ 2*b <= n+1 ==> ODD n`,
  MESON_TAC[EVEN_DOUBLE;sandwich_add1;even_add1_odd;NOT_EVEN]);;

(* ----- range *)

let empty_ifnever = prove(
  `!s:A->bool. (!x. ~(x IN s)) ==> s = EMPTY`,
  REWRITE_TAC[IN;FUN_EQ_THM;EMPTY;IN_ELIM_THM]);;

let range_in = prove(
  `!k n. k IN range n <=> k < n`,
  MESON_TAC[range;IN_ELIM_THM]);;

let range_in_flip = prove(
  `!k n. k < n <=> k IN range n`,
  MESON_TAC[range_in]);;

let range_0_lemma = prove(
  `!x. ~(x IN range 0)`,
  REWRITE_TAC[range;IN_ELIM_THM] THEN
  ARITH_TAC);;

let range_0 = prove(
  `range 0 = EMPTY`,
  MESON_TAC[empty_ifnever;range_0_lemma]);;

let range_suc = prove(
  `!n. range(SUC n) = n INSERT range n`,
  REWRITE_TAC[range;INSERT;FUN_EQ_THM;IN_ELIM_THM;LT] THEN
  MESON_TAC[]);;

let range_plus1 = prove(
  `!n. range(n+1) = n INSERT range n`,
  MESON_TAC[range_suc;suc_isadd1]);;

let range_finite = prove(
  `!n. FINITE(range n)`,
  INDUCT_TAC THEN
  ASM_MESON_TAC[FINITE_RULES;range_0;range_suc]);;

let range_card_0 = prove(
  `CARD(range 0) = 0`,
  MESON_TAC[range_0;CARD_CLAUSES]);;

let range_card_lemma = prove(
  `!n. ~(n IN range n)`,
  REWRITE_TAC[range;IN;IN_ELIM_THM] THEN
  ARITH_TAC);;

let range_card = prove(
  `!n. CARD(range n) = n`,
  INDUCT_TAC THEN
  REWRITE_TAC[range_card_0] THEN
  REWRITE_TAC[range_suc] THEN
  ASM_MESON_TAC[CARD_CLAUSES;range_finite;range_card_lemma]);;

(* ----- xor1 *)

let xor1_double = prove(
  `!n. xor1 (2*n) = 2*n+1`,
  ASM_SIMP_TAC[xor1;EVEN_DOUBLE]);;

let xor1_distinct = prove(
  `!n. ~(xor1 n = n)`,
  REWRITE_TAC[xor1] THEN
  GEN_TAC THEN
  ASSUME_TAC(ARITH_RULE `~(n+1 = n)`) THEN
  ASSUME_TAC(SPEC `n:num` odd_sub1distinct) THEN
  DISJ_CASES_TAC (SPEC `n:num` EVEN_OR_ODD) THEN
  ASM_SIMP_TAC[] THEN
  ASM_MESON_TAC[NOT_ODD]);;

let xor1_oneven_isadd1 = prove(
  `!n. EVEN n ==> xor1 n = n+1`,
  MESON_TAC[xor1]);;

let xor1_oneven_isodd = prove(
  `!n. EVEN n ==> ODD(xor1 n)`,
  MESON_TAC[even_odd_add1;xor1]);;

let xor1_onodd_issub1 = prove(
  `!n. ODD n ==> xor1 n = n-1`,
  MESON_TAC[NOT_EVEN;xor1]);;

let xor1_onodd_iseven = prove(
  `!n. ODD n ==> EVEN(xor1 n)`,
  MESON_TAC[xor1_onodd_issub1;odd_even_sub1]);;

let xor1_parity = prove(
  `!n. ODD(xor1 n) <=> ~ODD n`,
  MESON_TAC[xor1_onodd_iseven;xor1_oneven_isodd;NOT_EVEN]);;

let xor1xor1_ifeven = prove(
  `!n. EVEN n ==> xor1(xor1 n) = n`,
  MESON_TAC[xor1_oneven_isodd;xor1_onodd_issub1;
    xor1_oneven_isadd1;ARITH_RULE `(n+1)-1 = n`]);;

let xor1xor1_ifodd = prove(
  `!n. ODD n ==> xor1(xor1 n) = n`,
  MESON_TAC[xor1_onodd_iseven;xor1_onodd_issub1;
    xor1_oneven_isadd1;odd_sub1add1]);;

let xor1xor1 = prove(
  `!n. xor1(xor1 n) = n`,
  MESON_TAC[xor1xor1_ifodd;xor1xor1_ifeven;EVEN_OR_ODD]);;

let xor1_involution_o = prove(
  `xor1 o xor1 = I`,
  REWRITE_TAC[I_DEF;o_DEF;xor1xor1]);;

let xor1_involution = prove(
  `involution xor1`,
  MESON_TAC[xor1xor1;involution]);;

let xor1_lteven = prove(
  `!n b. n < 2*b ==> xor1 n < 2*b`,
  REWRITE_TAC[xor1] THEN
  ASM_CASES_TAC(`EVEN n`) THEN
  MESON_TAC[LTE_CASES;sandwich_even_add1_odd;
    pre_le;NOT_EVEN;LET_TRANS]);;

let xor1_geeven = prove(
  `!n b. n >= 2*b ==> xor1 n >= 2*b`,
  MESON_TAC[xor1xor1;xor1_lteven;NOT_LT;GE]);;

let xor1_lemma101 = prove(
  `!m n. EVEN m ==> EVEN n ==> ~(n = m + 1)`,
  MESON_TAC[even_odd_add1;NOT_ODD]);;

let xor1_lemma102 = prove(
  `!m n. EVEN m ==> EVEN n ==> n <= m + 1 ==> n <= m`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPEC `m:num` suc_isadd1) THEN
  ASM_MESON_TAC[xor1_lemma101;LE_LT;LT_SUC_LE]);;

let xor1_lemma103 = prove(
  `!m n. EVEN m ==> EVEN n ==> m < xor1 n /\ n <= xor1 m ==> m = n`,
  REWRITE_TAC[xor1] THEN
  REPEAT STRIP_TAC THEN
  ASM_SIMP_TAC[] THEN
  ASSUME_TAC(ARITH_RULE `n <= m /\ m < n + 1 ==> m = n`) THEN
  ASM_MESON_TAC[xor1_lemma102]);;

let xor1_lemma104 = prove(
  `!m n. ~EVEN m ==> ~EVEN n ==> m < xor1 n ==> xor1 m < n`,
  REPEAT GEN_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
  REWRITE_TAC[xor1] THEN
  ASM_SIMP_TAC[] THEN
  ARITH_TAC);;

let xor1_lemma105 = prove(
  `!m n. ~EVEN m ==> EVEN n ==> m < xor1 n /\ n <= xor1 m ==> m = n`,
  REPEAT GEN_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
  REWRITE_TAC[xor1] THEN
  ASM_SIMP_TAC[] THEN
  ARITH_TAC);;

let xor1_lemma106 = prove(
  `!m n. EVEN m ==> ~EVEN n ==> m < xor1 n ==> xor1 m < n`,
  REPEAT GEN_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
  REWRITE_TAC[xor1] THEN
  ASM_SIMP_TAC[] THEN
  ARITH_TAC);;

let xor1_lemma107 = prove(
  `!m n. m < xor1 n /\ n <= xor1 m ==> m = n`,
  REPEAT GEN_TAC THEN
  DISJ_CASES_TAC (TAUT `EVEN m \/ ~EVEN m`) THEN
  DISJ_CASES_TAC (TAUT `EVEN n \/ ~EVEN n`) THEN
  ASM_MESON_TAC[NOT_LT;xor1_lemma103;xor1_lemma104;
                       xor1_lemma105;xor1_lemma106]);;

let xor1_sandwich = prove(
  `!m n. m <= xor1 n /\ n <= xor1 m /\ ~(m = n) ==> m = xor1 n`,
  MESON_TAC[xor1_lemma107;LE_LT]);;

(* ----- DIV 2 *)

let double_div2 = prove(
  `!n. (2*n) DIV 2 = n`,
  MESON_TAC[DIV_MULT;ARITH_RULE `~(2 = 0)`]);;

let double_flip_plus1_div2 = prove(
  `!n. (n*2+1) DIV 2 = n`,
  MESON_TAC[DIVMOD_UNIQ;ARITH_RULE `(1 < 2)`]);;

let double_plus1_div2 = prove(
  `!n. (2*n+1) DIV 2 = n`,
  MESON_TAC[double_flip_plus1_div2;ARITH_RULE `2*n = n*2`]);;

let double_orplus1_div2 = prove(
  `!n. (2*n+1) DIV 2 = (2*n) DIV 2`,
  MESON_TAC[double_div2;double_plus1_div2]);;

let double_plus1_orminus1_div2 = prove(
  `!n. (2*n+1) DIV 2 = ((2*n+1)-1) DIV 2`,
  MESON_TAC[double_orplus1_div2;ARITH_RULE `(2*n+1)-1 = 2*n`]);;

let double_suc_orminus1_div2 = prove(
  `!n. SUC(2*n) DIV 2 = (SUC(2*n)-1) DIV 2`,
  MESON_TAC[suc_isadd1;double_plus1_orminus1_div2]);;

let xor1_div2 = prove(
  `!n. xor1 n DIV 2 = n DIV 2`,
  REWRITE_TAC[xor1] THEN
  GEN_TAC THEN
  ASM_CASES_TAC `EVEN n` THEN
  ASM_SIMP_TAC[] THENL
  [
    ASSUME_TAC(SPEC `n:num` EVEN_EXISTS) THEN
    ASM_MESON_TAC[double_orplus1_div2]
  ;
    ASSUME_TAC(SPEC `n:num` EVEN_EXISTS_LEMMA) THEN
    ASM_MESON_TAC[double_suc_orminus1_div2]
  ]);;

let div2_lt_doubling = prove(
  `!x b. x DIV 2 < b ==> x < 2*b`,
  MESON_TAC[RDIV_LT_EQ;ARITH_RULE `~(2 = 0)`]);;

let div2_lt_doubling_ge = prove(
  `!x b. x DIV 2 < b ==> ~(x >= 2*b)`,
  MESON_TAC[div2_lt_doubling;NOT_LT;GE]);;

(* ----- pow_num: natural powers of a function from A to A *)

let pow_num_eval = prove(
  `!p:A->A. !n. ~(n = 0) ==> !x. (p pow_num n)x = p((p pow_num(n-1))x)`,
  ASM_MESON_TAC[pow_num;o_DEF]);;

let pow_num_0 = prove(
  `!p:A->A. p pow_num 0 = I`,
  REWRITE_TAC[pow_num]);;

let pow_num_0_eval = prove(
  `!p:A->A. !x. (p pow_num 0)x = x`,
  REWRITE_TAC[pow_num_0;I_DEF]);;

let pow_num_11 = prove(
  `!p:A->A. p pow_num (1-1) = I`,
  REWRITE_TAC[ARITH_RULE `1-1=0`;pow_num_0]);;

let pow_num_111 = prove(
  `!p:A->A. p o (p pow_num (1-1)) = p`,
  REWRITE_TAC[pow_num_11;I_O_ID]);;

let pow_num_1 = prove(
  `!p:A->A. p pow_num 1 = p`,
  ASM_MESON_TAC[pow_num;pow_num_111;ARITH_RULE `~(1 = 0)`]);;

let pow_num_1_eval = prove(
  `!p:A->A. !x. (p pow_num 1) x = p x`,
  REWRITE_TAC[pow_num_1]);;

let pow_num_n11 = prove(
  `!n p:A->A. p pow_num(n+1) = p o (p pow_num((n+1)-1))`,
  ASM_MESON_TAC[pow_num;ARITH_RULE `~(n+1 = 0)`]);;

let pow_num_plus1 = prove(
  `!n p:A->A. p pow_num(n+1) = p o (p pow_num n)`,
  ASM_MESON_TAC[pow_num_n11;ARITH_RULE `(n+1)-1 = n`]);;

let pow_num_plus1_eval = prove(
  `!n p:A->A. !x. (p pow_num(n+1)) x = p((p pow_num n) x)`,
  ASM_MESON_TAC[pow_num_plus1;o_DEF]);;

let pow_num_plus_flip = prove(
  `!m n p:A->A. p pow_num(n+m) = (p pow_num m) o (p pow_num n)`,
  INDUCT_TAC THENL [
    REWRITE_TAC[pow_num_0;I_O_ID;ARITH_RULE `n+0 = n`]
  ;
    REWRITE_TAC[suc_isadd1;ARITH_RULE `n+m+1 = (n+m)+1`;
                pow_num_plus1] THEN
    ASM_MESON_TAC[o_ASSOC]
  ]);;

let pow_num_plus_flip_eval = prove(
  `!m n p:A->A. !x. (p pow_num(n+m))x = (p pow_num m)((p pow_num n) x)`,
  ASM_MESON_TAC[pow_num_plus_flip;o_DEF]);;

let pow_num_plus = prove(
  `!m n p:A->A. p pow_num(m+n) = (p pow_num m) o (p pow_num n)`,
  MESON_TAC[pow_num_plus_flip;ARITH_RULE `n+m = m+n`]);;

let pow_num_plus_eval = prove(
  `!m n p:A->A. !x. (p pow_num(m+n))x = (p pow_num m)((p pow_num n) x)`,
  MESON_TAC[pow_num_plus_flip_eval;ARITH_RULE `n+m = m+n`]);;

let pow_num_plus1_right = prove(
  `!n p:A->A. p pow_num(n+1) = (p pow_num n) o p`,
  MESON_TAC[pow_num_plus;pow_num_1]);;

let pow_num_plus1_right_eval = prove(
  `!n p:A->A. !x. (p pow_num(n+1))x = (p pow_num n)(p x)`,
  MESON_TAC[pow_num_plus1_right;o_DEF]);;

let pow_num_bijection = prove(
  `!p:A->A. bijection p ==> !n. bijection (p pow_num n)`,
  GEN_TAC THEN DISCH_TAC THEN
  INDUCT_TAC THENL
  [ REWRITE_TAC[pow_num_0;bijection_I]
  ; REWRITE_TAC[suc_isadd1] THEN
    ASM_MESON_TAC[pow_num_plus1;bijection_composes]
  ]);;

let pow_num_plus1_bijection = prove(
  `!n p:A->A. bijection p ==>
              inverse p o (p pow_num(n+1)) = p pow_num n`,
  REWRITE_TAC[pow_num_plus1] THEN
  MESON_TAC[bijection_inverse_composition6;o_ASSOC;I_O_ID]);;

let pow_num_plus1_inverse = prove(
  `!n p:A->A. bijection p ==>
              p o ((inverse p) pow_num(n+1)) = (inverse p) pow_num n`,
  MESON_TAC[pow_num_plus1_bijection;
    bijection_inverseisbijection;bijection_inverse_inverse]);;

(* ----- pow_int: integer powers of a permutation of A *)

let pow_int_num = prove(
  `!p:A->A n. p pow_num n = p pow_int &n`,
  REWRITE_TAC[pow_int] THEN
  REPEAT GEN_TAC THEN
  SIMP_TAC[INT_ARITH `((&0):int) <= &n`] THEN
  MESON_TAC[NUM_OF_INT_OF_NUM] THEN
  ASM_SIMP_TAC[]);;

let pow_int_0 = prove(
  `!p:A->A. p pow_int &0 = I`,
  REWRITE_TAC[pow_int;NUM_OF_INT_OF_NUM;pow_num_0] THEN
  SIMP_TAC[INT_ARITH `&0:int <= &0`]);;

let pow_int_1 = prove(
  `!p:A->A. p pow_int &1 = p`,
  REWRITE_TAC[pow_int;NUM_OF_INT_OF_NUM;pow_num_1] THEN
  SIMP_TAC[INT_ARITH `&0:int <= &1`]);;

let pow_int_bijection_nonnegative = prove(
  `!p:A->A. bijection p ==> !k:int. &0 <= k ==> bijection (p pow_int k)`,
  REPEAT STRIP_TAC THEN
  REWRITE_TAC[pow_int] THEN
  ASM_SIMP_TAC[] THEN
  ASM_MESON_TAC[pow_num_bijection]);;

let pow_int_bijection_negative = prove(
  `!p:A->A. !k:int. bijection p /\ k < &0 ==> bijection (p pow_int k)`,
  REPEAT STRIP_TAC THEN
  REWRITE_TAC[pow_int] THEN
  ASM_MESON_TAC[pow_num_bijection;bijection_inverseisbijection]);;

let pow_int_bijection = prove(
  `!p:A->A. !k:int. bijection p ==> bijection (p pow_int k)`,
  REPEAT STRIP_TAC THEN
  DISJ_CASES_TAC(INT_ARITH `k:int < &0 \/ &0 <= k`) THENL
  [ ASM_MESON_TAC[pow_int_bijection_negative]
  ; ASM_MESON_TAC[pow_int_bijection_nonnegative]
  ]);;

let pow_int_cancel = prove(
  `!p:A->A k x y. bijection p ==>
                  (p pow_int k) x = (p pow_int k) y ==> x = y`,
  REPEAT GEN_TAC THEN
  ASSUME_TAC(SPEC `p:A->A` pow_int_bijection) THEN
  ASM_MESON_TAC[bijection;injection]);;

let pow_int_plus1_nonnegative = prove(
  `!p:A->A. !k:int. &0 <= k ==> p pow_int(k + &1) = p o (p pow_int k)`,
  REWRITE_TAC[pow_int] THEN
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(INT_ARITH `&0 <= k:int ==> &0 <= k + &1`) THEN
  ASSUME_TAC(SPEC `p:A->A`(SPEC `num_of_int(k:int)` pow_num_plus1)) THEN
  ASSUME_TAC(INT_ARITH `(&0:int) <= &1`) THEN
  ASSUME_TAC(SPEC `1` NUM_OF_INT_OF_NUM) THEN
  ASSUME_TAC(SPECL[`k:int`;`&1:int`]NUM_OF_INT_ADD) THEN
  SUBGOAL_THEN `&0 <= (k:int) + &1` ASSUME_TAC THEN
  ASM_SIMP_TAC[] THEN
  ASM_MESON_TAC[]);;

let int_negative_num_towards0 = prove(
  `!k:int. k < &0 ==> num_of_int(--(k + &1)) + 1 = num_of_int(--k)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPECL[`--((k:int) + &1)`;`&1:int`]NUM_OF_INT_ADD) THEN
  ASSUME_TAC(INT_ARITH `k:int < &0 ==> &0 <= --(k + &1)`) THEN
  ASSUME_TAC(INT_ARITH `--((k:int) + &1) + &1 = --k`) THEN
  ASSUME_TAC(INT_ARITH `(&0:int) <= &1`) THEN
  ASSUME_TAC(SPEC `1` NUM_OF_INT_OF_NUM) THEN
  ASM_MESON_TAC[]);;

let pow_int_plus1_negative = prove(
  `!p:A->A. bijection p ==> !k:int. k < &0 ==>
            p pow_int(k + &1) = p o (p pow_int k)`,
  REWRITE_TAC[pow_int] THEN
  REPEAT STRIP_TAC THEN
  DISJ_CASES_TAC(INT_ARITH `-- &1 <= k:int \/ k < -- &1`) THENL
  [
    ASSUME_TAC(INT_ARITH `-- &1 <= (k:int) /\ k < &0 ==> k = -- &1`) THEN
    ASSUME_TAC(INT_ARITH `k:int = -- &1 ==> ~(&0 <= k)`) THEN
    ASSUME_TAC(INT_ARITH `k:int = -- &1 ==> &0 <= k + &1`) THEN
    ASSUME_TAC(INT_ARITH `-- -- &1:int = &1`) THEN
    ASSUME_TAC(INT_ARITH `-- (&1:int) + &1 = &0`) THEN
    ASSUME_TAC(SPEC `1` NUM_OF_INT_OF_NUM) THEN
    ASSUME_TAC(SPEC `0` NUM_OF_INT_OF_NUM) THEN
    ASSUME_TAC(SPEC `p:A->A` pow_num_0) THEN
    ASSUME_TAC(SPEC `inverse(p:A->A)` pow_num_1) THEN
    ASM_SIMP_TAC[] THEN
    ASM_MESON_TAC[bijection_inverse_composition5]
  ;
    ASSUME_TAC(INT_ARITH `k:int < -- &1 ==> ~(&0 <= k)`) THEN
    ASSUME_TAC(INT_ARITH `k:int < -- &1 ==> ~(&0 <= k + &1)`) THEN
    ASSUME_TAC(SPEC `k:int` int_negative_num_towards0) THEN
    ASSUME_TAC(SPECL[`num_of_int(--((k:int) + &1))`;
                     `p:A->A`]pow_num_plus1_inverse) THEN
    ASM_MESON_TAC[]
  ]);;

let pow_int_plus1 = prove(
  `!p:A->A. bijection p ==> !k:int.
            p pow_int(k + &1) = p o (p pow_int k)`,
  REPEAT STRIP_TAC THEN
  DISJ_CASES_TAC(INT_ARITH `k:int < &0 \/ &0 <= k`)
  THENL[ASM_MESON_TAC[pow_int_plus1_negative];
    ASM_MESON_TAC[pow_int_plus1_nonnegative]]);;

let pow_int_plusnum = prove(
  `!p:A->A. bijection p ==> !m. !k:int.
            p pow_int(k + &m) = (p pow_num m) o (p pow_int k)`,
  GEN_TAC THEN DISCH_TAC THEN
  INDUCT_TAC THENL
  [
    ASSUME_TAC(INT_ARITH `(k:int) + &0 = k`) THEN
    ASM_SIMP_TAC[] THEN
    REWRITE_TAC[pow_num_0;I_O_ID]
  ;
    GEN_TAC THEN
    REWRITE_TAC[suc_isadd1;pow_num_plus1] THEN
    ASSUME_TAC(INT_ARITH `(k:int) + (&m + &1) = (k + &m) + &1`) THEN
    ASSUME_TAC(SPECL[`m:num`;`1:num`]INT_OF_NUM_ADD) THEN
    ASM_MESON_TAC[o_ASSOC;pow_int_plus1]
  ]);;

let pow_int_plus_nonnegative = prove(
  `!p:A->A. bijection p ==> !j:int. &0 <= j ==>
    !k:int. p pow_int(k + j) = (p pow_int j) o (p pow_int k)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPEC `j:int` NUM_OF_INT) THEN
  ASM_MESON_TAC[pow_int_plusnum;pow_int]);;

let pow_int_inverse_lemma1 = prove(
  `!p:A->A. bijection p ==> !j:int. &0 <= j ==>
    p pow_int(--j + j) = (p pow_int j) o (p pow_int --j)`,
  MESON_TAC[pow_int_plus_nonnegative]);;

let pow_int_inverse_lemma2 = prove(
  `!p:A->A. bijection p ==> !j:int. &0 <= j ==>
    p pow_int &0 = (p pow_int j) o (p pow_int --j)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(INT_ARITH `--j + (j:int) = &0`) THEN
  ASM_MESON_TAC[pow_int_inverse_lemma1]);;

let pow_int_inverse_lemma3 = prove(
  `!p:A->A. bijection p ==> !j:int. &0 <= j ==>
    (p pow_int j) o (p pow_int --j) = I`,
  MESON_TAC[pow_int_inverse_lemma2;pow_int_0]);;

let pow_int_inverse_nonnegative = prove(
  `!p:A->A. bijection p ==> !j:int. &0 <= j ==>
    p pow_int --j = inverse(p pow_int j)`,
  MESON_TAC[pow_int_bijection;bijection_matchinverse;
                pow_int_inverse_lemma3]);;

let pow_int_inverse_negative = prove(
  `!p:A->A. bijection p ==> !j:int. j < &0 ==>
    p pow_int --j = inverse(p pow_int j)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ARITH_RULE `(j:int) < &0 ==> &0 <= --j`) THEN
  ASSUME_TAC(ARITH_RULE `(j:int) = -- --j`) THEN
  ASM_MESON_TAC[pow_int_bijection;
    bijection_inverse_inverse;pow_int_inverse_nonnegative]);;

let pow_int_inverse = prove(
  `!p:A->A. !j:int. bijection p ==>
    p pow_int --j = inverse(p pow_int j)`,
  REPEAT STRIP_TAC THEN
  DISJ_CASES_TAC(INT_ARITH `j:int < &0 \/ &0 <= j`) THENL
  [ ASM_MESON_TAC[pow_int_inverse_negative]
  ; ASM_MESON_TAC[pow_int_inverse_nonnegative]
  ]);;

let pow_int_plus_lemma1 = prove(
  `!p:A->A. bijection p ==> !j:int. j < &0 ==>
    !k:int. p pow_int(k + --j) = (p pow_int --j) o (p pow_int k)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ARITH_RULE `(j:int) < &0 ==> &0 <= --j`) THEN
  ASM_MESON_TAC[pow_int_plus_nonnegative]);;

let pow_int_plus_lemma2 = prove(
  `!p:A->A. !j:int. !k:int. bijection p /\ j < &0 ==>
    p pow_int(k - j) = (p pow_int --j) o (p pow_int k)`,
  REPEAT STRIP_TAC THEN
  REWRITE_TAC[ARITH_RULE `(k:int)-(j:int) = k + --j`] THEN
  ASM_MESON_TAC[pow_int_plus_lemma1]);;

let pow_int_plus_lemma3 = prove(
  `!p:A->A. !j:int. !k:int. bijection p /\ j < &0 ==>
    p pow_int(k-j) = inverse(p pow_int j) o (p pow_int k)`,
  MESON_TAC[pow_int_plus_lemma2;pow_int_inverse;pow_int_bijection]);;

let pow_int_plus_lemma4 = prove(
  `!p:A->A j:int k:int. bijection p /\ j < &0 ==>
    (p pow_int j) o (p pow_int(k-j)) = p pow_int k`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPECL[`p:A->A`;`j:int`;`k:int`]pow_int_plus_lemma3) THEN
  ASSUME_TAC(SPECL[`p:A->A`;`j:int`]pow_int_bijection) THEN
  ASSUME_TAC(ISPEC `(p:A->A) pow_int (j:int)`
                   bijection_inverse_composition5) THEN
  ASM_MESON_TAC[o_ASSOC;I_O_ID]);;

let pow_int_plus_negative = prove(
  `!p:A->A. bijection p ==> !j:int. j < &0 ==>
    !k:int. (p pow_int j) o (p pow_int k) = p pow_int (k+j)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPECL[`p:A->A`;`j:int`;`(k:int)+j`]
                  pow_int_plus_lemma4) THEN
  ASSUME_TAC(ARITH_RULE `((k:int)+(j:int))-j=k`) THEN
  ASM_MESON_TAC[]);;

let pow_int_plus_swap = prove(
  `!p:A->A j:int k:int. bijection p ==>
    p pow_int(k+j) = (p pow_int j) o (p pow_int k)`,
  REPEAT STRIP_TAC THEN
  DISJ_CASES_TAC(INT_ARITH `j:int < &0 \/ &0 <= j`) THENL
  [ ASM_MESON_TAC[pow_int_plus_negative]
  ; ASM_MESON_TAC[pow_int_plus_nonnegative]
  ]);;

let pow_int_plus = prove(
  `!p:A->A j:int k:int. bijection p ==>
    p pow_int(j+k) = (p pow_int j) o (p pow_int k)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ARITH_RULE `(k:int)+(j:int)=j+k`) THEN
  ASM_MESON_TAC[pow_int_plus_swap]);;

let pow_int_plus_eval = prove(
  `!p:A->A j:int k:int x. bijection p ==>
    (p pow_int(j+k))x = (p pow_int j)((p pow_int k)x)`,
  MESON_TAC[pow_int_plus;o_THM]);;

let pow_int_cancel2 = prove(
  `!p:A->A x j k. bijection p ==>
   (p pow_int j) x = (p pow_int k) x ==> x = (p pow_int (k-j)) x`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ISPECL[`p:A->A`;`j:int`;`k:int-j:int`]
             pow_int_plus_eval) THEN
  ASSUME_TAC(ARITH_RULE `(j:int)+(k-j)=(k:int)`) THEN
  ASSUME_TAC(ISPECL[`p:A->A`;`j:int`;`x:A`;
                    `((p:A->A) pow_int (k-j)) (x:A)`]
                    pow_int_cancel) THEN
  ASM_MESON_TAC[]);;

let pow_int_cancel_num = prove(
  `!p:A->A x j k. bijection p ==>
   (p pow_num j) x = (p pow_num k) x ==>
   x = (p pow_int (&k - &j)) x`,
  MESON_TAC[pow_int_num;pow_int_cancel2]);;

let pow_int_cancel_num2 = prove(
  `!p:A->A x j k. bijection p ==>
   (p pow_num j) x = (p pow_num k) x /\ j <= k
   ==> x = (p pow_num (k-j)) x`,
  MESON_TAC[pow_int_cancel_num;INT_OF_NUM_SUB;pow_int_num]);;

(* ----- cycle *)

let cycle_contains_start = prove(
  `!p:A->A x. x IN cycle p x`,
  REPEAT GEN_TAC THEN
  REWRITE_TAC[cycle;IN_ELIM_THM] THEN
  EXISTS_TAC `&0:int` THEN
  REWRITE_TAC[pow_int_0;I_THM]);;

let cycle_lemma1 = prove(
  `!p:A->A x y k. bijection p /\ y = (p pow_int k) (p x) ==>
    y = (p pow_int (k + &1)) x`,
  REPEAT STRIP_TAC THEN
  ASM_SIMP_TAC[pow_int_plus_eval;pow_int_1]);;

let cycle_lemma2 = prove(
  `!p:A->A x y k. bijection p /\ y = (p pow_int k) (p x) ==>
    y IN cycle p x`,
  REPEAT STRIP_TAC THEN
  REWRITE_TAC[cycle;IN_ELIM_THM] THEN
  EXISTS_TAC `(k:int) + &1` THEN
  ASM_MESON_TAC[cycle_lemma1]);;

let cycle_lemma3 = prove(
  `!p:A->A x y. y IN cycle p x ==> ?k:int. y = (p pow_int k)(x)`,
  REWRITE_TAC[cycle;IN_ELIM_THM]);;

let cycle_lemma4 = prove(
  `!p:A->A x y k. bijection p /\ y = (p pow_int k) x ==>
    y = (p pow_int (k - &1)) (p x)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(INT_ARITH `(k:int) = (k - &1) + &1`) THEN
  ASM_MESON_TAC[pow_int_plus_eval;pow_int_1]);;

let cycle_lemma5 = prove(
  `!p:A->A x y k. bijection p /\ y = (p pow_int k) x ==>
    y IN cycle p (p x)`,
  REPEAT STRIP_TAC THEN
  REWRITE_TAC[cycle;IN_ELIM_THM] THEN
  EXISTS_TAC `(k:int) - &1` THEN
  ASM_MESON_TAC[cycle_lemma4]);;

let cycle_shift_forward = prove(
  `!p:A->A x y. bijection p ==> y IN cycle p (p x) ==> y IN cycle p x`,
  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC cycle_lemma2 THEN
  ASM_MESON_TAC[cycle_lemma3]);;

let cycle_shift_backward = prove(
  `!p:A->A x y. bijection p ==> y IN cycle p x ==> y IN cycle p (p x)`,
  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC cycle_lemma5 THEN
  ASM_MESON_TAC[cycle_lemma3]);;

let cycle_shift = prove(
  `!p:A->A x. bijection p ==> cycle p (p x) = cycle p x`,
  MESON_TAC[cycle_shift_backward;cycle_shift_forward;EXTENSION]);;

let cycle_ifpow = prove(
  `!p:A->A x y k. y = (p pow_int k) x ==> y IN cycle p x`,
  REWRITE_TAC[cycle;IN_ELIM_THM] THEN
  MESON_TAC[]);;

let cycle_aspow = prove(
  `!p:A->A x y. y IN cycle p x ==> ?k. y = (p pow_int k) x`,
  REWRITE_TAC[cycle;IN_ELIM_THM]);;

(* ----- cyclemin *)

let cyclemin_in_cycle = prove(
  `!p x. cyclemin p x IN cycle p x`,
  REPEAT GEN_TAC THEN
  REWRITE_TAC[IN] THEN
  REWRITE_TAC[cyclemin] THEN
  MATCH_MP_TAC(prove(`!P. (?n. P n) ==> P((minimal) P)`,
                     MESON_TAC[MINIMAL])) THEN
  ASSUME_TAC(ISPECL[`p:num->num`;`x:num`]cycle_contains_start) THEN
  ASM_MESON_TAC[IN]);;

let cyclemin_le = prove(
  `!p x. cyclemin p x <= x`,
  REPEAT GEN_TAC THEN
  REWRITE_TAC[cyclemin] THEN
  MATCH_MP_TAC MINIMAL_UBOUND THEN
  MESON_TAC[cycle_contains_start;IN]);;

let cyclemin_0 = prove(
  `!p. cyclemin p 0 = 0`,
  MESON_TAC[cyclemin_le;LE_0;LE_ANTISYM]);;

let cyclemin_shift = prove(
  `!p x. bijection p ==> cyclemin p (p x) = cyclemin p x`,
  MESON_TAC[cycle_shift;cyclemin]);;

let cyclemin_aspow = prove(
  `!p x. ?k. cyclemin p x = (p pow_int k) x`,
  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC cycle_aspow THEN
  ASM_MESON_TAC[cyclemin_in_cycle]);;

(* ----- MIN and minimal *)

let min_le_first = prove(
  `!m n. MIN m n <= m`,
  REWRITE_TAC[MIN] THEN
  MESON_TAC[LE_REFL;NOT_LE;LT_LE]);;

let min_le_second = prove(
  `!m n. MIN m n <= n`,
  REWRITE_TAC[MIN] THEN
  MESON_TAC[LE_REFL;NOT_LE;LT_LE]);;

let minimal_union_le = prove(
  `!s:num->bool t:num->bool.
    ~(s = EMPTY) ==> (minimal) (s UNION t) <= (minimal) s`,
  MESON_TAC[CHOICE_DEF;MINIMAL;IN;IN_UNION;MINIMAL_UBOUND]);;

let minimal_union_le_min = prove(
  `!s:num->bool t:num->bool.
   ~(s = EMPTY) ==> ~(t = EMPTY) ==>
   (minimal) (s UNION t) <= MIN ((minimal) s) ((minimal) t)`,
  REWRITE_TAC[MIN] THEN
  MESON_TAC[minimal_union_le;UNION_COMM]);;

let nonempty_union = prove(
  `!s:A->bool t:A->bool.
  ~(s = EMPTY) ==> ~(s UNION t = EMPTY)`,
  MESON_TAC[CHOICE_DEF;MINIMAL;IN;IN_UNION;MEMBER_NOT_EMPTY]);;

let minimal_union_lemma = prove(
  `!s:num->bool t:num->bool.
   (minimal) (s UNION t) IN s ==>
   (minimal) s <= (minimal) (s UNION t)`,
  MESON_TAC[MINIMAL_UBOUND;IN]);;

let minimal_union_lemma2 = prove(
  `!s:num->bool t:num->bool.
   (minimal) (s UNION t) IN t ==>
   (minimal) t <= (minimal) (s UNION t)`,
  MESON_TAC[MINIMAL_UBOUND;IN]);;

let minimal_union_lemma3 = prove(
  `!s:num->bool t:num->bool.
   (minimal) (s UNION t) IN s ==>
   MIN ((minimal) s) ((minimal) t) <= (minimal) (s UNION t)`,
  MESON_TAC[minimal_union_lemma;IN;min_le_first;LE_TRANS]);;

let minimal_union_lemma4 = prove(
  `!s:num->bool t:num->bool.
   (minimal) (s UNION t) IN t ==>
   MIN ((minimal) s) ((minimal) t) <= (minimal) (s UNION t)`,
  MESON_TAC[minimal_union_lemma2;IN;min_le_second;LE_TRANS]);;

let minimal_union_lemma5 = prove(
  `!s:num->bool t:num->bool.
   ~(s = EMPTY) ==> ~(t = EMPTY) ==>
   MIN ((minimal) s) ((minimal) t) <= (minimal) (s UNION t)`,
  MESON_TAC[nonempty_union;CHOICE_DEF;MINIMAL;IN;IN_UNION;
            minimal_union_lemma3;minimal_union_lemma4]);;

let minimal_union = prove(
  `!s:num->bool t:num->bool.
   ~(s = EMPTY) ==> ~(t = EMPTY) ==>
   (minimal) (s UNION t) = MIN ((minimal) s) ((minimal) t)`,
  MESON_TAC[minimal_union_lemma5;minimal_union_le_min;LE_ANTISYM]);;

(* ----- pigeonhole principle for range *)

let range_pigeonhole_lemma1 = prove(
  `!f:num->A n.
    (!j k. j IN range n /\ k IN range n /\ f j = f k ==> j = k)
     ==> CARD(IMAGE f (range n)) = CARD(range n)`,
  MESON_TAC[CARD_IMAGE_INJ;range_finite]);;

let range_pigeonhole_lemma2 = prove(
  `!f:num->A n.
   (!j k. j IN range n /\ k IN range n /\ f j = f k ==> j = k)
   ==> CARD(IMAGE f (range n)) = n`,
  MESON_TAC[range_pigeonhole_lemma1;range_card]);;

let range_pigeonhole_lemma3 = prove(
  `!f:num->A n.
   (!j k. j IN range n /\ k IN range n /\ f j = f k ==> j = k)
   ==> CARD { y | ?k. k IN range n /\ y = f k } = n`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ISPECL[`f:num->A`;`n:num`]
             range_pigeonhole_lemma2) THEN
  ASSUME_TAC(ISPECL[`range n`;`f:num->A`]IMAGE) THEN
  ASM_MESON_TAC[]);;

let range_pigeonhole_lemma4 = prove(
  `!f:num->A n.
   (!j k. j < n /\ k < n /\ f j = f k ==> j = k)
   ==> CARD { y | ?k. k < n /\ y = f k } = n`,
  REWRITE_TAC[range_in_flip] THEN
  MESON_TAC[range_pigeonhole_lemma3]);;

let range_pigeonhole = prove(
  `!f:num->A n.
   CARD { y | ?k. k < n /\ y = f k } < n ==>
   (?j k. j < n /\ k < n /\ f j = f k /\ ~(j = k))`,
  MESON_TAC[range_pigeonhole_lemma4;LT_REFL]);;

(* ----- partcycle *)

let partcycle_subsetcycle = prove(
  `!p:A->A x m. partcycle m p x SUBSET cycle p x`,
  REWRITE_TAC[partcycle;cycle;SUBSET;IN_ELIM_THM] THEN
  MESON_TAC[pow_int_num]);;

let partcycle_monotonic = prove(
  `!p:A->A x m n. m <= n ==> partcycle m p x SUBSET partcycle n p x`,
  REWRITE_TAC[partcycle;SUBSET;IN_ELIM_THM] THEN
  MESON_TAC[LTE_TRANS]);;

let partcycle_lemma1 = prove(
 `!p:A->A x n j k. bijection p ==>
   (p pow_num j) x = (p pow_num k) x /\ j < k /\ k < n
   ==> ?m. 0 < m /\ m < n /\ x = (p pow_num m) x`,
  REPEAT STRIP_TAC THEN
  EXISTS_TAC `k-j` THEN
  ASSUME_TAC(ARITH_RULE `j < k ==> 0 < k - j`) THEN
  ASSUME_TAC(ARITH_RULE `k < n ==> k - j < n`) THEN
  ASM_MESON_TAC[pow_int_cancel_num2;LT_LE]);;

let partcycle_lemma2 = prove(
  `!p:A->A x n j k. bijection p ==>
   (p pow_num j) x = (p pow_num k) x /\ j < n /\ k < n /\ ~(j = k)
   ==> ?m. 0 < m /\ m < n /\ x = (p pow_num m) x`,
  REPEAT STRIP_TAC THEN
  ASM_CASES_TAC `j < k` THENL
  [
    ASM_MESON_TAC[partcycle_lemma1]
  ;
    ASSUME_TAC(SPECL[`j:num`;`k:num`]LT_CASES) THEN
    ASM_MESON_TAC[partcycle_lemma1]
  ]);;

let partcycle_lemma3 = prove(
  `!p:A->A x n.
   CARD { y | ?k. k < n /\ y = (p pow_num k) x } < n ==>
   (?j k. j < n /\ k < n /\
          (p pow_num j) x = (p pow_num k) x /\ ~(j = k))`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ISPECL[`\m. ((p:A->A) pow_num m) (x:A)`;`n:num`]
                   range_pigeonhole) THEN
  ASM_MESON_TAC[BETA_THM]);;

let partcycle_lemma4 = prove(
  `!p:A->A x n. bijection p ==>
   CARD(partcycle n p x) < n ==>
   ?m. 0 < m /\ m < n /\ x = (p pow_num m) x`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ISPECL[`p:A->A`;`x:A`;`n:num`]
             partcycle_lemma3) THEN
  ASSUME_TAC(ISPECL[`p:A->A`;`x:A`;`n:num`]
             partcycle_lemma2) THEN
  ASM_MESON_TAC[partcycle]);;

let partcycle_lemma5 = prove(
  `!p:A->A x m k.
   0 < m /\ x = (p pow_num m) x ==> x = (p pow_num (k*m)) x`,
  GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
  INDUCT_TAC THENL
  [
    MESON_TAC[pow_num_0_eval;ARITH_RULE `0*m = 0`]
  ;
    ASM_MESON_TAC[pow_num_plus_eval;
                  ARITH_RULE `(SUC k * m) = m + (k * m)`]
  ]);;

let partcycle_lemma6 = prove(
  `!p:A->A x m k.
   0 < m /\ x = (p pow_num m) x ==> x = (p pow_int (&k * &m)) x`,
  MESON_TAC[partcycle_lemma5;INT_OF_NUM_MUL;pow_int_num]);;

let partcycle_lemma7 = prove(
  `!p:A->A x m k. bijection p ==>
   0 < m /\ x = (p pow_num m) x ==> x = (p pow_int (--(&k) * &m)) x`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ISPEC `p:A->A` pow_int_0) THEN
  ASSUME_TAC(INT_ARITH `--(&k) * ((&m):int) + &k * &m = &0`) THEN
  ASSUME_TAC(ISPECL[`p:A->A`;`--(&k) * ((&m):int)`;
                    `&k * ((&m):int)`;`x:A`]pow_int_plus_eval) THEN
  ASSUME_TAC(ISPECL[`p:A->A`;`x:A`;`m:num`;`k:num`]
                    partcycle_lemma6) THEN
  ASM_MESON_TAC[I_THM]);;

let partcycle_lemma8 = prove(
  `!p:A->A x m k. bijection p ==>
   0 < m /\ x = (p pow_num m) x ==> x = (p pow_int (k * &m)) x`,
  REPEAT STRIP_TAC THEN
  ASM_CASES_TAC `&0 <= (k:int)` THENL
  [
    ASM_MESON_TAC[INT_OF_NUM_OF_INT;partcycle_lemma6]
  ;
    ASSUME_TAC(INT_ARITH `~(&0 <= (k:int)) ==> &0 <= --k`) THEN
    ASSUME_TAC(INT_ARITH `(k:int) = -- (--k)`) THEN
    ASSUME_TAC(SPEC `--k:int` INT_OF_NUM_OF_INT) THEN
    ASM_MESON_TAC[partcycle_lemma7]
  ]);;

let partcycle_lemma9 = prove(
  `!p:A->A x m j. bijection p ==>
   0 < m /\ x = (p pow_num m) x ==>
   (p pow_int j) x = (p pow_int (j rem &m)) x`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPECL[`j:int`;`&(m:num):int`]INT_DIVISION) THEN
  ASSUME_TAC(ARITH_RULE `0 < m ==> ~(m = 0)`) THEN
  ASSUME_TAC(SPECL[`m:num`;`0`]INT_OF_NUM_EQ) THEN
  ASSUME_TAC(ARITH_RULE
             `j div &m * &m + j rem &m =
              j rem &m + j div &m * &m`) THEN
  ASSUME_TAC(ISPECL[`p:A->A`;`x:A`;`m:num`;`j div &m`]
             partcycle_lemma8) THEN
  ASSUME_TAC(ISPECL[`p:A->A`;`j rem &m`;`j div &m * &m`;`x:A`]
             pow_int_plus_eval) THEN
  ASM_MESON_TAC[]);;

let partcycle_lemma10 = prove(
  `!p:A->A x m j. bijection p ==>
   0 < m /\ x = (p pow_num m) x ==>
   (p pow_int j) x IN partcycle m p x`,
  REPEAT STRIP_TAC THEN
  REWRITE_TAC[partcycle;IN_ELIM_THM] THEN
  EXISTS_TAC `num_of_int(j rem &m)` THEN
  ASSUME_TAC(ARITH_RULE `0 < m ==> ~(m = 0)`) THEN
  ASSUME_TAC(SPECL[`m:num`;`0`]INT_OF_NUM_EQ) THEN
  ASSUME_TAC(SPECL[`m:num`]INT_ABS_NUM) THEN
  ASSUME_TAC(SPECL[`j rem &m`]INT_OF_NUM_OF_INT) THEN
  ASSUME_TAC(SPECL[`j:int`;`&(m:num):int`]INT_DIVISION) THEN
  ASSUME_TAC(SPECL[`p:A->A`;`x:A`;`m:num`;`j:int`]
                   partcycle_lemma9) THEN
  ASSUME_TAC(SPECL[`p:A->A`;`num_of_int(j rem &m)`]pow_int_num) THEN
  ASSUME_TAC(SPECL[`num_of_int(j rem &m)`;`m:num`]INT_OF_NUM_LT) THEN
  ASM_MESON_TAC[]);;

let partcycle_lemma11 = prove(
  `!p:A->A x m. bijection p ==>
   0 < m /\ x = (p pow_num m) x ==>
   cycle p x SUBSET partcycle m p x`,
  MESON_TAC[cycle_aspow;partcycle_lemma10;SUBSET]);;

let partcycle_lemma12 = prove(
  `!p:A->A x m n. bijection p ==>
   0 < m /\ m <= n /\ x = (p pow_num m) x ==>
   cycle p x = partcycle n p x`,
  MESON_TAC[partcycle_subsetcycle;partcycle_lemma11;
            SUBSET_ANTISYM;SUBSET_TRANS;partcycle_monotonic]);;

let partcycle_lemma13 = prove(
  `!p:A->A x n. bijection p ==>
   CARD(partcycle n p x) < n ==> cycle p x = partcycle (n-1) p x`,
  MESON_TAC[partcycle_lemma4;
            partcycle_lemma12;
            ARITH_RULE `m < n ==> m <= n-1`]);;

let partcycle_ifcyclelt = prove(
  `!p:A->A x n. bijection p ==> FINITE(cycle p x) ==>
   CARD(cycle p x) < n ==> cycle p x = partcycle (n-1) p x`,
  MESON_TAC[partcycle_subsetcycle;CARD_SUBSET;LET_TRANS;
            partcycle_lemma13]);;

let partcycle_ifcyclele = prove(
  `!p:A->A x n. bijection p ==> FINITE(cycle p x) ==>
   CARD(cycle p x) <= n ==> cycle p x = partcycle n p x`,
  MESON_TAC[partcycle_ifcyclelt;LT_SUC_LE;
            ARITH_RULE `(n+1)-1 = n`;suc_isadd1]);;
           
(* ----- part2powcycle *)

let part2powcycle_hasstart = prove(
  `!i p:A->A x. x IN part2powcycle i p x`,
  REWRITE_TAC[part2powcycle;partcycle;IN_ELIM_THM] THEN
  REPEAT GEN_TAC THEN
  EXISTS_TAC `0` THEN
  REWRITE_TAC[pow_num_0_eval] THEN
  MESON_TAC[EXP_EQ_0;ARITH_RULE `~(2 = 0)`;
            ARITH_RULE `~(n = 0) ==> 0 < n`]);;

let part2powcycle_nonempty = prove(
  `!i p:A->A x. ~(part2powcycle i p x = EMPTY)`,
  MESON_TAC[part2powcycle_hasstart;MEMBER_NOT_EMPTY]);;

let part2powcycle_0_lemma = prove(
  `!p:num->num x. { x } = { y | ?k. k = 0 /\ y = (p pow_num k)(x) }`,
  REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING] THEN
  MESON_TAC[pow_num_0_eval]);;

let part2powcycle_0_lemma2 = prove(
  `!x m. m < x ==> ~{x} m`,
  MESON_TAC[LT_REFL;IN_SING;IN]);;

let part2powcycle_0_lemma3 = prove(
  `!x. x = (minimal) {x}`,
  MESON_TAC[part2powcycle_0_lemma2;MINIMAL_UNIQUE;IN_SING;IN]);;

let part2powcycle_0 = prove(
  `!p x. x = (minimal) (part2powcycle 0 p x)`,
  SIMP_TAC[part2powcycle;partcycle] THEN
  REWRITE_TAC[ARITH_RULE `2 EXP 0 = 1`] THEN
  REWRITE_TAC[ARITH_RULE `k < 1 <=> k = 0`] THEN
  MESON_TAC[part2powcycle_0_lemma;part2powcycle_0_lemma3]);;

let part2powcycle_plus1_lemma1 = prove(
  `!i. 2 EXP i <= 2 EXP (i+1)`,
  MESON_TAC[LE_EXP;ARITH_RULE `i <= i+1`;ARITH_RULE `~(2 = 0)`]);;

let part2powcycle_plus1_lemma2 = prove(
  `!i k. k < 2 EXP i ==> k < 2 EXP (i+1)`,
  MESON_TAC[part2powcycle_plus1_lemma1;LTE_TRANS]);;

let part2powcycle_plus1_lemma3 = prove(
  `!i p:A->A x. part2powcycle i p x SUBSET
                part2powcycle (i+1) p x`,
  REWRITE_TAC[part2powcycle;partcycle;SUBSET;IN_ELIM_THM] THEN
  MESON_TAC[part2powcycle_plus1_lemma2]);;

let part2powcycle_plus1_lemma4 = prove(
  `!i. 2 EXP i + 2 EXP i = 2 EXP (i+1)`,
  MESON_TAC[EXP;suc_isadd1;ARITH_RULE `2*n = n+n`]);;

let part2powcycle_plus1_lemma5 = prove(
  `!i k. k < 2 EXP i ==> k + 2 EXP i < 2 EXP (i+1)`,
  MESON_TAC[part2powcycle_plus1_lemma4;
            ARITH_RULE `m < n ==> m + p < n + p`]);;

let part2powcycle_plus1_lemma6 = prove(
  `!i p:A->A x.
   part2powcycle i p ((p pow_num (2 EXP i)) x)
   SUBSET part2powcycle (i+1) p x`,
  REWRITE_TAC[part2powcycle;partcycle;SUBSET;IN_ELIM_THM] THEN
  MESON_TAC[part2powcycle_plus1_lemma5;pow_num_plus_eval]);;

let part2powcycle_plus1_lemma7 = prove(
  `!k n. k < n+n ==> k < n \/ (k-n < n /\ k = (k-n)+n)`,
  REPEAT STRIP_TAC THEN
  ASM_CASES_TAC `k<n` THEN
  ASM_MESON_TAC[NOT_LT;SUB_ADD;LT_ADD_RCANCEL]);;

let part2powcycle_plus1_lemma8 = prove(
  `!i k. k < 2 EXP(i+1) ==>
         k < 2 EXP i \/
         (k-2 EXP i < 2 EXP i /\ k = (k-2 EXP i)+2 EXP i)`,
  MESON_TAC[part2powcycle_plus1_lemma7;part2powcycle_plus1_lemma4]);;

let part2powcycle_plus1_lemma9 = prove(
  `!i p:A->A x k. k < 2 EXP (i+1) ==> ~(k < 2 EXP i) ==>
   (p pow_num k) x IN
   part2powcycle i p ((p pow_num (2 EXP i)) x)`,
  REWRITE_TAC[part2powcycle;partcycle;IN;IN_ELIM_THM] THEN
  REPEAT STRIP_TAC THEN
  EXISTS_TAC `k - 2 EXP i` THEN
  ASM_MESON_TAC[part2powcycle_plus1_lemma8;pow_num_plus_eval]);;

let part2powcycle_plus1_lemma10 = prove(
  `!i p:A->A x k. k < 2 EXP i ==>
   (p pow_num k) x IN part2powcycle i p x`,
  REWRITE_TAC[part2powcycle;partcycle;IN;IN_ELIM_THM] THEN
  MESON_TAC[]);;

let part2powcycle_plus1_lemma11 = prove(
  `!i p:A->A x.
   {y | ?k. k < 2 EXP (i+1) /\ y = (p pow_num k) x}
   SUBSET part2powcycle i p x UNION
          part2powcycle i p ((p pow_num (2 EXP i)) x)`,
  REWRITE_TAC[SUBSET;UNION;IN_ELIM_THM] THEN
  MESON_TAC[part2powcycle_plus1_lemma9;part2powcycle_plus1_lemma10]);;

let part2powcycle_plus1_lemma12 = prove(
  `!i p:A->A x.
   part2powcycle (i+1) p x
   = {y | ?k. k < 2 EXP (i+1) /\ y = (p pow_num k) x}`,
  SIMP_TAC[part2powcycle;partcycle]);;

let part2powcycle_plus1_lemma13 = prove(
  `!i p:A->A x.
   part2powcycle (i+1) p x
   SUBSET part2powcycle i p x UNION
          part2powcycle i p ((p pow_num (2 EXP i)) x)`,
  REWRITE_TAC[part2powcycle_plus1_lemma12] THEN
  MESON_TAC[part2powcycle_plus1_lemma11]);;

let part2powcycle_plus1_lemma14 = prove(
  `!i p:A->A x.
   part2powcycle i p x UNION
   part2powcycle i p ((p pow_num (2 EXP i)) x)
   SUBSET part2powcycle (i+1) p x`,
  MESON_TAC[UNION_SUBSET;part2powcycle_plus1_lemma3;
            part2powcycle_plus1_lemma6]);;

let part2powcycle_plus1 = prove(
  `!i p:A->A x.
   part2powcycle (i+1) p x =
   part2powcycle i p x UNION
   part2powcycle i p ((p pow_num (2 EXP i)) x)`,
  MESON_TAC[SUBSET_ANTISYM;part2powcycle_plus1_lemma13;
            part2powcycle_plus1_lemma14]);;

let part2powcycle_ifcyclele = prove(
  `!p:A->A x i. bijection p ==> FINITE(cycle p x) ==>
   CARD(cycle p x) <= 2 EXP i ==> cycle p x = part2powcycle i p x`,
  MESON_TAC[partcycle_ifcyclele;part2powcycle]);;

(* ----- fastcyclemin *)

let fastcyclemin_part2powcycle_0 = prove(
  `!p x. fastcyclemin 0 p x = (minimal) (part2powcycle 0 p x)`,
  MESON_TAC[fastcyclemin;part2powcycle_0]);;

let fastcyclemin_lemma1 = prove(
  `!i p x.
   fastcyclemin (i+1) p x =
   if i+1 = 0 then x else
   MIN (fastcyclemin ((i+1)-1) p x)
       (fastcyclemin ((i+1)-1) p ((p pow_num (2 EXP ((i+1)-1))) x))`,
  MESON_TAC[fastcyclemin]);;

let fastcyclemin_lemma2 = prove(
  `!i p x. fastcyclemin (i+1) p x =
           MIN (fastcyclemin i p x)
               (fastcyclemin i p ((p pow_num (2 EXP i)) x))`,
  REPEAT GEN_TAC THEN
  ASSUME_TAC(ARITH_RULE `~(i+1 = 0)`) THEN
  ASSUME_TAC(ARITH_RULE `(i+1)-1 = i`) THEN
  ASM_SIMP_TAC[fastcyclemin_lemma1]);;

let fastcyclemin_part2powcycle = prove(
  `!i p x. fastcyclemin i p x = (minimal) (part2powcycle i p x)`,
  INDUCT_TAC THENL
  [
    MESON_TAC[fastcyclemin_part2powcycle_0]
  ;
    REWRITE_TAC[suc_isadd1] THEN
    REWRITE_TAC[part2powcycle_plus1] THEN
    ASSUME_TAC(ISPECL[`i:num`;`p:num->num`;`x:num`]part2powcycle_nonempty)
    THEN
    ASSUME_TAC(ISPECL[`i:num`;`p:num->num`;
               `(p pow_num (2 EXP i)) x:num`]part2powcycle_nonempty) THEN
    ASM_SIMP_TAC[minimal_union] THEN
    ASM_MESON_TAC[fastcyclemin_lemma2]
  ]);;

let fastcyclemin_works = prove(
  `!p:num->num x i. bijection p ==> FINITE(cycle p x) ==>
   CARD(cycle p x) <= 2 EXP i ==> cyclemin p x = fastcyclemin i p x`,
  REWRITE_TAC[cyclemin;fastcyclemin_part2powcycle] THEN
  MESON_TAC[part2powcycle_ifcyclele]);;

(* ----- Xif *)

let xif_parity = prove(
  `!s n. ODD(Xif s n) = ~(s(n DIV 2) = ODD n)`,
  REWRITE_TAC[xif] THEN
  MESON_TAC[xor1_parity]);;

let xif_double_parity = prove(
  `!s j. ODD(Xif s (2*j)) = s j`,
  REWRITE_TAC[xif_parity;double_div2] THEN
  MESON_TAC[NOT_EVEN;EVEN_DOUBLE]);;

let xif_double_plus1_parity = prove(
  `!s j. ODD(Xif s (2*j+1)) = ~(s j)`,
  REWRITE_TAC[xif_parity;double_plus1_div2] THEN
  MESON_TAC[ODD_DOUBLE;suc_isadd1]);;

let xif_involution = prove(
  `!s. involution(Xif s)`,
  REWRITE_TAC[involution;xif] THEN
  REPEAT GEN_TAC THEN
  ASM_CASES_TAC `(s:num->bool)(x DIV 2)` THEN
  ASM_SIMP_TAC[xor1_div2;xor1xor1]);;

let xif_fixesge = prove(
  `!s b. s subsetrange b ==> Xif s fixesge(2*b)`,
  REWRITE_TAC[subsetrange;fixesge;xif] THEN
  MESON_TAC[div2_lt_doubling_ge]);;

(* ----- vanishesifonbothsidesof *)

let vanishesifonbothsidesof_eval = prove(
  `!p:A->A q:A->A. p vanishesifonbothsidesof q <=> !x. p(q(p x)) = q x`,
  REWRITE_TAC[vanishesifonbothsidesof] THEN
  MESON_TAC[o_DEF;EQ_EXT]);;

let vanishesifonbothsidesof_pow_num_eval = prove(
  `!p:A->A q:A->A. p vanishesifonbothsidesof q ==>
    !n. !x. (p pow_num n)(q((p pow_num n)x)) = q x`,
  REWRITE_TAC[vanishesifonbothsidesof_eval] THEN
  REPEAT GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL
  [
    REWRITE_TAC[pow_num_0;I_DEF]
  ;
    REWRITE_TAC[suc_isadd1] THEN
    ASSUME_TAC(SPECL[`n:num`;`p:A->A`]pow_num_plus1_eval) THEN
    ASSUME_TAC(SPECL[`n:num`;`p:A->A`]pow_num_plus1_right_eval) THEN
    ASM_MESON_TAC[]
  ]);;

let vanishesifonbothsidesof_pow_num_lemma = prove(
  `!p:A->A q:A->A. p vanishesifonbothsidesof q ==>
    !n. (p pow_num n) o q o (p pow_num n) = q`,
  REPEAT GEN_TAC THEN DISCH_TAC THEN
  ASM_MESON_TAC[vanishesifonbothsidesof_pow_num_eval;o_DEF;EQ_EXT]);;

let vanishesifonbothsidesof_pow_num = prove(
  `!p:A->A q:A->A. p vanishesifonbothsidesof q ==>
    !n. (p pow_num n) vanishesifonbothsidesof q`,
  MESON_TAC[vanishesifonbothsidesof_pow_num_lemma;
            vanishesifonbothsidesof]);;

let vanishesifonbothsidesof_inverse = prove(
  `!p:A->A. bijection p ==> !q:A->A. p vanishesifonbothsidesof q ==>
    inverse p vanishesifonbothsidesof q`,
  REWRITE_TAC[vanishesifonbothsidesof_eval] THEN
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ISPEC `p:A->A` bijection_inverse_composition1) THEN
  ASSUME_TAC(ISPEC `p:A->A` bijection_inverse_composition2) THEN
  ASM_MESON_TAC[]);;

let vanishesifonbothsidesof_pow_int = prove(
  `!p:A->A. bijection p ==> !q:A->A. p vanishesifonbothsidesof q
    ==> !k:int. p pow_int k vanishesifonbothsidesof q`,
  REWRITE_TAC[pow_int] THEN
  REPEAT STRIP_TAC THEN 
  ASSUME_TAC(INT_ARITH `k < &0 ==> ~(&0 <= k)`) THEN
  ASM_MESON_TAC[vanishesifonbothsidesof_pow_num;
                vanishesifonbothsidesof_inverse]);;

(* ----- fixesge *)

let fixesge_double_odd = prove(
  `!p b x. p fixesge(2*b) ==> x >= b ==> ~ODD(p(2*x))`,
  MESON_TAC[fixesge;LE_MULT_LCANCEL;GE;EVEN_DOUBLE;NOT_ODD]);;

let fixesge_inverts_1 = prove(
  `!p n. bijection p ==> p fixesge n ==> inverse p fixesge n`,
  REWRITE_TAC[bijection;surjection;injection;inverse;fixesge] THEN
  MESON_TAC[]);;

let fixesge_inverts_2 = prove(
  `!p n. bijection p /\ (!x. x >= n ==> p x = x) ==>
         !x. x >= n ==> inverse p x = x`,
  MESON_TAC[fixesge_inverts_1;fixesge]);;

let fixesge_lemma1 = prove(
  `!p n m. bijection p ==> p fixesge n ==> p m >= n ==> m >= n`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPECL[`p:num->num`;`n:num`]fixesge_inverts_1) THEN
  ASSUME_TAC(ISPECL[`p:num->num`;`m:num`]
             bijection_inverse_composition2) THEN
  ASM_MESON_TAC[GE;NOT_LT;fixesge]);;

let fixesge_lt = prove(
  `!p n m. bijection p ==> p fixesge n ==> m < n ==> p m < n`,
  MESON_TAC[fixesge_lemma1;GE;NOT_LT]);;

let fixesge_I = prove(
  `!n. I fixesge n`,
  REWRITE_TAC[fixesge;I_DEF]);;

let fixesge_composes = prove(
  `!f g n. f fixesge n /\ g fixesge n ==> f o g fixesge n`,
  REWRITE_TAC[fixesge] THEN
  MESON_TAC[o_DEF]);;

let fixesge_pow_lemma1 = prove(
  `!f n m. f fixesge n ==> f pow_num m fixesge n
           ==> f o (f pow_num m) fixesge n`,
  REPEAT STRIP_TAC THEN
  ASM_MESON_TAC[fixesge_composes]);;

let fixesge_pow_lemma2 = prove(
  `!f n m. f fixesge n ==> f pow_num m fixesge n
           ==> f o (f pow_num ((m+1)-1)) fixesge n`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ARITH_RULE `(m+1)-1 = m`) THEN
  ASM_MESON_TAC[fixesge_pow_lemma1]);;

let fixesge_pow_lemma3 = prove(
  `!f n m. f fixesge n ==> f pow_num m fixesge n
           ==> f pow_num (m+1) fixesge n`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ARITH_RULE `~(m+1 = 0)`) THEN
  ASM_MESON_TAC[pow_num;fixesge_pow_lemma2]);;

let fixesge_pow_num = prove(
  `!f n m. f fixesge n ==> f pow_num m fixesge n`,
  GEN_TAC THEN GEN_TAC THEN
  INDUCT_TAC THENL
  [
    ASM_MESON_TAC[pow_num;fixesge_I]
  ;
    REWRITE_TAC[suc_isadd1] THEN
    ASM_MESON_TAC[fixesge_pow_lemma3]
  ]);;

let fixesge_pow_int = prove(
  `!p n k. bijection p ==> p fixesge n ==> p pow_int k fixesge n`,
  MESON_TAC[fixesge_pow_num;pow_int;fixesge_inverts_1]);;

let fixesge_cyclemin = prove(
  `!p n. bijection p ==> p fixesge n ==> cyclemin p fixesge n`,
  MESON_TAC[fixesge_pow_int;cyclemin_aspow;fixesge]);;

(* ----- XbackXforth *)

let XbackXforth_forward = prove(
  `!p x. bijection p ==> (XbackXforth p)(xor1(p x)) = p(xor1 x)`,
  REWRITE_TAC[XbackXforth] THEN
  REWRITE_TAC[o_DEF] THEN
  MESON_TAC[xor1xor1;bijection_inverse_composition2]);;

let XbackXforth_fixesge = prove(
  `!p b. bijection p ==> p fixesge(2*b) ==> XbackXforth p fixesge(2*b)`,
  REWRITE_TAC[XbackXforth;fixesge;o_THM] THEN
  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `!x. x >= 2*b ==> xor1 x >= 2*b` ASSUME_TAC
  THENL [MESON_TAC[xor1_geeven];ALL_TAC] THEN
  SUBGOAL_THEN `!x. x >= 2*b ==> p(xor1 x) = xor1 x` ASSUME_TAC
  THENL [ASM_MESON_TAC[];ALL_TAC] THEN
  SUBGOAL_THEN `!x. x >= 2*b ==> xor1(p(xor1 x)) = x` ASSUME_TAC
  THENL [ASM_MESON_TAC[xor1xor1];ALL_TAC] THEN
  SUBGOAL_THEN `!x. x >= 2*b ==>
                inverse p(xor1(p(xor1 x))) = x` ASSUME_TAC
  THENL [ASM_MESON_TAC[fixesge_inverts_2];ALL_TAC]
  THEN ASM_MESON_TAC[]);;

let XbackXforth_bijection = prove(
  `!p. bijection p ==> bijection(XbackXforth p)`,
  REWRITE_TAC[XbackXforth] THEN
  MESON_TAC[xor1_involution;bijection_ifinvolution;
    bijection_inverseisbijection;bijection_composes]);;

let XbackXforth_cyclemin_twist = prove(
  `!p x. bijection p ==>
         cyclemin(XbackXforth p) (xor1(p(x)))
         = cyclemin(XbackXforth p) (p(xor1(x)))`,
  MESON_TAC[XbackXforth_bijection;XbackXforth_forward;
            cyclemin_shift]);;

let XbackXforth_lemma1 = prove(
  `!i:A->A p:A->A q:A->A.
    (!x. (i o i)x = x) /\ (!x. (q o p)x = x) /\ (!x. (p o q)x = x) ==>
    !x. ((p o i o q o i) o i o (p o i o q o i))x = i x`,
  REWRITE_TAC[o_DEF] THEN
  MESON_TAC[]);;

let XbackXforth_lemma2 = prove(
  `!i:A->A p:A->A q:A->A. i o i = I /\ q o p = I /\ p o q = I ==>
    (!x. (i o i)x = x) /\ (!x. (q o p)x = x) /\ (!x. (p o q)x = x)`,
  REWRITE_TAC[I_DEF;o_DEF] THEN
  MESON_TAC[]);;

let XbackXforth_lemma3 = prove(
  `!i:A->A p:A->A q:A->A. i o i = I /\ q o p = I /\ p o q = I ==>
    !x. ((p o i o q o i) o i o (p o i o q o i))x = i x`,
  REPEAT GEN_TAC THEN DISCH_TAC THEN
  ASSUME_TAC(SPECL[`i:A->A`;`p:A->A`;`q:A->A`]
                   XbackXforth_lemma1) THEN
  ASSUME_TAC(SPECL[`i:A->A`;`p:A->A`;`q:A->A`]
                   XbackXforth_lemma2) THEN
  ASM_MESON_TAC[]);;

let XbackXforth_lemma4 = prove(
  `!i:A->A p:A->A q:A->A. i o i = I /\ q o p = I /\ p o q = I ==>
    (p o i o q o i) o i o (p o i o q o i) = i`,
  MESON_TAC[XbackXforth_lemma3;EQ_EXT]);;

let XbackXforth_lemma5 = prove(
  `!i:A->A p:A->A q:A->A. i o i = I /\ q o p = I /\ p o q = I ==>
    p o i o q o i vanishesifonbothsidesof i`,
  MESON_TAC[XbackXforth_lemma4;vanishesifonbothsidesof]);;

let XbackXforth_lemma6 = prove(
  `!i:A->A. i o i = I ==> !p:A->A. bijection p ==>
    p o i o inverse p o i vanishesifonbothsidesof i`,
  MESON_TAC[XbackXforth_lemma5;
    bijection_inverse_composition5;
    bijection_inverse_composition6]);;

let XbackXforth_vanishesifonbothsidesof_xor1 = prove(
  `!p. bijection p ==> XbackXforth p vanishesifonbothsidesof xor1`,
  REWRITE_TAC[XbackXforth] THEN
  MESON_TAC[xor1_involution_o;XbackXforth_lemma6]);;

let XbackXforth_power_vanishesifonbothsidesof_xor1 = prove(
  `!p k:int. bijection p ==>
             (XbackXforth p pow_int k) vanishesifonbothsidesof xor1`,
  MESON_TAC[XbackXforth_bijection;
    XbackXforth_vanishesifonbothsidesof_xor1;
    vanishesifonbothsidesof_pow_int]);;

let XbackXforth_powpow_xor1 = prove(
  `!p k:int x. bijection p ==>
               (XbackXforth p pow_int k)
                 (xor1((XbackXforth p pow_int k) x)) = xor1 x`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPECL[`p:num->num`;`k:int`]
                   XbackXforth_power_vanishesifonbothsidesof_xor1)
  THEN ASM_MESON_TAC[vanishesifonbothsidesof;o_THM]);;

let XbackXforth_even_avoids_xor1 = prove(
  `!p k:int x. bijection p ==>
    ~((XbackXforth p pow_int (k+k)) x = xor1 x)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPECL[`p:num->num`;`k:int`;`x:num`]
                  XbackXforth_powpow_xor1) THEN
  ASSUME_TAC(SPEC `p:num->num` XbackXforth_bijection) THEN
  ASSUME_TAC(ISPECL[`XbackXforth p`;`k:int`;`k:int`]
                    pow_int_plus) THEN
  ASSUME_TAC(ISPECL[`XbackXforth p`;`k:int`;
                    `(XbackXforth p pow_int (k:int))(x:num)`;
                    `xor1((XbackXforth p pow_int (k:int))(x:num))`
                   ]pow_int_cancel) THEN
  ASSUME_TAC(SPEC `(XbackXforth p pow_int (k:int)) (x:num)`
             xor1_distinct) THEN
  ASM_MESON_TAC[o_THM]);;

let XbackXforth_1_avoids_xor1 = prove(
  `!p x. bijection p ==> ~(XbackXforth p x = xor1 x)`,
  REWRITE_TAC[XbackXforth;o_DEF] THEN
  MESON_TAC[xor1_distinct;bijection_inverse_composition2]);;

let XbackXforth_odd_avoids_xor1 = prove(
  `!p k:int x. bijection p ==>
    ~((XbackXforth p pow_int ((k + &1) + k)) x = xor1 x)`,
  REPEAT GEN_TAC THEN DISCH_TAC THEN
  ASSUME_TAC(SPEC `p:num->num` XbackXforth_bijection) THEN
  ASM_SIMP_TAC[ISPECL[`XbackXforth p`;
                      `(k:int)+ &1`;`k:int`]pow_int_plus] THEN
  ASM_SIMP_TAC[o_THM] THEN
  ASM_SIMP_TAC[ISPECL[`XbackXforth p`;
                      `k:int`;`&1:int`]pow_int_plus] THEN
  ASM_SIMP_TAC[o_THM] THEN
  ASM_SIMP_TAC[ISPECL[`XbackXforth p`]pow_int_1] THEN
  ASSUME_TAC(SPECL[`p:num->num`;`k:int`;`x:num`]
                   XbackXforth_powpow_xor1) THEN
  ASSUME_TAC(ISPECL[`XbackXforth p`;`k:int`]pow_int_bijection) THEN
  ASSUME_TAC(ISPECL[`XbackXforth p:num->num`;`k:int`;
                    `(XbackXforth p)((XbackXforth p pow_int k)(x:num))`;
                    `xor1((XbackXforth p pow_int k)(x:num))`
                   ]pow_int_cancel) THEN
  ASSUME_TAC(SPECL[`p:num->num`;`(XbackXforth p pow_int k) (x:num)`]
                  XbackXforth_1_avoids_xor1) THEN
  ASM_MESON_TAC[o_THM]);;

let XbackXforth_pow_avoids_xor1 = prove(
  `!p n:int x. bijection p ==>
    ~((XbackXforth p pow_int n) x = xor1 x)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPECL[`n:int`;`&2:int`]INT_DIVISION_SIMP) THEN
  DISJ_CASES_TAC(SPEC `n:int` INT_REM_2_CASES) THENL
  [
    ASSUME_TAC(INT_ARITH
               `(n:int) div &2 * &2 + &0 = n div &2 + n div &2`)
    THEN ASM_MESON_TAC[XbackXforth_even_avoids_xor1]
  ;
    ASSUME_TAC(INT_ARITH
               `(n:int) div &2 * &2 + &1 = (n div &2 + &1) + n div &2`)
    THEN ASM_MESON_TAC[XbackXforth_odd_avoids_xor1]
  ]);;

let XbackXforth_powpow_avoids_xor1 = prove(
  `!p n:int m:int x. bijection p ==>
    ~((XbackXforth p pow_int n) x =
      xor1 ((XbackXforth p pow_int m) x))`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPEC `p:num->num` XbackXforth_bijection) THEN
  ASSUME_TAC(ISPECL[`XbackXforth p`;`m:int`]pow_int_bijection) THEN
  ASSUME_TAC(ISPECL[`XbackXforth p`;`(n:int)-(m:int)`;`m:int`]
                   pow_int_plus) THEN
  ASSUME_TAC(INT_ARITH `((n:int)-(m:int))+m = n`) THEN
  ASSUME_TAC(SPECL[`p:num->num`;`(n:int)-(m:int)`;
                   `((XbackXforth p pow_int m) x)`
                  ]XbackXforth_pow_avoids_xor1) THEN
  ASM_MESON_TAC[o_THM]);;

let XbackXforth_powpow2_avoids_xor1 = prove(
  `!p n:int m:int x. bijection p ==>
    ~((XbackXforth p pow_int n) x =
       (XbackXforth p pow_int m) (xor1 x))`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPEC `p:num->num` XbackXforth_bijection) THEN
  ASSUME_TAC(ISPECL[`XbackXforth p`;`m:int`]pow_int_bijection) THEN
  ASSUME_TAC(ISPECL[`XbackXforth p`;`m:int`;
                    `(n:int)-(m:int)`]pow_int_plus) THEN
  ASSUME_TAC(INT_ARITH `m+((n:int)-(m:int)) = n`) THEN
  ASSUME_TAC(ISPECL[`XbackXforth p`;`m:int`;
                    `(XbackXforth p pow_int(n-m))x`;`xor1 x:num`
                   ]pow_int_cancel) THEN
  ASSUME_TAC(SPECL[`p:num->num`;`(n:int)-(m:int)`;`x:num`
                  ]XbackXforth_pow_avoids_xor1) THEN
  ASM_MESON_TAC[o_THM]);;

let XbackXforth_pow_xor1 = prove(
  `!p k:int x. bijection p ==>
    xor1((XbackXforth p pow_int k) x) =
    (XbackXforth p pow_int --k)(xor1 x)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(ISPECL[`p:num->num`]XbackXforth_bijection) THEN
  ASM_SIMP_TAC[ISPECL[`XbackXforth p`;`k:int`]pow_int_inverse] THEN
  ASSUME_TAC(ISPECL[`XbackXforth p`;`k:int`]pow_int_bijection) THEN
  ASSUME_TAC(SPECL[`p:num->num`;`k:int`;`x:num`]
                  XbackXforth_powpow_xor1) THEN
  ASSUME_TAC(ISPECL[`XbackXforth p pow_int k`;
                    `xor1 x:num`]bijection_inverse_composition1) THEN
  ASSUME_TAC(ISPECL[`XbackXforth p`;`k:int`;
                    `inverse(XbackXforth p pow_int k)(xor1 x)`;
                    `xor1((XbackXforth p pow_int k)x)`
                   ]pow_int_cancel) THEN
  ASM_MESON_TAC[]);;

let XbackXforth_pow_xor1_incycle = prove(
  `!p k:int x. bijection p ==>
    xor1((XbackXforth p pow_int k) x) IN
      cycle (XbackXforth p) (xor1 x)`,
  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC(ISPECL[`XbackXforth p`;`xor1 x`;
                      `xor1((XbackXforth p pow_int k) x)`;`--k:int`
                     ]cycle_ifpow) THEN
  ASM_MESON_TAC[XbackXforth_pow_xor1]);;

let XbackXforth_pow_xor1_gecyclemin = prove(
  `!p x k:int. bijection p ==>
    cyclemin (XbackXforth p) (xor1 x) <=
      xor1((XbackXforth p pow_int k) x)`,
  REPEAT STRIP_TAC THEN
  REWRITE_TAC[cyclemin] THEN
  MATCH_MP_TAC MINIMAL_UBOUND THEN
  ASM_MESON_TAC[XbackXforth_pow_xor1_incycle;IN]);;

let XbackXforth_cyclemin_xor1_gecyclemin = prove(
  `!p x. bijection p ==>
    cyclemin (XbackXforth p) (xor1 x) <=
      xor1(cyclemin (XbackXforth p) x)`,
  REPEAT STRIP_TAC THEN
  ASSUME_TAC(SPECL[`XbackXforth p:num->num`;
                   `x:num`]cyclemin_aspow) THEN
  ASSUME_TAC(SPECL[`p:num->num`;`x:num`]
                  XbackXforth_pow_xor1_gecyclemin) THEN
  ASM_MESON_TAC[]);;

let XbackXforth_cyclemin_xor1_gecyclemin_reverse = prove(
  `!p x. bijection p ==>
    cyclemin (XbackXforth p) x <=
      xor1(cyclemin (XbackXforth p) (xor1 x))`,
  MESON_TAC[xor1xor1;XbackXforth_cyclemin_xor1_gecyclemin]);;

let XbackXforth_cyclemin_xor1_ne = prove(
  `!p x k:int. bijection p ==>
   ~(cyclemin(XbackXforth p) (xor1 x) = cyclemin(XbackXforth p) x)`,
  MESON_TAC[XbackXforth_powpow2_avoids_xor1;cyclemin_aspow]);;

let XbackXforth_cyclemin_xor1 = prove(
  `!p x. bijection p ==>
    cyclemin (XbackXforth p) (xor1 x) =
      xor1(cyclemin (XbackXforth p) x)`,
  MESON_TAC[xor1_sandwich;XbackXforth_cyclemin_xor1_ne;
            XbackXforth_cyclemin_xor1_gecyclemin_reverse;
            XbackXforth_cyclemin_xor1_gecyclemin]);;

let XbackXforth_cyclemin_xor1_double = prove(
  `!p j. bijection p ==>
         cyclemin (XbackXforth p) (2*j+1) =
         xor1(cyclemin (XbackXforth p) (2*j))`,
  MESON_TAC[XbackXforth_cyclemin_xor1;xor1_double]);;

let XbackXforth_cyclemin_xor1_double_parity = prove(
  `!p j. bijection p ==>
         ODD(cyclemin (XbackXforth p) (2*j+1)) =
         ~ODD(cyclemin (XbackXforth p) (2*j))`,
  MESON_TAC[XbackXforth_cyclemin_xor1_double;xor1_parity]);;

let XbackXforth_cyclemin_twist2 = prove(
  `!p x. bijection p ==>
         xor1(cyclemin(XbackXforth p) (p x))
         = cyclemin(XbackXforth p) (p(xor1 x))`,
  MESON_TAC[XbackXforth_cyclemin_twist;XbackXforth_cyclemin_xor1]);;

let XbackXforth_cyclemin_twist2_parity = prove(
  `!p x. bijection p ==>
         ~ODD(cyclemin(XbackXforth p) (p x))
         = ODD(cyclemin(XbackXforth p) (p(xor1 x)))`,
  MESON_TAC[XbackXforth_cyclemin_twist2;xor1_parity]);;

let XbackXforth_cyclemin_twist2_parity_double = prove(
  `!p j. bijection p ==>
         ~ODD(cyclemin(XbackXforth p) (p(2*j)))
         = ODD(cyclemin(XbackXforth p) (p(2*j+1)))`,
  MESON_TAC[XbackXforth_cyclemin_twist2_parity;xor1_double]);;

(* ----- XbackXforth cycle lengths *)

let XbackXforth_cycle_lemma1 = prove(
  `!p x y k. bijection p ==>
             y = ((XbackXforth p) pow_int k) x ==>
             ~(y IN cycle (XbackXforth p) (xor1 x))`,
  MESON_TAC[cycle_aspow;XbackXforth_powpow2_avoids_xor1]);;

let XbackXforth_cycle_lemma2 = prove(
  `!p x y. bijection p ==>
           y IN cycle (XbackXforth p) x ==>
           ~(y IN cycle (XbackXforth p) (xor1 x))`,
  MESON_TAC[cycle_aspow;XbackXforth_cycle_lemma1]);;

let XbackXforth_cycle_lemma3 = prove(
  `!p x. bijection p ==>
         DISJOINT (cycle (XbackXforth p) x)
                  (cycle (XbackXforth p) (xor1 x))`,
  MESON_TAC[IN_DISJOINT;XbackXforth_cycle_lemma2]);;

let XbackXforth_cycle_lemma4 = prove(
  `!p x. bijection p ==>
         cycle (XbackXforth p) x INTER
         cycle (XbackXforth p) (xor1 x) = EMPTY`,
  MESON_TAC[DISJOINT;XbackXforth_cycle_lemma3]);;

let XbackXforth_cycle_lemma5 = prove(
  `!p n k x. bijection p ==> p fixesge n ==> x < n ==>
             (p pow_int k) x < n`,
  MESON_TAC[fixesge_pow_int;pow_int_bijection;fixesge_lt]);;

let XbackXforth_cycle_lemma6 = prove(
  `!p b x y. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
             y IN cycle (XbackXforth p) x ==> y < 2*b`,
  MESON_TAC[XbackXforth_bijection;XbackXforth_fixesge;
            XbackXforth_cycle_lemma5;cycle_aspow]);;

let XbackXforth_cycle_lemma7 = prove(
  `!p b x. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
           cycle (XbackXforth p) x SUBSET range(2*b)`,
  REWRITE_TAC[SUBSET;range;IN_ELIM_THM] THEN
  MESON_TAC[XbackXforth_cycle_lemma6]);;

let XbackXforth_cycle_lemma8 = prove(
  `!p b x. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
           FINITE(cycle (XbackXforth p) x)`,
  MESON_TAC[XbackXforth_cycle_lemma7;FINITE_SUBSET;range_finite]);;

let XbackXforth_cycle_lemma9 = prove(
  `!p b x. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
           cycle (XbackXforth p) (xor1 x) SUBSET range(2*b)`,
  MESON_TAC[xor1_lteven;XbackXforth_cycle_lemma7]);;

let XbackXforth_cycle_lemma10 = prove(
  `!p b x. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
           cycle (XbackXforth p) x UNION
           cycle (XbackXforth p) (xor1 x) SUBSET range(2*b)`,
  MESON_TAC[XbackXforth_cycle_lemma7;XbackXforth_cycle_lemma9;
            UNION_SUBSET]);;

let XbackXforth_cycle_lemma11 = prove(
  `!p b x. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
           CARD(cycle (XbackXforth p) x
                UNION cycle (XbackXforth p) (xor1 x))
           <= 2*b`,
  MESON_TAC[XbackXforth_cycle_lemma10;range_card;
            range_finite;CARD_SUBSET]);;

let XbackXforth_cycle_lemma12 = prove(
  `!p b x. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
           CARD(cycle (XbackXforth p) x
                UNION cycle (XbackXforth p) (xor1 x))
           = CARD(cycle (XbackXforth p) x)
           + CARD(cycle (XbackXforth p) (xor1 x))`,
  MESON_TAC[CARD_UNION;XbackXforth_cycle_lemma4;
            XbackXforth_cycle_lemma8;xor1_lteven]);;

let XbackXforth_cycle_lemma13 = prove(
  `!p b x. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
           CARD(cycle (XbackXforth p) x)
           + CARD(cycle (XbackXforth p) (xor1 x)) <= 2*b`,
  MESON_TAC[XbackXforth_cycle_lemma11;XbackXforth_cycle_lemma12]);;

let XbackXforth_cycle_lemma14 = prove(
  `!p x. bijection p ==>
         IMAGE xor1 (cycle (XbackXforth p) x) SUBSET
         cycle (XbackXforth p) (xor1 x)`,
  REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM] THEN
  MESON_TAC[cycle_aspow;XbackXforth_pow_xor1_incycle]);;

let XbackXforth_cycle_lemma15 = prove(
  `!p x. bijection p ==>
         cycle (XbackXforth p) (xor1 x) SUBSET
         IMAGE xor1 (cycle (XbackXforth p) x)`,
  REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM] THEN
  MESON_TAC[cycle_aspow;XbackXforth_pow_xor1_incycle;xor1xor1]);;

let XbackXforth_cycle_lemma16 = prove(
  `!p x. bijection p ==>
         cycle (XbackXforth p) (xor1 x) =
         IMAGE xor1 (cycle (XbackXforth p) x)`,
  MESON_TAC[XbackXforth_cycle_lemma14;
            XbackXforth_cycle_lemma15;SUBSET_ANTISYM]);;

let XbackXforth_cycle_lemma17 = prove(
  `!p x b. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
           CARD(IMAGE xor1 (cycle (XbackXforth p) x)) =
           CARD(cycle (XbackXforth p) x)`,
  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC CARD_IMAGE_INJ THEN
  ASM_MESON_TAC[xor1_involution;injection_ifinvolution;
                injection;XbackXforth_cycle_lemma8]);;

let XbackXforth_cycle_lemma18 = prove(
  `!p x b. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
           CARD(cycle (XbackXforth p) (xor1 x)) =
           CARD(cycle (XbackXforth p) x)`,
  MESON_TAC[XbackXforth_cycle_lemma16;XbackXforth_cycle_lemma17]);;

let XbackXforth_cycle_lemma19 = prove(
  `!p b x. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
           2*CARD(cycle (XbackXforth p) x) <= 2*b`,
  MESON_TAC[XbackXforth_cycle_lemma18;XbackXforth_cycle_lemma13;
            ARITH_RULE `2*n = n+n`]);;

let XbackXforth_cycle_size = prove(
  `!p b x. bijection p ==> p fixesge (2*b) ==> x < 2*b ==>
           CARD(cycle (XbackXforth p) x) <= b`,
  MESON_TAC[XbackXforth_cycle_lemma19;LE_MULT_LCANCEL;
            ARITH_RULE `~(2 = 0)`]);;

(* ----- firstcontrol *)

let firstcontrol_0 = prove(
  `!p. ~(firstcontrol p 0)`,
  MESON_TAC[ODD;firstcontrol;cyclemin_0;ARITH_RULE `2*0 = 0`]);;

let firstcontrol_subsetrange = prove(
  `!p b. bijection p ==> p fixesge(2*b) ==>
         firstcontrol p subsetrange b`,
  MESON_TAC[subsetrange;firstcontrol;XbackXforth_fixesge;
            XbackXforth_bijection;fixesge_cyclemin;
            fixesge_double_odd;GE;NOT_LT]);;

let firstcontrol_even = prove(
  `!p j. bijection p ==>
         ODD(Xif(firstcontrol p) (2*j)) =
         ODD(cyclemin(XbackXforth p)(2*j))`,
  MESON_TAC[firstcontrol;xif_double_parity]);;

let firstcontrol_odd_lemma1 = prove(
  `!p j. (firstcontrol p) ((2*j+1) DIV 2) =
         ODD(cyclemin(XbackXforth p)(2*j))`,
  MESON_TAC[firstcontrol;double_plus1_div2]);;

let firstcontrol_odd_lemma2 = prove(
  `!p j. bijection p ==>
         (firstcontrol p) ((2*j+1) DIV 2) =
         ~ODD(cyclemin(XbackXforth p)(2*j+1))`,
  REWRITE_TAC[firstcontrol_odd_lemma1] THEN
  MESON_TAC[XbackXforth_cyclemin_xor1_double_parity]);;

let firstcontrol_odd = prove(
  `!p j. bijection p ==>
         ODD(Xif(firstcontrol p) (2*j+1)) =
         ODD(cyclemin(XbackXforth p)(2*j+1))`,
  MESON_TAC[firstcontrol_odd_lemma2;xif_parity;
            ODD_DOUBLE;suc_isadd1]);;

let firstcontrol_parity = prove(
  `!p x. bijection p ==>
         ODD(Xif(firstcontrol p) x) =
         ODD(cyclemin(XbackXforth p) x)`,
  REPEAT STRIP_TAC THEN
  DISJ_CASES_TAC (SPEC `x:num` EVEN_OR_ODD) THENL
  [
    ASM_MESON_TAC[EVEN_EXISTS;firstcontrol_even]
  ;
    ASM_MESON_TAC[odd_isdoubleplus1;firstcontrol_odd]
  ]);;

(* ----- lastcontrol *)

let lastcontrol_lemma1 = prove(
  `!p b. bijection p ==> p fixesge(2*b) ==>
         Xif (firstcontrol p) o p fixesge(2*b)`,
  MESON_TAC[firstcontrol_subsetrange;xif_fixesge;fixesge_composes]);;

let lastcontrol_lemma2 = prove(
  `!p b x. bijection p ==> p fixesge(2*b) ==> x >= b ==>
           ~ODD(Xif (firstcontrol p) (p(2*x)))`,
  MESON_TAC[lastcontrol_lemma1;fixesge_double_odd;o_THM]);;

let lastcontrol_subsetrange = prove(
  `!p b. bijection p ==> p fixesge(2*b) ==>
         lastcontrol p subsetrange b`,
  REWRITE_TAC[subsetrange;lastcontrol] THEN
  MESON_TAC[lastcontrol_lemma2;GE;NOT_LT]);;

let lastcontrol_first_even = prove(
  `!p k. bijection p ==>
         ODD(Xif(firstcontrol p) (p(2*k))) =
         ODD(Xif(lastcontrol p) (2*k))`,
  REWRITE_TAC[xif_double_parity;lastcontrol]);;

let lastcontrol_first_odd = prove(
  `!p k. bijection p ==>
         ODD(Xif(firstcontrol p) (p(2*k+1))) =
         ODD(Xif(lastcontrol p) (2*k+1))`,
  REWRITE_TAC[xif_double_plus1_parity;lastcontrol] THEN
  REPEAT STRIP_TAC THEN
  ASM_MESON_TAC[XbackXforth_cyclemin_twist2_parity_double;
                firstcontrol_parity]);;

let lastcontrol_first = prove(
  `!p x. bijection p ==>
         ODD(Xif(firstcontrol p) (p x)) =
         ODD(Xif(lastcontrol p) x)`,
  REPEAT STRIP_TAC THEN
  DISJ_CASES_TAC (SPEC `x:num` EVEN_OR_ODD) THENL
  [
    ASM_MESON_TAC[EVEN_EXISTS;lastcontrol_first_even]
  ;
    ASM_MESON_TAC[odd_isdoubleplus1;lastcontrol_first_odd]
  ]);;

(* ----- middleperm *)

let middleperm_bijection = prove(
  `!p. bijection p ==> bijection(middleperm p)`,
  REWRITE_TAC[middleperm] THEN
  MESON_TAC[xif_involution;bijection_ifinvolution;
            bijection_composes]);;

let middleperm_fixesge = prove(
  `!p b. bijection p ==> p fixesge(2*b) ==>
         middleperm p fixesge(2*b)`,
  REWRITE_TAC[middleperm] THEN
  MESON_TAC[firstcontrol_subsetrange;lastcontrol_subsetrange;
            xif_fixesge;fixesge_composes]);;

let middleperm_parity = prove(
  `!p x. bijection p ==> ODD(middleperm p x) = ODD(x)`,
  REWRITE_TAC[middleperm;o_DEF] THEN
  MESON_TAC[xif_involution;involution;lastcontrol_first]);;

(* ----- review public definitions and theorems *)

let xor1 = xor1;;
let involution = involution;;
let surjection = surjection;;
let injection = injection;;
let bijection = bijection;;
let inverse = inverse;;
let pow_num = pow_num;;
let pow_int = pow_int;;
let cycle = cycle;;
let cyclemin = cyclemin;;
let partcycle = partcycle;;
let part2powcycle = part2powcycle;;
let fastcyclemin = fastcyclemin;;
let subsetrange = subsetrange;;
let fixesge = fixesge;;
let xif = xif;;
let XbackXforth = XbackXforth;;
let firstcontrol = firstcontrol;;
let lastcontrol = lastcontrol;;
let middleperm = middleperm;;
let cycle_shift = cycle_shift;;
let fastcyclemin_part2powcycle = fastcyclemin_part2powcycle;;
let fastcyclemin_works = fastcyclemin_works;;
let xor1_lteven = xor1_lteven;;
let xor1_div2 = xor1_div2;;
let xif_fixesge = xif_fixesge;;
let xif_involution = xif_involution;;
let XbackXforth_fixesge = XbackXforth_fixesge;;
let XbackXforth_bijection = XbackXforth_bijection;;
let XbackXforth_powpow_xor1 = XbackXforth_powpow_xor1;;
let XbackXforth_powpow_avoids_xor1 = XbackXforth_powpow_avoids_xor1;;
let XbackXforth_cycle_size = XbackXforth_cycle_size;;
let XbackXforth_cyclemin_xor1 = XbackXforth_cyclemin_xor1;;
let firstcontrol_subsetrange = firstcontrol_subsetrange;;
let lastcontrol_subsetrange = lastcontrol_subsetrange;;
let firstcontrol_0 = firstcontrol_0;;
let firstcontrol_parity = firstcontrol_parity;;
let lastcontrol_first = lastcontrol_first;;
let middleperm_bijection = middleperm_bijection;;
let middleperm_fixesge = middleperm_fixesge;;
let middleperm_parity = middleperm_parity;;