Theory TD_widen

section ‹TD with Widening›

theory TD_widen
  imports Destabilization Basics
begin

declare fun_upd_apply[simp del]

locale TD_widen =
  fixes T :: "'x ⇒ ('x, 'd :: bounded_semilattice_sup_bot) strategy_tree"

  fixes widening :: "'d ⇒ 'd ⇒ 'd" (infixl "∇" 65) (* i.e. ~ union *)
  assumes widening_ge: "a ⊔ b ≤ a ∇ b"
(*  and widening_bounded: "b ≤ a ⟹ a ∇ b = a" *)
(*  Regarding widening constraints (strictest to weakest):
                  A²I: a ⊓ b ≤ a Δ b ∧ a Δ b ≤ a
             Seidl WN: b ≤ a ⟹ b ≤ a Δ b ∧ a Δ b ≤ a
    If we don't care about termination / because of warrowing operator, it suffices that: *)
begin

subsection ‹Definitions›

function (domintros)
    query :: "'x ⇒ 'x ⇒ 'x set ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map
              ⇒ 'd × ('x, 'x list) fmap × 'x set × 'x set × ('x, 'd) map" and
  iterate :: "'x ⇒ 'x set ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map
              ⇒ 'd × ('x, 'x list) fmap × 'x set × 'x set × ('x, 'd) map" and
     eval :: "'x ⇒ ('x, 'd) strategy_tree ⇒ 'x set ⇒ ('x, 'x list) fmap ⇒ 'x set => 'x set
              ⇒ ('x, 'd) map ⇒ 'd × ('x, 'x list) fmap × 'x set × 'x set × ('x, 'd) map" where
  "query y x c infl stabl p σ = (
    let (xd, infl, stabl, p, σ) =
      if x ∈ c then
        (mlup σ x, infl, stabl, insert x p, σ)
      else
        iterate x (insert x c) infl stabl p σ
    in (xd, fminsert infl x y, stabl, p, σ))"
(* Set.remove x p → either x was in p and is now removed or this call does not change anything *)
| "iterate x c infl stabl p σ = (
    if x ∉ stabl then
      let (xd, infl, stabl, p', σ) = eval x (T x) c infl (insert x stabl) p σ in
      let d_new = if x ∉ p then xd else mlup σ x ∇ xd in
      if mlup σ x = d_new then
        (mlup σ x, infl, stabl, Set.remove x p', σ)
      else
        let (infl, stabl) = destab x infl stabl in
        iterate x c infl stabl p' (σ(x ↦ d_new))
    else
      (mlup σ x, infl, stabl, Set.remove x p, σ))"
| "eval x t c infl stabl p σ = (case t of
      Answer d ⇒ (d, infl, stabl, p, σ)
    | Query y g ⇒ (
        let (yd, infl, stabl, p, σ) = query x y c infl stabl p σ in
        eval x (g yd) c infl stabl p σ))"
  by pat_completeness auto
(* I use the case construct here because this makes the proof structure nicer later. In my opinion
the decision Answer/Query is on the same level as Iterate/Lookup or Continue/Fixpoint. If one has
this distinction on the call level (without case construct) the the distinction Answer/Query is
already incorporated in the pinduct rule and the eval..._cases rule becomes akward. *)

definition solve :: "'x ⇒ 'x set × ('x, 'd) map" where
  "solve x = (let (_, _, stabl, _, σ) = iterate x {x} fmempty {} {} Map.empty in (stabl, σ))"

definition query_dom where
  "query_dom y x c infl stabl p σ = query_iterate_eval_dom (Inl (y, x, c, infl, stabl, p, σ))"
declare query_dom_def [simp]
definition iterate_dom where
  "iterate_dom x c infl stabl p σ = query_iterate_eval_dom (Inr (Inl (x, c, infl, stabl, p, σ)))"
declare iterate_dom_def [simp]
definition eval_dom where
  "eval_dom x t c infl stabl p σ = query_iterate_eval_dom (Inr (Inr (x, t, c, infl, stabl, p, σ)))"
declare eval_dom_def [simp]

definition solve_dom where
  "solve_dom x = iterate_dom x {x} fmempty {} {} Map.empty"

(* Probably not needed? *)
lemmas dom_defs = query_dom_def iterate_dom_def eval_dom_def


subsubsection ‹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_eval_pinduct[consumes 1, case_names Query Iterate Eval]
  = query_iterate_eval.pinduct(1)[
      folded query_dom_def iterate_dom_def eval_dom_def,
      of y x c infl stabl p σ for y x c infl stabl p σ
    ]
    query_iterate_eval.pinduct(2)[
      folded query_dom_def iterate_dom_def eval_dom_def,
      of x c infl stabl p σ for x c infl stabl p σ
    ]
    query_iterate_eval.pinduct(3)[
      folded query_dom_def iterate_dom_def eval_dom_def,
      of x t c infl stabl p σ for x t c infl stabl p σ
    ]

lemmas iterate_pinduct[consumes 1, case_names Iterate]
  = query_iterate_eval_pinduct(2)[where ?P="λy x c infl stabl p σ. True"
    and ?R="λx t c infl stabl p σ. True", simplified (no_asm_use),
    folded query_dom_def iterate_dom_def eval_dom_def]

(* add simps to simp set *)
declare query.psimps [simp]
declare iterate.psimps [simp]
declare eval.psimps [simp]

subsubsection ‹Domain lemmas›

lemma dom_backwards_pinduct:
  shows "query_dom y x c infl stabl p σ
    ⟹ x ∉ c ⟹ iterate_dom x (insert x c) infl stabl p σ"
  and "iterate_dom x c infl stabl p σ
    ⟹ x ∉ stabl ⟹ (eval_dom x (T x) c infl (insert x stabl) p σ ∧
        ((xd, infl1, stabl1, p1, σ1) = eval x (T x) c infl (insert x stabl) p σ
          ⟶ d_new = (if x ∉ p then xd else mlup σ1 x ∇ xd)
          ⟶ mlup σ1 x ≠ d_new ⟶ (infl2, stabl2) = destab x infl1 stabl1 ⟶
          iterate_dom x c infl2 stabl2 p1 (σ1(x ↦ d_new))))"
  and "eval_dom x (Query y g) c infl stabl p σ
    ⟹ (query_dom x y c infl stabl p σ ∧
        ((yd, infl', stabl', p', σ') = query x y c infl stabl p σ ⟶
          eval_dom x (g yd) c infl' stabl' p' σ'))"
proof (induction y x c infl stabl p σ and x c infl stabl p σ and x "Query y g" c infl stabl p σ
    arbitrary: and xd infl1 stabl1 p1 σ1 d_new infl2 stabl2 and y g yd infl' stabl' p' σ'
    rule: query_iterate_eval_pinduct)
  case (Query y x c infl stabl p σ)
  then show ?case using query_iterate_eval.domintros(2) by (auto, presburger)
next
  case (Iterate x c infl stabl p σ)

  have 1: "eval_dom x (T x) c infl (insert x stabl) p σ"
    using Iterate.hyps(2) Iterate.prems query_iterate_eval.domintros(3) by force

  obtain xd infl1 stabl1 p1 σ1 and d_new and infl2 stabl2
    where eval: "(xd, infl1, stabl1, p1, σ1) = eval x (T x) c infl (insert x stabl) p σ"
     and d_new: "d_new = (if x ∉ p then xd else mlup σ1 x ∇ xd)"
     and destab: "(infl2, stabl2) = destab x infl1 stabl1"
    by (metis old.prod.exhaust)

  have 2: "mlup σ1 x ≠ d_new ⟶ iterate_dom x c infl2 stabl2 p1 (σ1(x ↦ d_new))"
    using Iterate.hyps(3)[OF Iterate.prems eval _ _ _ _ d_new _ destab, simplified]
          iterate_dom_def query_iterate_eval.domintros(2) by presburger

  show ?case using 1 d_new destab eval 2
    by (metis Pair_inject)
next
  case (Eval x c infl stabl p σ)
  then show ?case using query_iterate_eval.domintros(1,3) by simp
qed

subsubsection ‹Case rules›

lemma iterate_continue_fixpoint_cases[consumes 3]:
  assumes "iterate_dom x c infl stabl p σ"
    and "(xd, infl', stabl', p', σ') = iterate x c infl stabl p σ"
    and "x ∈ c"
  obtains (Stable) "x ∈ stabl"
    and "xd = mlup σ x"
    and "infl' = infl"
    and "stabl' = stabl"
    and "p' = Set.remove x p"
    and "σ' = σ"
  | (Fixpoint) p1
  where "x ∉ stabl" and "x ∉ p"
    and "eval_dom x (T x) c infl (insert x stabl) p σ"
    and "(xd, infl', stabl', p1, σ') = eval x (T x) c infl (insert x stabl) p σ"
    and "mlup σ' x = xd" (* equality, not assignment *)
    and "p' = Set.remove x p1"
  | (Continue) xd1 infl1 stabl1 p1 σ1 stabl2 infl2
  where "x ∉ stabl" and "x ∉ p"
    and "eval_dom x (T x) c infl (insert x stabl) p σ"
    and "(xd1, infl1, stabl1, p1, σ1) = eval x (T x) c infl (insert x stabl) p σ"
    and "mlup σ1 x ≠ xd1"
    and "(infl2, stabl2) = destab x infl1 stabl1"
    and "iterate_dom x c infl2 stabl2 p1 (σ1(x ↦ xd1))"
    and "(xd, infl', stabl', p', σ') = iterate x c infl2 stabl2 p1 (σ1(x ↦ xd1))"
  | (WN_Fixpoint) xd1 p1
  where "x ∉ stabl" and "x ∈ p"
    and "eval_dom x (T x) c infl (insert x stabl) p σ"
    and "(xd1, infl', stabl', p1, σ') = eval x (T x) c infl (insert x stabl) p σ"
    and "xd = mlup σ' x ∇ xd1"
    and "mlup σ' x = xd" (* equality, not assignment *)
    and "p' = Set.remove x p1"
  | (WN_Continue) xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2
  where "x ∉ stabl" and "x ∈ p"
    and "eval_dom x (T x) c infl (insert x stabl) p σ"
    and "(xd1, infl1, stabl1, p1, σ1) = eval x (T x) c infl (insert x stabl) p σ"
    and "d_new = mlup σ1 x ∇ xd1"
    and "mlup σ1 x ≠ d_new"
    and "(infl2, stabl2) = destab x infl1 stabl1"
    and "iterate_dom x c infl2 stabl2 p1 (σ1(x ↦ d_new))"
    and "(xd, infl', stabl', p', σ') = iterate x c infl2 stabl2 p1 (σ1(x ↦ d_new))"
proof(cases "x ∈ stabl" rule: case_split[case_names Stable Unstable])
  case Stable
  then show ?thesis using that(1) assms(1,2) by auto
next
  case Unstable
  then have sldom: "eval_dom x (T x) c infl (insert x stabl) p σ"
    using assms(1) dom_backwards_pinduct(2)
    by simp
  then obtain xd1 infl1 stabl1 p1 σ1
    where slapp: "eval x (T x) c infl (insert x stabl) p σ = (xd1, infl1, stabl1, p1, σ1)"
    by (cases "eval x (T x) c infl (insert x stabl) p σ") auto
  then obtain d_new
    where d_new: "d_new = (if x ∉ p then xd1 else mlup σ1 x ∇ xd1)"
    by blast
  show ?thesis
  proof (cases "mlup σ1 x = d_new" rule: case_split[case_names Fixpoint Continue])
    case Fixpoint
    then show ?thesis
      using Unstable sldom slapp d_new assms that(2,4)
      apply (cases "x ∈ p") by auto
  next
    case Continue
    obtain infl2 stabl2 where destab: "destab x infl1 stabl1 = (infl2, stabl2)"
      by (cases "destab x infl1 stabl1")
    then have dom: "iterate_dom x c infl2 stabl2 p1 (σ1(x ↦ d_new))"
      using Unstable Continue slapp d_new assms(1) dom_backwards_pinduct(2) by auto
    then show ?thesis
      using Unstable slapp sldom d_new assms destab Continue that(3,5)
      by (cases "x ∈ p") (auto simp add: Let_def)
  qed
qed

lemma iterate_fmlookup:
  assumes "iterate_dom x c infl stabl p σ"
    and "(xd, infl', stabl', p', σ') = iterate x c infl stabl p σ"
    and "x ∈ c"
  shows "mlup σ' x = xd"
  using assms
proof(induction rule: iterate_pinduct)
  case Iterate
  show ?case
    using Iterate.hyps Iterate.prems
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Continue
    then show ?thesis
      by (simp add: Iterate.IH Iterate.prems(2))
  next
    case WN_Continue
    then show ?thesis
      by (simp add: Iterate.IH Iterate.prems(2))
  qed simp+
qed

corollary query_fmlookup:
  assumes "query_dom y x c infl stabl p σ"
    and "(xd, infl', stabl', p', σ') = query y x c infl stabl p σ"
  shows "mlup σ' x = xd"
  using assms iterate_fmlookup dom_backwards_pinduct(1)[of y x c infl stabl p σ]
  by (auto split: prod.splits if_splits)

lemma query_iterate_lookup_cases[consumes 2]:
  assumes "query_dom y x c infl stabl p σ"
    and "(xd, infl', stabl', p', σ') = query y x c infl stabl p σ"
  obtains (Iterate) infl1
  where "x ∉ c"
    and "iterate_dom x (insert x c) infl stabl p σ"
    and "(xd, infl1, stabl', p', σ') = iterate x (insert x c) infl stabl p σ"
    and "infl' = fminsert infl1 x y"
  | (Lookup) "x ∈ c"
    and "xd = mlup σ x"
    and "infl' = fminsert infl x y"
    and "stabl' = stabl"
    and "p' = insert x p"
    and "σ' = σ"
  using assms that dom_backwards_pinduct(1)
  by (cases "x ∈ c"; auto split: prod.splits)

lemma eval_query_answer_cases[consumes 2]:
  assumes "eval_dom x t c infl stabl p σ"
    and "(xd, infl', stabl', p', σ') = eval x t c infl stabl p σ"
  obtains (Query) y g yd infl1 stabl1 p1 σ1
  where "t = Query y g" (* assumption, not assignment *)
    and "query_dom x y c infl stabl p σ"
    and "(yd, infl1, stabl1, p1, σ1) = query x y c infl stabl p σ"
    and "eval_dom x (g yd) c infl1 stabl1 p1 σ1"
    and "(xd, infl', stabl', p', σ') = eval x (g yd) c infl1 stabl1 p1 σ1"
  | (Answer) "t = Answer xd" (* assumption, only indirect assignment *)
    and "infl' = infl"
    and "stabl' = stabl"
    and "p' = p"
    and "σ' = σ"
  using assms dom_backwards_pinduct(3) that
  by (cases t; auto split: prod.splits)

end ― ‹end of @{term TD_widen} locale›


subsection ‹Partial Correctness›

context TD_widen
begin

subsubsection ‹Predicate for valid input state›

definition invariant where
  "invariant c σ infl stabl ≡
    c ⊆ stabl
    ∧ (∀u ∈ stabl - c. eq T u σ = mlup σ u)
    ∧ fset (fmdom infl) ⊆ stabl
    ∧ (∀y∈stabl - c. ∀x ∈ dep T σ y. y ∈ slookup infl x)"

lemma invariant_simp_c_stabl:
  assumes "x ∈ c"
    and "invariant (c - {x}) σ infl stabl"
  shows "invariant c σ infl (insert x stabl)"
  using assms
proof -
  have "c - {x} ⊆ stabl ≡ c ⊆ insert x stabl"
    using assms(1)
    by (simp add: subset_insert_iff)
  moreover have "stabl - (c - {x}) ⊇ insert x stabl - c"
    using assms(1)
    by auto
  ultimately show ?thesis
    using assms(2)
    unfolding invariant_def
    by (meson subset_iff subset_insertI2)
qed

abbreviation eq_subsumed :: "('x, 'd) map ⇒ 'x set ⇒ bool" where
  "eq_subsumed σ vars ≡ (∀x ∈ vars. eq T x σ ≤ mlup σ x)"

definition post_invariant where
  "post_invariant c σ infl stabl ≡
    c ⊆ stabl
    ∧ eq_subsumed σ (stabl - c)
    ∧ fset (fmdom infl) ⊆ stabl
    ∧ (∀y∈stabl - c. ∀x ∈ dep T σ y. y ∈ slookup infl x)"

lemma post_invariant_simp_c_stabl:
  assumes "x ∈ c"
    and "post_invariant (c - {x}) σ infl stabl"
  shows "post_invariant c σ infl (insert x stabl)"
  using assms
proof -
  have "c - {x} ⊆ stabl ≡ c ⊆ insert x stabl"
    using assms(1)
    by (simp add: subset_insert_iff)
  moreover have "stabl - (c - {x}) ⊇ insert x stabl - c"
    using assms(1)
    by auto
  ultimately show ?thesis
    using assms(2)
    unfolding post_invariant_def
    by (meson subset_iff subset_insertI2)
qed


subsubsection ‹Auxiliary lemmas for correctness proofs›

lemma stabl_infl_empty:
  assumes "x ∉ stabl"
    and "fset (fmdom infl) ⊆ stabl"
  shows "slookup infl x = {}"
proof (rule ccontr, goal_cases)
  case 1
  then have "x ∈ fset (fmdom infl)"
    unfolding fmlookup_default_def by fastforce
  then show ?case using assms by blast
qed

lemma dep_closed_implies_reach_cap_tree_closed:
  assumes "x ∈ stabl'"
    and "∀ξ∈stabl' - (c - {x}). dep T σ' ξ ⊆ stabl'"
  shows "reach_cap T σ' (c - {x}) x ⊆ stabl'"
proof (intro subsetI, goal_cases)
  case (1 y)
  then show ?case using assms
  proof(cases "x = y")
    case False
    then have "y ∈ reach_cap_tree T σ' (c - {x}) (T x)"
      using 1 reach_cap_tree_simp2[of x "c - {x}" T σ'] by auto
    then show ?thesis using assms
    proof(induction)
      case (base y)
      then show ?case using base.hyps dep_def[of T] by auto
    next
      case (step y z)
      then show ?case by (metis (no_types, lifting) Diff_iff insert_subset mk_disjoint_insert)
    qed
  qed simp
qed

lemma dep_subset_stable:
  assumes "fset (fmdom infl) ⊆ stabl"
    and "(∀y∈stabl - c. ∀x ∈ dep T σ y. y ∈ slookup infl x)"
  shows "(∀ξ∈stabl - c. dep T σ ξ ⊆ stabl)"
  using assms stabl_infl_empty[of _ stabl infl]
  by (metis DiffD2 Diff_empty subsetI)

lemma new_lookup_to_infl_not_stabl:
  assumes "∀ξ. (slookup infl1 ξ - slookup infl ξ) ∩ stabl = {}"
    and "x ∉ stabl"
    and "fset (fmdom infl) ⊆ stabl"
  shows "influenced_by infl1 x ∩ stabl = {}"
proof -
  have "u ∉ stabl" if "u ∈ influenced_by infl1 x" for u
    using that
  proof (induction rule: influenced_by.induct)
    case (base ys y)
    have "slookup infl x = {}" using stabl_infl_empty[OF assms(2,3)] by auto
    then have "y ∈ slookup infl1 x - slookup infl x"
      using base.hyps(1,2) by auto
    then show ?case using base.hyps(1) assms(1,3) by force
  next
    case (step y zs z)
    have "slookup infl y = {}"
      by (meson assms(3) stabl_infl_empty step.IH)
    then have "z ∈ slookup infl1 y - slookup infl y"
      by (simp add: step.hyps(2,3))
    then show ?case using assms(1) stabl_infl_empty[OF _ assms(3)] by fastforce
  qed
  then show ?thesis by auto
qed

lemma infl_upd_diff:
  assumes "∀ξ. (slookup infl' ξ - slookup infl ξ) ∩ stabl = {}"
  shows "∀ξ. (slookup (fminsert infl' x y) ξ - slookup infl ξ) ∩ (stabl - {y}) = {}"
proof(intro allI, goal_cases)
  case (1 ξ)
  show ?case using assms unfolding fminsert_def fmlookup_default_def
  by (cases "x = ξ") auto
qed

lemma infl_diff_eval_step:
  assumes "stabl ⊆ stabl1"
    and "∀ξ. (slookup infl' ξ - slookup infl1 ξ) ∩ (stabl1 - {x}) = {}"
    and "∀ξ. (slookup infl1 ξ - slookup infl ξ) ∩ (stabl - {x}) = {}"
  shows "∀ξ. (slookup infl' ξ - slookup infl ξ) ∩ (stabl - {x}) = {}"
proof(intro allI, goal_cases)
  case (1 ξ)
  have "((slookup infl' ξ - slookup infl1 ξ)
          ∪ (slookup infl1 ξ - slookup infl ξ)) ∩ (stabl - {x}) = {}"
    using assms by auto
  then show ?case by blast
qed


subsubsection ‹Destabilize and Sigma update preserve invariant›

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

lemma destab_preserves_c_subset_stabl:
  assumes "c ⊆ stabl"
    and "stabl ⊆ stabl'"
  shows "c ⊆ stabl'"
  using assms by auto

lemma destab_preserves_infl_dom_stabl:
  assumes "(infl', stabl') = destab x infl stabl"
    and "fset (fmdom infl) ⊆ stabl"
  shows "fset (fmdom infl') ⊆ stabl'"
proof -
  have "infl' = fmdrop_set (insert x (influenced_by infl x)) infl"
    and A: "stabl' = stabl - influenced_by infl x"
    using assms(1) destab_infl_stabl_relation by metis+
  then show ?thesis
    using assms(2)
    by (metis Diff_mono fmdom'_alt_def fmdom'_drop_set subset_insertI)
qed

lemma destab_and_upd_preserves_dep_closed_in_infl:
  assumes "(infl2, stabl2) = destab x infl1 stabl1"
    and "(∀y∈stabl1 - (c - {x}). ∀z∈dep T σ1 y. y ∈ slookup infl1 z)"
  shows "(∀y∈stabl2 - (c - {x}). ∀z∈dep T (σ1(x ↦ xd')) y. y ∈ slookup infl2 z)"
proof (intro ballI, goal_cases)
  case (1 z y)
  have infl2_def: "infl2 = fmdrop_set (insert x (influenced_by infl1 x)) infl1"
    and stabl2_def: "stabl2 = stabl1 - influenced_by infl1 x"
    using assms(1) destab_infl_stabl_relation by metis+

  have "y ∈ dep T σ1 z"
  proof (goal_cases)
    case 1
    have "∀y∈stabl2 - (c - {x}). x ∉ dep T σ1 y"
      using assms(2) stabl2_def destab_x_no_dep by auto
    then have "x ∉ dep T σ1 z"
        using ‹z ∈ stabl2 - (c - {x})› by blast
    then have "dep T (σ1(x ↦ xd')) z = dep T σ1 z"
      using dep_eq[of T σ1 z "σ1(x ↦ xd')"] mlup_eq_mupd_set[of x "dep T σ1 z" σ1 σ1 xd']
      by metis
    then show ?case using ‹y ∈ dep T (σ1(x ↦ xd')) z› by auto
  qed
  then have z_in_infl1_y: "z ∈ slookup infl1 y"
    using 1(1) stabl2_def assms(2) by fastforce

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

lemma destab_upd_preserves_part_post_sol:
  assumes "(infl2, stabl2) = destab x infl1 stabl1"
    and "eq_subsumed σ1 (stabl1 - c)"
    and "∀y∈stabl1 - (c - {x}). ∀x∈dep T σ1 y. y ∈ slookup infl1 x"
    and "traverse_rhs (T x) σ1 ≤ xd'"
  shows "eq_subsumed (σ1(x ↦ xd')) (stabl2 - (c - {x}))"
proof (intro ballI, goal_cases)
  case (1 y)
  have stabl2_def: "stabl2 = stabl1 - influenced_by infl1 x"
    using destab_infl_stabl_relation[OF assms(1)] by auto
  have x_no_dep: "∀y ∈ stabl2 - (c - {x}). x ∉ dep T σ1 y"
    using destab_x_no_dep[OF stabl2_def assms(3)] by simp
  have eq_y_upd: "eq T y (σ1(x ↦ xd')) = eq T y σ1"
    using 1 eq_mupd_no_dep[of x T σ1 y] x_no_dep
    by auto
  show ?case
  proof (cases "y = x")
    case True
    then show ?thesis using assms(4) eq_y_upd unfolding mlup_def by (simp add: fun_upd_same)
  next
    case False
    then have "y ∈ stabl1 - c"
      using 1 stabl2_def by force
    then have "eq T y σ1 ≤ mlup σ1 y"
      using assms(2) by blast
    then show ?thesis using False eq_y_upd unfolding mlup_def by (simp add: fun_upd_other)
  qed
qed


lemma destab_preserves_invariant:
  assumes "(infl2, stabl2) = destab x infl1 stabl1"
    and "post_invariant c σ1 infl1 stabl1"
    and "stabl ⊆ stabl2"
    and "c - {x} ⊆ stabl"
    and "traverse_rhs (T x) σ1 ≤ xd'"
    and "∀y∈dep T σ1 x. x ∈ set (fmlookup_default infl1 [] y)"
  shows "post_invariant (c - {x}) (σ1(x ↦ xd')) infl2 stabl2"
  using assms(2)
  unfolding post_invariant_def
proof (intro conjI, goal_cases)
  case 1
  show ?case using destab_preserves_c_subset_stabl[OF _ assms(3)] assms(4) by auto
next
  case 2
  then have A: "∀y∈stabl1 - (c - {x}). ∀z∈dep T σ1 y. y ∈ set (fmlookup_default infl1 [] z)"
    using assms(6) by auto
  then show ?case using destab_upd_preserves_part_post_sol[OF assms(1) _ _ assms(5)] 2 by auto
  case 4
  show ?case using A destab_and_upd_preserves_dep_closed_in_infl[OF assms(1)] by auto
next
  case 3
  then show ?case using destab_preserves_infl_dom_stabl[OF assms(1)] by auto
qed


subsubsection ‹Induction Proof for Partial Correctness›

abbreviation "update_rel x infl stabl infl' stabl' ≡
    stabl ⊆ stabl' ∧
    (∀u ∈ stabl. slookup infl u ⊆ slookup infl' u) ∧
    (∀u. (slookup infl' u - slookup infl u) ∩ (stabl - {x}) = {})"

lemma post_invariant_continue:
  assumes "x ∉ stabl"
    and "post_invariant c σ infl stabl"
    and "∀y∈stabl. mlup σ y = mlup σ1 y"
  shows "post_invariant c (σ1(x ↦ xd)) infl stabl"
proof -
  show ?thesis
  using assms mlup_eq_mupd_set[OF assms(1,3)] unfolding post_invariant_def
  proof(intro conjI, goal_cases)
    case 1 then show ?case using dep_eq by blast
  next
    case 2 then show ?case
      by (metis Diff_cancel Diff_iff solution_sufficient stabl_infl_empty)
  next
    case 3 then show ?case by blast
  next
    case 4 then show ?case by (metis dep_eq empty_iff stabl_infl_empty)
  qed
qed

(* Compare to old lemma called_mapping_invariance??? *)
lemma partial_correctness_ind:
    (* Note: Removed unused assumption y ∈ stabl (c.f. TD2_equiv) *)
  shows "query_dom y x c infl stabl p σ
    ⟹ (xd, infl', stabl', p', σ') = query y x c infl stabl p σ
    ⟹ post_invariant c σ infl stabl
    ⟹ post_invariant c σ' infl' stabl'
      ∧ (∀ξ ∈ stabl. mlup σ ξ = mlup σ' ξ)
      ∧ y ∈ slookup infl' x
      ∧ update_rel y infl stabl infl' stabl'"
    (* Note: Goal x ∈ stabl' is not mentioned in TD2 → Potentially related to stabl ⊆ stabl' (TD3)
       vs stabl ∪ reach_cap σ' (c - {x}) x ⊆ stabl' (TD2)? *)
    and "iterate_dom x c infl stabl p σ
    ⟹ (xd, infl', stabl', p', σ') = iterate x c infl stabl p σ
    ⟹ x ∈ c
    ⟹ post_invariant (c - {x}) σ infl stabl
    ⟹ post_invariant (c - {x}) σ' infl' stabl'
      ∧ (∀ξ ∈ stabl. mlup σ ξ = mlup σ' ξ)
      ∧ x ∈ stabl'
      ∧ update_rel x infl stabl infl' stabl'"
    and "eval_dom x t c infl stabl p σ
    ⟹ (xd, infl', stabl', p', σ') = eval x t c infl stabl p σ
    ⟹ post_invariant c σ infl stabl
    ⟹ x ∈ stabl
    ⟹ post_invariant c σ' infl' stabl'
      ∧ (∀ξ ∈ stabl. mlup σ ξ = mlup σ' ξ)
      ∧ traverse_rhs t σ' = xd
      ∧ (∀y∈dep_aux σ' t. x ∈ slookup infl' y)
      ∧ update_rel x infl stabl infl' stabl'"
proof(induction y x c infl stabl p σ and x c infl stabl p σ and y t c infl stabl p σ
    arbitrary: xd infl' stabl' p' σ' and xd infl' stabl' p' σ' and xd infl' stabl' p' σ'
    rule: query_iterate_eval_pinduct)
  case (Query y x c infl stabl σ)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate infl1)
    moreover
    note IH = Query.IH(2)[simplified, OF Iterate(1,3) Query.prems(2)]
    ultimately show ?thesis
    proof(intro conjI, goal_cases)
      case 1 then show ?case unfolding post_invariant_def
        by (auto simp add: fminsert_def fmlookup_default_def)
    next
    next case 6 then have "∀ξ. (slookup infl1 ξ - slookup infl ξ) ∩ stabl = {}"
        using Query.prems(2)[unfolded post_invariant_def]
        apply (cases "x ∈ stabl")
         apply (smt (verit) Diff_Int_distrib2 Diff_cancel insertI1 iterate_continue_fixpoint_cases)
        by simp
        (* by (cases "x ∈ stabl"; simp) *)
      then show ?case
        using 6 infl_upd_diff[of infl1 infl stabl x] by auto
    qed (auto simp add: fminsert_def fmlookup_default_def Iterate(3) IH)
  next
    case Lookup
    then show ?thesis using Query.prems(2)
    proof(intro conjI, goal_cases)
      case 1 then show ?case unfolding post_invariant_def
        by (auto simp add: fminsert_def fmlookup_default_def)
    next case 6 then show ?case
      using infl_upd_diff[of infl infl stabl x] Query.prems(2) by auto
    qed (auto simp add: fminsert_def fmlookup_default_def)
  qed
next
  case (Iterate x c infl stabl p σ)
  then have inv: "post_invariant c σ infl (insert x stabl)"
    using post_invariant_simp_c_stabl by metis
  have xstabl: "x ∈ insert x stabl" by simp
  show ?case using Iterate.IH(1) Iterate.prems(1-2)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    show ?thesis using Stable(1) Iterate.prems(1,3) Iterate.IH(1) by auto
  next
    case Fixpoint
    note IH = Iterate.IH(2)[OF Fixpoint(1,4) inv xstabl, folded eq_def dep_def]
    then show ?thesis
    proof(intro conjI, goal_cases)
      case 1 then show ?case unfolding post_invariant_def
      proof(intro conjI, goal_cases)
        case 1 then have "eq_subsumed σ' (stabl' - (c - {x}))"
          using Fixpoint(5) unfolding eq_def post_invariant_def by auto
        then show ?case using IH post_invariant_def by auto
      next
        case 2
        then show ?case using Fixpoint(5) by auto
      next
        case 3 then show ?case using Iterate.prems(2) by (simp add: insert_absorb)
      qed auto
    next
      case 3 then show ?case using Fixpoint(3) by (auto split: prod.splits)
    next
      case 6 then show ?case
        using Fixpoint(4) by blast
    qed auto
  next
    case (Continue xd1 infl1 stabl1 p1 σ1 stabl2 infl2)
    have infl2_def: "infl2 = fmdrop_set (insert x (influenced_by infl1 x)) infl1"
      and stabl2_def: "stabl2 = stabl1 - influenced_by infl1 x"
      using destab_infl_stabl_relation[of infl2 stabl2 x infl1 stabl1] Continue(6) by auto
    note IH = Iterate.IH(2)[OF Continue(1,4) inv xstabl]

    have "(slookup infl1 ξ - slookup infl ξ) ∩ stabl = {}" for ξ
      using Iterate.prems(3) Continue(1) IH
      by auto
    then have stabl_inc: "stabl ⊆ stabl2"
      using Iterate.prems(3) Continue(1,6) new_lookup_to_infl_not_stabl[of infl1 infl stabl x]
        destab_infl_stabl_relation[of infl2 stabl2] IH
      unfolding post_invariant_def
      by auto

    have infl_closed: "(∀x∈stabl1 - (c - {x}). ∀y∈dep T σ1 x. x ∈ slookup infl1 y)"
      using IH[unfolded post_invariant_def, folded dep_def] by auto

    have x_no_dep: "x ∉ dep T σ1 y" if "y ∈ stabl2 - (c - {x})" for y
      using that Continue(6) destab_infl_stabl_relation destab_x_no_dep[OF _ infl_closed]
      by fastforce

    have inv: "post_invariant (c - {x}) (σ1(x ↦ xd1)) infl2 stabl2"
      using destab_preserves_invariant[OF Continue(6) _ stabl_inc] Continue(6) stabl_inc IH
        Iterate.prems(3)[unfolded post_invariant_def]
      unfolding dep_def
      by auto
    have xd1: "xd1 = (if x ∉ p then xd1 else mlup σ1 x ∇ xd1)" using Continue(2) by simp
    note ih = Iterate.IH(3)[OF Continue(1,4) _ _ _ _ xd1 Continue(5,6) _ Continue(8)
        Iterate.prems(2) inv, of "(infl1, stabl1, p1, σ1)" "(stabl1, p1, σ1)" "(p1, σ1)",
        simplified]
    then show ?thesis
    proof(intro conjI, goal_cases)
      case 2 show ?case
        using IH ih Continue(1) insert_iff mlup_eq_mupd_set stabl_inc subsetD by metis
      case 3 then show ?case using IH ih
        by (auto split: prod.split)
    next case 4 show ?case
        using ih stabl_inc by auto
    next case 5
      then show ?case unfolding post_invariant_def
      proof(elim conjE, intro ballI subsetI, goal_cases)
        case (1 ξ u)
        have "ξ ∉ insert x (influenced_by infl1 x)"
          using 1(11) Continue(1) stabl2_def stabl_inc by blast
        then show ?case
          using stabl_inc infl2_def 1(8,11,12) IH
            fmlookup_default_drop_set[of "insert x (influenced_by infl1 x)" infl1 ξ]
          by fastforce
      qed
    next case 6
      then show ?case unfolding post_invariant_def
      proof(intro allI, goal_cases)
        case (1 ξ)
        have "slookup infl2 ξ ⊆ slookup infl1 ξ"
          using infl2_def unfolding fmlookup_default_def by auto
        moreover have "(slookup infl' ξ - slookup infl2 ξ) ∩ stabl = {}"
        proof (cases "x ∈ stabl2")
          case True
          then show ?thesis using Continue(7,8) by auto
        next
          case False
          then show ?thesis
            using 1(1) inv[unfolded post_invariant_def] stabl_inc
            by fastforce
        qed
        moreover have "(slookup infl1 ξ - slookup infl ξ) ∩ stabl = {}"
          using Continue(1) Iterate.prems(3) IH stabl_infl_empty[of x stabl infl]
          by auto
        ultimately show ?case using infl2_def stabl2_def by blast
      qed
    qed auto
  next
    case (WN_Fixpoint xd1 p1)
    note IH = Iterate.IH(2)[OF WN_Fixpoint(1,4) inv xstabl, folded eq_def dep_def]
    moreover have "xd1 ≤ mlup σ' x"
    proof (rule ccontr, goal_cases)
      case 1
      then have "mlup σ' x ∇ xd1 = mlup σ' x" using WN_Fixpoint(5,6) by argo
      then have "xd1 ≤ mlup σ' x" using widening_ge by (metis le_supE)
      then show ?case using 1 by simp
    qed
    ultimately show ?thesis
      unfolding post_invariant_def by auto
  next
    case (WN_Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2)
    have infl2_def: "infl2 = fmdrop_set (insert x (influenced_by infl1 x)) infl1"
      and stabl2_def: "stabl2 = stabl1 - influenced_by infl1 x"
      using destab_infl_stabl_relation[of infl2 stabl2 x infl1 stabl1] WN_Continue(7) by auto
    note IH = Iterate.IH(2)[OF WN_Continue(1,4) inv xstabl]

    have "(slookup infl1 ξ - slookup infl ξ) ∩ stabl = {}" for ξ
      using Iterate.prems(3) WN_Continue(1) IH
      by auto
    then have stabl_inc: "stabl ⊆ stabl2"
      using Iterate.prems(3) WN_Continue(1,7) new_lookup_to_infl_not_stabl[of infl1 infl stabl x]
        destab_infl_stabl_relation[of infl2 stabl2] IH
      unfolding post_invariant_def
      by auto

    have infl_closed: "(∀x∈stabl1 - (c - {x}). ∀y∈dep T σ1 x. x ∈ slookup infl1 y)"
      using IH[unfolded post_invariant_def, folded dep_def] by auto

    have x_no_dep: "x ∉ dep T σ1 y" if "y ∈ stabl2 - (c - {x})" for y
      using that WN_Continue(7) destab_infl_stabl_relation destab_x_no_dep[OF _ infl_closed]
        by fastforce

    have "post_invariant (c - {x}) (σ1(x ↦ d_new)) infl2 stabl2"
      using IH Iterate.prems(2,3) WN_Continue(4,8)
      unfolding post_invariant_def
    proof(elim conjE, intro conjI, goal_cases)
      case 1
      define σ2 where [simp]: "σ2 = σ1(x ↦ xd1)"
      show ?case using stabl_inc
        by (meson Iterate.prems(3) dual_order.trans post_invariant_def)
      case 2
      show ?case
        apply (intro destab_upd_preserves_part_post_sol[OF WN_Continue(7) 2(8) infl_closed, of d_new])
        using widening_ge by (auto simp: "2"(9) WN_Continue(5))
      case 3
      show ?case using destab_preserves_infl_dom_stabl[OF WN_Continue(7) 3(12)] by auto
      case 4
      show ?case
      proof(intro ballI, goal_cases)
        case (1 y z)
        have "dep T σ1 y = dep T σ2 y"
          using x_no_dep[OF 1(1)] dep_eq[of T σ1 _ σ2] σ2_def fun_upd_apply
          unfolding mlup_def by metis
        then show ?case
          using 1 destab_and_upd_preserves_dep_closed_in_infl infl_closed WN_Continue(7) by auto
      qed
    qed
    then have "post_invariant (c - {x}) (σ1(x ↦ d_new)) infl2 stabl2" by simp+
    note inv = this
    have d_new: "d_new = (if x ∉ p then xd1 else mlup σ1 x ∇ xd1)" using WN_Continue(2,5) by simp
    note ih = Iterate.IH(3)[OF WN_Continue(1,4) _ _ _ _ d_new WN_Continue(6,7) _ WN_Continue(9)
        Iterate.prems(2) inv, of "(infl1, stabl1, p1, σ1)" "(stabl1, p1, σ1)" "(p1, σ1)",
        simplified]
    then show ?thesis
    proof(intro conjI, goal_cases)
      case 2 show ?case
        using IH ih WN_Continue(1) insert_iff mlup_eq_mupd_set stabl_inc subsetD by metis
      case 3 then show ?case using IH ih
        by (auto split: prod.split)
    next case 4 show ?case
        using ih stabl_inc by auto
    next case 5
      then show ?case unfolding post_invariant_def
      proof(elim conjE, intro ballI subsetI, goal_cases)
        case (1 ξ u)
        have "ξ ∉ insert x (influenced_by infl1 x)"
          using 1(11) WN_Continue(1) stabl2_def stabl_inc by blast
        then show ?case
          using stabl_inc infl2_def 1(8,11,12) IH
            fmlookup_default_drop_set[of "insert x (influenced_by infl1 x)" infl1 ξ]
          by fastforce
      qed
    next case 6
      then show ?case unfolding post_invariant_def
      proof(intro allI, goal_cases)
        case (1 ξ)
        have "slookup infl2 ξ ⊆ slookup infl1 ξ"
          using infl2_def unfolding fmlookup_default_def by auto
        moreover have "(slookup infl' ξ - slookup infl2 ξ) ∩ stabl = {}"
        proof (cases "x ∈ stabl2")
          case True
          then show ?thesis using WN_Continue(8,9) by auto
        next
          case False
          then show ?thesis
            using 1(1) inv[unfolded post_invariant_def] stabl_inc
            by fastforce
        qed
        moreover have "(slookup infl1 ξ - slookup infl ξ) ∩ stabl = {}"
          using WN_Continue(1) Iterate.prems(3) IH stabl_infl_empty[of x stabl infl]
          by auto
        ultimately show ?case using infl2_def stabl2_def by blast
      qed
    qed auto
  qed
next
  case (Eval x t c infl stabl σ)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (Query y g yd infl1 stabl1 p1 σ1)
    note IH = Eval.IH(2)[OF Query(1,3) Eval.prems(2)]
    then have "post_invariant c σ1 infl1 stabl1"
      by simp
    note inv = this
    have C: "x ∈ stabl1" using IH Eval.prems(3) by blast
    note ih = Eval.IH(3)[OF Query(1,3) _ _ _ _ Query(5) inv(1) C,
        of "(infl1, stabl1, p1, σ1)" "(stabl1, p1, σ1)" "(p1, σ1)", simplified]

    have "y ∈ stabl1"
      using IH stabl_infl_empty[of y stabl1 infl1]
      unfolding post_invariant_def
      by fastforce
    then have "mlup σ1 y = mlup σ' y"
      using ih by fastforce
    then have mlup: "mlup σ' y = yd"
      using Query(2,3) query_fmlookup by metis

    show ?thesis using ih
    proof(intro conjI, goal_cases)
      case 2
      then show ?case using IH by auto
    next
      case 3 then show ?case by (simp add: Query(1) mlup)
    next
      case 4
      then show ?case using Query IH mlup ‹y ∈ stabl1› by auto
    next
      case 5
      then show ?case using IH by auto
    next
      case 6
      then show ?case using IH by blast
    next
      case 7
      then show ?case using IH by blast
    qed auto
  next
    case Answer
    then show ?thesis by (simp add: Eval.prems(2,3))
  qed
qed


corollary partial_correctness:
  assumes "solve_dom x"
    and "solve x = (stabl, σ)"
  shows "part_post_solution T x σ stabl"
proof -
  note it_dom = assms(1)[unfolded solve_dom_def]
  obtain xd infl p where it: "(xd, infl, stabl, p, σ) = iterate x {x} fmempty {} {} Map.empty"
    using assms unfolding solve_def by (cases "iterate x {x} fmempty {} {} Map.empty") auto
  have "post_invariant ({x} - {x}) σ infl stabl" "x ∈ stabl"
    using partial_correctness_ind(2)[OF it_dom it] unfolding post_invariant_def by auto
  then show ?thesis
    using dep_subset_stable[of infl stabl "{}"]
    unfolding post_invariant_def
    by auto
qed

end ― ‹end of @{term TD_widen} context for partial correctness proof›


subsection ‹Termination›

locale TD_widen_term = TD_widen T
  for T :: "'x ⇒ ('x, 'd :: complete_lattice) strategy_tree" +

  fixes widening_chains narrowing_chains :: "('d × 'd) set"
  defines widening_chains: "widening_chains ≡ {(x,y). ∃a. x ≠ y ∧ x = y ∇ a}"
  assumes widening_finite: "wf widening_chains"
    (* just wf {(x,y). ∃a. x = y ∇ a} as assumption causes contradiction due to wf_not_refl and
       widening_bounded *)

      and finite_vars: "finite (UNIV :: 'x set)"
begin

subsubsection ‹Construction of Wellfounded Relation for Termination Proof›

type_synonym ('a,'b) query_in =
  "'a × 'a × 'a set × ('a, 'a list) fmap × 'a set × 'a set × ('a, 'b) map"
type_synonym ('a,'b) iterate_in =
  "'a × 'a set × ('a, 'a list) fmap × 'a set × 'a set × ('a, 'b) map"
type_synonym ('a,'b) eval_in =
  "'a × ('a, 'b) strategy_tree × 'a set × ('a, 'a list) fmap × 'a set × 'a set × ('a, 'b) map"


text ‹For finding a fitting termination relation for the solver with widening, we make the
  following considerations:
  - Most of the termination relation for TD\_plain can be reused. The differing and therefore
    interesting case is when continuing with the iteration.
  - For termination we do not require monotonicity of right-hand sides, since the widening operator
    guarantees accumulation at widening points. Additionally, we require the textbook property for
    widening operators that chains composed of repeated application of the widening operator need
    to be finite.
  - Because the check, whether x is in point is done based on the previous point set, there is one
    special iteration in the beginning where the value of x is not yet widened. We cover this
    iteration by adding an extra component to the lexicographic order that covers the case when
    x was not in point before and is now added to it.
›

definition points_relation :: "(('x × 'x set) × ('x × 'x set)) set" where
  "points_relation = {((x',p'),(x,p)). x' ∈ p' ∧ x ∉ p}"

lemma wf_points_relation: "wf points_relation"
proof (intro wfI_min, goal_cases)
  case (1 t Q)
  obtain x p where "t = (x, p)" by fastforce
  then show ?case
  proof (cases "x ∈ p")
    case True
    then have "(y, (x, p)) ∉ points_relation" for y
      unfolding points_relation_def by auto
    then show ?thesis using 1 ‹t = (x, p)› by blast
  next
    case False
    then show ?thesis
    proof (cases "∃(x',p') ∈ Q. x' ∈ p'")
      case True
      then obtain x' p' where "(x',p') ∈ Q" and "x' ∈ p'" by auto
      then have "∀y ∈ Q. (y, (x', p')) ∉ points_relation"
        unfolding points_relation_def by auto
      then show ?thesis using 1 ‹t = (x, p)› ‹(x', p') ∈ Q› by blast
    next
      case False
      then have "∀(x',p') ∈ Q. x' ∉ p'" by auto
      then have "∀y ∈ Q. (y, (x, p)) ∉ points_relation"
        unfolding points_relation_def by auto
      then show ?thesis using 1 ‹t = (x, p)› by blast
    qed
  qed
qed

definition prod_relation :: "(('x set × nat × ('x, 'd) strategy_tree × nat × 'd)
    × ('x set × nat × ('x, 'd) strategy_tree × nat × 'd)) set" where
  "prod_relation = lex_prod c_relation (lex_prod (measure id) (lex_prod
    strict_subt_relation (lex_prod (measure id) widening_chains)))"

lemma wf_prod_relation: "wf prod_relation"
  unfolding prod_relation_def c_relation_def
  using widening_finite wf_rhs_relation wf_points_relation
  by blast

definition term_relation :: "((('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in) ×
   (('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in)) set"
  where
  "term_relation = inv_image prod_relation (λst. case st of
      Inl (x,y,c,infl,stabl,p,σ) ⇒ (c, 1, T x, 0, mlup σ x)
    | Inr (Inl (x,c,infl,stabl,p,σ)) ⇒ (c, 3, T x, if x ∉ p then 1 else 0, mlup σ x)
    | Inr (Inr (x,t,c,infl,stabl,p,σ)) ⇒ (c, 2, t, 0, mlup σ x))"

lemma wf_term_relation: "wf term_relation"
  unfolding term_relation_def
  by (simp add: wf_prod_relation)


subsubsection ‹Auxiliary Lemmas›

lemma continue_preserves_post_invariant:
  assumes eval_dom: "eval_dom x (T x) c infl (insert x stabl) p σ"
    and eval: "eval x (T x) c infl (insert x stabl) p σ = (xd, infl1, stabl1, p', σ')"
    and destab: "destab x infl1 stabl1 = (infl', stabl')"
    and "x ∈ c"
    and "x ∉ stabl"
    and pinv: "post_invariant (c - {x}) σ infl stabl"
  shows "post_invariant (c - {x}) (σ'(x ↦ if x ∈ p then mlup σ' x ∇ xd else xd)) infl' stabl'"
proof -
  have pinv': "post_invariant c σ infl (insert x stabl)"
      using pinv ‹x ∈ c› post_invariant_simp_c_stabl by auto
  have A: "x ∈ insert x stabl" by simp
  note pcorr1 = partial_correctness_ind(3)[OF eval_dom eval[symmetric] pinv' A]
  have pinv1: "post_invariant c σ' infl1 stabl1" using pcorr1 by auto
  have stabl_incr: "stabl ⊆ stabl'"
  proof -
    have B: "∀ξ. (slookup infl1 ξ - slookup infl ξ) ∩ stabl = {}"
      using pinv ‹x ∉ stabl› pcorr1
      by simp
    have "fset (fmdom infl) ⊆ stabl" using pinv ‹x ∈ c› unfolding post_invariant_def by simp
    then show ?thesis
      using pinv new_lookup_to_infl_not_stabl[OF B ‹x ∉ stabl›]
        destab_infl_stabl_relation[OF destab[symmetric]] pcorr1[simplified]
      unfolding post_invariant_def
      by auto
  qed
  have "traverse_rhs (T x) σ' ≤ (if x ∈ p then mlup σ' x ∇ xd else xd)"
    using pcorr1 widening_ge by auto
  then show ?thesis
    using destab_preserves_invariant[OF destab[symmetric] pinv1 stabl_incr]
      pinv[unfolded post_invariant_def] pcorr1 dep_def[of T]
    by fast
qed

lemma add_c_to_point_infl_inv:
  assumes "x ∉ stabl" "post_invariant (c - {x}) σ infl stabl"
    "{u ∈ c - {x}. fmlookup_default infl [] u ≠ []} ⊆ p"
  shows "{u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p"
proof -
  have "fmlookup_default infl [] x = []"
    using assms(1,2) unfolding post_invariant_def
    by (metis set_empty stabl_infl_empty)
  then show ?thesis
    using assms(3) by auto
qed

lemma p_inv_preserved_by_destab:
  assumes "destab x infl1 stabl1 = (infl2, stabl2)"
    and "{u ∈ (c - {x}). fmlookup_default infl1 [] u ≠ []} ⊆ p1"
  shows "{u ∈ c - {x}. fmlookup_default infl2 [] u ≠ []} ⊆ p1"
proof
  fix v
  assume A: "v ∈ {u ∈ c - {x}. fmlookup_default infl2 [] u ≠ []}"
  then have "v ∈ c - {x}" and "fmlookup_default infl2 [] v ≠ []" by auto
  then have "fmlookup_default infl1 [] v ≠ []"
    using destab_infl_stabl_relation[OF assms(1)[symmetric]]
    by (metis fmlookup_default_drop_set)
  then show "v ∈ p1" using assms(2) ‹v ∈ c - {x}› by blast
qed

lemma p_inv_ind:
  shows "query_dom y x c infl stabl p σ
    ⟹ (xd, infl', stabl', p', σ') = query y x c infl stabl p σ
    ⟹ post_invariant c σ infl stabl
    ⟹ p ⊆ c
    ⟹ {u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p
    ⟹ p ⊆ p' ∧ p' ⊆ c
        ∧ {u ∈ c. fmlookup_default infl' [] u ≠ []} ⊆ p'"
    and "iterate_dom x c infl stabl p σ
    ⟹ (xd, infl', stabl', p', σ') = iterate x c infl stabl p σ
    ⟹ x ∈ c
    ⟹ post_invariant (c - {x}) σ infl stabl
    ⟹ p ⊆ c
    ⟹ {u ∈ c - {x}. fmlookup_default infl [] u ≠ []} ⊆ p
    ⟹ Set.remove x p ⊆ p' ∧ p' ⊆ c - {x}
        ∧ {u ∈ c - {x}. fmlookup_default infl' [] u ≠ []} ⊆ p'"
    and "eval_dom x t c infl stabl p σ
    ⟹ (xd, infl', stabl', p', σ') = eval x t c infl stabl p σ
    ⟹ post_invariant c σ infl stabl
    ⟹ x ∈ stabl
    ⟹ p ⊆ c
    ⟹ {u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p
    ⟹ p ⊆ p' ∧ p' ⊆ c
        ∧ {u ∈ c. fmlookup_default infl' [] u ≠ []} ⊆ p'"
proof(induction y x c infl stabl p σ and x c infl stabl p σ and y t c infl stabl p σ
    arbitrary: xd infl' stabl' p' σ' and xd infl' stabl' p' σ' and xd infl' stabl' p' σ'
    rule: query_iterate_eval_pinduct)
  case (Query y x c infl stabl p σ)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate infl1)
    have inv: "post_invariant (insert x c - {x}) σ infl stabl"
      by (simp add: Iterate(1) Query.prems(2))
    moreover have "x ∉ p" using Iterate(1) Query.prems(3) by auto
    moreover have "{u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p"
        using Query.prems(4) Iterate(1) by simp
    ultimately have IH: "Set.remove x p ⊆ p'" "p' ⊆ c"
        "{u ∈ c. fmlookup_default infl1 [] u ≠ []} ⊆ insert x p'"
      using Query.IH(2)[OF Iterate(1,3)] Iterate(1) Query.prems(3) by blast+
    have "{u ∈ c. fmlookup_default infl' [] u ≠ []} ⊆ p'"
    proof
      fix v
      assume "v ∈ {u ∈ c. fmlookup_default infl' [] u ≠ []}"
      then have "v ∈ c" and "fmlookup_default (fminsert infl1 x y) [] v ≠ []"
        using Iterate(4) by auto
      then have "fmlookup_default infl1 [] v ≠ []"
        using ‹v ∈ c› ‹x ∉ c› unfolding fmlookup_default_def fminsert_def by (metis fmupd_lookup)
      then show "v ∈ p'" using ‹v ∈ c› ‹x ∉ c› IH by blast
    qed
    then show ?thesis using Iterate(4) IH ‹x ∉ p› ‹p' ⊆ c› by auto
  next
    case Lookup
    have "{u ∈ c. fmlookup_default infl' [] u ≠ []} ⊆ p'"
      using Query.prems(4) Lookup(3,5) unfolding fminsert_def fmlookup_default_def by auto
    then show ?thesis using Query.prems(3) Lookup(1,3,5) by auto
  qed
next
  case (Iterate x c infl stabl p σ)
  show ?case using Iterate.IH(1) Iterate.prems(1-2)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Stable Iterate.prems(2-5) Iterate.IH(1) by auto
  next
    case (Fixpoint p1)
    have "post_invariant c σ infl (insert x stabl)"
      using Iterate.prems(2,3) post_invariant_simp_c_stabl by auto
    moreover have "{u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p"
      using add_c_to_point_infl_inv Fixpoint(1) Iterate.prems(3,5) by auto
    ultimately have "p ⊆ p1" and "p1 ⊆ c"
      and "{u ∈ c - {x}. fmlookup_default infl' [] u ≠ []} ⊆ p1"
      using Iterate.IH(2)[OF Fixpoint(1,4)] Iterate.prems by blast+
    then have "{u ∈ c - {x}. fmlookup_default infl' [] u ≠ []} ⊆ insert x p'"
      using Fixpoint(6) by auto
    then show ?thesis using Fixpoint(6) ‹p ⊆ p1› ‹p1 ⊆ c› by fastforce
  next
    case (Continue xd1 infl1 stabl1 p1 σ1 stabl2 infl2)
    have "post_invariant c σ infl (insert x stabl)"
      using Iterate.prems(2-3) post_invariant_simp_c_stabl by auto
    moreover have "{u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p"
      using add_c_to_point_infl_inv Continue(1) Iterate.prems(3,5) by auto
    ultimately have IH: "p ⊆ p1" "p1 ⊆ c" "{u ∈ (c - {x}). fmlookup_default infl1 [] u ≠ []} ⊆ p1"
      using Iterate.IH(2)[OF Continue(1,4)] Iterate.prems by blast+
    have pinv2: "post_invariant (c - {x}) (σ1(x ↦ xd1)) infl2 stabl2"
      using continue_preserves_post_invariant[OF Continue(3) Continue(4,6)[symmetric]
          Iterate.prems(2) Continue(1) Iterate.prems(3)] Continue(2) by auto
    moreover have "{u ∈ c - {x}. fmlookup_default infl2 [] u ≠ []} ⊆ p1"
      using p_inv_preserved_by_destab[OF Continue(6)[symmetric] IH(3)] by auto
    ultimately have "Set.remove x p1 ⊆ p'" and "p' ⊆ c - {x}"
        and "{u ∈ (c - {x}). fmlookup_default infl' [] u ≠ []} ⊆ p'"
      using Iterate.IH(3)[OF Continue(1,4) _ _ _ _ _ Continue(5,6) _ Continue(8) Iterate.prems(2)
          pinv2 ‹p1 ⊆ c›] Continue(2) by auto
    then show ?thesis using ‹p ⊆ p1› by fastforce
  next
    case (WN_Fixpoint xd1 p1)
    have inv: "post_invariant c σ infl (insert x stabl)"
      using Iterate.prems(2,3) post_invariant_simp_c_stabl by auto
    moreover have "{u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p"
      using add_c_to_point_infl_inv WN_Fixpoint(1) Iterate.prems(3,5) by auto
    ultimately have "p ⊆ p1" and "p1 ⊆ c" and "{u ∈ c. fmlookup_default infl' [] u ≠ []} ⊆ p1"
      using Iterate.IH(2)[OF WN_Fixpoint(1,4)] Iterate.prems by blast+
    then have "{u ∈ c. fmlookup_default infl' [] u ≠ []} ⊆ insert x p'"
      using WN_Fixpoint(7) by auto
    then show ?thesis using ‹p ⊆ p1› ‹p1 ⊆ c› WN_Fixpoint(7) by fastforce
  next
    case (WN_Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2)
    have "post_invariant c σ infl (insert x stabl)"
      using Iterate.prems(2-3) post_invariant_simp_c_stabl by auto
    moreover have "{u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p"
      using add_c_to_point_infl_inv WN_Continue(1) Iterate.prems(3,5) by auto
    ultimately have IH: "p ⊆ p1" "p1 ⊆ c" "{u ∈ c. fmlookup_default infl1 [] u ≠ []} ⊆ p1"
      using Iterate.IH(2)[OF WN_Continue(1,4)] Iterate.prems by blast+
    have "post_invariant (c - {x}) (σ1(x ↦ mlup σ1 x ∇ xd1)) infl2 stabl2"
      using continue_preserves_post_invariant[OF WN_Continue(3) WN_Continue(4,7)[symmetric]
          Iterate.prems(2) WN_Continue(1) Iterate.prems(3)] WN_Continue(2) by auto
    moreover have "{u ∈ c - {x}. fmlookup_default infl2 [] u ≠ []} ⊆ p1"
      using p_inv_preserved_by_destab[OF WN_Continue(7)[symmetric]] IH(3) by auto
    ultimately have "Set.remove x p1 ⊆ p'" and "p' ⊆ c - {x}"
        and "{u ∈ c - {x}. fmlookup_default infl' [] u ≠ []} ⊆ p'"
      using Iterate.IH(3)[OF WN_Continue(1,4) _ _ _ _ _ WN_Continue(6,7) _ WN_Continue(9)
          Iterate.prems(2)] WN_Continue(2,5) IH
      by auto
    then show ?thesis using IH by fastforce
  qed
next
  case (Eval x t c infl stabl p σ)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (Query y g yd infl1 stabl1 p1 σ1)
    have "{u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p" using Eval.prems(5) by auto
    then have IH1: "p ⊆ p1" "p1 ⊆ c" "{u ∈ c. fmlookup_default infl1 [] u ≠ []} ⊆ p1"
      using Eval.IH(2)[OF Query(1,3) Eval.prems(2,4)] by auto
    have pinv: "post_invariant c σ1 infl1 stabl1" and "x ∈ stabl1"
      using partial_correctness_ind(1)[OF Query(2,3) Eval.prems(2)] Eval.prems(3) by auto
    have "p1 ⊆ p'" and "p' ⊆ c" and "{u ∈ c. fmlookup_default infl' [] u ≠ []} ⊆ p'"
      using Eval.IH(3)[OF Query(1,3) _ _ _ _ Query(5) pinv ‹x ∈ stabl1›] IH1 by auto
    then show ?thesis using ‹p1 ⊆ p'› ‹p ⊆ p1› ‹p' ⊆ c› by simp
  next
    case Answer
    then show ?thesis using Eval.prems(4,5) by auto
  qed
qed


subsection ‹Induction Proof for Termination›

abbreviation term_cond_aux where
  "term_cond_aux c σ infl stabl p ≡
    post_invariant c σ infl stabl ∧ {u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p"

abbreviation term_cond where
  "term_cond st ≡ (case st of
      Inl (x, y, c, infl, stabl, p, σ) ⇒ term_cond_aux c σ infl stabl p ∧ p ⊆ c
    | Inr (Inl (x, c, infl, stabl, p, σ)) ⇒ term_cond_aux (c - {x}) σ infl stabl p ∧ x ∈ c ∧ p ⊆ c
    | Inr (Inr (x, t, c, infl, stabl, p, σ)) ⇒
        term_cond_aux c σ infl stabl p ∧ x ∈ stabl ∧ p ⊆ c)"

lemma cond_termination: "query_iterate_eval_dom st" if "term_cond st"
  using wf_term_relation that
proof (induction st rule: wf_induct_rule[where ?r = term_relation])
  case (less st)
  then consider (Query) x y c infl stabl p σ where "st = Inl (x, y, c, infl, stabl, p, σ)"
    | (Iterate) x c infl stabl p σ where "st = Inr (Inl (x, c, infl, stabl, p, σ))"
    | (Eval) x t c infl stabl p σ where "st = Inr (Inr (x, t, c, infl, stabl, p, σ))"
    by (metis (no_types, opaque_lifting) sumE surj_pair)
  then show ?case
  proof cases
    case Query
    show ?thesis
    proof (cases "y ∈ c")
      case True
      then show ?thesis using Query query_iterate_eval.domintros(1)[of y c] by blast
    next
      case False
      then have "card (UNIV - insert y c) < card (UNIV - c)"
        using finite_vars
        by (metis Diff_iff UNIV_I card_Diff_insert card_UNIV_unit card_gt_0_iff diff_less empty_iff
            finite_Diff finite_UNIV)
      then have "(insert y c, c) ∈ c_relation"
        unfolding c_relation_def by (meson in_measure)
      then have "(Inr (Inl (y, insert y c, infl, stabl, p, σ)), st) ∈ term_relation"
        unfolding term_relation_def prod_relation_def Query by force
      moreover have "post_invariant c σ infl stabl" "p ⊆ (insert y c) - {y}"
          "{u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p"
        using Query less.prems False by auto
      ultimately show ?thesis
        using Query less(1)[of "Inr (Inl (y, insert y c, infl, stabl, p, σ))"]
          query_iterate_eval.domintros(1) False by force
      qed
  next
    case Iterate
    show ?thesis
    proof (cases "x ∈ stabl")
      case True
      then show ?thesis using Iterate query_iterate_eval.domintros(2) by blast
    next
      case False
      have inv: "post_invariant (c - {x}) σ infl stabl" "x ∈ c" "p ⊆ c"
          "{u ∈ c - {x}. fmlookup_default infl [] u ≠ []} ⊆ p"
        using less.prems Iterate by auto
      have "(Inr (Inr (x, T x, c, infl, insert x stabl, p, σ)), st) ∈ term_relation"
        using Iterate unfolding term_relation_def prod_relation_def by simp
      moreover have pinv: "post_invariant c σ infl (insert x stabl)"
        using ‹post_invariant (c - {x}) σ infl stabl› ‹x ∈ c› post_invariant_simp_c_stabl by auto
      moreover have wpinv: "{u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p"
        using add_c_to_point_infl_inv False inv(1,4) by auto
      ultimately have eval_dom: "eval_dom x (T x) c infl (insert x stabl) p σ"
        using less.IH less.prems Iterate by auto
      then obtain xd infl1 stabl1  p' σ' where
          eval: "eval x (T x) c infl (insert x stabl) p σ = (xd, infl1, stabl1, p', σ')"
        by (metis surj_pair)
      have pcorr: "post_invariant c σ' infl1 stabl1 ∧
        (∀ξ∈insert x stabl. mlup σ ξ = mlup σ' ξ) ∧
        traverse_rhs (T x) σ' = xd ∧
        (∀y∈dep_aux σ' (T x). x ∈ set (fmlookup_default infl1 [] y)) ∧
        insert x stabl ⊆ stabl1 ∧
        (∀u∈insert x stabl. set (fmlookup_default infl [] u) ⊆ set (fmlookup_default infl1 [] u)) ∧
        (∀u. (slookup infl1 u - slookup infl u) ∩ (stabl - {x}) = {})"
        using partial_correctness_ind(3)[OF eval_dom eval[symmetric] pinv] by auto
      have pinv': "p ⊆ p'" "p' ⊆ c" "{u ∈ c. fmlookup_default infl1 [] u ≠ []} ⊆ p'"
        using p_inv_ind(3)[OF eval_dom eval[symmetric] pinv _ ‹p ⊆ c› wpinv] by auto
      show ?thesis
      proof (cases "x ∈ p")
        case True
        then show ?thesis
        proof (cases "mlup σ' x ∇ xd = mlup σ' x")
          case True
          then show ?thesis
            using eval_dom eval query_iterate_eval.domintros(2) Iterate eval_dom_def ‹x ∈ p›
              ‹x ∉ stabl›
            by fastforce
        next
          case False
          obtain infl' stabl' where destab: "destab x infl1 stabl1 = (infl', stabl')" by fastforce
          have "iterate_dom x c infl' stabl' p' (σ'(x ↦ mlup σ' x ∇ xd))"
          proof -
            have "x ∈ p'" using ‹x ∈ p› ‹p ⊆ p'› by blast
            have "(Inr (Inl (x, c, infl', stabl', p', σ'(x ↦ mlup σ' x ∇ xd))), st)
                ∈ term_relation"
            proof -
              have "mlup σ' x ∇ xd ≠ mlup σ' x" using False widening_ge by metis
              moreover have "mlup σ' x = mlup σ x"
                using pinv eval eval_dom partial_correctness_ind(3) by force
              ultimately have "(mlup σ' x ∇ xd, mlup σ x) ∈ widening_chains"
                unfolding widening_chains by auto
              then have "(mlup (σ'(x ↦ mlup σ' x ∇ xd)) x, mlup σ x) ∈ widening_chains"
                unfolding mlup_def
                by (simp add: fun_upd_same)
              then show ?thesis using False ‹x ∈ p› ‹x ∈ p'› Iterate
                unfolding term_relation_def prod_relation_def by auto
            qed
            moreover have "post_invariant (c - {x}) (σ'(x ↦ mlup σ' x ∇ xd)) infl' stabl'"
              using continue_preserves_post_invariant[OF eval_dom eval destab _ ‹x ∉ stabl›]
                Iterate less.prems ‹x ∈ p›
              by auto
            moreover have "x ∈ c" using less.prems Iterate by auto
            moreover have "{u ∈ c - {x}. fmlookup_default infl' [] u ≠ []} ⊆ p'"
              using p_inv_preserved_by_destab[OF destab] pinv'(3) by auto
            ultimately show ?thesis
              using less.IH less.prems Iterate ‹p' ⊆ c›
              unfolding iterate_dom_def by auto
          qed
          then show ?thesis
            using Iterate query_iterate_eval.domintros(2)[of x stabl c infl p σ] eval eval_dom False
              True destab
            unfolding eval_dom_def iterate_dom_def by auto
        qed
      next
        case False
        show ?thesis
        proof (cases "mlup σ' x = xd")
          case True
          then show ?thesis
            using eval_dom eval query_iterate_eval.domintros(2)[folded dom_defs] Iterate ‹x ∉ p›
              ‹x ∉ stabl›
            by fastforce
        next
          case False
          obtain infl' stabl' where destab: "destab x infl1 stabl1 = (infl', stabl')" by fastforce
          have "infl' = fmdrop_set (insert x (influenced_by infl1 x)) infl1"
            and "stabl' = stabl1 - influenced_by infl1 x"
            using destab_infl_stabl_relation[OF destab[symmetric]] by auto
          have "x ∈ stabl1" using pcorr by blast
          have "p' ⊇ {u ∈ c. fmlookup_default infl1 [] u ≠ []}"
            using p_inv_ind(3)[OF eval_dom eval[symmetric] pinv _ ‹p ⊆ c›] ‹x ∈ c› wpinv by auto
          then have "x ∉ influenced_by infl1 x ∨ x ∈ p'"
            using ‹x ∈ c› influenced_by_aux by (cases "fmlookup_default infl1 [] x ≠ []") force+
          then consider (Stable) "x ∈ stabl'" | (Point) "x ∈ p'"
            using ‹stabl' = stabl1 - influenced_by infl1 x› ‹x ∈ stabl1› by blast
          then have "iterate_dom x c infl' stabl' p' (σ'(x ↦ xd))"
          proof (cases)
            case Stable
            then show ?thesis using iterate_dom_def query_iterate_eval.domintros(2) by blast
          next
            case Point
            then have "(Inr (Inl (x, c, infl', stabl', p', σ'(x ↦ xd))), st) ∈ term_relation"
              unfolding term_relation_def prod_relation_def
              using ‹x ∉ p› Iterate
              by auto
            moreover have "post_invariant (c - {x}) (σ'(x ↦ xd)) infl' stabl'"
              using continue_preserves_post_invariant[OF eval_dom eval destab _ ‹x ∉ stabl›]
                Iterate less.prems ‹x ∉ p›
              by auto
            moreover have "{u ∈ c - {x}. fmlookup_default infl' [] u ≠ []} ⊆ p'"
              using p_inv_preserved_by_destab[OF destab] pinv'(3) by auto
            ultimately show ?thesis
              using less.IH less.prems Iterate ‹p' ⊆ c›
              unfolding iterate_dom_def
              by fastforce
          qed
          then show ?thesis
            using Iterate query_iterate_eval.domintros(2) eval eval_dom False ‹x ∉ p› destab
            unfolding eval_dom_def iterate_dom_def by fastforce
        qed
      qed
    qed
  next
    case Eval
    show ?thesis
    proof (cases t)
      case (Answer d)
      then show ?thesis using Eval query_iterate_eval.domintros(3) by fastforce
    next
      case (Query y g)
      then have "(Inl (x, y, c, infl, stabl, p, σ), st) ∈ term_relation"
        unfolding term_relation_def prod_relation_def Eval by simp
      then have query_dom: "query_dom x y c infl stabl p σ"
        using less.IH less.prems Eval by simp
      then obtain σ' infl' stabl' p' d' where
        query: "query x y c infl stabl p σ = (d', infl', stabl', p', σ')" by (metis surj_pair)
      have pinv: "post_invariant c σ infl stabl" "x ∈ stabl" "p ⊆ c"
          "{u ∈ c. fmlookup_default infl [] u ≠ []} ⊆ p"
        using less.prems Eval by auto
      have "eval_dom x (g d') c infl' stabl' p' σ'"
      proof -
        have "d' = mlup σ' y" using query_fmlookup query_dom_def query query_dom by metis
        then have "(g d', t) ∈ strict_subt_relation"
          using Query direct_subt.intros by fastforce
        then have "(Inr (Inr (x, g d', c, infl', stabl', p', σ')), st) ∈ term_relation"
          using Eval unfolding term_relation_def prod_relation_def by simp
        moreover have "post_invariant c σ' infl' stabl'" "x ∈ stabl'"
        proof -
          have "post_invariant c σ' infl' stabl'" and "stabl ⊆ stabl'"
            using partial_correctness_ind(1)[OF query_dom query[symmetric]] pinv
            by auto
          then show "post_invariant c σ' infl' stabl'" "x ∈ stabl'" using ‹x ∈ stabl› by auto
        qed
        moreover have "p' ⊆ c" using p_inv_ind(1)[OF query_dom query[symmetric] pinv(1,3,4)]
          by auto
        moreover have "{u ∈ c. fmlookup_default infl' [] u ≠ []} ⊆ p'"
          using p_inv_ind(1)[OF query_dom query[symmetric] pinv(1,3,4)] by auto
        ultimately show ?thesis using less.IH unfolding eval_dom_def by auto
      qed
      then show ?thesis
        using query_iterate_eval.domintros(3)[of t x c infl stabl p σ] Query Eval query query_dom
        unfolding query_dom_def eval_dom_def
        by (smt (verit, best) Pair_inject strategy_tree.inject(2))
    qed
  qed
qed

corollary terminating: "solve_dom x"
  unfolding solve_dom_def
  using cond_termination[of "Inr (Inl (x, {x}, fmempty, {}, {}, Map.empty))"]
  by (auto simp add: post_invariant_def)

end ― ‹end of termination locale›

end