Theory TD_side

section ‹TD side›

theory TD_side
  imports Basics_side Destabilization_side
begin

declare fun_upd_apply[simp del]


subsection ‹Definition of the Solver Algorithm With Parameterized Destabilization Function›

record ('x,'g,'d) state =
  called :: "'x set"
  infl :: "('x + 'g, 'x list) fmap"
  stabl :: "'x set"
  σ :: "'x + 'g ⇒'d"

locale TD_side =
  fixes destab :: "'x + 'g ⇒ ('x + 'g, 'x list) fmap ⇒ 'x set ⇒ 'x set
                   ⇒ ('x + 'g, 'x list) fmap × 'x set"
    and abort :: "bool"
    and T :: "('x,'g,'d::bounded_semilattice_sup_bot) eqsT"
  assumes destab_removes: "(i2,s2) = destab x i1 s1 c1 ⟹ s2 ⊆ s1"
begin

function (domintros)
    query :: "'x ⇒ 'x ⇒ ('x,'g,'d) state ⇒
              'd × ('x,'g,'d) state" and
  iterate :: "'x ⇒ ('x,'g,'d) state ⇒ 'd × ('x,'g,'d) state" and
   repeat :: "'x ⇒ ('x,'g,'d) state ⇒ 'd × ('x,'g,'d) state" and
     eval :: "'x ⇒ ('x,'g,'d) strategy_tree ⇒ ('x,'g,'d) state ⇒ 'd × ('x,'g,'d) state" where
  "query x y state = (
    let (xd, state) =
      if y ∈ (called state) then
        ((σ state) (Inl y), state)
      else
        iterate y (state ⦇called := insert y (called state)⦈)
    in (xd, state⦇infl := fminsert (infl state) (Inl y) x⦈))"
| "iterate x state = (
    if x ∉ (stabl state) then
      let (d_new, state) = repeat x state in
      if (σ state) (Inl x) = d_new then
        (d_new, state⦇called := called state - {x} ⦈)
      else
        let (infl', stabl') = destab (Inl x) (infl state) (stabl state) (called state) in
        iterate x (state ⦇infl := infl', stabl := stabl', σ := (σ state)(Inl x := d_new) ⦈)
    else
      ((σ state) (Inl x), state⦇called := called state - {x} ⦈))"
| "repeat x state = (
    let (d_new, state) = eval x (T x) (state ⦇stabl := insert x (stabl state)⦈) in
    if x ∈ stabl state then (d_new, state)
    else repeat x state)"
| "eval x t state =
    (if ¬ abort ∨ x ∈ stabl state then
    (case t of
      Answer d ⇒ (d, state)
    | QueryL y g ⇒ (
        let (yd, state) = query x y state in eval x (g yd) state)
    | QueryG y g ⇒ (
        let yd = (σ state) (Inr y) in
        eval x (g yd) (state ⦇infl := fminsert (infl state) (Inr y) x⦈))
    | Side y d t ⇒ (
        let d' = (σ state) (Inr y) ⊔ d in
        if (σ state) (Inr y) = d' then eval x t state
        else
          let (infl', stabl') = destab (Inr y) (infl state) (stabl state) (called state) in
          eval x t (state ⦇infl := infl', stabl := stabl', σ := (σ state)(Inr y := d') ⦈)))
    else ((σ state) (Inl x), state))"
  by pat_completeness auto

definition init_state :: "('x,'g,'d) state" where
  "init_state = ⦇ called = {}, infl = fmempty, stabl = {}, σ = (λ_. ⊥) ⦈"

definition solve :: "'x ⇒ 'x set × ('x + 'g ⇒ 'd)" where
  "solve x = (let (d, state) = iterate x (init_state ⦇ called := insert x (called init_state) ⦈) in
  (stabl state, σ state))"

definition query_dom where
  "query_dom y x state = query_iterate_repeat_eval_dom (Inl (Inl (y, x, state)))"
declare query_dom_def [simp]
definition iterate_dom where
  "iterate_dom x state = query_iterate_repeat_eval_dom (Inl (Inr (x, state)))"
declare iterate_dom_def [simp]
definition repeat_dom where
  "repeat_dom x state = query_iterate_repeat_eval_dom (Inr (Inl (x, state)))"
declare repeat_dom_def [simp]
definition eval_dom where
  "eval_dom x t state = query_iterate_repeat_eval_dom (Inr (Inr (x, t, state)))"
declare eval_dom_def [simp]

definition solve_dom where
  "solve_dom x = iterate_dom x (init_state ⦇ called := insert x (called init_state) ⦈)"

lemmas dom_defs = query_dom_def iterate_dom_def repeat_dom_def eval_dom_def


subsection ‹Refinement of auto-generated rules›

text ‹The auto-generated \texttt{pinduct} rule contains a redundant assumption. This lemma removes
this redundant assumption such that the rule is easier to instantiate and gives comprehensible
names to the cases.›

lemmas query_iterate_repeat_eval_pinduct[consumes 1, case_names Query Iterate Repeat Eval]
  = query_iterate_repeat_eval.pinduct(1)[
      folded dom_defs,
      of x y state for x y state
    ]
    query_iterate_repeat_eval.pinduct(2)[
      folded dom_defs,
      of x state for x state
    ]
    query_iterate_repeat_eval.pinduct(3)[
      folded dom_defs,
      of x state for x state
    ]
    query_iterate_repeat_eval.pinduct(4)[
      folded dom_defs,
      of x t state for x t state
    ]

lemmas iterate_pinduct[consumes 1, case_names Iterate]
  = query_iterate_repeat_eval_pinduct(2)[where ?P="λy x state. True"
    and ?R="λx state. True" and ?S="λx t state. True", simplified (no_asm_use),
    folded dom_defs]

declare query.psimps[simp] iterate.psimps[simp] repeat.psimps[simp] eval.psimps[simp]


subsection ‹Domain Lemmas›

lemma dom_backwards_pinduct:
  shows "query_dom x y state
    ⟹ y ∉ called state ⟹ iterate_dom y (state ⦇called := insert y (called state)⦈)"
  and "iterate_dom x state
    ⟹ x ∉ (stabl state) ⟹
         repeat_dom x state
          ∧ ((xd_new1, state1) = repeat x state
          ⟶ (σ state1) (Inl x) ≠ xd_new1
          ⟶ (infl2, stabl2) = destab (Inl x) (infl state1) (stabl state1) (called state1)
          ⟶ iterate_dom x (state1 ⦇infl := infl2, stabl := stabl2,
              σ := (σ state1)(Inl x := xd_new1)⦈))"
  and "repeat_dom x state ⟹
        eval_dom x (T x) (state ⦇stabl := insert x (stabl state)⦈) ∧
        ((d', state') = eval x (T x) (state ⦇stabl := insert x (stabl state)⦈)
        ⟶ x ∉ stabl state' ⟶ repeat_dom x state')"
  and "eval_dom x t state
    ⟹ (¬ abort ∨ x ∈ stabl state ⟶ t = QueryL y g ⟶ query_dom x y state ∧
          ((yd, state') = query x y state ⟶ eval_dom x (g yd) state')) ∧
        (¬ abort ∨ x ∈ stabl state ⟶ t = QueryG z h ⟶ zd = (σ state) (Inr z) ⟶
          eval_dom x (h zd) (state⦇infl := fminsert (infl state) (Inr z) x⦈)) ∧
        (¬ abort ∨ x ∈ stabl state ⟶ t = Side u d t' ⟶ d' = (σ state) (Inr u) ⊔ d ⟶
          (((σ state) (Inr u) = d' ⟶ eval_dom x t' state)
          ∧ ((σ state) (Inr u) ≠ d' ⟶
            (infl1, stabl1) = destab (Inr u) (infl state) (stabl state) (called state) ⟶
            eval_dom x t' (state ⦇infl := infl1, stabl := stabl1,
              σ := (σ state)(Inr u := d')⦈))))"
proof (induction x y state and x state and x state and x t state
    arbitrary: and xd_new1 state1 infl2 stabl2 and d' state'
               and y g yd d z h zd u t' d' state' infl1 stabl1
    rule: query_iterate_repeat_eval_pinduct)
  case (Query y x state)
  show ?case
    apply (rule query_iterate_repeat_eval.domintros(2)[folded dom_defs])
    using Query.IH(2)[OF Query.prems]
    by simp+
next
  case (Iterate x state)
  show ?case
    apply (intro impI conjI)
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(3)[folded dom_defs])
      using Iterate.IH(2)[OF Iterate.prems] by fastforce+
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(2)[folded dom_defs destab.simps])
      using Iterate.IH(3)[OF Iterate.prems, folded dom_defs] by simp+
    done
next
  case (Repeat x state)
  show ?case
    apply (intro impI conjI)
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(4)[folded dom_defs])
      using Repeat.IH(2)[OF Repeat.prems] by (fastforce split: prod.splits)+
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(3)[folded dom_defs])
      using Repeat.IH(3)[OF Repeat.prems] by fastforce+
    done
next
  case (Eval x t state)
  show ?case
    apply (intro impI conjI)
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(1)[folded dom_defs])
      using Eval.IH(2) by simp
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(4)[folded dom_defs])
      using Eval.IH(3) by (fastforce split: prod.splits)+
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(4)[folded dom_defs])
      using Eval.IH(4) by (fastforce split: prod.splits)+
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(4)[folded dom_defs])
      using Eval.IH(5) by (fastforce split: prod.splits)+
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(4)[folded dom_defs])
      using Eval.IH(6) by (fastforce split: prod.splits)+
    done
qed


subsection ‹Case Rules›

lemma iterate_continue_fixpoint_cases[consumes 3]:
  assumes "iterate_dom x state"
    and "(xd, state') = iterate x state"
  obtains (Stable) "state' = state⦇called := called state - {x} ⦈"
    and "(σ state) (Inl x) = xd"
    and "x ∈ stabl state"
  | (Fixpoint) state1
  where "repeat_dom x state"
    and "(xd, state1) = repeat x state"
    and "(σ state1) (Inl x) = xd"
    and "x ∉ stabl state"
    and "state' = state1⦇called := called state1 - {x} ⦈"
  | (Continue) state1 xd_new infl2 stabl2
  where "repeat_dom x state"
    and "(xd_new, state1) = repeat x state"
    and "(σ state1) (Inl x) ≠ xd_new"
    and "(infl2, stabl2) = destab (Inl x) (infl state1) (stabl state1) (called state1)"
    and "iterate_dom x (state1 ⦇infl := infl2, stabl := stabl2, σ := (σ state1)(Inl x := xd_new)⦈)"
    and "(xd, state') = iterate x
          (state1 ⦇infl := infl2, stabl := stabl2, σ := (σ state1)(Inl x := xd_new)⦈)"
    and "x ∉ stabl state"
proof(cases "x ∈ stabl state" rule: case_split[case_names Stable Unstable])
  case Stable
  then show ?thesis using that(1) assms by auto
next
  case Unstable
  have repeat_dom: "repeat_dom x state"
    using dom_backwards_pinduct(2)[OF assms(1) Unstable]
    by simp
  then obtain xd_new state1 where repeat: "(xd_new, state1) = repeat x state"
    by (cases "repeat x state") auto
  show ?thesis
  proof (cases "(σ state1) (Inl x) = xd_new")
    case True
    then have "xd_new = xd" and "state1⦇called := called state1 - {x} ⦈ = state'"
      using assms(1) Unstable repeat assms(2)
      by (cases "repeat x state", simp)+
    then show ?thesis
      using Unstable assms repeat that(2)[OF repeat_dom] True by blast
  next
    case False
    then obtain infl2 stabl2 where destab:
        "(infl2, stabl2) = destab (Inl x) (infl state1) (stabl state1) (called state1)"
      by (cases "destab (Inl x) (infl state1) (stabl state1) (called state1)") simp
    then have iterate_dom: "iterate_dom x (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new)⦈)"
      using Unstable False repeat assms(1-2) dom_backwards_pinduct(2)
      by simp
    have iterate: "(xd, state') = iterate x (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new)⦈)"
      using iterate.psimps[folded dom_defs, OF assms(1)] Unstable repeat False
        destab assms(2) by (auto split: prod.split)
    show ?thesis
      using that(3)[OF repeat_dom repeat False destab iterate_dom iterate
          Unstable]
      by simp
  qed
qed

lemma repeat_unstable_stable_cases [consumes 2]:
  assumes "repeat_dom x state"
    and "(d', state') = repeat x state"
  obtains (Unstable) state1 d1
  where "eval_dom x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
    and "(d1, state1) = eval x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
    and "x ∉ stabl state1"
    and "repeat_dom x state1"
    and "(d', state') = repeat x state1"
  | (Stable) "eval_dom x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
    and "(d', state') = eval x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
    and "x ∈ stabl state'"
proof -
  have eval_dom: "eval_dom x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
    using dom_backwards_pinduct(3)[OF assms(1)] by simp
  obtain d1 state1 where eval:
    "(d1, state1) = eval x (T x) (state ⦇stabl := insert x (stabl state)⦈)"
    by (cases "eval x (T x) (state ⦇stabl := insert x (stabl state)⦈)") auto
  show ?thesis
  proof (cases "x ∈ stabl state1" rule: case_split[case_names Stable Unstable])
    case Stable
    show ?thesis
      apply (rule that(2)[OF eval_dom])
      using Stable eval assms(2) repeat.psimps[folded dom_defs, OF assms(1)]
      by (cases "eval x (T x) (state⦇stabl := insert x (stabl state)⦈)", simp)+
  next
    case Unstable
    show ?thesis
      apply (rule that(1)[OF eval_dom eval])
      subgoal using Unstable by simp
      subgoal using dom_backwards_pinduct(3)[OF assms(1)] eval Unstable by simp
      subgoal
        using repeat.psimps[folded dom_defs, OF assms(1)] eval Unstable assms(2)
        by (cases "eval x (T x) (state⦇stabl := insert x (stabl state)⦈)") simp
      done
  qed
qed

lemma query_iterate_lookup_cases_basic [consumes 2]:
  assumes "query_dom y x state"
    and "(xd, state') = query y x state"
  obtains (Iterate) state1
  where "iterate_dom x (state⦇called := insert x (called state) ⦈)"
    and "(xd, state1) = iterate x (state⦇called := insert x (called state) ⦈)"
    and "state' = state1 ⦇infl := fminsert (infl state1) (Inl x) y⦈"
    and "x ∉ called state"
  | (Lookup) "(σ state) (Inl x) = xd"
    and "state' = state ⦇infl := fminsert (infl state) (Inl x) y⦈"
    and "x ∈ called state"
proof (cases "x ∈ called state")
  case True
  show ?thesis using assms True by (auto intro: that(2))
next
  case False
  obtain xd1 state1 where iterate: "(xd1, state1) = iterate x (state⦇called := insert x (called state)⦈)"
    by (cases "iterate x (state⦇called := insert x (called state)⦈)") simp
  then have "xd1 = xd"
    using assms False by (auto split: prod.splits)
  show ?thesis
    apply (rule that(1)[of state1])
    using dom_backwards_pinduct(1)[OF assms(1) False] assms(1,2) iterate False ‹xd1 = xd›
    by (simp split: if_splits prod.splits)+
qed

lemma eval_query_answer_cases_basic [consumes 2]:
  assumes "eval_dom x t state"
    and "(xd, state') = eval x t state"
  obtains (QueryL) y g yd state1
  where "¬ abort ∨ x ∈ stabl state"
    and "t = QueryL y g"
    and "query_dom x y state"
    and "(yd, state1) = query x y state"
    and "eval_dom x (g yd) state1"
    and "(xd, state') = eval x (g yd) state1"
  | (QueryG) y g yd
  where "¬ abort ∨ x ∈ stabl state"
    and "t = QueryG y g"
    and "yd = (σ state) (Inr y)"
    and "eval_dom x (g yd) (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
    and "(xd, state') = eval x (g yd) (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
  | (Side_Subsumed) y yd d' t1
  where "¬ abort ∨ x ∈ stabl state"
    and "t = Side y yd t1"
    and "d' = (σ state) (Inr y) ⊔ yd"
    and "(σ state) (Inr y) = d'"
    and "eval_dom x t1 state"
    and "(xd, state') = eval x t1 state"
  | (Side_Effect) y yd d' t1 infl1 stabl1
  where "¬ abort ∨ x ∈ stabl state"
    and "t = Side y yd t1"
    and "d' = (σ state) (Inr y) ⊔ yd"
    and "(σ state) (Inr y) ≠ d'"
    and "(infl1, stabl1) = destab (Inr y) (infl state) (stabl state) (called state)"
    and "eval_dom x t1 (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
    and "(xd, state') =
          eval x t1 (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
  | (Answer) "¬ abort ∨ x ∈ stabl state"
    and "t = Answer xd"
    and "state' = state"
  | (Abort) "abort ∧ x ∉ stabl state"
    and "xd = (σ state) (Inl x)"
    and "state' = state"
proof (cases "¬ abort ∨ x ∈ stabl state")
  assume Stabl : "¬ abort ∨ x ∈ stabl state"
  then show ?thesis
  proof (cases t)
    case (Answer d)
    then show ?thesis using that eval.psimps[folded dom_defs, OF assms(1)] assms(2) Stabl by auto
  next
    case (QueryL y g)
    obtain yd1 state1 where query_y: "(yd1, state1) = query x y state"
      by (cases "query x y state", simp)
    have query_y_dom: "query_dom x y state"
      using dom_backwards_pinduct(4)[OF assms(1), THEN conjunct1, folded
            atomize_imp, OF _ QueryL, of yd1 state1] Abort Stabl by simp
    have "(xd, state') = eval x (g yd1) state1"
      using eval.psimps[folded dom_defs, OF assms(1)] QueryL query_y assms(2) Stabl
      by (auto split: prod.splits)
    then show ?thesis
      using that(1) QueryL query_y_dom query_y dom_backwards_pinduct(4) assms Stabl by fast
  next
    case (QueryG y g)
    obtain yd1 where query_y: "yd1 = (σ state) (Inr y)" by simp
    have "(xd, state') = eval x (g yd1) (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using eval.psimps[folded dom_defs, OF assms(1)] QueryG query_y assms(2) Stabl
      by (auto split: prod.splits)
    then show ?thesis
      using QueryG query_y dom_backwards_pinduct(4)[OF assms(1)] that(2) Stabl
      by (auto intro: that(2))
  next
    case (Side y d t)
    define d' where "d' = (σ state) (Inr y) ⊔ d"
    show ?thesis
    proof (cases "(σ state) (Inr y) = d'")
      case True
      then have eval: "(xd, state') = eval x t state"
        using eval.psimps[folded dom_defs, OF assms(1)] Side d'_def assms(2) Stabl
        by (auto simp add: Let_def split: prod.splits)
      then show ?thesis
        using True Side d'_def dom_backwards_pinduct(4)[OF assms(1)] Stabl
        by (auto intro: that(3)[OF _ Side d'_def]
            simp add: Side_Subsumed TD_side.eval_dom_def TD_side_axioms eval)
    next
      case False
      obtain infl1 stabl1 where
        destab: "(infl1, stabl1) = destab (Inr y) (infl state) (stabl state) (called state)"
        by (cases "destab (Inr y) (infl state) (stabl state) (called state)") simp
      then have eval: "(xd, state') =
          eval x t (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
        using eval.psimps[folded dom_defs, OF assms(1)] Side d'_def assms(2) False Stabl
        by (auto simp add: Let_def split: prod.splits)
      then show ?thesis
        using False destab Side d'_def dom_backwards_pinduct(4)[OF assms(1)] Stabl
        by (auto intro: that(4)[OF Stabl Side d'_def]
            simp add: Side_Subsumed TD_side.eval_dom_def TD_side_axioms eval)
    qed
  qed
next
  case False
  then show ?thesis using that eval.psimps[folded dom_defs, OF assms(1)] assms(2) by force
qed


lemma c_same:
  shows
    "query_dom x y state ⟹ (xd, state') = query x y state ⟹ called state' = called state"
    "iterate_dom x state ⟹ (xd, state') = iterate x state ⟹ called state' = called state - {x}"
    "repeat_dom x state ⟹ (xd, state') = repeat x state ⟹ called state' = called state"
    "eval_dom x t state ⟹ (xd, state') = eval x t state ⟹ called state' = called state"
proof (induction x y state and x state and x state and x t state
       arbitrary: xd state' and xd state' and xd state' and xd state'
       rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state)
  show ?case using Query(1,3)
  proof (cases rule: query_iterate_lookup_cases_basic)
    case (Iterate state1)
    then show ?thesis using Query(2)[of xd state1] by simp
  next
    case Lookup
    then show ?thesis by fastforce
  qed
next
  case (Iterate x state)
  show ?case using Iterate(1,4)
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis by simp
  next
    case Fixpoint
    then show ?thesis using Iterate.IH(2) by simp
  next
    case (Continue state1 xd_new infl⇩L2 stabl2)
    then show ?thesis
      using Iterate.IH(2)[OF Continue(7,2)]
        Iterate.IH(3)[OF Continue(7,2) _ _ Continue(4) _ Continue(6)]
      by simp
  qed
next
  case (Repeat x state)
  show ?case using Repeat(1,4)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    show ?thesis
      using Repeat.IH(2)[OF Unstable(2)] Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5)] by simp
  next
    case Stable
    then show ?thesis using Repeat.IH(2)[OF Stable(2)] by simp
  qed
next
  case (Eval x t state)
  show ?case using Eval(1,7)
  proof (cases rule: eval_query_answer_cases_basic)
    case (QueryL y g yd state1)
    show ?thesis
      using Eval.IH(2)[OF QueryL(1,2,4)] Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6)] by simp
  next
    case (QueryG y g yd)
    then show ?thesis using Eval.IH(4)[OF QueryG(1,2,3,5)] by simp
  next
    case (Side_Subsumed y yd d' t1)
    then show ?thesis
      using Eval.IH(5)[OF Side_Subsumed(1,2,3) _ Side_Subsumed(6)] Side_Subsumed(4)
      by (simp split: if_splits prod.splits)
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    then show ?thesis
      using Eval.IH(6)[OF Side_Effect(1,2,3) _ _ _ Side_Effect(7)]
      by (cases "destab (Inr y) (infl state) (stabl state) (called state)") auto
  qed fast+
qed

lemma iterate_fmlookup:
  assumes "iterate_dom x state"
    and "(xd, state') = iterate x state"
  shows "(σ state') (Inl x) = xd"
  using assms
proof(induction x state rule: iterate_pinduct)
  case (Iterate x state)
  show ?case
    using Iterate.hyps Iterate.prems
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis by simp
  next
    case Fixpoint
    then show ?thesis by simp
  next
    case (Continue state1 xd_new infl⇩L2 stabl2)
    then show ?thesis
      using Iterate.IH(1) c_same(3)[OF Continue(1,2)] Iterate(3) by fastforce
  qed
qed

corollary query_fmlookup:
  assumes "query_dom y x state"
    and "(xd, state') = query y x state"
  shows "(σ state') (Inl x) = xd"
  using assms iterate_fmlookup[OF dom_backwards_pinduct(1)[OF assms(1)]]
  by (auto split: prod.splits if_splits)

lemma eval_query_answer_cases [consumes 2]:
  assumes "eval_dom x t state"
    and "(xd, state') = eval x t state"
  obtains (QueryL) y g yd state1
  where "¬ abort ∨ x ∈ stabl state"
    and "t = QueryL y g"
    and "query_dom x y state"
    and "(yd, state1) = query x y state"
    and "eval_dom x (g yd) state1"
    and "(xd, state') = eval x (g yd) state1"
    and "(σ state1) (Inl y) = yd"
  | (QueryG) y g yd
  where "¬ abort ∨ x ∈ stabl state"
    and "t = QueryG y g"
    and "yd = (σ state) (Inr y)"
    and "eval_dom x (g yd) (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
    and "(xd, state') = eval x (g yd) (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
  | (Side_Subsumed) y yd d' t1
  where "¬ abort ∨ x ∈ stabl state"
    and "t = Side y yd t1"
    and "d' = (σ state) (Inr y) ⊔ yd"
    and "(σ state) (Inr y) = d'"
    and "eval_dom x t1 state"
    and "(xd, state') = eval x t1 state"
  | (Side_Effect) y yd d' t1 infl1 stabl1
  where "¬ abort ∨ x ∈ stabl state"
    and "t = Side y yd t1"
    and "d' = (σ state) (Inr y) ⊔ yd"
    and "(σ state) (Inr y) ≠ d'"
    and "(infl1, stabl1) = destab (Inr y) (infl state) (stabl state) (called state)"
    and "eval_dom x t1 (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
    and "(xd, state') =
          eval x t1 (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
  | (Answer) "¬ abort ∨ x ∈ stabl state"
    and "t = Answer xd"
    and "state' = state"
  | (Abort) "abort ∧ x ∉ stabl state"
    and "xd = (σ state) (Inl x)"
    and "state' = state"
  apply (rule eval_query_answer_cases_basic[OF assms])
  apply (simp add: query_fmlookup[of x _ state])
  by metis+

lemma query_iterate_lookup_cases [consumes 2]:
  assumes "query_dom y x state"
    and "(xd, state') = query y x state"
  obtains (Iterate) state1
  where "iterate_dom x (state⦇called := insert x (called state) ⦈)"
    and "(xd, state1) = iterate x (state⦇called := insert x (called state) ⦈)"
    and "state' = state1 ⦇infl := fminsert (infl state1) (Inl x) y⦈"
    and "(σ state') (Inl x) = xd"
    and "x ∉ called state"
  | (Lookup) "(σ state) (Inl x) = xd"
    and "state' = state ⦇infl := fminsert (infl state) (Inl x) y⦈"
    and "x ∈ called state"
  apply (rule query_iterate_lookup_cases_basic[OF assms])
  using iterate_fmlookup[of x "state⦇called := insert x (called state)⦈"]
  by (simp_all split: if_splits del: dom_defs)


subsection ‹Basic Properties of the Solver State›

lemma called_value_unchanged:
  shows "query_dom x y state
    ⟹ (xd, state') = query x y state
    ⟹ ∀x ∈ called state. (σ state) (Inl x) = (σ state') (Inl x)"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ ∀x ∈ called state - {x}. (σ state) (Inl x) = (σ state') (Inl x)"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ ∀x ∈ called state. (σ state) (Inl x) = (σ state') (Inl x)"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ ∀x ∈ called state. (σ state) (Inl x) = (σ state') (Inl x)"
proof(induction x y state and x state and x state and y t state
    arbitrary: xd state' and xd state' and xd state' and xd state'
    rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state)
  show ?case using Query(1,3)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    note IH = Query.IH(2)[OF Iterate(5,2)]
    then show ?thesis using Iterate(3) c_same(2)[OF Iterate(1,2), simplified] Iterate(5) by auto
  next
    case Lookup
    then show ?thesis by simp
  qed
next
  case (Iterate x state)
  show ?case using Iterate(1,4)
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Iterate(4) by auto
  next
    case (Fixpoint state1)
    note IH = Iterate.IH(2)[OF Fixpoint(4,2)]
    then show ?thesis
      using Iterate(4) Fixpoint(5) by (simp add: image_Int Diff_eq flip: restrict_restrict)
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = Iterate.IH(2)[OF Continue(7,2)]
    have c_same: "called state1 = called state" using c_same(3)[OF Continue(1,2)] by simp
    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6), simplified]
    then show ?thesis
      using Iterate(4) IH by (simp add: c_same fun_upd_other)
  qed
next
  case (Repeat x state)
  show ?case using Repeat(1,4)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2)]
    have c_same: "called state1 = called state" using c_same(4)[OF Unstable(1,2)] by simp
    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5), of d1, simplified]
    then show ?thesis using IH by (simp add: c_same)
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2)]
    then show ?thesis by simp
  qed
next
  case (Eval x t state)
  show ?case using Eval(1,7)
  proof (cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,2,4)]
    have c_same: "called state1 = called state" using c_same(1)[OF QueryL(3,4)] by simp
    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6), simplified]
    then show ?thesis using IH by (simp add: c_same)
  next
    case (QueryG y g yd)
    note IH = Eval.IH(4)[OF QueryG(1-3,5)]
    then show ?thesis by simp
  next
    case (Side_Subsumed y yd d' t1)
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6)]
    then show ?thesis by auto
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7), simplified]
    then show ?thesis by (simp add: c_same fun_upd_other)
  qed fast+
qed

lemma increasing_values_for_globals:
  shows "query_dom x y state
    ⟹ (xd, state') = query x y state
    ⟹ ∀u. (σ state) (Inr u) ≤ (σ state') (Inr u)"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ ∀u. (σ state) (Inr u) ≤ (σ state') (Inr u)"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ ∀u. (σ state) (Inr u) ≤ (σ state') (Inr u)"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ ∀u. (σ state) (Inr u) ≤ (σ state') (Inr u)"
proof(induction x y state and x state and x state and y t state
    arbitrary: xd state' and xd state' and xd state' and xd state'
    rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state)
  show ?case using Query(1,3)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    note IH = Query.IH(2)[OF Iterate(5,2)]
    then show ?thesis using Iterate(3) by simp
  next
    case Lookup
    then show ?thesis by simp
  qed
next
  case (Iterate x state)
  show ?case using Iterate(1,4)
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Iterate(4) by auto
  next
    case (Fixpoint state1)
    note IH = Iterate.IH(2)[OF Fixpoint(4,2)]
    then show ?thesis using Fixpoint(5) by simp
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = Iterate.IH(2)[OF Continue(7,2)]
    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6), simplified]
    have "((σ state1)(Inl x := xd_new)) (Inr u) = (σ state1) (Inr u)" for u
      by (simp add: fun_upd_other)
    then show ?thesis using IH ih order.trans by fastforce
  qed
next
  case (Repeat x state)
  show ?case using Repeat(1,4)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2)]
    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5), of d1, simplified]
    then show ?thesis using IH order.trans by fastforce
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2)]
    then show ?thesis by simp
  qed
next
  case (Eval x t state)
  show ?case using Eval(1,7)
  proof (cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,2,4)]
    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6), simplified]
    then show ?thesis using IH order.trans by fastforce
  next
    case (QueryG y g yd)
    note IH = Eval.IH(4)[OF QueryG(1-3,5)]
    then show ?thesis by simp
  next
    case (Side_Subsumed y yd d' t1)
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6)]
    then show ?thesis by auto
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7), simplified]
    have "(σ state) (Inr u) ≤ ((σ state)(Inr y := d')) (Inr u)" for u
      apply (cases "u = y")
      subgoal using Side_Effect(3) by (simp add: fun_upd_same)
      subgoal by (simp add: fun_upd_other)
      done
    then show ?thesis using IH order.trans by fastforce
  qed fast+
qed

lemma called_non_stabl_increasing:
  shows "query_dom x y state
    ⟹ (xd, state') = query x y state
    ⟹ called state - stabl state ⊆ called state' - stabl state'"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ (called state - {x}) - stabl state ⊆ (called state' - {x}) - stabl state'"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ (called state - {x}) - stabl state ⊆ (called state' - {x}) - stabl state'"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ called state - stabl state ⊆ called state' - stabl state'"
proof(induction x y state and x state and x state and y t state
    arbitrary: xd state' and xd state' and xd state' and xd state'
    rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state)
  show ?case using Query(1,3)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    note IH = Query.IH(2)[OF Iterate(5,2)]
    then show ?thesis using Iterate(3) c_same(2)[OF Iterate(1,2), simplified] Iterate(5) by auto
  next
    case Lookup
    then show ?thesis by simp
  qed
next
  case (Iterate x state)
  show ?case using Iterate(1,4)
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Iterate(4) by auto
  next
    case (Fixpoint state1)
    note IH = Iterate.IH(2)[OF Fixpoint(4,2)]
    then show ?thesis using Iterate(4) Fixpoint(5) by simp
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = Iterate.IH(2)[OF Continue(7,2)]
    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6), simplified]
    then show ?thesis using IH destab_removes[OF Continue(4)] by blast
  qed
next
  case (Repeat x state)
  show ?case using Repeat(1,4)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2)]
    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5), of d1, simplified]
    then show ?thesis using IH by auto
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2)]
    then show ?thesis using Stable(3) by auto
  qed
next
  case (Eval x t state)
  show ?case using Eval(1,7)
  proof (cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,2,4)]
    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6), simplified]
    then show ?thesis using IH by auto
  next
    case (QueryG y g yd)
    note IH = Eval.IH(4)[OF QueryG(1-3,5)]
    then show ?thesis by simp
  next
    case (Side_Subsumed y yd d' t1)
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6)]
    then show ?thesis by auto
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7), simplified]
    then show ?thesis using destab_removes[OF Side_Effect(5)] by blast
  qed fast+
qed


subsection ‹Predicate for Well-formed Stable Set and Infl Map›

definition well_infl_stabl where
  "well_infl_stabl state ≡
    (∀y∈(stabl state) - (called state). ∀x ∈ dep T (σ state) y. y ∈ slookup (infl state) x)
    ∧ {u. slookup (infl state) (Inl u) ≠ {}} ⊆ stabl state ∪ called state"

abbreviation "update_rel state state' ≡
  let no_indirect_side = {u. ∃x ∈ called state ∩ stabl state'. x ∈ slookup (infl state) u} in
  (∀u ∈ no_indirect_side. slookup (infl state) u ⊆ slookup (infl state') u)
  ∧ {u. Inl u ∈ no_indirect_side} ∩ stabl state ⊆ stabl state'
  ∧ (∀u ∈ no_indirect_side. (σ state) u = (σ state') u)"
(* A sufficient weaker version for property (2) for TD_unopt is:
   {u. Inl u ∈ no_indirect_side} ∩ stabl state ⊆ stabl state' ∪ called state'
   This corresponds to the predicate used for TD_opt.
*)

abbreviation "update_rel_opt state state' ≡
  let no_indirect_side = {u. ∃x ∈ called state ∩ stabl state'. x ∈ slookup (infl state) u} in
  (∀u ∈ no_indirect_side. slookup (infl state) u ⊆ slookup (infl state') u)
  ∧ {u. Inl u ∈ no_indirect_side} ∩ stabl state ⊆ stabl state' ∪ called state'
  ∧ (∀u ∈ no_indirect_side. (σ state) u = (σ state') u)"
(* Property (2) needs to be relaxed for TD_opt compared to update_rel.
   The predicate update_rel as is does not hold for TD_opt.
   This weaker version also holds for TD_unopt and is sufficient to prove it correct *)

lemma well_infl_stabl_implies_stabl_c_closed:
  assumes "well_infl_stabl state"
  shows "∀y∈(stabl state) - (called state). dep⇩L T (σ state) y ⊆ stabl state ∪ called state"
proof (intro ballI subsetI, goal_cases)
  case (1 y x)
  then have "y ∈ slookup (infl state) (Inl x)"
    using assms(1) unfolding well_infl_stabl_def dep⇩L_def by blast
  then have "slookup (infl state) (Inl x) ≠ {}" by auto
  then show ?case using assms(1) unfolding well_infl_stabl_def by blast
qed

lemma well_infl_stabl_simp_c_stabl:
  assumes "x ∈ called state"
    and "well_infl_stabl state"
  shows "well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
proof -
  have "stabl state ∪ (called state - {x}) ⊆ insert x (stabl state ∪ called state)" by auto
  moreover have "insert x (stabl state) - called state ⊆ stabl state - (called state - {x})"
    using assms(1) by auto
  ultimately show ?thesis
    using assms(2)
    unfolding well_infl_stabl_def
    by fastforce
qed

lemma well_infl_stabl_simp_add_to_c:
  assumes "well_infl_stabl (state⦇ called := (called state) - {x} ⦈)"
  shows "well_infl_stabl state"
  using assms
  unfolding well_infl_stabl_def
  by auto

end ―‹end of locale TD_side defining the solver›


subsection ‹Correctness of Unoptimized TDside with Full Destabilization›

locale TD_side_unopt =
  fixes abort :: "bool"
    and T :: "('x,'g,'d::bounded_semilattice_sup_bot) eqsT"
begin

sublocale TD_side "λx i s called. destab x i s"
  unfolding TD_side_def
  using destab_infl_stabl_relation
  by blast

subsubsection ‹Well-formedness of Stable Set and Infl Map›

paragraph ‹Preservation of the Well-formedness of Stabl and Infl when Destabilizing›

lemma destab_x_no_dep:
  assumes "stabl2 = (stabl state1) - influenced_by (infl state1) (Inl x)"
    and "∀y∈(stabl state1) - (called state1 - {x}). ∀z∈dep T (σ state1) y. y ∈ slookup (infl state1) z"
  shows "∀y ∈ stabl2 - (called state1 - {x}). Inl x ∉ dep T (σ state1) y"
proof (intro ballI, goal_cases)
  case (1 y)
  show ?case
  proof (rule ccontr, goal_cases)
    case 1
    then have "y ∈ slookup (infl state1) (Inl x)"
      using assms ‹y ∈ stabl2 - (called state1 - {x})› by blast
    then have "y ∈ influenced_by (infl state1) (Inl x)"
      using lookup_in_influenced by force
    moreover have "y ∉ influenced_by (infl state1) (Inl x)"
      using assms(1) ‹y ∈ stabl2 - (called state1 - {x})› by fastforce
    ultimately show ?case by auto
  qed
qed

lemma destab_and_upd_preserves_dep_closed_in_infl:
  assumes "(infl2, stabl2) = destab (Inl x) (infl state1) (stabl state1)"
    and "(∀y∈stabl state1 - (called state1 - {x}). ∀z∈dep T (σ state1) y. y ∈ slookup (infl state1) z)"
  shows "(∀y∈stabl2 - (called state1 - {x}). ∀z∈dep T ((σ state1)(Inl x := xd')) y.
            y ∈ slookup infl2 z)"
proof (intro ballI, goal_cases)
  case (1 z y)
  have infl2_def:
      "infl2 = fmdrop_set (Inl ` insert x (influenced_by (infl state1) (Inl x))) (infl state1)"
    and stabl2_def: "stabl2 = (stabl state1) - influenced_by (infl state1) (Inl x)"
    using destab_infl_stabl_relation[OF assms(1)]
    by simp+

  have "y ∈ dep T (σ state1) z"
  proof (goal_cases)
    case 1
    have "∀y∈stabl2 - (called state1 - {x}). Inl x ∉ dep T (σ state1) y"
      using assms(2) stabl2_def destab_x_no_dep by blast
    then have "Inl x ∉ dep T (σ state1) z"
        using ‹z ∈ stabl2 - (called state1 - {x})› by blast
      then have "dep T ((σ state1)(Inl x := xd')) z = dep T (σ state1) z"
        apply (intro dep_eq[of T "σ state1", symmetric])
        apply (intro ballI)
        subgoal for y
          apply (cases "y = Inl x")
          by (auto simp add: fun_upd_same fun_upd_other)
        done
    then show ?case using ‹y ∈ dep T ((σ state1)(Inl x := xd')) z› by auto
  qed
  then have z_in_infl1_y: "z ∈ slookup (infl state1) y"
    using 1(1) stabl2_def assms(2) by fastforce

  have "z ∈ influenced_by (infl state1) y"
    using lookup_in_influenced[of "infl state1" y] z_in_infl1_y
    by auto
  then have "y ∉ Inl ` influenced_by (infl state1) (Inl x)" and "y ≠ Inl x"
    using stabl2_def 1(1) influenced_by_transitive by fast+
  then show ?case
    using z_in_infl1_y fmlookup_drop_set infl2_def
    unfolding fmlookup_default_def
    by fastforce
qed

text‹The following lemmas show that the well-formedness of infl and stabl are preserved when
  destabilizing and unknown and updating its value in @{term σ}.›

lemma destab_upd_locale_preserves_well_infl_stabl:
  assumes "(infl2, stabl2) = destab (Inl x) (infl state1) (stabl state1)"
      and "well_infl_stabl (state1⦇called := called state1 - {x}⦈)"
    shows "well_infl_stabl (state1⦇infl := infl2, stabl := stabl2,
            σ := (σ state1)(Inl x := d_new), called := called state1 - {x} ⦈)"
proof -
  show ?thesis
    using assms(2)
    unfolding well_infl_stabl_def
  proof (intro conjI subsetI, goal_cases)
    case 1
    then show ?case
      using destab_and_upd_preserves_dep_closed_in_infl[OF assms(1)]
      by simp

    case (2 u)
    then show ?case
      apply simp
      by (auto simp add: destab_infl_stabl_relation[OF assms(1)] fmlookup_default_drop_set
        simp flip: fmdrop_set_insert split: if_splits)
  qed
qed

lemma destab_upd_globale_preserves_well_infl_stabl:
  assumes destab: "(infl1, stabl1) = destab (Inr y) (infl state) (stabl state)"
      and "well_infl_stabl state"
    shows "well_infl_stabl (state⦇infl := infl1, stabl := stabl1,
            σ := (σ state)(Inr y := d') ⦈)"
  using assms(2) unfolding well_infl_stabl_def
  apply (simp add: destab_infl_stabl_relation[OF destab])
  apply (intro conjI)
  subgoal
  proof (intro ballI, goal_cases 2)
    case (2 u v)
    have "v ∈ dep T (σ state) u"
    proof -
      have "u ∉ influenced_by (infl state) (Inr y)" using 2(2) by simp
      then have "Inr y ∉ dep T (σ state) u" using 2(1,2) lookup_in_influenced by fastforce
      then show ?thesis
        using 2(3)
        apply (subst dep_eq[of _ _ _ "(σ state)(Inr y := d')"])
        by (metis fun_upd_other)
    qed
    then have "u ∈ slookup (infl state) v" using 2(1,2) by blast
    then show ?case
      using 2(2) influenced_by_transitive[of _ _ "Inr y" u]
        lookup_in_influenced[of "infl state" v] ‹u ∈ slookup (infl state) v›
      by (auto simp add: fmlookup_default_drop_set simp flip: fmdrop_set_insert)
  qed
  subgoal
  proof -
    have "{u. slookup (infl state) (Inl u) ≠ {}} ⊆ stabl state ∪ called state"
      using assms(2) unfolding well_infl_stabl_def by simp
    then show ?thesis
    by (auto simp add: destab_infl_stabl_relation[OF assms(1)] fmlookup_default_drop_set
        simp flip: fmdrop_set_insert)
  qed
  done


paragraph ‹Helper Lemmas to Deduced Update Predicate›

lemma influencing_stabl_after_destab':
  assumes "(infl2, stabl2) = destab y infl1 stabl1"
    "z ∈ slookup infl1 u" "z ∈ stabl2"
  shows "z ∈ slookup infl2 u"
proof (rule ccontr, goal_cases)
  case 1
  then have "z ∉ slookup (fmdrop_set (insert y (Inl ` influenced_by infl1 y)) infl1) u"
    using destab_infl_stabl_relation[OF assms(1)] by blast
  then consider "u = y" | "u ∈ Inl ` influenced_by infl1 y"
    using assms(2)
    unfolding fmlookup_default_def
    by (auto split: if_splits)
  then have "z ∈ influenced_by infl1 y"
    using assms(2)
    apply cases
    subgoal using lookup_in_influenced by fast
    subgoal using lookup_in_influenced influenced_by_transitive[of _ infl1 y z] by fast
    done
  then have "z ∉ stabl2" using destab_infl_stabl_relation[OF assms(1)] by blast
  then show ?case using assms(3) by simp
qed

lemma update_rel_transitive:
  assumes update_rel: "update_rel state1 state2" "update_rel state2 state3"
    and indicator_u_dec: "called state3 ∩ stabl state3 ⊆ called state2 ∩ stabl state2"
    and called_same: "called state1 = called state2" "called state2 = called state3"
  shows "update_rel state1 state3"
proof -
  let ?no_indirect_side1 = "{u. ∃x∈called state1 ∩ stabl state2. x ∈ slookup (infl state1) u}"
  let ?no_indirect_side2 = "{u. ∃x∈called state2 ∩ stabl state3. x ∈ slookup (infl state2) u}"
  let ?no_indirect_side3 = "{u. ∃x∈called state1 ∩ stabl state3. x ∈ slookup (infl state1) u}"
  have unaffected_subset: "?no_indirect_side3 ⊆ ?no_indirect_side1"
      "?no_indirect_side3 ⊆ ?no_indirect_side2"
    using update_rel(1) indicator_u_dec called_same
    by fastforce+

  show ?thesis
    apply simp
    apply (intro conjI)
    subgoal
      using unaffected_subset conjunct1[OF update_rel(1)[simplified]]
        conjunct1[OF update_rel(2)[simplified]]
      by blast
    subgoal
      using unaffected_subset conjunct1[OF conjunct2[OF update_rel(1)[simplified]]]
        conjunct1[OF conjunct2[OF update_rel(2)[simplified]]]
      by blast
    subgoal
      using unaffected_subset conjunct2[OF conjunct2[OF update_rel(1)[simplified]]]
        conjunct2[OF conjunct2[OF update_rel(2)[simplified]]]
      by fastforce
    done
qed


paragraph ‹Induction Proof›

lemma well_infl_stabl_ind:
  shows "query_dom x y state
    ⟹ (xd, state') = query x y state
    ⟹ well_infl_stabl state
    ⟹ well_infl_stabl state'
      ∧ x ∈ slookup (infl state') (Inl y)
      ∧ update_rel state state'"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ well_infl_stabl (state'⦇called := called state' - {x}⦈)
      ∧ x ∈ stabl state'
      ∧ update_rel (state⦇called := called state - {x}⦈) (state'⦇called := called state' - {x}⦈)"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl state
    ⟹ well_infl_stabl (state'⦇called := called state' - {x}⦈)
      ∧ x ∈ stabl state'
      ∧ update_rel (state⦇called := called state - {x}⦈) (state'⦇called := called state' - {x}⦈)"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ well_infl_stabl state
    ⟹ x ∈ called state
    ⟹ x ∈ stabl state ⟶ (subt_for_prefix (T x) pre (σ state) = Some t
        ∧ (∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p))
    ⟹ well_infl_stabl state'
      ∧ (x ∈ stabl state' ⟶ (∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y))
      ∧ update_rel state state'"
proof(induction x y state and x state and x state and y t state
    arbitrary: xd state' and xd state' and xd state' and pre xd state'
    rule: query_iterate_repeat_eval_pinduct)
  case (Query y x state)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    note IH = Query.IH(2)[simplified, OF Iterate(5,2) Query.prems(2)]
    then show ?thesis
      using Iterate(3,4) unfolding well_infl_stabl_def
      by (auto simp add: slookup_fminsert split: if_splits)
  next
    case Lookup
    show ?thesis
      using Query.prems(2) Lookup(3)
      unfolding well_infl_stabl_def
      by (auto simp add: Lookup(2) slookup_fminsert)
  qed
next
  case (Iterate x state)
  have inv: "well_infl_stabl state"
    using well_infl_stabl_simp_add_to_c[OF Iterate.prems(3)] by simp
  note IH' = Iterate.IH(2)[rotated 2, OF Iterate.prems(2) inv]

  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    show ?thesis using Stable(2,3) Iterate.prems(3) by (simp add: Stable(1))
  next
    case (Fixpoint state1)
    note IH = IH'[OF Fixpoint(4,2), folded dep_def]
    then show ?thesis
      unfolding well_infl_stabl_def
      by (auto simp add: Fixpoint(5))
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = IH'[OF Continue(7,2)]

    have c_state1_same_state: "called state1 = called state"
      using c_same(3)[OF Continue(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Iterate.prems(2) by simp

    have inv: "well_infl_stabl (state1⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
      apply (rule destab_upd_locale_preserves_well_infl_stabl[OF Continue(4)])
      using IH
      by auto

    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6), simplified,
              OF x_in_c1 inv]

    have "called state' = called state1 - {x}" using c_same(2)[OF Continue(5,6)] x_in_c1 by simp

    with IH show ?thesis
    proof(elim conjE, intro conjI, goal_cases)
      case 1
      show ?case using ih by blast
    next
      case 2
      show ?case using ih by blast
    next
      case 3
      have upd_rel_destab:
        "update_rel (state1⦇called := called state1 - {x}⦈) (state1⦇infl := infl2, stabl := stabl2,
          σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
        using destab_infl_stabl_relation[OF Continue(4)]
          influencing_stabl_after_destab'[OF Continue(4)]
        by (auto simp add: fmlookup_default_drop_set fun_upd_other simp del: fmdrop_set_insert
            split: if_split)
      have upd_rel_begin_destab:
        "update_rel (state⦇called := called state - {x}⦈) (state1⦇infl := infl2, stabl := stabl2,
          σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
        apply (intro update_rel_transitive[OF 3(4) upd_rel_destab])
        using called_non_stabl_increasing(3)[OF Continue(1,2)] ‹called state1 = called state›
          destab_infl_stabl_relation[OF Continue(4)]
        by auto
      show ?case
        apply (intro update_rel_transitive[OF upd_rel_begin_destab])
        using ih called_non_stabl_increasing(2)[OF Continue(5,6)] ‹called state' = called state1 - {x}›
          c_state1_same_state
        by auto
    qed
  qed
next
  case (Repeat x state)
  have inv: "well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: well_infl_stabl_simp_c_stabl)
  have prefix: "x ∈ stabl (state⦇stabl := insert x (stabl state)⦈) ⟶ (
      subt_for_prefix (T x) [] (σ (state⦇stabl := insert x (stabl state)⦈)) = Some (T x)
      ∧ (∀p ∈ {p. Inl p ∈ set []}. x ∈ slookup (infl (state⦇stabl := insert x (stabl state)⦈)) p))"
    by simp+

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2) inv _ prefix, simplified, OF Repeat.prems(2)]

    have "called state1 = called state"
      using c_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have inv1: "well_infl_stabl state1"
      using IH by simp

    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5) x_in_c1 inv1, of d1, simplified]

    have "called state' = called state1" using c_same(3)[OF Unstable(4,5)] by simp

    show ?thesis
      apply (intro conjI)
      subgoal using ih by simp
      subgoal using ih by simp
      subgoal
        apply (rule update_rel_transitive[of _ "state1⦇called := called state1 - {x} ⦈"])
        subgoal using IH Unstable(3) by auto
        subgoal using ih Unstable(3) by simp
        subgoal using called_non_stabl_increasing(3)[OF Unstable(4,5)] ‹called state' = called state1› by auto
        subgoal using ‹called state1 = called state› by simp
        subgoal using ‹called state' = called state1› by simp
        done
      done
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2) inv _ prefix, simplified, OF Repeat.prems(2)]
    show ?thesis
      unfolding well_infl_stabl_def
      apply (intro conjI)
      subgoal
        apply (rule ballI)
        using IH Stable(3)
        unfolding well_infl_stabl_def dep_def
        by auto
      subgoal using IH Stable(3) unfolding well_infl_stabl_def by auto
      subgoal
        using Stable(3) by blast
      subgoal
        apply simp
        using Stable(3) IH by blast
      done
  qed
next
  case (Eval x t state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,2,4) Eval.prems(2)]

    have "called state1 = called state" using c_same(1)[OF QueryL(3,4)] by simp
    then have "x ∈ called state1" using Eval.prems(3) by simp
    have "called state' = called state1" using c_same(4)[OF QueryL(5,6)] by simp

    have prefix_no_indirect_side: "{p. Inl p ∈ set pre}
        ⊆ {u. ∃x ∈ called state ∩ stabl state1. x ∈ slookup (infl state) u}"
        if "x ∈ stabl state1"
      using that called_non_stabl_increasing(1)[OF QueryL(3,4)] ‹x ∈ called state1› Eval.prems(3,4) IH
      by fastforce

    have prefix: "x ∈ stabl state1 ⟶
      (subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state1) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inl y)])}. x ∈ slookup (infl state1) p))"
    proof (intro impI, goal_cases)
      case 1
      then have "x ∈ stabl state"
        using called_non_stabl_increasing(1)[OF QueryL(3,4)] Eval.prems(3) by blast
      show ?case using Eval.prems(4)[rule_format, OF ‹x ∈ stabl state›]
      proof (intro conjI impI, goal_cases)
        case 1
        then show ?case
          apply (intro subt_for_prefix_transitive[where ?t2.0=t])
          subgoal
            apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
            subgoal using prefix_no_indirect_side ‹x ∈ stabl state1› IH by fastforce
            subgoal by simp
            done
          subgoal using QueryL(2,7) by simp
          done
      next
        case 2
        then show ?case
          using conjunct2[OF IH] prefix_no_indirect_side[OF 1] by fastforce
      qed
    qed

    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6) conjunct1[OF IH] ‹x ∈ called state1› prefix,
        simplified]

    have y_unaffected:
      "Inl y ∈ {u. ∃x ∈ called state1 ∩ stabl state'. x ∈ slookup (infl state1) u}"
        if "x ∈ stabl state'"
      using lookup_in_influenced that called_non_stabl_increasing(4)[OF QueryL(5,6)]
        prefix c_same(4)[OF QueryL(5,6)] ‹x ∈ called state1›
      by fastforce
    have y_value_unchanged: "(σ state') (Inl y) = yd" if "x ∈ stabl state'"
      using y_unaffected[OF that] ih QueryL(7) by fastforce
    have y_infl_incr: "slookup (infl state1) (Inl y) ⊆ slookup (infl state') (Inl y)"
      if "x ∈ stabl state'"
      using y_unaffected[OF that] ih by auto

    show ?thesis
      apply (intro conjI)
      subgoal using ih by simp
      subgoal using ih IH y_infl_incr by (auto simp add: QueryL(2) y_value_unchanged)
      subgoal
        apply (rule update_rel_transitive[of _ state1])
        using IH ih called_non_stabl_increasing(4)[OF QueryL(5,6)] ‹called state' = called state1›
          ‹called state1 = called state›
        by auto
      done
  next
    case (QueryG y g yd)
    have inv: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def by auto
    have prefix: "x ∈ stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈) ⟶ (
        subt_for_prefix (T x) (pre @ [Inl (Inr y)])
        (σ (state⦇infl := fminsert (infl state) (Inr y) x⦈)) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inr y)])}. x ∈ slookup
        (infl (state⦇infl := fminsert (infl state) (Inr y) x⦈)) p))"
      using Eval.prems(4) QueryG(2,3) subt_for_prefix_transitive[of "T x" pre _ t "[Inl (Inr y)]"]
      by (simp add: fminsert_def fmlookup_default_def)
    note IH = Eval.IH(4)[OF QueryG(1-3,5) inv _ prefix, simplified, OF Eval.prems(3)]

    have y_unaffected: "Inr y ∈ {u. ∃z ∈ called state ∩ stabl state'.
        z ∈ slookup (fminsert (infl state) (Inr y) x) u}"
        if "x ∈ stabl state'"
      using lookup_in_influenced that called_non_stabl_increasing(4)[OF QueryG(4,5)]
        c_same(4)[OF QueryG(4,5)] ‹x ∈ called state›
      by (auto simp add: slookup_fminsert_same)
    have y_value_unchanged: "(σ state') (Inr y) = yd" if "x ∈ stabl state'"
      using y_unaffected IH QueryG(3) that by fastforce
    have y_infl_incr: "slookup (infl (state⦇infl := fminsert (infl state) (Inr y) x⦈)) (Inr y)
        ⊆ slookup (infl state') (Inr y)" if "x ∈ stabl state'"
      using y_unaffected IH that by fastforce

    show ?thesis
      apply (intro conjI)
      subgoal using IH by simp
      subgoal
        using IH y_infl_incr by (auto simp add: QueryG(2) y_value_unchanged slookup_fminsert_same)
      subgoal using IH by (auto simp add: slookup_fminsert split: if_splits)
      done
  next
    case (Side_Subsumed y yd d' t1)
    have prefix: "x ∈ stabl state ⟶
      (subt_for_prefix (T x) (pre @ [Inr (y, yd)]) (σ state) = Some t1
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inr (y, yd)])}. x ∈ slookup (infl state) p))"
      using Eval.prems(4) subt_for_prefix_transitive[of "T x" pre _ t "[Inr (y, yd)]" t1]
        Side_Subsumed(2)
      by simp
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6) Eval.prems(2,3) prefix]

    have "x ∈ stabl state' ⟶ (∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y)"
      using IH
      by (simp add: Side_Subsumed(2) dep_aux⇩L_def)

    then show ?thesis using IH by simp
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    have inv:
        "well_infl_stabl (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
      using destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5) Eval.prems(2)]
      by simp
    have x_stabl_if_stabl1: "x ∈ stabl state" if "x ∈ stabl1"
      using destab_infl_stabl_relation[OF Side_Effect(5)] that by simp

    have prefix_recorded_in_infl:
      "∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p" if "x ∈ stabl state"
      using Eval.prems(4) that by simp

    have y_not_in_prefix: "Inl (Inr y) ∉ set pre" if "x ∈ stabl1"
    proof (rule ccontr, goal_cases)
      case 1
      then have "x ∈ slookup (infl state) (Inr y)"
        using prefix_recorded_in_infl that x_stabl_if_stabl1 by simp
      then have "x ∈ influenced_by (infl state) (Inr y)"
        using lookup_in_influenced by fastforce
      then show ?case using destab_infl_stabl_relation[OF Side_Effect(5)] that by simp
    qed

    have prefix: "x ∈ stabl (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)
      ⟶ (subt_for_prefix (T x) (pre @ [Inr (y, yd)]) (σ (state
        ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)) = Some t1
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inr (y, yd)])}. x ∈ slookup
        (infl (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)) p))"
      apply simp
    proof
      assume A: "x ∈ stabl1"
      have P: "subt_for_prefix (T x) pre ((σ state)(Inr y := d')) = Some t"
        apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
        subgoal using y_not_in_prefix A by (simp add: fun_upd_apply)
        subgoal using Eval.prems(4) x_stabl_if_stabl1 A by simp
        done
      show "subt_for_prefix (T x) (pre @ [Inr (y, yd)]) ((σ state)(Inr y := d')) = Some t1 ∧
        (∀p. Inl p ∈ set pre ⟶ x ∈ slookup infl1 p)"
        apply (intro conjI)
        apply (subst subt_for_prefix_transitive[OF P(1), of "[Inr (y, yd)]" t1])
        subgoal using Side_Effect(2) by simp
        subgoal by simp
        subgoal using destab_infl_stabl_relation[OF Side_Effect(5)]
          by (smt (z3) A Diff_iff influenced_by_transitive
              lookup_in_influenced fmlookup_default_drop_set
              image_iff insert_iff mem_Collect_eq prefix_recorded_in_infl
              subset_iff)
        done
    qed

    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7) inv _ prefix, simplified,
        OF Eval.prems(3)]

    have upd_rel_destab:
      "update_rel state (state⦇infl := infl1, stabl := stabl1,
        σ := (σ state)(Inr y := d')⦈)"
      using destab_infl_stabl_relation[OF Side_Effect(5)] Side_Effect(5)
        influencing_stabl_after_destab'[OF Side_Effect(5)]
      by (auto simp add: fmlookup_default_drop_set fun_upd_other simp del: fmdrop_set_insert
          split: if_split)

    have "called state' = called state"
      using c_same(4)[OF Side_Effect(6,7)] by simp

    have "x ∈ stabl state' ⟶ (∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y)"
      using IH by (simp add: Side_Effect(2) dep_aux⇩L_def)

    then show ?thesis
      apply (intro conjI)
      subgoal using IH by simp
      subgoal using IH by simp
      subgoal
        apply (rule update_rel_transitive[OF upd_rel_destab])
        subgoal using IH by auto
        subgoal
          using called_non_stabl_increasing(4)[OF Side_Effect(6,7)] ‹called state' = called state› by auto
        subgoal by simp
        subgoal using ‹called state' = called state› by simp
        done
      done
  next
    case Answer
    have "∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y"
      by (simp add: Answer(2) dep_aux_def)
    moreover have "dep_aux⇩L (σ state) t ⊆ stabl state ∪ called state"
      by (simp add: Answer(2) dep_aux⇩L_def)
    ultimately show ?thesis using Eval.prems(2) Answer(3) by simp
  next
    case Abort
    then show ?thesis using Eval.prems(2) by fastforce
  qed
qed

corollary solve_returns_stabl_closed_under_dep:
  assumes "solve_dom x"
    and "solve x = (st, sigma)"
  shows "∀x∈st. dep⇩L T sigma x ⊆ st"
proof -
  obtain xd state' where
      iterate: "(xd, state') = iterate x (init_state⦇ called := insert x (called init_state) ⦈)"
      and "st = stabl state'" and "sigma = σ state'"
    using assms unfolding solve_dom_def solve_def
    by (cases "iterate x (init_state⦇called := insert x (called init_state)⦈)") auto
  then have "well_infl_stabl (state'⦇called := called state' - {x}⦈)"
    using well_infl_stabl_ind(2)[OF assms(1)[unfolded solve_dom_def]]
    unfolding well_infl_stabl_def init_state_def fmlookup_default_def
    by auto
  show ?thesis
    using well_infl_stabl_implies_stabl_c_closed[OF ‹well_infl_stabl (state'⦇called := called state' - {x}⦈)›]
      ‹st = stabl state'› ‹sigma = σ state'› c_same(2)[OF assms(1)[unfolded solve_dom_def] iterate]
    unfolding well_infl_stabl_def init_state_def
    by simp
qed

subsubsection ‹Partial Correctness›

paragraph ‹Preservation of the Partial Solution when Destabilizing›

lemma destab_upd_locale_preserves_part_solution:
  assumes destab: "(infl2, stabl2) = destab (Inl x) (infl state1) (stabl state1)"
      and IH: "eq_equal_sides_subsumed T (σ state1) (stabl state1 - called state1)"
          "eq T x (σ state1) = xd_new"
          "sides_of_rhs (T x) (σ state1) ≤ σ state1"
      and x_in_c1: "x ∈ called state1"
      and well_infl_stabl_1: "well_infl_stabl (state1⦇called := called state1 - {x}⦈)"
    shows "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - (called state1 - {x}))"
proof -
  have "eq_equal_sides_subsumed T (σ state1) (stabl state1 - called state1)"
    using IH by simp
  have "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - called state1)"
  proof (intro ballI, goal_cases)
    case (1 y)
    then have "y ∈ stabl state1 - called state1" "x ≠ y"
      using destab_infl_stabl_relation[OF destab] x_in_c1 by auto
    then have "eq T y (σ state1) = (σ state1) (Inl y)"
      "sides_of_rhs (T y) (σ state1) ≤ σ state1"
      using IH by simp+
    have "Inl x ∉ dep T (σ state1) y"
    proof (rule ccontr, goal_cases)
      case 1
      then have "Inl x ∈ dep T (σ state1) y" by simp
      then have "y ∈ slookup (infl state1) (Inl x)"
        using well_infl_stabl_1 ‹y ∈ stabl state1 - called state1›
        unfolding well_infl_stabl_def
        by simp
      then have "y ∈ influenced_by (infl state1) (Inl x)"
        using lookup_in_influenced by fast
      then have "y ∉ stabl2" using destab_infl_stabl_relation[OF destab] by simp
      then show ?case using ‹y ∈ stabl2 - called state1› by simp
    qed
    then have "eq T y (σ state1) = eq T y ((σ state1)(Inl x := xd_new))"
      using eq_mupd_no_dep
      unfolding dep_def by fast
    moreover have "(σ state1) (Inl y) = ((σ state1)(Inl x := xd_new)) (Inl y)"
      using ‹x ≠ y› by (simp add: fun_upd_other)
    moreover have "sides_of_rhs (T y) ((σ state1)(Inl x := xd_new)) ≤ (σ state1)(Inl x := xd_new)"
      apply (rule subsumes_se_eq[of "σ state1"])
      subgoal
      proof -
        have "Inl x ∉ dep_aux (σ state1) (T y)"
          using ‹Inl x ∉ dep T (σ state1) y› unfolding dep_aux_def dep_def by simp
        then show ?thesis by (metis fun_upd_other)
      qed
      subgoal
        by (simp add: fun_upd_other)
      subgoal
        using IH ‹y ∈ stabl state1 - called state1› by blast
      done
    ultimately show ?case
      using ‹eq T y (σ state1) = (σ state1) (Inl y)› by simp
  qed
  moreover have "eq T x ((σ state1)(Inl x := xd_new)) = xd_new"
    "sides_of_rhs (T x) ((σ state1)(Inl x := xd_new)) ≤ (σ state1)(Inl x := xd_new)"
    if "x ∈ stabl2"
  proof -
    have "x ∈ stabl state1"
      using that destab_infl_stabl_relation[OF destab] by simp
    have "x ∉ influenced_by (infl state1) (Inl x)"
      using that destab_infl_stabl_relation[OF destab] by simp
    then have "x ∉ slookup (infl state1) (Inl x)"
      using lookup_in_influenced by fast
    then have "Inl x ∉ dep T (σ state1) x"
      using conjunct1[OF well_infl_stabl_1[unfolded well_infl_stabl_def]]
        ‹x ∈ stabl state1›
      by auto
    then show "eq T x ((σ state1)(Inl x := xd_new)) = xd_new"
      using eq_mupd_no_dep IH by fastforce
    show "sides_of_rhs (T x) ((σ state1)(Inl x := xd_new)) ≤ (σ state1)(Inl x := xd_new)"
      apply (rule subsumes_se_eq[of "σ state1"])
      subgoal
      proof -
        have "Inl x ∉ dep_aux (σ state1) (T x)"
          using ‹Inl x ∉ dep T (σ state1) x› unfolding dep_aux_def dep_def by simp
        then show ?thesis
          using ‹Inl x ∉ dep T (σ state1) x›
          by (metis fun_upd_other)
      qed
      subgoal
        by (simp add: fun_upd_other)
      subgoal
        using IH by blast
      done
  qed
  ultimately show ?thesis by (auto simp add: fun_upd_same)
qed

lemma destab_upd_globale_preserves_part_solution:
  assumes destab: "(infl1, stabl1) = destab (Inr y) (infl state) (stabl state)"
      and part_sol: "eq_equal_sides_subsumed T (σ state) (stabl state - called state)"
      and well_infl_stabl: "well_infl_stabl state"
      and d_join: "d' = (σ state) (Inr y) ⊔ d"
    shows "eq_equal_sides_subsumed T ((σ state)(Inr y := d')) (stabl1 - called state)"
proof (intro ballI, goal_cases)
  case (1 x)
  then have "x ∈ stabl state - called state"
    using destab_infl_stabl_relation[OF destab] by auto
  then have "eq T x (σ state) = (σ state) (Inl x)" "sides_of_rhs (T x) (σ state) ≤ σ state"
    using part_sol by simp+
  have "Inr y ∉ dep T (σ state) x"
  proof (rule ccontr, goal_cases)
    case 1
    then have "Inr y ∈ dep T (σ state) x" by simp
    then have "x ∈ slookup (infl state) (Inr y)"
      using well_infl_stabl ‹x ∈ stabl state - called state›
      unfolding well_infl_stabl_def by simp
    then have "x ∈ influenced_by (infl state) (Inr y)"
      using lookup_in_influenced by fast
    then have "x ∉ stabl1" using destab_infl_stabl_relation[OF destab] by simp
    then show ?case using ‹x ∈ stabl1 - called state› by simp
  qed
  then have "eq T x (σ state) = eq T x ((σ state)(Inr y := d'))"
    using eq_mupd_no_dep
    unfolding dep_def by fast
  moreover have "(σ state) (Inl x) = ((σ state)(Inr y := d')) (Inl x)"
    by (simp add: fun_upd_other)
  moreover have "sides_of_rhs (T x) ((σ state)(Inr y := d')) ≤ (σ state)(Inr y := d')"
    apply (rule subsumes_se_eq[of "σ state"])
    subgoal
    proof -
      have "Inr y ∉ dep_aux (σ state) (T x)"
        using ‹Inr y ∉ dep T (σ state) x› unfolding dep_aux_def dep_def by simp
      then show ?thesis
        using ‹Inr y ∉ dep T (σ state) x›
        by (metis fun_upd_other)
    qed
    subgoal
    proof
      fix u
      show "(σ state) (Inr u) ≤ ((σ state)(Inr y := d')) (Inr u)"
        apply (cases "u = y")
        subgoal using d_join by (simp add: fun_upd_same)
        subgoal by (simp add: fun_upd_other)
        done
    qed
    subgoal
      using part_sol ‹x ∈ stabl state - called state› by blast
    done
  ultimately show ?case
    using ‹eq T x (σ state) = (σ state) (Inl x)› by simp
qed

paragraph ‹Induction Proof›

lemma eq_equal_sides_subsumed_ind:
  shows "query_dom x y state
    ⟹ (xd, state') = query x y state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ eq_equal_sides_subsumed T (σ state') (stabl state' - called state')"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {x}))
    ⟹ eq_equal_sides_subsumed T (σ state') (stabl state' - (called state' - {x}))"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ eq_equal_sides_subsumed T (σ state') (stabl state' - called state')
        ∧ eq T x (σ state') = xd
        ∧ sides_of_rhs (T x) (σ state') ≤ σ state'"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ x ∈ called state
    ⟹ x ∈ stabl state ⟶ (subt_for_prefix (T x) pre (σ state) = Some t
        ∧ (∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p)
        ∧ (∀(u, ud) ∈ {s. Inr s ∈ set pre}. ud ≤ (σ state) (Inr u)))
    ⟹ eq_equal_sides_subsumed T (σ state') (stabl state' - called state')
        ∧ (x ∈ stabl state' ⟶ eq T x (σ state') = xd
                                ∧ sides_of_rhs (T x) (σ state') ≤ σ state')"
proof(induction x y state and x state and x state and y t state
    arbitrary: xd state' and xd state' and xd state' and pre xd state'
    rule: query_iterate_repeat_eval_pinduct)
  case (Query y x state)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    note IH = Query.IH(2)[simplified, OF Iterate(5,2) Query.prems(2,3)]
    then show ?thesis by (simp add: Iterate(3))
  next
    case Lookup
    show ?thesis using Query.prems(3) by (simp add: Lookup(2))
  qed
next
  case (Iterate x state)
  have inv: "well_infl_stabl state"
    using well_infl_stabl_simp_add_to_c[OF Iterate.prems(3)] by simp
  have eq_equal_sides_subsumed: "eq_equal_sides_subsumed T (σ state) (stabl state - called state)"
    using Iterate.prems(4) by simp
  note IH' = Iterate.IH(2)[rotated 2, OF Iterate.prems(2) inv eq_equal_sides_subsumed]

  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    show ?thesis using Stable(2,3) Iterate.prems(4) by (simp add: Stable(1))
  next
    case (Fixpoint state1)
    note IH = IH'[OF Fixpoint(4,2), folded dep_def]

    then show ?thesis by (auto simp add: Fixpoint(3,5))
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = IH'[OF Continue(7,2)]
    note well_infl_stabl_1 = well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) inv]

    have c_state1_same_state: "called state1 = called state" using c_same(3)[OF Continue(1,2)] by simp
    then have x_in_c1: "x ∈ called state1" using Iterate.prems(2) by simp

    have inv: "well_infl_stabl (state1⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
      apply (rule destab_upd_locale_preserves_well_infl_stabl[OF Continue(4)])
      using conjunct1[OF well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) inv]]
      unfolding well_infl_stabl_def
      by auto
    have eq_equal_sides_subsumed_2:
        "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - (called state1 - {x}))"
      apply (rule destab_upd_locale_preserves_part_solution[OF Continue(4)])
      using IH well_infl_stabl_1 x_in_c1 by simp+

    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6), simplified,
              OF x_in_c1 inv eq_equal_sides_subsumed_2]

    then show ?thesis by simp
  qed
next
  case (Repeat x state)
  have inv: "well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: well_infl_stabl_simp_c_stabl)
  have eq_equal_sides_subsumed:
      "eq_equal_sides_subsumed T (σ (state⦇stabl := insert x (stabl state)⦈))
      (stabl (state⦇stabl := insert x (stabl state)⦈) - called (state⦇stabl := insert x (stabl state)⦈))"
    using Repeat.prems(2,4) by simp

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2) inv eq_equal_sides_subsumed, of "[]", simplified,
        OF Repeat.prems(2)]

    have "called state1 = called state"
      using c_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have inv1: "well_infl_stabl state1"
      using well_infl_stabl_ind(4)[OF Unstable(1,2) inv, of "[]", simplified, OF Repeat.prems(2)]
      by simp

    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5) x_in_c1 inv1 conjunct1[OF IH],
        of d1, simplified]

    then show ?thesis by simp
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2) inv eq_equal_sides_subsumed, of "[]", simplified,
        OF Repeat.prems(2)]
    then show ?thesis using Stable(3) by simp
  qed
next
  case (Eval x t state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,2,4) Eval.prems(2,3)]
    note well_infl_stabl_1 = well_infl_stabl_ind(1)[OF QueryL(3,4) Eval.prems(2)]

    have prefix_no_indirect_side: "{p. Inl p ∈ set pre}
          ⊆ {u. ∃x ∈ called state ∩ stabl state1. x ∈ slookup (infl state) u}"
        if "x ∈ stabl state1"
      using lookup_in_influenced that called_non_stabl_increasing(1)[OF QueryL(3,4)] Eval.prems(4,5)
      by fastforce

    have prefix: "x ∈ stabl state1 ⟶
      (subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state1) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inl y)])}. x ∈ slookup (infl state1) p)
      ∧ (∀(u,ud) ∈ {s. Inr s ∈ set (pre @ [Inl (Inl y)])}. ud ≤ (σ state1) (Inr u)))"
    proof (intro impI, goal_cases)
      case 1
      then have "x ∈ stabl state"
        using called_non_stabl_increasing(1)[OF QueryL(3,4)] Eval.prems(4) by blast
      show ?case using Eval.prems(5)[rule_format, OF ‹x ∈ stabl state›]
      proof (intro conjI impI, goal_cases)
        case 1
        then show ?case
          apply (intro subt_for_prefix_transitive[where ?t2.0=t])
          subgoal
            apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
            subgoal using prefix_no_indirect_side ‹x ∈ stabl state1› well_infl_stabl_1 by fastforce
            subgoal by simp
            done
          subgoal using QueryL(2,7) by simp
          done
      next
        case 2
        then show ?case
          using conjunct2[OF well_infl_stabl_1] prefix_no_indirect_side[OF 1] by fastforce
      next
        case 3
        then show ?case
          using conjunct2[OF well_infl_stabl_1] prefix_no_indirect_side[OF 1]
            increasing_values_for_globals(1)[OF QueryL(3,4)]
          by (auto intro: order.trans[of _ "σ state a" "σ state1 a" for a])
      qed
    qed

    have "called state1 = called state" using c_same(1)[OF QueryL(3,4)] by simp
    then have "x ∈ called state1" using Eval.prems(4) by simp
    have "called state' = called state1" using c_same(4)[OF QueryL(5,6)] by simp

    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6) conjunct1[OF well_infl_stabl_1] IH
        ‹x ∈ called state1› prefix, simplified]

    then show ?thesis using ih by simp
  next
    case (QueryG y g yd)
    have inv: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    have prefix: "x ∈ stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈) ⟶ (
        subt_for_prefix (T x) (pre @ [Inl (Inr y)])
        (σ (state⦇infl := fminsert (infl state) (Inr y) x⦈)) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inr y)])}. x ∈ slookup
        (infl (state⦇infl := fminsert (infl state) (Inr y) x⦈)) p)
      ∧ (∀(u, ud) ∈ {s. Inr s ∈ set (pre @ [Inl (Inr y)])}.
        ud ≤ (σ (state⦇infl := fminsert (infl state) (Inr y) x⦈)) (Inr u)))"
      using Eval.prems(5) QueryG(2,3) subt_for_prefix_transitive[of "T x" pre _ t "[Inl (Inr y)]"]
      by (simp add: fminsert_def fmlookup_default_def)

    note IH = Eval.IH(4)[OF QueryG(1-3,5) inv _ _ prefix, simplified, OF Eval.prems(3,4)]

    then show ?thesis using IH by simp
  next
    case (Side_Subsumed y yd d' t1)
    have "yd ≤ (σ state) (Inr y)"
      using Side_Subsumed(3,4) sup_ge2[of yd d'] by simp
    then have prefix: "x ∈ stabl state ⟶
      (subt_for_prefix (T x) (pre @ [Inr (y, yd)]) (σ state) = Some t1
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inr (y, yd)])}. x ∈ slookup (infl state) p)
      ∧ (∀(u, ud) ∈ {s. Inr s ∈ set (pre @ [Inr (y, yd)])}. ud ≤ (σ state) (Inr u)))"
      using Eval.prems(5) subt_for_prefix_transitive[of "T x" pre _ t "[Inr (y, yd)]" t1]
        Side_Subsumed(2)
      by simp

    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6) Eval.prems(2-4) prefix]

    show ?thesis using IH by simp
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    have inv:
        "well_infl_stabl (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
      using destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5) Eval.prems(2)] by simp
    have x_stabl_if_stabl1: "x ∈ stabl state" if "x ∈ stabl1"
      using destab_infl_stabl_relation[OF Side_Effect(5)] that by simp

    have prefix_recorded_in_infl:
      "∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p" if "x ∈ stabl state"
      using Eval.prems(5) that by simp

    have y_not_in_prefix: "Inl (Inr y) ∉ set pre" if "x ∈ stabl1"
    proof (rule ccontr, goal_cases)
      case 1
      then have "x ∈ slookup (infl state) (Inr y)"
        using prefix_recorded_in_infl that x_stabl_if_stabl1 by simp
      then have "x ∈ influenced_by (infl state) (Inr y)"
        using lookup_in_influenced by fastforce
      then show ?case using destab_infl_stabl_relation[OF Side_Effect(5)] that by simp
    qed

    have prefix: "x ∈ stabl1 ⟶
      subt_for_prefix (T x) (pre @ [Inr (y, yd)]) ((σ state)(Inr y := d')) = Some t1 ∧
      (∀p. Inl p ∈ set (pre @ [Inr (y, yd)]) ⟶ x ∈ slookup infl1 p) ∧
      (∀a b. Inr (a, b) ∈ set (pre @ [Inr (y, yd)]) ⟶ b ≤ ((σ state)(Inr y := d')) (Inr a))"
    proof (intro impI, goal_cases)
      case 1
      then have "x ∈ stabl state" using x_stabl_if_stabl1 by simp
      show ?case using Eval.prems(5)[rule_format, OF ‹x ∈ stabl state›]
      proof (intro conjI impI allI, goal_cases)
        case 1
        then show ?case
          apply (intro subt_for_prefix_transitive[where ?t2.0=t])
          subgoal
            apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
            by (auto simp add: ‹x ∈ stabl1› fun_upd_def y_not_in_prefix)
          subgoal using Side_Effect(2) by simp
          done
      next
        case (2 p)
        then show ?case using influencing_stabl_after_destab'[OF Side_Effect(5) _ 1] by simp
      next
        case (3 a b)
        then show ?case
          by (auto intro: order.trans[OF _ sup_ge1] simp add: Side_Effect(3) fun_upd_def)
      qed
    qed

    have eq_equal_sides_subsumed_1:
      "eq_equal_sides_subsumed T ((σ state)(Inr y := d')) (stabl1 - called state)"
      using destab_upd_globale_preserves_part_solution[OF Side_Effect(5) Eval.prems(3,2)
          Side_Effect(3)]
      by simp

    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7) inv, simplified,
        OF eq_equal_sides_subsumed_1 Eval.prems(4) prefix]

    then show ?thesis by simp
  next
    case Answer
    have "eq T x (σ state') = xd" if "x ∈ stabl state'"
    proof -
      have "subt_for_prefix (T x) pre (σ state) = Some t"
        using Eval.prems(5) Answer(3) that by simp
      then have "eq T x (σ state) = xd"
        using subt_for_prefix_Answer_eq_traverse Answer(2) by blast
      then show ?thesis using Answer(3) by simp
    qed
    moreover have "sides_of_rhs (T x) (σ state') ≤ σ state'" if "x ∈ stabl state'"
    proof -
      have "subt_for_prefix (T x) pre (σ state) = Some (Answer xd)"
        using Eval.prems(5) Answer that by simp
      then show ?thesis using subt_for_prefix_Answer_subsumes Eval.prems(5) that Answer(3) by blast
    qed
    ultimately show ?thesis using Eval.prems(3) Answer(3) by simp
  next
    case Abort
    then show ?thesis using Eval.prems(3) by force
  qed
qed

theorem partial_solution:
  assumes "solve_dom x"
      and "solve x = (st, sigma)"
    shows "part_solution T x sigma st"
proof -
  obtain d state where
    iterate: "(d, state) = iterate x (init_state ⦇ called := insert x (called init_state) ⦈)"
    and st: "st = stabl state" and sigma: "sigma = σ state"
    using assms(2) unfolding solve_def by (auto split: prod.splits)
  have c_empty: "called state = {}"
    using c_same(2)[OF assms(1)[unfolded solve_dom_def] iterate]
    unfolding init_state_def
    by simp
  have well_init: "well_infl_stabl (init_state⦇called := called init_state - {x}⦈)"
    unfolding init_state_def well_infl_stabl_def fmlookup_default_def
    by simp
  then have well_result_state: "well_infl_stabl (state⦇called := called state - {x}⦈)"
    and x_stabl: "x ∈ stabl state"
    using well_infl_stabl_ind(2)[OF assms(1)[unfolded solve_dom_def] iterate]
    by auto
  moreover have "eq_equal_sides_subsumed T (σ state) (stabl state)"
    using eq_equal_sides_subsumed_ind(2)[OF assms(1)[unfolded solve_dom_def] iterate] c_empty
      well_init
    unfolding init_state_def
    by simp
  moreover have "∀u ∈ stabl state. dep⇩L T (σ state) u ⊆ stabl state"
    using well_infl_stabl_implies_stabl_c_closed[OF well_result_state] c_empty
    unfolding well_infl_stabl_def dep⇩L_def
    by simp
  ultimately show ?thesis using x_stabl st sigma by simp
qed

end ―‹end of context TD_side_unopt›


subsection ‹Least Partial Post-Solution with Monotonicity and Abort for Unoptimized Solver›

locale TD_side_unopt_mono = TD_side_unopt True T for
  T :: "'x ⇒ ('x, 'g, 'd :: bounded_semilattice_sup_bot) strategy_tree" +
  assumes mono_eq: "is_mono_eq T"
    and mono_sides: "mono_sides T"
    and mono_deps: "mono_deps T"
begin

subsubsection ‹Increasing Sigma and Upper Bound for Locales›

abbreviation locales_upper_bound :: "('x,'g,'d) state ⇒ bool" where
  "locales_upper_bound state ≡ ∀ξ. (σ state) (Inl ξ) ≤ eq T ξ (σ state)"

lemma increasing_sigma:
  shows "query_dom x y state
    ⟹ (yd, state') = query x y state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ (σ state) ≤ (σ state')
        ∧ locales_upper_bound state'"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {x}))
    ⟹ locales_upper_bound state
    ⟹ (σ state) ≤ (σ state')
        ∧ locales_upper_bound state'"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ (σ state) ≤ (σ state')
        ∧ locales_upper_bound state'"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ (σ state) ≤ (σ state')
        ∧ locales_upper_bound state'"
proof(induction x y state and x state and x state and x t state
    arbitrary: yd state' and xd state' and xd state' and xd state'
    rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state)
  show ?case using Query.IH(1) Query.prems(1)
  proof (cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    have well_infl_stabl: "well_infl_stabl (state⦇called := called state - {y}⦈)"
      using Query.prems(2) Iterate(5) by auto
    have eq_equal_sides_subsumed:
      "eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {y}))"
      using Query.prems(3) Iterate(5) by simp
    note IH = Query.IH(2)[OF Iterate(5,2), simplified, OF well_infl_stabl eq_equal_sides_subsumed
        Query.prems(4)]
    then show ?thesis by (simp add: Iterate(3))
  next
    case Lookup
    then show ?thesis using Query.prems(2-4) by auto
  qed
next
  case (Iterate x state)
  have well_infl_stabl: "well_infl_stabl state"
    using well_infl_stabl_simp_add_to_c[OF Iterate.prems(3)] by simp
  have part_sol: "eq_equal_sides_subsumed T (σ state) (stabl state - called state)"
    using Iterate.prems(4) by simp
  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Iterate.prems(5) by simp
  next
    case (Fixpoint state1)
    note IH = Iterate.IH(2)[OF Fixpoint(4,2) Iterate.prems(2) well_infl_stabl part_sol
      Iterate.prems(5)]
    have "x ∈ stabl state1"
      using well_infl_stabl_ind(3)[OF Fixpoint(1,2) Iterate.prems(2) well_infl_stabl] by simp
    then show ?thesis using IH by (auto simp add: Fixpoint(5))
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = Iterate.IH(2)[OF Continue(7,2) Iterate.prems(2) well_infl_stabl part_sol
      Iterate.prems(5)]
    note well_infl_stabl_1 =
      well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]
    note part_sol_1 = eq_equal_sides_subsumed_ind(3)[OF Continue(1,2) Iterate.prems(2)
      well_infl_stabl part_sol]

    have x_in_c1: "x ∈ called state1" using c_same(3)[OF Continue(1,2)] Iterate.prems(2) by simp
    have well_infl_stabl_2: "well_infl_stabl (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
      apply (rule destab_upd_locale_preserves_well_infl_stabl[OF Continue(4)])
      using conjunct1[OF well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]]
      unfolding well_infl_stabl_def
      by auto
    have eq_equal_sides_subsumed_2:
      "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - (called state1 - {x}))"
      apply (rule destab_upd_locale_preserves_part_solution[OF Continue(4)])
      using IH well_infl_stabl_1 part_sol_1 x_in_c1 by simp+

    have "σ state1 ≤ (σ state1)(Inl x := xd_new)"
    proof -
      have "eq T x (σ state1) = xd_new" using part_sol_1 by simp
      moreover have "σ state1 (Inl x) ≤ eq T x (σ state1)" using IH by simp
      ultimately have "σ state1 (Inl x) ≤ xd_new" by simp
      then show ?thesis
        apply (intro le_funI)
        subgoal for a
          by (cases "a = Inl x") (auto simp add: fun_upd_same fun_upd_other)
        done
    qed
    then have "eq T z (σ state1) ≤ eq T z ((σ state1)(Inl x := xd_new))" for z
      using mono_eq unfolding is_mono_eq_def by blast
    then have inv_2:
        "∀ξ. ((σ state1)(Inl x := xd_new)) (Inl ξ) ≤ eq T ξ ((σ state1)(Inl x := xd_new))"
      apply (intro allI)
      subgoal for y
        apply (cases "x = y")
        subgoal
          using part_sol_1 by (auto simp add: fun_upd_same)
        subgoal
          using IH
          by (auto intro: order_trans[of _ "eq T y (σ state1)"] simp add: fun_upd_other)
        done
      done

    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6), simplified, OF x_in_c1
        well_infl_stabl_2 eq_equal_sides_subsumed_2 inv_2]

    show ?thesis
      using IH ih ‹σ state1 ≤ (σ state1)(Inl x := xd_new)› order.trans
      by meson
  qed
next
  case (Repeat x state)
  have well_infl_stabl: "well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: well_infl_stabl_simp_c_stabl)
  have eq_equal_sides_subsumed:
    "eq_equal_sides_subsumed T (σ (state⦇stabl := insert x (stabl state)⦈))
      (stabl (state⦇stabl := insert x (stabl state)⦈) - called (state⦇stabl := insert x (stabl state)⦈))"
    using Repeat.prems(2,4) by simp
  have inv: "locales_upper_bound (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(5) by simp

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2) well_infl_stabl eq_equal_sides_subsumed inv]

    have "called state1 = called state"
      using c_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have well_infl_stabl_1: "well_infl_stabl state1"
      using well_infl_stabl_ind(4)[OF Unstable(1,2) well_infl_stabl, of "[]", simplified,
          OF Repeat.prems(2)]
      by simp
    note part_sol_1 = eq_equal_sides_subsumed_ind(4)[OF Unstable(1,2) well_infl_stabl, of "[]",
        simplified, OF Repeat.prems(4,2)]
    have inv_1: "locales_upper_bound state1" using IH by simp

    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5) x_in_c1 well_infl_stabl_1
        conjunct1[OF part_sol_1] inv_1, of d1, simplified]

    then show ?thesis using IH order.trans by fastforce
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2) well_infl_stabl eq_equal_sides_subsumed inv]
    then show ?thesis using Stable(3) by simp
  qed
next
  case (Eval x t state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,2,4) Eval.prems(2-4)]
    note well_infl_stabl_1 = well_infl_stabl_ind(1)[OF QueryL(3,4) Eval.prems(2)]
    note eq_equal_sides_subsumed_1 = eq_equal_sides_subsumed_ind(1)[OF QueryL(3,4) Eval.prems(2,3)]
    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6) conjunct1[OF well_infl_stabl_1]
      eq_equal_sides_subsumed_1 conjunct2[OF IH], simplified]
    have "σ state ≤ σ state'" using IH ih unfolding map_le_def
      by (meson dual_order.trans)
    then show ?thesis
      using QueryL IH ih by (auto simp add: Un_assoc)
  next
    case (QueryG y g yd)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    note IH = Eval.IH(4)[OF QueryG(1-3) QueryG(5), simplified, OF well_infl_stabl Eval.prems(3,4)]
    show ?thesis using IH by simp
  next
    case (Side_Subsumed y yd d' t1)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6) Eval.prems(2-4)]
    show ?thesis using IH by simp
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    have well_infl_stabl:
      "well_infl_stabl (state⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
      using destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5) Eval.prems(2)] by simp
    have part_sol: "eq_equal_sides_subsumed T ((σ state)(Inr y := d')) (stabl1 - called state)"
      using destab_upd_globale_preserves_part_solution Side_Effect(3,5) Eval.prems(3,2) by blast
    have inv: "locales_upper_bound (state⦇infl := infl1, stabl := stabl1,
      σ := (σ state)(Inr y := d')⦈)"
      apply (intro allI)
      subgoal for z
      proof -
        have "σ state ≤ (σ state)(Inr y := d')"
          apply (intro le_funI)
          subgoal for z
            apply (cases "Inr y = z")
            by (auto simp add: Side_Effect(3) fun_upd_same fun_upd_other)
          done
        then have "eq T z (σ state) ≤ eq T z ((σ state)(Inr y := d'))"
          using mono_eq unfolding is_mono_eq_def by blast
        moreover have "σ state (Inl z) ≤ eq T z (σ state)" using Eval.prems(4) by blast
        ultimately show ?thesis by (auto simp add: fun_upd_other)
      qed
      done
    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7) well_infl_stabl _ inv, simplified,
        OF part_sol]
    have "σ state ≤ (σ state)(Inr y := d')"
      using Side_Effect(3)
      apply (intro le_funI)
      subgoal for a
        by (cases "a = Inr y") (auto simp add: fun_upd_same fun_upd_other)
      done
    then show ?thesis using IH order.trans by blast
  next
    case (Abort)
    then show ?thesis using Eval.prems(4) by fast
  next
    case Answer
    then show ?thesis using Eval.prems(4) by simp
  qed
qed

subsubsection ‹Smallest Closed Set Stabl Containing the Unknown of Interest›

lemma mono_trans_dep⇩L: "sigma1 ≤ sigma2 ⟹ trans_dep⇩L T sigma1 x ⊆ trans_dep⇩L T sigma2 x"
proof
  fix u
  assume A: "sigma1 ≤ sigma2" "u ∈ trans_dep⇩L T sigma1 x"
  have "(x, u) ∈ trans_dep⇩L_rel T sigma1" using A(2) by blast
  then have "(x, u) ∈ trans_dep⇩L_rel T sigma2"
  proof (induction rule: trancl.induct)
    case (r_into_trancl u d)
    then have "d ∈ dep⇩L T sigma2 u" using mono_deps A(1) unfolding mono_deps_def dep⇩L_def by auto
    then show ?case by blast
  next
    case (trancl_into_trancl v u d)
    then have "d ∈ dep⇩L T sigma2 u" using mono_deps A(1) unfolding mono_deps_def dep⇩L_def by auto
    then have "(u,d) ∈ trans_dep⇩L_rel T sigma2" by blast
    then show ?case using trancl_into_trancl(3) by simp
  qed
  then show "u ∈ trans_dep⇩L T sigma2 x" by blast
qed

abbreviation stabl_in_trans_dep :: "('x,'g,'d) state ⇒ ('x,'g,'d) state ⇒ 'x ⇒ bool" where
  "stabl_in_trans_dep state state' x ≡
    stabl state' ⊆ stabl state ∪ trans_dep⇩L T (σ state') x"

lemma stabl_in_trans_dep_ind:
  shows "query_dom x y state
    ⟹ (yd, state') = query x y state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ y ∈ dep⇩L T (σ state) x
    ⟹ stabl_in_trans_dep state state' x"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {x}))
    ⟹ locales_upper_bound state
    ⟹ stabl_in_trans_dep (state⦇stabl := insert x (stabl state)⦈) state' x"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ stabl_in_trans_dep (state⦇stabl := insert x (stabl state)⦈) state' x"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ x ∈ called state
    ⟹ x ∈ stabl state ⟶ (subt_for_prefix (T x) pre (σ state) = Some t
        ∧ (∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p))
    ⟹ stabl_in_trans_dep state state' x"
proof(induction x y state and x state and x state and x t state
    arbitrary: yd state' and xd state' and xd state' and xd state' pre
    rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state)
  show ?case using Query.IH(1) Query.prems(1)
  proof (cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    have well_infl_stabl: "well_infl_stabl (state⦇called := called state - {y}⦈)"
      using Query.prems(2) Iterate(5) by auto
    have part_sol: "eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {y}))"
      using Query.prems(3) Iterate(5) by simp
    note IH = Query.IH(2)[OF Iterate(5,2), simplified, OF well_infl_stabl part_sol Query.prems(4)]
    have "insert y (trans_dep⇩L T (σ state1) y) ⊆ trans_dep⇩L T (σ state1) x"
    proof -
      have "y ∈ dep⇩L T (σ state) x" using Query.prems(5) by simp
      then have "y ∈ dep⇩L T (σ state1) x"
        using increasing_sigma(2)[OF Iterate(1,2), simplified, OF well_infl_stabl part_sol
            Query.prems(4)] mono_deps
        unfolding mono_deps_def dep⇩L_def
        by blast
      then show ?thesis using trans_dep⇩L_step[of y] by simp
    qed
    then show ?thesis using IH by (auto simp add: Iterate(3) simp flip: Un_insert_right)
  next
    case Lookup
    then show ?thesis using Query.prems(2-4) by auto
  qed
next
  case (Iterate x state)
  have well_infl_stabl: "well_infl_stabl state"
    using well_infl_stabl_simp_add_to_c[OF Iterate.prems(3)] by simp
  have eq_equal_sides_subsumed: "eq_equal_sides_subsumed T (σ state) (stabl state - called state)"
    using Iterate.prems(4) by simp
  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis by auto
  next
    case (Fixpoint state1)
    note IH = Iterate.IH(2)[OF Fixpoint(4,2) Iterate.prems(2) well_infl_stabl
      eq_equal_sides_subsumed Iterate.prems(5)]
    have "x ∈ stabl state1"
      using well_infl_stabl_ind(3)[OF Fixpoint(1,2) Iterate.prems(2) well_infl_stabl] by simp
    then show ?thesis using IH by (auto simp add: Fixpoint(5))
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = Iterate.IH(2)[OF Continue(7,2) Iterate.prems(2) well_infl_stabl
      eq_equal_sides_subsumed Iterate.prems(5)]
    note well_infl_stabl_1 =
      well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]
    note eq_equal_sides_subsumed_1 = eq_equal_sides_subsumed_ind(3)[OF Continue(1,2)
      Iterate.prems(2) well_infl_stabl eq_equal_sides_subsumed]

    have x_in_c1: "x ∈ called state1" using c_same(3)[OF Continue(1,2)] Iterate.prems(2) by simp
    have well_infl_stabl_2: "well_infl_stabl (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
      apply (rule destab_upd_locale_preserves_well_infl_stabl[OF Continue(4)])
      using conjunct1[OF well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]]
      unfolding well_infl_stabl_def
      by auto
    have eq_equal_sides_subsumed_2:
      "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - (called state1 - {x}))"
      apply (rule destab_upd_locale_preserves_part_solution[OF Continue(4)])
      using IH well_infl_stabl_1 eq_equal_sides_subsumed_1 x_in_c1 by simp+
    have sigma_smaller_upd: "σ state1 ≤ (σ state1)(Inl x := xd_new)"
      proof -
        have "eq T x (σ state1) = xd_new" using eq_equal_sides_subsumed_1 by simp
        moreover have "σ state1 (Inl x) ≤ eq T x (σ state1)"
          using increasing_sigma(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl
              eq_equal_sides_subsumed Iterate.prems(5)]
          by simp
        ultimately have "σ state1 (Inl x) ≤ xd_new" by simp
        then show ?thesis
          apply (intro le_funI)
          subgoal for a
            by (cases "a = Inl x") (auto simp add: fun_upd_same fun_upd_other)
          done
      qed
    have locales_ub_2: "locales_upper_bound (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new)⦈)"
    proof -
      have "eq T z (σ state1) ≤ eq T z ((σ state1)(Inl x := xd_new))" for z
        using sigma_smaller_upd mono_eq unfolding is_mono_eq_def by blast
      then show ?thesis
        apply (intro allI)
        subgoal for y
          apply (cases "x = y")
          subgoal
            using eq_equal_sides_subsumed_1 by (auto simp add: fun_upd_same)
          subgoal
            using increasing_sigma(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl
                eq_equal_sides_subsumed Iterate.prems(5)]
            by (auto intro: order_trans[of _ "eq T y (σ state1)"] simp add: fun_upd_other)
          done
        done
    qed

    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6) _ _ _ locales_ub_2,
      simplified, OF x_in_c1 well_infl_stabl_2 eq_equal_sides_subsumed_2]

    note sigma_incr_2 = increasing_sigma(2)[OF Continue(5,6) _ _ _ locales_ub_2, simplified,
        OF x_in_c1 well_infl_stabl_2 eq_equal_sides_subsumed_2]
    then have "σ state1 ≤ σ state'"
      using sigma_smaller_upd order.trans by blast
    then have "trans_dep⇩L T (σ state1) x ⊆ trans_dep⇩L T (σ state') x"
      using mono_trans_dep⇩L by simp
    moreover have "stabl2 ⊆ stabl state1"
      using destab_infl_stabl_relation[OF Continue(4)] by simp
    moreover have "called state1 = called state" using c_same(3)[OF Continue(1,2)] by simp
    ultimately show ?thesis using IH ih apply simp by blast
  qed
next
  case (Repeat x state)
  have well_infl_stabl: "well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: well_infl_stabl_simp_c_stabl)
  have eq_equal_sides_subsumed:
    "eq_equal_sides_subsumed T (σ (state⦇stabl := insert x (stabl state)⦈))
      (stabl (state⦇stabl := insert x (stabl state)⦈) - called (state⦇stabl := insert x (stabl state)⦈))"
    using Repeat.prems(2,4) by simp

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2) well_infl_stabl eq_equal_sides_subsumed, of "[]",
        simplified, OF Repeat.prems(5,2)]

    have "called state1 = called state"
      using c_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have well_infl_stabl_1: "well_infl_stabl state1"
      using well_infl_stabl_ind(4)[OF Unstable(1,2) well_infl_stabl, of "[]", simplified,
          OF Repeat.prems(2)]
      by simp
    note part_sol_1 = eq_equal_sides_subsumed_ind(4)[OF Unstable(1,2) well_infl_stabl, of "[]",
        simplified, OF Repeat.prems(4,2)]
    note incr_sigma_1 = increasing_sigma(4)[OF Unstable(1,2) well_infl_stabl
        eq_equal_sides_subsumed, simplified, OF Repeat.prems(5)]

    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5) x_in_c1 well_infl_stabl_1
        conjunct1[OF part_sol_1] conjunct2[OF incr_sigma_1] , of d1, simplified]

    note incr_sigma_2 = increasing_sigma(3)[OF Unstable(4,5) x_in_c1 well_infl_stabl_1
        conjunct1[OF part_sol_1] conjunct2[OF incr_sigma_1]]

    then have "trans_dep⇩L T (σ state1) x ⊆ trans_dep⇩L T (σ state') x"
      using mono_trans_dep⇩L by simp
    then show ?thesis using IH ih Repeat.prems(2) by auto
  next
    case Stable
    have locales_ub: "locales_upper_bound (state⦇stabl := insert x (stabl state)⦈)"
      using Repeat.prems(2,5) by simp
    note IH = Repeat.IH(2)[OF Stable(2) well_infl_stabl eq_equal_sides_subsumed locales_ub, of "[]",
        simplified]
    then show ?thesis using Stable(3) Repeat.prems(2) by auto
  qed
next
  case (Eval x t state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    have "subt_for_prefix (T x) pre (σ state) = Some t" using Eval.prems(6) QueryL(1) by simp
    then have "subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state) = Some (g ((σ state) (Inl y)))"
      by (rule subt_for_prefix_transitive[where ?pre2.0="[Inl (Inl y)]"])
         (simp add: QueryL(2))
    then have y_dep: "y ∈ dep⇩L T (σ state) x"
      using subt_for_prefix_subset_dep[of "T x" "pre @ [Inl (Inl y)]" "σ state"]
      unfolding dep⇩L_def dep_def by auto
    note IH = Eval.IH(2)[OF QueryL(1,2,4) Eval.prems(2-4) y_dep]
    note well_infl_stabl_1 = well_infl_stabl_ind(1)[OF QueryL(3,4) Eval.prems(2)]
    note part_sol_1 = eq_equal_sides_subsumed_ind(1)[OF QueryL(3,4) Eval.prems(2,3)]
    note incr_sigma = increasing_sigma(1)[OF QueryL(3,4) Eval.prems(2-4)]

    have x_in_c1: "x ∈ called state1" using c_same(1)[OF QueryL(3,4)] Eval.prems(5) by simp

    have prefix_no_indirect_side: "{p. Inl p ∈ set pre}
          ⊆ {u. ∃x ∈ called state ∩ stabl state1. x ∈ slookup (infl state) u}"
        if "x ∈ stabl state1"
      using lookup_in_influenced that called_non_stabl_increasing(1)[OF QueryL(3,4)] Eval.prems(5,6)
      by fastforce

    have prefix: "x ∈ stabl state1 ⟶
      (subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state1) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inl y)])}. x ∈ slookup (infl state1) p))"
    proof (intro impI, goal_cases)
      case 1
      then have "x ∈ stabl state"
        using called_non_stabl_increasing(1)[OF QueryL(3,4)] Eval.prems(5) by blast
      show ?case using Eval.prems(6)[rule_format, OF ‹x ∈ stabl state›]
      proof (intro conjI impI, goal_cases)
        case 1
        then show ?case
          apply (intro subt_for_prefix_transitive[where ?t2.0=t])
          subgoal
            apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
            subgoal using prefix_no_indirect_side ‹x ∈ stabl state1› well_infl_stabl_1 by fastforce
            subgoal by simp
            done
          subgoal using QueryL(2,7) by simp
          done
      next
        case 2
        then show ?case
          using conjunct2[OF well_infl_stabl_1] prefix_no_indirect_side[OF 1] by fastforce
      qed
    qed

    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6) conjunct1[OF well_infl_stabl_1] part_sol_1
        conjunct2[OF incr_sigma] x_in_c1 prefix, simplified]
    note incr_sigma_2 = increasing_sigma(4)[OF QueryL(5,6) conjunct1[OF well_infl_stabl_1]
        part_sol_1 conjunct2[OF incr_sigma]]
    then have "trans_dep⇩L T (σ state1) x ⊆ trans_dep⇩L T (σ state') x"
      using mono_trans_dep⇩L by simp
    then show ?thesis using IH ih by blast
  next
    case (QueryG y g yd)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    have pre: "x ∈ stabl state ⟶
      subt_for_prefix (T x) (pre @ [Inl (Inr y)]) (σ state) = Some (g yd) ∧
      (∀p. Inl p ∈ set (pre @ [Inl (Inr y)]) ⟶ x ∈ slookup (fminsert (infl state) (Inr y) x) p)"
      using Eval.prems(6) QueryG(2,3) subt_for_prefix_transitive[of "T x" pre _ t "[Inl (Inr y)]"]
      by (simp add: fminsert_def fmlookup_default_def)
    note IH = Eval.IH(4)[OF QueryG(1-3) QueryG(5), simplified, OF well_infl_stabl Eval.prems(3,4,5)
        pre]
    show ?thesis using IH by simp
  next
    case (Side_Subsumed y yd d' t1)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    have pre: "x ∈ stabl state ⟶
      subt_for_prefix (T x) (pre @ [Inr (y,yd)]) (σ state) = Some t1 ∧
      (∀p∈{p. Inl p ∈ set (pre @ [Inr (y,yd)])}. x ∈ slookup (infl state) p)"
      using Eval.prems(6) subt_for_prefix_transitive[of "T x" pre _ t "[Inr (y, yd)]" t1]
        Side_Subsumed(2)
      by simp
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6) Eval.prems(2-5) pre]
    show ?thesis using IH by simp
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    have well_infl_stabl:
      "well_infl_stabl (state⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
      using destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5) Eval.prems(2)] by simp
    have eq_equal_sides_subsumed:
      "eq_equal_sides_subsumed T ((σ state)(Inr y := d')) (stabl1 - called state)"
      using destab_upd_globale_preserves_part_solution Side_Effect(3,5) Eval.prems(3,2) by blast
    have B: "∀ξ. ((σ state)(Inr y := d')) (Inl ξ) ≤ eq T ξ ((σ state)(Inr y := d'))"
    proof -
      have "σ state ≤ (σ state)(Inr y := d')"
        apply (intro le_funI allI)
        subgoal for a
          apply (cases "a = Inr y")
          subgoal using Side_Effect(3) sup_ge1 by (simp add: fun_upd_same)
          subgoal by (simp add: fun_upd_other)
          done
        done
      then have "eq T a (σ state) ≤ eq T a ((σ state)(Inr y := d'))" for a
        using mono_eq unfolding is_mono_eq_def by simp
      then show ?thesis
        using Eval.prems(4) order.trans
        apply (simp add: fun_upd_other) by blast
    qed

    have prefix_recorded_in_infl:
      "∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p" if "x ∈ stabl state"
      using Eval.prems(6) that by simp
    have y_not_in_prefix: "Inl (Inr y) ∉ set pre" if "x ∈ stabl1"
    proof (rule ccontr, goal_cases)
      case 1
      then have "x ∈ slookup (infl state) (Inr y)"
        using prefix_recorded_in_infl that Side_Effect(1) by simp
      then have "x ∈ influenced_by (infl state) (Inr y)"
        using lookup_in_influenced by fastforce
      then show ?case using destab_infl_stabl_relation[OF Side_Effect(5)] that

        by simp
    qed
    have pre: "x ∈ stabl1 ⟶
      subt_for_prefix (T x) (pre @ [Inr (y,yd)]) ((σ state)(Inr y := d')) = Some t1 ∧
      (∀p. Inl p ∈ set (pre @ [Inr (y,yd)]) ⟶ x ∈ slookup infl1 p)"
    proof
      assume A: "x ∈ stabl1"
      have P: "subt_for_prefix (T x) pre ((σ state)(Inr y := d')) = Some t"
        apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
        subgoal using y_not_in_prefix A by (simp add: fun_upd_apply)
        subgoal using Eval.prems(6) Side_Effect(1) A by simp
        done
      show "subt_for_prefix (T x) (pre @ [Inr (y, yd)]) ((σ state)(Inr y := d')) = Some t1 ∧
        (∀p. Inl p ∈ set (pre @ [Inr (y, yd)]) ⟶ x ∈ slookup infl1 p)"
        apply (intro conjI)
        apply (subst subt_for_prefix_transitive[OF P(1), of "[Inr (y, yd)]" t1])
        subgoal using Side_Effect(2) by simp
        subgoal by simp
        subgoal
          apply (simp add: destab_infl_stabl_relation[OF Side_Effect(5)])
          by (smt (z3) A Diff_iff Side_Effect(5) destab_infl_stabl_relation fmdrop_set_insert
              fmlookup_default_drop_set image_iff influenced_by_transitive insert_iff
              lookup_in_influenced mem_Collect_eq prefix_recorded_in_infl subset_iff)
        done
    qed
    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7) well_infl_stabl, simplified,
        OF eq_equal_sides_subsumed B Eval.prems(5) pre]
    then show ?thesis using IH destab_infl_stabl_relation[OF Side_Effect(5)] by blast
  next
    case (Abort)
    then show ?thesis
      using Eval.prems(4) by fast
  next
    case Answer
    then show ?thesis
      using Eval.prems(2-4) unfolding map_le_def by simp
  qed
qed

lemma stabl_is_least:
  assumes "solve_dom x"
    and "(st, sigma) = solve x"
  shows "st = insert x (trans_dep⇩L T sigma x)"
proof -
  obtain xd state' where iterate: "st = stabl state'" "sigma = σ state'"
    "(xd, state') = iterate x (init_state⦇called := insert x (called init_state)⦈)"
    using assms
    unfolding solve_dom_def solve_def
    by (auto split: prod.splits)
  have "called state' = {}"
      using c_same(2)[OF assms(1)[unfolded solve_dom_def] iterate(3)]
      unfolding init_state_def by simp
  have "st ⊆ insert x (trans_dep⇩L T sigma x)"
    using stabl_in_trans_dep_ind(2)[OF assms(1)[unfolded solve_dom_def] iterate(3)] ‹called state' = {}›
    unfolding init_state_def well_infl_stabl_def fmlookup_default_def
    by (simp add: iterate(1,2))
  moreover have "insert x (trans_dep⇩L T sigma x) ⊆ st"
  proof -
    have "well_infl_stabl (state'⦇called := called state' - {x}⦈)" "x ∈ stabl state'"
      using well_infl_stabl_ind(2)[OF assms(1)[unfolded solve_dom_def] iterate(3)]
      unfolding well_infl_stabl_def init_state_def fmlookup_default_def
      by auto
    then have S: "∀y∈stabl state'. dep⇩L T (σ state') y ⊆ stabl state'"
      using well_infl_stabl_implies_stabl_c_closed[of "state'⦇called := called state' - {x}⦈"]
      by (simp add: ‹called state' = {}›)
    have "u ∈ stabl state'" if "(x,u) ∈ trans_dep⇩L_rel T (σ state')" "x ∈ stabl state'" for u
      using that
    proof (induction rule: trancl.induct)
      case (r_into_trancl a b)
      then show ?case using S(1) by blast
    next
      case (trancl_into_trancl a b called)
      then show ?case using S(1) by blast
    qed
    then show ?thesis using ‹x ∈ stabl state'› by (auto simp add: iterate(1,2))
  qed
  ultimately show ?thesis by simp
qed

subsubsection ‹Least Partial Post-Solution›

definition less_than_least :: "'x ⇒ ('x + 'g ⇒ 'd) ⇒ bool" where
  "less_than_least x sigma ≡
    (∀σl varsl. part_post_solution T x σl varsl ⟶ sigma ≤ σl)"

lemma less_than_part_post_solution_ind:
  shows "query_dom x y state
    ⟹ (yd, state') = query x y state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ less_than_least z (σ state)
    ⟹ y ∈ insert z (trans_dep⇩L T (σ state) z)
    ⟹ less_than_least z (σ state')"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {x}))
    ⟹ locales_upper_bound state
    ⟹ less_than_least z (σ state)
    ⟹ x ∈ insert z (trans_dep⇩L T (σ state) z)
    ⟹ less_than_least z (σ state')"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ less_than_least z (σ state)
    ⟹ x ∈ insert z (trans_dep⇩L T (σ state) z)
    ⟹ less_than_least z (σ state')"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ x ∈ called state
    ⟹ less_than_least z (σ state)
    ⟹ x ∈ insert z (trans_dep⇩L T (σ state) z)
    ⟹ x ∈ stabl state ⟶ (subt_for_prefix (T x) pre (σ state) = Some t
        ∧ (∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p))
    ⟹ less_than_least z (σ state')"
proof(induction x y state and x state and x state and x t state
    arbitrary: yd state' and xd state' and xd state' and xd state' pre
    rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state)
  show ?case using Query.IH(1) Query.prems(1)
  proof (cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    have well_infl_stabl: "well_infl_stabl (state⦇called := called state - {y}⦈)"
      using Query.prems(2) Iterate(5) by auto
    have part_sol: "eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {y}))"
      using Query.prems(3) Iterate(5) by simp
    have stabl_subset_P: "y ∈ insert z (trans_dep⇩L T (σ (state⦇called := insert y (called state)⦈)) z)"
      using Query.prems(6) Iterate(3) by simp
    note IH = Query.IH(2)[OF Iterate(5,2) _ _ _ _ _ stabl_subset_P, simplified,
        OF well_infl_stabl part_sol Query.prems(4) Query.prems(5)]
    show ?thesis using IH by (simp add: Iterate(3))
  next
    case Lookup
    show ?thesis using Query.prems(5) Lookup(2) by auto
  qed
next
  case (Iterate x state)
  have well_infl_stabl: "well_infl_stabl state"
    using well_infl_stabl_simp_add_to_c[OF Iterate.prems(3)] by simp
  have part_sol: "eq_equal_sides_subsumed T (σ state) (stabl state - called state)"
    using Iterate.prems(4) by simp
  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    show ?thesis using Stable(1) Iterate.prems(6) by auto
  next
    case (Fixpoint state1)
    have "σ state1 ≤ σ state'"
      using Fixpoint(5) by simp
    have subset_P: "x ∈ insert z (trans_dep⇩L T (σ state) z)"
      using Iterate.prems(7)
      by (simp add: Fixpoint(5))
    note IH = Iterate.IH(2)[OF Fixpoint(4,2) Iterate.prems(2) well_infl_stabl part_sol
        Iterate.prems(5,6) subset_P]
    have "x ∈ stabl state1"
      using well_infl_stabl_ind(3)[OF Fixpoint(1,2) Iterate.prems(2) well_infl_stabl] by simp
    show ?thesis using IH unfolding less_than_least_def by (auto simp add: Fixpoint(5))
  next
    case (Continue state1 xd_new infl2 stabl2)
    have x_in_c1: "x ∈ called state1" using c_same(3)[OF Continue(1,2)] Iterate.prems(2) by simp

    note well_infl_stabl_1 =
      well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]
    note part_sol_1 = eq_equal_sides_subsumed_ind(3)[OF Continue(1,2) Iterate.prems(2)
      well_infl_stabl part_sol]
    note incr_sigma_1 = increasing_sigma(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl
      part_sol Iterate.prems(5)]

    have well_infl_stabl_2: "well_infl_stabl (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
      apply (rule destab_upd_locale_preserves_well_infl_stabl[OF Continue(4)])
      using conjunct1[OF well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]]
      unfolding well_infl_stabl_def
      by auto
    have eq_equal_sides_subsumed_2:
      "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - (called state1 - {x}))"
      apply (rule destab_upd_locale_preserves_part_solution[OF Continue(4)])
      using well_infl_stabl_1 part_sol_1 x_in_c1 by simp+

    have sigma_smaller_upd: "σ state1 ≤ (σ state1)(Inl x := xd_new)"
    proof -
      have "xd_new = eq T x (σ state1)" using part_sol_1 by simp
      then have "σ state1 (Inl x) ≤ xd_new" using incr_sigma_1 by simp
      then show ?thesis
        apply (intro le_funI)
        subgoal for a
          by (cases "a = Inl x") (auto simp add: fun_upd_same fun_upd_other)
        done
    qed

    have locales_ub_2: "locales_upper_bound (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new)⦈)"
    proof -
      have "eq T z (σ state1) ≤ eq T z ((σ state1)(Inl x := xd_new))" for z
        using sigma_smaller_upd mono_eq unfolding is_mono_eq_def by blast
      then show ?thesis
        apply (intro allI)
        subgoal for y
          apply (cases "x = y")
          subgoal
            using part_sol_1 by (auto simp add: fun_upd_same)
          subgoal
            using increasing_sigma(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl part_sol
              Iterate.prems(5)]
            by (auto intro: order_trans[of _ "eq T y (σ state1)"] simp add: fun_upd_other)
          done
        done
    qed

    have "σ state1 ≤ σ state'"
      using increasing_sigma(2)[OF Continue(5,6) _ _ _ locales_ub_2, simplified,
          OF x_in_c1 well_infl_stabl_2 eq_equal_sides_subsumed_2] sigma_smaller_upd
      by auto
    then have subset_P: "x ∈ insert z (trans_dep⇩L T (σ state) z)"
      using Iterate.prems(7) mono_trans_dep⇩L
      by blast
    note IH = Iterate.IH(2)[OF Continue(7,2) Iterate.prems(2) well_infl_stabl part_sol
        Iterate.prems(5,6) subset_P]

    have less_inv_2: "less_than_least z ((σ state1)(Inl x := xd_new))"
      unfolding less_than_least_def
    proof (intro allI impI)
      fix σl varsl y
      assume P: "part_post_solution T z σl varsl"
      show "(σ state1)(Inl x := xd_new) ≤ σl"
      proof (intro conjI le_funI, goal_cases)
        case (1 y)
        show ?case
        proof (cases "y = Inl x")
          case True
          have "σ state ≤ σl" using Iterate.prems(6) P unfolding less_than_least_def by auto
          then have "x ∈ insert z (trans_dep⇩L T σl z)" using mono_trans_dep⇩L subset_P by blast
          then have x_varsl: "x ∈ varsl"
            using part_post_solution_implies_trans_dep_subsumed[of z varsl T] P by auto
          have "xd_new = eq T x (σ state1)" using part_sol_1 by auto
          moreover have "eq T x (σ state1) ≤ eq T x σl"
          proof -
            have "eq T x (σ state1) ≤ eq T x ((σ state1)(Inl x := xd_new))"
              using mono_eq ‹σ state1 ≤ (σ state1)(Inl x := xd_new)›
              unfolding is_mono_eq_def by blast
            moreover have "eq T x ((σ state1)(Inl x := xd_new)) ≤ eq T x σl"
            proof -
              have "σ state1 ≤ σl" using IH P unfolding less_than_least_def by auto
              then have "eq T x (σ state1) ≤ eq T x σl"
                using mono_eq unfolding is_mono_eq_def by blast
              then have "xd_new ≤ eq T x σl" by (simp add: ‹xd_new = eq T x (σ state1)›)
              have "xd_new ≤ σl (Inl x)"
                using ‹xd_new ≤ eq T x σl› P x_varsl by auto
              then have "(σ state1)(Inl x := xd_new) ≤ σl"
                using ‹σ state1 ≤ σl›
                apply (intro le_funI)
                subgoal for a
                  by (cases "a = Inl x") (auto simp add: le_funD fun_upd_same fun_upd_other)
                done
              then show ?thesis using mono_eq unfolding is_mono_eq_def by blast
            qed
            ultimately show ?thesis by simp
          qed
          moreover have "eq T x σl ≤ σl (Inl x)"
            using P IH x_varsl unfolding less_than_least_def by blast
          ultimately show ?thesis by (simp add: True fun_upd_same)
        next
          case False
          have "σ state1 ≤ σl" using IH P unfolding less_than_least_def by blast
          then show ?thesis using False by (auto simp add: fun_upd_other le_fun_def)
        qed
      qed
    qed
    have "x ∈ insert z (trans_dep⇩L T (σ state1) z)"
      using Iterate.prems(7) mono_trans_dep⇩L[OF conjunct1[OF incr_sigma_1]] by blast
    then have in_trans_dep: "x ∈ insert z (trans_dep⇩L T
          (σ (state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(Inl x := xd_new)⦈)) z)"
      using mono_trans_dep⇩L[OF ‹σ state1 ≤ (σ state1)(Inl x := xd_new)›]
      by auto

    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6) _ _ _ locales_ub_2 _
        in_trans_dep, simplified, OF x_in_c1 well_infl_stabl_2 eq_equal_sides_subsumed_2
        less_inv_2]

    show ?thesis
      using IH ih ‹σ state1 ≤ (σ state1)(Inl x := xd_new)› order.trans
      by meson
  qed
next
  case (Repeat x state)
  have well_infl_stabl: "well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: well_infl_stabl_simp_c_stabl)
  have eq_equal_sides_subsumed:
    "eq_equal_sides_subsumed T (σ (state⦇stabl := insert x (stabl state)⦈))
      (stabl (state⦇stabl := insert x (stabl state)⦈) - called (state⦇stabl := insert x (stabl state)⦈))"
    using Repeat.prems(2,4) by simp
  have subset_trans: "x ∈ insert z (trans_dep⇩L T (σ (state⦇stabl := insert x (stabl state)⦈)) z)"
    using Repeat.prems(7) by simp

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)

    have "called state1 = called state"
      using c_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have well_infl_stabl_1: "well_infl_stabl state1"
      using well_infl_stabl_ind(4)[OF Unstable(1,2) well_infl_stabl, of "[]", simplified,
          OF Repeat.prems(2)]
      by simp
    note eq_equal_sides_subsumed_1 = eq_equal_sides_subsumed_ind(4)[OF Unstable(1,2)
        well_infl_stabl, of "[]", simplified, OF Repeat.prems(4,2)]
    have eq_equal_sides_subsumed:
      "eq_equal_sides_subsumed T (σ state) (insert x (stabl state) - called state)"
      using Repeat.prems(2,4) by simp
    note incr_sigma_1 = increasing_sigma(4)[OF Unstable(1,2) well_infl_stabl, simplified,
        OF eq_equal_sides_subsumed Repeat.prems(5)]
    note incr_sigma_2 = increasing_sigma(3)[OF Unstable(4,5) x_in_c1 well_infl_stabl_1
        conjunct1[OF eq_equal_sides_subsumed_1] conjunct2[OF incr_sigma_1]]

    note IH = Repeat.IH(2)[OF Unstable(2) well_infl_stabl _ _ _ _ subset_trans, of "[]",
        simplified, OF Repeat.prems(4,5,2,6)]

    have subset_trans_1: "x ∈ insert z (trans_dep⇩L T (σ state1) z)"
      using mono_trans_dep⇩L[OF conjunct1[OF incr_sigma_1]] Repeat.prems(7) by blast
    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5) x_in_c1 well_infl_stabl_1
        conjunct1[OF eq_equal_sides_subsumed_1] conjunct2[OF incr_sigma_1] IH subset_trans_1,
        of d1, simplified]

    show ?thesis using IH ih order.trans by fastforce
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2) well_infl_stabl eq_equal_sides_subsumed _ _ _
        subset_trans, of "[]", simplified, OF Repeat.prems(5,2,6)]
    then show ?thesis using Stable(3) by simp
  qed
next
  case (Eval x t state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    have "subt_for_prefix (T x) pre (σ state) = Some t" using Eval.prems(8) QueryL(1) by simp
    then have "subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state) = Some (g ((σ state) (Inl y)))"
      by (rule subt_for_prefix_transitive[where ?pre2.0="[Inl (Inl y)]"])
         (simp add: QueryL(2))
    then have y_dep_x: "y ∈ dep⇩L T (σ state) x"
      using subt_for_prefix_subset_dep[of "T x" "pre @ [Inl (Inl y)]" "σ state"]
      unfolding dep⇩L_def dep_def by auto
    note well_infl_stabl_1 = well_infl_stabl_ind(1)[OF QueryL(3,4) Eval.prems(2)]
    note eq_equal_sides_subsumed_1 = eq_equal_sides_subsumed_ind(1)[OF QueryL(3,4) Eval.prems(2,3)]
    note incr_sigma_1 = increasing_sigma(1)[OF QueryL(3,4) Eval.prems(2-4)]
    have x_in_c1: "x ∈ called state1" using c_same(1)[OF QueryL(3,4)] Eval.prems(5) by simp
    note incr_sigma' = increasing_sigma(4)[OF QueryL(5,6) conjunct1[OF well_infl_stabl_1]
        eq_equal_sides_subsumed_1 conjunct2[OF incr_sigma_1]]
    have "x ∈ stabl state" using QueryL(1) by simp

    have "σ state ≤ σ state'" using incr_sigma' incr_sigma_1 by auto
    then have y_dep_x': "y ∈ dep⇩L T (σ state') x"
      using y_dep_x mono_deps unfolding mono_deps_def dep_def dep⇩L_def by auto
    have "y ∈ trans_dep⇩L T (σ state) x"
      using trancl.r_into_trancl y_dep_x by blast
    then have subset_trans: "y ∈ insert z (trans_dep⇩L T (σ state) z)"
      using Eval.prems(7) trancl_trans by fastforce

    note IH = Eval.IH(2)[OF QueryL(1,2,4) Eval.prems(2-4) Eval.prems(6) subset_trans]

    have prefix_no_indirect_side: "{p. Inl p ∈ set pre}
        ⊆ {u. ∃x ∈ called state ∩ stabl state1. x ∈ slookup (infl state) u}" if "x ∈ stabl state1"
      using that Eval.prems(5,8) ‹x ∈ stabl state› by blast

    have prefix: "x ∈ stabl state1 ⟶
      (subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state1) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inl y)])}. x ∈ slookup (infl state1) p))"
    proof (intro impI, goal_cases)
      case 1
      then have "x ∈ stabl state"
        using called_non_stabl_increasing(1)[OF QueryL(3,4)] Eval.prems(5) by blast
      show ?case using Eval.prems(8)[rule_format, OF ‹x ∈ stabl state›]
      proof (intro conjI impI, goal_cases)
        case 1
        then show ?case
          apply (intro subt_for_prefix_transitive[where ?t2.0=t])
          subgoal
            apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
            subgoal using prefix_no_indirect_side ‹x ∈ stabl state1› well_infl_stabl_1 by fastforce
            subgoal by simp
            done
          subgoal using QueryL(2,7) by simp
          done
      next
        case 2
        then show ?case
          using conjunct2[OF well_infl_stabl_1] prefix_no_indirect_side[OF 1] by fastforce
      qed
    qed

    have subset_trans_1: "x ∈ insert z (trans_dep⇩L T (σ state1) z)"
      using mono_trans_dep⇩L[OF conjunct1[OF incr_sigma_1]] Eval.prems(7) by blast
    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6) conjunct1[OF well_infl_stabl_1]
        eq_equal_sides_subsumed_1 conjunct2[OF incr_sigma_1] x_in_c1 IH subset_trans_1 prefix]
    show ?thesis using QueryL IH ih by auto
  next
    case (QueryG y g yd)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    have pre: "x ∈ stabl state ⟶
      subt_for_prefix (T x) (pre @ [Inl (Inr y)]) (σ state) = Some (g yd) ∧
      (∀p. Inl p ∈ set (pre @ [Inl (Inr y)]) ⟶ x ∈ slookup (fminsert (infl state) (Inr y) x) p)"
      using Eval.prems(8) QueryG(2,3) subt_for_prefix_transitive[of "T x" pre _ t "[Inl (Inr y)]"]
      by (simp add: fminsert_def fmlookup_default_def)
    have subset_trans:
      "x ∈ insert z (trans_dep⇩L T (σ (state⦇infl := fminsert (infl state) (Inr y) x⦈)) z)"
      using Eval.prems(7) by simp
    note IH = Eval.IH(4)[OF QueryG(1-3) QueryG(5) _ _ _ _ _ subset_trans, simplified,
        OF well_infl_stabl Eval.prems(3-6) pre]
    show ?thesis using IH by simp
  next
    case (Side_Subsumed y yd d' t1)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    have pre: "x ∈ stabl state ⟶
      subt_for_prefix (T x) (pre @ [Inr (y,yd)]) (σ state) = Some t1 ∧
      (∀p∈{p. Inl p ∈ set (pre @ [Inr (y,yd)])}. x ∈ slookup (infl state) p)"
      using Eval.prems(8) subt_for_prefix_transitive[of "T x" pre _ t "[Inr (y, yd)]" t1]
        Side_Subsumed(2)
      by simp
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6) Eval.prems(2-7) pre]
    show ?thesis using IH by simp
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    have well_infl_stabl:
      "well_infl_stabl (state⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
      using destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5) Eval.prems(2)] by simp
    have eq_equal_sides_subsumed:
      "eq_equal_sides_subsumed T ((σ state)(Inr y := d')) (stabl1 - called state)"
      using destab_upd_globale_preserves_part_solution Side_Effect(3,5) Eval.prems(3,2) by blast
    have locale_ub: "locales_upper_bound (state⦇infl := infl1, stabl := stabl1,
      σ := (σ state)(Inr y := d')⦈)"
      apply (intro allI)
      subgoal for z
      proof -
        have "σ state ≤ (σ state)(Inr y := d')"
          apply (intro le_funI)
          subgoal for z
            apply (cases "Inr y = z")
            by (auto simp add: Side_Effect(3) fun_upd_same fun_upd_other)
          done
        then have "eq T z (σ state) ≤ eq T z ((σ state)(Inr y := d'))"
          using mono_eq unfolding is_mono_eq_def by blast
        moreover have "σ state (Inl z) ≤ eq T z (σ state)" using Eval.prems(4) by blast
        ultimately show ?thesis by (auto simp add: fun_upd_other)
      qed
      done
    have less_inv:
      "less_than_least z ((σ state)(Inr y := d'))"
      unfolding less_than_least_def
    proof (intro allI impI)
      fix σl varsl
      assume P: "part_post_solution T z σl varsl"
      then have "σ state ≤ σl" using Eval.prems(6) unfolding less_than_least_def by blast
      moreover have "d' ≤ σl (Inr y)"
        apply (auto simp add: Side_Effect(3))
        subgoal using ‹σ state ≤ σl› by (simp add: le_funD)
        subgoal
        proof -
          have "yd ≤ sides_of_rhs (T x) (σ state) (Inr y)"
            using sides_of_rhs_helper[of "T x" pre "σ state" y yd t1] Eval.prems(8)
              Side_Effect(1,2)
            by blast
          moreover have "sides_of_rhs (T x) (σ state) (Inr y) ≤ sides_of_rhs (T x) σl (Inr y)"
            using ‹σ state ≤ σl› mono_sides unfolding mono_sides_def by (simp add: le_funD)
          moreover have "sides_of_rhs (T x) σl (Inr y) ≤ σl (Inr y)"
          proof -
            have "x ∈ insert z (trans_dep⇩L T σl z)"
              using Eval.prems(7) mono_trans_dep⇩L[OF ‹σ state ≤ σl›] by blast
            then have "x ∈ varsl"
              using part_post_solution_implies_trans_dep_subsumed[of z varsl] P by blast
            then have "sides_of_rhs (T x) σl ≤ σl"
              using ‹part_post_solution T z σl varsl› Eval.prems(6)
              unfolding less_than_least_def by blast
            then show ?thesis by (simp add: le_fun_def)
          qed
          ultimately show ?thesis
            using Eval.prems(6) ‹part_post_solution T z σl varsl› unfolding less_than_least_def
            by auto
        qed
        done
      ultimately show "(σ state)(Inr y := d') ≤ σl"
        apply (intro conjI le_funI)
        subgoal for z
          by (cases "z = Inr y") (auto elim: le_funE simp add: fun_upd_same fun_upd_other)
        done
    qed

    have prefix_recorded_in_infl:
      "∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p" if "x ∈ stabl state"
      using Eval.prems(8) that by simp
    have y_not_in_prefix: "Inl (Inr y) ∉ set pre" if "x ∈ stabl1"
    proof (rule ccontr, goal_cases)
      case 1
      then have "x ∈ slookup (infl state) (Inr y)"
        using prefix_recorded_in_infl that Side_Effect(1) by simp
      then have "x ∈ influenced_by (infl state) (Inr y)"
        using lookup_in_influenced by fastforce
      then show ?case using destab_infl_stabl_relation[OF Side_Effect(5)] that by simp
    qed
    have pre: "x ∈ stabl1 ⟶
      subt_for_prefix (T x) (pre @ [Inr (y,yd)]) ((σ state)(Inr y := d')) = Some t1 ∧
      (∀p. Inl p ∈ set (pre @ [Inr (y,yd)]) ⟶ x ∈ slookup infl1 p)"
    proof
      assume A: "x ∈ stabl1"
      have P: "subt_for_prefix (T x) pre ((σ state)(Inr y := d')) = Some t"
        apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
        subgoal using y_not_in_prefix A by (simp add: fun_upd_apply)
        subgoal using Eval.prems(8) Side_Effect(1) A by simp
        done
      show "subt_for_prefix (T x) (pre @ [Inr (y, yd)]) ((σ state)(Inr y := d')) = Some t1 ∧
        (∀p. Inl p ∈ set (pre @ [Inr (y, yd)]) ⟶ x ∈ slookup infl1 p)"
        apply (intro conjI)
        apply (subst subt_for_prefix_transitive[OF P(1), of "[Inr (y, yd)]" t1])
        subgoal using Side_Effect(2) by simp
        subgoal by simp
        subgoal
          apply (simp add: destab_infl_stabl_relation[OF Side_Effect(5)])
          by (smt (z3) A Diff_iff Side_Effect(5) destab_infl_stabl_relation fmdrop_set_insert
              fmlookup_default_drop_set image_iff influenced_by_transitive insert_iff
              lookup_in_influenced mem_Collect_eq prefix_recorded_in_infl subset_iff)
        done
    qed
    have "σ state ≤ (σ state)(Inr y := d')"
      apply (intro le_funI)
      subgoal for z
        apply (cases "z = Inr y")
        by (auto simp add: fun_upd_same fun_upd_other Side_Effect(3))
      done
    then have trans_dep_1: "x ∈ insert z (trans_dep⇩L T
      (σ (state⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)) z)"
      using mono_trans_dep⇩L Eval.prems(7) by auto
    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7) well_infl_stabl _ locale_ub _ _
        trans_dep_1, simplified, OF eq_equal_sides_subsumed Eval.prems(5) less_inv pre]
    show ?thesis using IH by blast
  next
    case (Abort)
    then show ?thesis
      using Eval.prems(6) by fast
  next
    case Answer
    then show ?thesis
      using Eval.prems(6) by simp
  qed
qed

lemma less_than_part_post_solution:
  assumes "solve_dom x"
    and "solve x = (st, sigma)"
  shows "∀σl varsl. part_post_solution T x σl varsl ⟶ sigma ≤ σl ∧ st ⊆ varsl"
proof (intro allI impI, goal_cases)
  case (1 σl varsl)
  obtain xd state' where
    iterate: "(xd, state') = iterate x (init_state⦇called := insert x (called init_state)⦈)" and
    "st = stabl state'" and sigma: "sigma = σ state'"
    using assms unfolding solve_dom_def solve_def by (auto split: prod.splits)
  then have st: "st = insert x (trans_dep⇩L T (σ state') x)"
    using stabl_is_least[OF assms(1) assms(2)[symmetric]] by simp
  then have "∀σl varsl. part_post_solution T x σl varsl ⟶ σ state' ≤ σl"
    apply (intro less_than_part_post_solution_ind(2)[OF assms(1)[unfolded solve_dom_def] iterate(1),
          unfolded less_than_least_def])
    unfolding init_state_def well_infl_stabl_def fmlookup_default_def
    by (auto simp add: le_fun_def)
  then have "σ state' ≤ σl" using 1 by blast
  then have "insert x (trans_dep⇩L T (σ state') x) ⊆ insert x (trans_dep⇩L T σl x)"
    using mono_trans_dep⇩L by blast
  then have "insert x (trans_dep⇩L T (σ state') x) ⊆ varsl"
    using 1 part_post_solution_implies_trans_dep_subsumed[of x varsl] mono_trans_dep⇩L by blast
  then show ?case
    using ‹σ state' ≤ σl› by (auto simp add: sigma st)
qed

theorem least_partial_post_solution:
  assumes "solve_dom x"
    and "solve x = (st, sigma)"
  shows "least_part_post_solution T x sigma st"
proof -
  note part_sol = partial_solution[OF assms]
  then have "part_post_solution T x sigma st" by simp
  moreover have least: "∀σl varsl. part_post_solution T x σl varsl ⟶ sigma ≤ σl ∧ st ⊆ varsl"
    using less_than_part_post_solution[OF assms]
    by auto
  ultimately show ?thesis by blast
qed


end ―‹end of context TD_side_unopt_mono›


subsection ‹Correctness of Optimized TDside Stopping Destabilization at Called Unknowns›

locale TD_side_opt =
  fixes abort :: "bool"
    and T :: "('x,'g,'d::bounded_semilattice_sup_bot) eqsT"
begin

sublocale TD_side destab_opt
  unfolding TD_side_def
  using destab_opt_infl_stabl_relation
  by blast


subsubsection ‹Well-formedness of Stable Set and Infl Map›

paragraph ‹Preservation of the Well-formedness of Stabl and Infl when Destabilizing›

lemma destab_x_no_dep:
  assumes "stabl2 = stabl state1 - influenced_by_cutoff (infl state1) (Inl x)
    (Inl ` called state1 - {Inl x})"
    and "∀y∈(stabl state1) - (called state1 - {x}). ∀z∈dep T (σ state1) y. y ∈ slookup (infl state1) z"
  shows "∀y ∈ stabl2 - (called state1 - {x}). Inl x ∉ dep T (σ state1) y"
proof (intro ballI, goal_cases)
  case (1 y)
  show ?case
  proof (rule ccontr, goal_cases)
    case 1
    then have "y ∈ slookup (infl state1) (Inl x)"
      using assms ‹y ∈ stabl2 - (called state1 - {x})› by blast
    then have "y ∈ influenced_by_cutoff (infl state1) (Inl x) (Inl ` called state1 - {Inl x})"
      by (metis Diff_iff influenced_by_cutoff.simps set_fmlookup_default_cases singletonI)
    moreover have "y ∉ influenced_by_cutoff (infl state1) (Inl x) (Inl ` called state1 - {Inl x})"
      using assms(1) ‹y ∈ stabl2 - (called state1 - {x})› by fastforce
    ultimately show ?case by blast
  qed
qed

lemma destab_and_upd_preserves_dep_closed_in_infl:
  assumes "(infl2, stabl2) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1)"
    and "(∀y∈stabl state1 - (called state1 - {x}). ∀z∈dep T (σ state1) y. y ∈ slookup (infl state1) z)"
  shows "(∀y∈stabl2 - (called state1 - {x}). ∀z∈dep T ((σ state1)(Inl x := xd')) y.
            y ∈ slookup infl2 z)"
proof (intro ballI, goal_cases)
  case (1 z y)
  have infl2_def: "infl2 = fmdrop_set (insert (Inl x) (Inl ` (influenced_by_cutoff (infl state1)
      (Inl x) (Inl ` called state1 - {Inl x})) - (Inl ` called state1 - {Inl x}))) (infl state1)"
    and stabl2_def: "stabl2 = (stabl state1) - influenced_by_cutoff (infl state1) (Inl x)
      (Inl ` called state1 - {Inl x})"
    using destab_opt_infl_stabl_relation[OF assms(1)]
    by auto

  have "y ∈ dep T (σ state1) z"
  proof (goal_cases)
    case 1
    have "∀y∈stabl2 - (called state1 - {x}). Inl x ∉ dep T (σ state1) y"
      using assms(2) stabl2_def destab_x_no_dep by blast
    then have "Inl x ∉ dep T (σ state1) z"
        using ‹z ∈ stabl2 - (called state1 - {x})› by blast
      then have "dep T ((σ state1)(Inl x := xd')) z = dep T (σ state1) z"
        apply (intro dep_eq[of T "σ state1", symmetric])
        apply (intro ballI)
        subgoal for y
          apply (cases "y = Inl x")
          by (auto simp add: fun_upd_same fun_upd_other)
        done
    then show ?case using ‹y ∈ dep T ((σ state1)(Inl x := xd')) z› by auto
  qed
  then have z_in_infl1_y: "z ∈ slookup (infl state1) y"
    using 1(1) stabl2_def assms(2) by fastforce

  consider "y ∈ Inl ` called state1 - {Inl x}" |
      "z ∈ influenced_by_cutoff (infl state1) y (Inl ` called state1 - {Inl x})"
    using influenced_by_cutoff.simps z_in_infl1_y
    by (metis set_fmlookup_default_cases)
  then have "y ∉ Inl ` influenced_by_cutoff (infl state1) (Inl x) (Inl ` called state1 - {Inl x}) -
    (Inl ` called state1 - {Inl x})"
    and "y ≠ Inl x"
    subgoal
      apply (cases)
      subgoal by blast
      subgoal
        by (smt (verit, best) "1"(1) Diff_iff image_iff influenced_by_transitive
        influenced_unknowns_fmdrop_set stabl2_def)
      done
    subgoal
      by (metis "1"(1) destab_x_no_dep ‹y ∈ dep T (σ state1) z› assms(2) stabl2_def)
    done
  then show ?case
    using z_in_infl1_y
    unfolding fmlookup_default_def infl2_def
    by auto
qed

text‹The following lemmas show that the well-formedness of infl and stabl are preserved when
  destabilizing and unknown and updating its value in @{term σ}.›

lemma destab_upd_locale_preserves_well_infl_stabl:
  assumes "(infl2, stabl2) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1)"
      and "well_infl_stabl (state1⦇called := called state1 - {x}⦈)"
    shows "well_infl_stabl (state1⦇infl := infl2, stabl := stabl2,
            σ := (σ state1)(Inl x := d_new), called := called state1 - {x} ⦈)"
proof -
  show ?thesis
    unfolding well_infl_stabl_def
    apply simp
  proof (intro conjI, goal_cases)
    case 2
    have "{u. slookup (infl (state1⦇called := called state1 - {x}⦈)) (Inl u) ≠ {}}
      ⊆ stabl (state1⦇called := called state1 - {x}⦈) ∪ called (state1⦇called := called state1 - {x}⦈)"
      using assms(2) unfolding well_infl_stabl_def by simp
    then show ?case
      using destab_opt_infl_stabl_relation[OF assms(1)]
      by (auto simp add: fmlookup_default_drop_set simp flip: fmdrop_set_insert)

    case 1
    show ?case
      using destab_and_upd_preserves_dep_closed_in_infl[OF assms(1)] assms(2)
      unfolding well_infl_stabl_def
      by simp
  qed
qed

lemma destab_upd_globale_preserves_well_infl_stabl:
  assumes destab: "(infl1, stabl1) = destab_opt (Inr y) (infl state) (stabl state) (called state)"
      and "well_infl_stabl state"
    shows "well_infl_stabl (state⦇infl := infl1, stabl := stabl1,
            σ := (σ state)(Inr y := d') ⦈)"
  using assms(2) unfolding well_infl_stabl_def
  apply (simp add: destab_opt_infl_stabl_relation[OF assms(1)])
  apply (intro conjI)
  subgoal
  proof (intro ballI, goal_cases 2)
    case (2 u v)
    have "v ∈ dep T (σ state) u"
    proof -
      have "u ∉ influenced_by_cutoff (infl state) (Inr y) (Inl ` called state - {Inr y})"
        "u ∈ stabl state" "u ∉ called state"
        using 2(2) by auto
      then have "u ∉ slookup (infl state) (Inr y)"
        using influenced_by_cutoff.base[of "Inr y" "Inl ` called state - {Inr y}" "infl state" _ u]
        unfolding fmlookup_default_def
        by (split option.splits, auto)
      then have "Inr y ∉ dep T (σ state) u"
        using 2(1) ‹u ∈ stabl state› ‹u ∉ called state› by blast
      then show ?thesis
        using 2(3)
        apply (subst dep_eq[of _ _ _ "(σ state)(Inr y := d')"])
        by (metis fun_upd_other)
    qed
    then have "u ∈ slookup (infl state) v" using 2(1,2) by blast
    then have "v ∈ Inl ` called state - {Inr y} ∨
      u ∈ influenced_by_cutoff (infl state) v (Inl ` called state - {Inr y})"
      using influenced_by_cutoff.base[of v _ "infl state" _ u]
      by (meson set_fmlookup_default_cases)
    then have "v ∈ Inl ` called state ∨
      (v ∉ Inl ` influenced_by_cutoff (infl state) (Inr y) (Inl ` called state - {Inr y}) ∧ v ≠ Inr y)"
      using 2(2) influenced_by_transitive[of _ _ "Inr y" u]
      by (auto simp flip: influenced_unknowns_fmdrop_set)
    then show ?case
      using ‹u ∈ slookup (infl state) v›
      by (auto simp add: fmlookup_default_drop_set simp flip: fmdrop_set_insert)
  qed
  subgoal
  proof -
    have "{u. slookup (infl state) (Inl u) ≠ {}} ⊆ stabl state ∪ called state"
      using assms(2) unfolding well_infl_stabl_def by simp
    then show ?thesis
      by (auto simp add: fmlookup_default_drop_set simp flip: fmdrop_set_insert)
  qed
  done


paragraph ‹Helper Lemmas to Deduce Update Predicate›

lemma influencing_stabl_after_destab':
  assumes "(infl2, stabl2) = destab_opt y infl1 stabl1 c1"
    "z ∈ slookup infl1 u" "z ∈ stabl2"
  shows "z ∈ slookup infl2 u"
proof (rule ccontr, goal_cases)
  case 1
  then have "z ∉ slookup (fmdrop_set (insert y (Inl ` influenced_by_cutoff infl1 y (Inl ` c1 - {y})
     - (Inl ` c1 - {y}))) infl1) u"
    using destab_opt_infl_stabl_relation[OF assms(1)] by blast
  then consider "u = y"
    | "u ∈ Inl ` influenced_by_cutoff infl1 y (Inl ` c1 - {y})" "u ∉ Inl ` c1 - {y}"
    using assms(2)
    unfolding fmlookup_default_def
    by (metis DiffE fmlookup_drop_set insertE)
  then have "z ∈ influenced_by_cutoff infl1 y (Inl ` c1 - {y})"
    using assms(2)
    apply cases
    subgoal using lookup_in_influenced_cutoff by fast
    subgoal
      using influenced_by_cutoff.step[of _ _ y _ _ z]
      unfolding fmlookup_default_def by fastforce
    done
  then have "z ∉ stabl2" using destab_opt_infl_stabl_relation[OF assms(1)] by blast
  then show ?case using assms(3) by simp
qed

lemma update_rel_transitive:
  assumes update_rel: "update_rel_opt state1 state2" "update_rel_opt state2 state3"
    and indicator_u_dec: "called state3 ∩ stabl state3 ⊆ called state2 ∩ stabl state2"
    and called_same: "called state1 = called state2" "called state2 = called state3"
  shows "update_rel_opt state1 state3"
proof -
  let ?no_indirect_side1 = "{u. ∃x∈called state1 ∩ stabl state2. x ∈ slookup (infl state1) u}"
  let ?no_indirect_side2 = "{u. ∃x∈called state2 ∩ stabl state3. x ∈ slookup (infl state2) u}"
  let ?no_indirect_side3 = "{u. ∃x∈called state1 ∩ stabl state3. x ∈ slookup (infl state1) u}"
  have unaffected_subset: "?no_indirect_side3 ⊆ ?no_indirect_side1"
      "?no_indirect_side3 ⊆ ?no_indirect_side2"
    using update_rel(1) indicator_u_dec called_same
    by fastforce+

  show ?thesis
    apply simp
    apply (intro conjI)
    subgoal
      using unaffected_subset conjunct1[OF update_rel(1)[simplified]]
        conjunct1[OF update_rel(2)[simplified]]
      by blast
    subgoal
      using unaffected_subset conjunct1[OF conjunct2[OF update_rel(1)[simplified]]]
        conjunct1[OF conjunct2[OF update_rel(2)[simplified]]]
      apply (simp only: called_same)
      by blast
    subgoal
      using unaffected_subset conjunct2[OF conjunct2[OF update_rel(1)[simplified]]]
        conjunct2[OF conjunct2[OF update_rel(2)[simplified]]]
      by fastforce
    done
qed


paragraph ‹Induction Proof›

lemma well_infl_stabl_ind:
  shows "query_dom x y state
    ⟹ (xd, state') = query x y state
    ⟹ well_infl_stabl state
    ⟹ well_infl_stabl state'
      ∧ x ∈ slookup (infl state') (Inl y)
      ∧ update_rel_opt state state'"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ well_infl_stabl (state'⦇called := called state' - {x}⦈)
      ∧ x ∈ stabl state'
      ∧ update_rel_opt (state⦇called := called state - {x}⦈) (state'⦇called := called state' - {x}⦈)"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl state
    ⟹ well_infl_stabl (state'⦇called := called state' - {x}⦈)
      ∧ x ∈ stabl state'
      ∧ update_rel_opt (state⦇called := called state - {x}⦈) (state'⦇called := called state' - {x}⦈)"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ well_infl_stabl state
    ⟹ x ∈ called state
    ⟹ x ∈ stabl state ⟶ (subt_for_prefix (T x) pre (σ state) = Some t
        ∧ (∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p))
    ⟹ well_infl_stabl state'
      ∧ (x ∈ stabl state' ⟶ (∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y))
      ∧ update_rel_opt state state'"
proof(induction x y state and x state and x state and y t state
    arbitrary: xd state' and xd state' and xd state' and pre xd state'
    rule: query_iterate_repeat_eval_pinduct)
  case (Query y x state)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    note IH = Query.IH(2)[simplified, OF Iterate(5,2) Query.prems(2)]
    then show ?thesis
      using Iterate(3,4) unfolding well_infl_stabl_def
      by (auto simp add: slookup_fminsert split: if_splits)
  next
    case Lookup
    show ?thesis
      using Query.prems(2) Lookup(3)
      unfolding well_infl_stabl_def
      by (auto simp add: Lookup(2) slookup_fminsert)
  qed
next
  case (Iterate x state)
  have inv: "well_infl_stabl state"
    using well_infl_stabl_simp_add_to_c[OF Iterate.prems(3)] by simp
  note IH' = Iterate.IH(2)[rotated 2, OF Iterate.prems(2) inv]

  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    show ?thesis using Stable(2,3) Iterate.prems(3) by (auto simp add: Stable(1))
  next
    case (Fixpoint state1)
    note IH = IH'[OF Fixpoint(4,2), folded dep_def]
    then show ?thesis
      unfolding well_infl_stabl_def
      by (auto simp add: Fixpoint(5))
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = IH'[OF Continue(7,2)]

    have c_state1_same_state: "called state1 = called state"
      using c_same(3)[OF Continue(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Iterate.prems(2) by simp

    have inv: "well_infl_stabl (state1⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
      apply (rule destab_upd_locale_preserves_well_infl_stabl[OF Continue(4)])
      using IH
      by auto

    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6), simplified,
              OF x_in_c1 inv]

    have "called state' = called state1 - {x}" using c_same(2)[OF Continue(5,6)] x_in_c1 by simp

    with IH show ?thesis
    proof(elim conjE, intro conjI, goal_cases)
      case 1
      show ?case using ih by blast
    next
      case 2
      show ?case using ih by blast
    next
      case 3
      have upd_rel_destab:
        "update_rel_opt (state1⦇called := called state1 - {x}⦈) (state1⦇infl := infl2, stabl := stabl2,
          σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
        using destab_opt_infl_stabl_relation[OF Continue(4)] Continue(4)
          influencing_stabl_after_destab'[OF Continue(4)]
        by (auto simp add: fmlookup_default_drop_set fun_upd_other simp del: fmdrop_set_insert
            split: if_split)
      have upd_rel_begin_destab:
        "update_rel_opt (state⦇called := called state - {x}⦈) (state1⦇infl := infl2, stabl := stabl2,
          σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
        apply (intro update_rel_transitive[OF 3(4) upd_rel_destab])
        using called_non_stabl_increasing(3)[OF Continue(1,2)] ‹called state1 = called state›
          destab_opt_infl_stabl_relation[OF Continue(4)]
        by auto
      show ?case
        apply (intro update_rel_transitive[OF upd_rel_begin_destab])
        using ih called_non_stabl_increasing(2)[OF Continue(5,6)] ‹called state' = called state1 - {x}›
          c_state1_same_state
        by auto
    qed
  qed
next
  case (Repeat x state)
  have inv: "well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: well_infl_stabl_simp_c_stabl)
  have prefix: "x ∈ stabl (state⦇stabl := insert x (stabl state)⦈) ⟶ (
      subt_for_prefix (T x) [] (σ (state⦇stabl := insert x (stabl state)⦈)) = Some (T x)
      ∧ (∀p ∈ {p. Inl p ∈ set []}. x ∈ slookup (infl (state⦇stabl := insert x (stabl state)⦈)) p))"
    by simp+

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2) inv _ prefix, simplified, OF Repeat.prems(2)]

    have "called state1 = called state"
      using c_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have inv1: "well_infl_stabl state1"
      using IH by simp

    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5) x_in_c1 inv1, of d1, simplified]

    have "called state' = called state1" using c_same(3)[OF Unstable(4,5)] by simp
    have "(called state - {x}) ∩ stabl state1 = called state ∩ stabl state1" using Unstable(3) by blast

    show ?thesis
      apply (intro conjI)
      subgoal using ih by simp
      subgoal using ih by simp
      subgoal
        apply (rule update_rel_transitive[of _
          "state1⦇called := called state1 - {x}, stabl := insert x (stabl state1)⦈"])
        subgoal using IH Unstable(3) Repeat.prems(2)
          by (auto simp add: ‹called state1 = called state› ‹called state' = called state1›
              ‹(called state - {x}) ∩ stabl state1 = called state ∩ stabl state1› Let_def)
        subgoal using ih Unstable(3) by auto
        subgoal using called_non_stabl_increasing(3)[OF Unstable(4,5)] ‹called state' = called state1› by auto
        subgoal using ‹called state1 = called state› by simp
        subgoal using ‹called state' = called state1› by simp
        done
      done
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2) inv _ prefix, simplified, OF Repeat.prems(2)]
    show ?thesis
      unfolding well_infl_stabl_def
      apply (intro conjI)
      subgoal
        apply (rule ballI)
        using IH Stable(3)
        unfolding well_infl_stabl_def dep_def
        by auto
      subgoal using IH Stable(3) unfolding well_infl_stabl_def by auto
      subgoal
        using Stable(3) by blast
      subgoal
        apply simp
        using Stable(3) IH by blast
      done
  qed
next
  case (Eval x t state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,2,4) Eval.prems(2)]

    have "called state1 = called state" using c_same(1)[OF QueryL(3,4)] by simp
    then have "x ∈ called state1" using Eval.prems(3) by simp
    have "called state' = called state1" using c_same(4)[OF QueryL(5,6)] by simp

    have prefix_no_indirect_side: "{p. Inl p ∈ set pre}
        ⊆ {u. ∃x ∈ called state ∩ stabl state1. x ∈ slookup (infl state) u}"
        if "x ∈ stabl state1"
      using that called_non_stabl_increasing(1)[OF QueryL(3,4)] ‹x ∈ called state1› Eval.prems(3,4) IH
      by fastforce

    have prefix: "x ∈ stabl state1 ⟶
      (subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state1) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inl y)])}. x ∈ slookup (infl state1) p))"
    proof (intro impI, goal_cases)
      case 1
      then have "x ∈ stabl state"
        using called_non_stabl_increasing(1)[OF QueryL(3,4)] Eval.prems(3) by blast
      show ?case using Eval.prems(4)[rule_format, OF ‹x ∈ stabl state›]
      proof (intro conjI impI, goal_cases)
        case 1
        then show ?case
          apply (intro subt_for_prefix_transitive[where ?t2.0=t])
          subgoal
            apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
            subgoal using prefix_no_indirect_side ‹x ∈ stabl state1› IH by fastforce
            subgoal by simp
            done
          subgoal using QueryL(2,7) by simp
          done
      next
        case 2
        then show ?case
          using conjunct2[OF IH] prefix_no_indirect_side[OF 1] by fastforce
      qed
    qed

    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6) conjunct1[OF IH] ‹x ∈ called state1› prefix,
        simplified]

    have y_unaffected:
      "Inl y ∈ {u. ∃x ∈ called state1 ∩ stabl state'. x ∈ slookup (infl state1) u}"
        if "x ∈ stabl state'"
      using lookup_in_influenced that called_non_stabl_increasing(4)[OF QueryL(5,6)]
        prefix c_same(4)[OF QueryL(5,6)] ‹x ∈ called state1›
      by fastforce
    have y_value_unchanged: "(σ state') (Inl y) = yd" if "x ∈ stabl state'"
      using y_unaffected[OF that] ih QueryL(7) by fastforce
    have y_infl_incr: "slookup (infl state1) (Inl y) ⊆ slookup (infl state') (Inl y)"
      if "x ∈ stabl state'"
      using y_unaffected[OF that] ih by auto

    show ?thesis
      apply (intro conjI)
      subgoal using ih by simp
      subgoal using ih IH y_infl_incr by (auto simp add: QueryL(2) y_value_unchanged)
      subgoal
        apply (rule update_rel_transitive[of _ state1])
        using IH ih called_non_stabl_increasing(4)[OF QueryL(5,6)] ‹called state' = called state1›
          ‹called state1 = called state›
        by auto
      done
  next
    case (QueryG y g yd)
    have inv: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def by auto
    have prefix: "x ∈ stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈) ⟶ (
        subt_for_prefix (T x) (pre @ [Inl (Inr y)])
        (σ (state⦇infl := fminsert (infl state) (Inr y) x⦈)) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inr y)])}. x ∈ slookup
        (infl (state⦇infl := fminsert (infl state) (Inr y) x⦈)) p))"
      using Eval.prems(4) QueryG(2,3) subt_for_prefix_transitive[of "T x" pre _ t "[Inl (Inr y)]"]
      by (simp add: fminsert_def fmlookup_default_def)
    note IH = Eval.IH(4)[OF QueryG(1-3,5) inv _ prefix, simplified, OF Eval.prems(3)]

    have y_unaffected: "Inr y ∈ {u. ∃z ∈ called state ∩ stabl state'.
        z ∈ slookup (fminsert (infl state) (Inr y) x) u}"
        if "x ∈ stabl state'"
      using lookup_in_influenced that called_non_stabl_increasing(4)[OF QueryG(4,5)]
        c_same(4)[OF QueryG(4,5)] ‹x ∈ called state›
      by (auto simp add: slookup_fminsert_same)
    have y_value_unchanged: "(σ state') (Inr y) = yd" if "x ∈ stabl state'"
      using y_unaffected IH QueryG(3) that by fastforce
    have y_infl_incr: "slookup (infl (state⦇infl := fminsert (infl state) (Inr y) x⦈)) (Inr y)
        ⊆ slookup (infl state') (Inr y)" if "x ∈ stabl state'"
      using y_unaffected IH that by fastforce

    show ?thesis
      apply (intro conjI)
      subgoal using IH by simp
      subgoal
        using IH y_infl_incr by (auto simp add: QueryG(2) y_value_unchanged slookup_fminsert_same)
      subgoal using IH by (auto simp add: slookup_fminsert split: if_splits)
      done
  next
    case (Side_Subsumed y yd d' t1)
    have prefix: "x ∈ stabl state ⟶
      (subt_for_prefix (T x) (pre @ [Inr (y, yd)]) (σ state) = Some t1
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inr (y, yd)])}. x ∈ slookup (infl state) p))"
      using Eval.prems(4) subt_for_prefix_transitive[of "T x" pre _ t "[Inr (y, yd)]" t1]
        Side_Subsumed(2)
      by simp
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6) Eval.prems(2,3) prefix]

    have "x ∈ stabl state' ⟶ (∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y)"
      using IH
      by (simp add: Side_Subsumed(2) dep_aux⇩L_def)

    then show ?thesis using IH by simp
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    have inv:
        "well_infl_stabl (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
      using destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5) Eval.prems(2)]
      by simp
    have x_stabl_if_stabl1: "x ∈ stabl state" if "x ∈ stabl1"
      using destab_opt_infl_stabl_relation[OF Side_Effect(5)] that by simp

    have prefix_recorded_in_infl:
      "∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p" if "x ∈ stabl state"
      using Eval.prems(4) that by simp

    have y_not_in_prefix: "Inl (Inr y) ∉ set pre" if "x ∈ stabl1"
    proof (rule ccontr, goal_cases)
      case 1
      then have "x ∈ slookup (infl state) (Inr y)"
        using prefix_recorded_in_infl that x_stabl_if_stabl1 by simp
      then have "x ∈ influenced_by_cutoff (infl state) (Inr y) (Inl ` called state - {Inr y})"
        using lookup_in_influenced_cutoff by fastforce
      then show ?case using destab_opt_infl_stabl_relation[OF Side_Effect(5)] that by simp
    qed

    have prefix: "x ∈ stabl (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)
      ⟶ (subt_for_prefix (T x) (pre @ [Inr (y, yd)]) (σ (state
        ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)) = Some t1
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inr (y, yd)])}. x ∈ slookup
        (infl (state ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)) p))"
      apply simp
    proof
      assume A: "x ∈ stabl1"
      have P: "subt_for_prefix (T x) pre ((σ state)(Inr y := d')) = Some t"
        apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
        subgoal using y_not_in_prefix A by (simp add: fun_upd_apply)
        subgoal using Eval.prems(4) x_stabl_if_stabl1 A by simp
        done
      show "subt_for_prefix (T x) (pre @ [Inr (y, yd)]) ((σ state)(Inr y := d')) = Some t1 ∧
        (∀p. Inl p ∈ set pre ⟶ x ∈ slookup infl1 p)"
        apply (intro conjI)
        apply (subst subt_for_prefix_transitive[OF P(1), of "[Inr (y, yd)]" t1])
        subgoal using Side_Effect(2) by simp
        subgoal by simp
        subgoal
          using influencing_stabl_after_destab'[OF Side_Effect(5) _ A]
            prefix_recorded_in_infl[OF x_stabl_if_stabl1[OF A]]
          by fast
        done
    qed

    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7) inv _ prefix, simplified,
        OF Eval.prems(3)]

    have upd_rel_destab:
      "update_rel_opt state (state⦇infl := infl1, stabl := stabl1,
        σ := (σ state)(Inr y := d')⦈)"
      using destab_opt_infl_stabl_relation[OF Side_Effect(5)] Side_Effect(5)
        influencing_stabl_after_destab'[OF Side_Effect(5)]
      by (auto simp add: fmlookup_default_drop_set fun_upd_other simp del: fmdrop_set_insert
          split: if_split)

    have "called state' = called state"
      using c_same(4)[OF Side_Effect(6,7)] by simp

    have "x ∈ stabl state' ⟶ (∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y)"
      using IH by (simp add: Side_Effect(2) dep_aux⇩L_def)

    then show ?thesis
      apply (intro conjI)
      subgoal using IH by simp
      subgoal using IH by simp
      subgoal
        apply (rule update_rel_transitive[OF upd_rel_destab])
        subgoal using IH by auto
        subgoal
          using called_non_stabl_increasing(4)[OF Side_Effect(6,7)] ‹called state' = called state› by auto
        subgoal by simp
        subgoal using ‹called state' = called state› by simp
        done
      done
  next
    case Answer
    have "∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y"
      by (simp add: Answer(2) dep_aux_def)
    moreover have "dep_aux⇩L (σ state) t ⊆ stabl state ∪ called state"
      by (simp add: Answer(2) dep_aux⇩L_def)
    ultimately show ?thesis using Eval.prems(2) Answer(3) by fastforce
  next
    case Abort
    then show ?thesis using Eval.prems(2) by fastforce
  qed
qed

corollary solve_returns_stabl_closed_under_dep:
  assumes "solve_dom x"
    and "solve x = (st, sigma)"
  shows "∀x∈st. dep⇩L T sigma x ⊆ st"
proof -
  obtain xd state' where
      iterate: "(xd, state') = iterate x (init_state⦇ called := insert x (called init_state) ⦈)"
      and "st = stabl state'" and "sigma = σ state'"
    using assms unfolding solve_dom_def solve_def
    by (cases "iterate x (init_state⦇called := insert x (called init_state)⦈)") auto
  then have "well_infl_stabl (state'⦇called := called state' - {x}⦈)"
    using well_infl_stabl_ind(2)[OF assms(1)[unfolded solve_dom_def]]
    unfolding well_infl_stabl_def init_state_def fmlookup_default_def
    by auto
  show ?thesis
    using well_infl_stabl_implies_stabl_c_closed[OF ‹well_infl_stabl (state'⦇called := called state' - {x}⦈)›]
      ‹st = stabl state'› ‹sigma = σ state'› c_same(2)[OF assms(1)[unfolded solve_dom_def] iterate]
    unfolding well_infl_stabl_def init_state_def
    by simp
qed

subsubsection ‹Partial Correctness›

paragraph ‹Preservation of the Partial Solution when Destabilizing›

lemma destab_upd_locale_preserves_part_solution:
  assumes destab: "(infl2, stabl2) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1)"
      and IH: "eq_equal_sides_subsumed T (σ state1) (stabl state1 - called state1)"
          "eq T x (σ state1) = xd_new"
          "sides_of_rhs (T x) (σ state1) ≤ σ state1"
      and x_in_c1: "x ∈ called state1"
      and well_infl_stabl_1: "well_infl_stabl (state1⦇called := called state1 - {x}⦈)"
    shows "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - (called state1 - {x}))"
proof -
  have "eq_equal_sides_subsumed T (σ state1) (stabl state1 - called state1)"
    using IH by simp
  have "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - called state1)"
  proof (intro ballI, goal_cases)
    case (1 y)
    then have "y ∈ stabl state1 - called state1" "x ≠ y"
      using destab x_in_c1 destab_opt_infl_stabl_relation[OF destab] by auto
    then have "eq T y (σ state1) = (σ state1) (Inl y)"
      "sides_of_rhs (T y) (σ state1) ≤ σ state1"
      using IH by simp+
    have "Inl x ∉ dep T (σ state1) y"
    proof (rule ccontr, goal_cases)
      case 1
      then have "Inl x ∈ dep T (σ state1) y" by simp
      then have "y ∈ slookup (infl state1) (Inl x)"
        using well_infl_stabl_1 ‹y ∈ stabl state1 - called state1›
        unfolding well_infl_stabl_def
        by simp
      then have "y ∈ influenced_by_cutoff (infl state1) (Inl x) (Inl ` called state1 - {Inl x})"
        using lookup_in_influenced_cutoff by fast
      then have "y ∉ stabl2" using destab_opt_infl_stabl_relation[OF destab] by simp
      then show ?case using ‹y ∈ stabl2 - called state1› by simp
    qed
    then have "eq T y (σ state1) = eq T y ((σ state1)(Inl x := xd_new))"
      using eq_mupd_no_dep
      unfolding dep_def by fast
    moreover have "(σ state1) (Inl y) = ((σ state1)(Inl x := xd_new)) (Inl y)"
      using ‹x ≠ y› by (simp add: fun_upd_other)
    moreover have "sides_of_rhs (T y) ((σ state1)(Inl x := xd_new)) ≤ (σ state1)(Inl x := xd_new)"
      apply (rule subsumes_se_eq[of "σ state1"])
      subgoal
      proof -
        have "Inl x ∉ dep_aux (σ state1) (T y)"
          using ‹Inl x ∉ dep T (σ state1) y› unfolding dep_aux_def dep_def by simp
        then show ?thesis by (metis fun_upd_other)
      qed
      subgoal
        by (simp add: fun_upd_other)
      subgoal
        using IH ‹y ∈ stabl state1 - called state1› by blast
      done
    ultimately show ?case
      using ‹eq T y (σ state1) = (σ state1) (Inl y)› by simp
  qed
  moreover have "eq T x ((σ state1)(Inl x := xd_new)) = xd_new"
    "sides_of_rhs (T x) ((σ state1)(Inl x := xd_new)) ≤ (σ state1)(Inl x := xd_new)" if "x ∈ stabl2"
  proof -
    have "x ∈ stabl state1"
      using that destab_opt_infl_stabl_relation[OF destab] by simp
    have "x ∉ influenced_by_cutoff (infl state1) (Inl x) (Inl ` called state1 - {Inl x})"
      using that destab_opt_infl_stabl_relation[OF destab] by simp
    then have "x ∉ slookup (infl state1) (Inl x)"
      using lookup_in_influenced_cutoff by fast
    then have "Inl x ∉ dep T (σ state1) x"
      using conjunct1[OF well_infl_stabl_1[unfolded well_infl_stabl_def]]
        ‹x ∈ stabl state1›
      by auto
    then show "eq T x ((σ state1)(Inl x := xd_new)) = xd_new"
      using eq_mupd_no_dep IH
      unfolding dep_def by fastforce
    show "sides_of_rhs (T x) ((σ state1)(Inl x := xd_new)) ≤ (σ state1)(Inl x := xd_new)"
      apply (rule subsumes_se_eq[of "σ state1"])
      subgoal
      proof -
        have "Inl x ∉ dep_aux (σ state1) (T x)"
          using ‹Inl x ∉ dep T (σ state1) x› unfolding dep_aux_def dep_def by simp
        then show ?thesis
          using ‹Inl x ∉ dep T (σ state1) x›
          by (metis fun_upd_other)
      qed
      subgoal
        by (simp add: fun_upd_other)
      subgoal
        using IH by blast
      done
  qed
  ultimately show ?thesis by (auto simp add: fun_upd_same)
qed

lemma destab_upd_globale_preserves_part_solution:
  assumes destab: "(infl1, stabl1) = destab_opt (Inr y) (infl state) (stabl state) (called state)"
      and eq_equal_sides_subsumed: "eq_equal_sides_subsumed T (σ state) (stabl state - called state)"
      and well_infl_stabl: "well_infl_stabl state"
      and d_join: "d' = (σ state) (Inr y) ⊔ d"
    shows "eq_equal_sides_subsumed T ((σ state)(Inr y := d')) (stabl1 - called state)"
proof (intro ballI, goal_cases)
  case (1 x)
  then have "x ∈ stabl state - called state"
    using destab_opt_infl_stabl_relation[OF destab] by auto
  then have "eq T x (σ state) = (σ state) (Inl x)" "sides_of_rhs (T x) (σ state) ≤ σ state"
    using eq_equal_sides_subsumed by simp+
  have "Inr y ∉ dep T (σ state) x"
  proof (rule ccontr, goal_cases)
    case 1
    then have "Inr y ∈ dep T (σ state) x" by simp
    then have "x ∈ slookup (infl state) (Inr y)"
      using well_infl_stabl ‹x ∈ stabl state - called state›
      unfolding well_infl_stabl_def by simp
    then have "x ∈ influenced_by_cutoff (infl state) (Inr y) (Inl ` called state - {Inr y})"
      using lookup_in_influenced_cutoff by fast
    then have "x ∉ stabl1" using destab_opt_infl_stabl_relation[OF destab] by simp
    then show ?case using ‹x ∈ stabl1 - called state› by simp
  qed
  then have "eq T x (σ state) = eq T x ((σ state)(Inr y := d'))"
    using eq_mupd_no_dep
    unfolding dep_def by fast
  moreover have "(σ state) (Inl x) = ((σ state)(Inr y := d')) (Inl x)"
    by (simp add: fun_upd_other)
  moreover have "sides_of_rhs (T x) ((σ state)(Inr y := d')) ≤ (σ state)(Inr y := d')"
    apply (rule subsumes_se_eq[of "σ state"])
    subgoal
    proof -
      have "Inr y ∉ dep_aux (σ state) (T x)"
        using ‹Inr y ∉ dep T (σ state) x› unfolding dep_aux_def dep_def by simp
      then show ?thesis
        using ‹Inr y ∉ dep T (σ state) x›
        by (metis fun_upd_other)
    qed
    subgoal
    proof
      fix u
      show "(σ state) (Inr u) ≤ ((σ state)(Inr y := d')) (Inr u)"
        apply (cases "u = y")
        subgoal using d_join by (simp add: fun_upd_same)
        subgoal by (simp add: fun_upd_other)
        done
    qed
    subgoal
      using eq_equal_sides_subsumed ‹x ∈ stabl state - called state› by blast
    done
  ultimately show ?case
    using ‹eq T x (σ state) = (σ state) (Inl x)› by simp
qed


paragraph ‹Induction Proof›

lemma eq_equal_sides_subsumed_ind:
  shows "query_dom x y state
    ⟹ (xd, state') = query x y state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ eq_equal_sides_subsumed T (σ state') (stabl state' - called state')"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {x}))
    ⟹ eq_equal_sides_subsumed T (σ state') (stabl state' - (called state' - {x}))"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ eq_equal_sides_subsumed T (σ state') (stabl state' - called state')
        ∧ eq T x (σ state') = xd
        ∧ sides_of_rhs (T x) (σ state') ≤ σ state'"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ x ∈ called state
    ⟹ x ∈ stabl state ⟶ (subt_for_prefix (T x) pre (σ state) = Some t
        ∧ (∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p)
        ∧ (∀(u, ud) ∈ {s. Inr s ∈ set pre}. ud ≤ (σ state) (Inr u)))
    ⟹ eq_equal_sides_subsumed T (σ state') (stabl state' - called state')
        ∧ (x ∈ stabl state' ⟶ eq T x (σ state') = xd
                                ∧ sides_of_rhs (T x) (σ state') ≤ σ state')"
proof(induction x y state and x state and x state and y t state
    arbitrary: xd state' and xd state' and xd state' and pre xd state'
    rule: query_iterate_repeat_eval_pinduct)
  case (Query y x state)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    note IH = Query.IH(2)[simplified, OF Iterate(5,2) Query.prems(2,3)]
    then show ?thesis by (simp add: Iterate(3))
  next
    case Lookup
    show ?thesis using Query.prems(3) by (simp add: Lookup(2))
  qed
next
  case (Iterate x state)
  have inv: "well_infl_stabl state"
    using well_infl_stabl_simp_add_to_c[OF Iterate.prems(3)] by simp
  have eq_equal_sides_subsumed: "eq_equal_sides_subsumed T (σ state) (stabl state - called state)"
    using Iterate.prems(4) by simp
  note IH' = Iterate.IH(2)[rotated 2, OF Iterate.prems(2) inv eq_equal_sides_subsumed]

  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    show ?thesis using Stable(2,3) Iterate.prems(4) by (simp add: Stable(1))
  next
    case (Fixpoint state1)
    note IH = IH'[OF Fixpoint(4,2), folded dep_def]

    then show ?thesis by (auto simp add: Fixpoint(3,5))
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = IH'[OF Continue(7,2)]
    note well_infl_stabl_1 = well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) inv]

    have c_state1_same_state: "called state1 = called state" using c_same(3)[OF Continue(1,2)] by simp
    then have x_in_c1: "x ∈ called state1" using Iterate.prems(2) by simp

    have inv: "well_infl_stabl (state1⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
      apply (rule destab_upd_locale_preserves_well_infl_stabl[OF Continue(4)])
      using conjunct1[OF well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) inv]]
      unfolding well_infl_stabl_def
      by auto
    have eq_equal_sides_subsumed_2:
        "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - (called state1 - {x}))"
      apply (rule destab_upd_locale_preserves_part_solution[OF Continue(4)])
      using IH well_infl_stabl_1 x_in_c1 by simp+

    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6), simplified,
              OF x_in_c1 inv eq_equal_sides_subsumed_2]

    then show ?thesis by simp
  qed
next
  case (Repeat x state)
  have inv: "well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: well_infl_stabl_simp_c_stabl)
  have eq_equal_sides_subsumed:
    "eq_equal_sides_subsumed T (σ (state⦇stabl := insert x (stabl state)⦈))
      (stabl (state⦇stabl := insert x (stabl state)⦈) - called (state⦇stabl := insert x (stabl state)⦈))"
    using Repeat.prems(2,4) by simp

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2) inv eq_equal_sides_subsumed, of "[]", simplified,
        OF Repeat.prems(2)]

    have "called state1 = called state"
      using c_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have inv1: "well_infl_stabl state1"
      using well_infl_stabl_ind(4)[OF Unstable(1,2) inv, of "[]", simplified, OF Repeat.prems(2)]
      by simp

    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5) x_in_c1 inv1 conjunct1[OF IH],
        of d1, simplified]

    then show ?thesis by simp
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2) inv eq_equal_sides_subsumed, of "[]", simplified,
        OF Repeat.prems(2)]
    then show ?thesis using Stable(3) by simp
  qed
next
  case (Eval x t state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,2,4) Eval.prems(2,3)]
    note well_infl_stabl_1 = well_infl_stabl_ind(1)[OF QueryL(3,4) Eval.prems(2)]

    have prefix_recorded_in_infl:
      "∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p" if "x ∈ stabl state"
      using Eval.prems(5) that by simp

    have prefix_no_indirect_side: "{p. Inl p ∈ set pre}
          ⊆ {u. ∃x ∈ called state ∩ stabl state1. x ∈ slookup (infl state) u}"
        if "x ∈ stabl state1"
      using lookup_in_influenced that called_non_stabl_increasing(1)[OF QueryL(3,4)] Eval.prems(4)
        prefix_recorded_in_infl
      by fastforce

    have prefix_recorded_in_infl':
      "∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inl y)])}. x ∈ slookup (infl state1) p"
      if "x ∈ stabl state1"
    proof -
      have "∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state1) p"
        using prefix_recorded_in_infl called_non_stabl_increasing(1)[OF QueryL(3,4)] that
          Eval.prems(4) well_infl_stabl_1 prefix_no_indirect_side by fastforce
      then show ?thesis using well_infl_stabl_1 by auto
    qed
    have prefix: "x ∈ stabl state1 ⟶
      (subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state1) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inl y)])}. x ∈ slookup (infl state1) p)
      ∧ (∀(u,ud) ∈ {s. Inr s ∈ set (pre @ [Inl (Inl y)])}. ud ≤ (σ state1) (Inr u)))"
    proof (intro impI, goal_cases)
      case 1
      have "x ∈ stabl state"
        using 1 called_non_stabl_increasing(1)[OF QueryL(3,4)] Eval.prems(4) by auto
      then have pre0: "subt_for_prefix (T x) pre (σ state) = Some t"
        using Eval.prems(5) by simp
      then have pre1: "subt_for_prefix (T x) pre (σ state1) = Some t"
        apply (subst subt_for_prefix_same[of pre "σ state1" "σ state" "T x"])
        subgoal using 1 prefix_no_indirect_side well_infl_stabl_1  by fastforce
        subgoal by simp
        done
      have pre_sides_subsumed:
        "∀(u, ud)∈{s. Inr s ∈ set pre}. ud ≤ (σ state1) (Inr u)"
      proof -
        have "∀(u, ud) ∈ {s. Inr s ∈ set pre}. ud ≤ (σ state) (Inr u)"
          using Eval.prems(5) ‹x ∈ stabl state› by simp
        moreover have
          "∀(u, ud) ∈ {s. Inr s ∈ set pre}. (σ state) (Inr u) ≤ (σ state1) (Inr u)"
          using increasing_values_for_globals(1)[OF QueryL(3,4)] by simp
        ultimately show ?thesis using order.trans by fastforce
      qed
      show ?case
        using pre1 QueryL(2,7) prefix_recorded_in_infl' 1 pre_sides_subsumed
          subt_for_prefix_transitive[of "T x" pre "σ state1" t "[Inl (Inl y)]" "g yd"]
        by auto
    qed

    have "called state1 = called state" using c_same(1)[OF QueryL(3,4)] by simp
    then have "x ∈ called state1" using Eval.prems(4) by simp
    have "called state' = called state1" using c_same(4)[OF QueryL(5,6)] by simp

    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6) conjunct1[OF well_infl_stabl_1] IH
        ‹x ∈ called state1› prefix, simplified]

    then show ?thesis using ih by simp
  next
    case (QueryG y g yd)
    have inv: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2)
      unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    have prefix: "x ∈ stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈) ⟶ (
        subt_for_prefix (T x) (pre @ [Inl (Inr y)])
        (σ (state⦇infl := fminsert (infl state) (Inr y) x⦈)) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inr y)])}. x ∈ slookup
        (infl (state⦇infl := fminsert (infl state) (Inr y) x⦈)) p)
      ∧ (∀(u, ud) ∈ {s. Inr s ∈ set (pre @ [Inl (Inr y)])}.
        ud ≤ (σ (state⦇infl := fminsert (infl state) (Inr y) x⦈)) (Inr u)))"
      using Eval.prems(5) QueryG(2,3) subt_for_prefix_transitive[of "T x" pre _ t "[Inl (Inr y)]"]
      by (simp add: fminsert_def fmlookup_default_def)

    note IH = Eval.IH(4)[OF QueryG(1-3,5) inv _ _ prefix, simplified, OF Eval.prems(3,4)]

    then show ?thesis using IH by simp
  next
    case (Side_Subsumed y yd d' t1)
    have "yd ≤ (σ state) (Inr y)"
      using Side_Subsumed(3,4) sup_ge2[of yd d'] by simp
    then have prefix: "x ∈ stabl state ⟶
      (subt_for_prefix (T x) (pre @ [Inr (y, yd)]) (σ state) = Some t1
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inr (y, yd)])}. x ∈ slookup (infl state) p)
      ∧ (∀(u, ud) ∈ {s. Inr s ∈ set (pre @ [Inr (y, yd)])}. ud ≤ (σ state) (Inr u)))"
      using Eval.prems(5) subt_for_prefix_transitive[of "T x" pre _ t "[Inr (y, yd)]" t1]
        Side_Subsumed(2)
      by simp

    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6) Eval.prems(2-4) prefix]

    show ?thesis using IH by simp
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    have inv: "well_infl_stabl (state ⦇infl := infl1, stabl := stabl1,
        σ := (σ state)(Inr y := d')⦈)"
      using destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5) Eval.prems(2)] by simp
    have x_stabl_if_stabl1: "x ∈ stabl state" if "x ∈ stabl1"
      using that destab_opt_infl_stabl_relation[OF Side_Effect(5)] by simp

    have prefix_recorded_in_infl:
      "∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p" if "x ∈ stabl state"
      using Eval.prems(5) that by simp

    have y_not_in_prefix: "Inl (Inr y) ∉ set pre" if "x ∈ stabl1"
    proof (rule ccontr, goal_cases)
      case 1
      then have "x ∈ slookup (infl state) (Inr y)"
        using prefix_recorded_in_infl that x_stabl_if_stabl1 by simp
      then have "x ∈ influenced_by_cutoff (infl state) (Inr y) (Inl ` called state - {Inr y})"
        using lookup_in_influenced_cutoff by fastforce
      then show ?case using that destab_opt_infl_stabl_relation[OF Side_Effect(5)] by simp
    qed

    have prefix: "x ∈ stabl1 ⟶
      subt_for_prefix (T x) (pre @ [Inr (y, yd)]) ((σ state)(Inr y := d')) = Some t1 ∧
      (∀p. Inl p ∈ set (pre @ [Inr (y, yd)]) ⟶ x ∈ slookup infl1 p) ∧
      (∀a b. Inr (a, b) ∈ set (pre @ [Inr (y, yd)]) ⟶ b ≤ ((σ state)(Inr y := d')) (Inr a))"
    proof (intro impI, goal_cases)
      case 1
      then have "x ∈ stabl state" using x_stabl_if_stabl1 by simp
      show ?case using Eval.prems(5)[rule_format, OF ‹x ∈ stabl state›]
      proof (intro conjI impI allI, goal_cases)
        case 1
        then show ?case
          apply (intro subt_for_prefix_transitive[where ?t2.0=t])
          subgoal
            apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
            by (auto simp add: ‹x ∈ stabl1› fun_upd_def y_not_in_prefix)
          subgoal using Side_Effect(2) by simp
          done
      next
        case (2 p)
        then show ?case using influencing_stabl_after_destab'[OF Side_Effect(5) _ 1] by simp
      next
        case (3 a b)
        then show ?case
          by (auto intro: order.trans[OF _ sup_ge1] simp add: Side_Effect(3) fun_upd_def)
      qed
    qed

    have eq_equal_sides_subsumed_1:
      "eq_equal_sides_subsumed T ((σ state)(Inr y := d')) (stabl1 - called state)"
      using destab_upd_globale_preserves_part_solution[OF Side_Effect(5) Eval.prems(3,2)
          Side_Effect(3)]
      by simp

    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7) inv, simplified,
        OF eq_equal_sides_subsumed_1 Eval.prems(4) prefix]

    then show ?thesis by simp
  next
    case Answer
    have "eq T x (σ state') = xd" if "x ∈ stabl state'"
    proof -
      have "subt_for_prefix (T x) pre (σ state) = Some t"
        using Eval.prems(5) Answer(3) that by simp
      then have "eq T x (σ state) = xd"
        using subt_for_prefix_Answer_eq_traverse Answer(2) by blast
      then show ?thesis using Answer(3) by simp
    qed
    moreover have "sides_of_rhs (T x) (σ state') ≤ σ state'" if "x ∈ stabl state'"
    proof -
      have "subt_for_prefix (T x) pre (σ state) = Some (Answer xd)"
        using Eval.prems(5) Answer that by simp
      then show ?thesis using subt_for_prefix_Answer_subsumes Eval.prems(5) that Answer(3) by blast
    qed
    ultimately show ?thesis using Eval.prems(3) Answer(3) by simp
  next
    case Abort
    then show ?thesis using Eval.prems(3) by force
  qed
qed

theorem partial_solution:
  assumes "solve_dom x"
      and "solve x = (st, sigma)"
    shows "part_solution T x sigma st"
proof -
  obtain d state where
    iterate: "(d, state) = iterate x (init_state ⦇ called := insert x (called init_state) ⦈)"
    and st: "st = stabl state" and sigma: "sigma = σ state"
    using assms(2) unfolding solve_def by (auto split: prod.splits)
  have c_empty: "called state = {}"
    using c_same(2)[OF assms(1)[unfolded solve_dom_def] iterate]
    unfolding init_state_def
    by simp
  have well_init: "well_infl_stabl (init_state⦇called := called init_state - {x}⦈)"
    unfolding init_state_def well_infl_stabl_def fmlookup_default_def
    by simp
  then have well_result_state: "well_infl_stabl (state⦇called := called state - {x}⦈)"
    and x_stabl: "x ∈ stabl state"
    using well_infl_stabl_ind(2)[OF assms(1)[unfolded solve_dom_def] iterate]
    by auto
  moreover have "eq_equal_sides_subsumed T (σ state) (stabl state)"
    using eq_equal_sides_subsumed_ind(2)[OF assms(1)[unfolded solve_dom_def] iterate] c_empty
      well_init
    unfolding init_state_def
    by simp
  moreover have "∀u ∈ stabl state. dep⇩L T (σ state) u ⊆ stabl state"
    using well_infl_stabl_implies_stabl_c_closed[OF well_result_state] c_empty
    unfolding well_infl_stabl_def dep⇩L_def
    by simp
  ultimately show ?thesis using x_stabl st sigma by simp
qed

end ―‹end of context TD_side_opt›


subsection ‹Least Partial Post-Solution with Monotonicity and Abort for Optimized Solver›

locale TD_side_mono = TD_side_opt True T for
  T :: "'x ⇒ ('x, 'g, 'd :: bounded_semilattice_sup_bot) strategy_tree" +
  assumes mono_eq: "is_mono_eq T"
    and mono_sides: "mono_sides T"
    and mono_deps: "mono_deps T"
begin

subsubsection ‹Increasing Sigma and Upper Bound for Locales›

abbreviation locales_upper_bound :: "('x,'g,'d) state ⇒ bool" where
  "locales_upper_bound state ≡ ∀ξ. (σ state) (Inl ξ) ≤ eq T ξ (σ state)"

lemma locales_upper_bound_ind:
  shows "query_dom x y state
    ⟹ (yd, state') = query x y state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ locales_upper_bound state'"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {x}))
    ⟹ locales_upper_bound state
    ⟹ locales_upper_bound state'"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ locales_upper_bound state'"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ locales_upper_bound state'"
proof(induction x y state and x state and x state and x t state
    arbitrary: yd state' and xd state' and xd state' and xd state'
    rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state)
  show ?case using Query.IH(1) Query.prems(1)
  proof (cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    have well_infl_stabl: "well_infl_stabl (state⦇called := called state - {y}⦈)"
      using Query.prems(2) Iterate(5) by auto
    have eq_equal_sides_subsumed:
      "eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {y}))"
      using Query.prems(3) Iterate(5) by simp
    note IH = Query.IH(2)[OF Iterate(5,2), simplified, OF well_infl_stabl eq_equal_sides_subsumed
        Query.prems(4)]
    then show ?thesis by (simp add: Iterate(3))
  next
    case Lookup
    then show ?thesis using Query.prems(2-4) by auto
  qed
next
  case (Iterate x state)
  have well_infl_stabl: "well_infl_stabl state"
    using well_infl_stabl_simp_add_to_c[OF Iterate.prems(3)] by simp
  have eq_equal_sides_subsumed: "eq_equal_sides_subsumed T (σ state) (stabl state - called state)"
    using Iterate.prems(4) by simp
  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Iterate.prems(5) by simp
  next
    case (Fixpoint state1)
    note IH = Iterate.IH(2)[OF Fixpoint(4,2) Iterate.prems(2) well_infl_stabl
        eq_equal_sides_subsumed Iterate.prems(5)]
    have "x ∈ stabl state1"
      using well_infl_stabl_ind(3)[OF Fixpoint(1,2) Iterate.prems(2) well_infl_stabl] by simp
    then show ?thesis using IH by (auto simp add: Fixpoint(5))
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = Iterate.IH(2)[OF Continue(7,2) Iterate.prems(2) well_infl_stabl
        eq_equal_sides_subsumed Iterate.prems(5)]
    note well_infl_stabl_1 =
      well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]
    note eq_equal_sides_subsumed_1 = eq_equal_sides_subsumed_ind(3)[OF Continue(1,2)
        Iterate.prems(2) well_infl_stabl eq_equal_sides_subsumed]

    have x_in_c1: "x ∈ called state1" using c_same(3)[OF Continue(1,2)] Iterate.prems(2) by simp
    have well_infl_stabl_2: "well_infl_stabl (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
      apply (rule destab_upd_locale_preserves_well_infl_stabl[OF Continue(4)])
      using conjunct1[OF well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]]
      unfolding well_infl_stabl_def
      by auto
    have eq_equal_sides_subsumed_2:
      "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - (called state1 - {x}))"
      apply (rule destab_upd_locale_preserves_part_solution[OF Continue(4)])
      using IH well_infl_stabl_1 eq_equal_sides_subsumed_1 x_in_c1 by simp+

    have "σ state1 ≤ (σ state1)(Inl x := xd_new)"
    proof -
      have "eq T x (σ state1) = xd_new" using eq_equal_sides_subsumed_1 by simp
      moreover have "σ state1 (Inl x) ≤ eq T x (σ state1)" using IH by simp
      ultimately have "σ state1 (Inl x) ≤ xd_new" by simp
      then show ?thesis
        apply (intro le_funI)
        subgoal for a
          by (cases "a = Inl x") (auto simp add: fun_upd_same fun_upd_other)
        done
    qed
    then have "eq T z (σ state1) ≤ eq T z ((σ state1)(Inl x := xd_new))" for z
      using mono_eq unfolding is_mono_eq_def by blast
    then have inv_2:
        "∀ξ. ((σ state1)(Inl x := xd_new)) (Inl ξ) ≤ eq T ξ ((σ state1)(Inl x := xd_new))"
      apply (intro allI)
      subgoal for y
        apply (cases "x = y")
        subgoal
          using eq_equal_sides_subsumed_1 by (auto simp add: fun_upd_same)
        subgoal
          using IH
          by (auto intro: order_trans[of _ "eq T y (σ state1)"] simp add: fun_upd_other)
        done
      done

    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6), simplified, OF x_in_c1
        well_infl_stabl_2 eq_equal_sides_subsumed_2 inv_2]

    show ?thesis
      using IH ih ‹σ state1 ≤ (σ state1)(Inl x := xd_new)› order.trans
      by meson
  qed
next
  case (Repeat x state)
  have well_infl_stabl: "well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: well_infl_stabl_simp_c_stabl)
  have eq_equal_sides_subsumed:
    "eq_equal_sides_subsumed T (σ (state⦇stabl := insert x (stabl state)⦈))
      (stabl (state⦇stabl := insert x (stabl state)⦈) - called (state⦇stabl := insert x (stabl state)⦈))"
    using Repeat.prems(2,4) by simp
  have inv: "locales_upper_bound (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(5) by simp

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2) well_infl_stabl eq_equal_sides_subsumed inv]

    have "called state1 = called state"
      using c_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have well_infl_stabl_1: "well_infl_stabl state1"
      using well_infl_stabl_ind(4)[OF Unstable(1,2) well_infl_stabl, of "[]", simplified,
          OF Repeat.prems(2)]
      by simp
    note part_sol_1 = eq_equal_sides_subsumed_ind(4)[OF Unstable(1,2) well_infl_stabl, of "[]",
        simplified, OF Repeat.prems(4,2)]
    have inv_1: "locales_upper_bound state1" using IH by simp

    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5) x_in_c1 well_infl_stabl_1
        conjunct1[OF part_sol_1] inv_1, of d1, simplified]

    then show ?thesis using IH order.trans by fastforce
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2) well_infl_stabl eq_equal_sides_subsumed inv]
    then show ?thesis using Stable(3) by simp
  qed
next
  case (Eval x t state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,2,4) Eval.prems(2-4)]
    note well_infl_stabl_1 = well_infl_stabl_ind(1)[OF QueryL(3,4) Eval.prems(2)]
    note part_sol_1 = eq_equal_sides_subsumed_ind(1)[OF QueryL(3,4) Eval.prems(2,3)]
    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6) conjunct1[OF well_infl_stabl_1] part_sol_1
      IH, simplified]
    show ?thesis using QueryL IH ih by (auto simp add: Un_assoc)
  next
    case (QueryG y g yd)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    note IH = Eval.IH(4)[OF QueryG(1-3) QueryG(5), simplified, OF well_infl_stabl Eval.prems(3,4)]
    show ?thesis using IH by simp
  next
    case (Side_Subsumed y yd d' t1)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6) Eval.prems(2-4)]
    show ?thesis using IH by simp
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    have well_infl_stabl:
      "well_infl_stabl (state⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
      using destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5) Eval.prems(2)] by simp
    have eq_equal_sides_subsumed:
      "eq_equal_sides_subsumed T ((σ state)(Inr y := d')) (stabl1 - called state)"
      using destab_upd_globale_preserves_part_solution Side_Effect(3,5) Eval.prems(3,2) by blast
    have inv: "locales_upper_bound (state⦇infl := infl1, stabl := stabl1,
      σ := (σ state)(Inr y := d')⦈)"
      apply (intro allI)
      subgoal for z
      proof -
        have "σ state ≤ (σ state)(Inr y := d')"
          apply (intro le_funI)
          subgoal for z
            apply (cases "Inr y = z")
            by (auto simp add: Side_Effect(3) fun_upd_same fun_upd_other)
          done
        then have "eq T z (σ state) ≤ eq T z ((σ state)(Inr y := d'))"
          using mono_eq unfolding is_mono_eq_def by blast
        moreover have "σ state (Inl z) ≤ eq T z (σ state)" using Eval.prems(4) by blast
        ultimately show ?thesis by (auto simp add: fun_upd_other)
      qed
      done
    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7) well_infl_stabl _ inv, simplified,
        OF eq_equal_sides_subsumed]
    have "σ state ≤ (σ state)(Inr y := d')"
      using Side_Effect(3)
      apply (intro le_funI)
      subgoal for a
        by (cases "a = Inr y") (auto simp add: fun_upd_same fun_upd_other)
      done
    then show ?thesis using IH order.trans by blast
  next
    case (Abort)
    then show ?thesis using Eval.prems(4) by fast
  next
    case Answer
    then show ?thesis using Eval.prems(4) by simp
  qed
qed


lemma increasing_sigma:
  shows "query_dom x y state
    ⟹ (yd, state') = query x y state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ σ state ≤ σ state'"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {x}))
    ⟹ locales_upper_bound state
    ⟹ σ state ≤ σ state'"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ σ state ≤ σ state'"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ σ state ≤ σ state'"
proof(induction x y state and x state and x state and x t state
    arbitrary: yd state' and xd state' and xd state' and xd state'
    rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state)
  show ?case using Query.IH(1) Query.prems(1)
  proof (cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    have well_infl_stabl: "well_infl_stabl (state⦇called := called state - {y}⦈)"
      using Query.prems(2) Iterate(5) by auto
    have eq_equal_sides_subsumed:
      "eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {y}))"
      using Query.prems(3) Iterate(5) by simp
    note IH = Query.IH(2)[OF Iterate(5,2), simplified, OF well_infl_stabl eq_equal_sides_subsumed
        Query.prems(4)]
    then show ?thesis by (simp add: Iterate(3))
  next
    case Lookup
    then show ?thesis using Query.prems(2-4) by auto
  qed
next
  case (Iterate x state)
  have well_infl_stabl: "well_infl_stabl state"
    using well_infl_stabl_simp_add_to_c[OF Iterate.prems(3)] by simp
  have eq_equal_sides_subsumed: "eq_equal_sides_subsumed T (σ state) (stabl state - called state)"
    using Iterate.prems(4) by simp
  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Iterate.prems(5) by simp
  next
    case (Fixpoint state1)
    note IH = Iterate.IH(2)[OF Fixpoint(4,2) Iterate.prems(2) well_infl_stabl
        eq_equal_sides_subsumed Iterate.prems(5)]
    have "x ∈ stabl state1"
      using well_infl_stabl_ind(3)[OF Fixpoint(1,2) Iterate.prems(2) well_infl_stabl] by simp
    then show ?thesis using IH by (auto simp add: Fixpoint(5))
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = Iterate.IH(2)[OF Continue(7,2) Iterate.prems(2) well_infl_stabl
        eq_equal_sides_subsumed Iterate.prems(5)]
    note well_infl_stabl_1 =
      well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]
    note eq_equal_sides_subsumed_1 = eq_equal_sides_subsumed_ind(3)[OF Continue(1,2)
        Iterate.prems(2) well_infl_stabl eq_equal_sides_subsumed]
    note locales_upper_bound_1 = locales_upper_bound_ind(3)[OF Continue(1,2) Iterate.prems(2)
        well_infl_stabl eq_equal_sides_subsumed Iterate.prems(5)]

    have x_in_c1: "x ∈ called state1" using c_same(3)[OF Continue(1,2)] Iterate.prems(2) by simp
    have well_infl_stabl_2: "well_infl_stabl (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
      apply (rule destab_upd_locale_preserves_well_infl_stabl[OF Continue(4)])
      using conjunct1[OF well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]]
      unfolding well_infl_stabl_def
      by auto
    have eq_equal_sides_subsumed_2:
      "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - (called state1 - {x}))"
      apply (rule destab_upd_locale_preserves_part_solution[OF Continue(4)])
      using IH well_infl_stabl_1 eq_equal_sides_subsumed_1 x_in_c1 by simp+

    have "σ state1 ≤ (σ state1)(Inl x := xd_new)"
    proof -
      have "eq T x (σ state1) = xd_new" using eq_equal_sides_subsumed_1 by simp
      moreover have "σ state1 (Inl x) ≤ eq T x (σ state1)"
        using locales_upper_bound_1 by simp
      ultimately have "σ state1 (Inl x) ≤ xd_new" by simp
      then show ?thesis
        apply (intro le_funI)
        subgoal for a
          by (cases "a = Inl x") (auto simp add: fun_upd_same fun_upd_other)
        done
    qed
    then have "eq T z (σ state1) ≤ eq T z ((σ state1)(Inl x := xd_new))" for z
      using mono_eq unfolding is_mono_eq_def by blast
    then have inv_2:
        "∀ξ. ((σ state1)(Inl x := xd_new)) (Inl ξ) ≤ eq T ξ ((σ state1)(Inl x := xd_new))"
      apply (intro allI)
      subgoal for y
        apply (cases "x = y")
        subgoal
          using eq_equal_sides_subsumed_1 by (auto simp add: fun_upd_same)
        subgoal
          using IH locales_upper_bound_1
          by (auto intro: order_trans[of _ "eq T y (σ state1)"] simp add: fun_upd_other)
        done
      done

    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6), simplified, OF x_in_c1
        well_infl_stabl_2 eq_equal_sides_subsumed_2 inv_2]

    show ?thesis
      using IH ih ‹σ state1 ≤ (σ state1)(Inl x := xd_new)› order.trans
      by meson
  qed
next
  case (Repeat x state)
  have well_infl_stabl: "well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: well_infl_stabl_simp_c_stabl)
  have eq_equal_sides_subsumed:
    "eq_equal_sides_subsumed T (σ (state⦇stabl := insert x (stabl state)⦈))
      (stabl (state⦇stabl := insert x (stabl state)⦈) - called (state⦇stabl := insert x (stabl state)⦈))"
    using Repeat.prems(2,4) by simp
  have inv: "locales_upper_bound (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(5) by simp

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2) well_infl_stabl eq_equal_sides_subsumed inv]

    have "called state1 = called state"
      using c_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have well_infl_stabl_1: "well_infl_stabl state1"
      using well_infl_stabl_ind(4)[OF Unstable(1,2) well_infl_stabl, of "[]", simplified,
          OF Repeat.prems(2)]
      by simp
    note part_sol_1 = eq_equal_sides_subsumed_ind(4)[OF Unstable(1,2) well_infl_stabl, of "[]",
        simplified, OF Repeat.prems(4,2)]
    have locales_upper_bound_1: "locales_upper_bound state1"
      using locales_upper_bound_ind(4)[OF Unstable(1,2) well_infl_stabl eq_equal_sides_subsumed]
        Repeat.prems(5) by simp

    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5) x_in_c1 well_infl_stabl_1
        conjunct1[OF part_sol_1] locales_upper_bound_1, of d1, simplified]

    then show ?thesis using IH order.trans by fastforce
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2) well_infl_stabl eq_equal_sides_subsumed inv]
    then show ?thesis using Stable(3) by simp
  qed
next
  case (Eval x t state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,2,4) Eval.prems(2-4)]
    note well_infl_stabl_1 = well_infl_stabl_ind(1)[OF QueryL(3,4) Eval.prems(2)]
    note part_sol_1 = eq_equal_sides_subsumed_ind(1)[OF QueryL(3,4) Eval.prems(2,3)]
    note locales_upper_bound_1 = locales_upper_bound_ind(1)[OF QueryL(3,4) Eval.prems(2,3,4)]
    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6) conjunct1[OF well_infl_stabl_1] part_sol_1
      locales_upper_bound_1, simplified]
    have "σ state ≤ σ state'" using IH ih unfolding map_le_def
      by (meson dual_order.trans)
    then show ?thesis
      using QueryL IH ih by (auto simp add: Un_assoc)
  next
    case (QueryG y g yd)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    note IH = Eval.IH(4)[OF QueryG(1-3) QueryG(5), simplified, OF well_infl_stabl Eval.prems(3,4)]
    show ?thesis using IH by simp
  next
    case (Side_Subsumed y yd d' t1)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6) Eval.prems(2-4)]
    show ?thesis using IH by simp
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    have well_infl_stabl:
      "well_infl_stabl (state⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
      using destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5) Eval.prems(2)] by simp
    have eq_equal_sides_subsumed:
      "eq_equal_sides_subsumed T ((σ state)(Inr y := d')) (stabl1 - called state)"
      using destab_upd_globale_preserves_part_solution Side_Effect(3,5) Eval.prems(3,2) by blast
    have inv: "locales_upper_bound (state⦇infl := infl1, stabl := stabl1,
      σ := (σ state)(Inr y := d')⦈)"
      apply (intro allI)
      subgoal for z
      proof -
        have "σ state ≤ (σ state)(Inr y := d')"
          apply (intro le_funI)
          subgoal for z
            apply (cases "Inr y = z")
            by (auto simp add: Side_Effect(3) fun_upd_same fun_upd_other)
          done
        then have "eq T z (σ state) ≤ eq T z ((σ state)(Inr y := d'))"
          using mono_eq unfolding is_mono_eq_def by blast
        moreover have "σ state (Inl z) ≤ eq T z (σ state)" using Eval.prems(4) by blast
        ultimately show ?thesis by (auto simp add: fun_upd_other)
      qed
      done
    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7) well_infl_stabl _ inv, simplified,
        OF eq_equal_sides_subsumed]
    have "σ state ≤ (σ state)(Inr y := d')"
      using Side_Effect(3)
      apply (intro le_funI)
      subgoal for a
        by (cases "a = Inr y") (auto simp add: fun_upd_same fun_upd_other)
      done
    then show ?thesis using IH order.trans by blast
  next
    case (Abort)
    then show ?thesis using Eval.prems(4) by fast
  next
    case Answer
    then show ?thesis using Eval.prems(4) by simp
  qed
qed

subsubsection ‹Least Partial Solution›

lemma mono_trans_dep⇩L: "sigma1 ≤ sigma2 ⟹ trans_dep⇩L T sigma1 x ⊆ trans_dep⇩L T sigma2 x"
proof
  fix u
  assume A: "sigma1 ≤ sigma2" "u ∈ trans_dep⇩L T sigma1 x"
  have "(x, u) ∈ trans_dep⇩L_rel T sigma1" using A(2) by blast
  then have "(x, u) ∈ trans_dep⇩L_rel T sigma2"
  proof (induction rule: trancl.induct)
    case (r_into_trancl u d)
    then have "d ∈ dep⇩L T sigma2 u" using mono_deps A(1) unfolding mono_deps_def dep⇩L_def by auto
    then show ?case by blast
  next
    case (trancl_into_trancl v u d)
    then have "d ∈ dep⇩L T sigma2 u" using mono_deps A(1) unfolding mono_deps_def dep⇩L_def by auto
    then have "(u,d) ∈ trans_dep⇩L_rel T sigma2" by blast
    then show ?case using trancl_into_trancl(3) by simp
  qed
  then show "u ∈ trans_dep⇩L T sigma2 x" by blast
qed

abbreviation less_than_least :: "'x ⇒ ('x, 'g, 'd) state ⇒ bool" where
  "less_than_least x state ≡
    (∀σl varsl. part_post_solution T x σl varsl ⟶ σ state ≤ σl ∧ stabl state ⊆ varsl)"

lemma less_than_part_post_solution_ind:
  shows "query_dom x y state
    ⟹ (yd, state') = query x y state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ less_than_least z state
    ⟹ y ∈ insert z (trans_dep⇩L T (σ state) z)
    ⟹ less_than_least z state'"
    and "iterate_dom x state
    ⟹ (xd, state') = iterate x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {x}))
    ⟹ locales_upper_bound state
    ⟹ less_than_least z state
    ⟹ x ∈ insert z (trans_dep⇩L T (σ state) z)
    ⟹ less_than_least z state'"
    and "repeat_dom x state
    ⟹ (xd, state') = repeat x state
    ⟹ x ∈ called state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ less_than_least z state
    ⟹ x ∈ insert z (trans_dep⇩L T (σ state) z)
    ⟹ less_than_least z state'"
    and "eval_dom x t state
    ⟹ (xd, state') = eval x t state
    ⟹ well_infl_stabl state
    ⟹ eq_equal_sides_subsumed T (σ state) (stabl state - called state)
    ⟹ locales_upper_bound state
    ⟹ x ∈ called state
    ⟹ less_than_least z state
    ⟹ x ∈ insert z (trans_dep⇩L T (σ state) z)
    ⟹ x ∈ stabl state ⟶ (subt_for_prefix (T x) pre (σ state) = Some t
        ∧ (∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p))
    ⟹ less_than_least z state'"
proof(induction x y state and x state and x state and x t state
    arbitrary: yd state' and xd state' and xd state' and xd state' pre
    rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state)
  show ?case using Query.IH(1) Query.prems(1)
  proof (cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    have well_infl_stabl: "well_infl_stabl (state⦇called := called state - {y}⦈)"
      using Query.prems(2) Iterate(5) by auto
    have part_sol: "eq_equal_sides_subsumed T (σ state) (stabl state - (called state - {y}))"
      using Query.prems(3) Iterate(5) by simp
    have stabl_subset_P: "y ∈ insert z (trans_dep⇩L T (σ (state⦇called := insert y (called state)⦈)) z)"
      using Query.prems(6) Iterate(3) by simp
    have less_than: "less_than_least z (state⦇called := insert y (called state)⦈)"
      using Query.prems(5) by auto
    note IH = Query.IH(2)[OF Iterate(5,2) _ _ _ _ less_than stabl_subset_P, simplified,
        OF well_infl_stabl part_sol Query.prems(4)]
    show ?thesis using IH by (auto simp add: Iterate(3))
  next
    case Lookup
    show ?thesis using Query.prems(5) Lookup(2) by auto
  qed
next
  case (Iterate x state)
  have well_infl_stabl: "well_infl_stabl state"
    using well_infl_stabl_simp_add_to_c[OF Iterate.prems(3)] by simp
  have part_sol: "eq_equal_sides_subsumed T (σ state) (stabl state - called state)"
    using Iterate.prems(4) by simp
  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    show ?thesis using Stable(1) Iterate.prems(6) by auto
  next
    case (Fixpoint state1)
    have "σ state1 ≤ σ state'"
      using Fixpoint(5) by simp
    have subset_P: "x ∈ insert z (trans_dep⇩L T (σ state) z)"
      using Iterate.prems(7)
      by (simp add: Fixpoint(5))
    note IH = Iterate.IH(2)[OF Fixpoint(4,2) Iterate.prems(2) well_infl_stabl part_sol
        Iterate.prems(5,6) subset_P]
    have "x ∈ stabl state1"
      using well_infl_stabl_ind(3)[OF Fixpoint(1,2) Iterate.prems(2) well_infl_stabl] by simp
    show ?thesis using IH by (auto simp add: Fixpoint(5))
  next
    case (Continue state1 xd_new infl2 stabl2)
    have x_in_c1: "x ∈ called state1" using c_same(3)[OF Continue(1,2)] Iterate.prems(2) by simp

    note well_infl_stabl_1 =
      well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]
    note part_sol_1 = eq_equal_sides_subsumed_ind(3)[OF Continue(1,2) Iterate.prems(2)
      well_infl_stabl part_sol]
    note incr_sigma_1 = increasing_sigma(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl
      part_sol Iterate.prems(5)]
    note locales_upper_bound_1 = locales_upper_bound_ind(3)[OF Continue(1,2) Iterate.prems(2)
      well_infl_stabl part_sol Iterate.prems(5)]

    have well_infl_stabl_2: "well_infl_stabl (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new), called := called state1 - {x}⦈)"
      apply (rule destab_upd_locale_preserves_well_infl_stabl[OF Continue(4)])
      using conjunct1[OF well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl]]
      unfolding well_infl_stabl_def
      by auto
    have eq_equal_sides_subsumed_2:
      "eq_equal_sides_subsumed T ((σ state1)(Inl x := xd_new)) (stabl2 - (called state1 - {x}))"
      apply (rule destab_upd_locale_preserves_part_solution[OF Continue(4)])
      using well_infl_stabl_1 part_sol_1 x_in_c1 by simp+

    have sigma_smaller_upd: "σ state1 ≤ (σ state1)(Inl x := xd_new)"
    proof -
      have "xd_new = eq T x (σ state1)" using part_sol_1 by simp
      then have "σ state1 (Inl x) ≤ xd_new" using locales_upper_bound_1 by simp
      then show ?thesis
        apply (intro le_funI)
        subgoal for a
          by (cases "a = Inl x") (auto simp add: fun_upd_same fun_upd_other)
        done
    qed

    have locales_ub_2: "locales_upper_bound (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new)⦈)"
    proof -
      have "eq T z (σ state1) ≤ eq T z ((σ state1)(Inl x := xd_new))" for z
        using sigma_smaller_upd mono_eq unfolding is_mono_eq_def by blast
      then show ?thesis
        apply (intro allI)
        subgoal for y
          apply (cases "x = y")
          subgoal
            using part_sol_1 by (auto simp add: fun_upd_same)
          subgoal
            using increasing_sigma(3)[OF Continue(1,2) Iterate.prems(2) well_infl_stabl part_sol
              Iterate.prems(5)] locales_upper_bound_1
            by (auto intro: order_trans[of _ "eq T y (σ state1)"] simp add: fun_upd_other)
          done
        done
    qed

    have "σ state1 ≤ σ state'"
      using increasing_sigma(2)[OF Continue(5,6) _ _ _ locales_ub_2, simplified,
          OF x_in_c1 well_infl_stabl_2 eq_equal_sides_subsumed_2] sigma_smaller_upd
      by auto
    then have subset_P: "x ∈ insert z (trans_dep⇩L T (σ state) z)"
      using Iterate.prems(7) mono_trans_dep⇩L
      by blast
    note IH = Iterate.IH(2)[OF Continue(7,2) Iterate.prems(2) well_infl_stabl part_sol
        Iterate.prems(5,6) subset_P]

    have less_inv_2: "less_than_least z (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new)⦈)"
    proof (intro allI impI)
      fix σl varsl y
      assume P: "part_post_solution T z σl varsl"
      have "(σ state1)(Inl x := xd_new) ≤ σl"
      proof (intro conjI le_funI, goal_cases)
        case (1 y)
        show ?case
        proof (cases "y = Inl x")
          case True
          have "σ state ≤ σl" using Iterate.prems(6) P by auto
          then have "x ∈ insert z (trans_dep⇩L T σl z)" using mono_trans_dep⇩L subset_P by blast
          then have x_varsl: "x ∈ varsl"
            using part_post_solution_implies_trans_dep_subsumed[of z] P by auto
          have "xd_new = eq T x (σ state1)" using part_sol_1 by auto
          moreover have "eq T x (σ state1) ≤ eq T x σl"
          proof -
            have "eq T x (σ state1) ≤ eq T x ((σ state1)(Inl x := xd_new))"
              using mono_eq ‹σ state1 ≤ (σ state1)(Inl x := xd_new)›
              unfolding is_mono_eq_def by blast
            moreover have "eq T x ((σ state1)(Inl x := xd_new)) ≤ eq T x σl"
            proof -
              have "σ state1 ≤ σl" using IH P by auto
              then have "eq T x (σ state1) ≤ eq T x σl"
                using mono_eq unfolding is_mono_eq_def by blast
              then have "xd_new ≤ eq T x σl" by (simp add: ‹xd_new = eq T x (σ state1)›)
              have "xd_new ≤ σl (Inl x)"
                using ‹xd_new ≤ eq T x σl› P x_varsl by auto
              then have "(σ state1)(Inl x := xd_new) ≤ σl"
                using ‹σ state1 ≤ σl›
                apply (intro le_funI)
                subgoal for a
                  by (cases "a = Inl x") (auto simp add: le_funD fun_upd_same fun_upd_other)
                done
              then show ?thesis using mono_eq unfolding is_mono_eq_def by blast
            qed
            ultimately show ?thesis by simp
          qed
          moreover have "eq T x σl ≤ σl (Inl x)"
            using P IH x_varsl by blast
          ultimately show ?thesis by (simp add: True fun_upd_same)
        next
          case False
          have "σ state1 ≤ σl" using IH P by blast
          then show ?thesis using False by (auto simp add: fun_upd_other le_fun_def)
        qed
      qed
      moreover have "stabl2 ⊆ varsl"
        using IH P destab_opt_infl_stabl_relation[OF Continue(4)] by blast
      ultimately show
        "σ (state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(Inl x := xd_new)⦈) ≤ σl
        ∧ stabl (state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(Inl x := xd_new)⦈) ⊆ varsl"
        by auto
    qed
    have "x ∈ insert z (trans_dep⇩L T (σ state1) z)"
      using Iterate.prems(7) mono_trans_dep⇩L[OF incr_sigma_1] by blast
    then have in_trans_dep: "x ∈ insert z (trans_dep⇩L T
          (σ (state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(Inl x := xd_new)⦈)) z)"
      using mono_trans_dep⇩L[OF ‹σ state1 ≤ (σ state1)(Inl x := xd_new)›]
      by auto

    note ih = Iterate.IH(3)[OF Continue(7,2) _ Continue(3,4) _ Continue(6) _ _ _ locales_ub_2
        less_inv_2 in_trans_dep, simplified, OF x_in_c1 well_infl_stabl_2 eq_equal_sides_subsumed_2]

    show ?thesis
      using IH ih ‹σ state1 ≤ (σ state1)(Inl x := xd_new)› order.trans
      by meson
  qed
next
  case (Repeat x state)
  have well_infl_stabl: "well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: well_infl_stabl_simp_c_stabl)
  have eq_equal_sides_subsumed:
    "eq_equal_sides_subsumed T (σ (state⦇stabl := insert x (stabl state)⦈))
      (stabl (state⦇stabl := insert x (stabl state)⦈) - called (state⦇stabl := insert x (stabl state)⦈))"
    using Repeat.prems(2,4) by simp
  have less_than: "less_than_least z (state⦇stabl := insert x (stabl state)⦈)"
  proof (intro allI impI, goal_cases)
    case (1 σl varsl)
    then have "σ state ≤ σl" using Repeat.prems(6) by auto
    have "insert z (trans_dep⇩L T σl z) ⊆ varsl"
      using part_post_solution_implies_trans_dep_subsumed[OF 1] 1 by simp
    then have "insert z (trans_dep⇩L T (σ state) z) ⊆ varsl"
      using ‹σ state ≤ σl› mono_trans_dep⇩L by blast
    then have "x ∈ varsl" using Repeat.prems(7) by blast
    then show ?case using Repeat.prems(6) 1 by auto
  qed
  have subset_trans: "x ∈ insert z (trans_dep⇩L T (σ (state⦇stabl := insert x (stabl state)⦈)) z)"
    using Repeat.prems(7) by simp

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)

    have "called state1 = called state"
      using c_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have well_infl_stabl_1: "well_infl_stabl state1"
      using well_infl_stabl_ind(4)[OF Unstable(1,2) well_infl_stabl, of "[]", simplified,
          OF Repeat.prems(2)]
      by simp
    note eq_equal_sides_subsumed_1 = eq_equal_sides_subsumed_ind(4)[OF Unstable(1,2)
        well_infl_stabl, of "[]", simplified, OF Repeat.prems(4,2)]
    have eq_equal_sides_subsumed:
      "eq_equal_sides_subsumed T (σ state) (insert x (stabl state) - called state)"
      using Repeat.prems(2,4) by simp
    note incr_sigma_1 = increasing_sigma(4)[OF Unstable(1,2) well_infl_stabl, simplified,
        OF eq_equal_sides_subsumed Repeat.prems(5)]
    note locales_upper_bound_1 = locales_upper_bound_ind(4)[OF Unstable(1,2) well_infl_stabl,
        simplified, OF eq_equal_sides_subsumed Repeat.prems(5)]
    note incr_sigma_2 = increasing_sigma(3)[OF Unstable(4,5) x_in_c1 well_infl_stabl_1
        conjunct1[OF eq_equal_sides_subsumed_1] locales_upper_bound_1]

    note IH = Repeat.IH(2)[OF Unstable(2) well_infl_stabl _ _ _ less_than subset_trans, of "[]",
        simplified, OF Repeat.prems(4,5,2)]

    have subset_trans_1: "x ∈ insert z (trans_dep⇩L T (σ state1) z)"
      using mono_trans_dep⇩L[OF incr_sigma_1] Repeat.prems(7) by blast
    note ih = Repeat.IH(3)[OF Unstable(2) _ Unstable(3,5) x_in_c1 well_infl_stabl_1
        conjunct1[OF eq_equal_sides_subsumed_1] locales_upper_bound_1 _ subset_trans_1,
        of d1, simplified, OF IH]

    show ?thesis using ih by auto
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2) well_infl_stabl eq_equal_sides_subsumed _ _ less_than
        subset_trans, of "[]", simplified, OF Repeat.prems(5,2)]
    then show ?thesis using Stable(3) by auto
  qed
next
  case (Eval x t state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    have "subt_for_prefix (T x) pre (σ state) = Some t" using Eval.prems(8) QueryL(1) by simp
    then have "subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state) = Some (g ((σ state) (Inl y)))"
      by (rule subt_for_prefix_transitive[where ?pre2.0="[Inl (Inl y)]"])
         (simp add: QueryL(2))
    then have y_dep_x: "y ∈ dep⇩L T (σ state) x"
      using subt_for_prefix_subset_dep[of "T x" "pre @ [Inl (Inl y)]" "σ state"]
      unfolding dep⇩L_def dep_def by auto
    note well_infl_stabl_1 = well_infl_stabl_ind(1)[OF QueryL(3,4) Eval.prems(2)]
    note locales_upper_bound_1 = locales_upper_bound_ind(1)[OF QueryL(3,4) Eval.prems(2,3,4)]
    note eq_equal_sides_subsumed_1 = eq_equal_sides_subsumed_ind(1)[OF QueryL(3,4) Eval.prems(2,3)]
    note incr_sigma_1 = increasing_sigma(1)[OF QueryL(3,4) Eval.prems(2-4)]
    have x_in_c1: "x ∈ called state1" using c_same(1)[OF QueryL(3,4)] Eval.prems(5) by simp
    note incr_sigma' = increasing_sigma(4)[OF QueryL(5,6) conjunct1[OF well_infl_stabl_1]
        eq_equal_sides_subsumed_1 locales_upper_bound_1]

    have "σ state ≤ σ state'" using incr_sigma' incr_sigma_1 by auto
    then have y_dep_x': "y ∈ dep⇩L T (σ state') x"
      using y_dep_x mono_deps unfolding mono_deps_def dep_def dep⇩L_def by auto
    have "y ∈ trans_dep⇩L T (σ state) x"
      using trancl.r_into_trancl y_dep_x by blast
    then have subset_trans: "y ∈ insert z (trans_dep⇩L T (σ state) z)"
      using Eval.prems(7) trancl_trans by fastforce

    note IH = Eval.IH(2)[OF QueryL(1,2,4) Eval.prems(2-4) Eval.prems(6) subset_trans]

    have prefix_no_indirect_side: "{p. Inl p ∈ set pre}
        ⊆ {u. ∃x ∈ called state ∩ stabl state1. x ∈ slookup (infl state) u}" if "x ∈ stabl state1"
      using that Eval.prems(5,8) QueryL(1) by blast

    have prefix: "x ∈ stabl state1 ⟶
      (subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state1) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inl y)])}. x ∈ slookup (infl state1) p))"
    proof (intro impI, goal_cases)
      case 1
      then have "x ∈ stabl state"
        using called_non_stabl_increasing(1)[OF QueryL(3,4)] Eval.prems(5) by blast
      show ?case using Eval.prems(8)[rule_format, OF ‹x ∈ stabl state›]
      proof (intro conjI impI, goal_cases)
        case 1
        then show ?case
          apply (intro subt_for_prefix_transitive[where ?t2.0=t])
          subgoal
            apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
            subgoal using prefix_no_indirect_side ‹x ∈ stabl state1› well_infl_stabl_1 by fastforce
            subgoal by simp
            done
          subgoal using QueryL(2,7) by simp
          done
      next
        case 2
        then show ?case
          using conjunct2[OF well_infl_stabl_1] prefix_no_indirect_side[OF 1] by fastforce
      qed
    qed

    have subset_trans_1: "x ∈ insert z (trans_dep⇩L T (σ state1) z)"
      using mono_trans_dep⇩L[OF incr_sigma_1] Eval.prems(7) by blast
    note ih = Eval.IH(3)[OF QueryL(1,2,4) _ QueryL(6) conjunct1[OF well_infl_stabl_1]
        eq_equal_sides_subsumed_1 locales_upper_bound_1 x_in_c1 IH subset_trans_1 prefix,
        simplified]
    then show ?thesis by auto
  next
    case (QueryG y g yd)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    have pre: "x ∈ stabl state ⟶
      subt_for_prefix (T x) (pre @ [Inl (Inr y)]) (σ state) = Some (g yd) ∧
      (∀p. Inl p ∈ set (pre @ [Inl (Inr y)]) ⟶ x ∈ slookup (fminsert (infl state) (Inr y) x) p)"
      using Eval.prems(8) QueryG(2,3) subt_for_prefix_transitive[of "T x" pre _ t "[Inl (Inr y)]"]
      by (simp add: fminsert_def fmlookup_default_def)
    have less_than: "less_than_least z (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(6) by auto
    have subset_trans:
      "x ∈ insert z (trans_dep⇩L T (σ (state⦇infl := fminsert (infl state) (Inr y) x⦈)) z)"
      using Eval.prems(7) by simp
    note IH = Eval.IH(4)[OF QueryG(1-3) QueryG(5) _ _ _ _ less_than subset_trans, simplified,
        OF well_infl_stabl Eval.prems(3-5) pre]
    show ?thesis using IH by auto
  next
    case (Side_Subsumed y yd d' t1)
    have well_infl_stabl: "well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding well_infl_stabl_def fmlookup_default_def fminsert_def
      by simp
    have pre: "x ∈ stabl state ⟶
      subt_for_prefix (T x) (pre @ [Inr (y,yd)]) (σ state) = Some t1 ∧
      (∀p∈{p. Inl p ∈ set (pre @ [Inr (y,yd)])}. x ∈ slookup (infl state) p)"
      using Eval.prems(8) subt_for_prefix_transitive[of "T x" pre _ t "[Inr (y, yd)]" t1]
        Side_Subsumed(2)
      by simp
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4,6) Eval.prems(2-7) pre]
    show ?thesis using IH by auto
  next
    case (Side_Effect y yd d' t1 infl1 stabl1)
    have well_infl_stabl:
      "well_infl_stabl (state⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
      using destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5) Eval.prems(2)] by simp
    have eq_equal_sides_subsumed:
      "eq_equal_sides_subsumed T ((σ state)(Inr y := d')) (stabl1 - called state)"
      using destab_upd_globale_preserves_part_solution Side_Effect(3,5) Eval.prems(3,2) by blast
    have locale_ub: "locales_upper_bound (state⦇infl := infl1, stabl := stabl1,
      σ := (σ state)(Inr y := d')⦈)"
      apply (intro allI)
      subgoal for z
      proof -
        have "σ state ≤ (σ state)(Inr y := d')"
          apply (intro le_funI)
          subgoal for z
            apply (cases "Inr y = z")
            by (auto simp add: Side_Effect(3) fun_upd_same fun_upd_other)
          done
        then have "eq T z (σ state) ≤ eq T z ((σ state)(Inr y := d'))"
          using mono_eq unfolding is_mono_eq_def by blast
        moreover have "σ state (Inl z) ≤ eq T z (σ state)" using Eval.prems(4) by blast
        ultimately show ?thesis by (auto simp add: fun_upd_other)
      qed
      done
    have less_inv:
      "less_than_least z (state⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)"
    proof (intro allI impI)
      fix σl varsl
      assume P: "part_post_solution T z σl varsl"
      then have "σ state ≤ σl" "stabl state ⊆ varsl" using Eval.prems(6) by auto
      moreover have "d' ≤ σl (Inr y)"
        apply (auto simp add: Side_Effect(3))
        subgoal using ‹σ state ≤ σl› by (simp add: le_funD)
        subgoal
        proof -
          have "yd ≤ sides_of_rhs (T x) (σ state) (Inr y)"
            using sides_of_rhs_helper[of "T x" pre "σ state" y yd t1] Eval.prems(8)
              Side_Effect(1,2)
            by blast
          moreover have "sides_of_rhs (T x) (σ state) (Inr y) ≤ sides_of_rhs (T x) σl (Inr y)"
            using ‹σ state ≤ σl› mono_sides unfolding mono_sides_def by (simp add: le_funD)
          moreover have "sides_of_rhs (T x) σl (Inr y) ≤ σl (Inr y)"
          proof -
            have "x ∈ insert z (trans_dep⇩L T σl z)"
              using Eval.prems(7) mono_trans_dep⇩L[OF ‹σ state ≤ σl›] by blast
            then have "x ∈ varsl"
              using part_post_solution_implies_trans_dep_subsumed[of z] P by blast
            then have "sides_of_rhs (T x) σl ≤ σl"
              using ‹part_post_solution T z σl varsl› Eval.prems(6)by blast
            then show ?thesis by (simp add: le_fun_def)
          qed
          ultimately show ?thesis
            using Eval.prems(6) ‹part_post_solution T z σl varsl› by auto
        qed
        done
      ultimately show "σ (state⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈) ≤ σl
        ∧ stabl (state⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈) ⊆ varsl"
        apply (intro conjI le_funI)
        subgoal for z
          by (cases "z = Inr y") (auto elim: le_funE simp add: fun_upd_same fun_upd_other)
        subgoal
          using destab_opt_infl_stabl_relation[OF Side_Effect(5)] by auto
        done
    qed

    (* Derive prefix for IH: *)
    have prefix_recorded_in_infl:
      "∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p" if "x ∈ stabl state"
      using Eval.prems(8) that by simp
    have y_not_in_prefix: "Inl (Inr y) ∉ set pre" if "x ∈ stabl1"
    proof (rule ccontr, goal_cases)
      case 1
      then have "x ∈ slookup (infl state) (Inr y)"
        using prefix_recorded_in_infl that Side_Effect(1) by simp
      then have "x ∈ influenced_by_cutoff (infl state) (Inr y) (Inl ` called state - {Inr y})"
        using lookup_in_influenced_cutoff by fast
      then show ?case using destab_opt_infl_stabl_relation[OF Side_Effect(5)] that by simp
    qed
    have pre: "x ∈ stabl1 ⟶
      subt_for_prefix (T x) (pre @ [Inr (y,yd)]) ((σ state)(Inr y := d')) = Some t1 ∧
      (∀p. Inl p ∈ set (pre @ [Inr (y,yd)]) ⟶ x ∈ slookup infl1 p)"
    proof
      assume A: "x ∈ stabl1"
      have P: "subt_for_prefix (T x) pre ((σ state)(Inr y := d')) = Some t"
        apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
        subgoal using y_not_in_prefix A by (simp add: fun_upd_apply)
        subgoal using Eval.prems(8) Side_Effect(1) A by simp
        done
      show "subt_for_prefix (T x) (pre @ [Inr (y, yd)]) ((σ state)(Inr y := d')) = Some t1 ∧
        (∀p. Inl p ∈ set (pre @ [Inr (y, yd)]) ⟶ x ∈ slookup infl1 p)"
        apply (intro conjI)
        apply (subst subt_for_prefix_transitive[OF P(1), of "[Inr (y, yd)]" t1])
        subgoal using Side_Effect(2) by simp
        subgoal by simp
        subgoal using destab_opt_infl_stabl_relation[OF Side_Effect(5)]
          by (metis A Inr_not_Inl Side_Effect(1,5) Un_iff equals0D influencing_stabl_after_destab'
              insert_iff list.simps(15) mem_Collect_eq prefix_recorded_in_infl set_append
              set_empty)
        done
    qed
    have "σ state ≤ (σ state)(Inr y := d')"
      apply (intro le_funI)
      subgoal for z
        apply (cases "z = Inr y")
        by (auto simp add: fun_upd_same fun_upd_other Side_Effect(3))
      done
    then have trans_dep_1: "x ∈ insert z (trans_dep⇩L T
      (σ (state⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d')⦈)) z)"
      using mono_trans_dep⇩L Eval.prems(7) by auto
    note IH = Eval.IH(6)[OF Side_Effect(1-5) _ Side_Effect(7) well_infl_stabl _ locale_ub _ less_inv
        trans_dep_1, simplified, OF eq_equal_sides_subsumed Eval.prems(5) pre]
    show ?thesis using IH by auto
  next
    case (Abort)
    then show ?thesis
      using Eval.prems(6) by fast
  next
    case Answer
    then show ?thesis
      using Eval.prems(6) by auto
  qed
qed

lemma less_than_part_post_solution:
  assumes "solve_dom x"
    and "solve x = (st, sigma)"
  shows "∀σl varsl. part_post_solution T x σl varsl ⟶ sigma ≤ σl ∧ st ⊆ varsl"
proof (intro allI impI, goal_cases)
  case (1 σl varsl)
  obtain xd state' where
    iterate_dom: "iterate_dom x (init_state⦇called := insert x (called init_state)⦈)" and
    iterate: "(xd, state') = iterate x (init_state⦇called := insert x (called init_state)⦈)" and
    st: "st = stabl state'" and sigma: "sigma = σ state'"
    using assms unfolding solve_dom_def solve_def by (auto split: prod.splits)
  have "less_than_least x state'"
    using less_than_part_post_solution_ind(2)[OF iterate_dom iterate, of x]
    unfolding init_state_def well_infl_stabl_def fmlookup_default_def
    by (auto simp add: le_fun_def)
  then show ?case using 1 by (auto simp add: st sigma)
qed

theorem least_partial_post_solution:
  assumes "solve_dom x"
    and "solve x = (st, sigma)"
  shows "least_part_post_solution T x sigma st"
proof -
  note part_sol = partial_solution[OF assms]
  then have "part_post_solution T x sigma st" by simp
  moreover have least: "∀σl varsl. part_post_solution T x σl varsl ⟶ sigma ≤ σl ∧ st ⊆ varsl"
    using less_than_part_post_solution[OF assms]
    by auto
  ultimately show ?thesis by blast
qed

end ―‹end of context TD_side_opt_mono›

end ―‹end of theory TD_side›