(*
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Mojmir Automata›

theory Mojmir
  imports Main Semi_Mojmir
begin

subsection ‹Definitions›

locale mojmir_def = semi_mojmir_def +
  fixes
    ― ‹Final States›
    F :: "'b set"
begin

definition token_succeeds :: "nat → bool"
where
  "token_succeeds x = (∃n. token_run x n ∈ F)"

definition token_fails :: "nat → bool"
where
  "token_fails x = (∃n. sink (token_run x n) ∧ token_run x n ∉ F)"

definition accept :: "bool" (‹accept_M›)
where
  "accept ⟷ (∀_\<infinity>x. token_succeeds x)"

definition fail :: "nat set"
where
  "fail = {x. token_fails x}"

definition merge :: "nat → (nat × nat) set"
where
  "merge i = {(x, y) | x y n j. j < i
    ∧ (token_run x n ≠ token_run y n ∧ rank y n ≠ None ∨ y = Suc n)
    ∧ token_run x (Suc n) = token_run y (Suc n)
    ∧ token_run x (Suc n) ∉ F
    ∧ rank x n = Some j}"

definition succeed :: "nat → nat set"
where
  "succeed i = {x. ∃n. rank x n = Some i
    ∧ token_run x n ∉ F - {q₀}
    ∧ token_run x (Suc n) ∈ F}"

definition smallest_accepting_rank :: "nat option"
where
  "smallest_accepting_rank ≡ (if accept then
    Some (LEAST i. finite fail ∧ finite (merge i) ∧ infinite (succeed i)) else None)"

definition fail_t :: "nat set"
where
  "fail_t = {n. ∃q q'. state_rank q n ≠ None ∧ q' = δ q (w n) ∧ q' ∉ F ∧ sink q'}"

definition merge_t :: "nat → nat set"
where
  "merge_t i = {n. ∃q q' j. state_rank q n = Some j ∧ j < i ∧ q' = δ q (w n) ∧ q' ∉ F ∧
    ((∃q''. q'' ≠ q ∧ q' = δ q'' (w n) ∧ state_rank q'' n ≠ None) ∨ q' = q₀)}"

definition succeed_t :: "nat → nat set"
where
  "succeed_t i = {n. ∃q. state_rank q n = Some i ∧ q ∉ F - {q₀} ∧ δ q (w n) ∈ F}"

fun "S"
where
  "S n = F ∪ {q. (∃j ≥ the smallest_accepting_rank. state_rank q n = Some j)}"

end

locale mojmir = semi_mojmir + mojmir_def +
  assumes
    ― ‹All states reachable from final states are also final›
    wellformed_F: "∧q ν. q ∈ F ==> δ q ν ∈ F"
begin

lemma token_stays_in_final_states:
  "token_run x n ∈ F ==> token_run x (n + m) ∈ F"
proof (induction m)
  case (Suc m)
    thus ?case
    proof (cases "n + m < x")
      case False
        hence "n + m ≥ x"
          by arith
        then obtain j where "n + m = x + j"
          using le_Suc_ex by blast
        hence "δ (token_run x (n + m)) (suffix x w j) = token_run x (n + (Suc m))"
          unfolding suffix_def by fastforce
        thus ?thesis
          using wellformed_F Suc suffix_nth by (metis (no_types, opaque_lifting))
    qed fastforce
qed simp

lemma token_run_enter_final_states:
  assumes "token_run x n ∈ F"
  shows "∃m ≥ x. token_run x m ∉ F - {q₀} ∧ token_run x (Suc m) ∈ F"
proof (cases "x ≤ n")
  case True
    then obtain n' where "token_run x (x + n') ∈ F"
      using assms by force
    hence "∃m. token_run x (x + m) ∉ F - {q₀} ∧ token_run x (x + Suc m) ∈ F"
      by (induction n') ((metis (erased, opaque_lifting) token_stays_in_final_states token_run_intial_state  Diff_iff Nat.add_0_right Suc_eq_plus1 insertCI ), blast)
    thus ?thesis
      by (metis add_Suc_right le_add1)
next
  case False
    hence "token_run x x ∉ F - {q₀}" and "token_run x (Suc x) ∈ F"
      using assms wellformed_F by simp_all
    thus ?thesis
      by blast
qed

subsection ‹Token Properties›

subsubsection ‹Alternative Definitions›

lemma token_succeeds_alt_def:
  "token_succeeds x = (∀_\<infinity>n. token_run x n ∈ F)"
  unfolding token_succeeds_def MOST_nat_le le_iff_add
  using token_stays_in_final_states by blast

lemma token_fails_alt_def:
  "token_fails x = (∀_\<infinity>n. sink (token_run x n) ∧ token_run x n ∉ F)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then obtain n where "sink (token_run x n)" and "token_run x n ∉ F"
    using token_fails_def by blast
  hence "∀m ≥ n. sink (token_run x m)" and "∀m ≥ n. token_run x m ∉ F"
    using token_stays_in_sink unfolding le_iff_add by auto
  thus ?rhs
    unfolding MOST_nat_le by blast
qed (unfold MOST_nat_le token_fails_def, blast)

lemma token_fails_alt_def_2:
  "token_fails x ⟷ ¬token_succeeds x ∧ ¬token_squats x"
  by (metis add.commute token_fails_def token_squats_def token_stays_in_final_states token_stays_in_sink token_succeeds_def)

subsubsection ‹Properties›

lemma token_succeeds_run_merge:
  "x ≤ n ==> y ≤ n ==> token_run x n = token_run y n ==> token_succeeds x ==> token_succeeds y"
  using token_run_merge token_stays_in_final_states add.commute unfolding token_succeeds_def by metis

lemma token_squats_run_merge:
  "x ≤ n ==> y ≤ n ==> token_run x n = token_run y n ==> token_squats x ==> token_squats y"
  using token_run_merge token_stays_in_sink add.commute unfolding token_squats_def by metis

subsubsection ‹Pulled-Up Lemmas›

lemma configuration_token_succeeds:
  "[x ∈ configuration q n; y ∈ configuration q n] ==> token_succeeds x = token_succeeds y"
  using token_succeeds_run_merge push_down_configuration_token_run by meson

lemma configuration_token_squats:
  "[x ∈ configuration q n; y ∈ configuration q n] ==> token_squats x = token_squats y"
  using token_squats_run_merge push_down_configuration_token_run by meson

subsection ‹Mojmir Acceptance›

lemma Mojmir_reject:
  "¬ accept ⟷ (∃_\<infinity>x. ¬token_succeeds x)"
  unfolding accept_def Alm_all_def by blast

lemma mojmir_accept_alt_def:
  "accept ⟷ finite {x. ¬token_succeeds x}"
  using Inf_many_def Mojmir_reject by blast

lemma mojmir_accept_initial:
  "q₀ ∈ F ==> accept"
  unfolding accept_def MOST_nat_le token_succeeds_def
  using token_run_intial_state by metis

subsection ‹Equivalent Acceptance Conditions›

subsubsection ‹Token-Based Definitions›

lemma merge_token_succeeds:
  assumes "(x, y) ∈ merge i"
  shows "token_succeeds x ⟷ token_succeeds y"
proof -
  obtain n j j' where "token_run x (Suc n) = token_run y (Suc n)"
    and "rank x n = Some j" and "rank y n = Some j' ∨ y = Suc n"
    using assms unfolding merge_def by blast
  hence "x ≤ Suc n" and "y ≤ Suc n"
    using rank_Some_time le_Suc_eq by blast+
  then obtain q where "x ∈ configuration q (Suc n)" and "y ∈ configuration q (Suc n)"
    using ‹token_run x (Suc n) = token_run y (Suc n)› pull_up_token_run_tokens by blast
  thus ?thesis
    using configuration_token_succeeds by blast
qed

lemma merge_subset:
   "i ≤ j ==> merge i ⊆ merge j"
proof
  assume "i ≤ j"
  fix p
  assume "p ∈ merge i"
  then obtain x y n k where "p = (x, y)" and "k < i" and "token_run x n ≠ token_run y n ∧ rank y n ≠ None ∨ y = Suc n"
    and "token_run x (Suc n) = token_run y (Suc n)" and "token_run x (Suc n) ∉ F" and "rank x n = Some k"
    unfolding merge_def by blast
  moreover
  hence "k < j"
    using ‹i ≤ j› by simp
  ultimately
  have "(x, y) ∈ merge j"
    unfolding merge_def by blast
  thus "p ∈ merge j"
    using ‹p = (x, y)› by simp
qed

lemma merge_finite:
  "i ≤ j ==> finite (merge j) ==> finite (merge i)"
  using merge_subset by (blast intro: rev_finite_subset)

lemma merge_finite':
  "i < j ==> finite (merge j) ==> finite (merge i)"
  using merge_finite[of i j] by force

lemma succeed_membership:
  "token_succeeds x ⟷ (∃i. x ∈ succeed i)"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  then obtain m where "token_run x m ∈ F"
    unfolding token_succeeds_alt_def MOST_nat_le by blast
  then obtain n where 1: "token_run x n ∉ F - {q₀}"
    and 2: "token_run x (Suc n) ∈ F" and "x ≤ n"
    using token_run_enter_final_states by blast
  moreover
  hence "¬sink (token_run x n)"
  proof (cases "token_run x n ≠ q₀")
    case True
      hence "token_run x n ∉ F"
        using ‹token_run x n ∉ F - {q₀}› by blast
      thus ?thesis
        using ‹token_run x (Suc n) ∈ F› token_stays_in_sink unfolding Suc_eq_plus1 by metis
  qed (simp add: sink_def)
  then obtain i where "rank x n = Some i"
    using ‹x ≤ n› by fastforce
  ultimately
  show ?rhs
    unfolding succeed_def by blast
qed (unfold token_succeeds_def succeed_def, blast)

lemma stable_rank_succeed:
  assumes "infinite (succeed i)"
      and "x ∈ succeed i"
      and "q₀ ∉ F"
  shows "¬stable_rank x i"
proof
  assume "stable_rank x i"
  then obtain n where "∀n' ≥ n. rank x n' = Some i"
    unfolding stable_rank_def MOST_nat_le by rule

  from assms(2) obtain m where "token_run x m ∉ F"
    and "token_run x (Suc m) ∈ F"
    and "rank x m = Some i"
    using assms(3) unfolding succeed_def by force

  obtain y where "y > max n m" and "y ∈ succeed i"
    using assms(1) unfolding infinite_nat_iff_unbounded by blast

  then obtain m' where "token_run y m' ∉ F"
    and "token_run y (Suc m') ∈ F"
    and "rank y m' = Some i"
    using assms(3) unfolding succeed_def by force

  moreover

  ― ‹token has still rank i at m'›
  have "m' ≥ n"
    using rank_Some_time[OF ‹rank y m' = Some i›] ‹y > max n m› by force
  hence "rank x m' = Some i"
    using  ‹∀n' ≥ n. rank x n' = Some i› by blast

  moreover

  ― ‹but x and y are not in the same state›
  have "m' ≥ Suc m"
    using rank_Some_time[OF ‹rank y m' = Some i›] ‹y > max n m› by force
  hence "token_run x m' ∈ F"
    using token_stays_in_final_states[OF ‹token_run x (Suc m) ∈ F›]
    unfolding le_iff_add by fast
  with ‹token_run y m' ∉ F › have "token_run y m' ≠ token_run x m'"
    by metis

  ultimately

  show "False"
    using push_down_rank_tokens by force
qed

lemma stable_rank_bounded:
  assumes stable: "stable_rank x j"
  assumes inf: "infinite (succeed i)"
  assumes "q₀ ∉ F"
  shows "j < i"
proof -
  from stable obtain m where "∀m' ≥ m. rank x m' = Some j"
    unfolding stable_rank_def MOST_nat_le by rule
  from inf obtain y where "y ≥ m" and "y ∈ succeed i"
    unfolding infinite_nat_iff_unbounded_le by meson
  then obtain n where "rank y n = Some i"
    unfolding succeed_def MOST_nat_le by blast

  moreover

  hence "n ≥ y"
    by (rule rank_Some_time)
  hence "rank x n = Some j"
    using ‹∀m' ≥ m. rank x m' = Some j› ‹y ≥ m› by fastforce

  ultimately

  ― ‹In the case @{term "i ≤ j"}, the token y has also to stabilise with @{term i} at @{term n}.›
  have "i ≤ j ==> stable_rank y i"
    using stable by (blast intro: stable_rank_tower)
  thus "j < i"
    using stable_rank_succeed[OF inf ‹y ∈ succeed i› ‹q₀ ∉ F›] by linarith
qed

― ‹Relation to Mojmir Acceptance›

lemma mojmir_accept_token_set_def1:
  assumes "accept"
  shows "∃i < max_rank. finite fail ∧ finite (merge i) ∧ infinite (succeed i) ∧ (∀j < i. finite (succeed j))"
proof (rule+)
  define i where "i = (LEAST k. infinite (succeed k))"

  from assms have "infinite {t. token_succeeds t}"
    unfolding mojmir_accept_alt_def by force

  moreover

  have "{x. token_succeeds x} = ∪{succeed i | i. i < max_rank}"
    (is "?lhs = ?rhs")
  proof -
    have "?lhs = ∪{succeed i | i. True}"
      using succeed_membership by blast
    also
    have "… = ?rhs"
    proof
      show "… ⊆ ?rhs"
      proof
        fix x
        assume "x ∈ ∪{succeed i |i. True}"
        then obtain i where "x ∈ succeed i"
          by blast
        moreover
        ― ‹Obtain upper bound for succeed ranks›
        have "∧u. u ≥ max_rank ==> succeed u = {}"
          unfolding succeed_def using rank_upper_bound by fastforce
        ultimately
        show "x ∈ ∪{succeed i |i. i < max_rank}"
          by (cases "i < max_rank") (blast, simp)
      qed
    qed blast
    finally
    show ?thesis .
  qed

  ultimately

  have "∃j. infinite (succeed j)"
    by force
  hence "infinite (succeed i)" and "∧j. j < i ==> finite (succeed j)"
    unfolding i_def by (metis LeastI_ex, metis not_less_Least)
  hence fin_succeed_ranks: "finite (∪{succeed j | j. j < i})"
    by auto

  ― ‹@{term i} is bounded by @{term max_rank}›
  {
    obtain x where "x ∈ succeed i"
      using ‹infinite (succeed i)› by fastforce
    then obtain n where "rank x n = Some i"
      unfolding succeed_def by blast
    thus "i < max_rank"
      by (rule rank_upper_bound)
  }

  define S where "S = {(x, y). token_succeeds x ∧ token_succeeds y}"

  have "finite (merge i ∩ S)"
  proof (rule finite_product)
    {
      fix x y
      assume "(x, y) ∈ (merge i ∩ S)"

      then obtain n k k'' where "k < i"
        and "rank x n = Some k"
        and "rank y n = Some k'' ∨ y = Suc n"
        and "token_run x (Suc n) ∉ F"
        and "token_run x (Suc n) = token_run y (Suc n)"
        and "token_succeeds x"
        unfolding merge_def S_def by fast

      then obtain m where "token_run x (Suc n + m) ∉ F"
        and "token_run x (Suc (Suc n + m)) ∈ F"
        by (metis Suc_eq_plus1 add.commute token_run_P[of "λq. q ∈ F"] token_stays_in_final_states token_succeeds_def)

      moreover

      have "x ≤ Suc n" and "y ≤ Suc n" and "x ≤ Suc n + m" and "y ≤ Suc n + m"
        using rank_Some_time ‹rank x n = Some k› ‹rank y n = Some k'' ∨ y = Suc n› by fastforce+

      hence "token_run y (Suc n + m) ∉ F" and "token_run y (Suc (Suc n + m)) ∈ F"
        using ‹token_run x (Suc n + m) ∉ F› ‹token_run x (Suc (Suc n + m)) ∈ F› ‹token_run x (Suc n) = token_run y (Suc n)›
        using token_run_merge token_run_merge_Suc by metis+

      moreover

      have "¬sink (token_run x (Suc n + m))"
        using ‹token_run x (Suc n + m) ∉ F› ‹token_run x (Suc(Suc n + m)) ∈ F›
        using token_is_not_in_sink by blast

      ― ‹Obtain rank used to enter final›
      obtain k' where "rank x (Suc n + m) = Some k'"
        using ‹¬sink (token_run x (Suc n + m))› ‹x ≤ Suc n + m› by fastforce

      moreover

      hence "rank y (Suc n + m) = Some k'"
        by (metis ‹x ≤ Suc n + m› ‹y ≤ Suc n + m› token_run_merge ‹x ≤ Suc n› ‹y ≤ Suc n›
                  ‹token_run x (Suc n) = token_run y (Suc n)› pull_up_token_run_tokens
                  pull_up_configuration_rank[of x _ "Suc n + m" y])

      moreover

      ― ‹Rank used to enter final states is strictly bounded by i›
      have "k' < i"
        using ‹rank x (Suc n + m) = Some k'› rank_monotonic[OF ‹rank x n = Some k›] ‹k < i›
        unfolding add_Suc_shift by fastforce

      ultimately

      have "x ∈ ∪{succeed j | j. j < i}" and "y ∈ ∪{succeed j | j. j < i}"
        unfolding succeed_def by blast+
    }
    hence "fst ` (merge i ∩ S) ⊆ ∪{succeed j | j. j < i}" and "snd ` (merge i ∩ S) ⊆ ∪{succeed j | j. j < i}"
      by force+
    thus "finite (fst ` (merge i ∩ S))" and "finite (snd ` (merge i ∩ S))"
      using finite_subset[OF _ fin_succeed_ranks] by meson+
  qed

  moreover

  have "finite (merge i ∩ (UNIV - S))"
  proof -
    obtain l where l_def: "∀x ≥ l. token_succeeds x"
      using assms unfolding accept_def MOST_nat_le by blast
    {
      fix x y
      assume "(x, y) ∈ merge i ∩ (UNIV - S)"
      hence "¬token_succeeds x ∨ ¬token_succeeds y"
        unfolding S_def by simp
      hence "¬token_succeeds x ∧ ¬token_succeeds y"
        using merge_token_succeeds ‹(x, y) ∈ merge i ∩ (UNIV - S)› by blast
      hence "x < l" and "y < l"
        by (metis l_def le_eq_less_or_eq linear)+
    }
    hence "merge i ∩ (UNIV - S) ⊆ {0..l} × {0..l}"
      by fastforce
    thus ?thesis
      using finite_subset by blast
  qed

  ultimately

  have "finite (merge i)"
    by (metis Int_Diff Un_Diff_Int finite_UnI inf_top_right)
  moreover
  have "finite fail"
    by (metis assms mojmir_accept_alt_def fail_def token_fails_alt_def_2 infinite_nat_iff_unbounded_le mem_Collect_eq)
  ultimately
  show "finite fail ∧ finite (merge i) ∧ infinite (succeed i) ∧ (∀j < i. finite (succeed j))"
    using ‹infinite (succeed i)› ‹∧j. j < i ==> finite (succeed j)› by blast
qed

lemma mojmir_accept_token_set_def2:
  assumes "finite fail"
      and "finite (merge i)"
      and "infinite (succeed i)"
  shows "accept"
proof (rule ccontr, cases "q₀ ∉ F")
  case True
    assume "¬ accept"
    moreover
    have "finite {x. ¬token_succeeds x ∧ ¬token_squats x}"
      using ‹finite fail› unfolding fail_def token_fails_alt_def_2[symmetric] .
    moreover
    have X: "{x. ¬ token_succeeds x} = {x. ¬ token_succeeds x ∧ token_squats x} ∪ {x. ¬ token_succeeds x ∧ ¬ token_squats x}"
      by blast
    ultimately
    have inf: "infinite {x. ¬token_succeeds x ∧ token_squats x}"
      unfolding mojmir_accept_alt_def X by blast

    ― ‹Obtain j, where j is the rank used by infinitely many configuration stabilising and not succeeding›
    have "{x. ¬token_succeeds x ∧ token_squats x} = {x. ∃j < i. ¬token_succeeds x ∧ token_squats x ∧ stable_rank x j}"
      using stable_rank_bounded ‹infinite (succeed i)› ‹q₀ ∉ F›
      unfolding stable_rank_equiv_token_squats by metis
    also
    have "… = ∪{{x. ¬token_succeeds x ∧ token_squats x ∧ stable_rank x j} | j. j < i}"
      by blast
    finally
    obtain j where "j < i" and "infinite {t. ¬token_succeeds t ∧ token_squats t ∧ stable_rank t j}"
      (is "infinite ?S")
      using inf by force

    ― ‹Obtain such a token x›
    then obtain x where "¬token_succeeds x" and "token_squats x" and "stable_rank x j"
      unfolding infinite_nat_iff_unbounded_le by blast
    then obtain n where "∀m ≥ n. rank x m = Some j"
      unfolding stable_rank_def MOST_nat_le by blast

    ― ‹All configuration with same stable rank are bought at some n with rank smaller i›
    have "{(x, y) | y. y > n ∧ stable_rank y j} ⊆ merge i"
      (is "?lhs ⊆ ?rhs")
    proof
      fix p
      assume "p ∈ ?lhs"
      then obtain y where "p = (x, y)" and "y > n" and "stable_rank y j"
        by blast
      hence "x < y" and "x ≠ y"
        using rank_Some_time ‹∀n'≥n. rank x n' = Some j› by fastforce+

      moreover

      ― ‹Obtain a time n'' where x and y have the same rank›
      obtain n'' where "rank x n'' = Some j" and "rank y n'' = Some j"
        using ‹∀n'≥n. rank x n' = Some j› ‹stable_rank y j›
        unfolding stable_rank_def MOST_nat_le by (metis add.commute le_add2)
      hence "token_run x n'' = token_run y n''" and "y ≤ n''"
        using push_down_rank_tokens rank_Some_time[OF ‹rank y n'' = Some j›] by simp_all

      ― ‹Obtain the time n' where x merges y and proof all necessary properties›
      then obtain n' where "token_run x n' ≠ token_run y n' ∨ y = Suc n'"
        and "token_run x (Suc n') = token_run y (Suc n')" and "y ≤ Suc n'"
        using token_run_mergepoint[OF ‹x < y›] le_add_diff_inverse by metis

      moreover

      hence "(∃j'. rank y n' = Some j') ∨ y = Suc n'"
        using ‹stable_rank y j› stable_rank_equiv_token_squats rank_token_squats
        unfolding le_Suc_eq by blast

      moreover

      have "rank x n' = Some j"
        using ‹∀n'≥n. rank x n' = Some j› ‹y ≤ Suc n'› ‹y > n› by fastforce

      moreover

      have "token_run x (Suc n') ∉ F"
        using ‹¬ token_succeeds x› token_succeeds_def by blast

      ultimately
      show "p ∈ ?rhs"
        unfolding merge_def ‹p = (x, y)›
        using ‹j < i› by blast
    qed

    moreover

    ― ‹However, x merges infinitely many configuration›
    hence "infinite {(x, y) | y. y > n ∧ stable_rank y j}"
      (is "infinite ?S'")
    proof -
      {
        {
          fix y
          assume "stable_rank y j" and "y > n"
          then obtain n' where "rank y n' = Some j"
            unfolding stable_rank_def MOST_nat_le by blast
          moreover
          hence "y ≤ n'"
            by (rule rank_Some_time)
          hence "n' > n"
            using ‹y > n› by arith
          hence "rank x n' = Some j"
            using ‹∀n' ≥ n. rank x n' = Some j› by simp
          ultimately
          have "¬token_succeeds y"
            by (metis ‹¬token_succeeds x› configuration_token_succeeds push_down_rank_tokens)
        }
        hence "{y | y. y > n ∧ stable_rank y j} = {y | y. token_squats y ∧ ¬token_succeeds y ∧ stable_rank y j ∧ y > n}"
          (is "_ = ?S''")
          using stable_rank_equiv_token_squats by blast
        moreover
        have "finite {y | y. token_squats y ∧ ¬token_succeeds y ∧ stable_rank y j ∧ y ≤ n}"
          (is "finite ?S'''")
          by simp
        moreover
        have "?S = ?S'' ∪ ?S'''"
          by auto
        ultimately
        have "infinite {y | y. y > n ∧ stable_rank y j}"
          using ‹infinite ?S› by simp
      }
      moreover
      have "{x} × {y. y > n ∧ stable_rank y j} = ?S'"
        by auto
      ultimately
      show ?thesis
        by (metis empty_iff finite_cartesian_productD2 singletonI)
    qed

    ultimately

    have "infinite (merge i)"
      by (rule infinite_super)
    with ‹finite (merge i)› show "False"
      by blast
qed (blast intro: mojmir_accept_initial)

theorem mojmir_accept_iff_token_set_accept:
  "accept ⟷ (∃i < max_rank. finite fail ∧ finite (merge i) ∧ infinite (succeed i))"
  using mojmir_accept_token_set_def1 mojmir_accept_token_set_def2 by blast

theorem mojmir_accept_iff_token_set_accept2:
  "accept ⟷ (∃i < max_rank. finite fail ∧ finite (merge i) ∧ infinite (succeed i) ∧ (∀j < i. finite (merge j) ∧ finite (succeed j)))"
  using mojmir_accept_token_set_def1 mojmir_accept_token_set_def2 merge_finite' by blast

subsubsection ‹Time-Based Definitions›

― ‹Proof Rules›

lemma finite_monotonic_image:
  fixes A B :: "nat set"
  assumes "∧i. i ∈ A ==> i ≤ f i"
  assumes "f ` A = B"
  shows "finite A ⟷ finite B"
proof
  assume "finite B"
  thus "finite A"
  proof (cases "B ≠ {}")
    case True
      hence "∧i. i ∈ A ==> i ≤ Max B"
        by (metis assms Max_ge_iff ‹finite B› imageI)
      thus "finite A"
        unfolding finite_nat_set_iff_bounded_le by blast
  qed (metis assms(2) image_is_empty)
qed (metis assms(2) finite_imageI)

lemma finite_monotonic_image_pairs:
  fixes A :: "(nat × nat) set"
  fixes B :: "nat set"
  assumes "∧i. i ∈ A ==> (fst i) ≤ f i + c"
  assumes "∧i. i ∈ A ==> (snd i) ≤ f i + d"
  assumes "f ` A = B"
  shows "finite A ⟷ finite B"
proof
  assume "finite B"
  thus "finite A"
  proof (cases "B ≠ {}")
    case True
      hence "∧i. i ∈ A ==> fst i ≤ Max B + c ∧ snd i ≤ Max B + d"
        by (metis assms Max_ge_iff ‹finite B› imageI le_diff_conv)
      thus "finite A"
        using finite_product[of A] unfolding finite_nat_set_iff_bounded_le by blast
  qed (metis assms(3) finite.emptyI image_is_empty)
qed (metis assms(3) finite_imageI)

lemma token_time_finite_rule:
  fixes A B :: "nat set"
  assumes unique:  "∧x y z. P x y ==> P x z ==> y = z"
      and existsA: "∧x. x ∈ A ==> (∃y. P x y)"
      and existsB: "∧y. y ∈ B ==> (∃x. P x y)"
      and inA:     "∧x y. P x y ==> x ∈ A"
      and inB:     "∧x y. P x y ==> y ∈ B"
      and mono:    "∧x y. P x y ==> x ≤ y"
  shows "finite A ⟷ finite B"
proof (rule finite_monotonic_image)
  let ?f = "(λx. if x ∈ A then The (P x) else undefined)"

  {
    fix x
    assume "x ∈ A"
    then obtain y where "P x y" and "y = ?f x"
      using existsA the_equality unique by metis
    thus "x ≤ ?f x"
      using mono by blast
  }

  {
    fix y
    have "y ∈ ?f ` A ⟷ (∃x. x ∈ A ∧ y = The (P x))"
      unfolding image_def by force
    also
    have "… ⟷ (∃x. P x y)"
      by (metis inA existsA unique the_equality)
    also
    have "… ⟷ y ∈ B"
      using inB existsB by blast
    finally
    have "y ∈ ?f ` A ⟷ y ∈ B"
      .
  }
  thus "?f ` A = B"
    by blast
qed

lemma token_time_finite_pair_rule:
  fixes A :: "(nat × nat) set"
  fixes B :: "nat set"
  assumes unique:  "∧x y z. P x y ==> P x z ==> y = z"
      and existsA: "∧x. x ∈ A ==> (∃y. P x y)"
      and existsB: "∧y. y ∈ B ==> (∃x. P x y)"
      and inA:     "∧x y. P x y ==> x ∈ A"
      and inB:     "∧x y. P x y ==> y ∈ B"
      and mono:    "∧x y. P x y ==> fst x ≤ y + c ∧ snd x ≤ y + d"
  shows "finite A ⟷ finite B"
proof (rule finite_monotonic_image_pairs)
  let ?f = "(λx. if x ∈ A then The (P x) else undefined)"

  {
    fix x
    assume "x ∈ A"
    then obtain y where "P x y" and "y = ?f x"
      using existsA the_equality unique by metis
    thus "fst x ≤ ?f x + c" and "snd x ≤ ?f x + d"
      using mono by blast+
  }

  {
    fix y
    have "y ∈ ?f ` A ⟷ (∃x. x ∈ A ∧ y = The (P x))"
      unfolding image_def by force
    also
    have "… ⟷ (∃x. P x y)"
      by (metis inA existsA unique the_equality)
    also
    have "… ⟷ y ∈ B"
      using inB existsB by blast
    finally
    have "y ∈ ?f ` A ⟷ y ∈ B"
      .
  }
  thus "?f ` A = B"
    by blast
qed

― ‹Correspondence Between Token- and Time-Based Definitions›

lemma fail_t_inclusion:
  assumes "x ≤ n"
  assumes "¬sink (token_run x n)"
  assumes "sink (token_run x (Suc n))"
  assumes "token_run x (Suc n) ∉ F"
  shows "n ∈ fail_t"
proof -
  define q q' where "q = token_run x n" and "q' = token_run x (Suc n)"
  hence *: "¬sink q" "sink q'" and "q' ∉ F"
    using assms by blast+
  moreover
  from * have **: "state_rank q n ≠ None"
    unfolding q_def by (metis oldest_token_always_def option.distinct(1) state_rank_None)
  moreover
  from ** have "q' = δ q (w n)"
    unfolding q_def q'_def using assms(1) token_run_step' by blast
  ultimately
  show "n ∈ fail_t"
    unfolding fail_t_def by blast
qed

lemma merge_t_inclusion:
  assumes "x ≤ n"
  assumes "(∃j'. token_run x n ≠ token_run y n ∧ y ≤ n ∧ state_rank (token_run y n) n = Some j') ∨ y = Suc n"
  assumes "token_run x (Suc n) = token_run y (Suc n)"
  assumes "token_run x (Suc n) ∉ F"
  assumes "state_rank (token_run x n) n = Some j"
  assumes "j < i"
  shows "n ∈ merge_t i"
proof -
  define q q' q''
    where "q = token_run x n"
      and "q' = token_run x (Suc n)"
      and "q'' = token_run y n"
  have "y ≤ Suc n"
    using assms(2) by linarith
  hence "(q' = δ q'' (w n) ∧ state_rank q'' n ≠ None ∧ q'' ≠ q) ∨ q' = q₀"
    unfolding q_def q'_def q''_def using assms(2-3)
    by (cases "y = Suc n") ((metis token_run_intial_state), (metis option.distinct(1) token_run_step))
  moreover
  have "state_rank q n = Some j ∧ j < i ∧ q' = δ q (w n) ∧ q' ∉ F"
    unfolding q_def q'_def using token_run_step[OF assms(1)] assms(4-6) by blast
  ultimately
  show "n ∈ merge_t i"
    unfolding merge_t_def by blast
qed

lemma succeed_t_inclusion:
  assumes "rank x n = Some i"
  assumes "token_run x n ∉ F - {q₀}"
  assumes "token_run x (Suc n) ∈ F"
  shows "n ∈ succeed_t i"
proof -
  define q where "q = token_run x n"
  hence "state_rank q n = Some i" and "q ∉ F - {q₀}" and "δ q (w n) ∈ F"
    using token_run_step' rank_Some_time[OF assms(1)] assms rank_eq_state_rank by auto
  thus "n ∈ succeed_t i"
    unfolding succeed_t_def by blast
qed

lemma finite_fail_t:
  "finite fail = finite fail_t"
proof (rule token_time_finite_rule)
  let ?P = "(λx n. x ≤ n
    ∧ ¬sink (token_run x n)
    ∧ sink (token_run x (Suc n))
    ∧ token_run x (Suc n) ∉ F)"

  {
    fix x
    have "¬sink (token_run x x)"
      unfolding sink_def by simp

    assume "x ∈ fail"
    hence "token_fails x"
      unfolding fail_def ..
    moreover
    then obtain y'' where "sink (token_run x (Suc (x + y'')))"
      unfolding token_fails_alt_def MOST_nat
      using ‹¬ sink (token_run x x)› less_add_Suc2 by blast
    then obtain y' where "¬sink (token_run x (x + y'))" and "sink (token_run x (Suc (x + y')))"
      using token_run_P[of "λq. sink q", OF ‹¬sink (token_run x x)›] by blast
    ultimately
    show "∃y. ?P x y"
      using token_fails_alt_def_2 token_succeeds_def by (metis le_add1)
  }

  {
    fix y
    assume "y ∈ fail_t"
    then obtain q q' i where "state_rank q y = Some i" and "q' = δ q (w y)" and "q' ∉ F" and "sink q'"
      unfolding fail_t_def by blast
    moreover
    then obtain x where "token_run x y = q" and "x ≤ y"
      by (blast dest: push_down_state_rank_token_run)
    moreover
    hence "token_run x (Suc y) = q'"
      using token_run_step[OF _ _ ‹q' = δ q (w y)›] by blast
    ultimately
    show "∃x. ?P x y"
      by (metis option.distinct(1) state_rank_sink)
  }

  {
    fix x y
    assume "?P x y"
    thus "x ∈ fail" and "x ≤ y" and "y ∈ fail_t"
      unfolding fail_def using token_fails_def fail_t_inclusion by blast+
  }

  ― ‹Uniqueness›
  {
    fix x y z
    assume "?P x y" and "?P x z"
    from ‹?P x y› have "¬sink (token_run x y)" and "sink (token_run x (Suc y))"
      by blast+
    moreover
    from ‹?P x z› have "¬sink (token_run x z)" and "sink (token_run x (Suc z))"
      by blast+
    ultimately
    show "y = z"
      using token_stays_in_sink
      by (cases y z rule: linorder_cases, simp_all)
         (metis (no_types, lifting) Suc_leI le_add_diff_inverse)+
  }
qed

lemma finite_succeed_t':
  assumes "q₀ ∉ F"
  shows "finite (succeed i) = finite (succeed_t i)"
proof (rule token_time_finite_rule)
  let ?P = "(λx n. x ≤ n
    ∧ state_rank (token_run x n) n = Some i
    ∧ (token_run x n) ∉ F - {q₀}
    ∧ (token_run x (Suc n)) ∈ F)"

  {
    fix x
    assume "x ∈ succeed i"
    then obtain y where "token_run x y ∉ F - {q₀}" and "token_run x (Suc y) ∈ F" and "rank x y = Some i"
       unfolding succeed_def by force
    moreover
    hence "rank (senior x y) y = Some i"
      using rank_Some_time[THEN rank_senior_senior] by presburger
    hence "state_rank (token_run x y) y = Some i"
      unfolding state_rank_eq_rank senior.simps by (metis oldest_token_always_def option.sel option.simps(5))
    ultimately
    show "∃y. ?P x y"
      using rank_Some_time by blast
  }

  {
    fix y
    assume "y ∈ succeed_t i"
    then obtain q where "state_rank q y = Some i" and "q ∉ F - {q₀}" and "(δ q (w y)) ∈ F"
      unfolding succeed_t_def by blast
    moreover
    then obtain x where "q = token_run x y" and "x ≤ y"
      by (metis oldest_token_bounded push_down_oldest_token_token_run push_down_state_rank_oldest_token)
    moreover
    hence "token_run x (Suc y) ∈ F"
      using token_run_step ‹(δ q (w y)) ∈ F› by simp
    ultimately
    show "∃x. ?P x y"
      by meson
  }

  {
    fix x y
    assume "?P x y"
    thus "x ≤ y" and "x ∈ succeed i" and "y ∈ succeed_t i"
      unfolding succeed_def using rank_eq_state_rank[of x y] succeed_t_inclusion
      by (metis (mono_tags, lifting) mem_Collect_eq)+
  }

  ― ‹Uniqueness›
  {
    fix x y z
    assume "?P x y" and "?P x z"
    from ‹?P x y› have "token_run x y ∉ F" and "token_run x (Suc y) ∈ F"
      using ‹q₀ ∉ F› by auto
    moreover
    from ‹?P x z› have "token_run x z ∉ F" and "token_run x (Suc z) ∈ F"
      using ‹q₀ ∉ F› by auto
    ultimately
    show "y = z"
      using token_stays_in_final_states
      by (cases y z rule: linorder_cases, simp_all)
         (metis le_Suc_ex less_Suc_eq_le not_le)+
  }
qed

lemma initial_in_F_token_run:
  assumes "q₀ ∈ F"
  shows "token_run x y ∈ F"
  using assms token_stays_in_final_states[of _ 0] by fastforce

lemma finite_succeed_t'':
  assumes "q₀ ∈ F"
  shows "finite (succeed i) = finite (succeed_t i)"
  (is "?lhs = ?rhs")
proof
  have "succeed_t i = {n. state_rank q₀ n = Some i}"
    unfolding succeed_t_def using initial_in_F_token_run assms wellformed_F by auto
  also
  have "... = {n. rank n n = Some i}"
    unfolding rank_eq_state_rank[OF order_refl] token_run_intial_state ..
  finally
  have succeed_t_alt_def: "succeed_t i = {n. rank n n = Some i ∧ token_run n n = q₀}"
    by simp

  have succeed_alt_def: "succeed i = {x. ∃n. rank x n = Some i ∧ token_run x n = q₀}"
    unfolding succeed_def using initial_in_F_token_run[OF assms] by auto

  {
    assume ?lhs
    moreover
    have "succeed_t i ⊆ succeed i"
      unfolding succeed_t_alt_def succeed_alt_def by blast
    ultimately
    show ?rhs
      by (rule rev_finite_subset)
  }

  {
    assume ?rhs
    then obtain U where U_def: "∧x. x ∈ succeed_t i ==> U ≥ x"
      unfolding finite_nat_set_iff_bounded_le by blast
    {
      fix x
      assume "x ∈ succeed i"
      then obtain n where "rank x n = Some i" and "token_run x n = q₀"
        unfolding succeed_alt_def by blast
      moreover
      hence "x ≤ n"
        by (blast dest: rank_Some_time)
      moreover
      hence "rank n n = Some i"
        using ‹rank x n = Some i› ‹token_run x n = q₀›
        by (metis order_refl token_run_intial_state[of n] pull_up_token_run_tokens pull_up_configuration_rank)
      hence "n ∈ succeed_t i"
        unfolding succeed_t_alt_def by simp
      ultimately
      have "U ≥ x"
        using U_def by fastforce
    }
    thus ?lhs
      unfolding finite_nat_set_iff_bounded_le by blast
  }
qed

lemma finite_succeed_t:
  "finite (succeed i) = finite (succeed_t i)"
  using finite_succeed_t' finite_succeed_t'' by blast

lemma finite_merge_t:
  "finite (merge i) = finite (merge_t i)"
proof (rule token_time_finite_pair_rule)
  let ?P = "(λ(x, y) n. ∃j. x ≤ n
    ∧ ((∃j'. token_run x n ≠ token_run y n ∧ y ≤ n ∧ state_rank (token_run y n) n = Some j') ∨ y = Suc n)
    ∧ token_run x (Suc n) = token_run y (Suc n)
    ∧ token_run x (Suc n) ∉ F
    ∧ state_rank (token_run x n) n = Some j
    ∧ j < i)"

  {
    fix x
    assume "x ∈ merge i"
    then obtain t t' n j where 1: "x = (t, t')"
      and 3: "(∃j'. token_run t n ≠ token_run t' n ∧ rank t' n = Some j') ∨ t' = Suc n"
      and 4: "token_run t (Suc n) = token_run t' (Suc n)"
      and 5: "token_run t (Suc n) ∉ F"
      and 6: "rank t n = Some j"
      and 7:  "j < i"
      unfolding merge_def by blast
    moreover
    hence 8: "t ≤ n" and 9: "t' ≤ Suc n"
      using rank_Some_time le_Suc_eq by blast+
    moreover
    hence 10: "state_rank (token_run t n) n = Some j"
      using ‹rank t n = Some j› rank_eq_state_rank by metis
    ultimately
    show "∃y. ?P x y"
    proof (cases "t' = Suc n")
      case False
        hence "t' ≤ n"
          using ‹t' ≤ Suc n› by simp
        with 1 3 4 5 7 8 10 show ?thesis
          unfolding rank_eq_state_rank[OF ‹t' ≤ n›] by blast
    qed blast
  }

  {
    fix y
    assume "y ∈ merge_t i"
    then obtain q q' j where 1: "state_rank q y = Some j"
      and 2: "j < i"
      and 3: "q' = δ q (w y)"
      and 4: "q' ∉ F"
      and 5: "(∃q''. q' = δ q'' (w y) ∧ state_rank q'' y ≠ None ∧ q'' ≠ q) ∨ q' = q₀"
      unfolding merge_t_def by blast

    then obtain t where 6: "q = token_run t y" and 7: "t ≤ y"
      using push_down_state_rank_token_run by metis
    hence 8: "q' = token_run t (Suc y)"
      unfolding ‹q' = δ q (w y)› using token_run_step by simp

    {
      assume "q' = q₀"
      hence "token_run t (Suc y) = token_run (Suc y) (Suc y)"
        unfolding 8 by simp
      moreover
      then obtain x where "x = (t, Suc y)"
        by simp
      ultimately
      have "?P x y"
        using 1 2 3 4 5 7 unfolding 6 8 by force
      hence "∃x. ?P x y"
        by blast
    }
    moreover
    {
      assume "q' ≠ q₀"
      then obtain q'' j' where 9: "q' = δ q'' (w y)"
        and "state_rank q'' y = Some j'"
        and "q'' ≠ q"
        using 5 by blast
      moreover
      then obtain t' where 12: "q'' = token_run t' y" and "t' ≤ y"
        by (blast dest: push_down_state_rank_token_run)
      moreover
      hence "token_run t (Suc y) = token_run t' (Suc y)"
        using 8 9 token_run_step by presburger
      moreover
      have "token_run t y ≠ token_run t' y"
        using ‹q'' ≠ q› unfolding 6 12 ..
      moreover
      then obtain x where "x = (t, t')"
        by simp
      ultimately
      have "?P x y"
        using 1 2 4 7 unfolding 6 8 by fast
      hence "∃x. ?P x y"
        by blast
    }
    ultimately
    show "∃x. ?P x y"
      by blast
  }

  {
    fix x y
    assume "?P x y"
    then obtain t t' j where 1: "x = (t, t')"
      and 3: "t ≤ y"
      and 4: "(∃j'. token_run t y ≠ token_run t' y ∧ t' ≤ y ∧ state_rank (token_run t' y) y = Some j') ∨ t' = Suc y"
      and 5: "token_run t (Suc y) = token_run t' (Suc y)"
      and 6: "token_run t (Suc y) ∉ F"
      and 7: "state_rank (token_run t y) y = Some j"
      and 8: "j < i"
      by blast

    thus "x ∈ merge i"
    proof (cases "t' = Suc y")
      case False
        hence "t' ≤ y"
          using 4 by blast
        thus ?thesis
          using 1 3 4 5 6 7 8 unfolding merge_def
          unfolding rank_eq_state_rank[OF ‹t' ≤ y›, symmetric] rank_eq_state_rank[OF ‹t ≤ y›, symmetric]
          by blast
    qed (unfold rank_eq_state_rank[OF ‹t ≤ y›, symmetric] merge_def, blast)

    show "y ∈ merge_t i" and "fst x ≤ y + 0 ∧ snd x ≤ y + 1"
      using merge_t_inclusion ‹?P x y› by force+
  }

  ― ‹Uniqueness›
  {
    fix x y z
    assume "?P x y" and "?P x z"
    then obtain t t' where "x = (t, t')"
      by blast
    from ‹?P x y›[unfolded ‹x = (t, t')›] have y1: "t ≤ y"
      and y2: "(token_run t y ≠ token_run t' y ∧ t' ≤ y) ∨ t' = Suc y"
      and y3: "token_run t (Suc y) = token_run t' (Suc y)" by blast+
    moreover
    from ‹?P x z›[unfolded ‹x = (t, t')›] have z1: "t ≤ z"
      and z2: "(token_run t z ≠ token_run t' z ∧ t' ≤ z) ∨ t' = Suc z"
      and z3: "token_run t (Suc z) = token_run t' (Suc z)" by blast+
    moreover
    have y4: "t' ≤ Suc y" and z4: "t' ≤ Suc z"
      using y2 z2 by linarith+
    ultimately
    show "y = z"
    proof (cases y z rule: linorder_cases)
      case less
        then obtain d where "Suc y + d = z"
          by (metis add_Suc_right add_Suc_shift less_imp_Suc_add)
        thus ?thesis
          using y1 y2 z2 token_run_merge[OF _ y4 y3] by auto
    next
      case greater
        then obtain d where "Suc z + d = y"
          by (metis add_Suc_right add_Suc_shift less_imp_Suc_add)
        thus ?thesis
          using z1 y2 z2 token_run_merge[OF _ z4 z3] by auto
    qed
  }
qed

subsubsection ‹Relation to Mojmir Acceptance›

lemma token_iff_time_accept:
  shows "(finite fail ∧ finite (merge i) ∧ infinite (succeed i) ∧ (∀j < i. finite (succeed j)))
       = (finite fail_t ∧ finite (merge_t i) ∧ infinite (succeed_t i) ∧ (∀j < i. finite (succeed_t j)))"
  unfolding finite_fail_t finite_merge_t finite_succeed_t by simp

subsection ‹Succeeding Tokens (Alternative Definition)›

definition stable_rank_at :: "nat → nat → bool"
where
  "stable_rank_at x n ≡ ∃i. ∀m ≥ n. rank x m = Some i"

lemma stable_rank_at_ge:
  "n ≤ m ==> stable_rank_at x n ==> stable_rank_at x m"
  unfolding stable_rank_at_def by fastforce

lemma stable_rank_equiv:
  "(∃i. stable_rank x i) = (∃n. stable_rank_at x n)"
  unfolding stable_rank_def MOST_nat_le stable_rank_at_def by blast

lemma smallest_accepting_rank_properties:
  assumes "smallest_accepting_rank = Some i"
  shows "accept" "finite fail" "finite (merge i)" "infinite (succeed i)" "∀j < i. finite (succeed j)" "i < max_rank"
proof -
  from assms show "accept"
    unfolding smallest_accepting_rank_def using option.distinct(1) by metis
  then obtain i' where "finite fail" and "finite (merge i')" and "infinite (succeed i')"
    and "∀j < i'. finite (succeed j)" and "i' < max_rank"
    unfolding mojmir_accept_iff_token_set_accept2 by blast
  moreover
  hence "∧y. finite fail ∧ finite (merge y) ∧ infinite (succeed y) ⟶ i' ≤ y"
    using not_le by blast
  ultimately
  have "(LEAST i. finite fail ∧ finite (merge i) ∧ infinite (succeed i)) = i'"
    using le_antisym unfolding Least_def by (blast dest: the_equality[of _ i'])
  hence "i' = i"
    using ‹smallest_accepting_rank = Some i› ‹accept› unfolding smallest_accepting_rank_def by simp
  thus "finite fail" and "finite (merge i)" and "infinite (succeed i)"
    and "∀j < i. finite (succeed j)" and "i < max_rank"
    using ‹finite fail› ‹finite (merge i')› ‹infinite (succeed i')›
    using ‹∀j < i'. finite (succeed j)› ‹i' < max_rank› by simp+
qed

lemma token_smallest_accepting_rank:
  assumes "smallest_accepting_rank = Some i"
  shows "∀_\<infinity>n. ∀x. token_succeeds x ⟷ (x > n ∨ (∃j ≥ i. rank x n = Some j) ∨ token_run x n ∈ F)"
proof -
  from assms have "accept" "finite fail" "infinite (succeed i)" "∀j < i. finite (succeed j)"
    using smallest_accepting_rank_properties by blast+

  then obtain n₁ where n₁_def: "∀x ≥ n₁. token_succeeds x"
    unfolding accept_def MOST_nat_le by blast
  define n₂ where "n₂ = Suc (Max (fail_t ∪ ∪{succeed_t j | j. j < i}))" (is "_ = Suc (Max ?S)")
  define n₃ where "n₃ = Max ({LEAST m. stable_rank_at x m | x. x < n₁ ∧ token_squats x})" (is "_ = Max ?S'")
  define n where "n = Max {n₁, n₂, n₃}"

  have "finite ?S" and "finite ?S'"
    using ‹finite fail› ‹∀j < i. finite (succeed j)›
    unfolding finite_fail_t finite_succeed_t by fastforce+

  {
    fix x
    assume "x < n₁" "token_squats x"
    hence "(LEAST m. stable_rank_at x m) ∈ ?S'" (is "?m ∈ _")
      by blast
    hence "?m ≤ n₃"
      using Max.coboundedI[OF ‹finite ?S'›] n₃_def by simp
    moreover
    obtain k where "stable_rank x k"
      using ‹x < n₁› ‹token_squats x› stable_rank_equiv_token_squats by blast
    hence "stable_rank_at x ?m"
      by (metis stable_rank_equiv LeastI)
    ultimately
    have "stable_rank_at x n₃"
      by (rule stable_rank_at_ge)
    hence "∃i. ∀m' ≥ n. rank x m' = Some i"
      unfolding n_def stable_rank_at_def by fastforce
  }
  note Stable = this

  have "∧m j. j < i ==> m ∈ succeed_t j ==> m < n"
    using Max.coboundedI[OF ‹finite ?S›] unfolding n_def n₂_def by fastforce
  hence Succeed: "∧m j x. n ≤ m ==> token_run x m ∉ F - {q₀} ==> token_run x (Suc m) ∈ F ==> rank x m = Some j ==> i ≤ j"
    by (metis not_le succeed_t_inclusion)

  have "∧m. m ∈ fail_t ==> m < n"
    using Max.coboundedI[OF ‹finite ?S›] unfolding n_def n₂_def by fastforce
  hence Fail: "∧m x. n ≤ m ==> x ≤ m ==> sink (token_run x m) ∨ ¬sink (token_run x (Suc m)) ∨ ¬token_run x (Suc m) ∉ F"
    using fail_t_inclusion by fastforce

  {
    fix m x
    assume "m ≥ n" "m ≥ x"
    moreover
    {
      assume "token_succeeds x" "token_run x m ∉ F"
      then obtain m' where "x ≤ m'" and "token_run x m' ∉ F - {q₀}" and "token_run x (Suc m') ∈ F"
        using token_run_enter_final_states unfolding token_succeeds_def by meson
      moreover
      hence "¬sink (token_run x m')"
        by (metis Diff_empty Diff_insert0 ‹token_run x m ∉ F› initial_in_F_token_run token_is_not_in_sink)
      ultimately
      obtain j' where "rank x m' = Some j'"
        by simp
      moreover
      have "m ≤ m'"
        by (metis ‹token_run x m ∉ F› token_stays_in_final_states[OF ‹token_run x (Suc m') ∈ F›] add_Suc_right add_Suc_shift less_imp_Suc_add not_le)
      moreover
      hence "m' ≥ n"
        using ‹x ≤ m› ‹m ≥ n› by simp
      hence "j' ≥ i"
        using Succeed[OF _ ‹token_run x m' ∉ F - {q₀}› ‹token_run x (Suc m') ∈ F› ‹rank x m' = Some j'›] by blast
      moreover
      obtain k where "rank x x = Some k"
        using rank_initial[of x] by blast
      ultimately
      obtain j where "rank x m = Some j"
        by (metis rank_continuous[OF ‹rank x x = Some k›, of "m' - x"] ‹x ≤ m'› ‹x ≤ m› diff_le_mono le_add_diff_inverse)
      hence "∃j ≥ i. rank x m = Some j"
        using rank_monotonic ‹rank x m' = Some j'› ‹j' ≥ i› ‹m ≤ m'›[THEN le_Suc_ex]
        by (blast dest: le_Suc_ex trans_le_add1)
    }
    moreover
    {
      assume "¬token_succeeds x"
      hence "∧m. token_run x m ∉ F"
        unfolding token_succeeds_def by blast
      moreover
      have "¬(∃j ≥ i. rank x m = Some j)"
      proof (cases "token_squats x")
        case True
          ― ‹The token already stabilised›
          have "x < n₁"
            using ‹¬token_succeeds x› n₁_def by (metis not_le)
          then obtain k where "∀m' ≥ n. rank x m' = Some k"
            using Stable[OF _ True] by blast
          moreover
          hence "stable_rank x k"
            unfolding stable_rank_def MOST_nat_le by blast
          moreover
          have "q₀ ∉ F"
            by (metis ‹∧m. token_run x m ∉ F› initial_in_F_token_run)
          ultimately
          ― ‹Hence the rank is smaller than i›
          have "k < i" and "rank x m = Some k"
            using stable_rank_bounded ‹infinite (succeed i)› ‹n ≤ m› by blast+
          thus ?thesis
            by simp
      next
        case False
          ― ‹Then token is already in a sink›
          have "sink (token_run x m)"
          proof (rule ccontr)
            assume "¬sink (token_run x m)"
            moreover
            obtain m' where "m < m'" and "sink (token_run x m')"
              by (metis False token_squats_def le_add2 not_le not_less_eq_eq token_stays_in_sink)
            ultimately
            obtain m'' where "m ≤ m''" and  "¬sink (token_run x m'')" and "sink (token_run x (Suc m''))"
              by (metis le_add1 less_imp_Suc_add token_run_P)
            thus False
              by (metis Fail ‹∧m. token_run x m ∉ F› ‹n ≤ m› ‹x ≤ m› le_trans)
          qed
          ― ‹Hence there is no rank›
          thus ?thesis
            by simp
      qed
      ultimately
      have "¬(∃j ≥ i. rank x m = Some j) ∧ token_run x m ∉ F"
        by blast
    }
    ultimately
    have "(∃j ≥ i. rank x m = Some j) ∨ token_run x m ∈ F ⟷ token_succeeds x"
      by (cases "token_succeeds x") (blast, simp)
  }
  moreover
  ― ‹By definition of n all tokens @{term "∧x. x ≥ n"} succeed›
  have "∧m x. m ≥ n ==> ¬x ≤ m ==> token_succeeds x"
    using n_def n₁_def by force
  ultimately
  show ?thesis
    unfolding MOST_nat_le not_le[symmetric] by blast
qed

lemma succeeding_states:
  assumes "smallest_accepting_rank = Some i"
  shows "∀_\<infinity>n. ∀q. ((∃x ∈ configuration q n. token_succeeds x) ⟶ q ∈ S n) ∧ (q ∈ S n ⟶ (∀x ∈ configuration q n. token_succeeds x))"
proof -
  obtain n where n_def: "∧m x. m ≥ n ==> token_succeeds x = (x > m ∨ (∃j ≥ i. rank x m = Some j) ∨ token_run x m ∈ F)"
    using token_smallest_accepting_rank[OF assms] unfolding MOST_nat_le by auto
  {
    fix m q
    assume "m ≥ n" "q ∉ F" "∃x ∈ configuration q m. token_succeeds x"
    moreover
    then obtain x where "token_run x m = q" and "x ≤ m" and "token_succeeds x"
      by auto
    ultimately
    have "∃j ≥ i. rank x m = Some j"
      using n_def by simp
    hence "∃j ≥ i. state_rank q m = Some j"
      using rank_eq_state_rank ‹x ≤ m› ‹token_run x m = q› by metis
  }
  moreover
  {
    fix m q x
    assume "m ≥ n" "x ∈ configuration q m"
    hence "x ≤ m" and "token_run x m = q"
      by simp+
    moreover
    assume "q ∈ S m"
    hence "(∃j ≥ i. state_rank q m = Some j) ∨ q ∈ F"
      using assms by fastforce
    ultimately
    have "(∃j ≥ i. rank x m = Some j) ∨ q ∈ F"
      using rank_eq_state_rank by presburger
    hence "token_succeeds x"
      unfolding n_def[OF ‹m ≥ n›] ‹token_run x m = q› by presburger
  }
  ultimately
  show ?thesis
    unfolding MOST_nat_le S.simps assms option.sel by blast
qed

end

end