Theory Decidability

section ‹Decidability of Galois Energy Games›

theory Decidability
  imports Galois_Energy_Game Complete_Non_Orders.Kleene_Fixed_Point
begin

text‹In this theory we give a proof of decidability for Galois energy games (over vectors of naturals). 
We do this by providing a proof of correctness of the simplifyed version of
Bisping's Algorithm to calculate minimal attacker winning budgets. 
We further formalise the key argument for its termination.
(This corresponds to section 3.2 in the preprint~\cite{preprint}.)
›

locale galois_energy_game_decidable = galois_energy_game attacker weight application inverse_application energies order energy_sup
  for attacker ::  "'position set" and 
      weight :: "'position ⇒ 'position ⇒ 'label option" and
      application :: "'label ⇒ 'energy ⇒ 'energy option" and
      inverse_application :: "'label ⇒ 'energy ⇒ 'energy option" and
      energies :: "'energy set" and
      order :: "'energy ⇒ 'energy ⇒ bool" (infix "e≤" 80)and 
      energy_sup :: "'energy set ⇒ 'energy"
+
assumes nonpos_eq_pos: "nonpos_winning_budget = winning_budget" and
        finite_positions: "finite positions"
begin

subsection‹Minimal Attacker Winning Budgets as Pareto Fronts›

text‹We now prepare the proof of decidability by introducing minimal winning budgets.›

abbreviation minimal_winning_budget:: "'energy ⇒ 'position ⇒ bool" where
"minimal_winning_budget e g ≡ e ∈ energy_Min {e. winning_budget_len e g}"
abbreviation "a_win g ≡ {e. winning_budget_len e g}"
abbreviation "a_win_min g ≡ energy_Min (a_win g)"

text‹Since the component-wise order on energies is well-founded, we can conclude that minimal winning budgets are finite.›

lemma minimal_winning_budget_finite:
  shows "⋀g. finite (a_win_min g)"
proof(rule energy_Min_finite)
  fix g 
  show "a_win g ⊆ energies" using nonpos_eq_pos winning_budget_len.cases
    by blast
qed 

text‹We now introduce the set of mappings from positions to possible Pareto fronts, i.e.\ incomparable sets of energies.›

definition possible_pareto:: "('position ⇒ 'energy set) set" where 
  "possible_pareto ≡ {F. ∀g. F g ⊆ {e. e∈energies} 
                          ∧ (∀e e'. (e ∈ F g ∧ e' ∈ F g ∧ e ≠ e') 
                             ⟶ (¬ e e≤ e' ∧ ¬ e' e≤ e))}"

text‹By definition minimal winning budgets are possible Pareto fronts.›

lemma a_win_min_in_pareto:
  shows "a_win_min ∈ possible_pareto" 
  unfolding energy_Min_def possible_pareto_def proof
  show "∀g. {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ⊆ {e. e∈energies} ∧
        (∀e e'.
            e ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧
            e' ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧ e ≠ e' ⟶
            incomparable (e≤) e e') "
  proof
    fix g 
    show "{e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ⊆ {e. e∈energies} ∧
         (∀e e'.
             e ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧
             e' ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧ e ≠ e' ⟶
             incomparable (e≤) e e')"
    proof
      show "{e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ⊆ {e. e∈energies}"
        using winning_budget_len.simps
        by (smt (verit) Collect_mono_iff mem_Collect_eq)
      show " ∀e e'.
       e ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧
       e' ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧ e ≠ e' ⟶
       incomparable (e≤) e e' "
      proof
        fix e
        show "∀e'. e ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧
              e' ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧ e ≠ e' ⟶
              incomparable (e≤) e e'"
        proof
          fix e'
          show "e ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧
          e' ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧ e ≠ e' ⟶
          incomparable (e≤) e e'"
          proof
            assume " e ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧
    e' ∈ {e ∈ a_win g. ∀e'∈a_win g. e ≠ e' ⟶ ¬ e' e≤ e} ∧ e ≠ e'"
            thus "incomparable (e≤) e e'" 
              by auto
          qed
        qed
      qed
    qed
  qed
qed

text‹We define a partial order on possible Pareto fronts.›

definition pareto_order:: "('position ⇒ 'energy set) ⇒ ('position ⇒ 'energy set) ⇒ bool"  (infix "≼" 80) where
  "pareto_order F F' ≡ (∀g e. e ∈ F(g) ⟶ (∃e'. e' ∈ F'(g) ∧  e' e≤ e))"

lemma pareto_partial_order_vanilla:
  shows reflexivity: "⋀F. F ∈ possible_pareto ⟹ F ≼ F" and 
transitivity: "⋀F F' F''. F ∈ possible_pareto ⟹ F' ∈ possible_pareto 
               ⟹ F'' ∈ possible_pareto ⟹  F ≼ F' ⟹ F' ≼ F'' 
               ⟹ F ≼ F'' " and
antisymmetry: "⋀F F'.  F ∈ possible_pareto ⟹ F' ∈ possible_pareto 
               ⟹ F ≼ F' ⟹ F' ≼ F ⟹ F = F'"
proof-
  fix F F' F''
  assume "F ∈ possible_pareto" and "F' ∈ possible_pareto" and "F'' ∈ possible_pareto"
  show "F ≼ F"
    unfolding pareto_order_def energy_order ordering_def
    by (meson energy_order ordering.eq_iff) 
  show "F ≼ F' ⟹ F' ≼ F'' ⟹ F ≼ F'' "
  proof-
    assume "F ≼ F'" and "F' ≼ F''" 
    show " F ≼ F'' "
      unfolding pareto_order_def proof
      show "⋀g. ∀e. e ∈ F g ⟶ (∃e'. e' ∈ F'' g ∧ e' e≤ e)"
      proof
        fix g e
        show "e ∈ F g ⟶ (∃e'. e' ∈ F'' g ∧ e' e≤ e)"
        proof
          assume "e ∈ F g"
          hence "(∃e'. e' ∈ F' g ∧ e' e≤ e)" using ‹F ≼ F'› unfolding pareto_order_def by simp
          from this obtain e' where "e' ∈ F' g ∧ e' e≤ e" by auto
          hence "(∃e''. e'' ∈ F'' g ∧ e'' e≤ e')" using ‹F' ≼ F''› unfolding pareto_order_def by simp
          from this obtain e'' where "e'' ∈ F'' g ∧ e'' e≤ e'" by auto
          hence "e'' ∈ F'' g ∧ e'' e≤ e" using ‹e' ∈ F' g ∧ e' e≤ e› energy_order ordering_def
            by (metis (mono_tags, lifting) partial_preordering.trans) 
          thus "∃e'. e' ∈ F'' g ∧ e' e≤ e" by auto
        qed
      qed
    qed
  qed
  show "F ≼ F' ⟹ F' ≼ F ⟹ F = F'"
  proof-
    assume "F ≼ F'" and "F' ≼ F"
    show "F = F'"
    proof
      fix g 
      show "F g = F' g"
      proof
        show "F g ⊆ F' g"
        proof
          fix e
          assume "e ∈ F g"
          hence "∃e'. e' ∈ F' g ∧ e' e≤ e" using ‹F ≼ F'› unfolding pareto_order_def by auto
          from this obtain e' where "e' ∈ F' g ∧ e' e≤ e" by auto
          hence "∃e''. e'' ∈ F g ∧ e'' e≤ e'" using ‹F' ≼ F› unfolding pareto_order_def by auto
          from this obtain e'' where "e'' ∈ F g ∧ e'' e≤ e'" by auto
          hence "e'' = e ∧ e' = e" using possible_pareto_def ‹F ∈ possible_pareto› energy_order ordering_def
            by (smt (verit, ccfv_SIG) ‹e ∈ F g› ‹e' ∈ F' g ∧ e' e≤ e› mem_Collect_eq ordering.antisym partial_preordering_def)
          thus "e ∈ F' g" using ‹e' ∈ F' g ∧ e' e≤ e› by auto
        qed
        show "F' g ⊆ F g" 
        proof
          fix e
          assume "e ∈ F' g"
          hence "∃e'. e' ∈ F g ∧ e' e≤ e" using ‹F' ≼ F› unfolding pareto_order_def by auto
          from this obtain e' where "e' ∈ F g ∧ e' e≤ e" by auto
          hence "∃e''. e'' ∈ F' g ∧ e'' e≤ e'" using ‹F ≼ F'› unfolding pareto_order_def by auto
          from this obtain e'' where "e'' ∈ F' g ∧ e'' e≤ e'" by auto
          hence "e'' = e ∧ e' = e" using possible_pareto_def ‹F' ∈ possible_pareto› energy_order ordering_def
            by (smt (verit, best) ‹F g ⊆ F' g› ‹e ∈ F' g› ‹e' ∈ F g ∧ e' e≤ e› in_mono mem_Collect_eq)
          thus "e ∈ F g" using ‹e' ∈ F g ∧ e' e≤ e› by auto
        qed
      qed
    qed
  qed
qed

lemma pareto_partial_order:
  shows "reflp_on possible_pareto (≼)" and 
        "transp_on possible_pareto (≼)" and 
        "antisymp_on possible_pareto (≼)"
proof-
  show "reflp_on possible_pareto (≼)"
    using reflexivity
    by (simp add: reflp_onI)
  show "transp_on possible_pareto (≼)"
    using transitivity
    using transp_onI by blast
  show "antisymp_on possible_pareto (≼)"
    using antisymmetry
    using antisymp_onI by auto
qed

text‹By defining a supremum, we show that the order is directed-complete bounded join-semilattice.›

definition pareto_sup:: "('position ⇒ 'energy set) set ⇒ ('position ⇒ 'energy set)" where 
  "pareto_sup P g = energy_Min {e. ∃F. F∈ P ∧ e ∈ F g}"

lemma pareto_sup_is_sup:
  assumes "P ⊆ possible_pareto"
  shows "pareto_sup P ∈ possible_pareto" and 
        "⋀F. F ∈ P ⟹ F ≼ pareto_sup P" and 
        "⋀Fs. Fs ∈ possible_pareto ⟹ (⋀F. F ∈ P ⟹ F ≼ Fs) 
         ⟹ pareto_sup P ≼ Fs"
proof-
  show "pareto_sup P ∈ possible_pareto" unfolding pareto_sup_def possible_pareto_def energy_Min_def
    by (smt (verit, ccfv_threshold) Ball_Collect assms mem_Collect_eq possible_pareto_def) 
  show "⋀F. F ∈ P ⟹ F ≼ pareto_sup P"
  proof-
    fix F
    assume "F ∈ P"
    show "F ≼ pareto_sup P"
      unfolding pareto_order_def proof
      show "⋀g. ∀e. e ∈ F g ⟶ (∃e'. e' ∈ pareto_sup P g ∧ e' e≤ e)"
      proof
        fix g e
        show "e ∈ F g ⟶ (∃e'. e' ∈ pareto_sup P g ∧ e' e≤ e)"
        proof
          have in_energy: "{e. ∃F. F ∈ P ∧ e ∈ F g} ⊆ energies"
            using assms possible_pareto_def by force 
          assume "e ∈ F g"
          hence "e∈{(e::'energy). (∃F. F∈ P ∧  e∈ (F g))}" using ‹F ∈ P› by auto
          hence "∃e'. e' ∈ energy_Min {(e::'energy). (∃F. F∈ P ∧  e∈ (F g))} ∧ e' e≤ e" 
            using energy_Min_contains_smaller in_energy
            by meson
          thus "∃e'. e' ∈ pareto_sup P g ∧ e' e≤ e" unfolding pareto_sup_def by simp
        qed
      qed
    qed
  qed
  show "⋀Fs. Fs ∈ possible_pareto ⟹ (⋀F. F ∈ P ⟹ F ≼ Fs) ⟹ pareto_sup P ≼ Fs"
  proof-
    fix Fs
    assume "Fs ∈ possible_pareto" and "(⋀F. F ∈ P ⟹ F ≼ Fs)"
    show "pareto_sup P ≼ Fs"
      unfolding pareto_order_def proof
      show "⋀g. ∀e. e ∈ pareto_sup P g ⟶ (∃e'. e' ∈ Fs g ∧ e' e≤ e) "
      proof
        fix g e 
        show "e ∈ pareto_sup P g ⟶ (∃e'. e' ∈ Fs g ∧ e' e≤ e)"
        proof
          assume "e ∈ pareto_sup P g"
          hence "e∈ {e. ∃F. F ∈ P ∧ e ∈ F g}" unfolding pareto_sup_def using energy_Min_def by simp
          from this obtain F where "F ∈ P ∧ e ∈ F g" by auto
          thus "∃e'. e' ∈ Fs g ∧ e' e≤ e" using ‹(⋀F. F ∈ P ⟹ F ≼ Fs)› pareto_order_def by auto 
        qed
      qed
    qed
  qed
qed

lemma pareto_directed_complete:
  shows "directed_complete possible_pareto (≼)"
  unfolding directed_complete_def 
proof-
  show "(λX r. directed X r ∧ X ≠ {})-complete possible_pareto (≼)"
    unfolding complete_def 
  proof
    fix P
    show "P ⊆ possible_pareto ⟶
         directed P (≼) ∧ P ≠ {} ⟶ (∃s. extreme_bound possible_pareto (≼) P s)"
    proof
      assume "P ⊆ possible_pareto"
      show "directed P (≼) ∧ P ≠ {} ⟶ (∃s. extreme_bound possible_pareto (≼) P s)"
      proof
        assume "directed P (≼) ∧ P ≠ {}"
        show "∃s. extreme_bound possible_pareto (≼) P s"
        proof
          show "extreme_bound possible_pareto (≼) P (pareto_sup P)"
            unfolding extreme_bound_def 
          proof
            show "pareto_sup P ∈ {b ∈ possible_pareto. bound P (≼) b}" 
              using pareto_sup_is_sup ‹P ⊆ possible_pareto› ‹directed P (≼) ∧ P ≠ {}›
              by blast
            show "⋀x. x ∈ {b ∈ possible_pareto. bound P (≼) b} ⟹ pareto_sup P ≼ x"
            proof-
              fix x 
              assume "x ∈ {b ∈ possible_pareto. bound P (≼) b}"
              thus "pareto_sup P ≼ x"
                using pareto_sup_is_sup ‹P ⊆ possible_pareto› ‹directed P (≼) ∧ P ≠ {}›
                by auto
            qed
          qed
        qed
      qed
    qed
  qed              
qed

lemma pareto_minimal_element:
  shows "(λg. {}) ≼ F"
  unfolding pareto_order_def by simp

subsection‹Proof of Decidability›

text‹Using Kleene's fixed point theorem we now show, that the minimal attacker winning budgets are the least fixed point of the algorithm.
For this we first formalise one iteration of the algorithm.  
›

definition iteration:: "('position ⇒ 'energy set) ⇒ ('position ⇒ 'energy set)" where 
  "iteration F g ≡ (if g ∈ attacker 
                    then energy_Min {inv_upd (the (weight g g')) e' | e' g'. 
                        e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ F g'}
                    else energy_Min {energy_sup
                         {inv_upd (the (weight g g')) (e_index g') | g'. 
                         weight g g' ≠ None} | e_index. ∀g'. weight g g' ≠ None
                         ⟶(e_index g')∈energies ∧ e_index g' ∈ F g'})"

text‹We now show that ‹iteration› is a Scott-continuous functor of possible Pareto fronts.›

lemma iteration_pareto_functor:
  assumes "F ∈ possible_pareto"
  shows "iteration F ∈ possible_pareto"
  unfolding possible_pareto_def
proof
  show "∀g. iteration F g ⊆ {e. e∈energies} ∧
        (∀e e'. e ∈ iteration F g ∧ e' ∈ iteration F g ∧ e ≠ e' ⟶ incomparable (e≤) e e')"
  proof
    fix g
    show "iteration F g ⊆ {e. e∈energies} ∧
        (∀e e'. e ∈ iteration F g ∧ e' ∈ iteration F g ∧ e ≠ e' ⟶ incomparable (e≤) e e')"
    proof
      show "iteration F g ⊆ {e. e∈energies}"
      proof
        fix e 
        assume "e ∈ iteration F g"
        show "e ∈ {e. e∈energies}"
        proof
          show "e∈energies"
          proof(cases "g ∈ attacker")
            case True
            hence "e ∈ energy_Min {inv_upd (the (weight g g')) e' | e' g'. e'∈energies ∧ weight g g' ≠ None ∧ e' ∈ F g'}"
              using ‹e ∈ iteration F g› iteration_def by auto 
            then show ?thesis using assms energy_Min_def
              using inv_well_defined by force 
          next
            case False
            hence "e ∈ energy_Min {energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}| e_index. (∀g'. weight g g' ≠ None ⟶ ((e_index g')∈energies ∧ e_index g' ∈ F g'))}"
              using ‹e ∈ iteration F g› iteration_def by auto
            hence "e ∈ {energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}| e_index. (∀g'. weight g g' ≠ None ⟶ ((e_index g')∈energies ∧ e_index g' ∈ F g'))}"
              using energy_Min_def
              by simp 
            from this obtain e_index where E: "e = energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}" and  A:"(∀g'. weight g g' ≠ None ⟶ ((e_index g')∈energies ∧ e_index g' ∈ F g'))"
              by blast
            have fin: "finite {inv_upd (the (weight g g')) (e_index g')| g'. g' ∈ positions}" using finite_positions
            proof -
              have "finite {p. p ∈ positions}"
                using finite_positions by auto
              then show ?thesis
                using finite_image_set by fastforce
            qed
            have "{inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (e_index g')| g'. g' ∈ positions}"
              by blast
            hence fin: "finite {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}" using fin
              by (meson finite_subset)
            have "{inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None} ⊆ energies"
            proof
              fix x 
              assume "x ∈ {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}"
              from this obtain g' where "x=inv_upd (the (weight g g')) (e_index g')" and "weight g g' ≠ None" by auto
              hence "(e_index g')∈energies ∧ e_index g' ∈ F g'" using A
                by blast 
              thus "x ∈ energies" using inv_well_defined
                using ‹weight g g' ≠ None› ‹x = inv_upd (the (weight g g')) (e_index g')› by blast
            qed
            then show ?thesis using bounded_join_semilattice fin E
              by meson
          qed  
        qed
      qed
      show "(∀e e'. e ∈ iteration F g ∧ e' ∈ iteration F g ∧ e ≠ e' ⟶ incomparable (e≤) e e')"
        using possible_pareto_def iteration_def energy_Min_def
        by (smt (verit) mem_Collect_eq)
    qed
  qed
qed

lemma iteration_monotonic:
  assumes "F ∈ possible_pareto" and "F' ∈ possible_pareto" and "F ≼ F'"
  shows "iteration F ≼ iteration F'"
  unfolding pareto_order_def 
proof
  fix g 
  show "∀e. e ∈ iteration F g ⟶ (∃e'. e' ∈ iteration F' g ∧ e' e≤ e)"
  proof
    fix e
    show "e ∈ iteration F g ⟶ (∃e'. e' ∈ iteration F' g ∧ e' e≤ e)"
    proof
      assume "e ∈ iteration F g"
      show "(∃e'. e' ∈ iteration F' g ∧ e' e≤ e)"
      proof(cases"g∈ attacker")
        case True
        hence "e ∈ energy_Min {inv_upd (the (weight g g')) e' | e' g'. e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ F g'}"
          using iteration_def ‹e ∈ iteration F g› by simp
        from this obtain e' g' where E: "e = inv_upd (the (weight g g')) e' ∧ e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ F g'" 
          using energy_Min_def by auto 
        hence "∃e''. e'' ∈ F' g' ∧ e'' e≤ e'" using pareto_order_def assms by simp
        from this obtain e'' where "e'' ∈ F' g' ∧ e'' e≤ e'" by auto

        have "F' g' ⊆ {e. e ∈ energies}" using assms(2) unfolding possible_pareto_def
          by simp
        hence E'': "e'' ∈ energies" using ‹e'' ∈ F' g' ∧ e'' e≤ e'›
          by auto

        have uE: "inv_upd (the (weight g g')) e'' e≤  inv_upd (the (weight g g')) e'" 
        proof(rule inverse_monotonic)
          show " weight g g' ≠ None"
            by (simp add: E)
          show "e'' e≤ e'" using ‹e'' ∈ F' g' ∧ e'' e≤ e'› by simp
          show "e'' ∈ energies" using E''.
          thus "inverse_application (the (weight g g')) e'' ≠ None"
            using ‹weight g g' ≠ None› inv_well_defined
            by auto
        qed 
        hence "inv_upd (the (weight g g')) e'' ∈ {inv_upd (the (weight g g')) e' | e' g'. e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ F' g'}"
          using E'' ‹e'' ∈ F' g' ∧ e'' e≤ e'› E
          by auto
        hence "∃e'''. e'''∈ energy_Min {inv_upd (the (weight g g')) e' | e' g'. e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ F' g'} ∧ e''' e≤ inv_upd (the (weight g g')) e''"
          using energy_Min_contains_smaller
          by (smt (verit, del_insts) inv_well_defined mem_Collect_eq subset_iff)
        hence "∃e'''. e''' ∈ iteration F' g ∧ e''' e≤ inv_upd (the (weight g g')) e''" 
          unfolding iteration_def using True by simp
        from this obtain e''' where E''': "e''' ∈ iteration F' g ∧ e''' e≤ inv_upd (the (weight g g')) e''" by auto
        hence "e''' e≤ e" using E uE energy_order
          by (smt (verit, ccfv_threshold) E'' assms(2) energy_wqo galois_energy_game_decidable.possible_pareto_def galois_energy_game_decidable_axioms in_mono inv_well_defined iteration_pareto_functor mem_Collect_eq transp_onD wqo_on_imp_transp_on)         
        then show ?thesis using E''' by auto
      next
        case False
        hence "e∈ (energy_Min {energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}| e_index. (∀g'. weight g g' ≠ None ⟶ ( (e_index g')∈ energies ∧ e_index g' ∈ F g'))})"
          using iteration_def ‹e ∈ iteration F g› by simp
        from this obtain e_index where E: "e= energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}" and "(∀g'. weight g g' ≠ None ⟶ ((e_index g')∈ energies ∧ e_index g' ∈ F g'))" 
          using energy_Min_def by auto
        hence "⋀g'.  weight g g' ≠ None ⟹ ∃e'. e' ∈ F' g' ∧ e' e≤ e_index g'"
          using assms(3) pareto_order_def by force
        define e_index' where "e_index' ≡ (λg'. (SOME e'. (e' ∈ F' g' ∧ e' e≤ e_index g')))"
        hence E': "⋀g'. weight g g' ≠ None ⟹ e_index' g' ∈ F' g' ∧ e_index' g' e≤ e_index g'"
          using ‹⋀g'.  weight g g' ≠ None ⟹ ∃e'. e' ∈ F' g' ∧ e' e≤ e_index g'› some_eq_ex
          by (metis (mono_tags, lifting))
        hence "⋀g'. weight g g' ≠ None ⟹ inv_upd (the (weight g g')) (e_index' g') e≤ inv_upd (the (weight g g')) (e_index g')"
          using inverse_monotonic 
          using ‹∀g'. weight g g' ≠ None ⟶ (e_index g')∈ energies ∧ e_index g' ∈ F g'›
          using inv_well_defined energy_order
          by (smt (verit) Collect_mem_eq assms(2) galois_energy_game_decidable.possible_pareto_def galois_energy_game_decidable_axioms mem_Collect_eq subsetD)
        hence leq: "⋀a. a∈ {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} ⟹ ∃b. b ∈ {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None} ∧ a e≤ b"
          by blast
        have len: "⋀a. a∈ {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} ⟹ a ∈ energies"
          using  E' E inv_well_defined
          using ‹∀g'. weight g g' ≠ None ⟶ (e_index g') ∈ energies ∧ e_index g' ∈ F g'› energy_order
          using assms(2) galois_energy_game_decidable.possible_pareto_def galois_energy_game_decidable_axioms in_mono by blast
        hence leq: "energy_sup {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} e≤ energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}"
        proof(cases "{g'. weight g g' ≠ None} = {}")
          case True
          hence "{inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} = {} ∧ {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None} = {}"
            by simp
          then show ?thesis
            by (simp add: bounded_join_semilattice)
        next
          case False

          have in_energy: "{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⊆ energies"
            using ‹∀g'. weight g g' ≠ None ⟶ e_index g' ∈ energies ∧ e_index g' ∈ F g'› inv_well_defined by blast 

          have fin: "finite {inv_upd (the (weight g g')) (e_index' g') |g'. weight g g' ≠ None} ∧ finite {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}"
          proof
            have "{inv_upd (the (weight g g')) (e_index' g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (e_index' g') |g'. g' ∈ positions}"
              by auto
            thus "finite {inv_upd (the (weight g g')) (e_index' g') |g'. weight g g' ≠ None}"
              using finite_positions
              using rev_finite_subset by fastforce 
            have "{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (e_index g') |g'. g' ∈ positions}"
              by auto
            thus "finite {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}"
              using finite_positions
              using rev_finite_subset by fastforce 
          qed

          from False have "{inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} ≠ {}" by simp
          then show ?thesis using energy_sup_leq_energy_sup len leq fin in_energy
            by meson
        qed

        have "⋀g'. weight g g' ≠ None ⟹ (e_index' g')∈ energies" using E' ‹∀g'. weight g g' ≠ None ⟶ (e_index g')∈ energies ∧ e_index g' ∈ F g'›
          using assms(2) galois_energy_game_decidable.possible_pareto_def galois_energy_game_decidable_axioms in_mono by blast
        hence "energy_sup {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} ∈ {energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}| e_index. (∀g'. weight g g' ≠ None ⟶ ((e_index g')∈ energies ∧ e_index g' ∈ F' g'))}"
          using E'
          by blast 
        hence "∃e'. e' ∈ energy_Min {energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}| e_index. (∀g'. weight g g' ≠ None ⟶ ((e_index g') ∈ energies ∧ e_index g' ∈ F' g'))}
              ∧ e' e≤ energy_sup {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None}"
          using energy_Min_contains_smaller
        proof -
          obtain ee :: "'energy ⇒ 'energy set ⇒ 'energy" and eea :: "'energy ⇒ 'energy set ⇒ 'energy" where
            f1: "∀e E. ee e E e≤ e ∧ ee e E ∈ energy_Min E ∨ ¬ E ⊆ energies ∨ e ∉ E"
            using energy_Min_contains_smaller by moura
          have "finite ({}::'energy set)"
            by blast
          have in_energy: "⋀f. ∀p. weight g p ≠ None ⟶ f p ∈ energies ∧ f p ∈ F' p ⟹ {inv_upd (the (weight g p)) (f p) |p. weight g p ≠ None} ⊆ energies"
            using inv_well_defined by blast 
          have "⋀f. ∀p. weight g p ≠ None ⟶ f p ∈ energies ∧ f p ∈ F' p ⟹ finite {inv_upd (the (weight g p)) (f p) |p. weight g p ≠ None}"
          proof-
            fix f 
            have "{inv_upd (the (weight g p)) (f p) |p. weight g p ≠ None} ⊆ {inv_upd (the (weight g p)) (f p) |p. p ∈ positions}" by auto
            thus "∀p. weight g p ≠ None ⟶ f p ∈ energies ∧ f p ∈ F' p ⟹ finite {inv_upd (the (weight g p)) (f p) |p. weight g p ≠ None}" using finite_positions
              by (simp add: rev_finite_subset) 
          qed
          then have "{energy_sup {inv_upd (the (weight g p)) (f p) |p. weight g p ≠ None} | f. ∀p. weight g p ≠ None ⟶ f p ∈ energies ∧ f p ∈ F' p} ⊆ energies"
            using in_energy bounded_join_semilattice
            by force
          then show ?thesis
            using f1 ‹energy_sup {inv_upd (the (weight g g')) (e_index' g') |g'. weight g g' ≠ None} ∈ {energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} | e_index. ∀g'. weight g g' ≠ None ⟶ e_index g' ∈ energies ∧ e_index g' ∈ F' g'}› by blast
        qed 
        hence "∃e'. e' ∈ iteration F' g ∧ e' e≤ energy_sup {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} "
          unfolding iteration_def using False by auto
        from this obtain e' where "e' ∈ iteration F' g" and "e' e≤ energy_sup {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} " by auto
        hence " e' e≤ energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}"
          using leq energy_order ordering_def
          by (metis (no_types, lifting) partial_preordering.trans)
        then show ?thesis using E energy_order ordering_def ‹e' ∈ iteration F' g›
          by auto
      qed
    qed
  qed
qed

lemma finite_directed_set_upper_bound:
  assumes "⋀F F'. F ∈ P ⟹ F' ∈ P ⟹ ∃F''. F'' ∈ P ∧ F ≼ F'' ∧ F' ≼ F''" 
          and "P ≠ {}" and "P' ⊆ P" and "finite P'" and "P ⊆ possible_pareto"
  shows "∃F'. F' ∈ P ∧ (∀F. F ∈ P' ⟶ F ≼ F')"
  using assms proof(induct "card P'" arbitrary: P')
  case 0
  then show ?case
    by auto
next
  case (Suc x)
  hence "∃F. F ∈ P'"
    by auto 
  from this obtain F where "F ∈ P'" by auto
  define P'' where "P'' = P' - {F}"
  hence "card P'' = x" using Suc card_Suc_Diff1 ‹F ∈ P'› by simp
  hence "∃F'. F' ∈ P ∧ (∀F. F ∈ P'' ⟶ F ≼ F')" using Suc
    using P''_def by blast 
  from this obtain F' where "F' ∈ P ∧ (∀F. F ∈ P'' ⟶ F ≼ F')" by auto
  hence "∃F''. F'' ∈ P ∧ F ≼ F'' ∧ F' ≼ F''" using Suc
    by (metis (no_types, lifting) ‹F ∈ P'› in_mono)
  from this obtain F'' where "F'' ∈ P ∧ F ≼ F'' ∧ F' ≼ F''" by auto
  show ?case 
  proof
    show "F'' ∈ P ∧ (∀F. F ∈ P' ⟶ F ≼ F'')" 
    proof
      show "F'' ∈ P" using ‹F'' ∈ P ∧ F ≼ F'' ∧ F' ≼ F''› by simp
      show "∀F. F ∈ P' ⟶ F ≼ F''"
      proof
        fix F0
        show "F0 ∈ P' ⟶ F0 ≼ F''"
        proof
          assume "F0 ∈ P'"
          show "F0 ≼ F''"
          proof(cases "F0 = F")
            case True
            then show ?thesis using ‹F'' ∈ P ∧ F ≼ F'' ∧ F' ≼ F''› by simp
          next
            case False
            hence "F0 ∈ P''" using P''_def ‹F0 ∈ P'› by auto 
            hence "F0 ≼ F'" using ‹F' ∈ P ∧ (∀F. F ∈ P'' ⟶ F ≼ F')› by simp
            then show ?thesis using ‹F'' ∈ P ∧ F ≼ F'' ∧ F' ≼ F''› transitivity Suc
              by (smt (z3) ‹F' ∈ P ∧ (∀F. F ∈ P'' ⟶ F ≼ F')› ‹F0 ∈ P'› subsetD) 
          qed
        qed
      qed
    qed
  qed
qed

lemma iteration_scott_continuous_vanilla:
  assumes "P ⊆ possible_pareto" and 
          "⋀F F'. F ∈ P ⟹ F' ∈ P ⟹ ∃F''. F'' ∈ P ∧ F ≼ F'' ∧ F' ≼ F''" and "P ≠ {}"
  shows "iteration (pareto_sup P) = pareto_sup {iteration F | F. F ∈ P}"
proof(rule antisymmetry)
  from assms have "(pareto_sup P) ∈ possible_pareto" using assms pareto_sup_is_sup by simp
  thus A: "iteration (pareto_sup P) ∈ possible_pareto" using iteration_pareto_functor by simp

  have B: "{iteration F |F. F ∈ P} ⊆ possible_pareto"
  proof
    fix F
    assume "F ∈ {iteration F |F. F ∈ P}"
    from this obtain F' where "F = iteration F'" and "F' ∈ P" by auto
    thus "F ∈ possible_pareto" using iteration_pareto_functor
      using assms by auto 
  qed
  thus "pareto_sup {iteration F |F. F ∈ P} ∈ possible_pareto" using pareto_sup_is_sup by simp

  show "iteration (pareto_sup P) ≼ pareto_sup {iteration F |F. F ∈ P}"
    unfolding pareto_order_def proof
    fix g 
    show " ∀e. e ∈ iteration (pareto_sup P) g ⟶
             (∃e'. e' ∈ pareto_sup {iteration F |F. F ∈ P} g ∧ e' e≤ e)"
    proof
      fix e
      show "e ∈ iteration (pareto_sup P) g ⟶
             (∃e'. e' ∈ pareto_sup {iteration F |F. F ∈ P} g ∧ e' e≤ e)"
      proof
        assume "e ∈ iteration (pareto_sup P) g"
        show "∃e'. e' ∈ pareto_sup {iteration F |F. F ∈ P} g ∧ e' e≤ e"
        proof(cases "g ∈ attacker")
          case True
          hence "e ∈ energy_Min {inv_upd (the (weight g g')) e' | e' g'. e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ (pareto_sup P) g'}"
            using iteration_def ‹e ∈ iteration (pareto_sup P) g› by auto 
          from this obtain e' g' where "e = inv_upd (the (weight g g')) e'" and "e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ (pareto_sup P) g'" 
            using energy_Min_def by auto
          hence "∃F. F∈ P ∧ e' ∈ F g'" using pareto_sup_def energy_Min_def by simp
          from this obtain F where "F∈ P ∧ e' ∈ F g'" by auto
          hence E:  "e ∈ {inv_upd (the (weight g g')) e' | e' g'. e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ F g'}" using ‹e = inv_upd (the (weight g g')) e'›
            using ‹e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ pareto_sup P g'› by blast  

          have "{inv_upd (the (weight g g')) e' |e' g'. e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ F g'} ⊆ energies"
            using inv_well_defined by blast
          hence "∃e''. e'' ∈ energy_Min {inv_upd (the (weight g g')) e' | e' g'. e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ F g'} ∧ e'' e≤ e"
            using energy_Min_contains_smaller E
            by meson
          hence "∃e''. e'' ∈ iteration F g ∧ e'' e≤ e" using True iteration_def by simp
          from this obtain e'' where "e'' ∈ iteration F g ∧ e'' e≤ e" by auto
          have "∃e''' ∈ pareto_sup {iteration F |F. F ∈ P} g.  e''' e≤ e''" 
            unfolding pareto_sup_def proof(rule energy_Min_contains_smaller)
            show "e'' ∈ {e. ∃F. F ∈ {iteration F |F. F ∈ P} ∧ e ∈ F g}"
              using ‹e'' ∈ iteration F g ∧ e'' e≤ e›
              using ‹F ∈ P ∧ e' ∈ F g'› by blast
            show "{e. ∃F. F ∈ {iteration F |F. F ∈ P} ∧ e ∈ F g} ⊆ energies"
            proof
              fix x
              assume X: "x ∈ {e. ∃F. F ∈ {iteration F |F. F ∈ P} ∧ e ∈ F g}"
              from this obtain F where "F ∈ {iteration F |F. F ∈ P} ∧ x ∈ F g" by auto
              from this obtain F' where "F = iteration F'" and "F' ∈ P" by auto
              hence "F ∈ possible_pareto" using assms
                using iteration_pareto_functor by auto 
              thus "x ∈ energies " unfolding possible_pareto_def using X
                using ‹F ∈ {iteration F |F. F ∈ P} ∧ x ∈ F g› by blast 
            qed
          qed
          then show ?thesis
            using ‹e'' ∈ iteration F g ∧ e'' e≤ e› energy_order ordering_def
            by (metis (mono_tags, lifting) partial_preordering_def)
        next
          case False
          hence "e ∈ energy_Min {energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}| e_index. (∀g'. weight g g' ≠ None ⟶ ((e_index g') ∈ energies ∧ e_index g' ∈ (pareto_sup P) g'))}"
            using iteration_def ‹e ∈ iteration (pareto_sup P) g› by auto
          from this obtain e_index where "e= energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}" and "(∀g'. weight g g' ≠ None ⟶ ( (e_index g')∈ energies  ∧ e_index g' ∈ (pareto_sup P) g'))"
            using energy_Min_def by auto
          hence "⋀g'. weight g g' ≠ None ⟹ e_index g' ∈ (pareto_sup P) g'" by auto
          hence "⋀g'. weight g g' ≠ None ⟹ ∃F'. F' ∈ P ∧ e_index g' ∈ F' g'" using pareto_sup_def energy_Min_def
            by (simp add: mem_Collect_eq) 
          define F_index where "F_index ≡ λg'. SOME F'. F' ∈ P ∧ e_index g' ∈ F' g'"
          hence Fg: "⋀g'. weight g g' ≠ None ⟹ F_index g' ∈ P ∧ e_index g' ∈ F_index g' g'" 
            using ‹⋀g'. weight g g' ≠ None ⟹ ∃F'. F' ∈ P ∧ e_index g' ∈ F' g'› some_eq_ex
            by (smt (verit)) 

          have "∃F'. F' ∈ P ∧ (∀F. F ∈ {F_index g' | g'. weight g g' ≠ None} ⟶ F ≼ F')"
          proof(rule finite_directed_set_upper_bound)
            show "⋀F F'. F ∈ P ⟹ F' ∈ P ⟹ ∃F''. F'' ∈ P ∧ F ≼ F'' ∧ F' ≼ F''" using assms by simp
            show "P ≠ {}" using assms by simp
            show "{F_index g' |g'. weight g g' ≠ None} ⊆ P"
              using Fg
              using subsetI by auto 
            have "finite {g'. weight g g' ≠ None}" using finite_positions
              by (metis Collect_mono finite_subset)
            thus "finite {F_index g' | g'. weight g g' ≠ None}" by auto
            show "P ⊆ possible_pareto" using assms by simp
          qed
          from this obtain F where F: "F ∈ P ∧ (∀g'. weight g g' ≠ None ⟶  F_index g' ≼ F)" by auto
          hence "F ∈ possible_pareto" using assms by auto
          have "⋀g'. weight g g' ≠ None ⟹ ∃e'. e' ∈ F g' ∧ e' e≤ e_index g'"
          proof-
            fix g'
            assume "weight g g' ≠ None"
            hence "e_index g' ∈ F_index g' g'" using Fg by auto
            have "F_index g' ≼ F" using F ‹weight g g' ≠ None›  by auto
            thus "∃e'. e' ∈ F g' ∧ e' e≤ e_index g'" unfolding pareto_order_def
              using ‹e_index g' ∈ F_index g' g'› by fastforce
          qed

          define e_index' where "e_index' ≡ λg'. SOME e'. e' ∈ F g' ∧ e' e≤ e_index g'"
          hence "⋀g'. weight g g' ≠ None ⟹ e_index' g'∈ F g' ∧ e_index' g' e≤ e_index g'"
            using ‹⋀g'. weight g g' ≠ None ⟹ ∃e'. e' ∈ F g' ∧ e' e≤ e_index g'› some_eq_ex by (smt (verit))
          hence "energy_sup {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} e≤ energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}"
          proof(cases "{g'. weight g g' ≠ None} = {}")
            case True
            hence "{inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} = {}" by simp
            have "{inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None} = {}" using True by simp
            then show ?thesis unfolding energy_order using ‹{inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} = {}›
              using energy_order ordering.eq_iff by fastforce
          next
            case False            
            show ?thesis 
            proof(rule energy_sup_leq_energy_sup)
              show "{inv_upd (the (weight g g')) (e_index' g') |g'. weight g g' ≠ None} ≠ {}" 
                using False by simp
              show "⋀a. a ∈ {inv_upd (the (weight g g')) (e_index' g') |g'. weight g g' ≠ None} ⟹
                    ∃b∈{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}. a e≤ b"
              proof-
                fix a 
                assume "a ∈ {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None}"
                from this obtain g' where "a=inv_upd (the (weight g g')) (e_index' g')" and "weight g g' ≠ None" by auto
                have "(e_index' g') e≤  (e_index' g')" 
                  using ‹weight g g' ≠ None› ‹⋀g'. weight g g' ≠ None ⟹ e_index' g'∈ F g' ∧ e_index' g' e≤ e_index g'›
                  by (meson energy_order ordering.eq_iff)
                have "(e_index' g') ∈ energies " 
                  using ‹⋀g'. weight g g' ≠ None ⟹ e_index' g'∈ F g' ∧ e_index' g' e≤ e_index g'› possible_pareto_def ‹weight g g' ≠ None› F assms
                  by blast 
                hence "a e≤ inv_upd (the (weight g g')) (e_index' g')"
                  using ‹a=inv_upd (the (weight g g')) (e_index' g')› ‹(e_index' g') e≤ (e_index' g')› inverse_monotonic  ‹weight g g' ≠ None›
                  using inv_well_defined by presburger
                hence "a e≤ inv_upd (the (weight g g')) (e_index g')"
                  using ‹⋀g'. weight g g' ≠ None ⟹ e_index' g' ∈ F g' ∧ e_index' g' e≤ e_index g'›
                  using ‹a = inv_upd (the (weight g g')) (e_index' g')› ‹e_index' g' ∈ energies› ‹weight g g' ≠ None› inv_well_defined inverse_monotonic by blast
                thus "∃b∈{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}. a e≤ b"
                  using ‹weight g g' ≠ None› by blast
              qed
              show "⋀a. a ∈ {inv_upd (the (weight g g')) (e_index' g') |g'. weight g g' ≠ None} ⟹
                    a ∈ energies"
              proof-
                fix a 
                assume "a ∈ {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None}"
                from this obtain g' where "a=inv_upd (the (weight g g')) (e_index' g')" and "weight g g' ≠ None" by auto
                hence "e_index' g'∈ F g'" using ‹⋀g'. weight g g' ≠ None ⟹ e_index' g'∈ F g' ∧ e_index' g' e≤ e_index g'›
                  by simp
                hence "(e_index' g') ∈ energies" using ‹F ∈ possible_pareto› possible_pareto_def
                  by blast 
                thus "a ∈ energies" using ‹a=inv_upd (the (weight g g')) (e_index' g')›  ‹weight g g' ≠ None›
                  using inv_well_defined by blast
              qed
              have "{inv_upd (the (weight g g')) (e_index' g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (e_index' g') |g'. g' ∈ positions}" by auto
              thus "finite {inv_upd (the (weight g g')) (e_index' g') |g'. weight g g' ≠ None}"
                using finite_positions
                using rev_finite_subset by fastforce 
              have "{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (e_index g') |g'. g' ∈ positions}" by auto
              thus "finite {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}"
                using finite_positions
                using rev_finite_subset by fastforce
              show "{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⊆ energies"
                using ‹∀g'. weight g g' ≠ None ⟶ e_index g' ∈ energies ∧ e_index g' ∈ pareto_sup P g'› inv_well_defined by blast
            qed
          qed
          hence leq: "energy_sup {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None} e≤ e"
            using ‹e= energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}› by simp

          have in_energies: "{energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} |e_index. ∀g'. weight g g' ≠ None ⟶ e_index g' ∈ energies ∧ e_index g' ∈ F g'} ⊆ energies"
          proof
            fix x 
            assume "x ∈ {energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} |e_index. ∀g'. weight g g' ≠ None ⟶ e_index g' ∈ energies ∧ e_index g' ∈ F g'}"
            from this obtain e_index where X: "x = energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}" and "∀g'. weight g g' ≠ None ⟶ e_index g' ∈ energies ∧ e_index g' ∈ F g'" by auto
            have "{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (e_index g') |g'. g' ∈ positions}" by auto
            hence fin: "finite {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}" using finite_positions
              using rev_finite_subset by fastforce 
            have "{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⊆ energies"
              using ‹∀g'. weight g g' ≠ None ⟶ e_index g' ∈ energies ∧ e_index g' ∈ F g'› inv_well_defined by force 
            thus "x ∈ energies" unfolding X using bounded_join_semilattice fin
              by meson
          qed
          have in_energies2: "{e. ∃F. (F ∈ {iteration F |F. F ∈ P} ∧ e ∈ F g)} ⊆ energies"
            using assms unfolding possible_pareto_def
            by (smt (verit) B mem_Collect_eq possible_pareto_def subset_iff) 
          have "⋀g'. weight g g' ≠ None ⟹ e_index' g'∈ F g'" using ‹⋀g'. weight g g' ≠ None ⟹ e_index' g'∈ F g' ∧ e_index' g' e≤ e_index g'›
            by simp
          hence "⋀g'. weight g g' ≠ None ⟹ (e_index' g') ∈ energies" using ‹F ∈ possible_pareto› possible_pareto_def
            by blast 
          hence "(energy_sup {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None}) ∈ {energy_sup
            {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} |
           e_index.
           ∀g'. weight g g' ≠ None ⟶ (e_index g') ∈ energies ∧ e_index g' ∈ F g'}"
            using ‹⋀g'. weight g g' ≠ None ⟹ e_index' g' ∈ F g' ∧ e_index' g' e≤ e_index g'› by auto
          hence "∃e'. e' ∈ iteration F g ∧ e' e≤ (energy_sup {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None})"
            unfolding iteration_def using energy_Min_contains_smaller False in_energies
            by meson 
          from this obtain e' where E': "e' ∈ iteration F g ∧ e' e≤ (energy_sup {inv_upd (the (weight g g')) (e_index' g')| g'. weight g g' ≠ None})"
            by auto
          hence "e' ∈ {(e::'energy). (∃F. F∈ {iteration F |F. F ∈ P} ∧  e∈ (F g))}" using F by auto 

          hence "∃a. a ∈ pareto_sup {iteration F |F. F ∈ P} g ∧ a e≤ e'"
            unfolding pareto_sup_def using energy_Min_contains_smaller in_energies2 by meson
          from this obtain a where "a ∈ pareto_sup {iteration F |F. F ∈ P} g ∧ a e≤ e'" by auto
          hence "a e≤ e" using E' leq energy_order ordering_def
            by (metis (no_types, lifting) partial_preordering.trans) 
          then show ?thesis using ‹a ∈ pareto_sup {iteration F |F. F ∈ P} g ∧ a e≤ e'› by auto
        qed
      qed
    qed
  qed
  
  show "pareto_sup {iteration F |F. F ∈ P} ≼ iteration (pareto_sup P)"
  proof(rule pareto_sup_is_sup(3))
    show "{iteration F |F. F ∈ P} ⊆ possible_pareto" using B by simp
    show "iteration (pareto_sup P) ∈ possible_pareto" using A by simp
    show "⋀F. F ∈ {iteration F |F. F ∈ P} ⟹ F ≼ iteration (pareto_sup P)"
    proof-
      fix F
      assume "F ∈ {iteration F |F. F ∈ P}"
      from this obtain F' where "F = iteration F'" and "F' ∈ P" by auto
      hence "F' ≼ pareto_sup P" using pareto_sup_is_sup
        by (simp add: assms)
      thus "F ≼ iteration (pareto_sup P)" using ‹F = iteration F'› iteration_monotonic assms
        by (simp add: ‹F' ∈ P› ‹pareto_sup P ∈ possible_pareto› subsetD) 
    qed
  qed
qed

lemma iteration_scott_continuous: 
  shows "scott_continuous possible_pareto (≼) possible_pareto (≼) iteration"
proof
  show "iteration ` possible_pareto ⊆ possible_pareto"
    using iteration_pareto_functor
    by blast 
  show "⋀X s. directed_set X (≼) ⟹
           X ≠ {} ⟹
           X ⊆ possible_pareto ⟹
           extreme_bound possible_pareto (≼) X s ⟹
           extreme_bound possible_pareto (≼) (iteration ` X) (iteration s)"
  proof-
    fix P s
    assume A1: "directed_set P (≼)" and A2: "P ≠ {}" and A3: "P ⊆ possible_pareto" and
           A4: "extreme_bound possible_pareto (≼) P s"
    hence A4: "s = pareto_sup P" unfolding extreme_bound_def using pareto_sup_is_sup
      by (metis (no_types, lifting) A4 antisymmetry extreme_bound_iff)

    from A1 have A1: "⋀F F'. F ∈ P ⟹ F' ∈ P ⟹ ∃F''. F'' ∈ P ∧ F ≼ F'' ∧ F' ≼ F''" 
      unfolding directed_set_def
      by (metis A1 directedD2) 

    hence "iteration s = pareto_sup {iteration F |F. F ∈ P}" 
      using iteration_scott_continuous_vanilla A2 A3 A4 finite_positions
      by blast 

    show "extreme_bound possible_pareto (≼) (iteration ` P) (iteration s)"
      unfolding ‹iteration s = pareto_sup {iteration F |F. F ∈ P}› extreme_bound_def
    proof
      have A3: "{iteration F |F. F ∈ P} ⊆ possible_pareto" 
        using iteration_pareto_functor A3
        by auto 

      thus "pareto_sup {iteration F |F. F ∈ P} ∈ {b ∈ possible_pareto. bound (iteration ` P) (≼) b}"
      using pareto_sup_is_sup
      by (simp add: Setcompr_eq_image bound_def)

      show "⋀x. x ∈ {b ∈ possible_pareto. bound (iteration ` P) (≼) b} ⟹
         pareto_sup {iteration F |F. F ∈ P} ≼ x"
        using A3 pareto_sup_is_sup
        by (smt (verit, del_insts) bound_def image_eqI mem_Collect_eq)
    qed
  qed
qed

text‹We now show that ‹a_win_min› is a fixed point of ‹iteration›.›

lemma a_win_min_is_fp:
  shows "iteration a_win_min = a_win_min"
proof
  
  have  minimal_winning_budget_attacker: "⋀g e. g ∈ attacker ⟹ minimal_winning_budget e g = (e ∈ energy_Min {e. ∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e=(the (inverse_application (the (weight g g')) e'))})"
  proof-
    fix g e 
    assume "g ∈ attacker" ‹g ∈ attacker›
    have attacker_inv_in_winning_budget: "⋀g g' e'. g ∈ attacker ⟹ weight g g' ≠ None ⟹ winning_budget_len e' g' ⟹ winning_budget_len (inv_upd (the (weight g g')) e') g"
    proof-
      fix g g' e' 
      assume A1: "g ∈ attacker" and A2: " weight g g' ≠ None" and A3: "winning_budget_len e' g'"
      show "winning_budget_len (inv_upd (the (weight g g')) e') g"
      proof
        from A3 have "e' ∈ energies" using winning_budget_len.simps
          by blast
        show "(the (inverse_application (the (weight g g')) e')) ∈ energies ∧ g ∈ attacker ∧
           (∃g'a. weight g g'a ≠ None ∧
           application (the (weight g g'a)) (the (inverse_application (the (weight g g')) e')) ≠ None ∧
           winning_budget_len (the (application (the (weight g g'a)) (the (inverse_application (the (weight g g')) e')))) g'a) "
        proof
          show "(the (inverse_application (the (weight g g')) e')) ∈ energies" using ‹e' ∈ energies› A2
            using inv_well_defined by blast
          show "g ∈ attacker ∧
           (∃g'a. weight g g'a ≠ None ∧
           application (the (weight g g'a)) (the (inverse_application (the (weight g g')) e')) ≠ None ∧
           winning_budget_len (the (application (the (weight g g'a)) (the (inverse_application (the (weight g g')) e')))) g'a) "
          proof
            show "g ∈ attacker" using A1 .
            show "∃g'a. weight g g'a ≠ None ∧
          application (the (weight g g'a)) (the (inverse_application (the (weight g g')) e')) ≠ None ∧
          winning_budget_len (the (application (the (weight g g'a)) (the (inverse_application (the (weight g g')) e')))) g'a"
            proof
              show "weight g g' ≠ None ∧
                application (the (weight g g')) (the (inverse_application (the (weight g g')) e')) ≠ None ∧
                winning_budget_len (the (application (the (weight g g')) (the (inverse_application (the (weight g g')) e')))) g'"
              proof
                show "weight g g' ≠ None" using A2 .
                show "application (the (weight g g')) (the (inverse_application (the (weight g g')) e')) ≠ None ∧
                    winning_budget_len (the (application (the (weight g g')) (the (inverse_application (the (weight g g')) e')))) g'"
                proof 
                  from A1 A2 show "application (the (weight g g')) (the (inverse_application (the (weight g g')) e')) ≠ None" using inv_well_defined
                    by (simp add: ‹e' ∈ energies›) 
                  have "order e' (the (application (the (weight g g')) (the (inverse_application (the (weight g g')) e'))))" using upd_inv_increasing
                    using A2 ‹e' ∈ energies› by blast 
                  thus "winning_budget_len (the (application (the (weight g g')) (the (inverse_application (the (weight g g')) e')))) g'" using  upwards_closure_wb_len
                    using A3 by auto 
                qed
              qed
            qed
          qed
        qed
      qed
    qed

    have min_winning_budget_is_inv_a: "⋀e g. g ∈ attacker ⟹ minimal_winning_budget e g ⟹ ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g' ∧ e = (inv_upd (the (weight g g')) e')"
    proof-
      fix e g
      assume A1: "g ∈ attacker" and A2: " minimal_winning_budget e g"
      show "∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g' ∧ e = (inv_upd (the (weight g g')) e')"
      proof-
        from A1 A2 have "winning_budget_len e g" using energy_Min_def by simp
        hence ‹e ∈ energies› using winning_budget_len.simps by blast
        from A1 A2 ‹winning_budget_len e g› have " (∃g'. (weight g g' ≠ None) ∧ (application (the (weight g g')) e)≠ None ∧ (winning_budget_len (the (application (the (weight g g')) e)) g') )" 
          using winning_budget_len.simps
          by blast 
        from this obtain g' where G: "(weight g g' ≠ None) ∧ (application (the (weight g g')) e)≠ None ∧ (winning_budget_len (the (application (the (weight g g')) e)) g')" by auto
        hence "(the (application (the (weight g g')) e)) ∈ energies"
          using ‹e ∈ energies› upd_well_defined by blast 
        hence W: "winning_budget_len (the (inverse_application (the (weight g g')) (the (application (the (weight g g')) e)))) g" using G attacker_inv_in_winning_budget
          by (meson A1)
        have "order (the (inverse_application (the (weight g g')) (the (application (the (weight g g')) e)))) e" using inv_upd_decreasing
          using G
          using ‹e ∈ energies› by blast
        hence E: "e = (the (inverse_application (the (weight g g')) (the (application (the (weight g g')) e))))" using W A1 A2 energy_Min_def
          by auto 
        show ?thesis 
        proof
          show "∃e'. weight g g' ≠ None ∧ winning_budget_len e' g' ∧ e = the (inverse_application (the (weight g g')) e') "
          proof
            show "weight g g' ≠ None ∧ winning_budget_len (the (application (the (weight g g')) e)) g' ∧ e = the (inverse_application (the (weight g g')) (the (application (the (weight g g')) e)))" 
              using G E by simp 
          qed
        qed
      qed
    qed

    have min_winning_budget_a_iff_energy_Min: "minimal_winning_budget e g
    ⟷ e ∈ energy_Min {e. ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g' ∧ e=(inv_upd (the (weight g g')) e')}"
    proof-
      have len: "⋀e. e∈ {e. ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))} ⟹ e ∈ energies"
      proof-
        fix e
        assume "e∈ {e. ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))}"
        hence "∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))" by auto
        from this obtain g' e' where eg: "weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))" by auto
        hence "weight g g' ≠ None" by auto
        from eg have "e' ∈ energies" using winning_budget_len.simps by blast 
        thus "e ∈ energies" using eg ‹e' ∈ energies›
          using inv_well_defined by blast
      qed

      show ?thesis 
      proof
        assume "minimal_winning_budget e g"
        hence A: "winning_budget_len e g ∧ (∀e'. e' ≠ e ⟶ e' e≤ e ⟶ ¬ winning_budget_len e' g)" using energy_Min_def by auto
        hence E: "e∈ {e. ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))}" 
          using min_winning_budget_is_inv_a ‹g ∈ attacker›
          by (simp add: ‹minimal_winning_budget e g›) 

        have "⋀x. x ∈ {e. ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))} ∧ order x e ⟹ e=x"
        proof-
          fix x 
          assume X: "x ∈ {e. ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g' ∧ e=(the (inverse_application (the (weight g g')) e'))} ∧ order x e"
          have "winning_budget_len x g" 
          proof
            show "x ∈ energies ∧
              g ∈ attacker ∧
              (∃g'. weight g g' ≠ None ∧
            application (the (weight g g')) x ≠ None ∧ winning_budget_len (the (application (the (weight g g')) x)) g')"
            proof
              show "x ∈ energies" using len X by blast
              show "g ∈ attacker ∧
                (∃g'. weight g g' ≠ None ∧
                application (the (weight g g')) x ≠ None ∧ winning_budget_len (the (application (the (weight g g')) x)) g')"                         
              proof
                show "g ∈ attacker" using ‹g ∈ attacker›.

                from X have "∃g' e'.
              weight g g' ≠ None ∧
              winning_budget_len e' g' ∧ x = inv_upd (the (weight g g')) e'"
                  by blast
                from this obtain g' e' where X: "weight g g' ≠ None ∧
              winning_budget_len e' g' ∧ x = inv_upd (the (weight g g')) e'" by auto

                show "∃g'. weight g g' ≠ None ∧
         apply_w g g' x ≠ None ∧ winning_budget_len (upd (the (weight g g')) x) g'"
                proof
                  show "weight g g' ≠ None ∧
         apply_w g g' x ≠ None ∧ winning_budget_len (upd (the (weight g g')) x) g'"
                  proof
                    show "weight g g' ≠ None" using X by simp
                    show "apply_w g g' x ≠ None ∧ winning_budget_len (upd (the (weight g g')) x) g'"
                    proof

                      have "e' e≤ (upd (the (weight g g')) x)" 
                        using X upd_inv_increasing 
                        by (metis winning_budget_len.simps)
                      have "winning_budget_len (inv_upd (the (weight g g')) e') g"
                        using X attacker_inv_in_winning_budget ‹weight g g' ≠ None› ‹g ∈ attacker›
                        by blast
                      thus "winning_budget_len (upd (the (weight g g')) x) g'"
                        using ‹e' e≤ (upd (the (weight g g')) x)› upwards_closure_wb_len X by blast

                      have "inverse_application (the (weight g g')) e' ≠ None" 
                        using inv_well_defined  ‹weight g g' ≠ None›
                        by (metis X winning_budget_len.simps)
                      thus "apply_w g g' x ≠ None"
                        using X inv_well_defined
                        using nonpos_eq_pos winning_bugget_len_is_wb by blast 
                    qed
                  qed
                qed
              qed
            qed
          qed
          thus "e=x" using X A 
            by metis 
        qed
        thus "e ∈ energy_Min {e. ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))}"
          using E energy_Min_def
          by (smt (verit, del_insts) mem_Collect_eq) 
      next
        assume "e ∈ energy_Min {e. ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))}"
        hence E: "e ∈ {e. ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))}"
          using energy_Min_def by auto
        have "winning_budget_len e g ∧ (∀e'. e' ≠ e ⟶ order e' e ⟶ ¬ winning_budget_len e' g)"
        proof
          show W: "winning_budget_len e g" using len E ‹g ∈ attacker› winning_budget_len.intros
            by (smt (verit, ccfv_SIG) attacker_inv_in_winning_budget mem_Collect_eq)

          from W have "e∈ {e''. order e'' e ∧ winning_budget_len e'' g}" using energy_order ordering_def
            by (metis (no_types, lifting) mem_Collect_eq partial_preordering_def)
          hence notempty: "{} ≠ {e''. order e'' e ∧ winning_budget_len e'' g}" by auto
          have "⋀e''. e'' ∈ {e''. order e'' e ∧ winning_budget_len e'' g} ⟹ e'' ∈ energies" 
            using winning_budget_len.simps by blast
          hence "{} ≠ energy_Min {e''. order e'' e ∧ winning_budget_len e'' g}" using energy_Min_not_empty notempty
            by (metis (no_types, lifting) subsetI) 
          hence "∃e''. e'' ∈ energy_Min {e''. order e'' e ∧ winning_budget_len e'' g}" by auto
          from this obtain e'' where "e'' ∈ energy_Min {e''. order e'' e ∧ winning_budget_len e'' g}" by auto
          hence X: "order e'' e ∧ winning_budget_len e'' g ∧ (∀e'. e'∈ {e''. order e'' e ∧ winning_budget_len e'' g} ⟶ e'' ≠ e' ⟶ ¬ order e' e'')"
            using energy_Min_def by simp

          have "(∀e' ≠ e''. order e' e'' ⟶ ¬ winning_budget_len e' g)" 
          proof
            fix e'
            show " e' ≠ e'' ⟶ order e' e'' ⟶ ¬ winning_budget_len e' g"
            proof
              assume " e' ≠ e''"
              show "order e' e'' ⟶ ¬ winning_budget_len e' g"
              proof               
                assume "order e' e''"
                from ‹order e' e''› have "order e' e" using X energy_order ordering_def
                  by (metis (no_types, lifting) partial_preordering_def)
                show "¬ winning_budget_len e' g"
                proof
                  assume "winning_budget_len e' g"
                  hence "e'∈{e''. order e'' e ∧ winning_budget_len e'' g}" using ‹order e' e› by auto
                  hence "¬ order e' e''" using X ‹e' ≠ e''› by simp
                  thus "False" using ‹order e' e''› by simp
                qed
              qed
            qed
          qed
          hence E: "order e'' e ∧ winning_budget_len e'' g ∧ (∀e' ≠ e''. order e' e'' ⟶ ¬ winning_budget_len e' g)" using X
            by meson 
          hence "order e'' e ∧ minimal_winning_budget e'' g" using energy_Min_def by auto
          hence "∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e''=(the (inverse_application (the (weight g g')) e'))" 
            using min_winning_budget_is_inv_a X ‹g ∈ attacker› by simp
          hence "e'' ∈ {e. ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))}" by auto
          hence "e=e''" using ‹g ∈ attacker› X energy_Min_def E
            by (smt (verit, best) ‹e ∈ energy_Min {e. ∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g' ∧ e = the (inverse_application (the (weight g g')) e')}› mem_Collect_eq)
          thus "(∀e'. e' ≠ e ⟶ order e' e ⟶ ¬ winning_budget_len e' g)" using E by auto
        qed
        thus "minimal_winning_budget e g" using energy_Min_def by auto
      qed
    qed

    have min_winning_budget_is_minimal_inv_a: "⋀e g. g ∈ attacker ⟹ minimal_winning_budget e g ⟹ ∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e=(inv_upd (the (weight g g')) e')"
    proof-
      fix e g 
      assume A1: "g ∈ attacker" and A2: "minimal_winning_budget e g"
      show "∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e=(inv_upd (the (weight g g')) e')"
      proof-
        from A1 A2 have "winning_budget_len e g" using energy_Min_def by simp
        from A1 A2 have "∀e' ≠ e. order e' e ⟶ ¬ winning_budget_len e' g" using energy_Min_def
          using mem_Collect_eq by auto 
        hence "∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))"
          using min_winning_budget_is_inv_a A1 A2 ‹winning_budget_len e g› by auto
        from this obtain g' e' where G: "weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))" by auto
        hence "e' ∈ {e. winning_budget_len e g' ∧ order e e'}" using energy_order ordering_def
          using partial_preordering.refl by fastforce
        have "⋀e'. e' ∈ {e. winning_budget_len e g' ∧ order e e'} ⟹ e' ∈ energies" using winning_budget_len.simps by blast
        hence "energy_Min {e. winning_budget_len e g' ∧ order e e'} ≠ {}" using ‹e' ∈ {e. winning_budget_len e g' ∧ order e e'}› energy_Min_not_empty
          by (metis (mono_tags, lifting) empty_iff energy_order mem_Collect_eq ordering.eq_iff subsetI)
        hence "∃e''. e'' ∈ energy_Min {e. winning_budget_len e g' ∧ order e e'}" by auto
        from this obtain e'' where "e'' ∈ energy_Min {e. winning_budget_len e g' ∧ order e e'}" by auto
        have ‹minimal_winning_budget e'' g'› 
          unfolding energy_Min_def proof
          show "e'' ∈ a_win g' ∧ (∀e'∈a_win g'. e'' ≠ e' ⟶ ¬ e' e≤ e'')"
          proof
            have "winning_budget_len e'' g' ∧ order e'' e'"
              using ‹e'' ∈ energy_Min {e. winning_budget_len e g' ∧ order e e'}› energy_Min_def by auto
            thus "e'' ∈ a_win g'" by auto
            show "(∀e'∈a_win g'. e'' ≠ e' ⟶ ¬ e' e≤ e'')"
            proof
              fix e
              assume "e∈a_win g'"
              show "e'' ≠ e ⟶ ¬ e e≤ e''"
              proof
                assume "e'' ≠ e" 
                show "¬ e e≤ e''"
                proof
                  assume "e e≤ e''"
                  hence "e e≤ e'" using ‹winning_budget_len e'' g' ∧ order e'' e'› energy_order ordering_def
                    by (metis (no_types, lifting) partial_preordering_def) 
                  hence "winning_budget_len e g' ∧ order e e'" 
                    using ‹e∈a_win g'› by auto
                  hence "e ∈ {e. winning_budget_len e g' ∧ order e e'} ∧ e'' ≠ e ∧ e e≤ e''"
                    by (simp add: ‹e e≤ e''› ‹e'' ≠ e›)
                  thus "False"
                    using ‹e'' ∈ energy_Min {e. winning_budget_len e g' ∧ order e e'}› energy_Min_def
                    by auto 
                qed
              qed
            qed
          qed
        qed

        from ‹e'' ∈ energy_Min {e. winning_budget_len e g' ∧ order e e'}› have "e'' ∈ {e. winning_budget_len e g' ∧ order e e'}" using energy_Min_def by auto
        hence "winning_budget_len e'' g' ∧ order e'' e'" by simp

        have "order e'' e'" using ‹e'' ∈ energy_Min {e. winning_budget_len e g' ∧ order e e'}› energy_Min_def by auto
        hence "order (the (inverse_application (the (weight g g')) e'')) (the (inverse_application (the (weight g g')) e'))" 
          using inverse_monotonic
          using G inv_well_defined energy_order nonpos_eq_pos winning_bugget_len_is_wb
          using ‹winning_budget_len e'' g' ∧ e'' e≤ e'› by presburger
        hence "order (the (inverse_application (the (weight g g')) e'')) e" using G by auto
        hence "e=(the (inverse_application (the (weight g g')) e''))" using ‹winning_budget_len e'' g' ∧ order e'' e'› ‹∀e' ≠ e. order e' e ⟶ ¬ winning_budget_len e' g›
          by (metis A1 G attacker_inv_in_winning_budget)
        thus ?thesis using G ‹minimal_winning_budget e'' g'› by auto
      qed
    qed

    show "minimal_winning_budget e g = (e ∈ energy_Min {e. ∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e=(the (inverse_application (the (weight g g')) e'))})"
    proof
      assume "minimal_winning_budget e g"
      show "(e ∈ energy_Min {e. ∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e=(the (inverse_application (the (weight g g')) e'))})"
      proof-
        from ‹g ∈ attacker› have exist: "∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e = inv_upd (the (weight g g')) e'"
          using ‹minimal_winning_budget e g› min_winning_budget_is_minimal_inv_a by simp
        have "⋀e''. e'' e≤ e ∧ e ≠ e'' ⟹ e'' ∉ {e. ∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e=(the (inverse_application (the (weight g g')) e'))}"
        proof-
          fix e''
          show "e'' e≤ e ∧ e ≠ e'' ⟹ e'' ∉ {e. ∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e=(the (inverse_application (the (weight g g')) e'))}"
          proof-
            assume "e'' e≤ e ∧ e ≠ e'' "
            show "e'' ∉ {e. ∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e=(the (inverse_application (the (weight g g')) e'))}"
            proof
              assume "e'' ∈ {e. ∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e=(the (inverse_application (the (weight g g')) e'))}"
              hence "∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e''=(the (inverse_application (the (weight g g')) e'))"
                by auto
              from this obtain g' e' where EG: "weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e''=(the (inverse_application (the (weight g g')) e'))" by auto
              hence "winning_budget_len e' g'" using energy_Min_def by simp
              hence "winning_budget_len e'' g" using EG winning_budget_len.simps
                by (metis ‹g ∈ attacker› attacker_inv_in_winning_budget) 
              then show "False" using ‹e'' e≤ e ∧ e ≠ e''› ‹minimal_winning_budget e g› energy_Min_def by auto
            qed
          qed
        qed
        thus "(e ∈ energy_Min {e. ∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e=(the (inverse_application (the (weight g g')) e'))})" 
          using exist energy_Min_def
          by (smt (verit) mem_Collect_eq) 
      qed
    next
      assume emin: "(e ∈ energy_Min {e. ∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g' ∧ e=(the (inverse_application (the (weight g g')) e'))})"
      show "minimal_winning_budget e g"
      proof-
        from emin have "∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))" using energy_Min_def by auto
        hence  "∃g' e'. weight g g' ≠ None ∧ winning_budget_len e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))" using energy_Min_def
          by (metis (no_types, lifting) mem_Collect_eq)
        hence element_of: "e∈{e. ∃g' e'.
                   weight g g' ≠ None ∧
                   winning_budget_len e' g' ∧ e = inv_upd (the (weight g g')) e'}" by auto

        have "⋀e''. e'' e< e ⟹ e'' ∉ {e. ∃g' e'.
                   weight g g' ≠ None ∧
                   winning_budget_len e' g' ∧ e = inv_upd (the (weight g g')) e'}"
        proof
          fix e''
          assume "e'' e< e"
          assume "e'' ∈ {e. ∃g' e'.
                   weight g g' ≠ None ∧
                   winning_budget_len e' g' ∧ e = inv_upd (the (weight g g')) e'}"
          hence "∃g' e'.
                   weight g g' ≠ None ∧
                   winning_budget_len e' g' ∧ e'' = inv_upd (the (weight g g')) e'" by auto
          from this obtain g' e' where E'G': "weight g g' ≠ None ∧
                   winning_budget_len e' g' ∧ e'' = inv_upd (the (weight g g')) e'" by auto
          hence "e' ∈ {e. winning_budget_len e g'}" by simp
          hence "∃e_min. minimal_winning_budget e_min g' ∧ e_min e≤ e'" 
            using energy_Min_contains_smaller
            by (metis mem_Collect_eq nonpos_eq_pos subsetI winning_bugget_len_is_wb)
          from this obtain e_min where "minimal_winning_budget e_min g' ∧ e_min e≤ e'" by auto
          have "inv_upd (the (weight g g')) e_min e≤ inv_upd (the (weight g g')) e'" 
          proof(rule inverse_monotonic)
            show "weight g g' ≠ None"           
              using ‹weight g g' ≠ None ∧ winning_budget_len e' g' ∧ e'' = inv_upd (the (weight g g')) e'› by simp
            show "e_min e≤ e'" using ‹minimal_winning_budget e_min g' ∧ e_min e≤ e'›
              by auto
            hence "e_min ∈ energies" using winning_budget_len.simps
              by (metis (no_types, lifting) ‹minimal_winning_budget e_min g' ∧ e_min e≤ e'› energy_Min_def mem_Collect_eq)
            thus " inverse_application (the (weight g g')) e_min ≠ None"
              using inv_well_defined ‹weight g g' ≠ None› by auto
            show "e_min ∈ energies"
              by (simp add: ‹e_min ∈ energies›) 
          qed
          hence "inv_upd (the (weight g g')) e_min e< e" using ‹e'' e< e› E'G'
            using energy_order ordering_def
            by (metis (no_types, lifting) ordering.antisym partial_preordering.trans) 

          have "inv_upd (the (weight g g')) e_min ∈ {e. ∃g' e'. weight g g' ≠ None ∧ minimal_winning_budget e' g'  ∧ e=(the (inverse_application (the (weight g g')) e'))}" 
            using ‹minimal_winning_budget e_min g' ∧ e_min e≤ e'› E'G'
            by blast
          thus "False" using ‹inv_upd (the (weight g g')) e_min e< e› energy_Min_def emin
            by (smt (verit) mem_Collect_eq)    
        qed

        hence "e ∈ energy_Min
            {e. ∃g' e'.
                   weight g g' ≠ None ∧
                   winning_budget_len e' g' ∧ e = inv_upd (the (weight g g')) e'}" 
          using energy_Min_def element_of 
          by (smt (verit, ccfv_threshold) mem_Collect_eq)
        then show ?thesis using min_winning_budget_a_iff_energy_Min ‹g ∈ attacker› by simp
      qed
    qed
  qed


  have minimal_winning_budget_defender: "⋀g e. g ∉ attacker ⟹ minimal_winning_budget e g = (e∈ energy_Min {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})})"
  proof-
    fix g e
    assume "g ∉ attacker"
    have sup_inv_in_winning_budget: "⋀(strat:: 'position ⇒'energy) g. g∉attacker ⟹ ∀g'.  weight g g' ≠ None ⟶ strat g' ∈ {inv_upd (the (weight g g')) e | e. winning_budget_len e g' } ⟹ winning_budget_len (energy_sup {strat g'| g'. weight g g' ≠ None}) g"
    proof-
      fix strat g 
      assume A1: "g∉attacker" and "∀g'.  weight g g' ≠ None ⟶ strat g' ∈ {inv_upd (the (weight g g')) e | e. winning_budget_len e g' }"
      hence A2: " ⋀g'.  weight g g' ≠ None ⟹ strat g' ∈ {inv_upd (the (weight g g')) e | e. winning_budget_len e g' }"
        by simp
      show "winning_budget_len (energy_sup {strat g'| g'. weight g g' ≠ None}) g"
      proof (rule winning_budget_len.intros(1))
        have A: "(∀g'. weight g g' ≠ None ⟶
          application (the (weight g g')) (energy_sup {strat g' |g'. weight g g' ≠ None}) ≠ None ∧
          winning_budget_len (the (application (the (weight g g')) (energy_sup {strat g' |g'. weight g g' ≠ None}))) g') " 
        proof
          fix g'
          show "weight g g' ≠ None ⟶
          application (the (weight g g')) (energy_sup {strat g' |g'. weight g g' ≠ None}) ≠ None ∧
          winning_budget_len (the (application (the (weight g g')) (energy_sup {strat g' |g'. weight g g' ≠ None}))) g'"
          proof
            assume "weight g g' ≠ None"
            hence "strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. winning_budget_len e g' }" using A2 by simp
            hence "∃e. strat g' = the (inverse_application (the (weight g g')) e) ∧ winning_budget_len e g'" by blast
            from this obtain e where E: "strat g' = the (inverse_application (the (weight g g')) e) ∧ winning_budget_len e g'" by auto

            hence "e ∈ energies" using winning_budget_len.simps by blast
            hence "inverse_application (the (weight g g')) e ≠ None" using inv_well_defined  ‹weight g g' ≠ None› by simp

            have "{strat g' |g'. weight g g' ≠ None} ⊆ energies ∧ finite {strat g' |g'. weight g g' ≠ None}"
            proof
              show "{strat g' |g'. weight g g' ≠ None} ⊆ energies"
                by (smt (verit, best) A2 inv_well_defined mem_Collect_eq nonpos_eq_pos subsetI winning_bugget_len_is_wb)
              have "{strat g' |g'. weight g g' ≠ None} ⊆ {strat g' |g'. g' ∈ positions}" by auto
              thus "finite {strat g' |g'. weight g g' ≠ None}"
                using finite_positions
                using rev_finite_subset by fastforce
            qed
            hence leq: "order (strat g') (energy_sup {strat g' |g'. weight g g' ≠ None})" 
              using bounded_join_semilattice ‹weight g g' ≠ None›
              by (metis (mono_tags, lifting) mem_Collect_eq)

            show "application (the (weight g g')) (energy_sup {strat g' |g'. weight g g' ≠ None}) ≠ None ∧
            winning_budget_len (the (application (the (weight g g')) (energy_sup {strat g' |g'. weight g g' ≠ None}))) g'"
            proof
              have "application (the (weight g g')) (strat g') = application (the (weight g g')) (the (inverse_application (the (weight g g')) e))" using E
                by simp
              also have "... ≠ None" using ‹inverse_application (the (weight g g')) e ≠ None› inv_well_defined
                using ‹e ∈ energies› ‹weight g g' ≠ None› by presburger
              finally have "application (the (weight g g')) (strat g') ≠ None" .
              thus "application (the (weight g g')) (energy_sup {strat g' |g'. weight g g' ≠ None}) ≠ None" 
                using leq domain_upw_closed
                using ‹weight g g' ≠ None› by blast  

              have "order e (the (application (the (weight g g')) (strat g')))" using upd_inv_increasing 
                by (metis ‹application (the (weight g g')) (strat g') = application (the (weight g g')) (the (inverse_application (the (weight g g')) e))› ‹e ∈ energies› ‹weight g g' ≠ None›) 
              hence W: "winning_budget_len (the (application (the (weight g g')) (strat g'))) g'" using E upwards_closure_wb_len
                by blast
              have "order (the (application (the (weight g g')) (strat g'))) (the (application (the (weight g g')) (energy_sup {strat g' |g'. weight g g' ≠ None})))" 
                using updates_monotonic
                using ‹apply_w g g' (strat g') ≠ None› ‹weight g g' ≠ None› ‹{strat g' |g'. weight g g' ≠ None} ⊆ energies ∧ finite {strat g' |g'. weight g g' ≠ None}› leq by blast 
              thus "winning_budget_len (the (application (the (weight g g')) (energy_sup {strat g' |g'. weight g g' ≠ None}))) g'" 
                using W upwards_closure_wb_len by blast
            qed
          qed
        qed

        have "(energy_sup {strat g' |g'. weight g g' ≠ None}) ∈ energies"
        proof-
          have "{strat g' |g'. weight g g' ≠ None} ⊆ {strat g' |g'. g' ∈ positions}" by auto
          hence fin: "finite {strat g' |g'. weight g g' ≠ None}" using finite_positions
            using rev_finite_subset by fastforce 
          have "{strat g' |g'. weight g g' ≠ None} ⊆ energies" 
            using A2
            by (smt (verit) inv_well_defined mem_Collect_eq subsetI winning_budget_len.cases) 
          thus ?thesis using bounded_join_semilattice fin by auto
        qed
        thus "(energy_sup {strat g' |g'. weight g g' ≠ None}) ∈ energies ∧ g ∉ attacker ∧
          (∀g'. weight g g' ≠ None ⟶
          application (the (weight g g')) (energy_sup {strat g' |g'. weight g g' ≠ None}) ≠ None ∧
          winning_budget_len (the (application (the (weight g g')) (energy_sup {strat g' |g'. weight g g' ≠ None}))) g') "
          using A1 A by auto
      qed
    qed

    have min_winning_budget_is_inv_d: "⋀e g. g∉attacker ⟹ minimal_winning_budget e g ⟹ ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {inv_upd (the (weight g g')) e | e. winning_budget_len e g'})
                  ∧ e = (energy_sup {strat g'| g'. weight g g' ≠ None})"
    proof-
      fix e g 
      assume A1: "g∉attacker" and A2: " minimal_winning_budget e g"
      show "∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {inv_upd (the (weight g g')) e | e. winning_budget_len e g'})
                  ∧ e = (energy_sup {strat g'| g'. weight g g' ≠ None})"
      proof-
        from A2 have "e ∈ energies" using winning_budget_len.simps energy_Min_def
          by (metis (no_types, lifting) mem_Collect_eq) 
        from A1 A2 have W: "(∀g'. weight g g' ≠ None ⟶
                  application (the (weight g g')) e ≠ None ∧
                  winning_budget_len (the (application (the (weight g g')) e)) g')" using winning_budget_len.simps energy_Min_def
          by (metis (no_types, lifting) mem_Collect_eq) 

        define strat where S: "∀g'.  strat g' = the ((inverse_application (the (weight g g'))) (the (application (the (weight g g')) e)))"
        have A: "(∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'})" 
        proof
          fix g'
          show "weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'}" 
          proof
            assume "weight g g' ≠ None"
            hence "winning_budget_len (the (application (the (weight g g')) e)) g'" using W by auto
            thus "strat g' ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'}" using S by blast
          qed
        qed
        hence W: "winning_budget_len (energy_sup {strat g' |g'. weight g g' ≠ None}) g" using sup_inv_in_winning_budget A1 by simp
        have "⋀g'. weight g g' ≠ None ⟹ order (strat g') e" 
        proof-
          fix g'
          assume "weight g g' ≠ None"
          hence "application (the (weight g g')) e ≠ None" using W
            using A1 A2 winning_budget_len.cases energy_Min_def
            by (metis (mono_tags, lifting) mem_Collect_eq) 
          from ‹weight g g' ≠ None› have "strat g' = the ((inverse_application (the (weight g g'))) (the (application (the (weight g g')) e)))" using S by auto
          thus "order (strat g') e" using inv_upd_decreasing  ‹application (the (weight g g')) e ≠ None›
            using ‹e ∈ energies› ‹weight g g' ≠ None› by presburger
        qed

        have BJSL: "finite {strat g' |g'. weight g g' ≠ None} ∧ {strat g' |g'. weight g g' ≠ None}⊆ energies"
        proof
          have "{strat g' |g'. weight g g' ≠ None} ⊆ {strat g' |g'. g'∈positions}"
            by auto
          thus "finite {strat g' |g'. weight g g' ≠ None}"
            using finite_positions
            using rev_finite_subset by fastforce 
          show "{strat g' |g'. weight g g' ≠ None}⊆ energies" 
          proof
            fix x 
            assume "x ∈ {strat g' |g'. weight g g' ≠ None}"
            from this obtain g' where "x = strat g'" and "weight g g' ≠ None" by auto
            hence "x ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'}" using A
              by simp 
            thus "x ∈ energies"
              using ‹weight g g' ≠ None› inv_well_defined nonpos_eq_pos winning_bugget_len_is_wb by auto 
          qed
        qed
        hence "(∀s. s ∈ {strat g' |g'. weight g g' ≠ None} ⟶ s e≤ e) ⟶ energy_sup {strat g' |g'. weight g g' ≠ None} e≤ e"
          using bounded_join_semilattice
          by (meson ‹e ∈ energies›)
        hence "order (energy_sup {strat g' |g'. weight g g' ≠ None}) e" 
          using ‹⋀g'. weight g g' ≠ None ⟹ order (strat g') e›
          by blast 
        hence "e = energy_sup {strat g' |g'. weight g g' ≠ None}" using W A1 A2 energy_Min_def
          by force 
        thus ?thesis using A by blast
      qed
    qed


    have  min_winning_budget_d_iff_energy_Min: "⋀e g. g∉attacker ⟹ e ∈ energies ⟹ ((e∈ energy_Min {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {inv_upd (the (weight g g')) e | e. winning_budget_len e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})})
        ⟷ minimal_winning_budget e g)"
    proof-
      fix e g
      show "g ∉ attacker ⟹
           e ∈ energies ⟹
           (e ∈ energy_Min
                  {e''.
                   ∃strat.
                      (∀g'. weight g g' ≠ None ⟶
                            strat g'
                            ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}) ∧
                      e'' = energy_sup {strat g' |g'. weight g g' ≠ None}}) =
           minimal_winning_budget e g"
      proof-
        assume A1: "g ∉ attacker" and A2: "e ∈ energies"
        show "(e ∈ energy_Min
                  {e''.
                   ∃strat.
                      (∀g'. weight g g' ≠ None ⟶
                            strat g'
                            ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}) ∧
                      e'' = energy_sup {strat g' |g'. weight g g' ≠ None}}) =
           minimal_winning_budget e g"
        proof
          assume assumption: "e∈ energy_Min {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. winning_budget_len e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}"
          show "minimal_winning_budget e g" 
            unfolding energy_Min_def 
          proof
            show "e ∈ {e. winning_budget_len e g} ∧ (∀e'∈{e. winning_budget_len e g}. e ≠ e' ⟶ ¬ e' e≤ e)"
            proof
              show "e ∈ {e. winning_budget_len e g}" 
              proof
                from A1 A2 assumption have "∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. winning_budget_len e g'})
                  ∧ e = (energy_sup {strat g'| g'. weight g g' ≠ None})" 
                  using energy_Min_def by simp
                thus "winning_budget_len e g" using sup_inv_in_winning_budget A1 A2 by blast
              qed
              hence W: "winning_budget_len e g" by simp
              hence "e ∈ energies" using winning_budget_len.simps by blast
              hence "e∈ {e''. order e'' e ∧ winning_budget_len e'' g ∧ e'' ∈ energies}" using W energy_order ordering_def ‹g ∉ attacker›
                using energy_wqo reflp_onD wqo_on_imp_reflp_on by fastforce
              hence "{e''. order e'' e ∧ winning_budget_len e'' g ∧ e'' ∈ energies} ≠ {}" by auto
              hence "energy_Min {e''. order e'' e ∧ winning_budget_len e'' g ∧ e'' ∈ energies} ≠ {}" using energy_Min_not_empty
                by (metis (no_types, lifting) mem_Collect_eq subsetI)
              hence "∃e''. e'' ∈ energy_Min {e''. order e'' e ∧ winning_budget_len e'' g ∧ e'' ∈ energies}" by auto
              from this obtain e'' where "e'' ∈ energy_Min {e''. order e'' e ∧ winning_budget_len e'' g ∧ e'' ∈ energies}" by auto
              hence X: "order e'' e ∧ winning_budget_len e'' g ∧ e'' ∈ energies 
                      ∧ ( ∀e'. e'∈{e''. order e'' e ∧ winning_budget_len e'' g ∧ e'' ∈ energies }⟶ e'' ≠ e' ⟶ ¬ order e' e'')" using energy_Min_def
                by simp
              have "(∀e' ≠ e''. order e' e'' ⟶ ¬ winning_budget_len e' g)" 
              proof
                fix e'
                show " e' ≠ e'' ⟶ order e' e'' ⟶ ¬ winning_budget_len e' g"
                proof
                  assume " e' ≠ e''"
                  show "order e' e'' ⟶ ¬ winning_budget_len e' g"
                  proof
                    assume " order e' e''"
                    from ‹order e' e''› have "order e' e" using X energy_order ordering_def
                      by (metis (no_types, lifting) partial_preordering.trans)
                    show "¬ winning_budget_len e' g"
                    proof(cases "e' ∈ energies")
                      case True
                      show ?thesis
                      proof
                        assume "winning_budget_len e' g"
                        hence "e'∈{e''. order e'' e ∧ winning_budget_len e'' g ∧ e'' ∈ energies}" using ‹e' ∈ energies› ‹order e' e› by auto
                        hence "¬ order e' e''" using X ‹e' ≠ e''› by simp
                        thus "False" using ‹order e' e''› by simp
                      qed
                    next
                      case False
                      then show ?thesis
                        by (simp add: nonpos_eq_pos winning_bugget_len_is_wb)
                    qed                    
                  qed
                qed
              qed
              hence "order e'' e ∧ winning_budget_len e'' g ∧ (∀e' ≠ e''. order e' e'' ⟶ ¬ winning_budget_len e' g)" using X
                by meson
              hence E: "order e'' e ∧ minimal_winning_budget e'' g" using energy_Min_def
                by (smt (verit) mem_Collect_eq) 
              hence "∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. winning_budget_len e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})" 
                using min_winning_budget_is_inv_d 
                by (simp add: X A1) 
              hence "e=e''" using assumption X energy_Min_def by auto 
              thus "(∀e'∈{e. winning_budget_len e g}. e ≠ e' ⟶ ¬ e' e≤ e)" using E
                using ‹∀e'. e' ≠ e'' ⟶ e' e≤ e'' ⟶ ¬ winning_budget_len e' g› by fastforce
            qed
          qed
        next
          assume assumption: "minimal_winning_budget e g" 
          show "e∈ energy_Min {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. winning_budget_len e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}"
            unfolding energy_Min_def 
          proof
            from assumption have "e ∈ energies" using winning_budget_len.simps energy_Min_def
              using A2 by blast
            show "e ∈ {e''.
          ∃strat.
             (∀g'. weight g g' ≠ None ⟶
                   strat g' ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'}) ∧
             e'' = energy_sup {strat g' |g'. weight g g' ≠ None}} ∧
          (∀e'∈{e''.
           ∃strat.
              (∀g'. weight g g' ≠ None ⟶
                    strat g' ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'}) ∧
              e'' = energy_sup {strat g' |g'. weight g g' ≠ None}}.
          e ≠ e' ⟶ ¬ order e' e)"
            proof
              from A1 A2 assumption have "∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. winning_budget_len e g'})
                  ∧ e = (energy_sup {strat g'| g'. weight g g' ≠ None})" using min_winning_budget_is_inv_d by simp
              thus "e ∈ {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. winning_budget_len e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}" by auto
              show " ∀e'∈{e''.
          ∃strat.
             (∀g'. weight g g' ≠ None ⟶
                   strat g' ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'}) ∧
             e'' = energy_sup {strat g' |g'. weight g g' ≠ None}}.
       e ≠ e' ⟶ ¬ order e' e"
              proof
                fix e'
                assume "e' ∈ {e''.
                ∃strat.
                   (∀g'. weight g g' ≠ None ⟶
                         strat g' ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'}) ∧
                   e'' = energy_sup {strat g' |g'. weight g g' ≠ None}}"
                hence "∃strat.
                   (∀g'. weight g g' ≠ None ⟶
                         strat g' ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'}) ∧
                   e' = energy_sup {strat g' |g'. weight g g' ≠ None}" by auto
                from this obtain strat where S: "(∀g'. weight g g' ≠ None ⟶
                         strat g' ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'}) ∧
                   e' = energy_sup {strat g' |g'. weight g g' ≠ None}" by auto
                have "finite {strat g' |g'. weight g g' ≠ None} ∧ {strat g' |g'. weight g g' ≠ None} ⊆ energies"
                proof
                  have "{strat g' |g'. weight g g' ≠ None} ⊆ {strat g' |g'. g' ∈ positions}" by auto
                  thus "finite {strat g' |g'. weight g g' ≠ None}" using finite_positions
                    using rev_finite_subset by fastforce 
                  show "{strat g' |g'. weight g g' ≠ None} ⊆ energies"
                  proof
                    fix x 
                    assume "x ∈ {strat g' |g'. weight g g' ≠ None}"
                    thus "x ∈ energies" using S
                      by (smt (verit, ccfv_threshold) inv_well_defined mem_Collect_eq nonpos_eq_pos winning_bugget_len_is_wb)
                  qed
                qed
                hence "e' ∈ energies" using bounded_join_semilattice S 
                  by (meson empty_iff empty_subsetI finite.emptyI upward_closed_energies)   
                show "e ≠ e' ⟶ ¬ order e' e "
                proof
                  assume "e ≠ e'"
                  have "(∀g'. weight g g' ≠ None ⟶
            application (the (weight g g')) e' ≠ None ∧
            winning_budget_len (the (application (the (weight g g')) e')) g')" 
                  proof
                    fix g'
                    show "weight g g' ≠ None ⟶
              application (the (weight g g')) e' ≠ None ∧ winning_budget_len (the (application (the (weight g g')) e')) g' "
                    proof
                      assume "weight g g' ≠ None"
                      hence "strat g' ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'}" using S by auto
                      hence "∃e''. strat g'= the (inverse_application (the (weight g g')) e'') ∧ winning_budget_len e'' g'" by auto
                      from this obtain e'' where E: "strat g'= the (inverse_application (the (weight g g')) e'') ∧ winning_budget_len e'' g'" by auto
                      hence "e'' ∈ energies" using winning_budget_len.simps by blast
                      show "application (the (weight g g')) e' ≠ None ∧ winning_budget_len (the (application (the (weight g g')) e')) g' "
                      proof
                        have "{strat g' |g'. weight g g' ≠ None} ⊆ energies ∧finite {strat g' |g'. weight g g' ≠ None}"
                        proof
                          show "{strat g' |g'. weight g g' ≠ None} ⊆ energies" using S
                            using ‹finite {strat g' |g'. weight g g' ≠ None} ∧ {strat g' |g'. weight g g' ≠ None} ⊆ energies› by blast
                          have "{strat g' |g'. weight g g' ≠ None} ⊆ {strat g' |g'. g' ∈ positions}" by auto
                          thus "finite {strat g' |g'. weight g g' ≠ None}"
                            using finite_positions
                            using rev_finite_subset by fastforce
                        qed
                        hence "order (strat g') e'" using S bounded_join_semilattice ‹weight g g' ≠ None›
                          by (metis (mono_tags, lifting) mem_Collect_eq)
                        have "application (the (weight g g')) (strat g') ≠ None" using E inv_well_defined inv_well_defined ‹e'' ∈ energies›
                          by (metis ‹weight g g' ≠ None› )
                        thus "application (the (weight g g')) e' ≠ None" using domain_upw_closed ‹order (strat g') e'›
                          using ‹weight g g' ≠ None› by blast
                        have "order e'' (the (application (the (weight g g')) (strat g')))" using E upd_inv_increasing
                          using ‹e'' ∈ energies› ‹weight g g' ≠ None›  by metis
                        hence W: "winning_budget_len (the (application (the (weight g g')) (strat g'))) g'" using upwards_closure_wb_len
                          using E by blast
                        from ‹order (strat g') e'› have "order (the (application (the (weight g g')) (strat g')))  (the (application (the (weight g g')) e'))" 
                          using updates_monotonic  ‹application (the (weight g g')) (strat g') ≠ None›
                          by (metis E ‹e'' ∈ energies› ‹weight g g' ≠ None› inv_well_defined)
                        thus "winning_budget_len (the (application (the (weight g g')) e')) g' " using upwards_closure_wb_len W
                          by blast 
                      qed
                    qed
                  qed
                  hence "winning_budget_len e' g" using winning_budget_len.intros(1) A1 ‹e' ∈ energies›
                    by blast
                  thus "¬ order e' e " using assumption ‹e ≠ e'› energy_Min_def by auto
                qed
              qed
            qed
          qed
        qed
      qed
    qed

    have  min_winning_budget_is_minimal_inv_d: "⋀e g. g∉attacker ⟹ minimal_winning_budget e g ⟹ ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e = (energy_sup {strat g'| g'. weight g g' ≠ None})"
    proof-
      fix e g
      assume A1: "g∉attacker" and A2: "minimal_winning_budget e g" 
      show "∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e = (energy_sup {strat g'| g'. weight g g' ≠ None})"
      proof-
        from A1 A2 have "winning_budget_len e g" using energy_Min_def by simp
        from A1 A2 have "∀e' ≠ e. order e' e ⟶ ¬ winning_budget_len e' g" using energy_Min_def
          using mem_Collect_eq by auto 

        hence "e∈ energy_Min {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. winning_budget_len e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}" 
          using ‹winning_budget_len e g› A1 A2 min_winning_budget_d_iff_energy_Min
          by (meson winning_budget_len.cases)
        hence " ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. winning_budget_len e g'})
                  ∧ e = (energy_sup {strat g'| g'. weight g g' ≠ None})" using energy_Min_def by auto

        from this obtain strat where Strat: "(∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. winning_budget_len e g'})
                  ∧ e = (energy_sup {strat g'| g'. weight g g' ≠ None})" by auto
        define strat_e where "strat_e ≡ λg'.(SOME e. strat g' = the (inverse_application (the (weight g g')) e) ∧ winning_budget_len e g')"
  
        have Strat_E: "⋀g'. weight g g' ≠ None ⟹ strat g' = the (inverse_application (the (weight g g')) (strat_e g')) ∧ winning_budget_len (strat_e g') g'"
        proof-
          fix g'
          have Strat_E: "strat_e g' = (SOME e. strat g' = the (inverse_application (the (weight g g')) e) ∧ winning_budget_len e g')" using strat_e_def by simp 
          assume "weight g g' ≠ None"
          hence "strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. winning_budget_len e g'}" using Strat by simp
          hence "∃e. strat g' = the (inverse_application (the (weight g g')) e) ∧ winning_budget_len e g'" by auto
          thus "strat g' = the (inverse_application (the (weight g g')) (strat_e g')) ∧ winning_budget_len (strat_e g') g'" 
            using Strat_E by (smt (verit, del_insts) some_eq_ex) 
        qed

        have exists: "⋀g'. weight g g' ≠ None ⟹ ∃e. e∈ energy_Min {e. winning_budget_len e g' ∧ order e (strat_e g')}"
        proof-
          fix g'
          assume "weight g g' ≠ None "
          hence notempty: "strat_e g' ∈ {e. winning_budget_len e g' ∧ order e (strat_e g')}" using Strat_E energy_order ordering_def
            using partial_preordering.refl by fastforce
          have "∀e ∈ {e. winning_budget_len e g' ∧ order e (strat_e g')}. e ∈ energies"
            using winning_budget_len.cases by auto 
          hence "{} ≠ energy_Min {e. winning_budget_len e g' ∧ order e (strat_e g')}"
            using energy_Min_not_empty notempty
            by (metis (no_types, lifting) empty_iff subsetI)
          thus "∃e. e∈ energy_Min {e. winning_budget_len e g' ∧ order e (strat_e g')}" by auto
        qed

        define strat' where "strat' ≡ λg'. the (inverse_application (the (weight g g')) (SOME e. e∈ energy_Min {e. winning_budget_len e g' ∧ order e (strat_e g')}))"
 
        have "(∀g'. weight g g' ≠ None ⟶ strat' g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e = (energy_sup {strat' g'| g'. weight g g' ≠ None})"
        proof
          show win: "∀g'. weight g g' ≠ None ⟶ strat' g' ∈ {the (inverse_application (the (weight g g')) e) |e. minimal_winning_budget e g'}"
          proof
            fix g'
            show "weight g g' ≠ None ⟶ strat' g' ∈ {the (inverse_application (the (weight g g')) e) |e. minimal_winning_budget e g'}"
            proof
              assume "weight g g' ≠ None"
              hence "strat' g' = the (inverse_application (the (weight g g')) (SOME e. e∈ energy_Min {e. winning_budget_len e g' ∧ order e (strat_e g')}))"
                using strat'_def by auto
              hence  "∃e. e∈ energy_Min {e. winning_budget_len e g' ∧ order e (strat_e g')} ∧ strat' g' = the (inverse_application (the (weight g g')) e)"
                using exists ‹weight g g' ≠ None› some_eq_ex
                by (metis (mono_tags)) 
              from this obtain e where E: "e∈ energy_Min {e. winning_budget_len e g' ∧ order e (strat_e g')} ∧ strat' g' = the (inverse_application (the (weight g g')) e)" by auto
              have "minimal_winning_budget e g'"
              
                unfolding energy_Min_def
              proof
                show "e ∈ a_win g' ∧ (∀e'∈a_win g'. e ≠ e' ⟶ ¬ e' e≤ e)"
                proof
                  show "e ∈ a_win g'"
                    using E energy_Min_def
                    by simp
                  show "(∀e'∈a_win g'. e ≠ e' ⟶ ¬ e' e≤ e)"
                  proof
                    fix e'
                    show "e' ∈ a_win g' ⟹ e ≠ e' ⟶ ¬ e' e≤ e"
                    proof
                      assume "e' ∈ a_win g'" and "e ≠ e'" 
                      hence "winning_budget_len e' g'" by simp
                      show "¬ e' e≤ e"
                      proof
                        assume "e' e≤ e"
                        have "order e (strat_e g')" using E energy_Min_def by auto
                        hence "order e' (strat_e g')" using ‹e' e≤ e› energy_order ordering_def
                          by (metis (no_types, lifting) partial_preordering_def) 
                        hence "e'∈{e. winning_budget_len e g' ∧ order e (strat_e g')}" using ‹winning_budget_len e' g'› by auto
                        thus "False" using E ‹e ≠ e'› ‹e' e≤ e› energy_Min_def
                          by fastforce
                      qed
                    qed
                  qed
                qed
              qed
              thus "strat' g' ∈ {the (inverse_application (the (weight g g')) e) |e. minimal_winning_budget e g'}" using E
                by blast 
            qed
          qed

          have "(⋀g'. weight g g' ≠ None ⟹
           strat' g' ∈ {the (inverse_application (the (weight g g')) e) |e. winning_budget_len e g'})"
            using win energy_Min_def
            by (smt (verit, del_insts) mem_Collect_eq) 
          hence win: "winning_budget_len (energy_sup {strat' g' |g'. weight g g' ≠ None}) g" 
            using sup_inv_in_winning_budget A1 A2 by simp

          have "order (energy_sup {strat' g' |g'. weight g g' ≠ None}) (energy_sup {strat g'| g'. weight g g' ≠ None})"
          proof(cases " {g'. weight g g' ≠ None} = {}")
            case True
            then show ?thesis using bounded_join_semilattice
              by auto 
          next
            case False
            show ?thesis 
            proof(rule energy_sup_leq_energy_sup)
              show "{strat' g' |g'. weight g g' ≠ None} ≠ {}" using False by simp

              have A: "⋀a. a ∈ {strat' g' |g'. weight g g' ≠ None} ⟹ ∃b∈{strat g' |g'. weight g g' ≠ None}. order a b ∧ a ∈ energies" 
              proof-
                fix a 
                assume "a ∈{strat' g' |g'. weight g g' ≠ None}"
                hence "∃g'. a = strat' g' ∧ weight g g' ≠ None" by auto
                from this obtain g' where "a = strat' g' ∧ weight g g' ≠ None" by auto

                have "(strat' g') = (the (inverse_application (the (weight g g'))
                  (SOME e. e ∈ energy_Min {e. winning_budget_len e g' ∧ order e (strat_e g')})))" using strat'_def by auto
                hence  "∃e. e∈ energy_Min {e. winning_budget_len e g' ∧ order e (strat_e g')} ∧ strat' g' = the (inverse_application (the (weight g g')) e)"
                  using exists ‹a = strat' g' ∧ weight g g' ≠ None› some_eq_ex
                  by (metis (mono_tags)) 
                from this obtain e where E: "e∈ energy_Min {e. winning_budget_len e g' ∧ order e (strat_e g')} ∧ strat' g' = the (inverse_application (the (weight g g')) e)" by auto
                hence "order e (strat_e g')" using energy_Min_def by auto

                hence "a ∈ energies " using ‹a = strat' g' ∧ weight g g' ≠ None› energy_Min_def
                  by (metis (no_types, lifting) E inv_well_defined mem_Collect_eq nonpos_eq_pos winning_bugget_len_is_wb)

                have leq: "order (the (inverse_application (the (weight g g')) e)) (the (inverse_application (the (weight g g')) (strat_e g')))" 
                proof(rule inverse_monotonic)
                  show "order e (strat_e g')" using ‹order e (strat_e g')›.
                  show "weight g g' ≠ None" using ‹a = strat' g' ∧ weight g g' ≠ None› by simp
                  from E have "e∈ {e. winning_budget_len e g' ∧ order e (strat_e g')}" using energy_Min_def
                    by auto 
                  hence "winning_budget_len e g'"
                    by simp 
                  thus "e ∈ energies"
                    using winning_budget_len.simps
                    by blast 
                  thus "inverse_application (the (weight g g')) e ≠ None"
                    using inv_well_defined ‹weight g g' ≠ None›
                    by simp
                qed
                have "the (inverse_application (the (weight g g')) (strat_e g')) = strat g'" using Strat_E ‹a = strat' g' ∧ weight g g' ≠ None› by auto
                hence "order (strat' g') (strat g')" using leq E by simp
                hence "∃b∈{strat g' |g'. weight g g' ≠ None}. order a b" using ‹a = strat' g' ∧ weight g g' ≠ None› by auto
                thus "∃b∈{strat g' |g'. weight g g' ≠ None}. order a b ∧ a ∈ energies" using ‹a ∈ energies› by simp
              qed
              thus "⋀a. a ∈ {strat' g' |g'. weight g g' ≠ None} ⟹ ∃b∈{strat g' |g'. weight g g' ≠ None}. order a b" by simp
              show "⋀a. a ∈ {strat' g' |g'. weight g g' ≠ None} ⟹ a ∈ energies " using A by simp
              
              have "{strat' g' |g'. weight g g' ≠ None} ⊆ {strat' g' |g'. g' ∈ positions}" by auto
              thus "finite {strat' g' |g'. weight g g' ≠ None}" using finite_positions rev_finite_subset by fastforce
              have "{strat g' |g'. weight g g' ≠ None} ⊆ {strat g' |g'. g' ∈ positions}" by auto
              thus "finite {strat g' |g'. weight g g' ≠ None}" using finite_positions rev_finite_subset by fastforce
              show "{strat g' |g'. weight g g' ≠ None} ⊆ energies"
                by (smt (verit) Strat_E inv_well_defined mem_Collect_eq subsetI winning_budget_len.simps) 
            qed
          qed
          thus "e = energy_sup {strat' g' |g'. weight g g' ≠ None}" using ‹g ∉ attacker› Strat win 
            by (metis (no_types, lifting) ‹∀e'. e' ≠ e ⟶ order e' e ⟶ ¬ winning_budget_len e' g›)
        qed
        thus ?thesis by blast
      qed
    qed

    show "minimal_winning_budget e g =
           (e ∈ energy_Min
                  {e''.
                   ∃strat.
                      (∀g'. weight g g' ≠ None ⟶
                            strat g'
                            ∈ {inv_upd (the (weight g g')) e |e. minimal_winning_budget e g'}) ∧
                      e'' = energy_sup {strat g' |g'. weight g g' ≠ None}})"
    proof
      assume "minimal_winning_budget e g"
      hence exist: "∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e= (energy_sup {strat g'| g'. weight g g' ≠ None})" 
        using min_winning_budget_is_minimal_inv_d ‹g ∉ attacker› by simp
      have "⋀e''. e'' e< e ⟹ ¬ e'' ∈ {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}"
      proof-
        fix e''
        show "e'' e< e ⟹ ¬ e'' ∈ {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}"
        proof-
          assume "e'' e< e"
          show "¬ e'' ∈ {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}"
          proof
            assume "e'' ∈ {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}"
            hence " ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})" by auto
            from this obtain strat where E'': "(∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})" by auto
            hence "⋀g'. weight g g' ≠ None ⟹
           strat g' ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}" using energy_Min_def
              by (smt (verit, del_insts) mem_Collect_eq) 
            hence "winning_budget_len (energy_sup {strat g' |g'. weight g g' ≠ None}) g" using sup_inv_in_winning_budget ‹g ∉ attacker› by simp
            hence "winning_budget_len e'' g" using E'' by simp
            thus "False" using ‹e'' e< e› ‹minimal_winning_budget e g› energy_Min_def by auto
          qed
        qed
      qed
      thus "e∈ energy_Min {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}"
        using exist energy_Min_def by (smt (verit) mem_Collect_eq)
    next 
      assume A: "(e∈ energy_Min {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})})"
    
      hence emin: "e∈ energy_Min {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}" using A by simp
      hence "∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e = (energy_sup {strat g'| g'. weight g g' ≠ None})" using energy_Min_def by auto
      hence "∃strat.
                (∀g'. weight g g' ≠ None ⟶
                      strat g' ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}) ∧
                e = energy_sup {strat g' |g'. weight g g' ≠ None}" using energy_Min_def
        by (smt (verit, ccfv_threshold) mem_Collect_eq) 
      hence element_of: "e ∈ {e''.
             ∃strat.
                (∀g'. weight g g' ≠ None ⟶
                      strat g' ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}) ∧
                e'' = energy_sup {strat g' |g'. weight g g' ≠ None}}" by auto
      hence "e ∈ energies"
        using ‹g ∉ attacker› sup_inv_in_winning_budget winning_budget_len.simps by blast

      have "⋀e'. e' e< e ⟹ e' ∉ {e''.
             ∃strat.
                (∀g'. weight g g' ≠ None ⟶
                      strat g' ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}) ∧
                e'' = energy_sup {strat g' |g'. weight g g' ≠ None}}"
      proof
        fix e'
        assume "e' e< e"
        assume A: "e' ∈ {e''. ∃strat.
                (∀g'. weight g g' ≠ None ⟶
                      strat g' ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}) ∧
                e'' = energy_sup {strat g' |g'. weight g g' ≠ None}}"
        hence "∃strat.
                (∀g'. weight g g' ≠ None ⟶
                      strat g' ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}) ∧
                e' = energy_sup {strat g' |g'. weight g g' ≠ None}" by auto
        from this obtain strat where Strat: "(∀g'. weight g g' ≠ None ⟶
                      strat g' ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}) ∧
                e' = energy_sup {strat g' |g'. weight g g' ≠ None}" by auto
        hence "e' ∈ energies" 
        proof-
          have "{strat g' |g'. weight g g' ≠ None} ⊆ {strat g' |g'. g' ∈ positions}" by auto
          hence fin: "finite {strat g' |g'. weight g g' ≠ None}" 
            using finite_positions
            using rev_finite_subset by fastforce 
          have "{strat g' |g'. weight g g' ≠ None} ⊆ energies" using Strat
            by (smt (verit, best) inv_well_defined mem_Collect_eq nonpos_eq_pos subsetI winning_bugget_len_is_wb) 
          thus ?thesis using bounded_join_semilattice fin Strat
            by auto 
        qed

        define the_e where "the_e ≡ λg'. (SOME x. strat g' = inv_upd (the (weight g g')) x ∧ winning_budget_len x g')"

        define strat' where "strat' ≡ λg'. (SOME x. x ∈ {inv_upd (the (weight g g')) x| 
                                                        x. (minimal_winning_budget x g' ∧ x e≤ the_e g')})"

        have some_not_empty: "⋀g'. weight g g' ≠ None ⟹ {inv_upd (the (weight g g')) x|x. (minimal_winning_budget x g' ∧ x e≤ the_e g')} ≠ {}"
        proof-
          fix g'
          assume "weight g g' ≠ None"
          hence "strat g' ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}" using Strat by auto
          hence "∃e. strat g' = inv_upd (the (weight g g')) e ∧ winning_budget_len e g'" by auto
          hence "strat g' = inv_upd (the (weight g g')) (the_e g') ∧ winning_budget_len (the_e g') g'" using the_e_def some_eq_ex
            by (metis (mono_tags, lifting)) 
          hence "the_e g' ∈ {x.  winning_budget_len x g'}" by auto
          hence "∃x.  (minimal_winning_budget x g' ∧ x e≤ the_e g')" using energy_Min_contains_smaller ‹the_e g' ∈ {x.  winning_budget_len x g'}›
            by (metis mem_Collect_eq nonpos_eq_pos subsetI winning_bugget_len_is_wb)
          hence "{x. (minimal_winning_budget x g' ∧ x e≤ the_e g')} ≠ {}" by auto
          thus "{inv_upd (the (weight g g')) x|x. (minimal_winning_budget x g' ∧ x e≤ the_e g')} ≠ {}"
            by auto
        qed
      
        hence len: "⋀a. a ∈ {strat' g' |g'. weight g g' ≠ None} ⟹ a ∈ energies" 
        proof-
          fix a
          assume "a ∈ {strat' g' |g'. weight g g' ≠ None}"
          hence "∃ g'. a= strat' g' ∧ weight g g' ≠ None" by auto
          from this obtain g' where "a= strat' g' ∧ weight g g' ≠ None" by auto
          hence some_not_empty: " {inv_upd (the (weight g g')) x|x. (minimal_winning_budget x g' ∧ x e≤ the_e g')} ≠ {}"
            using some_not_empty by blast

          have "strat' g' = (SOME x. x ∈ {inv_upd (the (weight g g')) x| 
                                                        x. (minimal_winning_budget x g' ∧ x e≤ the_e g')})" 
            using strat'_def by auto
          hence "strat' g' ∈ {inv_upd (the (weight g g')) x| x. (minimal_winning_budget x g' ∧ x e≤ the_e g')}"
            using some_not_empty some_in_eq
            by (smt (verit, ccfv_SIG) Eps_cong) 
          hence "∃x. strat' g' = inv_upd (the (weight g g')) x ∧  minimal_winning_budget x g' ∧ x e≤ the_e g'"
            by simp
          from this obtain x where X: "strat' g' = inv_upd (the (weight g g')) x ∧  minimal_winning_budget x g' ∧ x e≤ the_e g'" by auto
          hence "winning_budget_len x g'" using energy_Min_def by simp
          hence "x ∈ energies" using winning_budget_len.simps
            by blast 
          have "a=inv_upd (the (weight g g')) x" using X ‹a= strat' g' ∧ weight g g' ≠ None› by simp
          thus "a ∈ energies"
            using ‹a = strat' g' ∧ weight g g' ≠ None› ‹x ∈ energies› inv_well_defined by blast 
        qed

        show "False" 
        proof(cases "deadend g")
          case True (*  ⟹ e = NULLEVEKTOR *)

          from emin have " ∃strat.
            (∀g'. weight g g' ≠ None ⟶
                  strat g' ∈ {inv_upd (the (weight g g')) e |e. minimal_winning_budget e g'}) ∧
            e = energy_sup {strat g' |g'. weight g g' ≠ None}" using energy_Min_def by auto
          from this obtain strat where "(∀g'. weight g g' ≠ None ⟶
                  strat g' ∈ {inv_upd (the (weight g g')) e |e. minimal_winning_budget e g'}) ∧
            e = energy_sup {strat g' |g'. weight g g' ≠ None}" by auto
          hence "e = energy_sup {}" using True by simp

          have "energy_sup {} ∈ energies ∧ (∀s. s ∈ {} ⟶ order s (energy_sup {})) ∧ (e' ∈ energies ∧(∀s. s ∈ {} ⟶ order s e') ⟶ order (energy_sup {}) e')"
            using bounded_join_semilattice by blast
          hence "e e≤ e'" using ‹e = energy_sup {}› ‹e' ∈ energies› by auto

          from ‹e' e< e› have "e' e≤ e ∧ e' ≠ e" using energy_order ordering_def ordering.strict_iff_order
            by simp
          hence "e' e≤ e" by simp
          hence "e' = e" using ‹e e≤ e'› using energy_order ordering_def ordering.antisym
            by fastforce 
          thus ?thesis using ‹e' e≤ e ∧ e' ≠ e› by auto
        next
          case False
          hence notempty: "{strat' g' |g'. weight g g' ≠ None} ≠ {}" by auto

          have fin: "finite {strat' g' |g'. weight g g' ≠ None} ∧ finite {strat g' |g'. weight g g' ≠ None}"
          proof
            have "{strat' g' |g'. weight g g' ≠ None} ⊆ {strat' g' |g'. g' ∈ positions}" by auto
            thus "finite {strat' g' |g'. weight g g' ≠ None}" using finite_positions
              using finite_image_set rev_finite_subset by fastforce 
            have "{strat g' |g'. weight g g' ≠ None} ⊆ {strat g' |g'. g' ∈ positions}" by auto
            thus "finite {strat g' |g'. weight g g' ≠ None}" using finite_positions
              using finite_image_set rev_finite_subset by fastforce 
          qed

          have "⋀g'. weight g g' ≠ None ⟹ strat' g' e≤ strat g'" 
          proof-
            fix g'
            assume "weight g g' ≠ None"
            hence some_not_empty: "{inv_upd (the (weight g g')) x|x. (minimal_winning_budget x g' ∧ x e≤ the_e g')} ≠ {}" 
              using some_not_empty by auto
            have "strat' g' = (SOME x. x ∈ {inv_upd (the (weight g g')) x| 
                                                        x. (minimal_winning_budget x g' ∧ x e≤ the_e g')})" 
              using strat'_def by auto
            hence "strat' g' ∈ {inv_upd (the (weight g g')) x| x. (minimal_winning_budget x g' ∧ x e≤ the_e g')}"
              using some_not_empty some_in_eq
              by (smt (verit, ccfv_SIG) Eps_cong) 
            hence "∃x. strat' g' = inv_upd (the (weight g g')) x ∧  minimal_winning_budget x g' ∧ x e≤ the_e g'"
              by simp
            from this obtain x where X: "strat' g' = inv_upd (the (weight g g')) x ∧  minimal_winning_budget x g' ∧ x e≤ the_e g'" by auto
            hence "x ∈ energies" using winning_budget_len.simps energy_Min_def
              by (metis (mono_tags, lifting) mem_Collect_eq) 
            hence "strat' g' e≤  inv_upd (the (weight g g')) (the_e g')" using inverse_monotonic X
              by (metis ‹weight g g' ≠ None› inv_well_defined)

            have "strat g' ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}" using Strat ‹weight g g' ≠ None› by auto
            hence "∃e. strat g' = inv_upd (the (weight g g')) e ∧ winning_budget_len e g'" by auto
            hence "strat g' = inv_upd (the (weight g g')) (the_e g') ∧ winning_budget_len (the_e g') g'" using the_e_def some_eq_ex
              by (metis (mono_tags, lifting))
            thus "strat' g' e≤ strat g'" using ‹strat' g' e≤  inv_upd (the (weight g g')) (the_e g')› by auto
          qed

          hence leq: "(⋀a. a ∈ {strat' g' |g'. weight g g' ≠ None} ⟹ ∃b∈{strat g' |g'. weight g g' ≠ None}. a e≤ b)" by auto
          have in_energy: "{strat g' |g'. weight g g' ≠ None} ⊆ energies ∧ {strat' g' |g'. weight g g' ≠ None} ⊆ energies"
          proof
            show "{strat g' |g'. weight g g' ≠ None} ⊆ energies"
              using Strat
              by (smt (verit, ccfv_threshold) inv_well_defined mem_Collect_eq nonpos_eq_pos subsetI winning_bugget_len_is_wb) 
            show "{strat' g' |g'. weight g g' ≠ None} ⊆ energies"
              unfolding strat'_def
              using len strat'_def by blast 
          qed

          hence "energy_sup {strat' g' |g'. weight g g' ≠ None} e≤ e'" 
            using notempty len Strat energy_sup_leq_energy_sup fin leq
            by presburger 
          hence le: "energy_sup {strat' g' |g'. weight g g' ≠ None} e< e" using ‹e' e< e› in_energy
            by (smt (verit) ‹e ∈ energies› ‹e' ∈ energies› energy_order energy_wqo fin galois_energy_game.bounded_join_semilattice galois_energy_game_axioms ordering.antisym transp_onD wqo_on_imp_transp_on)

          have "energy_sup {strat' g' |g'. weight g g' ≠ None} ∈ {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}" 
          proof-
            have "(∀g'. weight g g' ≠ None ⟶ strat' g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})"
            proof
              fix g'
              show "weight g g' ≠ None ⟶
                    strat' g' ∈ {inv_upd (the (weight g g')) e |e. minimal_winning_budget e g'}"
              proof
                assume "weight g g' ≠ None"
                hence some_not_empty: "{inv_upd (the (weight g g')) x |x. minimal_winning_budget x g' ∧ x e≤ the_e g'} ≠ {}"
                  using some_not_empty by auto
                have "strat' g' = (SOME x. x ∈ {inv_upd (the (weight g g')) x| 
                                                        x. (minimal_winning_budget x g' ∧ x e≤ the_e g')})" 
                  using strat'_def by auto
                hence "strat' g' ∈ {inv_upd (the (weight g g')) x| x. (minimal_winning_budget x g' ∧ x e≤ the_e g')}"
                  using some_not_empty some_in_eq
                  by (smt (verit, ccfv_SIG) Eps_cong) 
                thus "strat' g' ∈ {inv_upd (the (weight g g')) e |e. minimal_winning_budget e g'}"
                  by auto
              qed
            qed
            hence "∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ energy_sup {strat' g' |g'. weight g g' ≠ None} = (energy_sup {strat g'| g'. weight g g' ≠ None})"
              by blast 
            then show ?thesis
              by simp 
          qed

          then show ?thesis 
            using energy_Min_def emin le 
            by (smt (verit) mem_Collect_eq)
        qed
      qed    

      hence "e ∈ energy_Min
            {e''.
             ∃strat.
                (∀g'. weight g g' ≠ None ⟶
                      strat g' ∈ {inv_upd (the (weight g g')) e |e. winning_budget_len e g'}) ∧
                e'' = energy_sup {strat g' |g'. weight g g' ≠ None}}" using element_of energy_Min_def
        by (smt (verit) mem_Collect_eq)  
      thus "minimal_winning_budget e g" 
        using min_winning_budget_d_iff_energy_Min ‹g ∉ attacker›  ‹e ∈ energies› by blast
    qed
  qed


  have "⋀g e. e ∈ a_win_min g ⟹ e ∈ energies" 
    using winning_budget_len.simps energy_Min_def
    by (metis (no_types, lifting) mem_Collect_eq)
  hence D: "⋀g e. e ∈ a_win_min g = (e ∈ a_win_min g ∧ e ∈ energies)" by auto
  fix g 
  show "iteration a_win_min g = a_win_min g"
  proof(cases "g ∈ attacker")
    case True
    have "a_win_min g = {e. minimal_winning_budget e g}" by simp
    hence "a_win_min g =  energy_Min {e. ∃g' e'.
                   weight g g' ≠ None ∧
                   minimal_winning_budget e' g' ∧ e = inv_upd (the (weight g g')) e'}" 
      using minimal_winning_budget_attacker True by simp
    also have "... = energy_Min {inv_upd (the (weight g g')) e'|g' e'.
                   weight g g' ≠ None ∧
                   minimal_winning_budget e' g' }"
      by meson
    also have "... = energy_Min {inv_upd (the (weight g g')) e'|e' g'.
                   weight g g' ≠ None ∧  e' ∈ a_win_min g'}"
      by (metis (no_types, lifting) mem_Collect_eq) 
    also have "... = energy_Min {inv_upd (the (weight g g')) e'|e' g'. e' ∈ energies ∧
                   weight g g' ≠ None ∧ e' ∈ a_win_min g'}" 
      using D by meson
    also have "... = iteration a_win_min g" using iteration_def True by simp
    finally show ?thesis by simp
  next
    case False
    have "a_win_min g = {e. minimal_winning_budget e g}" by simp
    hence minwin: "a_win_min g = energy_Min {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}"
      using minimal_winning_budget_defender False by simp
    hence "a_win_min g = energy_Min {energy_sup {strat g'| g'. weight g g' ≠ None} | strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})}"
      by (smt (z3) Collect_cong)
    have iteration: "energy_Min {energy_sup {inv_upd (the (weight g g')) (e_index g') | g'. weight g g' ≠ None} |
           e_index. ∀g'. weight g g' ≠ None ⟶ ((e_index g') ∈ energies ∧ e_index g' ∈ a_win_min g')} = iteration a_win_min g" 
      using iteration_def False by simp
    
    have "{e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}
        ={energy_sup {inv_upd (the (weight g g')) (e_index g') | g'. weight g g' ≠ None} |
           e_index. ∀g'. weight g g' ≠ None ⟶ ((e_index g') ∈ energies ∧ e_index g' ∈ a_win_min g')}"
    proof
      show "{e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}
            ⊆{energy_sup {inv_upd (the (weight g g')) (e_index g') | g'. weight g g' ≠ None} |
           e_index. ∀g'. weight g g' ≠ None ⟶((e_index g') ∈ energies ∧ e_index g' ∈ a_win_min g')}"
      proof
        fix e 
        assume "e ∈ {e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}"
        hence "∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e = (energy_sup {strat g'| g'. weight g g' ≠ None})"
          by auto
        from this obtain strat where S: "(∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e = (energy_sup {strat g'| g'. weight g g' ≠ None})"
          by auto
        define e_index where "e_index ≡ λg'. (SOME e''. e'' ∈ a_win_min g' ∧ strat g' = the (inverse_application (the (weight g g')) e''))"
        hence index: "⋀g'. weight g g' ≠ None ⟹ (e_index g') ∈ a_win_min g' ∧ strat g' = the (inverse_application (the (weight g g')) (e_index g'))"
        proof-
          fix g'
          have I: "e_index g' = (SOME e''. e'' ∈ a_win_min g' ∧ strat g' = the (inverse_application (the (weight g g')) e''))"
            using e_index_def by simp
          assume "weight g g' ≠ None"
          hence "strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'}"
            using S by simp
          hence "strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. e ∈ a_win_min g'}" by simp
          hence "∃e''. e'' ∈ a_win_min g' ∧ strat g' = the (inverse_application (the (weight g g')) e'')" by auto
          thus "(e_index g') ∈ a_win_min g' ∧ strat g' = the (inverse_application (the (weight g g')) (e_index g'))"
            unfolding e_index_def using some_eq_ex
            by (smt (verit, del_insts)) 
        qed

        show "e ∈ {energy_sup {inv_upd (the (weight g g')) (e_index g') | g'. weight g g' ≠ None} |
           e_index. ∀g'. weight g g' ≠ None ⟶ ((e_index g') ∈ energies ∧ e_index g' ∈ a_win_min g')}"
        proof
          show "∃e_index. e = energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ∧
       (∀g'. weight g g' ≠ None ⟶ ((e_index g') ∈ energies ∧ e_index g' ∈ a_win_min g'))"
          proof
            show "e = energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ∧
       (∀g'. weight g g' ≠ None ⟶ ((e_index g') ∈ energies ∧ e_index g' ∈ a_win_min g'))"
            proof
              show "e = energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}"
                using index S
                by (smt (verit) Collect_cong) 
              have "∀g'. weight g g' ≠ None ⟶ e_index g' ∈ a_win_min g'" 
                using index by simp
              thus "∀g'. weight g g' ≠ None ⟶ ((e_index g') ∈ energies ∧ e_index g' ∈ a_win_min g')" 
                using D by meson
            qed
          qed
        qed
      qed
      show "{energy_sup {inv_upd (the (weight g g')) (e_index g') | g'. weight g g' ≠ None} |
           e_index. ∀g'. weight g g' ≠ None ⟶ ((e_index g') ∈ energies ∧ e_index g' ∈ a_win_min g')}
          ⊆{e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}"
      proof
        fix e
        assume "e ∈ {energy_sup {inv_upd (the (weight g g')) (e_index g') | g'. weight g g' ≠ None} |
           e_index. ∀g'. weight g g' ≠ None ⟶ ((e_index g') ∈ energies ∧ e_index g' ∈ a_win_min g')}"
        from this obtain e_index where I: "e = energy_sup {inv_upd (the (weight g g')) (e_index g') | g'. weight g g' ≠ None} ∧ (∀g'. weight g g' ≠ None ⟶ e_index g' ∈ a_win_min g')"
          by blast
        define strat where "strat ≡ λg'. inv_upd (the (weight g g')) (e_index g')"
        
        show "e ∈{e''. ∃strat. (∀g'. weight g g' ≠ None ⟶ strat g' ∈ {the (inverse_application (the (weight g g')) e) | e. minimal_winning_budget e g'})
                  ∧ e'' = (energy_sup {strat g'| g'. weight g g' ≠ None})}"
        proof
          show "∃strat.
       (∀g'. weight g g' ≠ None ⟶
             strat g' ∈ {inv_upd (the (weight g g')) e |e. minimal_winning_budget e g'}) ∧
       e = energy_sup {strat g' |g'. weight g g' ≠ None}"
          proof
            show "(∀g'. weight g g' ≠ None ⟶
             strat g' ∈ {inv_upd (the (weight g g')) e |e. minimal_winning_budget e g'}) ∧
       e = energy_sup {strat g' |g'. weight g g' ≠ None}"
            proof
              show "∀g'. weight g g' ≠ None ⟶
         strat g' ∈ {inv_upd (the (weight g g')) e |e. minimal_winning_budget e g'}"
                using I strat_def by blast
              show "e = energy_sup {strat g' |g'. weight g g' ≠ None}" using I strat_def
                by blast 
            qed
          qed
        qed
      qed
    qed

    thus ?thesis using minwin iteration by simp
  qed
qed

text‹With this we can conclude that ‹iteration› maps subsets of winning budgets to subsets of winning budgets.›

lemma iteration_stays_winning:
  assumes "F ∈ possible_pareto" and "F ≼ a_win_min"
  shows "iteration F ≼ a_win_min"
proof-
  have "iteration F ≼ iteration a_win_min" 
    using assms iteration_monotonic  a_win_min_in_pareto by blast
  thus ?thesis 
    using a_win_min_is_fp by simp
qed

text‹We now prepare the proof that ‹a_win_min› is the \textit{least} fixed point of ‹iteration› by introducing ‹S›.
›

inductive S:: "'energy ⇒ 'position ⇒ bool" where
  "S e g" if "g ∉ attacker ∧ (∃index. e = (energy_sup 
              {inv_upd (the (weight g g')) (index g')| g'. weight g g' ≠ None})
              ∧ (∀g'.  weight g g' ≠ None ⟶  S (index g') g'))" |
  "S e g" if "g ∈ attacker ∧ (∃g'.( weight g g' ≠ None 
              ∧ (∃e'. S e' g' ∧ e = inv_upd (the (weight g g')) e')))"

lemma length_S: 
  shows "⋀e g. S e g ⟹ e ∈ energies"
proof-
  fix e g
  assume "S e g"
  thus "e ∈ energies"
  proof(rule S.induct)
    show "⋀g e. g ∉ attacker ∧
           (∃index.
               e =
               energy_sup
                {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ∧
               (∀g'. weight g g' ≠ None ⟶ S (index g') g' ∧ (index g') ∈ energies)) ⟹
           e ∈ energies"
    proof-
      fix e g 
      assume "g ∉ attacker ∧
           (∃index.
               e =
               energy_sup
                {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ∧
               (∀g'. weight g g' ≠ None ⟶ S (index g') g' ∧ (index g') ∈ energies))"
      from this obtain index where E: "e =
               energy_sup
                {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}" and "(∀g'. weight g g' ≠ None ⟶ S (index g') g' ∧ (index g') ∈ energies)" by auto
      hence in_energy: "{inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⊆ energies"
        using inv_well_defined by blast
      have "{inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (index g') |g'. g'∈ positions}" by auto
      hence "finite {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}"
        using finite_positions rev_finite_subset by fastforce 
      thus "e ∈ energies" using E in_energy bounded_join_semilattice by meson 
    qed

    show "⋀g e. g ∈ attacker ∧
           (∃g'. weight g g' ≠ None ∧
                 (∃e'. (S e' g' ∧ e' ∈ energies) ∧
                       e = inv_upd (the (weight g g')) e')) ⟹
           e ∈ energies"
    proof-
      fix e g 
      assume "g ∈ attacker ∧
           (∃g'. weight g g' ≠ None ∧
                 (∃e'. (S e' g' ∧ e' ∈ energies) ∧
                       e = inv_upd (the (weight g g')) e'))"
      from this obtain g' e' where "weight g g' ≠ None" and "(S e' g' ∧ e' ∈ energies) ∧
                       e = inv_upd (the (weight g g')) e'" by auto
      thus "e ∈ energies"
        using inv_well_defined by blast
    qed
  qed
qed

lemma a_win_min_is_minS:
  shows "energy_Min {e. S e g} = a_win_min g"
proof-
    have "{e. ∃e'. S e' g ∧ e' e≤ e} = a_win g"
  proof
    show "{e. ∃e'. S e' g ∧ e' e≤ e} ⊆ a_win g"
    proof
      fix e
      assume "e ∈ {e. ∃e'. S e' g ∧ e' e≤ e}"
      from this obtain e' where "S e' g ∧ e' e≤ e" by auto
      have "e' ∈ a_win g" 
      proof(rule S.induct)
        show "S e' g" using ‹S e' g ∧ e' e≤ e› by simp
        show "⋀g e. g ∉ attacker ∧
           (∃index.
               e =
               energy_sup
                {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ∧
               (∀g'. weight g g' ≠ None ⟶ S (index g') g' ∧ index g' ∈ a_win g')) ⟹
           e ∈ a_win g"
        proof
          fix e g 
          assume A: "g ∉ attacker ∧
           (∃index.
               e =
               energy_sup
                {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ∧
               (∀g'. weight g g' ≠ None ⟶ S (index g') g' ∧ index g' ∈ a_win g'))"
          from this obtain index where E: "e =
               energy_sup
                {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ∧
               (∀g'. weight g g' ≠ None ⟶ S (index g') g' ∧ index g' ∈ a_win g')" by auto
          show "winning_budget_len e g"
          proof(rule winning_budget_len.intros(1))
            show "e ∈ energies ∧
    g ∉ attacker ∧
    (∀g'. weight g g' ≠ None ⟶
          apply_w g g' e ≠ None ∧ winning_budget_len (upd (the (weight g g')) e) g')"
            proof
              have "{inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⊆{inv_upd (the (weight g g')) (index g') |g'. g' ∈ positions }" by auto
              hence fin: "finite {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}"
                using finite_positions rev_finite_subset by fastforce 
              have "{inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⊆ energies" using E
                using inv_well_defined length_S by blast 
              thus "e ∈ energies" using E fin bounded_join_semilattice by meson

              show "g ∉ attacker ∧
    (∀g'. weight g g' ≠ None ⟶
          apply_w g g' e ≠ None ∧ winning_budget_len (upd (the (weight g g')) e) g')"
              proof
                show "g ∉ attacker"
                  using A by simp
                show "∀g'. weight g g' ≠ None ⟶
         apply_w g g' e ≠ None ∧ winning_budget_len (upd (the (weight g g')) e) g'"
                proof
                  fix g'
                  show "weight g g' ≠ None ⟶
         apply_w g g' e ≠ None ∧ winning_budget_len (upd (the (weight g g')) e) g'"
                  proof
                    assume "weight g g' ≠ None"
                    hence "S (index g') g' ∧ index g' ∈ a_win g'" using E
                      by simp 
                    show "apply_w g g' e ≠ None ∧ winning_budget_len (upd (the (weight g g')) e) g'"
                    proof
                      from E have E:"e = energy_sup {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}" by simp


                      have "⋀s'. energy_sup {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ∈ energies ∧ (∀s. s ∈ {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⟶ s e≤ energy_sup {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}) ∧ (s' ∈ energies ∧ (∀s. s ∈ {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⟶ s e≤ s') ⟶ energy_sup {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} e≤ s')"
                      proof(rule bounded_join_semilattice)
                        show "⋀s'. {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⊆ energies"
                        proof-
                          fix s' 
                          show "{inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⊆ energies"
                            using ‹{inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⊆ energies› by auto
                        qed
                        show "⋀s'. finite {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}"
                        proof-
                          fix s'
                          have "{inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (index g') |g'. g' ∈ positions}" by auto
                          thus "finite {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}" using finite_positions
                            using rev_finite_subset by fastforce
                        qed
                      qed
                      hence "(∀s. s ∈ {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⟶ s e≤ energy_sup {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None})" by auto

                      hence leq: "inv_upd (the (weight g g')) (index g') e≤ e" 
                        unfolding E
                        using ‹weight g g' ≠ None› by blast 

                      show "apply_w g g' e ≠ None"
                      using ‹weight g g' ≠ None› proof(rule domain_upw_closed)
                        show "apply_w g g' (inv_upd (the (weight g g')) (index g')) ≠ None"
                          using inv_well_defined  ‹weight g g' ≠ None› ‹S (index g') g' ∧ index g' ∈ a_win g'› winning_budget_len.simps
                          by (metis inv_well_defined mem_Collect_eq) 
                        show "inv_upd (the (weight g g')) (index g') e≤ e" using leq by simp
                      qed

                      have A1: "index g' e≤ upd (the (weight g g')) (inv_upd (the (weight g g')) (index g'))"
                        using upd_inv_increasing  ‹S (index g') g' ∧ index g' ∈ a_win g'› winning_budget_len.simps
                        using ‹weight g g' ≠ None› by blast
                      have A2: "upd (the (weight g g')) (inv_upd (the (weight g g')) (index g')) e≤
    upd (the (weight g g')) e" using leq updates_monotonic  ‹weight g g' ≠ None›
                        using ‹S (index g') g' ∧ index g' ∈ a_win g'› inv_well_defined length_S by blast

                      hence "index g' e≤ upd (the (weight g g')) e" using A1 energy_order ordering_def
                        by (metis (mono_tags, lifting) partial_preordering.trans) 
                      
                      thus "winning_budget_len (upd (the (weight g g')) e) g'"
                        using upwards_closure_wb_len ‹S (index g') g' ∧ index g' ∈ a_win g'› by blast
                    qed
                  qed
                qed
              qed
            qed
          qed
        qed


        show "⋀g e. g ∈ attacker ∧
           (∃g'. weight g g' ≠ None ∧
                 (∃e'. (S e' g' ∧ e' ∈ a_win g') ∧ e = inv_upd (the (weight g g')) e')) ⟹
           e ∈ a_win g "
        proof
          fix e g 
          assume A: "g ∈ attacker ∧
           (∃g'. weight g g' ≠ None ∧
                 (∃e'. (S e' g' ∧ e' ∈ a_win g') ∧ e = inv_upd (the (weight g g')) e'))"
          from this obtain g' e' where "weight g g' ≠ None" and "(S e' g' ∧ e' ∈ a_win g') ∧ e = inv_upd (the (weight g g')) e'" by auto
          hence "e' e≤ upd (the (weight g g')) e" 
            using  updates_monotonic inv_well_defined inv_well_defined
            by (metis length_S upd_inv_increasing)
          show "winning_budget_len e g" 
          proof(rule winning_budget_len.intros(2))
            show "e ∈ energies ∧
    g ∈ attacker ∧
    (∃g'. weight g g' ≠ None ∧
          apply_w g g' e ≠ None ∧ winning_budget_len (upd (the (weight g g')) e) g')"
            proof
              have"e' ∈ energies" using ‹(S e' g' ∧ e' ∈ a_win g') ∧ e = inv_upd (the (weight g g')) e'› winning_budget_len.simps
                by blast
              show "e ∈ energies"
                using ‹(S e' g' ∧ e' ∈ a_win g') ∧ e = inv_upd (the (weight g g')) e'›  ‹e' ∈ energies› ‹weight g g' ≠ None›
                using inv_well_defined by blast               
              show "g ∈ attacker ∧
    (∃g'. weight g g' ≠ None ∧
          apply_w g g' e ≠ None ∧ winning_budget_len (upd (the (weight g g')) e) g')"
              proof
                show "g ∈ attacker" using A by simp
                show "∃g'. weight g g' ≠ None ∧
         apply_w g g' e ≠ None ∧ winning_budget_len (upd (the (weight g g')) e) g' "
                proof
                  show " weight g g' ≠ None ∧
         apply_w g g' e ≠ None ∧ winning_budget_len (upd (the (weight g g')) e) g'"
                  proof
                    show "weight g g' ≠ None"
                      using ‹weight g g' ≠ None› .
                    show "apply_w g g' e ≠ None ∧ winning_budget_len (upd (the (weight g g')) e) g'"
                    proof
                      show "apply_w g g' e ≠ None"
                        using ‹weight g g' ≠ None› ‹(S e' g' ∧ e' ∈ a_win g') ∧ e = inv_upd (the (weight g g')) e'›
                        ‹e' e≤ upd (the (weight g g')) e›  updates_monotonic inv_well_defined inv_well_defined
                        by (metis mem_Collect_eq winning_budget_len.cases)
                      show "winning_budget_len (upd (the (weight g g')) e) g'"
                        using ‹e' e≤ upd (the (weight g g')) e› upwards_closure_wb_len ‹(S e' g' ∧ e' ∈ a_win g') ∧ e = inv_upd (the (weight g g')) e'› by blast
                    qed
                  qed
                qed
              qed
            qed
          qed
        qed
      qed
      thus "e ∈ a_win g" using ‹S e' g ∧ e' e≤ e› upwards_closure_wb_len
        by blast 
    qed
  next
    show "a_win g ⊆ {e. ∃e'. S e' g ∧ e' e≤ e}"
    proof

      define P where "P ≡ λ(g,e). (e ∈{e. ∃e'. S e' g ∧ e' e≤ e})"
      
      fix e
      assume "e ∈ a_win g" 
      from this obtain s where S: "attacker_winning_strategy s e g"
        using nonpos_eq_pos
        by (metis winning_bugget_len_is_wb mem_Collect_eq winning_budget.elims(2))       
      have "reachable_positions_len s g e ⊆ reachable_positions s g e" by auto
      hence "wfp_on (strategy_order s) (reachable_positions_len s g e)" 
        using strategy_order_well_founded S
        using Restricted_Predicates.wfp_on_subset by blast
      hence "inductive_on (strategy_order s) (reachable_positions_len s g e)"
        by (simp add: wfp_on_iff_inductive_on)

      hence "P (g,e)" 
      proof(rule inductive_on_induct)
        show "(g,e) ∈ reachable_positions_len s g e"
          unfolding reachable_positions_def proof-
          have "lfinite LNil ∧
             llast (LCons g LNil) = g ∧
             valid_play (LCons g LNil) ∧ play_consistent_attacker s (LCons g LNil) e ∧
            Some e = energy_level e (LCons g LNil) (the_enat (llength LNil))"
            using valid_play.simps play_consistent_attacker.simps energy_level.simps
            by (metis lfinite_code(1) llast_singleton llength_LNil neq_LNil_conv the_enat_0) 
          thus "(g, e)
    ∈ {(g', e').
        (g', e')
        ∈ {(g', e') |g' e'.
            ∃p. lfinite p ∧
                llast (LCons g p) = g' ∧
                valid_play (LCons g p) ∧
                play_consistent_attacker s (LCons g p) e ∧ Some e' = energy_level e (LCons g p) (the_enat (llength p))} ∧
        e' ∈ energies}"
            using ‹e ∈ a_win g› nonpos_eq_pos winning_bugget_len_is_wb
            by auto
        qed

        show "⋀y. y ∈ reachable_positions_len s g e ⟹
              (⋀x. x ∈ reachable_positions_len s g e ⟹ strategy_order s x y ⟹ P x) ⟹ P y"
        proof-
          fix y 
          assume "y ∈ reachable_positions_len s g e"
          hence "∃e' g'. y = (g', e')" using reachable_positions_def by auto
          from this obtain e' g' where "y = (g', e')" by auto

          hence y_len: "(∃p. lfinite p ∧ llast (LCons g p) = g' 
                                                    ∧ valid_play (LCons g p) 
                                                    ∧ play_consistent_attacker s (LCons g p) e
                                                    ∧ (Some e' = energy_level e (LCons g p) (the_enat (llength p))))
                ∧ e' ∈ energies"
            using ‹y ∈ reachable_positions_len s g e› unfolding reachable_positions_def
            by auto 
          from this obtain p where P: "(lfinite p ∧ llast (LCons g p) = g' 
                                                    ∧ valid_play (LCons g p) 
                                                    ∧ play_consistent_attacker s (LCons g p) e) 
                                                    ∧ (Some e' = energy_level e (LCons g p) (the_enat (llength p)))" by auto
       
          show "(⋀x. x ∈ reachable_positions_len s g e ⟹ strategy_order s x y ⟹ P x) ⟹ P y"
          proof-
            assume ind: "(⋀x. x ∈ reachable_positions_len s g e ⟹ strategy_order s x y ⟹ P x)"
            thus "P y" 
            proof(cases "g' ∈ attacker")
              case True 
              then show ?thesis 
              proof(cases "deadend g'")
                case True (* wiederspruchsbeweis *)
                hence "attacker_stuck (LCons g p)" using ‹g' ∈ attacker› P
                  by (meson defender_wins_play_def attacker_winning_strategy.elims(2)) 
                hence "defender_wins_play e (LCons g p)" using defender_wins_play_def by simp
                have "¬defender_wins_play e (LCons g p)" using P S by simp
                then show ?thesis using ‹defender_wins_play e (LCons g p)› by simp
              next
                case False (* nehme s e' g' und wende ind.hyps. darauf an *)
                hence "(s e' g') ≠ None ∧ (weight g' (the (s e' g')))≠None" using S attacker_winning_strategy.simps
                  by (simp add: True attacker_strategy_def)

                define x where "x = (the (s e' g'), the (apply_w g' (the (s e' g')) e'))"
                define p' where "p' =  (lappend p (LCons (the (s e' g')) LNil))"
                hence "lfinite p'" using P by simp
                have "llast (LCons g p') = the (s e' g')" using p'_def ‹lfinite p'›
                  by (simp add: llast_LCons)

                have "the_enat (llength p') > 0" using P
                  by (metis LNil_eq_lappend_iff ‹lfinite p'› bot_nat_0.not_eq_extremum enat_0_iff(2) lfinite_conv_llength_enat llength_eq_0 llist.collapse(1) llist.distinct(1) p'_def the_enat.simps) 
                hence "∃i. Suc i = the_enat (llength p')"
                  using less_iff_Suc_add by auto 
                from this obtain i where "Suc i = the_enat (llength p')" by auto
                hence "i = the_enat (llength p)" using p'_def P                     
                  by (metis Suc_leI ‹lfinite p'› length_append_singleton length_list_of_conv_the_enat less_Suc_eq_le less_irrefl_nat lfinite_LConsI lfinite_LNil list_of_LCons list_of_LNil list_of_lappend not_less_less_Suc_eq)
                hence "Some e' = (energy_level e (LCons g p) i)" using P by simp

                have A: "lfinite (LCons g p) ∧ i < the_enat (llength (LCons g p)) ∧ energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None"
                proof
                  show "lfinite (LCons g p)" using P by simp
                  show "i < the_enat (llength (LCons g p)) ∧ energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None"
                  proof
                    show "i < the_enat (llength (LCons g p))" using ‹i = the_enat (llength p)› P
                      by (metis ‹lfinite (LCons g p)› length_Cons length_list_of_conv_the_enat lessI list_of_LCons) 
                    show "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None" using P ‹i = the_enat (llength p)›
                      using S defender_wins_play_def by auto
                  qed
                qed

                hence "Some e' = (energy_level e (LCons g p') i)" using p'_def energy_level_append P ‹Some e' = (energy_level e (LCons g p) i)›
                  by (metis lappend_code(2))
                hence "energy_level e (LCons g p') i ≠ None"
                  by (metis option.distinct(1))

                have "enat (Suc i) = llength p'" using ‹Suc i = the_enat (llength p')›
                  by (metis ‹lfinite p'› lfinite_conv_llength_enat the_enat.simps)
                also have "... < eSuc (llength p')"
                  by (metis calculation iless_Suc_eq order_refl) 
                also have "... = llength (LCons g p')" using ‹lfinite p'› by simp
                finally have "enat (Suc i) < llength (LCons g p')".

                have "(lnth (LCons g p) i) = g'" using ‹i = the_enat (llength p)› P
                  by (metis lfinite_conv_llength_enat llast_conv_lnth llength_LCons the_enat.simps) 
                hence "(lnth (LCons g p') i) = g'" using p'_def
                  by (metis P ‹i = the_enat (llength p)› enat_ord_simps(2) energy_level.elims lessI lfinite_llength_enat lnth_0 lnth_Suc_LCons lnth_lappend1 the_enat.simps) 

                have "energy_level e (LCons g p') (the_enat (llength p')) = energy_level e (LCons g p') (Suc i)" 
                  using ‹Suc i = the_enat (llength p')› by simp
                also have "... = apply_w (lnth (LCons g p') i) (lnth (LCons g p') (Suc i)) (the (energy_level e (LCons g p') i))" 
                  using energy_level.simps ‹enat (Suc i) < llength (LCons g p')› ‹energy_level e (LCons g p') i ≠ None›
                  by (meson leD)
                also have "... =  apply_w (lnth (LCons g p') i) (lnth (LCons g p') (Suc i)) e'" using ‹Some e' = (energy_level e (LCons g p') i)›
                  by (metis option.sel) 
                also have "... =  apply_w (lnth (LCons g p') i) (the (s e' g')) e'" using p'_def ‹enat (Suc i) = llength p'›
                  by (metis ‹eSuc (llength p') = llength (LCons g p')› ‹llast (LCons g p') = the (s e' g')› llast_conv_lnth) 
                also have  "... =  apply_w g' (the (s e' g')) e'" using ‹(lnth (LCons g p') i) = g'› by simp
                finally have "energy_level e (LCons g p') (the_enat (llength p')) = apply_w g' (the (s e' g')) e'" .
            
                have P': "lfinite p'∧
             llast (LCons g p') = (the (s e' g')) ∧
             valid_play (LCons g p') ∧ play_consistent_attacker s (LCons g p') e ∧
            Some (the (apply_w g' (the (s e' g')) e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                proof
                  show "lfinite p'" using p'_def P by simp
                  show "llast (LCons g p') = the (s e' g') ∧
    valid_play (LCons g p') ∧
    play_consistent_attacker s (LCons g p') e ∧
    Some (the (apply_w g' (the (s e' g')) e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                  proof
                    show "llast (LCons g p') = the (s e' g')" using p'_def ‹lfinite p'›
                      by (simp add: llast_LCons) 
                    show "valid_play (LCons g p') ∧
    play_consistent_attacker s (LCons g p') e ∧
    Some (the (apply_w g' (the (s e' g')) e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                    proof
                      show "valid_play (LCons g p')" using p'_def P
                        using ‹s e' g' ≠ None ∧ weight g' (the (s e' g')) ≠ None› valid_play.intros(2) valid_play_append by auto
                      show "play_consistent_attacker s (LCons g p') e ∧
    Some (the (apply_w g' (the (s e' g')) e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                      proof
                        have "(LCons g p') = lappend (LCons g p) (LCons (the (s e' g')) LNil)" using p'_def
                          by simp
                        have "play_consistent_attacker s (lappend (LCons g p) (LCons (the (s e' g')) LNil)) e"
                        proof (rule play_consistent_attacker_append_one)
                          show "play_consistent_attacker s (LCons g p) e"
                            using P by auto
                          show "lfinite (LCons g p)" using P by auto
                          show "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None" using P
                            using A by auto 
                          show "valid_play (lappend (LCons g p) (LCons (the (s e' g')) LNil))" 
                            using ‹valid_play (LCons g p')› ‹(LCons g p') = lappend (LCons g p) (LCons (the (s e' g')) LNil)› by simp
                          show "llast (LCons g p) ∈ attacker ⟶
    Some (the (s e' g')) =
    s (the (energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1))) (llast (LCons g p))"
                          proof
                            assume "llast (LCons g p) ∈ attacker"
                            show "Some (the (s e' g')) =
    s (the (energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1))) (llast (LCons g p))"
                              using ‹llast (LCons g p) ∈ attacker› P
                              by (metis One_nat_def ‹s e' g' ≠ None ∧ weight g' (the (s e' g')) ≠ None› diff_Suc_1' eSuc_enat lfinite_llength_enat llength_LCons option.collapse option.sel the_enat.simps) 
                          qed
                        qed
                        thus "play_consistent_attacker s (LCons g p') e" using ‹(LCons g p') = lappend (LCons g p) (LCons (the (s e' g')) LNil)› by simp
                    
                        show "Some (the (apply_w g' (the (s e' g')) e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                          by (metis ‹eSuc (llength p') = llength (LCons g p')› ‹enat (Suc i) = llength p'› ‹energy_level e (LCons g p') (the_enat (llength p')) = apply_w g' (the (s e' g')) e'› ‹play_consistent_attacker s (LCons g p') e› ‹valid_play (LCons g p')› S defender_wins_play_def diff_Suc_1 eSuc_enat option.collapse attacker_winning_strategy.elims(2) the_enat.simps)
                      qed
                    qed
                  qed
                qed

                have x_len: "(upd (the (weight g' (the (s e' g')))) e') ∈ energies" using y_len
                  by (metis P' ‹energy_level e (LCons g p') (the_enat (llength p')) = apply_w g' (the (s e' g')) e'› ‹s e' g' ≠ None ∧ weight g' (the (s e' g')) ≠ None› option.distinct(1) upd_well_defined)
                hence "x ∈ reachable_positions_len s g e" using P' reachable_positions_def x_def by auto

                have "(apply_w g' (the (s e' g')) e') ≠ None" using P'
                  by (metis ‹energy_level e (LCons g p') (the_enat (llength p')) = apply_w g' (the (s e' g')) e'› option.distinct(1)) 
    
                have "Some (the (apply_w g' (the (s e' g')) e')) = apply_w g' (the (s e' g')) e' ∧ (if g' ∈ attacker then Some (the (s e' g')) = s e' g' else weight g' (the (s e' g')) ≠ None)"
                  using ‹(s e' g') ≠ None ∧ (weight g' (the (s e' g')))≠None› ‹(apply_w g' (the (s e' g')) e') ≠ None› by simp
                hence "strategy_order s x y" unfolding strategy_order_def using x_def ‹y = (g', e')›
                  by blast
                hence "P x" using ind ‹x ∈ reachable_positions_len s g e› by simp 
               
                hence "∃e''. S e'' (the (s e' g')) ∧ e'' e≤ ( upd (the (weight g' (the (s e' g')))) e')" unfolding P_def x_def by simp
                from this obtain e'' where E: "S e'' (the (s e' g')) ∧ e'' e≤ (upd (the (weight g' (the (s e' g')))) e')" by auto
                hence "S (inv_upd (the (weight g' (the (s e' g')))) e'') g'" using True S.intros(2)
                  using ‹s e' g' ≠ None ∧ weight g' (the (s e' g')) ≠ None› by blast

                have "(inv_upd (the (weight g' (the (s e' g')))) e'') e≤ inv_upd (the (weight g' (the (s e' g')))) (upd (the (weight g' (the (s e' g')))) e')" 
                  using E inverse_monotonic  ‹s e' g' ≠ None ∧ weight g' (the (s e' g')) ≠ None›
                  using x_len
                  using inv_well_defined length_S by blast  
                hence "(inv_upd (the (weight g' (the (s e' g')))) e'') e≤ e'" using inv_upd_decreasing  ‹s e' g' ≠ None ∧ weight g' (the (s e' g')) ≠ None›
                  using ‹apply_w g' (the (s e' g')) e' ≠ None› energy_order ordering_def 
                  by (metis (mono_tags, lifting) E ‹apply_w g' (the (s e' g')) e' ≠ None› ‹y = (g', e')› ‹y ∈ reachable_positions_len s g e› case_prodD galois_energy_game.galois galois_energy_game_decidable.length_S galois_energy_game_decidable_axioms galois_energy_game_axioms mem_Collect_eq)
                thus "P y" unfolding P_def ‹y = (g', e')›
                  using ‹S (inv_upd (the (weight g' (the (s e' g')))) e'') g'› by blast 
              qed
            next
              case False
              hence P: "g' ∉ attacker ∧
            (∀g''. weight g' g'' ≠ None ⟶
          apply_w g' g'' e' ≠ None ∧ P (g'', (the (apply_w g' g'' e'))))"
              proof
                show "∀g''. weight g' g'' ≠ None ⟶
          apply_w g' g'' e' ≠ None ∧  P (g'', (the (apply_w g' g'' e')))"
                proof
                  fix g''
                  show "weight g' g'' ≠ None ⟶
           apply_w g' g'' e' ≠ None ∧  P (g'', (the (apply_w g' g'' e'))) "
                  proof
                    assume "weight g' g'' ≠ None"
                    show "apply_w g' g'' e' ≠ None ∧  P (g'', (the (apply_w g' g'' e')))"
                    proof
                      show "apply_w g' g'' e' ≠ None"
                      proof
                        assume "apply_w g' g'' e' = None"
                        define p' where "p' ≡ (LCons g (lappend p (LCons g'' LNil)))"
                        hence "lfinite p'" using P by simp
                        have "∃i. llength p = enat i" using P
                          by (simp add: lfinite_llength_enat) 
                        from this obtain i where "llength p = enat i" by auto
                        hence "llength (lappend p (LCons g'' LNil)) = enat (Suc i)"
                          by (simp add: ‹llength p = enat i› eSuc_enat iadd_Suc_right)
                        hence "llength p' = eSuc (enat(Suc i))" using p'_def
                          by simp 
                        hence "the_enat (llength p') = Suc (Suc i)"
                          by (simp add: eSuc_enat)
                        hence "the_enat (llength p') - 1 = Suc i"
                          by simp 
                        hence "the_enat (llength p') - 1 = the_enat (llength (lappend p (LCons g'' LNil)))"
                          using ‹llength (lappend p (LCons g'' LNil)) = enat (Suc i)›
                          by simp

                        have "(lnth p' i) = g'" using p'_def ‹llength p = enat i› P
                          by (smt (verit) One_nat_def diff_Suc_1' enat_ord_simps(2) energy_level.elims lessI llast_conv_lnth llength_LCons lnth_0 lnth_LCons' lnth_lappend the_enat.simps)
                        have "(lnth p' (Suc i)) = g''" using p'_def ‹llength p = enat i›
                          by (metis ‹llength p' = eSuc (enat (Suc i))› lappend.disc(2) llast_LCons llast_conv_lnth llast_lappend_LCons llength_eq_enat_lfiniteD llist.disc(1) llist.disc(2))
                        have "p' = lappend (LCons g p) (LCons g'' LNil)" using p'_def by simp
                        hence "the (energy_level e p' i) = the (energy_level e (lappend (LCons g p) (LCons g'' LNil)) i)" by simp
                        also have "... = the (energy_level e (LCons g p) i)" using ‹llength p = enat i› energy_level_append P
                          by (metis diff_Suc_1 eSuc_enat lessI lfinite_LConsI llength_LCons option.distinct(1) the_enat.simps) 
                        also have "... = e'" using P
                          by (metis ‹llength p = enat i› option.sel the_enat.simps) 
                        finally have "the (energy_level e p' i) = e'" . 
                        hence "apply_w (lnth p' i) (lnth p' (Suc i)) (the (energy_level e p' i)) = None" using ‹apply_w g' g'' e'=None› ‹(lnth p' i) = g'› ‹(lnth p' (Suc i)) = g''› by simp

                        have "energy_level e p' (the_enat (llength p') - 1) = 
                          energy_level e p' (the_enat (llength (lappend p (LCons g'' LNil))))" 
                          using ‹the_enat (llength p') - 1 = the_enat (llength (lappend p (LCons g'' LNil)))›
                          by simp 
                        also have "... = energy_level e p' (Suc i)" using ‹llength (lappend p (LCons g'' LNil)) = enat (Suc i)› by simp
                        also have "... = (if energy_level e p' i = None ∨ llength p' ≤ enat (Suc i) then None
                                      else apply_w (lnth p' i) (lnth p' (Suc i)) (the (energy_level e p' i)))" using energy_level.simps by simp
                        also have "... = None " using ‹apply_w (lnth p' i) (lnth p' (Suc i)) (the (energy_level e p' i)) = None›
                          by simp
                        finally have "energy_level e p' (the_enat (llength p') - 1) = None" .
                        hence "defender_wins_play e p'" unfolding defender_wins_play_def by simp

                        have "valid_play p'"
                          by (metis P ‹p' = lappend (LCons g p) (LCons g'' LNil)› ‹weight g' g'' ≠ None› energy_game.valid_play.intros(2) energy_game.valid_play_append lfinite_LConsI)

                        have "play_consistent_attacker s (lappend (LCons g p) (LCons g'' LNil)) e"
                        proof(rule play_consistent_attacker_append_one)
                          show "play_consistent_attacker s (LCons g p) e" 
                            using P by simp
                          show "lfinite (LCons g p)" using P by simp
                          show "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None"
                            using P
                            by (meson S defender_wins_play_def attacker_winning_strategy.elims(2))
                          show "valid_play (lappend (LCons g p) (LCons g'' LNil))"
                            using ‹valid_play p'› ‹p' = lappend (LCons g p) (LCons g'' LNil)› by simp
                          show "llast (LCons g p) ∈ attacker ⟶
    Some g'' =
    s (the (energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1))) (llast (LCons g p))"
                            using False P by simp
                        qed
                        hence "play_consistent_attacker s p' e"
                          using ‹p' = lappend (LCons g p) (LCons g'' LNil)› by simp
                        hence "¬defender_wins_play e p'" using ‹valid_play p'› p'_def S by simp
                        thus "False" using ‹defender_wins_play e p'› by simp
                      (* widerspruch weil in reachable und sonst defender_wins_play *)
                      qed

                      define x where "x = (g'', the (apply_w g' g'' e'))"
                      have "P x" 
                      proof(rule ind)
                        have X: "(∃p. lfinite p ∧
             llast (LCons g p) = g'' ∧
             valid_play (LCons g p) ∧ play_consistent_attacker s (LCons g p) e ∧
            Some (the (apply_w g' g'' e')) = energy_level e (LCons g p) (the_enat (llength p)))"
                        proof
                          define p' where "p' = lappend p (LCons g'' LNil)"
                          show "lfinite p' ∧
     llast (LCons g p') = g'' ∧
     valid_play (LCons g p') ∧ play_consistent_attacker s (LCons g p') e ∧
    Some (the (apply_w g' g'' e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                          proof
                            show "lfinite p'" using P p'_def by simp
                            show "llast (LCons g p') = g'' ∧
    valid_play (LCons g p') ∧
    play_consistent_attacker s (LCons g p') e ∧
    Some (the (apply_w g' g'' e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                            proof
                              show "llast (LCons g p') = g''" using p'_def
                                by (metis ‹lfinite p'› lappend.disc_iff(2) lfinite_lappend llast_LCons llast_lappend_LCons llast_singleton llist.discI(2))
                              show "valid_play (LCons g p') ∧
    play_consistent_attacker s (LCons g p') e ∧
    Some (the (apply_w g' g'' e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                              proof
                                show "valid_play (LCons g p')" using p'_def P
                                  using ‹weight g' g'' ≠ None› lfinite_LCons valid_play.intros(2) valid_play_append by auto
                                show "play_consistent_attacker s (LCons g p') e ∧
    Some (the (apply_w g' g'' e')) = energy_level e (LCons g p') (the_enat (llength p')) "
                                proof

                                  have "play_consistent_attacker s (lappend (LCons g p) (LCons g'' LNil)) e"
                                  proof(rule play_consistent_attacker_append_one)
                                    show "play_consistent_attacker s (LCons g p) e" 
                                      using P by simp
                                    show "lfinite (LCons g p)" using P by simp
                                    show "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None"
                                      using P
                                      by (meson S defender_wins_play_def attacker_winning_strategy.elims(2))
                                    show "valid_play (lappend (LCons g p) (LCons g'' LNil))"
                                      using ‹valid_play (LCons g p')› p'_def by simp
                                    show "llast (LCons g p) ∈ attacker ⟶
                                        Some g'' =
                                        s (the (energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1))) (llast (LCons g p))"
                                      using False P by simp
                                  qed
                                  thus "play_consistent_attacker s (LCons g p') e" using p'_def
                                    by (simp add: lappend_code(2)) 

                                  have "∃i. Suc i = the_enat (llength p')" using p'_def ‹lfinite p'›
                                    by (metis P length_append_singleton length_list_of_conv_the_enat lfinite_LConsI lfinite_LNil list_of_LCons list_of_LNil list_of_lappend)
                                  from this obtain i where "Suc i = the_enat (llength p')" by auto
                                  hence "i = the_enat (llength p)" using p'_def
                                    by (smt (verit) One_nat_def ‹lfinite p'› add.commute add_Suc_shift add_right_cancel length_append length_list_of_conv_the_enat lfinite_LNil lfinite_lappend list.size(3) list.size(4) list_of_LCons list_of_LNil list_of_lappend plus_1_eq_Suc)  
                                  hence "Suc i = llength (LCons g p)"
                                    using P eSuc_enat lfinite_llength_enat by fastforce
                                  have "(LCons g p') = lappend (LCons g p) (LCons g'' LNil)" using p'_def by simp
                                  have A: "lfinite (LCons g p) ∧ i < the_enat (llength (LCons g p)) ∧  energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None"
                                  proof
                                    show "lfinite (LCons g p)" using P by simp
                                    show " i < the_enat (llength (LCons g p)) ∧
    energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None "
                                    proof
                                      have "(llength p') = llength (LCons g p)" using p'_def
                                        by (metis P ‹lfinite p'› length_Cons length_append_singleton length_list_of lfinite_LConsI lfinite_LNil list_of_LCons list_of_LNil list_of_lappend) 
                                      thus "i < the_enat (llength (LCons g p))" using ‹Suc i = the_enat (llength p')›
                                        using lessI by force 
                                      show "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None" using P
                                        by (meson S energy_game.defender_wins_play_def energy_game.play_consistent_attacker.intros(2) attacker_winning_strategy.simps)
                                    qed
                                  qed
                                  hence "energy_level e (LCons g p') i ≠ None"
                                    using energy_level_append
                                    by (smt (verit) Nat.lessE Suc_leI ‹LCons g p' = lappend (LCons g p) (LCons g'' LNil)› diff_Suc_1 energy_level_nth)  
                                  have "enat (Suc i) < llength (LCons g p')" 
                                    using ‹Suc i = the_enat (llength p')›
                                    by (metis Suc_ile_eq ‹lfinite p'› ldropn_Suc_LCons leI lfinite_conv_llength_enat lnull_ldropn nless_le the_enat.simps) 
                                  hence  el_prems: "energy_level e (LCons g p') i ≠ None ∧ llength (LCons g p') > enat (Suc i)" using ‹energy_level e (LCons g p') i ≠ None› by simp

                                  have "(lnth (LCons g p') i) = lnth (LCons g p) i" 
                                    unfolding ‹(LCons g p') = lappend (LCons g p) (LCons g'' LNil)› using ‹i = the_enat (llength p)› lnth_lappend1
                                    by (metis A enat_ord_simps(2) length_list_of length_list_of_conv_the_enat)
                                  have "lnth (LCons g p) i = llast (LCons g p)" using ‹Suc i = llength (LCons g p)›
                                    by (metis enat_ord_simps(2) lappend_LNil2 ldropn_LNil ldropn_Suc_conv_ldropn ldropn_lappend lessI less_not_refl llast_ldropn llast_singleton)
                                  hence "(lnth (LCons g p') i) = g'" using P
                                    by (simp add: ‹lnth (LCons g p') i = lnth (LCons g p) i›) 
                                  have "(lnth (LCons g p') (Suc i)) = g''"
                                    using p'_def ‹Suc i = the_enat (llength p')›
                                    by (smt (verit) ‹enat (Suc i) < llength (LCons g p')› ‹lfinite p'› ‹llast (LCons g p') = g''› lappend_snocL1_conv_LCons2 ldropn_LNil ldropn_Suc_LCons ldropn_Suc_conv_ldropn ldropn_lappend2 lfinite_llength_enat llast_ldropn llast_singleton the_enat.simps wlog_linorder_le)

                                  have "energy_level e (LCons g p) i = energy_level e (LCons g p') i" 
                                    using energy_level_append A ‹(LCons g p') = lappend (LCons g p) (LCons g'' LNil)›
                                    by presburger
                                  hence "Some e' = (energy_level e (LCons g p') i)" 
                                    using P ‹i = the_enat (llength p)›
                                    by argo 

                                  have "energy_level e (LCons g p') (the_enat (llength p')) = energy_level e (LCons g p') (Suc i)" using ‹Suc i = the_enat (llength p')› by simp
                                  also have "... = apply_w (lnth (LCons g p') i) (lnth (LCons g p') (Suc i)) (the (energy_level e (LCons g p') i))" 
                                    using energy_level.simps el_prems
                                    by (meson leD) 
                                  also have "... = apply_w g' g'' (the (energy_level e (LCons g p') i))" 
                                    using ‹(lnth (LCons g p') i) = g'› ‹(lnth (LCons g p') (Suc i)) = g''› by simp
                                  finally have "energy_level e (LCons g p') (the_enat (llength p')) = (apply_w g' g'' e')" 
                                    using ‹Some e' = (energy_level e (LCons g p') i)›
                                    by (metis option.sel) 
                                  thus "Some (the (apply_w g' g'' e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                                    using ‹apply_w g' g'' e' ≠ None› by auto
                                qed
                              qed
                            qed
                          qed
                        qed

                        have x_len: "(upd (the (weight g' g'')) e') ∈ energies" using y_len
                          using ‹apply_w g' g'' e' ≠ None› ‹weight g' g'' ≠ None› upd_well_defined by blast 

                        thus "x ∈ reachable_positions_len s g e"
                          using X x_def reachable_positions_def
                          by (simp add: mem_Collect_eq) 

                        have "Some (the (apply_w g' g'' e')) = apply_w g' g'' e' ∧
         (if g' ∈ attacker then Some g'' = s e' g' else weight g' g'' ≠ None)"
                        proof
                          show "Some (the (apply_w g' g'' e')) = apply_w g' g'' e'"
                            using ‹apply_w g' g'' e' ≠ None› by auto
                          show "(if g' ∈ attacker then Some g'' = s e' g' else weight g' g'' ≠ None)"
                            using False
                            by (simp add: ‹weight g' g'' ≠ None›) 
                        qed
                        thus "strategy_order s x y" using strategy_order_def x_def ‹y = (g', e')›
                          by simp
                      qed

                      thus "P (g'', (the (apply_w g' g'' e')))" using x_def by simp
                    qed
                  qed
                qed
              qed

              hence "⋀g''. weight g' g'' ≠ None ⟹ ∃e0. S e0 g'' ∧ e0 e≤ (the (apply_w g' g'' e'))" using P_def
                by blast  
              define index where "index = (λg''. SOME e0.  S e0 g'' ∧ e0 e≤ (the (apply_w g' g'' e')))"
              hence I: "⋀g''. weight g' g'' ≠ None ⟹ S (index g'') g'' ∧ (index g'') e≤ (the (apply_w g' g'' e'))" 
                using ‹⋀g''. weight g' g'' ≠ None ⟹ ∃e0. S e0 g'' ∧ e0 e≤ (the (apply_w g' g'' e'))› some_eq_ex
                by (smt (verit, del_insts))
              hence "⋀g''. weight g' g'' ≠ None ⟹ inv_upd (the (weight g' g'')) (index g'') e≤ inv_upd (the (weight g' g'')) (the (apply_w g' g'' e'))"
                using inverse_monotonic P
                by (meson inv_well_defined length_S)
              hence  "⋀g''. weight g' g'' ≠ None ⟹ inv_upd (the (weight g' g'')) (index g'') e≤ e'" 
                using inv_upd_decreasing P
                by (meson I galois length_S y_len)     
              hence all: "∀s. s ∈ {inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None}⟶ s e≤ e'"
                by auto

              have "⋀s'. energy_sup {inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None} ∈ energies ∧ (∀s. s ∈ {inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None} ⟶ s e≤ energy_sup {inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None}) ∧ (s' ∈ energies ∧ (∀s. s ∈ {inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None} ⟶ s e≤ s') ⟶ energy_sup {inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None} e≤ s')"
              proof(rule bounded_join_semilattice)
                show "⋀s'. {inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None} ⊆ energies"
                proof-
                  fix s' 
                  show "{inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None} ⊆ energies"
                    using I inv_well_defined length_S by blast
                qed
                show "⋀s'. finite {inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None}"
                proof-
                  fix s'
                  have "{inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (index g') |g'. g' ∈ positions}" by auto
                  thus "finite {inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None}" using finite_positions
                    using rev_finite_subset by fastforce
                qed
              qed

              hence leq: "energy_sup {inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None} e≤ e'" 
                using all
                using y_len by blast
              have "S (energy_sup {inv_upd (the (weight g' g'')) (index g'')| g''. weight g' g'' ≠ None}) g'" 
                using False S.intros(1) I
                by blast
              thus "P y" using leq P_def
                using ‹y = (g', e')› by blast 
            qed
          qed
        qed
      qed
      thus "e ∈ {e. ∃e'. S e' g ∧ e' e≤ e}" using P_def by simp
    qed
  qed  
  hence "energy_Min {e. ∃e'. S e' g ∧ e' e≤ e} = a_win_min g" by simp

  have "energy_Min {e. ∃e'. S e' g ∧ e' e≤ e} = energy_Min {e. S e g}"
  proof

    have "{e. S e g} ⊆ {e. ∃e'. S e' g ∧ e' e≤ e}"
      using energy_order ordering.eq_iff by fastforce

    show "energy_Min {e. ∃e'. S e' g ∧ e' e≤ e} ⊆ energy_Min {e. S e g}" (* Min von upward-closure ist Min *)
    proof
      fix x
      assume "x ∈ energy_Min {e. ∃e'. S e' g ∧ e' e≤ e}"
      hence "∃e'.  S e' g ∧ e' e≤ x"
        using energy_Min_def by auto
      from this obtain e' where "S e' g ∧ e' e≤ x" by auto
      hence "S e' g ∧ e' e≤ e'" using energy_order ordering_def
        using ordering.eq_iff by fastforce 
      hence "e' ∈ {e. ∃e'. S e' g ∧ e' e≤ e} ∧ e' e≤ x"
        using ‹S e' g ∧ e' e≤ x› by auto 
      hence "x = e'" using energy_Min_def
        using ‹x ∈ energy_Min {e. ∃e'. S e' g ∧ e' e≤ e}› by auto 
      hence "S x g"
        by (simp add: ‹S e' g ∧ e' e≤ x›) 
      show "x ∈ energy_Min {e. S e g}"
      proof(rule ccontr)
        assume "x ∉ energy_Min {e. S e g}"
        hence "∃x'. x' e< x ∧ x' ∈ {e. S e g}"
          using ‹S x g› energy_Min_def
          by auto 
        from this obtain x' where "x' e< x" and "S x' g"
          by auto 
        hence "S x' g ∧ x' e≤ x'" using energy_order ordering_def
          using ordering.eq_iff by fastforce
        hence "x' ∈ {e. ∃e'. S e' g ∧ e' e≤ e}" by auto
        thus "False"
          using ‹x ∈ energy_Min {e. ∃e'. S e' g ∧ e' e≤ e}› unfolding energy_Min_def using ‹x' e< x›
          by auto
      qed
    qed
    show "energy_Min {e. S e g} ⊆ energy_Min {e. ∃e'. S e' g ∧ e' e≤ e} "
    proof
      fix x
      assume "x ∈ energy_Min {e. S e g}"
      hence "S x g" using energy_Min_def by auto
      hence "x ∈  {e. ∃e'. S e' g ∧ e' e≤ e}" using energy_Min_def energy_order ordering_def
        using ordering.eq_iff by fastforce
      show "x ∈ energy_Min {e. ∃e'. S e' g ∧ e' e≤ e} "
      proof(rule ccontr)
        assume "x ∉ energy_Min {e. ∃e'. S e' g ∧ e' e≤ e}"
        from this obtain x' where "x'∈{e. ∃e'. S e' g ∧ e' e≤ e}" and "x' e< x"
          using energy_Min_def
          using ‹x ∈ {e. ∃e'. S e' g ∧ e' e≤ e}› by auto 
        from this(1) obtain e' where "S e' g ∧ e' e≤ x'" by auto
        hence "e' e< x" using ‹x' e< x› energy_order ordering_def
          by (metis (no_types, lifting) ordering_axioms_def partial_preordering_def) 

        thus "False" 
          using ‹S e' g ∧ e' e≤ x'› ‹x ∈ energy_Min {e. S e g}› energy_Min_def
          by auto 
      qed
    qed
  qed

  thus " energy_Min {e. S e g} = a_win_min g" using ‹energy_Min {e. ∃e'. S e' g ∧ e' e≤ e} = a_win_min g› by simp
qed

text‹We now conclude that the algorithm indeed returns the minimal attacker winning budgets.›

lemma a_win_min_is_lfp_sup:
  shows "pareto_sup {(iteration ^^ i) (λg. {}) |. i} = a_win_min"
proof(rule antisymmetry)

  have in_pareto_leq: "⋀n. (iteration ^^ n) (λg. {}) ∈ possible_pareto ∧ (iteration ^^ n) (λg. {}) ≼ a_win_min"
  proof-
    fix n 
    show "(iteration ^^ n) (λg. {}) ∈ possible_pareto ∧ (iteration ^^ n) (λg. {}) ≼ a_win_min"
    proof(induct n)
      case 0
      show ?case 
      proof
        show "(iteration ^^ 0) (λg. {}) ∈ possible_pareto"
          using funpow_simps_right(1) possible_pareto_def by auto
        have "(λg. {}) ≼ a_win_min" 
          unfolding pareto_order_def by simp
        thus "(iteration ^^ 0) (λg. {}) ≼ a_win_min" using funpow_simps_right(1) by simp
      qed
    next
      case (Suc n)
      have "(iteration ^^ (Suc n)) (λg. {}) = iteration ((iteration ^^ n) (λg. {}))" 
        by simp
      then show ?case using Suc iteration_stays_winning iteration_pareto_functor by simp
    qed
  qed

  show "pareto_sup {(iteration ^^ n) (λg. {}) |. n} ∈ possible_pareto"
  proof(rule pareto_sup_is_sup)
    show "{(iteration ^^ n) (λg. {}) |. n} ⊆ possible_pareto"
      using in_pareto_leq by auto
  qed

  show "a_win_min ∈ possible_pareto"
    using a_win_min_in_pareto by simp
 
  show "pareto_sup {(iteration ^^ n) (λg. {}) |. n} ≼ a_win_min"
    using pareto_sup_is_sup in_pareto_leq a_win_min_in_pareto image_iff rangeE
    by (smt (verit) subsetI)

  define Smin where "Smin = (λg. energy_Min {e. S e g})"

  have "Smin ≼ pareto_sup {(iteration ^^ n) (λg. {}) |. n}"
    unfolding pareto_order_def proof
    fix g 
    show "∀e. e ∈ Smin g ⟶
             (∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ e' e≤ e)"
    proof
      fix e
      show "e ∈ Smin g ⟶
         (∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ e' e≤ e)"
      proof
        assume "e ∈ Smin g"
        hence "S e g" using energy_Min_def Smin_def by simp
        thus "∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ e' e≤ e"
        proof(rule S.induct)
          show "⋀g e. g ∉ attacker ∧
           (∃index.
               e =
               energy_sup
                {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ∧
               (∀g'. weight g g' ≠ None ⟶
                     S (index g') g' ∧
                     (∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧
                           e' e≤ index g'))) ⟹
           ∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ e' e≤ e"
          proof-
            fix e g 
            assume A: "g ∉ attacker ∧
           (∃index.
               e =
               energy_sup
                {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ∧
               (∀g'. weight g g' ≠ None ⟶
                     S (index g') g' ∧
                     (∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧
                           e' e≤ index g')))"
            from this obtain index where "e =
               energy_sup
                {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}" and
               "∀g'. weight g g' ≠ None ⟶
                     S (index g') g' ∧
                     (∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧
                           e' e≤ index g')" by auto

            define index' where "index' ≡ λg'. SOME e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧
                           e' e≤ index g'"
            
            have "⋀g'. weight g g' ≠ None ⟹ ∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧
                           e' e≤ index g'" using ‹∀g'. weight g g' ≠ None ⟶
                     S (index g') g' ∧
                     (∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧
                           e' e≤ index g')› by simp
            hence "⋀g'. weight g g' ≠ None ⟹ index' g' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧
                           index' g' e≤ index g'" unfolding index'_def using some_eq_ex
              by (metis (mono_tags, lifting)) 
            hence F: "⋀g'. weight g g' ≠ None ⟹ ∃F. F ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ index' g' ∈ F g'"
              unfolding pareto_sup_def using energy_Min_def by simp
            have index'_len: "⋀g'. weight g g' ≠ None ⟹ (index' g') ∈ energies" 
            proof-
              fix g' 
              assume "weight g g' ≠ None"
              hence "∃F. F ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ index' g' ∈ F g'" using F by auto
              from this obtain F where F: "F ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ index' g' ∈ F g'"
                by auto
              hence "F ∈ possible_pareto"
                using in_pareto_leq by auto 
              thus "(index' g') ∈ energies"
                unfolding possible_pareto_def using F
                using subset_iff by blast 
            qed

            define index_F where "index_F = (λg'. (SOME F. (F ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ index' g' ∈ F g')))"
            have IF: "⋀g'. weight g g' ≠ None ⟹ index_F g' ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ index' g' ∈ index_F g' g'"
              unfolding index_F_def using some_eq_ex ‹⋀g'. weight g g' ≠ None ⟹ ∃F. F ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ index' g' ∈ F g'›
              by (metis (mono_tags, lifting)) 

            have "∃F. (F∈ {(iteration ^^ n) (λg. {}) |. n} ∧ (∀g'. weight g g' ≠ None ⟶ index_F g' ≼ F))"
            proof-
              define P' where "P' = {index_F g'| g'. weight g g' ≠ None}"
              have "∃F'. F' ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ (∀F. F ∈ P' ⟶ F ≼ F')"
              proof(rule finite_directed_set_upper_bound)
                show "⋀F F'.
       F ∈ {(iteration ^^ n) (λg. {}) |. n} ⟹
       F' ∈ {(iteration ^^ n) (λg. {}) |. n} ⟹
       ∃F''. F'' ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ F ≼ F'' ∧ F' ≼ F''"
                proof-
                  fix F F'
                  assume "F ∈ {(iteration ^^ n) (λg. {}) |. n}" and "F' ∈ {(iteration ^^ n) (λg. {}) |. n}"
                  from this obtain n m where "F = (iteration ^^ n) (λg. {})" and "F' = (iteration ^^ m)(λg. {})" by auto
                  show "∃F''. F'' ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ F ≼ F'' ∧ F' ≼ F''"
                  proof
                    show "((iteration ^^ (max n m)) (λg. {})) ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ F ≼ ((iteration ^^ (max n m)) (λg. {})) ∧ F' ≼ ((iteration ^^ (max n m)) (λg. {}))"
                    proof-
                      have "⋀i j. i ≤ j ⟹ ((iteration ^^ i) (λg. {})) ≼ ((iteration ^^ j) (λg. {}))"
                      proof-
                        fix i j 
                        show " i ≤ j ⟹ ((iteration ^^ i) (λg. {})) ≼ ((iteration ^^ j) (λg. {}))"
                        proof-
                          assume "i ≤ j"
                          thus "(iteration ^^ i) (λg. {}) ≼ (iteration ^^ j) (λg. {})"
                          proof(induct "j-i" arbitrary: i j)
                            case 0
                            hence "i = j" by simp
                            then show ?case
                              by (simp add: in_pareto_leq reflexivity) 
                          next
                            case (Suc x)
                            show ?case
                            proof(rule transitivity)
                              show A: "(iteration ^^ i) (λg. {}) ∈ possible_pareto" using in_pareto_leq by simp
                              show B: "(iteration ^^ (Suc i)) (λg. {}) ∈ possible_pareto" using in_pareto_leq by blast
                              show C: "(iteration ^^ j) (λg. {}) ∈ possible_pareto" using in_pareto_leq by simp

                              have D: "(iteration ^^ (Suc i)) (λg. {}) = iteration ((iteration ^^ i) (λg. {}))" using funpow.simps by simp

                              have "((iteration ^^ i) (λg. {})) ≼ iteration ((iteration ^^ i) (λg. {}))"
                              proof(induct i)
                                case 0
                                then show ?case using pareto_minimal_element in_pareto_leq
                                  by simp 
                              next
                                case (Suc i)
                                then show ?case using in_pareto_leq iteration_monotonic funpow.simps(2)
                                  by (smt (verit, del_insts) comp_eq_dest_lhs)
                              qed
                              thus "(iteration ^^ i) (λg. {}) ≼ (iteration ^^ (Suc i)) (λg. {})"
                                unfolding D by simp

                              have "x = j - (Suc i)" using Suc by simp
                              have "(Suc i) ≤ j"
                                using diff_diff_left Suc by simp
                              show "(iteration ^^ (Suc i)) (λg. {}) ≼ (iteration ^^ j) (λg. {})"
                                using Suc ‹x = j - (Suc i)› ‹(Suc i) ≤ j› by blast
                            qed                   
                          qed
                        qed
                      qed
                      thus ?thesis
                        using ‹F = (iteration ^^ n) (λg. {})› ‹F' = (iteration ^^ m)(λg. {})› ‹F' ∈ {(iteration ^^ n) (λg. {}) |. n}› max.cobounded2 by auto 
                    qed
                  qed
                qed

                show "{(iteration ^^ n) (λg. {}) |. n} ≠ {}"
                  by auto 
                show "P' ⊆ {(iteration ^^ n) (λg. {}) |. n}" using P'_def IF
                  by blast 
                have "finite {g'. weight g g' ≠ None}" using finite_positions
                  by (smt (verit) Collect_cong finite_Collect_conjI) 
                thus "finite P'" unfolding P'_def using nonpos_eq_pos
                  by auto
                show "{(iteration ^^ n) (λg. {}) |. n} ⊆ possible_pareto" using in_pareto_leq by auto
              qed
              from this obtain F' where "F' ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ (∀F. F ∈ P' ⟶ F ≼ F')" by auto
              hence "F' ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ (∀g'. weight g g' ≠ None ⟶ index_F g' ≼ F')"
                using P'_def
                by auto
              thus ?thesis by auto
            qed
            from this obtain F' where F': "F' ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ (∀g'. weight g g' ≠ None ⟶ index_F g' ≼ F')" by auto
            
            have IE: "⋀g'. weight g g' ≠ None ⟹ ∃e'. e' ∈ F' g' ∧ e' e≤ index' g'"
            proof-
              fix g'
              assume "weight g g' ≠ None"
              hence "index_F g' ≼ F'" using F' by simp
              thus "∃e'. e' ∈ F' g' ∧ e' e≤ index' g'" unfolding pareto_order_def using IF ‹weight g g' ≠ None›
                by simp
            qed

            define e_index where "e_index = (λg'. SOME e'.  e' ∈ F' g' ∧ e' e≤ index' g')"
            hence "⋀g'. weight g g' ≠ None ⟹ e_index g' ∈ F' g' ∧ e_index g' e≤ index' g'"
              using IE some_eq_ex
              by (metis (no_types, lifting)) 

            have sup_leq1: "energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None} e≤ energy_sup {inv_upd (the (weight g g')) (index' g')| g'. weight g g' ≠ None}"
            proof(cases "{g'. weight g g' ≠ None} = {}")
              case True
              then show ?thesis
                by (simp add: bounded_join_semilattice)
            next
              case False
              hence "{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ≠ {}" by simp
              then show ?thesis 
              proof(rule energy_sup_leq_energy_sup)
                show "⋀a. a ∈ {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⟹
         ∃b∈{inv_upd (the (weight g g')) (index' g') |g'. weight g g' ≠ None}. a e≤ b"
                proof-
                  fix a 
                  assume "a ∈ {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}"
                  from this obtain g' where "weight g g' ≠ None" and "a=inv_upd (the (weight g g')) (e_index g')" by auto
                  have "a e≤ inv_upd (the (weight g g')) (index' g')"
                    unfolding ‹a=inv_upd (the (weight g g')) (e_index g')› 
                    using ‹weight g g' ≠ None› 
                  proof(rule inverse_monotonic)
                    show "e_index g' e≤ index' g'" using ‹⋀g'. weight g g' ≠ None ⟹ e_index g' ∈ F' g' ∧ e_index g' e≤ index' g'› ‹weight g g' ≠ None› by auto
                    hence "(e_index g') ∈ energies" using index'_len ‹weight g g' ≠ None› energy_order ordering_def
                      by (smt (z3) F' ‹⋀g'. weight g g' ≠ None ⟹ e_index g' ∈ F' g' ∧ e_index g' e≤ index' g'› full_SetCompr_eq in_pareto_leq mem_Collect_eq possible_pareto_def subset_iff) 
                    thus "inverse_application (the (weight g g')) (e_index g') ≠ None"
                      using inv_well_defined ‹weight g g' ≠ None›
                      by auto 
                    show "(e_index g') ∈ energies"
                      using ‹(e_index g') ∈ energies› by auto
                  qed
                  thus "∃b∈{inv_upd (the (weight g g')) (index' g') |g'. weight g g' ≠ None}. a e≤ b"
                    using ‹weight g g' ≠ None›
                    by blast 
                qed
                have "⋀g'.  weight g g' ≠ None ⟹ (e_index g') ∈ energies"
                  using index'_len  energy_order ordering_def
                  by (smt (z3) F' ‹⋀g'. weight g g' ≠ None ⟹ e_index g' ∈ F' g' ∧ e_index g' e≤ index' g'› full_SetCompr_eq in_pareto_leq mem_Collect_eq possible_pareto_def subset_iff)
                thus "⋀a. a ∈ {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⟹
         a ∈ energies"
                  using inv_well_defined by blast

                have "{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (e_index g') |g'. g'∈ positions}" by auto                
                thus " finite {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}"
                  using finite_positions finite_image_set rev_finite_subset by fastforce
                have "{inv_upd (the (weight g g'))  (index' g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (index' g') |g'. g'∈ positions}" by auto                
                thus " finite {inv_upd (the (weight g g'))  (index' g') |g'. weight g g' ≠ None}"
                  using finite_positions finite_image_set rev_finite_subset by fastforce
                show "{inv_upd (the (weight g g')) (index' g') |g'. weight g g' ≠ None} ⊆ energies" 
                proof-
                  have "⋀g'. weight g g' ≠ None ⟹ index' g' ∈ energies"
                    by (simp add: index'_len)
                  thus ?thesis
                    using inv_well_defined by blast 
                qed
              qed             
            qed

            have sup_leq2: "energy_sup {inv_upd (the (weight g g')) (index' g')|g'. weight g g' ≠ None} e≤ energy_sup {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}"
            proof(cases "{g'. weight g g' ≠ None} = {}")
              case True
              then show ?thesis
                using sup_leq1 by force 
            next
              case False
              hence "{inv_upd (the (weight g g')) (index' g') |g'. weight g g' ≠ None} ≠ {}" by simp
              then show ?thesis 
              proof(rule energy_sup_leq_energy_sup)
                show "⋀a. a ∈ {inv_upd (the (weight g g')) (index' g') |g'. weight g g' ≠ None} ⟹
         ∃b∈{inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}. a e≤ b"
                proof-
                  fix a 
                  assume "a ∈ {inv_upd (the (weight g g')) (index' g') |g'. weight g g' ≠ None}"
                  from this obtain g' where "weight g g' ≠ None" and "a=inv_upd (the (weight g g')) (index' g')" by auto
                  hence "a e≤ inv_upd (the (weight g g')) (index g')"
                    using inverse_monotonic  ‹⋀g'. weight g g' ≠ None ⟹ e_index g' ∈ F' g' ∧ e_index g' e≤ index' g'› F' possible_pareto_def
                    using ‹⋀g'. weight g g' ≠ None ⟹ index' g' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧ index' g' e≤ index g'› energy_order
                    by (meson inv_well_defined index'_len) 
                  thus "∃b∈{inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}. a e≤ b"
                    using ‹weight g g' ≠ None›
                    by blast 
                qed
                show "⋀a. a ∈ {inv_upd (the (weight g g')) (index' g') |g'. weight g g' ≠ None} ⟹
         a ∈ energies"
                  using index'_len inv_well_defined by blast 

                have "{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (e_index g') |g'. g'∈ positions}" by auto 
                thus " finite {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}"
                  using finite_positions finite_image_set rev_finite_subset by fastforce
                have "{inv_upd (the (weight g g'))  (index' g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (index' g') |g'. g'∈ positions}" by auto                
                thus " finite {inv_upd (the (weight g g'))  (index' g') |g'. weight g g' ≠ None}"
                  using finite_positions finite_image_set rev_finite_subset by fastforce
                show " {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None} ⊆ energies"
                  using inv_well_defined
                  by (smt (verit, best) ‹⋀g'. weight g g' ≠ None ⟹ index' g' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧ index' g' e≤ index g'› galois_energy_game.upward_closed_energies galois_energy_game_axioms index'_len mem_Collect_eq subsetI)
              qed             
            qed
            

            have "⋀g'. weight g g' ≠ None ⟹ (e_index g') ∈ energies" 
            proof-
              fix g'
              assume "weight g g' ≠ None"
              hence "e_index g' ∈ F' g' ∧ e_index g' e≤ index' g'" using ‹⋀g'. weight g g' ≠ None ⟹ e_index g' ∈ F' g' ∧ e_index g' e≤ index' g'›
                by simp
              thus "(e_index g') ∈ energies" using F' possible_pareto_def
                using in_pareto_leq by blast 
            qed
            hence es_in: "energy_sup {inv_upd (the (weight g g')) (e_index g')|g'. weight g g' ≠ None} ∈ {energy_sup
                        {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} |
                       e_index.
                       ∀g'. weight g g' ≠ None ⟶
                            (e_index g') ∈ energies ∧ e_index g' ∈ F' g'}"
              using ‹⋀g'. weight g g' ≠ None ⟹ e_index g' ∈ F' g' ∧ e_index g' e≤ index' g'›
              by blast 
            have "{energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} |e_index. ∀g'. weight g g' ≠ None ⟶ e_index g' ∈ energies ∧ e_index g' ∈ F' g'} ⊆ energies" 
            proof
              fix x 
              assume "x ∈ {energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} |e_index. ∀g'. weight g g' ≠ None ⟶ e_index g' ∈ energies ∧ e_index g' ∈ F' g'}"
              from this obtain e_index where "x = energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}" and "∀g'. weight g g' ≠ None ⟶ e_index g' ∈ energies ∧ e_index g' ∈ F' g'"
                by auto
              have "{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⊆ {inv_upd (the (weight g g')) (e_index g') |g'. g'∈ positions}"
                by auto
              hence fin: "finite {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}"
                using finite_positions
                by (simp add: Collect_mem_eq finite_image_set rev_finite_subset)
              have "{inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} ⊆ energies"
                using inv_well_defined
                using ‹∀g'. weight g g' ≠ None ⟶ e_index g' ∈ energies ∧ e_index g' ∈ F' g'› by blast 
              thus "x ∈ energies" unfolding ‹x = energy_sup {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None}› using bounded_join_semilattice fin
                by simp
            qed
            hence "∃em. em ∈  energy_Min
                      {energy_sup
                        {inv_upd (the (weight g g')) (e_index g') |g'. weight g g' ≠ None} |
                       e_index.
                       ∀g'. weight g g' ≠ None ⟶
                            (e_index g') ∈ energies ∧ e_index g' ∈ F' g'} 
                  ∧ em e≤ energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}"
              using energy_Min_contains_smaller es_in
              by meson 
            hence "∃em. em∈ iteration F' g ∧ em e≤ energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}"
              unfolding iteration_def using A
              by simp 
            from this obtain em where EM: "em ∈ iteration F' g ∧ em e≤ energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}"
              by auto
            from F' have F': "iteration F' ∈ {(iteration ^^ n) (λg. {}) |. n}" using funpow.simps image_iff rangeE
              by (smt (z3) UNIV_I comp_eq_dest_lhs)
            hence EM0:  "em ∈ {e. ∃F. F ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ e ∈ F g}" 
              using EM by auto
            have "{e. ∃F. F ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ e ∈ F g} ⊆ energies"
              using possible_pareto_def
              using in_pareto_leq by fastforce 
            hence "∃em'. em' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ em' e≤ em"
              unfolding pareto_sup_def using F' energy_Min_contains_smaller EM0 by meson 
            from this obtain em' where EM': "em' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ em' e≤ em" by auto
            hence "em' e≤ em" by simp
            hence "em' e≤ energy_sup {inv_upd (the (weight g g')) (e_index g')| g'. weight g g' ≠ None}" using EM energy_order ordering_def 
              by (metis (no_types, lifting) partial_preordering_def) 
            hence  "em' e≤ energy_sup {inv_upd (the (weight g g')) (index' g') |g'. weight g g' ≠ None}" using sup_leq1 energy_order ordering_def 
              by (metis (no_types, lifting) partial_preordering_def) 
            hence "em'  e≤ energy_sup {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}" using sup_leq2 energy_order ordering_def 
              by (metis (no_types, lifting) partial_preordering_def) 
            hence "em' e≤ e" using  ‹e =
               energy_sup
                {inv_upd (the (weight g g')) (index g') |g'. weight g g' ≠ None}› energy_order ordering_def
              by (metis (no_types, lifting) partial_preordering_def) 

            thus " ∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ e' e≤ e"
              using EM' by auto
          qed

          show "⋀g e. g ∈ attacker ∧
           (∃g'. weight g g' ≠ None ∧
                 (∃e'. (S e' g' ∧
                        (∃e'a. e'a ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧ e'a e≤ e')) ∧
                       e = inv_upd (the (weight g g')) e')) ⟹
           ∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ e' e≤ e"
          proof-
            fix g e 
            assume A: "g ∈ attacker ∧
           (∃g'. weight g g' ≠ None ∧
                 (∃e'. (S e' g' ∧
                        (∃e'a. e'a ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧ e'a e≤ e')) ∧
                       e = inv_upd (the (weight g g')) e'))"
            from this obtain g' e' e'' where " weight g g' ≠ None" and "S e' g'" and "e = inv_upd (the (weight g g')) e'" and 
                      "e'' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧ e'' e≤ e'" by auto
            
            have "e'' ∈ energies" using ‹e'' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧ e'' e≤ e'› in_pareto_leq possible_pareto_def
              using ‹pareto_sup {(iteration ^^ n) (λg. {}) |. n} ∈ possible_pareto› by blast
            have "inv_upd (the (weight g g')) e'' e≤ inv_upd (the (weight g g')) e'"
              using ‹weight g g' ≠ None›
            proof(rule inverse_monotonic)
              show "e'' e≤ e'" using ‹e'' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧ e'' e≤ e'› by auto
              have "e' ∈ energies" using length_S ‹weight g g' ≠ None› ‹S e' g'› by auto 
              show "inverse_application (the (weight g g')) e'' ≠ None"
                using inv_well_defined ‹weight g g' ≠ None› ‹e'' ∈ energies›
                by blast 
              show "e'' ∈ energies"
                by (simp add: ‹e'' ∈ energies›)
            qed
            have "e'' ∈ energy_Min {e. ∃F. F ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ e ∈ F g'}"
              using ‹e'' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧ e'' e≤ e'› unfolding pareto_sup_def by simp
            hence "∃n. e'' ∈ (iteration ^^ n) (λg. {}) g'"
              using energy_Min_def
              by auto 
            from this obtain n where "e'' ∈ (iteration ^^ n) (λg. {}) g'" by auto

            hence e''in: "inv_upd (the (weight g g')) e'' ∈ {inv_upd (the (weight g g')) e' |e' g'.
           e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ (iteration ^^ n) (λg. {}) g'}"
              using ‹weight g g' ≠ None› length_S ‹S e' g'› ‹e'' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g' ∧ e'' e≤ e'› ‹e'' ∈ energies› by blast 

            define Fn where "Fn =  (iteration ^^ n) (λg. {})"
            have "{inv_upd (the (weight g g')) e' |e' g'. e' ∈ energies ∧ weight g g' ≠ None ∧ e' ∈ Fn g'} ⊆ energies"
              using inv_well_defined by auto 
            hence "∃e'''. e''' ∈ iteration Fn g ∧ e''' e≤ inv_upd (the (weight g g')) e''"
              unfolding iteration_def using Fn_def energy_Min_contains_smaller A e''in
              by meson
            from this obtain e''' where E''': "e''' ∈ iteration ((iteration ^^ n) (λg. {})) g ∧ e''' e≤ inv_upd (the (weight g g')) e''"
              using Fn_def by auto 
            hence "e''' ∈ ((iteration ^^ (Suc n)) (λg. {})) g" by simp
            hence E'''1:  "e''' ∈ {e. ∃F. F ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ e ∈ F g}" by blast
            have "{e. ∃F. F ∈ {(iteration ^^ n) (λg. {}) |. n} ∧ e ∈ F g} ⊆ energies"
              using possible_pareto_def in_pareto_leq by blast
            hence "∃em. em ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ em e≤ e'''"
              unfolding pareto_sup_def using energy_Min_contains_smaller E'''1
              by meson
            from this obtain em where EM: "em ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ em e≤ e'''" by auto

            show " ∃e'. e' ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ e' e≤ e"
            proof
              show "em ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g ∧ em e≤ e"
              proof
                show "em ∈ pareto_sup {(iteration ^^ n) (λg. {}) |. n} g" using EM by simp
                have "inv_upd (the (weight g g')) e'' e≤ e"
                  using ‹e = inv_upd (the (weight g g')) e'› ‹inv_upd (the (weight g g')) e'' e≤ inv_upd (the (weight g g')) e'› by simp
                hence "e''' e≤ e" using E''' energy_order ordering_def
                  by (metis (mono_tags, lifting) partial_preordering_def) 
                thus "em e≤ e" using EM energy_order ordering_def
                  by (metis (mono_tags, lifting) partial_preordering_def) 
              qed
            qed
          qed
        qed
      qed
    qed
  qed

  thus "a_win_min ≼ pareto_sup {(iteration ^^ n) (λg. {}) |. n}" 
    using a_win_min_is_minS Smin_def by simp
qed

text‹We can argue that the algorithm always terminates by showing that only finitely many iterations 
are needed before a fixed point (the minimal attacker winning budgets) is reached.›

lemma finite_iterations: 
  shows "∃i. a_win_min = (iteration ^^ i) (λg. {})"
proof
  have in_pareto_leq: "⋀n. (iteration ^^ n) (λg. {}) ∈ possible_pareto ∧ (iteration ^^ n) (λg. {}) ≼ a_win_min"
  proof-
    fix n 
    show "(iteration ^^ n) (λg. {}) ∈ possible_pareto ∧ (iteration ^^ n) (λg. {}) ≼ a_win_min"
    proof(induct n)
      case 0
      show ?case 
      proof
        show "(iteration ^^ 0) (λg. {}) ∈ possible_pareto"
          using funpow.simps possible_pareto_def by auto
        have "(λg. {}) ≼ a_win_min" 
          unfolding pareto_order_def by simp
        thus "(iteration ^^ 0) (λg. {}) ≼ a_win_min" using funpow.simps by simp
      qed
    next
      case (Suc n)
      have "(iteration ^^ (Suc n)) (λg. {}) = iteration ((iteration ^^ n) (λg. {}))" 
        using funpow.simps by simp
      then show ?case using Suc iteration_stays_winning iteration_pareto_functor by simp
    qed
  qed

  have A: "⋀g n m e. n ≤ m ⟹  e ∈ a_win_min g ⟹ e∈ (iteration ^^ n) (λg. {}) g ⟹ e ∈ (iteration ^^ m)(λg. {}) g"
  proof-
    fix g n m e 
    assume "n ≤ m" and "e ∈ a_win_min g" and "e∈ (iteration ^^ n) (λg. {}) g"
    thus "e∈(iteration ^^ m)(λg. {}) g"
    proof(induct "m-n" arbitrary: n m)
      case 0
      then show ?case by simp
    next
      case (Suc x)
      hence "Suc n ≤ m"
        by linarith 
      have "x = m - (Suc n)" using Suc by simp
      have "e ∈ (iteration ^^ (Suc n)) (λg. {}) g"
      proof-
        have "(iteration ^^ n) (λg. {}) ≼ (iteration ^^ (Suc n)) (λg. {})"
        proof(induct n)
          case 0
          then show ?case
            by (simp add: pareto_minimal_element)
        next
          case (Suc n)
          have "(iteration ^^ (Suc (Suc n))) (λg. {}) = iteration ((iteration ^^ (Suc n)) (λg. {}))" 
            using funpow.simps by simp
          then show ?case using Suc iteration_monotonic in_pareto_leq funpow.simps(2)
            by (smt (verit) comp_apply)
        qed
        hence "∃e'. e' ∈ (iteration ^^ (Suc n)) (λg. {}) g ∧ e' e≤ e"
          unfolding pareto_order_def using Suc by simp
        from this obtain e' where "e' ∈ (iteration ^^ (Suc n)) (λg. {}) g ∧ e' e≤ e" by auto
        hence "(∃e''. e'' ∈ a_win_min g ∧ e'' e≤ e')" using in_pareto_leq unfolding pareto_order_def
          by blast 
        from this obtain e'' where "e'' ∈ a_win_min g ∧ e'' e≤ e'" by auto
        hence "e'' = e" using Suc energy_Min_def ‹e' ∈ (iteration ^^ (Suc n)) (λg. {}) g ∧ e' e≤ e›
          by (smt (verit, ccfv_SIG) mem_Collect_eq upwards_closure_wb_len)
        hence "e = e'" using ‹e' ∈ (iteration ^^ (Suc n)) (λg. {}) g ∧ e' e≤ e› ‹e'' ∈ a_win_min g ∧ e'' e≤ e'›
          by (meson energy_order ordering.antisym)
        thus ?thesis using ‹e' ∈ (iteration ^^ (Suc n)) (λg. {}) g ∧ e' e≤ e› by simp
      qed
      then show ?case using Suc ‹x = m - (Suc n)› ‹Suc n ≤ m› by auto
    qed
  qed
  hence A1: "⋀g n m. n ≤ m ⟹  a_win_min g = (iteration ^^ n) (λg. {}) g ⟹  a_win_min g = (iteration ^^ m)(λg. {}) g"
  proof-
    fix g n m 
    assume "n ≤ m" and "a_win_min g = (iteration ^^ n) (λg. {}) g"
    show "a_win_min g = (iteration ^^ m)(λg. {}) g"
    proof
      show "a_win_min g ⊆ (iteration ^^ m)(λg. {}) g"
      proof
        fix e
        assume "e ∈ a_win_min g"
        hence "e ∈ (iteration ^^ n) (λg. {}) g" using ‹a_win_min g = (iteration ^^ n) (λg. {}) g› by simp
        thus "e ∈ (iteration ^^ m)(λg. {}) g" using A ‹n ≤ m› ‹e ∈ a_win_min g› by auto
      qed
      show "(iteration ^^ m)(λg. {}) g ⊆ a_win_min g"
      proof
        fix e
        assume "e ∈ (iteration ^^ m)(λg. {}) g"
        hence "∃e'. e' ∈ a_win_min g ∧ e' e≤ e" using in_pareto_leq unfolding pareto_order_def by auto
        from this obtain e' where "e' ∈ a_win_min g ∧ e' e≤ e" by auto
        hence "e' ∈ (iteration ^^ n) (λg. {}) g" using ‹a_win_min g = (iteration ^^ n) (λg. {}) g› by simp
        hence "e' ∈ (iteration ^^ m)(λg. {}) g" using A ‹n ≤ m› ‹e' ∈ a_win_min g ∧ e' e≤ e› by simp
        hence "e = e'" using in_pareto_leq unfolding possible_pareto_def
          using ‹e ∈ (iteration ^^ m)(λg. {}) g› ‹e' ∈ a_win_min g ∧ e' e≤ e› by blast 
        thus "e ∈ a_win_min g" using ‹e' ∈ a_win_min g ∧ e' e≤ e› by simp
      qed
    qed
  qed

  have "⋀g e. e ∈ a_win_min g ⟹ ∃n. e ∈ (iteration ^^ n) (λg. {}) g"
  proof-
    fix g e
    assume "e ∈ a_win_min g"
    hence "e ∈ (pareto_sup {(iteration ^^ n) (λg. {}) |. n}) g" using a_win_min_is_lfp_sup finite_positions nonpos_eq_pos by simp
    thus "∃n. e ∈ (iteration ^^ n) (λg. {}) g" unfolding pareto_sup_def energy_Min_def
      by auto 
  qed
  define n_e where "n_e = (λ g e. SOME n. e ∈ (iteration ^^ n) (λg. {}) g)"
  hence "⋀g e. n_e g e = (SOME n. e ∈ (iteration ^^ n) (λg. {}) g)"
    by simp
  hence n_e: "⋀g e. e ∈ a_win_min g ⟹ e ∈ (iteration ^^ (n_e g e)) (λg. {}) g"
    using some_eq_ex ‹⋀g e. e ∈ a_win_min g ⟹ ∃n. e ∈ (iteration ^^ n) (λg. {}) g›
    by metis

  have fin_e: "⋀g. finite {n_e g e | e. e ∈ a_win_min g}"
    using minimal_winning_budget_finite by fastforce  
  define m_g where "m_g = (λg. Max {n_e g e | e. e ∈ a_win_min g})"
  hence n_e_leq: "⋀g e. e ∈ a_win_min g ⟹ n_e g e ≤ m_g g" using A fin_e
    using Collect_mem_eq Max.coboundedI by fastforce 
  have MG: "⋀g. a_win_min g = (iteration ^^ (m_g g)) (λg. {}) g"
  proof
    fix g 
    show "a_win_min g ⊆ (iteration ^^ (m_g g)) (λg. {}) g"
    proof
      fix e 
      assume "e∈ a_win_min g" 
      hence "e ∈ (iteration ^^ (n_e g e)) (λg. {}) g"
        using n_e by simp
      thus "e ∈ (iteration ^^ (m_g g)) (λg. {}) g"
        using A ‹e∈ a_win_min g› n_e_leq
        by blast 
    qed
    show "(iteration ^^ (m_g g)) (λg. {}) g ⊆ a_win_min g"
    proof
      fix e 
      assume "e ∈ (iteration ^^ (m_g g)) (λg. {}) g"
      hence "∃e'. e' ∈ a_win_min g ∧ e' e≤ e" 
        using in_pareto_leq unfolding pareto_order_def      
        by simp 
      from this obtain e' where "e' ∈ a_win_min g ∧ e' e≤ e" by auto
      hence "e' ∈ (iteration ^^ (m_g g)) (λg. {}) g" using ‹a_win_min g ⊆ (iteration ^^ (m_g g)) (λg. {}) g› by auto
      hence "e = e'" using ‹e' ∈ a_win_min g ∧ e' e≤ e› in_pareto_leq unfolding possible_pareto_def
        using ‹e ∈ (iteration ^^ (m_g g)) (λg. {}) g› by blast 
      thus "e ∈ a_win_min g" using ‹e' ∈ a_win_min g ∧ e' e≤ e› by auto
    qed
  qed

  have fin_m: "finite {m_g g| g. g∈positions}"
  proof-
    have "finite {p. p ∈ positions}"
      using finite_positions by fastforce
    then show ?thesis
      using finite_image_set by blast
  qed
  hence "⋀g. m_g g ≤ Max {m_g g| g. g ∈ positions}"
    using Max_ge by blast 
  have "⋀g. a_win_min g = (iteration ^^ (Max {m_g g| g. g ∈ positions})) (λg. {}) g"
  proof-
    fix g 
    have G: "a_win_min g = (iteration ^^ (m_g g)) (λg. {}) g" using MG by simp

    from fin_m have "⋀g. m_g g ≤ Max {m_g g| g. g ∈ positions}"
      using Max_ge by blast
    thus "a_win_min g = (iteration ^^ (Max {m_g g| g. g ∈ positions})) (λg. {}) g"
      using A1 G by simp
  qed

  hence "a_win_min ≼ (iteration ^^ (Max {m_g g| g. g ∈ positions})) (λg. {})" 
    using pareto_order_def
    using in_pareto_leq by auto
  thus "a_win_min = (iteration ^^ (Max {m_g g| g. g ∈ positions})) (λg. {})"
    using in_pareto_leq ‹⋀g. a_win_min g = (iteration ^^ (Max {m_g g| g. g ∈ positions})) (λg. {}) g› by auto
qed

subsection‹Applying Kleene's Fixed Point Theorem›

text‹We now establish compatablity with Complete\_Non\_Orders.thy.›

sublocale attractive possible_pareto pareto_order
  unfolding attractive_def using pareto_partial_order(2,3) 
  by (smt (verit) attractive_axioms_def semiattractiveI transp_on_def)

abbreviation pareto_order_dual (infix "≽" 80) where 
  "pareto_order_dual ≡ (λx y. y ≼ x)"

text‹We now conclude, that Kleene's fixed point theorem is applicable.›

lemma kleene_lfp_iteration:
  shows "extreme_bound possible_pareto (≼) {(iteration ^^ i) (λg. {}) |. i} =
        extreme {s ∈ possible_pareto. sympartp (≼) (iteration s) s} (≽)"
proof(rule kleene_qfp_is_dual_extreme)
  show "omega_chain-complete possible_pareto (≼)"
    unfolding omega_chain_def complete_def 
  proof
    fix P 
    show "P ⊆ possible_pareto ⟶
         (∃f. monotone (≤) (≼) f ∧ range f = P) ⟶ (∃s. extreme_bound possible_pareto (≼) P s)"
    proof
      assume "P ⊆ possible_pareto"
      show "(∃f. monotone (≤) (≼) f ∧ range f = P) ⟶ (∃s. extreme_bound possible_pareto (≼) P s) "
      proof
        assume "∃f. monotone (≤) (≼) f ∧ range f = P"
        show "∃s. extreme_bound possible_pareto (≼) P s"
        proof
          show "extreme_bound possible_pareto (≼) P (pareto_sup P)"
            unfolding extreme_bound_def extreme_def using pareto_sup_is_sup
            using ‹P ⊆ possible_pareto› by fastforce
        qed
      qed
    qed
  qed
  show "omega_chain-continuous possible_pareto (≼) possible_pareto (≼) iteration"
    using finite_positions iteration_scott_continuous scott_continuous_imp_omega_continuous by simp
  show "(λg. {}) ∈ possible_pareto"
    unfolding possible_pareto_def
    by simp
  show "∀x∈possible_pareto. x ≽ (λg. {})"
    using pareto_minimal_element
    by simp
qed

text‹We now apply Kleene's fixed point theorem, showing that minimal attacker winning budgets are the least fixed point.›

lemma a_win_min_is_lfp:
  shows "extreme {s ∈ possible_pareto. (iteration s) = s} (≽) a_win_min"
proof-
  have in_pareto_leq: "⋀n. (iteration ^^ n) (λg. {}) ∈ possible_pareto ∧ (iteration ^^ n) (λg. {}) ≼ a_win_min"
  proof-
    fix n 
    show "(iteration ^^ n) (λg. {}) ∈ possible_pareto ∧ (iteration ^^ n) (λg. {}) ≼ a_win_min"
    proof(induct n)
      case 0
      show ?case 
      proof
        show "(iteration ^^ 0) (λg. {}) ∈ possible_pareto"
          using funpow.simps possible_pareto_def by auto
        have "(λg. {}) ≼ a_win_min" 
          unfolding pareto_order_def by simp
        thus "(iteration ^^ 0) (λg. {}) ≼ a_win_min" using funpow.simps by simp
      qed
    next
      case (Suc n)
      have "(iteration ^^ (Suc n)) (λg. {}) = iteration ((iteration ^^ n) (λg. {}))" 
        using funpow.simps by simp
      then show ?case using Suc iteration_stays_winning iteration_pareto_functor by simp
    qed
  qed

  have "extreme_bound possible_pareto (≼) {(iteration ^^ n) (λg. {}) |. n} a_win_min"
  proof
    show "⋀b. bound {(iteration ^^ n) (λg. {}) |. n} (≼) b ⟹ b ∈ possible_pareto ⟹ b ≽ a_win_min"
    proof-
      fix b 
      assume "bound {(iteration ^^ n) (λg. {}) |. n} (≼) b" and "b ∈ possible_pareto"
      hence "⋀n. (iteration ^^ n) (λg. {}) ≼ b"
        by blast  
      hence "pareto_sup {(iteration ^^ n) (λg. {}) |. n} ≼ b" 
        using pareto_sup_is_sup in_pareto_leq ‹b ∈ possible_pareto›
        using nonpos_eq_pos finite_iterations a_win_min_is_lfp_sup by auto
      thus "b ≽ a_win_min" 
        using nonpos_eq_pos a_win_min_is_lfp_sup
        by simp 
    qed
    show "⋀x. x ∈ {(iteration ^^ n) (λg. {}) |. n} ⟹ a_win_min ≽ x"
    proof-
      fix F
      assume "F ∈ {(iteration ^^ n) (λg. {}) |. n}"
      thus "a_win_min ≽ F" 
        using pareto_sup_is_sup in_pareto_leq by force 
    qed

    show "a_win_min ∈ possible_pareto"
      by (simp add: a_win_min_in_pareto)
  qed

  thus "extreme {s ∈ possible_pareto. (iteration s) = s} (≽) a_win_min"
    using kleene_lfp_iteration nonpos_eq_pos
    by (smt (verit, best) Collect_cong antisymmetry iteration_pareto_functor reflexivity sympartp_def) 
qed

end
end