Theory Ranking

section ‹Rankings›

theory Ranking
imports
  "Alternate"
  "Graph"
begin

  subsection ‹Rankings›

  type_synonym 'state ranking = "'state node ⇒ nat"

  definition ranking :: "('label, 'state) nba ⇒ 'label stream ⇒ 'state ranking ⇒ bool" where
    "ranking A w f ≡
      (∀ v ∈ gunodes A w. f v ≤ 2 * card (nodes A)) ∧
      (∀ v ∈ gunodes A w. ∀ u ∈ gusuccessors A w v. f u ≤ f v) ∧
      (∀ v ∈ gunodes A w. gaccepting A v ⟶ even (f v)) ∧
      (∀ v ∈ gunodes A w. ∀ r k. gurun A w r v ⟶ smap f (gtrace r v) = sconst k ⟶ odd k)"

  subsection ‹Ranking Implies Word not in Language›

  lemma ranking_stuck:
    assumes "ranking A w f"
    assumes "v ∈ gunodes A w" "gurun A w r v"
    obtains n k
    where "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k"
  proof -
    have 0: "f u ≤ f v" if "v ∈ gunodes A w" "u ∈ gusuccessors A w v" for v u
      using assms(1) that unfolding ranking_def by auto
    have 1: "shd (v ## gtrace r v) ∈ gunodes A w" using assms(2) by auto
    have 2: "sdescending (smap f (v ## gtrace r v))"
    using 1 assms(3)
    proof (coinduction arbitrary: r v rule: sdescending.coinduct)
      case sdescending
      obtain u s where 1: "r = u ## s" using stream.exhaust by blast
      have 2: "v ∈ gunodes A w" using sdescending(1) by simp
      have 3: "gurun A w (u ## s) v" using sdescending(2) 1 by auto
      have 4: "u ∈ gusuccessors A w v" using 3 by auto
      have 5: "u ∈ gureachable A w v" using graph.reachable_successors 4 by blast
      show ?case
      unfolding 1
      proof (intro exI conjI disjI1)
        show "f u ≤ f v" using 0 2 4 by this
        show "shd (u ## gtrace s u) ∈ gunodes A w" using 2 5 by auto
        show "gurun A w s u" using 3 by auto
      qed auto
    qed
    obtain s k where 3: "smap f (v ## gtrace r v) = s @- sconst k"
      using sdescending_stuck[OF 2] by metis
    have "gtrace (sdrop (Suc (length s)) r) (gtarget (stake (Suc (length s)) r) v) = sdrop (Suc (length s)) (gtrace r v)"
      using sscan_sdrop by rule
    also have "smap f … = sdrop (length s) (smap f (v ## gtrace r v))"
      by (metis "3" id_apply sdrop_simps(2) sdrop_smap sdrop_stl shift_eq siterate.simps(2) stream.sel(2))
    also have "… = sconst k" unfolding 3 using shift_eq by metis
    finally show ?thesis using that by blast
  qed

  lemma ranking_stuck_odd:
    assumes "ranking A w f"
    assumes "v ∈ gunodes A w" "gurun A w r v"
    obtains n
    where "Ball (sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v)))) odd"
  proof -
    obtain n k where 1: "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k"
      using ranking_stuck assms by this
    have 2: "gtarget (stake n r) v ∈ gunodes A w"
      using assms(2, 3) by (simp add: graph.nodes_target graph.run_stake)
    have 3: "gurun A w (sdrop n r) (gtarget (stake n r) v)"
      using assms(2, 3) by (simp add: graph.run_sdrop)
    have 4: "odd k" using 1 2 3 assms(1) unfolding ranking_def by meson
    have 5: "Ball (sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v)))) odd"
      unfolding 1 using 4 by simp
    show ?thesis using that 5 by this
  qed

  lemma ranking_language:
    assumes "ranking A w f"
    shows "w ∉ language A"
  proof
    assume 1: "w ∈ language A"
    obtain r p where 2: "run A (w ||| r) p" "p ∈ initial A" "infs (accepting A) (p ## r)" using 1 by rule
    let ?r = "fromN 1 ||| r"
    let ?v = "(0, p)"
    have 3: "?v ∈ gunodes A w" "gurun A w ?r ?v" using 2(1, 2) by (auto intro: run_grun)

    obtain n where 4: "Ball (sset (smap f (gtrace (sdrop n ?r) (gtarget (stake n ?r) ?v)))) odd"
      using ranking_stuck_odd assms 3 by this
    let ?s = "stake n ?r"
    let ?t = "sdrop n ?r"
    let ?u = "gtarget ?s ?v"

    have "sset (gtrace ?t ?u) ⊆ gureachable A w ?v"
    proof (intro graph.reachable_trace graph.reachable_target graph.reachable.reflexive)
      show "gupath A w ?s ?v" using graph.run_stake 3(2) by this
      show "gurun A w ?t ?u" using graph.run_sdrop 3(2) by this
    qed
    also have "… ⊆ gunodes A w" using 3(1) by blast
    finally have 7: "sset (gtrace ?t ?u) ⊆ gunodes A w" by this
    have 8: "⋀ p. p ∈ gunodes A w ⟹ gaccepting A p ⟹ even (f p)"
      using assms unfolding ranking_def by auto
    have 9: "⋀ p. p ∈ sset (gtrace ?t ?u) ⟹ gaccepting A p ⟹ even (f p)" using 7 8 by auto

    have 19: "infs (accepting A) (smap snd ?r)" using 2(3) by simp
    have 18: "infs (gaccepting A) ?r" using 19 by simp
    have 17: "infs (gaccepting A) (gtrace ?r ?v)" using 18 unfolding gtrace_alt_def by this
    have 16: "infs (gaccepting A) (gtrace (?s @- ?t) ?v)" using 17 unfolding stake_sdrop by this
    have 15: "infs (gaccepting A) (gtrace ?t ?u)" using 16 by simp
    have 13: "infs (even ∘ f) (gtrace ?t ?u)" using infs_mono[OF _ 15] 9 by simp
    have 12: "infs even (smap f (gtrace ?t ?u))" using 13 by (simp add: comp_def)
    have 11: "Bex (sset (smap f (gtrace ?t ?u))) even" using 12 infs_any by metis

    show False using 4 11 by auto
  qed

  subsection ‹Word not in Language Implies Ranking›

  subsubsection ‹Removal of Endangered Nodes›

  definition clean :: "('label, 'state) nba ⇒ 'label stream ⇒ 'state node set ⇒ 'state node set" where
    "clean A w V ≡ {v ∈ V. infinite (greachable A w V v)}"

  lemma clean_decreasing: "clean A w V ⊆ V" unfolding clean_def by auto
  lemma clean_successors:
    assumes "v ∈ V" "u ∈ gusuccessors A w v"
    shows "u ∈ clean A w V ⟹ v ∈ clean A w V"
  proof -
    assume 1: "u ∈ clean A w V"
    have 2: "u ∈ V" "infinite (greachable A w V u)" using 1 unfolding clean_def by auto
    have 3: "u ∈ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast
    have 4: "greachable A w V u ⊆ greachable A w V v" using 3 by blast
    have 5: "infinite (greachable A w V v)" using 2(2) 4 by (simp add: infinite_super)
    show "v ∈ clean A w V" unfolding clean_def using assms(1) 5 by simp
  qed

  subsubsection ‹Removal of Safe Nodes›

  definition prune :: "('label, 'state) nba ⇒ 'label stream ⇒ 'state node set ⇒ 'state node set" where
    "prune A w V ≡ {v ∈ V. ∃ u ∈ greachable A w V v. gaccepting A u}"

  lemma prune_decreasing: "prune A w V ⊆ V" unfolding prune_def by auto
  lemma prune_successors:
    assumes "v ∈ V" "u ∈ gusuccessors A w v"
    shows "u ∈ prune A w V ⟹ v ∈ prune A w V"
  proof -
    assume 1: "u ∈ prune A w V"
    have 2: "u ∈ V" "∃ x ∈ greachable A w V u. gaccepting A x" using 1 unfolding prune_def by auto
    have 3: "u ∈ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast
    have 4: "greachable A w V u ⊆ greachable A w V v" using 3 by blast
    show "v ∈ prune A w V" unfolding prune_def using assms(1) 2(2) 4 by auto
  qed

  subsubsection ‹Run Graph Interation›

  definition graph :: "('label, 'state) nba ⇒ 'label stream ⇒ nat ⇒ 'state node set" where
    "graph A w k ≡ alternate (clean A w) (prune A w) k (gunodes A w)"

  abbreviation "level A w k l ≡ {v ∈ graph A w k. fst v = l}"

  lemma graph_0[simp]: "graph A w 0 = gunodes A w" unfolding graph_def by simp
  lemma graph_Suc[simp]: "graph A w (Suc k) = (if even k then clean A w else prune A w) (graph A w k)"
    unfolding graph_def by simp

  lemma graph_antimono: "antimono (graph A w)"
    using alternate_antimono clean_decreasing prune_decreasing
    unfolding monotone_def le_fun_def graph_def
    by metis
  lemma graph_nodes: "graph A w k ⊆ gunodes A w" using graph_0 graph_antimono le0 antimonoD by metis
  lemma graph_successors:
    assumes "v ∈ gunodes A w" "u ∈ gusuccessors A w v"
    shows "u ∈ graph A w k ⟹ v ∈ graph A w k"
  using assms
  proof (induct k arbitrary: u v)
    case 0
    show ?case using 0(2) by simp
  next
    case (Suc k)
    have 1: "v ∈ graph A w k" using Suc using antimono_iff_le_Suc graph_antimono rev_subsetD by blast
    show ?case using Suc(2) clean_successors[OF 1 Suc(4)] prune_successors[OF 1 Suc(4)] by auto
  qed

  lemma graph_level_finite:
    assumes "finite (nodes A)"
    shows "finite (level A w k l)"
  proof -
    have "level A w k l ⊆ {v ∈ gunodes A w. fst v = l}" by (simp add: graph_nodes subset_CollectI)
    also have "{v ∈ gunodes A w. fst v = l} ⊆ {l} × nodes A" using gnodes_nodes by force
    also have "finite ({l} × nodes A)" using assms(1) by simp
    finally show ?thesis by this
  qed

  lemma find_safe:
    assumes "w ∉ language A"
    assumes "V ≠ {}" "V ⊆ gunodes A w"
    assumes "⋀ v. v ∈ V ⟹ gsuccessors A w V v ≠ {}"
    obtains v
    where "v ∈ V" "∀ u ∈ greachable A w V v. ¬ gaccepting A u"
  proof (rule ccontr)
    assume 1: "¬ thesis"
    have 2: "⋀ v. v ∈ V ⟹ ∃ u ∈ greachable A w V v. gaccepting A u" using that 1 by auto
    have 3: "⋀ r v. v ∈ initial A ⟹ run A (w ||| r) v ⟹ fins (accepting A) r" using assms(1) by auto
    obtain v where 4: "v ∈ V" using assms(2) by force
    obtain x where 5: "x ∈ greachable A w V v" "gaccepting A x" using 2 4 by blast
    obtain y where 50: "gpath A w V y v" "x = gtarget y v" using 5(1) by rule
    obtain r where 6: "grun A w V r x" "infs (λ x. x ∈ V ∧ gaccepting A x) r"
    proof (rule graph.recurring_condition)
      show "x ∈ V ∧ gaccepting A x" using greachable_subset 4 5 by blast
    next
      fix v
      assume 1: "v ∈ V ∧ gaccepting A v"
      obtain v' where 20: "v' ∈ gsuccessors A w V v" using assms(4) 1 by (meson IntE equals0I)
      have 21: "v' ∈ V" using 20 by auto
      have 22: "∃ u ∈ greachable A w V v'. u ∈ V ∧ gaccepting A u"
        using greachable_subset 2 21 by blast
      obtain r where 30: "gpath A w V r v'" "gtarget r v' ∈ V ∧ gaccepting A (gtarget r v')"
        using 22 by blast
      show "∃ r. r ≠ [] ∧ gpath A w V r v ∧ gtarget r v ∈ V ∧ gaccepting A (gtarget r v)"
      proof (intro exI conjI)
        show "v' # r ≠ []" by simp
        show "gpath A w V (v' # r) v" using 20 30 by auto
        show "gtarget (v' # r) v ∈ V" using 30 by simp
        show "gaccepting A (gtarget (v' # r) v)" using 30 by simp
      qed
    qed auto
    obtain u where 100: "u ∈ ginitial A" "v ∈ gureachable A w u" using 4 assms(3) by blast
    have 101: "gupath A w y v" using gpath_subset 50(1) subset_UNIV by this
    have 102: "gurun A w r x" using grun_subset 6(1) subset_UNIV by this
    obtain t where 103: "gupath A w t u" "v = gtarget t u" using 100(2) by rule
    have 104: "gurun A w (t @- y @- r) u" using 101 102 103 50(2) by auto
    obtain s q where 7: "t @- y @- r = fromN (Suc 0) ||| s" "u = (0, q)"
      using grun_elim[OF 104] 100(1) by blast
    have 8: "run A (w ||| s) q" using grun_run[OF 104[unfolded 7]] by simp
    have 9: "q ∈ initial A" using 100(1) 7(2) by auto
    have 91: "sset (trace (w ||| s) q) ⊆ reachable A q"
      using nba.reachable_trace nba.reachable.reflexive 8 by this
    have 10: "fins (accepting A) s" using 3 9 8 by this
    have 12: "infs (gaccepting A) r" using infs_mono[OF _ 6(2)] by simp
    have "s = smap snd (t @- y @- r)" unfolding 7(1) by simp
    also have "infs (accepting A) …" using 12 by (simp add: comp_def)
    finally have 13: "infs (accepting A) s" by this
    show False using 10 13 by simp
  qed

  lemma remove_run:
    assumes "finite (nodes A)" "w ∉ language A"
    assumes "V ⊆ gunodes A w" "clean A w V ≠ {}"
    obtains v r
    where
      "grun A w V r v"
      "sset (gtrace r v) ⊆ clean A w V"
      "sset (gtrace r v) ⊆ - prune A w (clean A w V)"
  proof -
    obtain u where 1: "u ∈ clean A w V" "∀ x ∈ greachable A w (clean A w V) u. ¬ gaccepting A x"
    proof (rule find_safe)
      show "w ∉ language A" using assms(2) by this
      show "clean A w V ≠ {}" using assms(4) by this
      show "clean A w V ⊆ gunodes A w" using assms(3) by (meson clean_decreasing subset_iff)
    next
      fix v
      assume 1: "v ∈ clean A w V"
      have 2: "v ∈ V" using 1 clean_decreasing by blast
      have 3: "infinite (greachable A w V v)" using 1 clean_def by auto
      have "gsuccessors A w V v ⊆ gusuccessors A w v" by auto
      also have "finite …" using 2 assms(1, 3) finite_nodes_gsuccessors by blast
      finally have 4: "finite (gsuccessors A w V v)" by this
      have 5: "infinite (insert v (⋃((greachable A w V) ` (gsuccessors A w V v))))"
        using graph.reachable_step 3 by metis
      obtain u where 6: "u ∈ gsuccessors A w V v" "infinite (greachable A w V u)" using 4 5 by auto
      have 7: "u ∈ clean A w V" using 6 unfolding clean_def by auto
      show "gsuccessors A w (clean A w V) v ≠ {}" using 6(1) 7 by auto
    qed auto
    have 2: "u ∈ V" using 1(1) unfolding clean_def by auto
    have 3: "infinite (greachable A w V u)" using 1(1) unfolding clean_def by simp
    have 4: "finite (gsuccessors A w V v)" if "v ∈ greachable A w V u" for v
    proof -
      have 1: "v ∈ V" using that greachable_subset 2 by blast
      have "gsuccessors A w V v ⊆ gusuccessors A w v" by auto
      also have "finite …" using 1 assms(1, 3) finite_nodes_gsuccessors by blast
      finally show ?thesis by this
    qed
    obtain r where 5: "grun A w V r u" using graph.koenig[OF 3 4] by this
    have 6: "greachable A w V u ⊆ V" using 2 greachable_subset by blast
    have 7: "sset (gtrace r u) ⊆ V"
      using graph.reachable_trace[OF graph.reachable.reflexive 5(1)] 6 by blast
    have 8: "sset (gtrace r u) ⊆ clean A w V"
      unfolding clean_def using 7 infinite_greachable_gtrace[OF 5(1)] by auto
    have 9: "sset (gtrace r u) ⊆ greachable A w (clean A w V) u"
      using 5 8 by (metis graph.reachable.reflexive graph.reachable_trace grun_subset)
    show ?thesis
    proof
      show "grun A w V r u" using 5(1) by this
      show "sset (gtrace r u) ⊆ clean A w V" using 8 by this
      show "sset (gtrace r u) ⊆ - prune A w (clean A w V)"
      proof (intro subsetI ComplI)
        fix p
        assume 10: "p ∈ sset (gtrace r u)" "p ∈ prune A w (clean A w V)"
        have 20: "∃ x ∈ greachable A w (clean A w V) p. gaccepting A x"
          using 10(2) unfolding prune_def by auto
        have 30: "greachable A w (clean A w V) p ⊆ greachable A w (clean A w V) u"
          using 10(1) 9 by blast
        show "False" using 1(2) 20 30 by force
      qed
    qed
  qed

  lemma level_bounded:
    assumes "finite (nodes A)" "w ∉ language A"
    obtains n
    where "⋀ l. l ≥ n ⟹ card (level A w (2 * k) l) ≤ card (nodes A) - k"
  proof (induct k arbitrary: thesis)
    case (0)
    show ?case
    proof (rule 0)
      fix l :: nat
      have "finite ({l} × nodes A)" using assms(1) by simp
      also have "level A w 0 l ⊆ {l} × nodes A" using gnodes_nodes by force
      also (card_mono) have "card … = card (nodes A)" using assms(1) by simp
      finally show "card (level A w (2 * 0) l) ≤ card (nodes A) - 0" by simp
    qed
  next
    case (Suc k)
    show ?case
    proof (cases "graph A w (Suc (2 * k)) = {}")
      case True
      have 3: "graph A w (2 * Suc k) = {}" using True prune_decreasing by simp blast
      show ?thesis using Suc(2) 3 by simp
    next
      case False
      obtain v r where 1:
        "grun A w (graph A w (2 * k)) r v"
        "sset (gtrace r v) ⊆ graph A w (Suc (2 * k))"
        "sset (gtrace r v) ⊆ - graph A w (Suc (Suc (2 * k)))"
      proof (rule remove_run)
        show "finite (nodes A)" "w ∉ language A" using assms by this
        show "clean A w (graph A w (2 * k)) ≠ {}" using False by simp
        show "graph A w (2 * k) ⊆ gunodes A w" using graph_nodes by this
      qed auto
      obtain l q where 2: "v = (l, q)" by force
      obtain n where 90: "⋀ l. n ≤ l ⟹ card (level A w (2 * k) l) ≤ card (nodes A) - k"
        using Suc(1) by blast
      show ?thesis
      proof (rule Suc(2))
        fix j
        assume 100: "n + Suc l ≤ j"
        have 6: "graph A w (Suc (Suc (2 * k))) ⊆ graph A w (Suc (2 * k))"
          using graph_antimono antimono_iff_le_Suc by blast
        have 101: "gtrace r v !! (j - Suc l) ∈ graph A w (Suc (2 * k))" using 1(2) snth_sset by auto
        have 102: "gtrace r v !! (j - Suc l) ∉ graph A w (Suc (Suc (2 * k)))" using 1(3) snth_sset by blast
        have 103: "gtrace r v !! (j - Suc l) ∈ level A w (Suc (2 * k)) j"
          using 1(1) 100 101 2 by (auto elim: grun_elim)
        have 104: "gtrace r v !! (j - Suc l) ∉ level A w (Suc (Suc (2 * k))) j" using 100 102 by simp
        have "level A w (2 * Suc k) j = level A w (Suc (Suc (2 * k))) j" by simp
        also have "… ⊂ level A w (Suc (2 * k)) j" using 103 104 6 by blast
        also have "… ⊆ level A w (2 * k) j" by (simp add: Collect_mono clean_def)
        finally have 105: "level A w (2 * Suc k) j ⊂ level A w (2 * k) j" by this
        have "card (level A w (2 * Suc k) j) < card (level A w (2 * k) j)"
          using assms(1) 105 by (simp add: graph_level_finite psubset_card_mono)
        also have "… ≤ card (nodes A) - k" using 90 100 by simp
        finally show "card (level A w (2 * Suc k) j) ≤ card (nodes A) - Suc k" by simp
      qed
    qed
  qed
  lemma graph_empty:
    assumes "finite (nodes A)" "w ∉ language A"
    shows "graph A w (Suc (2 * card (nodes A))) = {}"
  proof -
    obtain n where 1: "⋀ l. l ≥ n ⟹ card (level A w (2 * card (nodes A)) l) = 0"
      using level_bounded[OF assms(1, 2), of "card (nodes A)"] by auto
    have "graph A w (2 * card (nodes A)) =
      (⋃ l ∈ {..< n}. level A w (2 * card (nodes A)) l) ∪
      (⋃ l ∈ {n ..}. level A w (2 * card (nodes A)) l)"
      by auto
    also have "(⋃ l ∈ {n ..}. level A w (2 * card (nodes A)) l) = {}"
      using graph_level_finite assms(1) 1 by fastforce
    also have "finite ((⋃ l ∈ {..< n}. level A w (2 * card (nodes A)) l) ∪ {})"
      using graph_level_finite assms(1) by auto
    finally have 100: "finite (graph A w (2 * card (nodes A)))" by this
    have 101: "finite (greachable A w (graph A w (2 * card (nodes A))) v)" for v
      using 100 greachable_subset[of A w "graph A w (2 * card (nodes A))" v]
      using finite_insert infinite_super by auto
    show ?thesis using 101 by (simp add: clean_def)
  qed
  lemma graph_le:
    assumes "finite (nodes A)" "w ∉ language A"
    assumes "v ∈ graph A w k"
    shows "k ≤ 2 * card (nodes A)"
    using graph_empty graph_antimono assms
    by (metis Suc_leI empty_iff monotone_def not_le_imp_less rev_subsetD)

  subsection ‹Node Ranks›

  definition rank :: "('label, 'state) nba ⇒ 'label stream ⇒ 'state node ⇒ nat" where
    "rank A w v ≡ GREATEST k. v ∈ graph A w k"

  lemma rank_member:
    assumes "finite (nodes A)" "w ∉ language A" "v ∈ gunodes A w"
    shows "v ∈ graph A w (rank A w v)"
  unfolding rank_def
  proof (rule GreatestI_nat)
    show "v ∈ graph A w 0" using assms(3) by simp
    show "k ≤ 2 * card (nodes A)" if "v ∈ graph A w k" for k
      using graph_le assms(1, 2) that by blast
  qed
  lemma rank_removed:
    assumes "finite (nodes A)" "w ∉ language A"
    shows "v ∉ graph A w (Suc (rank A w v))"
  proof
    assume "v ∈ graph A w (Suc (rank A w v))"
    then have 2: "Suc (rank A w v) ≤ rank A w v"
      unfolding rank_def using Greatest_le_nat graph_le assms by metis
    then show "False" by auto
  qed
  lemma rank_le:
    assumes "finite (nodes A)" "w ∉ language A"
    assumes "v ∈ gunodes A w" "u ∈ gusuccessors A w v"
    shows "rank A w u ≤ rank A w v"
  unfolding rank_def
  proof (rule Greatest_le_nat)
    have 1: "u ∈ gureachable A w v" using graph.reachable_successors assms(4) by blast
    have 2: "u ∈ gunodes A w" using assms(3) 1 by auto
    show "v ∈ graph A w (GREATEST k. u ∈ graph A w k)"
    unfolding rank_def[symmetric]
    proof (rule graph_successors)
      show "v ∈ gunodes A w" using assms(3) by this
      show "u ∈ gusuccessors A w v" using assms(4) by this
      show "u ∈ graph A w (rank A w u)" using rank_member assms(1, 2) 2 by this
    qed
    show "k ≤ 2 * card (nodes A)" if "v ∈ graph A w k" for k
      using graph_le assms(1, 2) that by blast
  qed

  lemma language_ranking:
    assumes "finite (nodes A)" "w ∉ language A"
    shows "ranking A w (rank A w)"
  unfolding ranking_def
  proof (intro conjI ballI allI impI)
    fix v
    assume 1: "v ∈ gunodes A w"
    have 2: "v ∈ graph A w (rank A w v)" using rank_member assms 1 by this
    show "rank A w v ≤ 2 * card (nodes A)" using graph_le assms 2 by this
  next
    fix v u
    assume 1: "v ∈ gunodes A w" "u ∈ gusuccessors A w v"
    show "rank A w u ≤ rank A w v" using rank_le assms 1 by this
  next
    fix v
    assume 1: "v ∈ gunodes A w" "gaccepting A v"
    have 2: "v ∈ graph A w (rank A w v)" using rank_member assms 1(1) by this
    have 3: "v ∉ graph A w (Suc (rank A w v))" using rank_removed assms by this
    have 4: "v ∈ prune A w (graph A w (rank A w v))" using 2 1(2) unfolding prune_def by auto
    have 5: "graph A w (Suc (rank A w v)) ≠ prune A w (graph A w (rank A w v))" using 3 4 by blast
    show "even (rank A w v)" using 5 by auto
  next
    fix v r k
    assume 1: "v ∈ gunodes A w" "gurun A w r v" "smap (rank A w) (gtrace r v) = sconst k"
    have "sset (gtrace r v) ⊆ gureachable A w v"
      using 1(2) by (metis graph.reachable.reflexive graph.reachable_trace)
    then have 6: "sset (gtrace r v) ⊆ gunodes A w" using 1(1) by blast
    have 60: "rank A w ` sset (gtrace r v) ⊆ {k}"
      using 1(3) by (metis equalityD1 sset_sconst stream.set_map)
    have 50: "sset (gtrace r v) ⊆ graph A w k"
      using rank_member[OF assms] subsetD[OF 6] 60 unfolding image_subset_iff by auto
    have 70: "grun A w (graph A w k) r v" using grun_subset 1(2) 50 by this
    have 7: "sset (gtrace r v) ⊆ clean A w (graph A w k)"
      unfolding clean_def using 50 infinite_greachable_gtrace[OF 70] by auto
    have 8: "sset (gtrace r v) ∩ graph A w (Suc k) = {}" using rank_removed[OF assms] 60 by blast
    have 9: "sset (gtrace r v) ≠ {}" using stream.set_sel(1) by auto
    have 10: "graph A w (Suc k) ≠ clean A w (graph A w k)" using 7 8 9 by blast
    show "odd k" using 10 unfolding graph_Suc by auto
  qed

  subsection ‹Correctness Theorem›

  theorem language_ranking_iff:
    assumes "finite (nodes A)"
    shows "w ∉ language A ⟷ (∃ f. ranking A w f)"
    using ranking_language language_ranking assms by blast

end