Theory Energy_Game

section ‹Energy Games›

theory Energy_Game
  imports Coinductive.Coinductive_List Open_Induction.Restricted_Predicates 
begin

text‹Energy games are two-player zero-sum games with perfect information played on labeled directed graphs. 
The labels contain information on how each edge affects the current energy.
We call the two players attacker and defender.
In this theory we give fundamental definitions of plays, energy levels and (winning) attacker strategies.
(This corresponds to section 2.1 and 2.2 in the preprint~\cite{preprint}.)›

locale energy_game =
  fixes attacker ::  "'position set" and 
        weight :: "'position ⇒ 'position ⇒ 'label option" and
        application :: "'label ⇒ 'energy ⇒ 'energy option" 
begin 

abbreviation "positions ≡ {g. g ∈ attacker ∨ g ∉ attacker}"
abbreviation "apply_w g g' ≡ application (the (weight g g'))"

text‹\subsubsection*{Plays}

A play is a possibly infinite walk in the underlying directed graph.›

coinductive valid_play :: "'position llist ⇒ bool" where
  "valid_play LNil" |
  "valid_play (LCons v LNil)" |
  "⟦weight v (lhd Ps) ≠ None; valid_play Ps; ¬lnull Ps⟧
    ⟹ valid_play (LCons v Ps)"

text‹The following lemmas follow directly from the definition ‹valid_play›. 
In particular, a play is valid if and only if for each position there is an edge to its successor 
in the play. We show this using the coinductive definition by first establishing coinduction. ›

lemma valid_play_append:
  assumes "valid_play (LCons v Ps)" and "lfinite (LCons v Ps)" and 
          "weight (llast (LCons v Ps)) v' ≠ None" and "valid_play (LCons v' Ps')"
  shows "valid_play (lappend (LCons v Ps) (LCons v' Ps'))"
using assms proof(induction "list_of Ps" arbitrary: v Ps)
  case Nil
  then show ?case using valid_play.simps
    by (metis lappend_code(2) lappend_lnull1 lfinite_LCons lhd_LCons lhd_LCons_ltl list.distinct(1) list_of_LCons llast_singleton llist.collapse(1) llist.disc(2))
next
  case (Cons a x)
  then show ?case using valid_play.simps
    by (smt (verit) lappend_code(2) lfinite_LCons lfinite_llist_of lhd_lappend list_of_llist_of llast_LCons llist.discI(2) llist.distinct(1) llist_of.simps(2) llist_of_list_of ltl_simps(2) valid_play.intros(3))
qed

lemma valid_play_coinduct:
  assumes "Q p" and  
          "⋀v Ps. Q (LCons v Ps) ⟹ Ps≠LNil ⟹ Q Ps ∧ weight v (lhd Ps) ≠ None"
  shows "valid_play p"
  using assms proof(coinduction arbitrary: p)
  case valid_play
  then show ?case 
  proof (cases "p = LNil")
    case True
    then show ?thesis by simp
  next
    case False
    then show ?thesis 
    proof(cases "(∃v. p = LCons v LNil)")
      case True
      then show ?thesis by simp
    next
      case False
      hence "∃v Ps. p = LCons v Ps ∧ ¬ lnull Ps" using ‹¬p = LNil›
        by (metis llist.collapse(1) not_lnull_conv)
      from this obtain v Ps where "p = LCons v Ps ∧ ¬ lnull Ps" by blast
      hence "Q Ps ∧ weight v (lhd Ps) ≠ None" using valid_play
        using llist.disc(1) by blast 
      then show ?thesis using valid_play.simps valid_play
        using ‹p = LCons v Ps ∧ ¬ lnull Ps› by blast 
    qed
  qed
qed

lemma valid_play_nth_not_None:
  assumes "valid_play p" and "Suc i < llength p"
  shows "weight (lnth p i) (lnth p (Suc i)) ≠ None"
proof- 
  have "∃prefix p'. p = lappend prefix p' ∧ llength prefix = Suc i ∧ weight (llast prefix) (lhd p') ≠ None ∧ valid_play p'"
    using assms proof(induct i)
    case 0
    hence "∃v Ps. p = LCons v Ps"
      by (metis llength_LNil neq_LNil_conv not_less_zero) 
    from this obtain v Ps where "p = LCons v Ps" by auto
    hence "p = lappend (LCons v LNil) Ps"
      by (simp add: lappend_code(2)) 
    have "llength (LCons v LNil) = Suc 0" using one_eSuc one_enat_def by simp
    have "weight v (lhd Ps) ≠ None" using 0 valid_play.simps ‹p = LCons v Ps›
      by (smt (verit) One_nat_def add.commute gen_llength_code(1) gen_llength_code(2) less_numeral_extra(4) lhd_LCons llength_code llist.distinct(1) ltl_simps(2) one_enat_def plus_1_eq_Suc) 
    hence "p = lappend (LCons v LNil) Ps ∧ llength (LCons v LNil) = Suc 0 ∧ weight (llast (LCons v LNil)) (lhd Ps) ≠ None" using ‹p = LCons v Ps›
      using ‹p = lappend (LCons v LNil) Ps› ‹llength (LCons v LNil) = Suc 0›
      by simp
    hence "p = lappend (LCons v LNil) Ps ∧ llength (LCons v LNil) = Suc 0 ∧ weight (llast (LCons v LNil)) (lhd Ps) ≠ None ∧ valid_play Ps" using valid_play.simps 0
      by (metis (no_types, lifting) ‹p = LCons v Ps› llist.distinct(1) ltl_simps(2)) 
    then show ?case by blast
  next
    case (Suc l)
    hence "∃prefix p'. p = lappend prefix p' ∧ llength prefix = enat (Suc l) ∧ weight (llast prefix) (lhd p') ≠ None ∧ valid_play p'"
      using Suc_ile_eq order_less_imp_le by blast
    from this obtain prefix p' where P: "p = lappend prefix p' ∧ llength prefix = enat (Suc l) ∧ weight (llast prefix) (lhd p') ≠ None ∧ valid_play p'" by auto
    have "p = lappend (lappend prefix (LCons (lhd p') LNil)) (ltl p') ∧ llength (lappend prefix (LCons (lhd p') LNil)) = enat (Suc (Suc l)) ∧ weight (llast (lappend prefix (LCons (lhd p') LNil))) (lhd (ltl p')) ≠ None ∧ valid_play (ltl p')"
    proof
      show "p = lappend (lappend prefix (LCons (lhd p') LNil)) (ltl p')" using P
        by (metis Suc.prems(2) enat_ord_simps(2) lappend_LNil2 lappend_snocL1_conv_LCons2 lessI llist.exhaust_sel order.asym) 
      show "llength (lappend prefix (LCons (lhd p') LNil)) = enat (Suc (Suc l)) ∧
    weight (llast (lappend prefix (LCons (lhd p') LNil))) (lhd (ltl p')) ≠ None ∧ valid_play (ltl p')"
      proof
        have "llength (lappend prefix (LCons (lhd p') LNil)) = 1+ (llength prefix)"
          by (smt (verit, best) add.commute epred_1 epred_inject epred_llength llength_LNil llength_eq_0 llength_lappend llist.disc(2) ltl_simps(2) zero_neq_one)
        thus "llength (lappend prefix (LCons (lhd p') LNil)) = enat (Suc (Suc l))" using P
          by (simp add: one_enat_def) 
        show "weight (llast (lappend prefix (LCons (lhd p') LNil))) (lhd (ltl p')) ≠ None ∧ valid_play (ltl p') "
        proof
          show "weight (llast (lappend prefix (LCons (lhd p') LNil))) (lhd (ltl p')) ≠ None" using P valid_play.simps
            by (metis Suc.prems(2) ‹llength (lappend prefix (LCons (lhd p') LNil)) = 1 + llength prefix› ‹llength (lappend prefix (LCons (lhd p') LNil)) = enat (Suc (Suc l))› ‹p = lappend (lappend prefix (LCons (lhd p') LNil)) (ltl p')› add.commute enat_add_mono eq_LConsD lappend_LNil2 less_numeral_extra(4) llast_lappend_LCons llast_singleton llength_eq_enat_lfiniteD ltl_simps(1))
          show "valid_play (ltl p')" using P valid_play.simps
            by (metis (full_types) energy_game.valid_play.intros(1) ltl_simps(1) ltl_simps(2)) 
        qed
      qed
    qed
    then show ?case by blast
  qed
  thus ?thesis
    by (smt (z3) assms(2) cancel_comm_monoid_add_class.diff_cancel eSuc_enat enat_ord_simps(2) lappend_eq_lappend_conv lappend_lnull2 lessI lhd_LCons_ltl linorder_neq_iff llast_conv_lnth lnth_0 lnth_lappend the_enat.simps)
qed

lemma valid_play_nth:
  assumes "⋀i. enat (Suc i) < llength p 
               ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None"
  shows "valid_play p"
  using assms proof(coinduction arbitrary: p rule: valid_play_coinduct)
  show "⋀v Ps p.
       LCons v Ps = p ⟹
       ∀i. enat (Suc i) < llength p ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None ⟹
       Ps ≠ LNil ⟹
       (∃p. Ps = p ∧ (∀i. enat (Suc i) < llength p ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None)) ∧
       weight v (lhd Ps) ≠ None"
  proof-
    fix v Ps p
    show "LCons v Ps = p ⟹
       ∀i. enat (Suc i) < llength p ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None ⟹
       Ps ≠ LNil ⟹
       (∃p. Ps = p ∧ (∀i. enat (Suc i) < llength p ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None)) ∧
       weight v (lhd Ps) ≠ None"
    proof-
      assume "LCons v Ps = p"
      show "∀i. enat (Suc i) < llength p ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None ⟹
       Ps ≠ LNil ⟹
       (∃p. Ps = p ∧ (∀i. enat (Suc i) < llength p ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None)) ∧
       weight v (lhd Ps) ≠ None"
      proof-
        assume A: "∀i. enat (Suc i) < llength p ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None"
        show "Ps ≠ LNil ⟹
       (∃p. Ps = p ∧ (∀i. enat (Suc i) < llength p ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None)) ∧
       weight v (lhd Ps) ≠ None"
        proof-
          assume "Ps ≠ LNil"
          show "(∃p. Ps = p ∧ (∀i. enat (Suc i) < llength p ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None)) ∧
       weight v (lhd Ps) ≠ None"
          proof
            show "∃p. Ps = p ∧ (∀i. enat (Suc i) < llength p ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None)"
            proof
              have "(∀i. enat (Suc i) < llength Ps ⟶ weight (lnth Ps i) (lnth Ps (Suc i)) ≠ None)"
              proof
                fix i 
                show "enat (Suc i) < llength Ps ⟶ weight (lnth Ps i) (lnth Ps (Suc i)) ≠ None "
                proof
                  assume "enat (Suc i) < llength Ps"
                  hence "enat (Suc (Suc i)) < llength (LCons v Ps)"
                    by (metis ldropn_Suc_LCons ldropn_eq_LNil linorder_not_le) 
                  have "(lnth Ps i) = (lnth (LCons v Ps) (Suc i))" by simp
                  have "(lnth Ps (Suc i)) = (lnth (LCons v Ps) (Suc (Suc i)))" by simp
                  thus "weight (lnth Ps i) (lnth Ps (Suc i)) ≠ None"
                    using A ‹(lnth Ps i) = (lnth (LCons v Ps) (Suc i))›
                    using ‹LCons v Ps = p› ‹enat (Suc (Suc i)) < llength (LCons v Ps)› by auto
                qed
              qed
              thus "Ps = Ps ∧ (∀i. enat (Suc i) < llength Ps ⟶ weight (lnth Ps i) (lnth Ps (Suc i)) ≠ None)"
                by simp
            qed
            have "v = lnth (LCons v Ps) 0" by simp
            have "lhd Ps = lnth (LCons v Ps) (Suc 0)" using lnth_def ‹Ps ≠ LNil›
              by (metis llist.exhaust_sel lnth_0 lnth_Suc_LCons) 
            thus "weight v (lhd Ps) ≠ None"
              using ‹v = lnth (LCons v Ps) 0› A
              by (metis ‹LCons v Ps = p› ‹Ps ≠ LNil› ‹∃p. Ps = p ∧ (∀i. enat (Suc i) < llength p ⟶ weight (lnth p i) (lnth p (Suc i)) ≠ None)› gen_llength_code(1) ldropn_0 ldropn_Suc_LCons ldropn_eq_LConsD llist.collapse(1) lnth_Suc_LCons not_lnull_conv)
          qed
        qed
      qed
    qed
  qed
qed

text‹\subsubsection*{Energy Levels}

The energy level of a play is calculated by repeatedly updating the current energy according to the 
edges in the play.
The final energy level of a finite play is ‹energy_level e p (the_enat (llength p -1))› where ‹e› is the initial energy.›

fun energy_level:: "'energy ⇒ 'position llist ⇒ nat ⇒ 'energy option" where 
 "energy_level e p 0 = (if p = LNil then None else Some e)" |
 "energy_level e p (Suc i) = 
          (if (energy_level e p i) = None ∨ llength p ≤ (Suc i) then None 
           else apply_w (lnth p i)(lnth p (Suc i)) (the (energy_level e p i)))"

text‹We establish some (in)equalities to simplify later proofs.›

lemma energy_level_cons:
  assumes "valid_play (LCons v Ps)"  and "¬lnull Ps" and 
          "apply_w v (lhd Ps) e ≠ None" and "enat i < (llength Ps)"
  shows "energy_level (the (apply_w v (lhd Ps) e)) Ps i 
         = energy_level e (LCons v Ps) (Suc i)"
  using assms proof(induction i arbitrary: e Ps rule: energy_level.induct)
  case (1 e p) 
  then show ?case using energy_level.simps
    by (smt (verit) ldropn_Suc_LCons ldropn_eq_LNil le_zero_eq lhd_conv_lnth llength_eq_0 llist.distinct(1) lnth_0 lnth_Suc_LCons lnull_def option.collapse option.discI option.sel zero_enat_def)
next
  case (2 e p n)
  hence "enat n < (llength Ps)"
    using Suc_ile_eq nless_le by blast
  hence IA: "energy_level (the (apply_w v (lhd Ps) e)) Ps n = energy_level e (LCons v Ps) (Suc n)"
    using 2 by simp 
  have "(llength Ps) > Suc n" using ‹enat (Suc n) < (llength Ps)›
    by simp
  hence "llength (LCons v Ps) > (Suc (Suc n))"
    by (metis ldropn_Suc_LCons ldropn_eq_LNil linorder_not_less) 
  show "energy_level (the (apply_w v (lhd Ps) e)) Ps (Suc n) = energy_level e (LCons v Ps) (Suc (Suc n))" 
  proof(cases "energy_level e (LCons v Ps) (Suc (Suc n)) = None")
    case True
    hence "(energy_level e (LCons v Ps) (Suc n)) = None ∨ llength (LCons v Ps) ≤ (Suc (Suc n)) ∨ apply_w (lnth (LCons v Ps) (Suc n)) (lnth (LCons v Ps) (Suc (Suc n))) (the (energy_level e (LCons v Ps) (Suc n))) = None " 
      using energy_level.simps
      by metis
    hence  none: "(energy_level e (LCons v Ps) (Suc n)) = None ∨ apply_w (lnth (LCons v Ps) (Suc n)) (lnth (LCons v Ps) (Suc (Suc n))) (the (energy_level e (LCons v Ps) (Suc n))) = None " 
      using ‹llength (LCons v Ps) > (Suc (Suc n))›
      by (meson linorder_not_less)
    show ?thesis 
    proof(cases "(energy_level e (LCons v Ps) (Suc n)) = None")
      case True
      then show ?thesis using IA by simp 
    next
      case False
      hence "apply_w (lnth (LCons v Ps) (Suc n)) (lnth (LCons v Ps) (Suc (Suc n))) (the (energy_level e (LCons v Ps) (Suc n))) = None " 
        using none by auto
      hence "apply_w (lnth (LCons v Ps) (Suc n)) (lnth (LCons v Ps) (Suc (Suc n))) (the (energy_level (the (apply_w v (lhd Ps) e)) Ps n)) = None " 
        using IA by auto
      then show ?thesis by (simp add: IA)
    qed
  next
    case False
    then show ?thesis using IA
      by (smt (verit) ‹enat (Suc n) < llength Ps› energy_level.simps(2) lnth_Suc_LCons order.asym order_le_imp_less_or_eq)
  qed
qed

lemma energy_level_nth:
  assumes "energy_level e p m ≠ None" and "Suc i ≤ m"
  shows "apply_w (lnth p i) (lnth p (Suc i)) (the (energy_level e p i)) ≠ None 
         ∧ energy_level e p i ≠ None"
using assms proof(induct "m - (Suc i)" arbitrary: i)
  case 0
  then show ?case using energy_level.simps
    by (metis diff_diff_cancel minus_nat.diff_0)
next
  case (Suc x)
  hence "x = m - Suc (Suc i)"
    by (metis add_Suc_shift diff_add_inverse2 diff_le_self le_add_diff_inverse)
  hence "apply_w (lnth p (Suc i)) (lnth p (Suc (Suc i))) (the (energy_level e p (Suc i))) ≠ None ∧ (energy_level e p (Suc i)) ≠ None" using Suc
    by (metis diff_is_0_eq nat.distinct(1) not_less_eq_eq) 
  then show ?case using energy_level.simps by metis
qed

lemma energy_level_append: 
  assumes "lfinite p" and "i < the_enat (llength p)" and 
          "energy_level e p (the_enat (llength p) -1) ≠ None"
  shows "energy_level e p i = energy_level e (lappend p p') i"
proof-
  have A: "⋀i. i < the_enat (llength p) ⟹ energy_level e p i ≠ None" using energy_level_nth assms
    by (metis Nat.lessE diff_Suc_1 less_eq_Suc_le) 
  show ?thesis using assms A proof(induct i)
    case 0
    then show ?case using energy_level.simps
      by (metis LNil_eq_lappend_iff llength_lnull llist.disc(1) the_enat_0 verit_comp_simplify1(1)) 
  next
    case (Suc i)
    hence "energy_level e p i = energy_level e (lappend p p') i"
      by simp 
    have "Suc i < (llength p) ∧ energy_level e p i ≠ None" using Suc
      by (metis Suc_lessD enat_ord_simps(2) lfinite_conv_llength_enat the_enat.simps)
    hence "Suc i <  (llength (lappend p p')) ∧ energy_level e (lappend p p') i ≠ None" 
      using ‹energy_level e p i = energy_level e (lappend p p') i›
      by (metis dual_order.strict_trans1 enat_le_plus_same(1) llength_lappend)
    then show ?case unfolding energy_level.simps using ‹Suc i < (llength p) ∧ energy_level e p i ≠ None› ‹energy_level e p i = energy_level e (lappend p p') i›
    by (smt (verit) Suc_ile_eq energy_level.elims le_zero_eq linorder_not_less lnth_lappend1 nle_le the_enat.simps zero_enat_def)
  qed
qed

text‹\subsubsection*{Won Plays}

All infinite plays are won by the defender. Further, the attacker is energy-bound and the defender
wins if the energy level becomes ‹None›. Finite plays with an energy level that is not ‹None› are won by 
a player, if the other is stuck.›

abbreviation "deadend g ≡ (∀g'. weight g g' = None)"
abbreviation "attacker_stuck p ≡ (llast p)∈ attacker ∧ deadend (llast p)"

definition defender_wins_play:: "'energy ⇒ 'position llist ⇒ bool" where
  "defender_wins_play e p ≡ lfinite p ⟶ 
         (energy_level e p (the_enat (llength p)-1) = None ∨ attacker_stuck p)"

subsection‹Energy-positional Strategies›

text‹
Energy-positional strategies map pairs of energies and positions to a next position.
Further, we focus on attacker strategies, i.e.\ partial functions mapping attacker positions to successors.›

definition attacker_strategy:: "('energy ⇒ 'position ⇒ 'position option) ⇒ bool" where 
  "attacker_strategy s = (∀g e. (g ∈ attacker ∧ ¬ deadend g) ⟶ 
                           (s e g ≠ None ∧ weight g (the (s e g))  ≠ None))"

text‹We now define what it means for a play to be consistent with some strategy.›

coinductive play_consistent_attacker::"('energy ⇒ 'position ⇒ 'position option) ⇒ 'position llist  ⇒ 'energy ⇒ bool" where
  "play_consistent_attacker _ LNil _" |
  "play_consistent_attacker _ (LCons v LNil) _" |
  "⟦play_consistent_attacker s Ps (the (apply_w v (lhd Ps) e)); ¬lnull Ps; 
    v ∈ attacker ⟶ (s e v) = Some (lhd Ps)⟧ 
    ⟹ play_consistent_attacker s (LCons v Ps) e"

text‹The coinductive definition allows for coinduction.›

lemma play_consistent_attacker_coinduct:
  assumes "Q s p e" and  
          "⋀s v Ps e'. Q s (LCons v Ps) e' ∧ ¬lnull Ps ⟹ 
                        Q s Ps (the (apply_w v (lhd Ps) e')) ∧
                        (v ∈ attacker ⟶ s e' v = Some (lhd Ps))"
  shows "play_consistent_attacker s p e"
  using assms proof(coinduction arbitrary: s p e)
  case play_consistent_attacker
  then show ?case 
  proof(cases "p = LNil")
    case True
    then show ?thesis by simp
  next
    case False
    hence "∃ v Ps. p = LCons v Ps"
      by (meson llist.exhaust) 
    from this obtain v Ps where "p = LCons v Ps" by auto
    then show ?thesis 
    proof(cases "Ps = LNil")
      case True
      then show ?thesis using ‹p = LCons v Ps› by simp 
    next
      case False
      hence "Q s Ps (the (apply_w v (lhd Ps) e)) ∧ (v ∈ attacker ⟶ s e v = Some (lhd Ps))"
        using assms
        using ‹p = LCons v Ps› llist.collapse(1) play_consistent_attacker(1) by blast 
      then show ?thesis using play_consistent_attacker play_consistent_attacker.simps
        by (metis (no_types, lifting) ‹p = LCons v Ps› lnull_def)
    qed
  qed
qed

text‹Adding a position to the beginning of a consistent play is simple by definition. 
It is harder to see, when a position can be added to the end of a finite play. For this we introduce the following lemma.›

lemma play_consistent_attacker_append_one:
  assumes "play_consistent_attacker s p e" and "lfinite p" and 
          "energy_level e p (the_enat (llength p)-1) ≠ None" and 
          "valid_play (lappend p (LCons g LNil))" and "llast p ∈ attacker ⟶ 
           Some g = s (the (energy_level e p (the_enat (llength p)-1))) (llast p)" 
  shows "play_consistent_attacker s (lappend p (LCons g LNil)) e"
using assms proof(induct "the_enat (llength p)" arbitrary: p e)
  case 0
  then show ?case
    by (metis lappend_lnull1 length_list_of length_list_of_conv_the_enat llength_eq_0 play_consistent_attacker.simps zero_enat_def)
next
  case (Suc x)
  hence "∃v Ps. p = LCons v Ps"
    by (metis Zero_not_Suc llength_LNil llist.exhaust the_enat_0) 
  from this obtain v Ps where "p = LCons v Ps" by auto

  have B: "play_consistent_attacker s (lappend Ps (LCons g LNil)) (the (apply_w v (lhd (lappend Ps (LCons g LNil)))e))" 
  proof(cases "Ps=LNil")
    case True
    then show ?thesis
      by (simp add: play_consistent_attacker.intros(2))
  next
    case False
    show ?thesis 
    proof(rule Suc.hyps)
      show "valid_play (lappend Ps (LCons g LNil))"
        by (metis (no_types, lifting) LNil_eq_lappend_iff Suc.prems(4) ‹p = LCons v Ps› lappend_code(2) llist.distinct(1) llist.inject valid_play.cases) 
      show "x = the_enat (llength Ps)"  using Suc ‹p = LCons v Ps›
        by (metis diff_add_inverse length_Cons length_list_of_conv_the_enat lfinite_ltl list_of_LCons ltl_simps(2) plus_1_eq_Suc) 
      show "play_consistent_attacker s Ps (the (apply_w v (lhd (lappend Ps (LCons g LNil))) e))"
        using False Suc.prems(1) ‹p = LCons v Ps› play_consistent_attacker.cases by fastforce
      show "lfinite Ps" using Suc ‹p = LCons v Ps› by simp

      hence EL: "energy_level (the (apply_w v (lhd (lappend Ps (LCons g LNil))) e)) Ps
     (the_enat (llength Ps) - 1) = energy_level e (LCons v (lappend Ps (LCons g LNil))) 
     (Suc (the_enat (llength Ps) - 1))"
      proof-
        have A: "valid_play (LCons v Ps) ∧  ¬ lnull Ps ∧  apply_w v (lhd Ps) e ≠ None ∧
  enat (the_enat (llength Ps) - 1) < llength Ps"
        proof
          show "valid_play (LCons v Ps)" proof(rule valid_play_nth)
            fix i
            show "enat (Suc i) < llength (LCons v Ps) ⟶
         weight (lnth (LCons v Ps) i) (lnth (LCons v Ps) (Suc i)) ≠ None "
            proof
              assume "enat (Suc i) < llength (LCons v Ps)"
              hence "(lnth (LCons v Ps) i) = (lnth (lappend p (LCons g LNil)) i)" using ‹p = LCons v Ps›
                by (metis Suc_ile_eq lnth_lappend1 order.strict_implies_order) 
              have "(lnth (LCons v Ps) (Suc i)) = (lnth (lappend p (LCons g LNil)) (Suc i))" using ‹p = LCons v Ps› ‹enat (Suc i) < llength (LCons v Ps)›
                by (metis lnth_lappend1) 

              from Suc have "valid_play (lappend p (LCons g LNil))" by simp
              hence "weight (lnth (lappend p (LCons g LNil)) i) (lnth (lappend p (LCons g LNil)) (Suc i)) ≠ None"
                using ‹enat (Suc i) < llength (LCons v Ps)› valid_play_nth_not_None
                by (metis Suc.prems(2) ‹p = LCons v Ps› llist.disc(2) lstrict_prefix_lappend_conv lstrict_prefix_llength_less min.absorb4 min.strict_coboundedI1) 

              thus "weight (lnth (LCons v Ps) i) (lnth (LCons v Ps) (Suc i)) ≠ None"
                using ‹(lnth (LCons v Ps) (Suc i)) = (lnth (lappend p (LCons g LNil)) (Suc i))› ‹(lnth (LCons v Ps) i) = (lnth (lappend p (LCons g LNil)) i)› by simp
            qed
          qed
          show "¬ lnull Ps ∧ apply_w v (lhd Ps) e ≠ None ∧ enat (the_enat (llength Ps) - 1) < llength Ps"
          proof
            show "¬ lnull Ps" using False by auto 
            show "apply_w v (lhd Ps) e ≠ None ∧ enat (the_enat (llength Ps) - 1) < llength Ps"
            proof
              show "apply_w v (lhd Ps) e ≠ None" using Suc
                by (smt (verit, ccfv_threshold) One_nat_def ‹¬ lnull Ps› ‹lfinite Ps› ‹p = LCons v Ps› ‹x = the_enat (llength Ps)› diff_add_inverse energy_level.simps(1) energy_level_nth le_SucE le_add1 length_list_of length_list_of_conv_the_enat lhd_conv_lnth llength_eq_0 llist.discI(2) lnth_0 lnth_ltl ltl_simps(2) option.sel plus_1_eq_Suc zero_enat_def) 
              show "enat (the_enat (llength Ps) - 1) < llength Ps" using False
                by (metis ‹¬ lnull Ps› ‹lfinite Ps› diff_Suc_1 enat_0_iff(2) enat_ord_simps(2) gr0_conv_Suc lessI lfinite_llength_enat llength_eq_0 not_gr_zero the_enat.simps)
            qed
          qed
        qed

        have "energy_level (the (apply_w v (lhd (lappend Ps (LCons g LNil))) e)) Ps
     (the_enat (llength Ps) - 1) = energy_level (the (apply_w v (lhd Ps) e)) Ps
     (the_enat (llength Ps) - 1)" using False
          by (simp add: lnull_def) 
        also have "... = energy_level e (LCons v Ps) (Suc (the_enat (llength Ps) - 1))" 
          using energy_level_cons A by simp
        also have "... = energy_level e (LCons v (lappend Ps (LCons g LNil))) 
     (Suc (the_enat (llength Ps) - 1))" using energy_level_append
          by (metis False One_nat_def Suc.hyps(2) Suc.prems(2) Suc.prems(3) ‹lfinite Ps› ‹p = LCons v Ps› ‹x = the_enat (llength Ps)› diff_Suc_less lappend_code(2) length_list_of length_list_of_conv_the_enat less_SucE less_Suc_eq_0_disj llength_eq_0 llist.disc(1) llist.expand nat_add_left_cancel_less plus_1_eq_Suc zero_enat_def) 
        finally show ?thesis .
      qed

      thus EL_notNone: "energy_level (the (apply_w v (lhd (lappend Ps (LCons g LNil))) e)) Ps
     (the_enat (llength Ps) - 1) ≠ None" 
        using Suc
        by (metis False One_nat_def Suc_pred ‹p = LCons v Ps› ‹x = the_enat (llength Ps)› diff_Suc_1' energy_level.simps(1) energy_level_append lappend_code(2) lessI not_less_less_Suc_eq not_one_less_zero option.distinct(1) zero_less_Suc zero_less_diff) 

      show "llast Ps ∈ attacker ⟶
    Some g = s (the (energy_level (the (apply_w v (lhd (lappend Ps (LCons g LNil))) e)) Ps
             (the_enat (llength Ps) - 1)))(llast Ps)"
      proof
        assume "llast Ps ∈ attacker"
        have "llast Ps = llast p" using False ‹p = LCons v Ps›
          by (simp add: llast_LCons lnull_def)
        hence "llast p ∈ attacker" using ‹llast Ps ∈ attacker› by simp
        hence "Some g = s (the (energy_level e p (the_enat (llength p) - 1))) (llast p)" using Suc by simp
        hence "Some g = s (the (energy_level e (LCons v Ps) (the_enat (llength (LCons v Ps)) - 1))) (llast Ps)" using ‹p = LCons v Ps› ‹llast Ps = llast p› by simp

        have "apply_w v (lhd Ps) e ≠ None" using Suc
          by (smt (verit, best) EL EL_notNone False One_nat_def energy_level.simps(1) energy_level_nth le_add1 lhd_conv_lnth lhd_lappend llist.discI(2) llist.exhaust_sel lnth_0 lnth_Suc_LCons lnull_lappend option.sel plus_1_eq_Suc)
        thus  "Some g = s (the (energy_level (the (apply_w v (lhd (lappend Ps (LCons g LNil))) e)) Ps
             (the_enat (llength Ps) - 1)))(llast Ps)" using EL
          by (metis (no_types, lifting) False Suc.hyps(2) Suc.prems(2) Suc.prems(3) Suc_diff_Suc ‹Some g = s (the (energy_level e (LCons v Ps) (the_enat (llength (LCons v Ps)) - 1))) (llast Ps)› ‹lfinite Ps› ‹p = LCons v Ps› ‹x = the_enat (llength Ps)› cancel_comm_monoid_add_class.diff_cancel diff_Suc_1 energy_level_append lappend_code(2) lessI lfinite.cases lfinite_conv_llength_enat linorder_neqE_nat llength_eq_0 llist.discI(2) not_add_less1 plus_1_eq_Suc the_enat.simps zero_enat_def) 
      qed
    qed
  qed

  have A: "¬ lnull (lappend Ps (LCons g LNil)) ∧ (v ∈ attacker ⟶ (s e v = Some (lhd (lappend Ps (LCons g LNil)))))"
  proof
    show "¬ lnull (lappend Ps (LCons g LNil))" by simp
    show "v ∈ attacker ⟶
    s e v = Some (lhd (lappend Ps (LCons g LNil)))"
    proof
      assume "v ∈ attacker"
      show "s e v = Some (lhd (lappend Ps (LCons g LNil)))" using ‹v ∈ attacker› Suc
        by (smt (verit) One_nat_def ‹p = LCons v Ps› diff_add_0 energy_game.energy_level.simps(1) eq_LConsD length_Cons length_list_of_conv_the_enat lfinite_ltl lhd_lappend list.size(3) list_of_LCons list_of_LNil llast_singleton llist.disc(1) option.exhaust_sel option.inject play_consistent_attacker.cases plus_1_eq_Suc) 
    qed
  qed

  have "(lappend p (LCons g LNil)) = LCons v (lappend Ps (LCons g LNil))"
    by (simp add: ‹p = LCons v Ps›) 
  thus ?case using play_consistent_attacker.simps A B
    by meson
qed

text‹We now define attacker winning strategies, i.e.\ attacker strategies where the defender does not win any consistent plays w.r.t\ some initial energy and a starting position.›

fun attacker_winning_strategy:: "('energy ⇒ 'position ⇒ 'position option) ⇒ 'energy ⇒ 'position ⇒ bool" where
  "attacker_winning_strategy s e g = (attacker_strategy s ∧ 
      (∀p. (play_consistent_attacker s (LCons g p) e ∧ valid_play (LCons g p))
            ⟶ ¬defender_wins_play e (LCons g p)))"

subsection‹Non-positional Strategies›

text‹A non-positional strategy maps finite plays to a next position. We now introduce non-positional strategies to better characterise attacker winning budgets. 
These definitions closely resemble the definitions for energy-positional strategies.›

definition attacker_nonpos_strategy:: "('position list ⇒ 'position option) ⇒ bool" where 
  "attacker_nonpos_strategy s = (∀list ≠ []. ((last list) ∈ attacker 
   ∧ ¬deadend (last list)) ⟶ s list ≠ None 
                               ∧ (weight (last list) (the (s list)))≠None)"

text‹We now define what it means for a play to be consistent with some non-positional strategy.›

coinductive play_consistent_attacker_nonpos::"('position list ⇒ 'position option) ⇒ ('position llist) ⇒ ('position list) ⇒ bool" where
  "play_consistent_attacker_nonpos s LNil _" |
  "play_consistent_attacker_nonpos s (LCons v LNil) []" |
  "(last (w#l))∉attacker 
  ⟹ play_consistent_attacker_nonpos s (LCons v LNil) (w#l)" |
  "⟦(last (w#l))∈attacker; the (s (w#l)) = v ⟧ 
  ⟹ play_consistent_attacker_nonpos s (LCons v LNil) (w#l)" |
  "⟦play_consistent_attacker_nonpos s Ps (l@[v]); ¬lnull Ps; v∉attacker⟧
   ⟹ play_consistent_attacker_nonpos s (LCons v Ps) l" |
  "⟦play_consistent_attacker_nonpos s Ps (l@[v]); ¬lnull Ps; v∈attacker; 
    lhd Ps = the (s (l@[v]))⟧
    ⟹ play_consistent_attacker_nonpos s (LCons v Ps) l"

inductive_simps play_consistent_attacker_nonpos_cons_simp: 
  "play_consistent_attacker_nonpos s (LCons x xs) []"

text‹The definition allows for coinduction.›

lemma play_consistent_attacker_nonpos_coinduct:
  assumes "Q s p l" and 
         base: "⋀s v l. Q s (LCons v LNil) l ⟹ (l = [] ∨ (last l) ∉ attacker 
                ∨ ((last l)∈attacker ∧ the (s l) = v))" and 
         step: "⋀s v Ps l. Q s (LCons v Ps) l ∧ Ps≠LNil 
                ⟹ Q s Ps (l@[v]) ∧ (v∈attacker ⟶ lhd Ps = the (s (l@[v])))"
  shows "play_consistent_attacker_nonpos s p l"
  using assms proof(coinduction arbitrary: s p l)
  case play_consistent_attacker_nonpos
  then show ?case proof(cases "p=LNil")
    case True
    then show ?thesis by simp
  next
    case False
    hence "∃v p'. p = LCons v p'"
      by (simp add: neq_LNil_conv)
    from this obtain v p' where "p=LCons v p'" by auto
    then show ?thesis proof(cases "p'=LNil")
      case True
      then show ?thesis
        by (metis ‹p = LCons v p'› neq_Nil_conv play_consistent_attacker_nonpos(1) play_consistent_attacker_nonpos(2))
    next
      case False
      then show ?thesis
        using ‹p = LCons v p'› assms(3) llist.expand play_consistent_attacker_nonpos(1) assms(2) by auto 
    qed
  qed
qed

text‹We now show that a position can be added to the end of a finite consitent play while remaining consistent.›

lemma consistent_nonpos_append_defender:
  assumes "play_consistent_attacker_nonpos s (LCons v Ps) l" and 
          "llast (LCons v Ps) ∉ attacker" and "lfinite (LCons v Ps)"
  shows "play_consistent_attacker_nonpos s (lappend (LCons v Ps) (LCons g' LNil)) l"
  using assms proof(induction "list_of Ps" arbitrary: v Ps l)
  case Nil
  hence v_append_Ps: "play_consistent_attacker_nonpos s (lappend (LCons v Ps) (LCons g' LNil)) l = play_consistent_attacker_nonpos s (LCons v (LCons g' LNil)) l"
    by (metis lappend_code(1) lappend_code(2) lfinite_LCons llist_of_eq_LNil_conv llist_of_list_of)

  from Nil.prems(1) have "play_consistent_attacker_nonpos s (LCons g' LNil) (l@[v])" using play_consistent_attacker_nonpos.intros Nil
    by (metis (no_types, lifting) lfinite_LCons list.exhaust_sel llast_singleton llist_of.simps(1) llist_of_list_of snoc_eq_iff_butlast)
  hence "play_consistent_attacker_nonpos s (LCons v (LCons g' LNil)) l" using play_consistent_attacker_nonpos.intros Nil
    by (metis lfinite_code(2) llast_singleton llist.disc(2) llist_of.simps(1) llist_of_list_of) 
  then show ?case using v_append_Ps by simp
next
  case (Cons a x)
  hence v_append_Ps: "play_consistent_attacker_nonpos s (lappend (LCons v Ps) (LCons g' LNil)) l = play_consistent_attacker_nonpos s (LCons v (lappend Ps (LCons g' LNil))) l"
    by simp

  from Cons have "¬lnull Ps"
    by (metis list.discI list_of_LNil llist.collapse(1)) 

  have "¬ lnull (lappend Ps (LCons g' LNil))" by simp

  have "x = list_of (ltl Ps)" using Cons.hyps(2)
    by (metis Cons.prems(3) lfinite_code(2) list.sel(3) tl_list_of)
  have "llast (LCons (lhd Ps) (ltl Ps)) ∉ attacker" using Cons.prems(2)
    by (simp add: ‹¬ lnull Ps› llast_LCons) 
  have "lfinite (LCons (lhd Ps) (ltl Ps))" using Cons.prems(3) by simp
  have "play_consistent_attacker_nonpos s (LCons (lhd Ps) (ltl Ps)) (l @ [v])" using Cons.prems(1) play_consistent_attacker_nonpos.simps
    by (smt (verit, best) ‹¬ lnull Ps› eq_LConsD lhd_LCons lhd_LCons_ltl ltl_simps(2))
  hence "play_consistent_attacker_nonpos s (lappend Ps (LCons g' LNil)) (l @ [v])" using Cons.hyps ‹lfinite (LCons (lhd Ps) (ltl Ps))› ‹llast (LCons (lhd Ps) (ltl Ps)) ∉ attacker› ‹x = list_of (ltl Ps)›
    by (metis ‹¬ lnull Ps› lhd_LCons_ltl)

  have "play_consistent_attacker_nonpos s (LCons v (lappend Ps (LCons g' LNil))) l" 
  proof(cases "v ∈ attacker")
    case True
    have "lhd Ps = the (s (l @ [v]))" using True Cons.prems(1) play_consistent_attacker_nonpos.simps
      by (smt (verit) ‹¬ lnull Ps› llist.distinct(1) llist.inject lnull_def) 
    hence "lhd (lappend Ps (LCons g' LNil)) = the (s (l @ [v]))" by (simp add: ‹¬ lnull Ps›) 

    then show ?thesis using play_consistent_attacker_nonpos.intros(6) True ‹play_consistent_attacker_nonpos s (lappend Ps (LCons g' LNil)) (l @ [v])› ‹lhd (lappend Ps (LCons g' LNil)) = the (s (l @ [v]))› ‹¬ lnull (lappend Ps (LCons g' LNil))›
      by simp
  next
    case False
    then show ?thesis using play_consistent_attacker_nonpos.intros(5) False ‹¬ lnull (lappend Ps (LCons g' LNil))› ‹play_consistent_attacker_nonpos s (lappend Ps (LCons g' LNil)) (l @ [v])›
      by simp
  qed
  then show ?case using v_append_Ps by simp
qed

lemma consistent_nonpos_append_attacker:
  assumes "play_consistent_attacker_nonpos s (LCons v Ps) l"  
          and "llast (LCons v Ps) ∈ attacker" and "lfinite (LCons v Ps)"
  shows "play_consistent_attacker_nonpos s (lappend  (LCons v Ps) (LCons (the (s (l@(list_of (LCons v Ps))))) LNil)) l"
  using assms proof(induction "list_of Ps" arbitrary: v Ps l)
  case Nil
  hence v_append_Ps: "play_consistent_attacker_nonpos s (lappend (LCons v Ps) (LCons (the (s (l@(list_of (LCons v Ps))))) LNil)) l 
        = play_consistent_attacker_nonpos s (LCons v (LCons (the (s (l@[v]))) LNil)) l"
    by (metis lappend_code(1) lappend_code(2) lfinite_code(2) list_of_LCons llist_of.simps(1) llist_of_list_of) 
  have "play_consistent_attacker_nonpos s (LCons v (LCons (the (s (l@[v]))) LNil)) l" using play_consistent_attacker_nonpos.intros Nil
    by (metis hd_Cons_tl lhd_LCons llist.disc(2)) 
  then show ?case using v_append_Ps by simp
next
  case (Cons a x)
  have v_append_Ps: "play_consistent_attacker_nonpos s (lappend (LCons v Ps) (LCons (the (s (l @ list_of (LCons v Ps)))) LNil)) l
                    = play_consistent_attacker_nonpos s (LCons v (lappend Ps (LCons (the (s (l @ [v]@list_of Ps))) LNil))) l"
    using Cons.prems(3) by auto
  have "x = list_of (ltl Ps)" using Cons.hyps(2)
    by (metis Cons.prems(3) lfinite_code(2) list.sel(3) tl_list_of) 
  have "play_consistent_attacker_nonpos s (LCons (lhd Ps) (ltl Ps)) (l@[v])" using Cons.prems(1) play_consistent_attacker_nonpos.simps
    by (smt (verit) Cons.hyps(2) eq_LConsD lhd_LCons list.discI list_of_LNil ltl_simps(2))
  have "llast (LCons (lhd Ps) (ltl Ps)) ∈ attacker" using Cons.prems(2)
    by (metis Cons.hyps(2) lhd_LCons_ltl list.distinct(1) list_of_LNil llast_LCons llist.collapse(1))
  have "lfinite (LCons (lhd Ps) (ltl Ps))" using Cons.prems(3) by simp
  hence "play_consistent_attacker_nonpos s (lappend Ps (LCons (the (s ((l @[v])@list_of Ps))) LNil)) (l@[v])"
    using Cons.hyps ‹x = list_of (ltl Ps)› ‹play_consistent_attacker_nonpos s (LCons (lhd Ps) (ltl Ps)) (l@[v])› 
    ‹llast (LCons (lhd Ps) (ltl Ps)) ∈ attacker›
    by (metis llist.exhaust_sel ltl_simps(1) not_Cons_self2)  
  hence "play_consistent_attacker_nonpos s (LCons v (lappend Ps (LCons (the (s ((l @[v])@(list_of Ps)))) LNil))) l"
    using play_consistent_attacker_nonpos.simps Cons
    by (smt (verit) lhd_LCons lhd_lappend list.discI list_of_LNil llist.distinct(1) lnull_lappend ltl_simps(2)) 
    
  then show ?case using v_append_Ps by simp
qed

text‹We now define non-positional attacker winning strategies, i.e. attacker strategies where the defender
 does not win any consistent plays w.r.t some initial energy and a starting position.›

fun nonpos_attacker_winning_strategy:: "('position list ⇒ 'position option) ⇒
  'energy ⇒ 'position ⇒ bool" where
  "nonpos_attacker_winning_strategy s e g = (attacker_nonpos_strategy s ∧ 
   (∀p. (play_consistent_attacker_nonpos s (LCons g p) [] 
         ∧ valid_play (LCons g p)) ⟶ ¬defender_wins_play e (LCons g p)))"

subsection‹Attacker Winning Budgets›

text‹We now define attacker winning budgets utilising strategies.›

fun winning_budget:: "'energy ⇒ 'position ⇒ bool" where
 "winning_budget e g = (∃s. attacker_winning_strategy s e g)"

fun nonpos_winning_budget:: "'energy ⇒ 'position ⇒ bool" where
 "nonpos_winning_budget e g = (∃s. nonpos_attacker_winning_strategy s e g)"

text‹Note that ‹nonpos_winning_budget = winning_budget› holds but is not proven in this theory.
Using this fact we can give an inductive characterisation of attacker winning budgets.
›

inductive winning_budget_ind:: "'energy ⇒ 'position ⇒ bool" where
 defender: "winning_budget_ind e g" if 
 "g ∉ attacker ∧ (∀g'. weight g g' ≠ None ⟶ (apply_w g g' e≠ None 
  ∧ winning_budget_ind (the (apply_w g g' e)) g'))" |
 attacker: "winning_budget_ind e g" if 
 "g ∈ attacker ∧ (∃g'. weight g g' ≠ None ∧ apply_w g g' e≠ None 
  ∧ winning_budget_ind (the (apply_w g g' e)) g')"

text‹Before proving some correspondence of those definitions we first note that attacker winning budgets
in monotonic energy games are upward-closed. We show this for two of the three definitions.›

lemma upward_closure_wb_nonpos:
  assumes monotonic: "⋀g g' e e'. weight g g' ≠ None 
          ⟹ apply_w g g' e ≠ None ⟹ leq e e' ⟹ apply_w g g' e' ≠ None
          ∧ leq (the (apply_w g g' e)) (the (apply_w g g' e'))"
          and "leq e e'" and "nonpos_winning_budget e g"
  shows "nonpos_winning_budget e' g"
proof-
  from assms have "∃s. nonpos_attacker_winning_strategy s e g" using nonpos_winning_budget.simps by simp
  from this obtain s where S: "nonpos_attacker_winning_strategy s e g" by auto
  have "nonpos_attacker_winning_strategy s e' g" unfolding nonpos_attacker_winning_strategy.simps 
  proof
    show "attacker_nonpos_strategy s" using S by simp
    show "∀p. play_consistent_attacker_nonpos s (LCons g p) [] ∧ valid_play (LCons g p) ⟶ ¬ defender_wins_play e' (LCons g p)"
    proof
      fix p
      show "play_consistent_attacker_nonpos s (LCons g p) [] ∧ valid_play (LCons g p) ⟶ ¬ defender_wins_play e' (LCons g p) "
      proof
        assume P: "play_consistent_attacker_nonpos s (LCons g p) [] ∧ valid_play (LCons g p)"
        hence X: "lfinite (LCons g p) ∧ ¬ (energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) = None ∨ llast (LCons g p) ∈ attacker ∧ deadend (llast (LCons g p)))" 
          using S unfolding nonpos_attacker_winning_strategy.simps defender_wins_play_def by simp
        have "lfinite (LCons g p) ∧ ¬ (energy_level e' (LCons g p) (the_enat (llength (LCons g p)) - 1) = None ∨ llast (LCons g p) ∈ attacker ∧ deadend (llast (LCons g p)))" 
        proof
          show "lfinite (LCons g p)" using P S unfolding nonpos_attacker_winning_strategy.simps defender_wins_play_def by simp
          have "energy_level e' (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None ∧ ¬(llast (LCons g p) ∈ attacker ∧ deadend (llast (LCons g p)))"
          proof
            have E: "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None" using P S unfolding nonpos_attacker_winning_strategy.simps defender_wins_play_def by simp
            have "⋀len. len ≤ the_enat (llength (LCons g p)) - 1 ⟶ energy_level e' (LCons g p) len ≠ None ∧ (leq (the (energy_level e (LCons g p) len)) (the (energy_level e' (LCons g p) len)))" 
            proof
              fix len
              show "len ≤ the_enat (llength (LCons g p)) - 1 ⟹ energy_level e' (LCons g p) len ≠ None ∧ leq (the (energy_level e (LCons g p) len)) (the (energy_level e' (LCons g p) len))"
              proof(induct len)
                case 0                
                then show ?case using energy_level.simps assms(2)
                  by (simp add: llist.distinct(1) option.discI option.sel)
              next
                case (Suc len)
                hence "energy_level e' (LCons g p) len ≠ None" by simp
                have W: "weight (lnth (LCons g p) len)(lnth (LCons g p) (Suc len)) ≠ None" using P Suc.prems valid_play.simps valid_play_nth_not_None
                  by (smt (verit) ‹lfinite (LCons g p)› diff_Suc_1 enat_ord_simps(2) le_less_Suc_eq less_imp_diff_less lfinite_llength_enat linorder_le_less_linear not_less_eq the_enat.simps)
                have A: "apply_w (lnth (LCons g p) len) (lnth (LCons g p) (Suc len)) (the (energy_level e (LCons g p) len)) ≠ None" 
                  using E Suc.prems energy_level_nth by blast
                have "llength (LCons g p) > Suc len" using Suc.prems
                  by (metis ‹lfinite (LCons g p)› diff_Suc_1 enat_ord_simps(2) less_imp_diff_less lfinite_conv_llength_enat nless_le not_le_imp_less not_less_eq the_enat.simps)
                hence "energy_level e' (LCons g p) (Suc len) = apply_w (lnth (LCons g p) len)(lnth (LCons g p) (Suc len)) (the (energy_level e' (LCons g p) len))"
                  using ‹energy_level e' (LCons g p) len ≠ None› energy_level.simps
                  by (meson leD) 
                then show ?case using A W Suc assms
                  by (smt (verit) E Suc_leD energy_level.simps(2) energy_level_nth)
              qed
            qed
            thus "energy_level e' (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None" by simp
            show " ¬ (llast (LCons g p) ∈ attacker ∧ deadend (llast (LCons g p)))" using P S unfolding nonpos_attacker_winning_strategy.simps defender_wins_play_def by simp
          qed
          thus "¬ (energy_level e' (LCons g p) (the_enat (llength (LCons g p)) - 1) = None ∨ llast (LCons g p) ∈ attacker ∧ deadend (llast (LCons g p)))"
            by simp
        qed
        thus "¬ defender_wins_play e' (LCons g p)" unfolding defender_wins_play_def by simp
      qed
    qed
  qed
  thus ?thesis using nonpos_winning_budget.simps by auto
qed

lemma upward_closure_wb_ind:
  assumes monotonic: "⋀g g' e e'. weight g g' ≠ None 
          ⟹ apply_w g g' e ≠ None ⟹ leq e e' ⟹ apply_w g g' e' ≠ None
          ∧ leq (the (apply_w g g' e)) (the (apply_w g g' e'))" 
          and "leq e e'" and "winning_budget_ind e g"
  shows "winning_budget_ind e' g"
proof-
  define P where "P ≡ λ e g. (∀e'. leq e e' ⟶ winning_budget_ind e' g)"
  have "P e g" using assms(3) proof (induct rule: winning_budget_ind.induct)
    case (defender g e)
    then show ?case using P_def
      using monotonic winning_budget_ind.defender by blast
  next
    case (attacker g e)
    then show ?case using P_def
      using monotonic winning_budget_ind.attacker by blast 
  qed

  thus ?thesis using assms(2) P_def  by blast
qed

text‹Now we prepare the proof of the inductive characterisation. For this we define an order and a set allowing for a well-founded induction.›

definition strategy_order::  "('energy ⇒ 'position ⇒ 'position option) ⇒ 
  'position × 'energy ⇒ 'position × 'energy ⇒ bool" where
  "strategy_order s ≡ λ(g1, e1)(g2, e2).Some e1 = apply_w g2 g1 e2 ∧ 
    (if g2 ∈ attacker then Some g1 = s e2 g2 else weight g2 g1 ≠ None)"

definition reachable_positions:: "('energy ⇒ 'position ⇒ 'position option) ⇒ 'position ⇒ 'energy ⇒ ('position × 'energy) set" where
  "reachable_positions s 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)))}"

lemma strategy_order_well_founded:
  assumes "attacker_winning_strategy s e g"
  shows "wfp_on (strategy_order s) (reachable_positions s g e)"
  unfolding Restricted_Predicates.wfp_on_def 
proof
  assume "∃f. ∀i. f i ∈ reachable_positions s g e ∧ strategy_order s (f (Suc i)) (f i)"
  from this obtain f where F: "∀i. f i ∈ reachable_positions s g e ∧ strategy_order s (f (Suc i)) (f i)" by auto

  define p where "p = lmap (λi. fst (f i))(iterates Suc 0)"
  hence "⋀i. lnth p i = fst (f i)"
    by simp 

  from p_def have "¬lfinite p" by simp

  have "⋀i. enat (Suc i) < llength p ⟹ weight (lnth p i) (lnth p (Suc i)) ≠ None"
  proof-
    fix i
    have "∃g1 e1 g2 e2. (f i) = (g2, e2) ∧ f (Suc i) = (g1, e1)" using F reachable_positions_def by simp
    from this obtain g1 e1 g2 e2 where "(f i) = (g2, e2)" and "f (Suc i) = (g1, e1)"
      by blast
    assume "enat (Suc i) < llength p"

    have "weight g2 g1 ≠ None"  
    proof(cases "g2 ∈ attacker")
      case True
      then show ?thesis 
      proof(cases "deadend g2")        
        case True
        have "(g2, e2) ∈ reachable_positions s g e" using F by (metis ‹f i = (g2, e2)›) 
        hence "(∃p'. (lfinite p' ∧ llast (LCons g p') = g2 
                                                    ∧ valid_play (LCons g p') 
                                                    ∧ play_consistent_attacker s (LCons g p') e) 
                                                    ∧ (Some e2 = energy_level e (LCons g p') (the_enat (llength p'))))"
          using reachable_positions_def by simp
        from this obtain p' where P': "(lfinite p' ∧ llast (LCons g p') = g2 
                                                    ∧ valid_play (LCons g p') 
                                                    ∧ play_consistent_attacker s (LCons g p') e) 
                                                    ∧ (Some e2 = energy_level e (LCons g p') (the_enat (llength p')))" by auto
        
        have "¬defender_wins_play e (LCons g p')" using assms unfolding attacker_winning_strategy.simps using P' by auto
        have "llast (LCons g p') ∈ attacker ∧ deadend (llast (LCons g p'))" using True ‹g2 ∈ attacker› P' by simp
        hence "defender_wins_play e (LCons g p')"
          unfolding defender_wins_play_def by simp
        hence "False" using ‹¬defender_wins_play e (LCons g p')› by simp
        then show ?thesis by simp
      next
        case False 
        from True have "Some g1 = s e2 g2" 
          using F unfolding strategy_order_def using  ‹f (Suc i) = (g1, e1)› ‹(f i) = (g2, e2)›
          by (metis (mono_tags, lifting) case_prod_conv)
        have "(∀g e. (g ∈ attacker ∧ ¬ deadend g) ⟶ (s e g ≠ None ∧ weight g (the (s e g)) ≠ None))"
          using assms unfolding attacker_winning_strategy.simps attacker_strategy_def
          by simp
        hence "weight g2 (the (s e2 g2)) ≠ None" using False True
          by simp 
        then show ?thesis using ‹Some g1 = s e2 g2›
          by (metis option.sel)
      qed
    next
      case False
      then show ?thesis using F unfolding strategy_order_def using ‹f (Suc i) = (g1, e1)› ‹(f i) = (g2, e2)›
        by (metis (mono_tags, lifting) case_prod_conv)
    qed
    thus "weight (lnth p i) (lnth p (Suc i)) ≠ None" 
      using p_def ‹f i = (g2, e2)› ‹f (Suc i) = (g1, e1)› by simp
  qed

  hence "valid_play p" using valid_play_nth
    by simp

  have "(f 0) ∈ reachable_positions s g e" using F by simp
  hence "∃g0 e0. f 0 = (g0,e0)" using reachable_positions_def by simp
  from this obtain g0 e0 where "f 0 = (g0,e0)" by blast
  hence "∃p'. (lfinite p' ∧ llast (LCons g p') = g0 
                                                    ∧ valid_play (LCons g p') 
                                                    ∧ play_consistent_attacker s (LCons g p') e) 
                                                    ∧ (Some e0 = energy_level e (LCons g p') (the_enat (llength p')))"
    using ‹(f 0) ∈ reachable_positions s g e› unfolding reachable_positions_def by auto
  from this obtain p' where P': "(lfinite p' ∧ llast (LCons g p') = g0 
                                                    ∧ valid_play (LCons g p') 
                                                    ∧ play_consistent_attacker s (LCons g p') e) 
                                                    ∧ (Some e0 = energy_level e (LCons g p') (the_enat (llength p')))" by auto

  have "⋀i. strategy_order s (f (Suc i)) (f i)" using F by simp
  hence "⋀i. Some (snd (f (Suc i))) = apply_w (fst (f i)) (fst (f (Suc i))) (snd (f i))" using strategy_order_def
    by (simp add: case_prod_beta)
  hence "⋀i. (snd (f (Suc i))) = the (apply_w (fst (f i)) (fst (f (Suc i))) (snd (f i)))"
    by (metis option.sel) 

  have "⋀i. (energy_level e0 p i) = Some (snd (f i))"
  proof-
    fix i
    show "(energy_level e0 p i) = Some (snd (f i))"
    proof(induct i)
      case 0
      then show ?case using ‹f 0 = (g0,e0)› ‹¬ lfinite p› by auto 
    next
      case (Suc i)
      have "Some (snd (f (Suc i))) = (apply_w (fst (f i)) (fst (f (Suc i))) (snd (f i)))" 
        using ‹⋀i. Some (snd (f (Suc i))) = apply_w (fst (f i)) (fst (f (Suc i))) (snd (f i))› by simp
      also have "... = (apply_w (fst (f i)) (fst (f (Suc i))) ( the (energy_level e0 p i)))" using Suc by simp
      also have "... = (apply_w (lnth p i) (lnth p (Suc i)) ( the (energy_level e0 p i)))" using ‹⋀i. lnth p i = fst (f i)› by simp
      also have "... = (energy_level e0 p (Suc i))" using energy_level.simps ‹¬ lfinite p› Suc
        by (simp add: lfinite_conv_llength_enat) 
      finally show ?case
        by simp 
    qed
  qed

  define Q where "Q ≡ λ s p e0. ¬lfinite p ∧ valid_play p ∧ (∀i. (energy_level e0 p i) ≠ None ∧ ((lnth p i), the (energy_level e0 p i)) ∈ reachable_positions s g e 
            ∧ strategy_order s ((lnth p (Suc i)), the (energy_level e0 p (Suc i))) ((lnth p i), the (energy_level e0 p i)))"

  have Q: "¬lfinite p ∧ valid_play p ∧ (∀i. (energy_level e0 p i) ≠ None ∧ ((lnth p i), the (energy_level e0 p i)) ∈ reachable_positions s g e 
            ∧ strategy_order s ((lnth p (Suc i)), the (energy_level e0 p (Suc i))) ((lnth p i), the (energy_level e0 p i)))"
  proof
    show "¬ lfinite p " using ‹¬lfinite p› .
    show "valid_play p ∧
    (∀i. energy_level e0 p i ≠ None ∧
         (lnth p i, the (energy_level e0 p i)) ∈ reachable_positions s g e ∧
         strategy_order s (lnth p (Suc i), the (energy_level e0 p (Suc i)))
          (lnth p i, the (energy_level e0 p i)))"
    proof
      show "valid_play p" using ‹valid_play p› .
      show "∀i. energy_level e0 p i ≠ None ∧
        (lnth p i, the (energy_level e0 p i)) ∈ reachable_positions s g e ∧
        strategy_order s (lnth p (Suc i), the (energy_level e0 p (Suc i)))
         (lnth p i, the (energy_level e0 p i)) "
      proof
        fix i
        show "energy_level e0 p i ≠ None ∧
         (lnth p i, the (energy_level e0 p i)) ∈ reachable_positions s g e ∧
         strategy_order s (lnth p (Suc i), the (energy_level e0 p (Suc i)))
          (lnth p i, the (energy_level e0 p i))"
        proof
          show "energy_level e0 p i ≠ None" using ‹⋀i. (energy_level e0 p i) = Some (snd (f i))› by simp
          show "(lnth p i, the (energy_level e0 p i)) ∈ reachable_positions s g e ∧
    strategy_order s (lnth p (Suc i), the (energy_level e0 p (Suc i)))
     (lnth p i, the (energy_level e0 p i)) "
          proof
            show "(lnth p i, the (energy_level e0 p i)) ∈ reachable_positions s g e"
              using ‹⋀i. (energy_level e0 p i) = Some (snd (f i))› F ‹⋀i. lnth p i = fst (f i)›
              by simp
            show "strategy_order s (lnth p (Suc i), the (energy_level e0 p (Suc i)))
     (lnth p i, the (energy_level e0 p i))"
              using ‹⋀i. strategy_order s (f (Suc i)) (f i)› ‹⋀i. lnth p i = fst (f i)› ‹⋀i. (energy_level e0 p i) = Some (snd (f i))›
              by (metis option.sel split_pairs)
          qed
        qed
      qed
    qed
  qed

  hence "Q s p e0" using Q_def by simp

  have "⋀s v Ps e'.
       (¬ lfinite (LCons v Ps) ∧
        valid_play (LCons v Ps) ∧
        (∀i. energy_level e' (LCons v Ps) i ≠ None ∧
             (lnth (LCons v Ps) i, the (energy_level e' (LCons v Ps) i)) ∈ reachable_positions s g e ∧
             strategy_order s (lnth (LCons v Ps) (Suc i), the (energy_level e' (LCons v Ps) (Suc i)))
              (lnth (LCons v Ps) i, the (energy_level e' (LCons v Ps) i)))) ∧
       ¬ lnull Ps ⟹
       (¬ lfinite Ps ∧
        valid_play Ps ∧
        (∀i. energy_level (the (apply_w v (lhd Ps) e')) Ps i ≠ None ∧
             (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i)) ∈ reachable_positions s g e ∧
             strategy_order s (lnth Ps (Suc i), the (energy_level (the (apply_w v (lhd Ps) e')) Ps (Suc i)))
              (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i)))) ∧
       (v ∈ attacker ⟶ s e' v = Some (lhd Ps)) ∧ (apply_w v (lhd Ps) e') ≠ None"
  proof-
    fix s v Ps e'
    assume A: "(¬lfinite (LCons v Ps) ∧ valid_play (LCons v Ps) ∧ (∀i. energy_level e' (LCons v Ps) i ≠ None ∧
            (lnth (LCons v Ps) i, the (energy_level e' (LCons v Ps) i))
            ∈ reachable_positions s g e ∧
            strategy_order s (lnth (LCons v Ps) (Suc i), the (energy_level e' (LCons v Ps) (Suc i)))
             (lnth (LCons v Ps) i, the (energy_level e' (LCons v Ps) i)))) ∧
       ¬ lnull Ps"

    show "(¬lfinite Ps ∧ valid_play Ps ∧ (∀i. energy_level (the (apply_w v (lhd Ps) e')) Ps i ≠ None ∧
            (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i))
            ∈ reachable_positions s g e ∧
            strategy_order s
             (lnth Ps (Suc i), the (energy_level (the (apply_w v (lhd Ps) e')) Ps (Suc i)))
             (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i)))) ∧
       (v ∈ attacker ⟶ s e' v = Some (lhd Ps))∧ (apply_w v (lhd Ps) e') ≠ None"
    proof
      show "¬lfinite Ps ∧valid_play Ps ∧ (∀i. energy_level (the (apply_w v (lhd Ps) e')) Ps i ≠ None ∧
        (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i))
        ∈ reachable_positions s g e ∧
        strategy_order s
         (lnth Ps (Suc i), the (energy_level (the (apply_w v (lhd Ps) e')) Ps (Suc i)))
         (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i)))" 
      proof
        show "¬ lfinite Ps" using A by simp
        show "valid_play Ps ∧
    (∀i. energy_level (the (apply_w v (lhd Ps) e')) Ps i ≠ None ∧
         (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i))
         ∈ reachable_positions s g e ∧
         strategy_order s
          (lnth Ps (Suc i), the (energy_level (the (apply_w v (lhd Ps) e')) Ps (Suc i)))
          (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i)))"
        proof
          show "valid_play Ps" using A valid_play.simps
            by (metis llist.distinct(1) llist.inject) 
          show "∀i. energy_level (the (apply_w v (lhd Ps) e')) Ps i ≠ None ∧
        (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i))
        ∈ reachable_positions s g e ∧
        strategy_order s
         (lnth Ps (Suc i), the (energy_level (the (apply_w v (lhd Ps) e')) Ps (Suc i)))
         (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i)) "
          proof
            fix i
            show "energy_level (the (apply_w v (lhd Ps) e')) Ps i ≠ None ∧
         (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i))
         ∈ reachable_positions s g e ∧
         strategy_order s
          (lnth Ps (Suc i), the (energy_level (the (apply_w v (lhd Ps) e')) Ps (Suc i)))
          (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i))"
            proof
              from A have "energy_level e' (LCons v Ps) (Suc i) ≠ None" by blast
              from A have "valid_play (LCons v Ps) ∧ ¬ lnull Ps" by simp
              have "apply_w v (lhd Ps) e' ≠ None" using energy_level.simps
                by (metis A lhd_conv_lnth lnth_0 lnth_Suc_LCons option.sel) 
              from A have "enat i < (llength Ps)"
                by (meson Suc_ile_eq ‹¬ lfinite Ps› enat_less_imp_le less_enatE lfinite_conv_llength_enat) 
              have EL: "energy_level (the (apply_w v (lhd Ps) e')) Ps i = energy_level e' (LCons v Ps) (Suc i)"
                using energy_level_cons ‹valid_play (LCons v Ps) ∧ ¬ lnull Ps› ‹apply_w v (lhd Ps) e' ≠ None›
                by (simp add: ‹enat i < llength Ps›)
              thus "energy_level (the (apply_w v (lhd Ps) e')) Ps i ≠ None"
                using ‹energy_level e' (LCons v Ps) (Suc i) ≠ None› by simp
              show "(lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i)) ∈ reachable_positions s g e ∧
    strategy_order s (lnth Ps (Suc i), the (energy_level (the (apply_w v (lhd Ps) e')) Ps (Suc i)))
     (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i))" 
              proof
                have "(lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i)) = (lnth (LCons v Ps) (Suc i), the (energy_level e' (LCons v Ps) (Suc i)))" 
                  using EL by simp
                thus "(lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i)) ∈ reachable_positions s g e"
                  using A by metis 
                have ‹enat (Suc i) < llength Ps›
                  using ‹¬ lfinite Ps› enat_iless linorder_less_linear llength_eq_enat_lfiniteD by blast 
                hence "(lnth Ps (Suc i), the (energy_level (the (apply_w v (lhd Ps) e')) Ps (Suc i)))
                       = (lnth (LCons v Ps) (Suc (Suc i)), the (energy_level e' (LCons v Ps) (Suc (Suc i))))" 
                  using energy_level_cons ‹valid_play (LCons v Ps) ∧ ¬ lnull Ps› ‹apply_w v (lhd Ps) e' ≠ None›
                  by (metis lnth_Suc_LCons)
                thus "strategy_order s (lnth Ps (Suc i), the (energy_level (the (apply_w v (lhd Ps) e')) Ps (Suc i)))
     (lnth Ps i, the (energy_level (the (apply_w v (lhd Ps) e')) Ps i)) " using A
                  by (metis EL lnth_Suc_LCons) 
              qed
            qed
          qed
        qed
      qed
      show "(v ∈ attacker ⟶ s e' v = Some (lhd Ps))∧ (apply_w v (lhd Ps) e') ≠ None"
      proof
        show "v ∈ attacker ⟶ s e' v = Some (lhd Ps)" 
        proof
          assume "v ∈ attacker"
          from A have "strategy_order s (lnth (LCons v Ps) (Suc 0), the (energy_level e' (LCons v Ps) (Suc 0))) (lnth (LCons v Ps) 0, the (energy_level e' (LCons v Ps) 0))"
            by blast 
          hence "strategy_order s ((lhd Ps), the (energy_level e' (LCons v Ps) (Suc 0))) (v, the (energy_level e' (LCons v Ps) 0))"
            by (simp add: A lnth_0_conv_lhd)
          hence "strategy_order s ((lhd Ps), the (energy_level e' (LCons v Ps) (Suc 0))) (v, e')" using energy_level.simps
            by simp
          hence "(if v ∈ attacker then Some (lhd Ps) = s e' v else weight v (lhd Ps) ≠ None)" using strategy_order_def
            using split_beta split_pairs by auto
          thus "s e' v = Some (lhd Ps)" using ‹v ∈ attacker› by auto
        qed
        from A have "energy_level (the (apply_w v (lhd Ps) e')) Ps 0 ≠ None" by auto
        show "apply_w v (lhd Ps) e' ≠ None"
          by (metis A energy_level.simps(1) energy_level.simps(2) eq_LConsD lnth_0 lnth_Suc_LCons not_lnull_conv option.sel) 
      qed
    qed
  qed

  hence "(⋀s v Ps e'.
        Q s (LCons v Ps) e' ∧ ¬ lnull Ps ⟹ (apply_w v (lhd Ps) e') ≠ None ∧
        Q s Ps (the (apply_w v (lhd Ps) e')) ∧ (v ∈ attacker ⟶ s e' v = Some (lhd Ps)))" using Q_def by blast

  hence "play_consistent_attacker s p e0" 
    using ‹Q s p e0› play_consistent_attacker_coinduct
    by metis

  have "valid_play (lappend (LCons g p') (ltl p)) ∧ play_consistent_attacker s (lappend (LCons g p') (ltl p)) e" 
  proof
    have "weight (llast (LCons g p')) (lhd (ltl p)) ≠ None" using P'
      by (metis ‹⋀i. lnth p i = fst (f i)› ‹¬ lfinite p› ‹f 0 = (g0, e0)› ‹valid_play p› fstI lfinite.simps lnth_0 ltl_simps(2) valid_play.cases) 
    show "valid_play (lappend (LCons g p') (ltl p))" using valid_play_append P'
      by (metis (no_types, lifting) ‹¬ lfinite p› ‹valid_play p› ‹weight (llast (LCons g p')) (lhd (ltl p)) ≠ None› lfinite_LConsI lfinite_LNil llist.exhaust_sel ltl_simps(2) valid_play.simps) 

    have "energy_level e (LCons g p') (the_enat (llength p')) ≠ None"
      by (metis P' not_Some_eq) 
    hence A: "lfinite p' ∧ llast (LCons g p') = lhd p ∧ play_consistent_attacker s p (the (energy_level e (LCons g p') (the_enat (llength p'))))
             ∧ play_consistent_attacker s (LCons g p') e ∧ valid_play (LCons g p') ∧ energy_level e (LCons g p') (the_enat (llength p')) ≠ None"
      using P' ‹play_consistent_attacker s p e0› p_def  ‹f 0 = (g0,e0)›
      by (metis ‹⋀i. lnth p i = fst (f i)› ‹¬ lfinite p› fst_conv lhd_conv_lnth lnull_imp_lfinite option.sel)

    show "play_consistent_attacker s (lappend (LCons g p') (ltl p)) e"
      using A proof(induct "the_enat (llength p')" arbitrary: p' g e)
      case 0
      hence "(lappend (LCons g p') (ltl p)) = p"
        by (metis ‹¬ lfinite p› gen_llength_code(1) lappend_code(1) lappend_code(2) lfinite_llength_enat lhd_LCons_ltl llast_singleton llength_LNil llength_code llength_eq_0 llist.collapse(1) the_enat.simps) 
      have "the (energy_level e (LCons g p') (the_enat (llength p'))) = e" using 0 energy_level.simps by auto
      then show ?case using ‹(lappend (LCons g p') (ltl p)) = p› 0 by simp
    next
      case (Suc x)
      hence "lhd p' = lhd (lappend (p') (ltl p))"
        using the_enat_0 by auto
      have "∃Ps. (lappend (LCons g p') (ltl p)) = LCons g Ps"
        by simp 
      from this obtain Ps where "(lappend (LCons g p') (ltl p)) = LCons g Ps" by auto
      hence "(lappend (p') (ltl p)) = Ps" by simp
      
      have "g ∈ attacker ⟶ s e g = Some (lhd Ps)"
      proof
        assume "g ∈ attacker"
        show "s e g = Some (lhd Ps)" 
          using Suc
          by (metis Zero_not_Suc ‹g ∈ attacker› ‹lappend p' (ltl p) = Ps› ‹lhd p' = lhd (lappend p' (ltl p))› lhd_LCons llength_LNil llist.distinct(1) ltl_simps(2) play_consistent_attacker.cases the_enat_0) 
      qed
      have "play_consistent_attacker s (lappend (LCons (lhd p') (ltl p')) (ltl p)) (the (apply_w g (lhd p') e))" 
      proof-
        have "x = the_enat (llength (ltl p'))" using Suc
          by (metis One_nat_def diff_Suc_1' epred_enat epred_llength lfinite_conv_llength_enat the_enat.simps)
        have "lfinite  (ltl p') ∧
    llast (LCons (lhd p') (ltl p')) = lhd p ∧
    play_consistent_attacker s p
     (the (energy_level (the (apply_w g (lhd p') e)) (LCons (lhd p') (ltl p')) (the_enat (llength  (ltl p'))))) ∧
    play_consistent_attacker s (LCons (lhd p') (ltl p')) (the (apply_w g (lhd p') e)) 
      ∧ valid_play (LCons (lhd p') (ltl p')) ∧ energy_level (the (apply_w g (lhd p') e)) (LCons (lhd p') (ltl p')) (the_enat (llength (ltl p'))) ≠ None"
        proof
          show "lfinite  (ltl p')" using Suc lfinite_ltl by simp 
          show "llast (LCons (lhd p') (ltl p')) = lhd p ∧
    play_consistent_attacker s p
     (the (energy_level (the (apply_w g (lhd p') e)) (LCons (lhd p') (ltl p'))
            (the_enat (llength (ltl p'))))) ∧
    play_consistent_attacker s (LCons (lhd p') (ltl p')) (the (apply_w g (lhd p') e)) ∧ 
    valid_play (LCons (lhd p') (ltl p')) ∧ energy_level (the (apply_w g (lhd p') e)) (LCons (lhd p') (ltl p')) (the_enat (llength (ltl p'))) ≠ None"
          proof
            show "llast (LCons (lhd p') (ltl p')) = lhd p" using Suc
              by (metis (no_types, lifting) ‹x = the_enat (llength (ltl p'))› llast_LCons2 llist.exhaust_sel ltl_simps(1) n_not_Suc_n) 
            show "play_consistent_attacker s p
     (the (energy_level (the (apply_w g (lhd p') e)) (LCons (lhd p') (ltl p'))
            (the_enat (llength (ltl p'))))) ∧
    play_consistent_attacker s (LCons (lhd p') (ltl p')) (the (apply_w g (lhd p') e)) ∧ 
    valid_play (LCons (lhd p') (ltl p')) ∧ energy_level (the (apply_w g (lhd p') e)) (LCons (lhd p') (ltl p')) (the_enat (llength (ltl p'))) ≠ None"
            proof
              have "energy_level e (LCons g p') (the_enat (llength p')) ≠ None" using Suc
                by blast 
              hence "apply_w g (lhd p') e ≠ None"
                by (smt (verit) Suc.hyps(2) Suc_leI ‹x = the_enat (llength (ltl p'))› energy_level.simps(1) energy_level_nth llist.distinct(1) llist.exhaust_sel lnth_0 lnth_Suc_LCons ltl_simps(1) n_not_Suc_n option.sel zero_less_Suc)
              hence cons_assms: "valid_play (LCons g p') ∧ ¬ lnull p' ∧ apply_w g (lhd p') e ≠ None ∧ enat (the_enat (llength (ltl p'))) < llength p'"
                using Suc
                by (metis ‹x = the_enat (llength (ltl p'))› enat_ord_simps(2) lessI lfinite_conv_llength_enat lnull_def ltl_simps(1) n_not_Suc_n the_enat.simps) 

              have "(the (energy_level e (LCons g p') (the_enat (llength p')))) = 
                    (the (energy_level e (LCons g p') (Suc (the_enat (llength (ltl p'))))))"
                using Suc.hyps(2) ‹x = the_enat (llength (ltl p'))› by auto
              also have "... = (the (energy_level (the (apply_w g (lhd p') e)) p' (the_enat (llength (ltl p')))))"
                using energy_level_cons cons_assms by simp
              finally have EL: "(the (energy_level e (LCons g p') (the_enat (llength p')))) = 
                    (the (energy_level (the (apply_w g (lhd p') e)) (LCons (lhd p') (ltl p')) (the_enat (llength (ltl p')))))"
                by (simp add: cons_assms)
              thus "play_consistent_attacker s p
     (the (energy_level (the (apply_w g (lhd p') e)) (LCons (lhd p') (ltl p'))
            (the_enat (llength (ltl p')))))"
                using Suc by argo 
              show "play_consistent_attacker s (LCons (lhd p') (ltl p')) (the (apply_w g (lhd p') e))∧ 
                  valid_play (LCons (lhd p') (ltl p')) ∧ energy_level (the (apply_w g (lhd p') e)) (LCons (lhd p') (ltl p')) (the_enat (llength (ltl p'))) ≠ None"
              proof
                show " play_consistent_attacker s (LCons (lhd p') (ltl p')) (the (apply_w g (lhd p') e))"
                  using Suc
                  by (metis cons_assms lhd_LCons lhd_LCons_ltl llist.distinct(1) ltl_simps(2) play_consistent_attacker.simps) 
                show "valid_play (LCons (lhd p') (ltl p')) ∧ energy_level (the (apply_w g (lhd p') e)) (LCons (lhd p') (ltl p')) (the_enat (llength (ltl p'))) ≠ None"
                proof 
                  show "valid_play (LCons (lhd p') (ltl p'))" using Suc
                    by (metis llist.distinct(1) llist.exhaust_sel llist.inject ltl_simps(1) valid_play.simps) 
                  show "energy_level (the (apply_w g (lhd p') e)) (LCons (lhd p') (ltl p')) (the_enat (llength (ltl p'))) ≠ None" 
                    using EL Suc
                    by (metis ‹x = the_enat (llength (ltl p'))› cons_assms energy_level_cons lhd_LCons_ltl) 
                qed
              qed
            qed
          qed
        qed
        thus ?thesis using ‹x = the_enat (llength (ltl p'))› Suc
          by blast 
      qed
      hence "play_consistent_attacker s Ps (the (apply_w g (lhd p') e))" 
        using ‹(lappend (p') (ltl p)) = Ps›
        by (metis Suc.hyps(2) diff_0_eq_0 diff_Suc_1 lhd_LCons_ltl llength_lnull n_not_Suc_n the_enat_0)
      then show ?case using play_consistent_attacker.simps ‹g ∈ attacker ⟶ s e g = Some (lhd Ps)› ‹(lappend (LCons g p') (ltl p)) = LCons g Ps›
        by (metis (no_types, lifting) Suc.prems ‹¬ lfinite p› ‹lappend p' (ltl p) = Ps› ‹lhd p' = lhd (lappend p' (ltl p))› energy_level.simps(1) lappend_code(1) lhd_LCons llast_singleton llength_LNil llist.distinct(1) lnull_lappend ltl_simps(2) option.sel the_enat_0)
    qed
  qed

  hence "¬defender_wins_play e (lappend (LCons g p') (ltl p))" using assms unfolding attacker_winning_strategy.simps using P'
    by simp

  have "¬lfinite (lappend p' p)" using p_def by simp
  hence "defender_wins_play e (lappend (LCons g p') (ltl p))" using defender_wins_play_def by auto
  thus "False" using ‹¬defender_wins_play e (lappend (LCons g p') (ltl p))› by simp 
qed

text‹We now show that an energy-positional attacker winning strategy w.r.t.\ some energy $e$ and position $g$ 
guarantees that $e$ is in the attacker winning budget of $g$.›

lemma winning_budget_implies_ind:
  assumes "winning_budget e g"
  shows "winning_budget_ind e g"
proof-
  define wb where "wb ≡ λ(g,e). winning_budget_ind e g"

  from assms have "∃s. attacker_winning_strategy s e g" using winning_budget.simps by auto
  from this obtain s where S: "attacker_winning_strategy s e g" by auto
  hence "wfp_on (strategy_order s) (reachable_positions s g e)" 
    using strategy_order_well_founded by simp
  hence "inductive_on (strategy_order s) (reachable_positions s g e)"
    by (simp add: wfp_on_iff_inductive_on)

  hence "wb (g,e)" 
  proof(rule inductive_on_induct)
    show "(g,e) ∈ reachable_positions 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') ∧
       (∃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 (metis lfinite_code(1) llast_singleton llength_LNil the_enat_0)
    qed

    show "⋀y. y ∈ reachable_positions s g e ⟹
         (⋀x. x ∈ reachable_positions s g e ⟹ strategy_order s x y ⟹ wb x) ⟹ wb y"
    proof-
      fix y 
      assume "y ∈ reachable_positions 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 "(∃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))))"
        using ‹y ∈ reachable_positions 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 s g e ⟹ strategy_order s x y ⟹ wb x) ⟹ wb y"
      proof-
        assume ind: "(⋀x. x ∈ reachable_positions s g e ⟹ strategy_order s x y ⟹ wb x)"
        have "winning_budget_ind e' g'" 
        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 S 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
            hence "x ∈ reachable_positions s g e" using 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 "wb x" using ind ‹x ∈ reachable_positions s g e› by simp
            hence "winning_budget_ind (the (apply_w g' (the (s e' g')) e')) (the (s e' g'))" using wb_def x_def by simp
            then show ?thesis using ‹g' ∈ attacker› winning_budget_ind.simps
              by (metis (mono_tags, lifting) ‹s e' g' ≠ None ∧ weight g' (the (s e' g')) ≠ None› ‹strategy_order s x y› ‹y = (g', e')› old.prod.case option.distinct(1) strategy_order_def x_def) 
          qed
        next
          case False
          hence "g' ∉ attacker ∧
            (∀g''. weight g' g'' ≠ None ⟶
          apply_w g' g'' e' ≠ None ∧ winning_budget_ind (the (apply_w g' g'' e')) g'')"
          proof
            show "∀g''. weight g' g'' ≠ None ⟶
          apply_w g' g'' e' ≠ None ∧ winning_budget_ind (the (apply_w g' g'' e')) g''"
            proof
              fix g''
              show "weight g' g'' ≠ None ⟶
           apply_w g' g'' e' ≠ None ∧ winning_budget_ind (the (apply_w g' g'' e')) g'' "
              proof
                assume "weight g' g'' ≠ None"
                show "apply_w g' g'' e' ≠ None ∧ winning_budget_ind (the (apply_w g' g'' e')) g''"
                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 "wb x" 
                  proof(rule ind)
                    have "(∃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'))"
                                by (simp add: ‹apply_w g' g'' e' ≠ None›)
                            qed
                          qed
                        qed
                      qed
                    qed

                    thus "x ∈ reachable_positions s g e"
                      using 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'"
                        by (simp add: ‹apply_w g' g'' e' ≠ None›) 
                      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 "winning_budget_ind (the (apply_w g' g'' e')) g'' " using x_def wb_def
                    by force 
                qed
              qed
            qed
          qed
          thus ?thesis using winning_budget_ind.intros by blast
        qed
        thus "wb y" using ‹y = (g', e')› wb_def by simp
      qed
    qed
  qed
  thus ?thesis using wb_def by simp
qed

text ‹We now prepare the proof of ‹winning_budget_ind› characterising subsets of ‹winning_budget_nonpos› for all positions.
For this we introduce a construction to obtain a non-positional attacker winning strategy from a strategy at a next position.›

fun nonpos_strat_from_next:: "'position ⇒ 'position ⇒ 
  ('position list ⇒ 'position option) ⇒ ('position list ⇒ 'position option)" 
where
  "nonpos_strat_from_next g g' s [] = s []" |
  "nonpos_strat_from_next g g' s (x#xs) = (if x=g then (if xs=[] then Some g' 
                                           else s xs) else s (x#xs))"

lemma play_nonpos_consistent_next:
  assumes "play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) (LCons g (LCons g' xs)) []" 
      and "g ∈ attacker" and "xs ≠ LNil"
  shows "play_consistent_attacker_nonpos s (LCons g' xs) []"
proof-
  have X: "⋀l. l≠[] ⟹(((nonpos_strat_from_next g g' s) ([g] @ l)) = s l)" using nonpos_strat_from_next.simps by simp
  have A1: "⋀s v l. play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) (LCons v LNil) ([g]@l) ⟹ (l = [] ∨ (last l) ∉ attacker ∨ ((last l)∈attacker ∧ the (s l) = v))" 
  proof-
    fix s v l
    assume "play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) (LCons v LNil) ([g] @ l)"
    show "l = [] ∨ last l ∉ attacker ∨ last l ∈ attacker ∧ the (s l) = v " 
    proof(cases "l=[]")
      case True
      then show ?thesis by simp
    next
      case False
      hence "l ≠ []" .
      then show ?thesis proof(cases "last l ∉ attacker")
        case True
        then show ?thesis by simp
      next
        case False
        hence "the ((nonpos_strat_from_next g g' s) ([g] @ l)) = v"
          by (smt (verit) ‹play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) (LCons v LNil) ([g] @ l)› append_is_Nil_conv assms(2) eq_LConsD last.simps last_append lhd_LCons list.distinct(1) llist.disc(1) play_consistent_attacker_nonpos.simps) 
        hence "the (s l) = v" using X ‹l ≠ []› by auto
        then show ?thesis using False by simp
      qed
    qed
  qed

  have A2: "⋀s v Ps l. play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) (LCons v Ps) ([g]@l) ∧ Ps≠LNil ⟹ play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) Ps ([g]@(l@[v])) ∧ (v∈attacker ⟶ lhd Ps = the (s (l@[v])))" 
  proof-
    fix s v Ps l
    assume play_cons: "play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) (LCons v Ps) ([g]@l) ∧ Ps≠LNil"
    show "play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) Ps ([g]@(l@[v])) ∧ (v∈attacker ⟶ lhd Ps = the (s (l@[v])))" 
    proof
      show "play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) Ps ([g]@(l@[v]))" using play_cons play_consistent_attacker_nonpos.simps
        by (smt (verit) append_assoc lhd_LCons llist.distinct(1) ltl_simps(2))
      show "v ∈ attacker ⟶ lhd Ps = the (s (l @ [v]))" 
      proof
        assume "v ∈ attacker"
        hence "lhd Ps = the ((nonpos_strat_from_next g g' s) ([g]@(l @ [v])))" using play_cons play_consistent_attacker_nonpos.simps
          by (smt (verit) append_assoc lhd_LCons llist.distinct(1) ltl_simps(2))
        thus "lhd Ps = the (s (l @ [v]))" using X by auto
      qed
    qed
  qed

  have "play_consistent_attacker_nonpos s xs [g']" proof (rule play_consistent_attacker_nonpos_coinduct)
    show "play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) xs ([g]@[g'])" using assms(1)
      by (metis A2 append_Cons append_Nil assms(3) llist.distinct(1) play_consistent_attacker_nonpos_cons_simp) 
    show "⋀s v l.
       play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) (LCons v LNil) ([g] @ l) ⟹
       l = [] ∨ last l ∉ attacker ∨ last l ∈ attacker ∧ the (s l) = v" using A1 by auto
    show "⋀s v Ps l.
       play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) (LCons v Ps) ([g] @ l) ∧ Ps ≠ LNil ⟹
       play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) Ps ([g] @ l @ [v]) ∧ (v ∈ attacker ⟶ lhd Ps = the (s (l @ [v])))" using A2 by auto
  qed

  thus ?thesis
    by (metis A2 append.left_neutral append_Cons assms(1) llist.distinct(1) lnull_def play_consistent_attacker_nonpos_cons_simp) 
qed

text‹We now introduce a construction to obtain a non-positional attacker winning strategy from a strategy at a previous position.›

fun nonpos_strat_from_previous:: "'position ⇒ 'position ⇒ 
  ('position list ⇒ 'position option) ⇒ ('position list ⇒ 'position option)" 
where
  "nonpos_strat_from_previous g g' s [] = s []" |
  "nonpos_strat_from_previous g g' s (x#xs) = (if x=g' then s (g#(g'#xs)) 
                                               else s (x#xs))"

lemma play_nonpos_consistent_previous: 
  assumes "play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) p ([g']@l)" 
          and "g∈attacker ⟹ g'=the (s [g])"
  shows "play_consistent_attacker_nonpos s p ([g,g']@l)"
proof(rule play_consistent_attacker_nonpos_coinduct)
  show "play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) p (tl([g,g']@l)) ∧ length ([g,g']@l) > 1 ∧ hd ([g,g']@l) = g ∧ hd (tl ([g,g']@l)) = g'" using assms(1) by simp
  have X: "⋀l. nonpos_strat_from_previous g g' s ([g']@l) = s ([g,g']@l)" using nonpos_strat_from_previous.simps by simp
  have Y: "⋀l. hd l ≠ g' ⟹ nonpos_strat_from_previous g g' s l = s l" using nonpos_strat_from_previous.simps
    by (metis list.sel(1) neq_Nil_conv) 
  show "⋀s v l.
       play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) (LCons v LNil) (tl l) ∧ 1 < length l ∧ hd l = g ∧ hd (tl l) = g' ⟹
       l = [] ∨ last l ∉ attacker ∨ last l ∈ attacker ∧ the (s l) = v"
  proof-
    fix s v l
    assume A: "play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) (LCons v LNil) (tl l) ∧ 1 < length l ∧ hd l = g ∧ hd (tl l) = g'"
    show "l = [] ∨ last l ∉ attacker ∨ last l ∈ attacker ∧ the (s l) = v" 
    proof(cases "last l ∈ attacker")
      case True
      hence "last (tl l) ∈ attacker"
        by (metis A hd_Cons_tl last_tl less_Suc0 remdups_adj.simps(2) remdups_adj_singleton remdups_adj_singleton_iff zero_neq_one) 
      hence "the (nonpos_strat_from_previous g g' s (tl l)) = v" using play_consistent_attacker_nonpos.simps A
        by (smt (verit) length_tl less_numeral_extra(3) list.size(3) llist.disc(1) llist.distinct(1) llist.inject zero_less_diff)
      hence "the (s l) = v" using X A
        by (smt (verit, del_insts) One_nat_def hd_Cons_tl length_Cons less_numeral_extra(4) list.inject list.size(3) not_one_less_zero nonpos_strat_from_previous.elims) 
      then show ?thesis by simp
    next
      case False
      then show ?thesis by simp
    qed
  qed
  show "⋀s v Ps l.
       (play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) (LCons v Ps) (tl l) ∧
        1 < length l ∧ hd l = g ∧ hd (tl l) = g') ∧
       Ps ≠ LNil ⟹
       (play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) Ps (tl (l @ [v])) ∧
        1 < length (l @ [v]) ∧ hd (l @ [v]) = g ∧ hd (tl (l @ [v])) = g') ∧
       (v ∈ attacker ⟶ lhd Ps = the (s (l @ [v])))" 
  proof-
    fix s v Ps l
    assume A: "(play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) (LCons v Ps) (tl l) ∧
        1 < length l ∧ hd l = g ∧ hd (tl l) = g') ∧ Ps ≠ LNil"
    show "(play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) Ps (tl (l @ [v])) ∧
        1 < length (l @ [v]) ∧ hd (l @ [v]) = g ∧ hd (tl (l @ [v])) = g') ∧
       (v ∈ attacker ⟶ lhd Ps = the (s (l @ [v])))" 
    proof 
      show "play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) Ps (tl (l @ [v])) ∧
    1 < length (l @ [v]) ∧ hd (l @ [v]) = g ∧ hd (tl (l @ [v])) = g'" 
      proof
        show "play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) Ps (tl (l @ [v]))" using A play_consistent_attacker_nonpos.simps
          by (smt (verit) lhd_LCons list.size(3) llist.distinct(1) ltl_simps(2) not_one_less_zero tl_append2)
        show "1 < length (l @ [v]) ∧ hd (l @ [v]) = g ∧ hd (tl (l @ [v])) = g'" using A
          by (metis Suc_eq_plus1 add.comm_neutral add.commute append_Nil hd_append2 length_append_singleton less_numeral_extra(4) list.exhaust_sel list.size(3) tl_append2 trans_less_add2)
      qed
      show "v ∈ attacker ⟶ lhd Ps = the (s (l @ [v]))" 
      proof
        assume "v ∈ attacker"
        hence "lhd Ps = the ((nonpos_strat_from_previous g g' s) (tl (l @ [v])))" using A play_consistent_attacker_nonpos.simps
          by (smt (verit) lhd_LCons list.size(3) llist.distinct(1) ltl_simps(2) not_one_less_zero tl_append2)
        thus "lhd Ps = the (s (l @ [v]))" using X A
          by (smt (verit, ccfv_SIG) One_nat_def Suc_lessD ‹play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) Ps (tl (l @ [v])) ∧ 1 < length (l @ [v]) ∧ hd (l @ [v]) = g ∧ hd (tl (l @ [v])) = g'› butlast.simps(2) butlast_snoc hd_Cons_tl length_greater_0_conv list.inject nonpos_strat_from_previous.elims) 
   
      qed
    qed
  qed
qed

text‹With these constructions we can show that the winning budgets defined by non-positional strategies are a fixed point of the inductive characterisation.
›
lemma nonpos_winning_budget_implies_inductive: 
  assumes "nonpos_winning_budget e g"
  shows "g ∈ attacker ⟹ (∃g'. (weight g g' ≠ None) ∧ (apply_w g g' e)≠ None
         ∧ (nonpos_winning_budget (the (apply_w g g' e)) g'))" and 
        "g ∉ attacker ⟹ (∀g'. (weight g g' ≠ None) ⟶ (apply_w g g' e)≠ None
         ∧ (nonpos_winning_budget (the (apply_w g g' e)) g'))"
proof-
  from assms obtain s where S: "nonpos_attacker_winning_strategy s e g" unfolding nonpos_winning_budget.simps by auto
  show "g ∈ attacker ⟹ (∃g'. (weight g g' ≠ None) ∧ (apply_w g g' e)≠ None ∧ (nonpos_winning_budget (the (apply_w g g' e)) g'))" 
  proof-
    assume "g∈ attacker"
    have finite: "lfinite (LCons g LNil)" by simp
    have play_cons_g: "play_consistent_attacker_nonpos s (LCons g LNil) []"
      by (simp add: play_consistent_attacker_nonpos.intros(2)) 
    have valid_play_g: "valid_play (LCons g LNil)"
      by (simp add: valid_play.intros(2)) 
    hence "¬defender_wins_play e (LCons g LNil)" using nonpos_attacker_winning_strategy.simps S play_cons_g by auto
    hence "¬ deadend g" using finite defender_wins_play_def
      by (simp add: ‹g ∈ attacker›) 
    hence "s [g] ≠ None" using nonpos_attacker_winning_strategy.simps attacker_nonpos_strategy_def S
      by (simp add: ‹g ∈ attacker›) 
    show "(∃g'. (weight g g' ≠ None) ∧ (apply_w g g' e)≠ None ∧ (nonpos_winning_budget (the (apply_w g g' e)) g'))" 
    proof
      show "weight g (the (s [g])) ≠ None ∧ apply_w g (the (s [g])) e ≠ None ∧ nonpos_winning_budget (the (apply_w g (the (s [g])) e)) (the (s [g]))"
      proof
        show "weight g (the (s [g])) ≠ None" using nonpos_attacker_winning_strategy.simps attacker_nonpos_strategy_def S ‹¬ deadend g›
          using ‹g ∈ attacker› by (metis last_ConsL not_Cons_self2)
        show "apply_w g (the (s [g])) e ≠ None ∧
              nonpos_winning_budget (the (apply_w g (the (s [g])) e)) (the (s [g]))" 
        proof
          show "apply_w g (the (s [g])) e ≠ None" 
          proof-
            have finite: "lfinite (LCons g (LCons (the (s [g])) LNil))" by simp
            have play_cons_g': "play_consistent_attacker_nonpos s (LCons g (LCons (the (s [g])) LNil)) []" using play_cons_g play_consistent_attacker_nonpos.intros
              by (metis append_Nil lhd_LCons llist.disc(2))
            have valid_play_g': "valid_play (LCons g (LCons (the (s [g])) LNil))" using valid_play.intros valid_play_g
              using ‹weight g (the (s [g])) ≠ None› by auto
            hence "¬defender_wins_play e (LCons g (LCons (the (s [g])) LNil))" using nonpos_attacker_winning_strategy.simps S play_cons_g' by auto
            hence notNone: "energy_level e (LCons g (LCons (the (s [g])) LNil)) 1 ≠ None" using finite defender_wins_play_def
              by (metis One_nat_def diff_Suc_1 length_Cons length_list_of_conv_the_enat lfinite_LConsI lfinite_LNil list.size(3) list_of_LCons list_of_LNil)
            hence "energy_level e (LCons g (LCons (the (s [g])) LNil)) 1 = apply_w (lnth (LCons g (LCons (the (s [g])) LNil)) 0)(lnth (LCons g (LCons (the (s [g])) LNil)) 1) (the (energy_level e (LCons g (LCons (the (s [g])) LNil)) 0))"
              using energy_level.simps by (metis One_nat_def) 
            hence "energy_level e (LCons g (LCons (the (s [g])) LNil)) 1 = apply_w g (the (s [g])) e" by simp
            thus "apply_w g (the (s [g])) e ≠ None" using notNone by simp
          qed

          show "nonpos_winning_budget (the (apply_w g (the (s [g])) e)) (the (s [g]))" 
            unfolding nonpos_winning_budget.simps proof
            show "nonpos_attacker_winning_strategy (nonpos_strat_from_previous g (the (s [g])) s) (the (apply_w g (the (s [g])) e)) (the (s [g]))" 
              unfolding nonpos_attacker_winning_strategy.simps proof
              show "attacker_nonpos_strategy (nonpos_strat_from_previous g (the (s [g])) s)" using S nonpos_strat_from_previous.simps
                by (smt (verit) nonpos_strat_from_previous.elims nonpos_attacker_winning_strategy.elims(2) attacker_nonpos_strategy_def last.simps list.distinct(1)) 
              show "∀p. play_consistent_attacker_nonpos (nonpos_strat_from_previous g (the (s [g])) s) (LCons (the (s [g])) p) [] ∧
                    valid_play (LCons (the (s [g])) p) ⟶
                    ¬ defender_wins_play (the (apply_w g (the (s [g])) e)) (LCons (the (s [g])) p) " 
              proof 
                fix p 
                show "play_consistent_attacker_nonpos (nonpos_strat_from_previous g (the (s [g])) s) (LCons (the (s [g])) p) [] ∧
                    valid_play (LCons (the (s [g])) p) ⟶
                    ¬ defender_wins_play (the (apply_w g (the (s [g])) e)) (LCons (the (s [g])) p) "
                proof 
                  assume A: "play_consistent_attacker_nonpos (nonpos_strat_from_previous g (the (s [g])) s) (LCons (the (s [g])) p) [] ∧
                    valid_play (LCons (the (s [g])) p)"

                  hence play_cons: "play_consistent_attacker_nonpos s (LCons g (LCons (the (s [g])) p)) []" 
                  proof(cases "p = LNil")
                    case True
                    then show ?thesis using nonpos_strat_from_previous.simps play_consistent_attacker_nonpos.simps
                      by (smt (verit) lhd_LCons llist.discI(2) self_append_conv2) 
                  next
                    case False
                    hence "play_consistent_attacker_nonpos (nonpos_strat_from_previous g (the (s [g])) s) p [(the (s [g]))]" using A play_consistent_attacker_nonpos.cases
                      using eq_Nil_appendI lhd_LCons by fastforce
                    have "(the (s [g])) ∈ attacker ⟹ lhd p = the ((nonpos_strat_from_previous g (the (s [g])) s) [(the (s [g]))])" using A play_consistent_attacker_nonpos.cases
                      by (simp add: False play_consistent_attacker_nonpos_cons_simp)
                    hence "(the (s [g])) ∈ attacker ⟹ lhd p = the (s [g,(the (s [g]))])" using nonpos_strat_from_previous.simps by simp
                    then show ?thesis using play_nonpos_consistent_previous
                      by (smt (verit, del_insts) False ‹play_consistent_attacker_nonpos (nonpos_strat_from_previous g (the (s [g])) s) p [the (s [g])]› append_Cons lhd_LCons llist.collapse(1) play_consistent_attacker_nonpos.intros(5) play_consistent_attacker_nonpos.intros(6) play_consistent_attacker_nonpos_cons_simp self_append_conv2) 
                  qed

                  from A have "valid_play (LCons g (LCons (the (s [g])) p))"
                    using ‹weight g (the (s [g])) ≠ None› valid_play.intros(3) by auto 
                  hence not_won: "¬ defender_wins_play e (LCons g (LCons (the (s [g])) p))" using S play_cons by simp 
                  hence "lfinite (LCons g (LCons (the (s [g])) p))" using defender_wins_play_def by simp
                  hence finite: "lfinite (LCons (the (s [g])) p)" by simp

                  from not_won have no_deadend: "¬(llast (LCons (the (s [g])) p) ∈ attacker ∧ deadend (llast (LCons (the (s [g])) p)))"
                    by (simp add: defender_wins_play_def)

                  have suc: "Suc (the_enat (llength (LCons (the (s [g])) p)) - 1) = (the_enat (llength (LCons g (LCons (the (s [g])) p))) - 1)" using finite
                    by (smt (verit, ccfv_SIG) Suc_length_conv diff_Suc_1 length_list_of_conv_the_enat lfinite_LCons list_of_LCons)                
                  have " the_enat (llength (LCons (the (s [g])) p)) - 1 < the_enat (llength (LCons (the (s [g])) p))" using finite
                     by (metis (no_types, lifting) diff_less lfinite_llength_enat llength_eq_0 llist.disc(2) not_less_less_Suc_eq the_enat.simps zero_enat_def zero_less_Suc zero_less_one) 
                   hence cons_e_l:"valid_play (LCons g (LCons (the (s [g])) p)) ∧  lfinite (LCons (the (s [g])) p) ∧  ¬ lnull (LCons (the (s [g])) p) ∧  apply_w g (lhd (LCons (the (s [g])) p)) e ≠ None ∧ the_enat (llength (LCons (the (s [g])) p)) - 1 < the_enat (llength (LCons (the (s [g])) p))"
                     using ‹valid_play (LCons g (LCons (the (s [g])) p))› finite ‹apply_w g (the (s [g])) e ≠ None› by simp 

                  from not_won have "energy_level e (LCons g (LCons (the (s [g])) p)) (the_enat (llength (LCons g (LCons (the (s [g])) p))) - 1) ≠ None"
                    by (simp add: defender_wins_play_def)
                  hence "energy_level (the (apply_w g (the (s [g])) e)) (LCons (the (s [g])) p) (the_enat (llength (LCons (the (s [g])) p)) - 1) ≠ None" 
                    using energy_level_cons cons_e_l suc
                    by (metis enat_ord_simps(2) eq_LConsD length_list_of length_list_of_conv_the_enat)

                  thus "¬ defender_wins_play (the (apply_w g (the (s [g])) e)) (LCons (the (s [g])) p) " using finite no_deadend defender_wins_play_def by simp
                qed
              qed
            qed
          qed
        qed
      qed
    qed
  qed
  show "g ∉ attacker ⟹ (∀g'. (weight g g' ≠ None) ⟶ (apply_w g g' e)≠ None ∧ (nonpos_winning_budget (the (apply_w g g' e)) g'))"
  proof-
    assume "g∉attacker"
    show "(∀g'. (weight g g' ≠ None) ⟶ (apply_w g g' e)≠ None ∧ (nonpos_winning_budget (the (apply_w g g' e)) g'))"
    proof
      fix g'
      show "(weight g g' ≠ None) ⟶ (apply_w g g' e)≠ None ∧ (nonpos_winning_budget (the (apply_w g g' e)) g')"
      proof 
        assume "(weight g g' ≠ None)"
        show "(apply_w g g' e)≠ None ∧ (nonpos_winning_budget (the (apply_w g g' e)) g')"
        proof
          have "valid_play (LCons g (LCons g' LNil))" using ‹(weight g g' ≠ None)›
            by (simp add: valid_play.intros(2) valid_play.intros(3))
          have "play_consistent_attacker_nonpos s (LCons g' LNil) [g]" using play_consistent_attacker_nonpos.intros(3)
            by (simp add: ‹g ∉ attacker›)
          hence "play_consistent_attacker_nonpos s (LCons g (LCons g' LNil)) []" using ‹g∉attacker› play_consistent_attacker_nonpos.intros(5) by simp
          hence "¬defender_wins_play e (LCons g (LCons g' LNil))" using ‹valid_play (LCons g (LCons g' LNil))› S by simp
          hence "energy_level e (LCons g (LCons g' LNil)) (the_enat (llength (LCons g (LCons g' LNil)))-1) ≠ None" using defender_wins_play_def by simp
          hence "energy_level e (LCons g (LCons g' LNil)) 1 ≠ None"
            by (metis One_nat_def diff_Suc_1 length_Cons length_list_of_conv_the_enat lfinite_LConsI lfinite_LNil list.size(3) list_of_LCons list_of_LNil)
          thus "apply_w g g' e ≠ None" using energy_level.simps
            by (metis One_nat_def lnth_0 lnth_Suc_LCons option.sel)
         
          show "(nonpos_winning_budget (the (apply_w g g' e)) g')"
            unfolding nonpos_winning_budget.simps proof
            show "nonpos_attacker_winning_strategy (nonpos_strat_from_previous g g' s) (the (apply_w g g' e)) g'"
              unfolding nonpos_attacker_winning_strategy.simps proof
              show "attacker_nonpos_strategy (nonpos_strat_from_previous g g' s)" using S
                by (smt (verit, del_insts) nonpos_strat_from_previous.elims nonpos_attacker_winning_strategy.elims(2) attacker_nonpos_strategy_def last_ConsR list.distinct(1)) 
              show "∀p. play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) (LCons g' p) [] ∧ valid_play (LCons g' p) ⟶
                    ¬ defender_wins_play (the (apply_w g g' e)) (LCons g' p)"
              proof
                fix p
                show "play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) (LCons g' p) [] ∧ valid_play (LCons g' p) ⟶
                      ¬ defender_wins_play (the (apply_w g g' e)) (LCons g' p) "
                proof
                  assume A: "play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) (LCons g' p) [] ∧ valid_play (LCons g' p)" 
                  hence "valid_play (LCons g (LCons g' p))"
                    using ‹weight g g' ≠ None› valid_play.intros(3) by auto


                  from A have "play_consistent_attacker_nonpos (nonpos_strat_from_previous g g' s) p [g']"
                    using play_consistent_attacker_nonpos.intros(1) play_consistent_attacker_nonpos_cons_simp by auto
                  hence "play_consistent_attacker_nonpos s p [g,g']" using play_nonpos_consistent_previous ‹g∉attacker›
                    by fastforce 
                  hence "play_consistent_attacker_nonpos s (LCons g (LCons g' p)) []"
                    by (smt (verit) A Cons_eq_appendI ‹play_consistent_attacker_nonpos s (LCons g (LCons g' LNil)) []› eq_Nil_appendI lhd_LCons llist.discI(2) llist.distinct(1) ltl_simps(2) play_consistent_attacker_nonpos.simps nonpos_strat_from_previous.simps(2))
                  hence not_won: "¬defender_wins_play e (LCons g (LCons g' p))" using S ‹valid_play (LCons g (LCons g' p))› by simp
                  hence finite: "lfinite (LCons g' p)"
                    by (simp add: defender_wins_play_def)

                  from not_won have no_deadend: "¬(llast (LCons g' p) ∈ attacker ∧ deadend (llast (LCons g' p)))" using defender_wins_play_def by simp
                    
                  have suc: "Suc ((the_enat (llength (LCons g' p)) - 1)) = (the_enat (llength (LCons g (LCons g' p))) - 1)" 
                    using finite
                    by (smt (verit, ccfv_SIG) Suc_length_conv diff_Suc_1 length_list_of_conv_the_enat lfinite_LCons list_of_LCons) 
                  from not_won have "energy_level e (LCons g (LCons g' p)) (the_enat (llength (LCons g (LCons g' p))) - 1) ≠ None" using defender_wins_play_def by simp
                  hence "energy_level (the (apply_w g g' e)) (LCons g' p) (the_enat (llength (LCons g' p)) - 1) ≠ None"
                    using suc energy_level_cons
                    by (smt (verit, best) One_nat_def Suc_diff_Suc Suc_lessD ‹apply_w g g' e ≠ None› ‹valid_play (LCons g (LCons g' p))› diff_zero enat_ord_simps(2) energy_level.elims lessI lfinite_conv_llength_enat lhd_LCons llist.discI(2) llist.distinct(1) local.finite option.collapse the_enat.simps zero_less_Suc zero_less_diff)
                    thus  " ¬ defender_wins_play (the (apply_w g g' e)) (LCons g' p)" using defender_wins_play_def finite no_deadend by simp
                qed
              qed
            qed
          qed
        qed
      qed
    qed
  qed
qed

lemma inductive_implies_nonpos_winning_budget: 
  shows "g ∈ attacker ⟹ (∃g'. (weight g g' ≠ None) ∧ (apply_w g g' e)≠ None
         ∧ (nonpos_winning_budget (the (apply_w g g' e)) g')) 
        ⟹ nonpos_winning_budget e g" 
        and "g ∉ attacker ⟹ (∀g'. (weight g g' ≠ None) 
        ⟶ (apply_w g g' e)≠ None 
        ∧ (nonpos_winning_budget (the (apply_w g g' e)) g'))
        ⟹ nonpos_winning_budget e g"
proof-
  assume "g ∈ attacker" 
  assume "(∃g'. (weight g g' ≠ None) ∧ (apply_w g g' e)≠ None ∧ (nonpos_winning_budget (the (apply_w g g' e)) g'))"

  from this obtain g' where A1: "(weight g g' ≠ None) ∧ (apply_w g g' e)≠ None ∧ (nonpos_winning_budget (the (apply_w g g' e)) g')" by auto
  hence "∃s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g'" using nonpos_winning_budget.simps by auto
  from this obtain s where s_winning: "nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g'" by auto
  have "nonpos_attacker_winning_strategy (nonpos_strat_from_next g g' s) e g" unfolding nonpos_attacker_winning_strategy.simps 
  proof
    show "attacker_nonpos_strategy (nonpos_strat_from_next g g' s)" 
      unfolding attacker_nonpos_strategy_def proof
      fix list 
      show "list ≠ [] ⟶
       last list ∈ attacker ∧ ¬ deadend (last list) ⟶
       nonpos_strat_from_next g g' s list ≠ None ∧ weight (last list) (the (nonpos_strat_from_next g g' s list)) ≠ None" 
      proof 
        assume "list ≠ []"
        show "last list ∈ attacker ∧ ¬ deadend (last list) ⟶
               nonpos_strat_from_next g g' s list ≠ None ∧ weight (last list) (the (nonpos_strat_from_next g g' s list)) ≠ None" 
        proof 
          assume "last list ∈ attacker ∧ ¬ deadend (last list)"
          show "nonpos_strat_from_next g g' s list ≠ None ∧ weight (last list) (the (nonpos_strat_from_next g g' s list)) ≠ None "
          proof
            from s_winning have "attacker_nonpos_strategy s" by auto
            thus "nonpos_strat_from_next g g' s list ≠ None" using nonpos_strat_from_next.simps(2) ‹list ≠ []› ‹last list ∈ attacker ∧ ¬ deadend (last list)›
              by (smt (verit) nonpos_strat_from_next.elims attacker_nonpos_strategy_def last_ConsR option.discI)
            show "weight (last list) (the (nonpos_strat_from_next g g' s list)) ≠ None " using nonpos_strat_from_next.simps(2) ‹list ≠ []› ‹last list ∈ attacker ∧ ¬ deadend (last list)›
              by (smt (verit) A1 ‹attacker_nonpos_strategy s› nonpos_strat_from_next.elims attacker_nonpos_strategy_def last_ConsL last_ConsR option.sel)
          qed
        qed
      qed
    qed
    show "∀p. play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) (LCons g p) [] ∧ valid_play (LCons g p) ⟶
        ¬ defender_wins_play e (LCons g p) "
    proof
      fix p
      show "play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) (LCons g p) [] ∧ valid_play (LCons g p) ⟶
        ¬ defender_wins_play e (LCons g p)" 
      proof 
        assume A: "play_consistent_attacker_nonpos (nonpos_strat_from_next g g' s) (LCons g p)[] ∧ valid_play (LCons g p)"
        hence "play_consistent_attacker_nonpos s p []" 
        proof(cases "p=LNil")
          case True
          then show ?thesis
            by (simp add: play_consistent_attacker_nonpos.intros(1)) 
        next
          case False
          hence "∃v p'. p=LCons v p'"
            by (meson llist.exhaust)
          from this obtain v p' where "p= LCons v p'" by auto
          then show ?thesis 
          proof(cases "p'=LNil")
            case True
            then show ?thesis
              by (simp add: ‹p = LCons v p'› play_consistent_attacker_nonpos.intros(2)) 
          next
            case False
            from ‹p= LCons v p'› have "v=g'" using A nonpos_strat_from_next.simps play_nonpos_consistent_previous ‹g ∈ attacker›
              by (simp add: play_consistent_attacker_nonpos_cons_simp)
            then show ?thesis using ‹p= LCons v p'› A nonpos_strat_from_next.simps play_nonpos_consistent_next
              using False ‹g ∈ attacker› by blast
          qed
        qed

        have "valid_play p" using A valid_play.simps
          by (metis eq_LConsD) 
        hence notNil: "p≠LNil ⟹ ¬ defender_wins_play (the (apply_w g g' e)) p" using s_winning ‹play_consistent_attacker_nonpos s p []› nonpos_attacker_winning_strategy.elims
          by (metis A ‹g ∈ attacker› lhd_LCons not_lnull_conv option.sel play_consistent_attacker_nonpos_cons_simp nonpos_strat_from_next.simps(2))
        show " ¬ defender_wins_play e (LCons g p)" 
        proof(cases "p=LNil")
          case True
          hence "lfinite (LCons g p)" by simp
          have "llast  (LCons g p) = g" using True by simp
          hence not_deadend: "¬ deadend (llast  (LCons g p))" using A1 by auto 
          have "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None" using True
            by (simp add: gen_llength_code(1) gen_llength_code(2) llength_code)
          then show ?thesis using defender_wins_play_def not_deadend ‹lfinite (LCons g p)› by simp
        next
          case False
          hence "¬ defender_wins_play (the (apply_w g g' e)) p" using notNil by simp
          hence not: "lfinite p ∧ energy_level (the (apply_w g g' e)) p (the_enat (llength p) - 1) ≠ None ∧ ¬(llast p ∈ attacker ∧ deadend (llast p))" using defender_wins_play_def
            by simp 
          hence "lfinite (LCons g p)" by simp

          from False have "llast (LCons g p) = llast p"
            by (meson llast_LCons llist.collapse(1)) 
          hence "¬(llast (LCons g p) ∈ attacker ∧ deadend (llast (LCons g p)))" using not by simp

          from  ‹lfinite (LCons g p)› have "the_enat (llength (LCons g p)) = Suc (the_enat (llength p))"
            by (metis eSuc_enat lfinite_LCons lfinite_conv_llength_enat llength_LCons the_enat.simps)
          hence E:"(the_enat (llength (LCons g p)) - 1) = Suc (the_enat (llength p) - 1)" using ‹lfinite (LCons g p)› False
            by (metis diff_Suc_1 diff_self_eq_0 gr0_implies_Suc i0_less less_enatE less_imp_diff_less lfinite_llength_enat llength_eq_0 llist.collapse(1) not the_enat.simps) 

          from False have "lhd p = g'" using A nonpos_strat_from_next.simps play_nonpos_consistent_previous ‹g∈attacker›
            by (simp add: play_consistent_attacker_nonpos_cons_simp)
          hence "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) = energy_level (the (apply_w g g' e)) p (the_enat (llength p) - 1)" 
            using energy_level_cons A not False A1 E
            by (metis ‹the_enat (llength (LCons g p)) = Suc (the_enat (llength p))› diff_Suc_1 enat_ord_simps(2) lessI lfinite_conv_llength_enat play_consistent_attacker_nonpos_cons_simp the_enat.simps)
          hence "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1) ≠ None" using not by auto 
          then show ?thesis using defender_wins_play_def ‹lfinite (LCons g p)› ‹¬(llast (LCons g p) ∈ attacker ∧ deadend (llast (LCons g p)))› by auto
        qed
      qed
    qed
  qed
  thus "nonpos_winning_budget e g" using nonpos_winning_budget.simps by auto
next
  assume "g ∉ attacker"
  assume all: "(∀g'. (weight g g' ≠ None) ⟶ (apply_w g g' e)≠ None ∧ (nonpos_winning_budget (the (apply_w g g' e)) g'))"

  have valid: "attacker_nonpos_strategy (λlist. (case list of
              [] ⇒ None |
              [x] ⇒ (if x ∈ attacker ∧ ¬deadend x then Some (SOME y. weight x y ≠ None) else None) |
              (x#(g'#xs)) ⇒ (if (x=g ∧ weight x g' ≠ None) then ((SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g' ) (g'#xs))
                              else (if (last (x#(g'#xs))) ∈ attacker ∧ ¬deadend (last (x#(g'#xs))) then Some (SOME y. weight (last (x#(g'#xs))) y ≠ None) else None))))"
    unfolding attacker_nonpos_strategy_def proof
    fix list
    show "list ≠ [] ⟶
       last list ∈ attacker ∧ ¬ deadend (last list) ⟶
       (case list of [] ⇒ None | [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
        | x # g' # xs ⇒
            if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
            else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                 then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None) ≠
       None ∧
       weight (last list)
        (the (case list of [] ⇒ None | [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
              | x # g' # xs ⇒
                  if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
                  else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                       then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None)) ≠
       None"
    proof
      assume "list ≠ []"
      show "last list ∈ attacker ∧ ¬ deadend (last list) ⟶
    (case list of [] ⇒ None | [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
     | x # g' # xs ⇒
         if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
         else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
              then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None) ≠
    None ∧
    weight (last list)
     (the (case list of [] ⇒ None | [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
           | x # g' # xs ⇒
               if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
               else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                    then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None)) ≠
    None"
      proof 
        assume "last list ∈ attacker ∧ ¬ deadend (last list)"
        show "(case list of [] ⇒ None | [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
     | x # g' # xs ⇒
         if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
         else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
              then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None) ≠
    None ∧
    weight (last list)
     (the (case list of [] ⇒ None | [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
           | x # g' # xs ⇒
               if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
               else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                    then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None)) ≠
    None"
        proof
          show "(case list of [] ⇒ None | 
                [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
                | x # g' # xs ⇒
                if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
                else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                      then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None) ≠ None"
          proof(cases "length list = 1")
            case True
            then show ?thesis
              by (smt (verit) One_nat_def ‹last list ∈ attacker ∧ ¬ deadend (last list)› append_butlast_last_id append_eq_Cons_conv butlast_snoc length_0_conv length_Suc_conv_rev list.simps(4) list.simps(5) option.discI) 
          next
            case False
            hence "∃x y xs. list = x # (y # xs)"
              by (metis One_nat_def ‹list ≠ []› length_Cons list.exhaust list.size(3))
            from this obtain x y xs where "list = x # (y # xs)" by auto
            then show ?thesis proof(cases "(x=g ∧ weight x y ≠ None)")
              case True
              hence A: "(case list of [] ⇒ None | 
                [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
                | x # g' # xs ⇒
                if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
                else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                      then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None) = (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g y e)) y) (y#xs)"
                using ‹list = x # y # xs› list.simps(5) by fastforce

              from all True have "∃s. nonpos_attacker_winning_strategy s (the (apply_w g y e)) y" by auto
              hence "nonpos_attacker_winning_strategy (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g y e)) y) (the (apply_w g y e)) y" 
                using some_eq_ex by metis 
              hence "attacker_nonpos_strategy (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g y e)) y)"
                by (meson nonpos_attacker_winning_strategy.simps)
              hence "(SOME s. nonpos_attacker_winning_strategy s (the (apply_w g y e)) y) (y#xs) ≠ None" 
                using ‹last list ∈ attacker ∧ ¬ deadend (last list)› ‹list = x # (y # xs)›
                by (simp add: list.distinct(1) attacker_nonpos_strategy_def) 

              then show ?thesis using A by simp
            next
              case False
              hence "(case list of [] ⇒ None | 
                [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
                | x # g' # xs ⇒
                if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
                else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                      then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None) = 
              Some (SOME z. weight (last (x # y # xs)) z ≠ None)"
                using ‹last list ∈ attacker ∧ ¬ deadend (last list)› ‹list = x # y # xs› by auto 
              then show ?thesis by simp 
            qed
          qed

          show "weight (last list)
                (the (case list of [] ⇒ None | [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
                      | x # g' # xs ⇒
                        if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
                        else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                        then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None)) ≠ None"
          proof(cases "length list =1")
            case True
            hence "the (case list of [] ⇒ None | [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
           | x # g' # xs ⇒
               if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
               else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                    then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None) = (SOME y. weight (last list) y ≠ None)" 
              using ‹last list ∈ attacker ∧ ¬ deadend (last list)›
              by (smt (verit) Eps_cong One_nat_def ‹(case list of [] ⇒ None | [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None | x # g' # xs ⇒ if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g' # xs) else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs)) then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None) ≠ None› last_snoc length_0_conv length_Suc_conv_rev list.case_eq_if list.sel(1) list.sel(3) option.sel self_append_conv2) 
            then show ?thesis
              by (smt (verit, del_insts) ‹last list ∈ attacker ∧ ¬ deadend (last list)› some_eq_ex)
          next
            case False
            hence "∃x y xs. list = x # (y # xs)"
              by (metis One_nat_def ‹list ≠ []› length_Cons list.exhaust list.size(3))
            from this obtain x y xs where "list = x # (y # xs)" by auto
            then show ?thesis proof(cases "(x=g ∧ weight x y ≠ None)")
              case True
              hence "(case list of [] ⇒ None | 
                [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
                | x # g' # xs ⇒
                if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
                else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                      then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None) = (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g y e)) y) (y#xs)"
                using ‹list = x # y # xs› list.simps(5) by fastforce

              from all True have "∃s. nonpos_attacker_winning_strategy s (the (apply_w g y e)) y" by auto
              hence "nonpos_attacker_winning_strategy (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g y e)) y) (the (apply_w g y e)) y" 
                using some_eq_ex by metis 
              then show ?thesis
                by (smt (verit) ‹(case list of [] ⇒ None | [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None | x # g' # xs ⇒ if x = g ∧ weight x g' ≠ None then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g' # xs) else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs)) then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None) = (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g y e)) y) (y # xs)› ‹last list ∈ attacker ∧ ¬ deadend (last list)› ‹list = x # y # xs› attacker_nonpos_strategy_def nonpos_attacker_winning_strategy.elims(1) last_ConsR list.distinct(1))
            next
              case False
              hence "(case list of [] ⇒ None | 
                [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
                | x # g' # xs ⇒
                if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
                else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                      then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None) = 
              Some (SOME z. weight (last (x # y # xs)) z ≠ None)"
                using ‹last list ∈ attacker ∧ ¬ deadend (last list)› ‹list = x # y # xs› by auto 
              then show ?thesis
                by (smt (verit, del_insts) ‹last list ∈ attacker ∧ ¬ deadend (last list)› ‹list = x # y # xs› option.sel verit_sko_ex_indirect)
            qed
          qed
        qed
      qed
    qed
  qed


  have winning: "(∀p. (play_consistent_attacker_nonpos (λlist. (case list of [] ⇒ None | 
                [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
                | x # g' # xs ⇒
                if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
                else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                      then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None)) (LCons g p) [] 
                ∧ valid_play (LCons g p)) ⟶ ¬ defender_wins_play e (LCons g p))" 
  proof
    fix p 
    show "(play_consistent_attacker_nonpos (λlist. (case list of [] ⇒ None | 
                [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
                | x # g' # xs ⇒
                if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
                else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                      then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None)) (LCons g p) [] 
                ∧ valid_play (LCons g p)) ⟶ ¬ defender_wins_play e (LCons g p)"
    proof
      assume A: "(play_consistent_attacker_nonpos (λlist. (case list of [] ⇒ None | 
                [x] ⇒ if x ∈ attacker ∧ ¬ deadend x then Some (SOME y. weight x y ≠ None) else None
                | x # g' # xs ⇒
                if (x=g ∧ weight x g' ≠ None) then (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g') (g'#xs)
                else if last (x # g' # xs) ∈ attacker ∧ ¬ deadend (last (x # g' # xs))
                      then Some (SOME y. weight (last (x # g' # xs)) y ≠ None) else None)) (LCons g p) [] 
                ∧ valid_play (LCons g p))"
      show "¬ defender_wins_play e (LCons g p)"

      proof(cases "p = LNil")
        case True
        hence "lfinite (LCons g p)"
          by simp 
        from True have "llength (LCons g p) = enat 1"
          by (simp add: gen_llength_code(1) gen_llength_code(2) llength_code)
        hence "the_enat (llength (LCons g p))-1 = 0" by simp
        hence "energy_level e (LCons g p) (the_enat (llength (LCons g p))-1) = Some e" using energy_level.simps
          by simp 
        thus ?thesis using ‹g ∉ attacker› ‹lfinite (LCons g p)› defender_wins_play_def
          by (simp add: True)
      next
        case False
        hence "weight g (lhd p) ≠ None" using A
          using llist.distinct(1) valid_play.cases by auto

        hence "∃s. (nonpos_attacker_winning_strategy s (the (apply_w g (lhd p) e)) (lhd p)) ∧ play_consistent_attacker_nonpos s p []"
        proof-
          have "∃s. (nonpos_attacker_winning_strategy s (the (apply_w g (lhd p) e)) (lhd p))" using ‹weight g (lhd p) ≠ None› all by simp
          hence a_win: "nonpos_attacker_winning_strategy (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g (lhd p) e)) (lhd p)) (the (apply_w g (lhd p) e)) (lhd p)"
            by (smt (verit, del_insts) list.simps(9) nat.case_distrib nat.disc_eq_case(1) neq_Nil_conv take_Suc take_eq_Nil2 tfl_some verit_sko_forall')
  
          define strat where Strat: "strat ≡ (SOME s. nonpos_attacker_winning_strategy s (the (apply_w g (lhd p) e)) (lhd p))"
          define strategy where Strategy: "strategy ≡ (λlist. (case list of
                          [] ⇒ None |
                          [x] ⇒ (if x ∈ attacker ∧ ¬deadend x then Some (SOME y. weight x y ≠ None) else None) |
                          (x#(g'#xs)) ⇒ (if (x=g ∧ weight x g' ≠ None) then ((SOME s. nonpos_attacker_winning_strategy s (the (apply_w g g' e)) g' ) (g'#xs))
                              else (if (last (x#(g'#xs))) ∈ attacker ∧ ¬deadend (last (x#(g'#xs))) then Some (SOME y. weight (last (x#(g'#xs))) y ≠ None) else None))))"

          hence "play_consistent_attacker_nonpos strategy (LCons g p) []" using A by simp
          hence strategy_cons: "play_consistent_attacker_nonpos strategy (ltl p) [g, lhd p]" using play_consistent_attacker_nonpos.simps
            by (smt (verit) False butlast.simps(2) last_ConsL last_ConsR lhd_LCons list.distinct(1) ltl_simps(2) play_consistent_attacker_nonpos_cons_simp snoc_eq_iff_butlast)

          have tail: "⋀p'. strategy (g#((lhd p)#p')) = strat ((lhd p)#p')" unfolding Strategy Strat 
            by (simp add: ‹weight g (lhd p) ≠ None›)

          define Q where Q: "⋀s P l. Q s P l ≡ play_consistent_attacker_nonpos strategy P (g#l)
                                                  ∧ l ≠ [] ∧ (∀p'. strategy (g#((hd l)#p')) = s ((hd l)#p'))"

          have "play_consistent_attacker_nonpos strat (ltl p) [lhd p]" 
          proof(rule play_consistent_attacker_nonpos_coinduct)
            show "Q strat (ltl p) [lhd p]"
              unfolding Q using tail strategy_cons False play_consistent_attacker_nonpos_cons_simp by auto 

            show "⋀s v l. Q s (LCons v LNil) l ⟹ l = [] ∨ last l ∉ attacker ∨ last l ∈ attacker ∧ the (s l) = v"
            proof-
              fix s v l
              assume "Q s (LCons v LNil) l" 
              have "l≠[] ∧ last l ∈ attacker ⟹ the (s l) = v" 
              proof-
                assume "l≠[] ∧ last l ∈ attacker"
                hence "(∀p'. strategy (g#((hd l)#p')) = s ((hd l)#p'))" using ‹Q s (LCons v LNil) l› Q by simp
                hence "s l = strategy (g#l)"
                  by (metis ‹l ≠ [] ∧ last l ∈ attacker› list.exhaust list.sel(1)) 

                from ‹l≠[] ∧ last l ∈ attacker› have "last (g#l) ∈ attacker" by simp
                from  ‹Q s (LCons v LNil) l› have "the (strategy (g#l)) = v" unfolding Q using play_consistent_attacker_nonpos.simps ‹last (g#l) ∈ attacker›
                  using eq_LConsD list.discI llist.disc(1) by blast
                thus "the (s l) = v" using ‹s l = strategy (g#l)› by simp
              qed
              thus "l = [] ∨ last l ∉ attacker ∨ last l ∈ attacker ∧ the (s l) = v" by auto
            qed


            show "⋀s v Ps l. Q s (LCons v Ps) l ∧ Ps ≠ LNil ⟹ Q s Ps (l @ [v]) ∧ (v ∈ attacker ⟶ lhd Ps = the (s (l @ [v])))"
            proof-
              fix s v Ps l
              assume "Q s (LCons v Ps) l ∧ Ps ≠ LNil"
              hence A: "play_consistent_attacker_nonpos strategy (LCons v Ps) (g#l)
                                                  ∧ l≠ [] ∧ (∀p'. strategy (g#((hd l)#p')) = s ((hd l)#p'))" unfolding Q by simp

              show "Q s Ps (l @ [v]) ∧ (v ∈ attacker ⟶ lhd Ps = the (s (l @ [v])))"
              proof
                show "Q s Ps (l @ [v])"
                  unfolding Q proof
                  show "play_consistent_attacker_nonpos strategy Ps (g # l @ [v])"
                    using A play_consistent_attacker_nonpos.simps
                    by (smt (verit) Cons_eq_appendI lhd_LCons llist.distinct(1) ltl_simps(2)) 
                  have "(∀p'. strategy (g # hd (l @ [v]) # p') = s (hd (l @ [v]) # p'))" using A by simp
                  thus "l @ [v] ≠ [] ∧ (∀p'. strategy (g # hd (l @ [v]) # p') = s (hd (l @ [v]) # p')) " by auto
                qed

                show "(v ∈ attacker ⟶ lhd Ps = the (s (l @ [v])))"
                proof
                  assume "v ∈ attacker"
                  hence "the (strategy (g#(l@[v]))) = lhd Ps" using A play_consistent_attacker_nonpos.simps
                    by (smt (verit) Cons_eq_appendI ‹Q s (LCons v Ps) l ∧ Ps ≠ LNil› lhd_LCons llist.distinct(1) ltl_simps(2)) 

                  have "s (l @ [v]) = strategy (g#(l@[v]))" using A
                    by (metis (no_types, lifting) hd_Cons_tl hd_append2 snoc_eq_iff_butlast) 
                  thus "lhd Ps = the (s (l @ [v]))" using ‹the (strategy (g#(l@[v]))) = lhd Ps› by simp
              qed
            qed
          qed
        qed
        hence "play_consistent_attacker_nonpos strat p []" using play_consistent_attacker_nonpos.simps
          by (smt (verit) False ‹g ∉ attacker› ‹play_consistent_attacker_nonpos strategy (LCons g p) []› append_butlast_last_id butlast.simps(2) last_ConsL last_ConsR lhd_LCons lhd_LCons_ltl list.distinct(1) ltl_simps(2) play_consistent_attacker_nonpos_cons_simp tail)
        thus ?thesis using Strat a_win by blast
        qed

        from this obtain s where S: "(nonpos_attacker_winning_strategy s (the (apply_w g (lhd p) e)) (lhd p)) ∧ play_consistent_attacker_nonpos s p []" by auto
        have "valid_play p" using A
          by (metis llist.distinct(1) ltl_simps(2) valid_play.simps)
        hence "¬defender_wins_play (the (apply_w g (lhd p) e)) p" using S
          by (metis False nonpos_attacker_winning_strategy.elims(2) lhd_LCons llist.collapse(1) not_lnull_conv)
        hence P: "lfinite p ∧ (energy_level (the (apply_w g (lhd p) e)) p (the_enat (llength p)-1)) ≠ None ∧ ¬ ((llast p)∈ attacker ∧ deadend (llast p))"
          using defender_wins_play_def by simp

        hence "∃n. llength p = enat (Suc n)" using False
          by (metis lfinite_llength_enat llength_eq_0 lnull_def old.nat.exhaust zero_enat_def) 
        from this obtain n where "llength p = enat (Suc n)" by auto
        hence "llength (LCons g p) = enat (Suc (Suc n))"
          by (simp add: eSuc_enat) 
        hence "Suc (the_enat (llength p)-1) = (the_enat (llength (LCons g p))-1)" using ‹llength p = enat (Suc n)› by simp

        from ‹weight g (lhd p) ≠ None› have "(apply_w g (lhd p) e)≠ None"
          by (simp add: all)
        hence "energy_level (the (apply_w g (lhd p) e)) p (the_enat (llength p)-1) = energy_level e (LCons g p) (the_enat (llength (LCons g p))-1)"
          using P energy_level_cons ‹Suc (the_enat (llength p)-1) = (the_enat (llength (LCons g p))-1)› A
          by (metis (no_types, lifting) False ‹∃n. llength p = enat (Suc n)› diff_Suc_1 enat_ord_simps(2) lessI llist.collapse(1) the_enat.simps)
        hence "(energy_level e (LCons g p) (the_enat (llength (LCons g p))-1)) ≠ None" 
          using P by simp
        then show ?thesis using P
          by (simp add: False energy_game.defender_wins_play_def llast_LCons lnull_def) 
      qed
    qed
  qed
 
  show "nonpos_winning_budget e g" using nonpos_winning_budget.simps nonpos_attacker_winning_strategy.simps winning valid
    by blast 
qed

lemma winning_budget_ind_implies_nonpos:
  assumes "winning_budget_ind e g"
  shows "nonpos_winning_budget e g" 
proof-
  define f where "f = (λp x1 x2.
            (∃g e. x1 = e ∧
                   x2 = g ∧
                   g ∉ attacker ∧
                   (∀g'. weight g g' ≠ None ⟶
                         apply_w g g' e ≠ None ∧ p (the (apply_w g g' e)) g')) ∨
            (∃g e. x1 = e ∧
                   x2 = g ∧
                   g ∈ attacker ∧
                   (∃g'. weight g g' ≠ None ∧
                         apply_w g g' e ≠ None ∧ p (the (apply_w g g' e)) g')))"

  have "f nonpos_winning_budget = nonpos_winning_budget"
    unfolding f_def 
  proof
    fix e0 
    show "(λx2. (∃g e. e0 = e ∧
                       x2 = g ∧
                       g ∉ attacker ∧
                       (∀g'. weight g g' ≠ None ⟶
                             apply_w g g' e ≠ None ∧
                             nonpos_winning_budget (the (apply_w g g' e)) g')) ∨
                (∃g e. e0 = e ∧
                       x2 = g ∧
                       g ∈ attacker ∧
                       (∃g'. weight g g' ≠ None ∧
                             apply_w g g' e ≠ None ∧
                             nonpos_winning_budget (the (apply_w g g' e)) g'))) =
          nonpos_winning_budget e0"
    proof
      fix g0
      show "((∃g e. e0 = e ∧
                  g0 = g ∧
                  g ∉ attacker ∧
                  (∀g'. weight g g' ≠ None ⟶
                        apply_w g g' e ≠ None ∧
                        nonpos_winning_budget (the (apply_w g g' e)) g')) ∨
           (∃g e. e0 = e ∧
                  g0 = g ∧
                  g ∈ attacker ∧
                  (∃g'. weight g g' ≠ None ∧
                        apply_w g g' e ≠ None ∧
                        nonpos_winning_budget (the (apply_w g g' e)) g'))) =
          nonpos_winning_budget e0 g0"
      proof
        assume " (∃g e. e0 = e ∧
           g0 = g ∧
           g ∉ attacker ∧
           (∀g'. weight g g' ≠ None ⟶
                 apply_w g g' e ≠ None ∧ nonpos_winning_budget (the (apply_w g g' e)) g')) ∨
    (∃g e. e0 = e ∧
           g0 = g ∧
           g ∈ attacker ∧
           (∃g'. weight g g' ≠ None ∧
                 apply_w g g' e ≠ None ∧ nonpos_winning_budget (the (apply_w g g' e)) g'))"
        thus "nonpos_winning_budget e0 g0" using inductive_implies_nonpos_winning_budget
          by blast
      next
        assume "nonpos_winning_budget e0 g0"
        thus " (∃g e. e0 = e ∧
           g0 = g ∧
           g ∉ attacker ∧
           (∀g'. weight g g' ≠ None ⟶
                 apply_w g g' e ≠ None ∧ nonpos_winning_budget (the (apply_w g g' e)) g')) ∨
    (∃g e. e0 = e ∧
           g0 = g ∧
           g ∈ attacker ∧
           (∃g'. weight g g' ≠ None ∧
                 apply_w g g' e ≠ None ∧ nonpos_winning_budget (the (apply_w g g' e)) g'))"
          using nonpos_winning_budget_implies_inductive
          by meson
      qed
    qed
  qed
  hence "lfp f ≤ nonpos_winning_budget " 
    using lfp_lowerbound
    by (metis order_refl)
  hence "winning_budget_ind ≤ nonpos_winning_budget"
    using f_def HOL.nitpick_unfold(211) by simp

  thus ?thesis using assms
    by blast 
qed

text‹Finally, we can state the inductive characterisation of attacker winning budgets assuming energy-positional determinacy.›

lemma inductive_winning_budget:
  assumes "nonpos_winning_budget = winning_budget"
  shows "winning_budget = winning_budget_ind"
proof
  fix e
  show "winning_budget e = winning_budget_ind e"
  proof
    fix g 
    show "winning_budget e g = winning_budget_ind e g"
    proof
      assume "winning_budget e g"
      thus "winning_budget_ind e g"
        using winning_budget_implies_ind winning_budget.simps by auto 
    next
      assume "winning_budget_ind e g"
      hence "nonpos_winning_budget e g"
        using winning_budget_ind_implies_nonpos by simp
      thus "winning_budget e g" using assms by simp
    qed
  qed
qed

end
end