Theory TD_wn_post

section ‹TD with Widening/Narrowing Phases per Unknown and Ghost State›

theory TD_wn_post
  imports Basics Destabilization TD_invariant_lemmas
begin

datatype phase = Widening | Narrowing

locale TD_wn_post =
  fixes T :: "'x ⇒ ('x, 'd :: bounded_lattice_bot) strategy_tree"

  fixes widening :: "'d ⇒ 'd ⇒ 'd" (infixl "∇" 65)
    and narrowing :: "'d ⇒ 'd ⇒ 'd" (infixl "Δ" 70)
  assumes widening_ge: "a ⊔ b ≤ a ∇ b"
    and widening_bounded: "b ≤ a ⟹ a ∇ b = a"
    and narrowing_ge: "a ⊓ b ≤ a Δ b"
    and narrowing_le: "a Δ b ≤ a"
begin

subsection ‹Definitions›

definition destab_barrier where
  "destab_barrier x pinfl post stabl =
  (fmdrop_set (insert x (influenced_by_cutoff pinfl x (stabl - {x})) - stabl) pinfl,
  post - (influenced_by_cutoff pinfl x (stabl - {x}) - stabl))"

definition destab_post ::
  "'x ⇒ 'x set ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x, 'x list) fmap × 'x set" where
  "destab_post x post pinfl' post' stabl' = (if x ∈ post then (pinfl', post')
    else destab_barrier x pinfl' post' stabl')"

function (domintros)
    query :: "'x ⇒ 'x ⇒ 'x set ⇒ 'x set ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map
              ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'd × ('x, 'x list) fmap × 'x set × 'x set
              × ('x, 'd) map × ('x, 'x list) fmap × 'x set" and
  iterate :: "'x ⇒ 'x set ⇒ 'x set ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x, 'd) map
              ⇒ phase ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'd × ('x, 'x list) fmap × 'x set
              × 'x set × ('x, 'd) map × ('x, 'x list) fmap × 'x set " and
     eval :: "'x ⇒ ('x, 'd) strategy_tree ⇒ 'x set ⇒ 'x set ⇒ ('x, 'x list) fmap ⇒ 'x set
              ⇒ 'x set ⇒ ('x, 'd) map ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'd × ('x, 'x list) fmap
              × 'x set × 'x set × ('x, 'd) map × ('x, 'x list) fmap × 'x set"
     where
  "query y x c⇩w c⇩n infl stabl p σ pinfl post = (
    let (xd, infl, stabl, p, σ, pinfl, post) =
      if x ∈ c⇩w ∪ c⇩n then
        (mlup σ x, infl, stabl, insert x p, σ, pinfl, post)
      else (
        let (c⇩w, c⇩n) = if x ∈ post then (c⇩w, insert x c⇩n) else (insert x c⇩w, c⇩n) in
        iterate x c⇩w c⇩n infl stabl p σ Widening pinfl post)
    in (xd, fminsert infl x y, stabl, p, σ, fminsert pinfl x y, post))"
| "iterate x c⇩w c⇩n infl stabl p σ wn pinfl post = (
    if x ∉ stabl then (
      let (xd, infl, stabl, p', σ, pinfl', post') =
        eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post) in
      let d_new = if x ∉ p then xd else if wn = Widening then mlup σ x ∇ xd else mlup σ x Δ xd in
      if d_new = mlup σ x then (
        if x ∈ p ∧ wn = Widening then (
          if mlup σ x Δ xd = mlup σ x then (
            (mlup σ x, infl, stabl, Set.remove x p', σ, pinfl', post'))
          else (
            let (infl, stabl) = destab x infl stabl in
            iterate x (Set.remove x c⇩w) (insert x c⇩n) infl stabl p' (σ(x ↦ mlup σ x Δ xd)) Narrowing pinfl' post'))
        else
          (mlup σ x, infl, stabl, Set.remove x p', σ, pinfl', post'))
      else (
        let (infl, stabl) = destab x infl stabl in
        let (pinfl', post') = destab_post x post pinfl' post' stabl in
        iterate x c⇩w c⇩n infl stabl p' (σ(x ↦ d_new)) wn pinfl' post'))
    else
      (mlup σ x, infl, stabl, Set.remove x p, σ, pinfl, post))"
| "eval x t c⇩w c⇩n infl stabl p σ pinfl post = (case t of
      Answer d ⇒ (d, infl, stabl, p, σ, pinfl, post)
    | Query y g ⇒ (
        let (yd, infl, stabl, p, σ, pinfl, post) = query x y c⇩w c⇩n infl stabl p σ pinfl post in
        eval x (g yd) c⇩w c⇩n infl stabl p σ pinfl post))"
  by pat_completeness auto

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

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

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

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⇩w c⇩n infl stabl p σ pinfl post for y x c⇩w c⇩n infl stabl p σ pinfl post
    ]
    query_iterate_eval.pinduct(2)[
      folded query_dom_def iterate_dom_def eval_dom_def,
      of x c⇩w c⇩n infl stabl p σ wn pinfl post for x c⇩w c⇩n infl stabl p σ wn pinfl post
    ]
    query_iterate_eval.pinduct(3)[
      folded query_dom_def iterate_dom_def eval_dom_def,
      of x t c⇩w c⇩n infl stabl p σ pinfl post for x t c⇩w c⇩n infl stabl p σ pinfl post
    ]

lemmas iterate_pinduct[consumes 1, case_names Iterate]
  = query_iterate_eval_pinduct(2)[where ?P="λy x c⇩w c⇩n infl stabl p σ pinfl post. True"
    and ?R="λx t c⇩w c⇩n infl stabl p σ pinfl post. 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⇩w c⇩n infl stabl p σ pinfl post
    ⟹ x ∉ c⇩w ∪ c⇩n ⟹ (c1⇩w, c1⇩n) = (if x ∈ post then (c⇩w, insert x c⇩n) else (insert x c⇩w, c⇩n))
          ⟶ iterate_dom x c1⇩w c1⇩n infl stabl p σ Widening pinfl post"
  and "iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post
    ⟹ x ∉ stabl ⟹ (eval_dom x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post) ∧
        ((xd, infl1, stabl1, p1, σ1, pinfl1, post1) =
          eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)
          ⟶ d_new = (if x ∉ p then xd else if wn = Widening then mlup σ1 x ∇ xd else mlup σ1 x Δ xd)
          ⟶ (d_new = mlup σ1 x ⟶ x ∈ p ⟶ wn = Widening ⟶ mlup σ1 x Δ xd ≠ mlup σ1 x ⟶ (infl2, stabl2) = destab x infl1 stabl1
          ⟶ iterate_dom x (Set.remove x c⇩w) (insert x c⇩n) infl2 stabl2 p1 (σ1(x ↦ mlup σ1 x Δ xd)) Narrowing pinfl1 post1)
          ∧ (d_new ≠ mlup σ1 x
          ⟶ (infl2, stabl2) = destab x infl1 stabl1
          ⟶ (pinfl2, post2) = destab_post x post pinfl1 post1 stabl2
          ⟶ iterate_dom x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ d_new)) wn pinfl2 post2)))"
  and "eval_dom x (Query y g) c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ (query_dom x y c⇩w c⇩n infl stabl p σ pinfl post ∧
        ((yd, infl', stabl', p', σ', pinfl', post') = query x y c⇩w c⇩n infl stabl p σ pinfl post ⟶
          eval_dom x (g yd) c⇩w c⇩n infl' stabl' p' σ' pinfl' post'))"
proof (induction y x c⇩w c⇩n infl stabl p σ pinfl post and x c⇩w c⇩n infl stabl p σ wn pinfl post
    and x "Query y g" c⇩w c⇩n infl stabl p σ pinfl post
    arbitrary: c1⇩w c1⇩n and xd infl1 stabl1 p1 σ1 d_new infl2 stabl2 pinfl1 post1 pinfl2 post2
    and y g yd infl' stabl' p' σ' pinfl' post'
    rule: query_iterate_eval_pinduct)
  case (Query y x c⇩w c⇩n infl stabl p σ pinfl post)
  show ?case
  proof (intro impI, goal_cases)
    case 1
    show ?case
      using Query(1) Query(2)[OF Query(3) 1, simplified]
        query_iterate_eval.domintros(2)[of x stabl c1⇩w c1⇩n infl p σ pinfl post Widening]
      by fastforce
  qed
next
  case (Iterate x c⇩w c⇩n infl stabl p σ wn pinfl post)

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

  show ?case
  proof (intro impI conjI, goal_cases)
    case 1
    then show ?case using eval_dom by force
  next
    case 2
    have B: "x ∈ p ∧ wn = Widening" using 2(4,5) by simp
    show ?case
      using Iterate.hyps(3)[OF Iterate.prems 2(1) _ _ _ _ _ _ 2(2-3) B 2(6,7), of "(infl1, stabl1,
        p1, σ1, pinfl1, post1)" "(stabl1, p1, σ1, pinfl1, post1)" "(p1, σ1, pinfl1, post1)" p1
        "(σ1, pinfl1, post1)" "(pinfl1, post1)" pinfl1 post1 infl2 stabl2, simplified]
        query_iterate_eval.domintros(2)[folded dom_defs, of x stabl2 "Set.remove x c⇩w"
        "insert x c⇩n" infl2 p1 "σ1(x ↦ mlup σ1 x Δ xd)" pinfl1 post1 Narrowing]
      by fastforce
  next
    case 3
    have "iterate_dom x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ d_new)) wn pinfl2 post2"
      using Iterate.hyps(4)[OF Iterate.prems 3(1) _ _ _ _ _ _ 3(2-4) _ 3(5)]
        iterate_dom_def query_iterate_eval.domintros(2)[of x stabl2 c⇩w c⇩n infl2 p1 "σ1(x ↦ d_new)"
        pinfl2 post2 wn]
      by fastforce
    then show ?case by auto
  qed
next
  case (Eval x c⇩w c⇩n infl stabl p σ pinfl post)
  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⇩w c⇩n infl stabl p σ wn pinfl post"
    and "(xd, infl', stabl', p', σ', pinfl', post') =
          iterate x c⇩w c⇩n infl stabl p σ wn pinfl post"
    and "x ∈ c⇩w ∪ c⇩n"
  obtains (Stable) "x ∈ stabl"
    and "xd = mlup σ x"
    and "infl' = infl"
    and "stabl' = stabl"
    and "p' = Set.remove x p"
    and "σ' = σ"
    and "post' = post"
    and "pinfl' = pinfl"
  | (Fixpoint) p1
  where "x ∉ stabl" and "x ∉ p"
    and "eval_dom x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
    and "(xd, infl', stabl', p1, σ', pinfl', post') =
          eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
    and "xd = mlup σ' x"
    and "p' = Set.remove x p1"
  | (W_Fixpoint) xd1 infl1 stabl1 p1 σ1 infl2 stabl2 pinfl1 post1
  where "x ∉ stabl" and "x ∈ p" and "wn = Widening"
    and "eval_dom x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
    and "(xd1, infl1, stabl1, p1, σ1, pinfl1, post1) =
          eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
    and "mlup σ1 x ∇ xd1 = mlup σ1 x"
    and "mlup σ1 x Δ xd1 ≠ mlup σ1 x"
    and "(infl2, stabl2) = destab x infl1 stabl1"
    and "iterate_dom x (Set.remove x c⇩w) (insert x c⇩n) infl2 stabl2 p1 (σ1(x ↦ mlup σ1 x Δ xd1)) Narrowing pinfl1 post1"
    and "(xd, infl', stabl', p', σ', pinfl', post') =
          iterate x (Set.remove x c⇩w) (insert x c⇩n) infl2 stabl2 p1 (σ1(x ↦ mlup σ1 x Δ xd1)) Narrowing pinfl1 post1"
  | (N_Fixpoint) xd1 p1
  where "x ∉ stabl" and "x ∈ p" and "wn = Narrowing ∨ (wn = Widening ∧ mlup σ' x ∇ xd1 = mlup σ' x)"
    and "eval_dom x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
    and "(xd1, infl', stabl', p1, σ', pinfl', post') =
          eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
    and "mlup σ' x Δ xd1 = xd"
    and "mlup σ' x = xd"
    and "p' = Set.remove x p1"
  | (Continue) xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2 pinfl1 post1 pinfl2 post2
  where "x ∉ stabl"
    and "eval_dom x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
    and "(xd1, infl1, stabl1, p1, σ1, pinfl1, post1) =
          eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
    and "d_new = (if x ∉ p then xd1 else if wn = Widening then mlup σ1 x ∇ xd1 else mlup σ1 x Δ xd1)"
    and "d_new ≠ mlup σ1 x"
    and "(infl2, stabl2) = destab x infl1 stabl1"
    and "(pinfl2, post2) = destab_post x post pinfl1 post1 stabl2"
    and "iterate_dom x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ d_new)) wn pinfl2 post2"
    and "(xd, infl', stabl', p', σ', pinfl', post') =
          iterate x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ d_new)) wn pinfl2 post2"
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⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
    using assms(1) dom_backwards_pinduct(2) by simp
  then obtain xd1 infl1 stabl1 p1 σ1 pinfl1 post1
    where slapp: "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)
      = (xd1, infl1, stabl1, p1, σ1, pinfl1, post1)"
    by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
  then obtain d_new where d_new:
      "d_new = (if x ∉ p then xd1 else if wn = Widening then mlup σ1 x ∇ 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
    proof (cases "x ∈ p")
      case True
      then show ?thesis
      proof (cases wn)
        case Widening
        show ?thesis
        proof (cases "mlup σ1 x Δ xd1 = mlup σ1 x")
          case True
          have "d_new = mlup σ1 x ∇ xd1" using d_new Widening ‹x ∈ p› by simp
          have "iterate x c⇩w c⇩n infl stabl p σ wn pinfl post = (mlup σ1 x, infl1, stabl1,
              Set.remove x p1, σ1, pinfl1, post1)"
            using assms iterate.psimps[folded dom_defs, OF assms(1)] Unstable slapp Fixpoint d_new Widening
              True by auto
          then have "mlup σ1 x = xd" "infl1 = infl'" "stabl1 = stabl'" "Set.remove x p1 = p'"
              "σ1 = σ'" "pinfl1 = pinfl'" "post1 = post'"
            using assms(2)[symmetric] slapp by auto
          then show ?thesis using that(4)[OF Unstable ‹x ∈ p› _ sldom] True slapp
                ‹d_new = mlup σ1 x ∇ xd1› Fixpoint Widening by auto
        next
          case False
          obtain infl2 stabl2 where destab: "destab x infl1 stabl1 = (infl2, stabl2)"
            by (cases "destab x infl1 stabl1")
          have "d_new = mlup σ1 x ∇ xd1" using d_new Widening True by simp
          moreover have "iterate x c⇩w c⇩n infl stabl p σ wn pinfl post
              = iterate x (Set.remove x c⇩w) (insert x c⇩n) infl2 stabl2 p1 (σ1(x ↦ mlup σ1 x Δ xd1)) Narrowing pinfl1 post1"
            using assms iterate.psimps[folded dom_defs, OF assms(1)] Unstable slapp Fixpoint d_new Widening False
              True destab
            by force
          moreover have "iterate_dom x (Set.remove x c⇩w) (insert x c⇩n) infl2 stabl2 p1 (σ1(x ↦ mlup σ1 x Δ xd1)) Narrowing pinfl1 post1"
            using Unstable slapp Fixpoint d_new Widening True assms(1) dom_backwards_pinduct(2) destab False
            by auto
          ultimately show ?thesis
            using assms(2) Fixpoint that(3)[OF Unstable True Widening sldom slapp[symmetric]] destab False
            by simp
        qed
      next
        case Narrowing
        have "d_new = mlup σ1 x Δ xd1" using d_new Narrowing True by simp
        moreover have "iterate x c⇩w c⇩n infl stabl p σ wn pinfl post = (mlup σ1 x, infl1, stabl1,
            Set.remove x p1, σ1, pinfl1, post1)"
          using assms iterate.psimps[folded dom_defs, OF assms(1)] Unstable slapp Fixpoint d_new Narrowing
            True
          by fastforce
        ultimately show ?thesis
          using Unstable sldom slapp d_new assms that(4)[OF Unstable True _ sldom] Narrowing Fixpoint
          by auto
      qed
    next
      case False
      have "iterate x c⇩w c⇩n infl stabl p σ wn pinfl post
          = (mlup σ1 x, infl1, stabl1, Set.remove x p1, σ1, pinfl1, post1)"
        using assms iterate.psimps[folded dom_defs, OF assms(1)] Unstable slapp Fixpoint d_new False
          by simp
      then show ?thesis
        using Unstable sldom slapp d_new assms that(2)[OF Unstable False sldom] False Fixpoint
        by auto
    qed
  next
    case Continue
    obtain infl2 stabl2 where destab: "(infl2, stabl2) = destab x infl1 stabl1"
      by (cases "destab x infl1 stabl1") auto
    obtain pinfl2 post2 where post1_def:
        "(pinfl2, post2) = destab_post x post pinfl1 post1 stabl2"
      unfolding destab_post_def
      by (smt (verit, ccfv_threshold) surj_pair)
    then have dom: "iterate_dom x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ d_new)) wn pinfl2 post2"
      using Unstable Continue slapp d_new assms(1) dom_backwards_pinduct(2) destab by auto
    moreover have "(xd, infl', stabl', p', σ', pinfl', post')
        = iterate x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ d_new)) wn pinfl2 post2"
      using iterate.psimps assms Unstable slapp d_new Continue destab post1_def
      by (auto simp: Let_def split: prod.splits if_splits)
    ultimately show ?thesis
      using Unstable Continue sldom slapp d_new assms destab that(3,5) post1_def
      by (cases "x ∈ p") auto
  qed
qed

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

corollary query_fmlookup:
  assumes "query_dom y x c⇩w c⇩n infl stabl p σ pinfl post"
    and "(xd, infl', stabl', p', σ', pinfl', post') = query y x c⇩w c⇩n infl stabl p σ pinfl post"
  shows "mlup σ' x = xd"
proof -
  obtain c1⇩w c1⇩n where
    c1_def: "(c1⇩w, c1⇩n) = (if x ∈ post then (c⇩w, insert x c⇩n) else (insert x c⇩w, c⇩n))"
    by fastforce
  then show ?thesis
  proof (cases "x ∈ c⇩w ∪ c⇩n")
    case True
    then have "query y x c⇩w c⇩n infl stabl p σ pinfl post =
                (mlup σ x, fminsert infl x y, stabl, insert x p, σ, fminsert pinfl x y, post)"
      using assms(1) by auto
    then show ?thesis using assms(2) by simp
  next
    case False
    have idom: "iterate_dom x c1⇩w c1⇩n infl stabl p σ Widening pinfl post"
      using assms(1) dom_backwards_pinduct(1)[OF assms(1) False] c1_def by simp
    have "query y x c⇩w c⇩n infl stabl p σ pinfl post =
      (let (xd, infl, stabl, p, σ, pinfl, post) = iterate x c1⇩w c1⇩n infl stabl p σ Widening pinfl post
       in (xd, fminsert infl x y, stabl, p, σ, fminsert pinfl x y, post))"
      using query.psimps[OF assms(1)[unfolded query_dom_def]] False c1_def by auto
    then obtain infl1 pinfl1 where "(xd, infl1, stabl', p', σ', pinfl1, post') =
        iterate x c1⇩w c1⇩n infl stabl p σ Widening pinfl post"
      "infl' = fminsert infl1 x y" "pinfl' = fminsert pinfl1 x y"
      using assms(2) by (cases "iterate x c1⇩w c1⇩n infl stabl p σ Widening pinfl post") simp
    then show ?thesis using iterate_fmlookup[OF idom] c1_def by (auto split: if_splits)
  qed
qed

lemma query_iterate_lookup_cases[consumes 2]:
  assumes "query_dom y x c⇩w c⇩n infl stabl p σ pinfl post"
    and "(xd, infl', stabl', p', σ', pinfl', post') = query y x c⇩w c⇩n infl stabl p σ pinfl post"
  obtains (Iterate) infl1 pinfl1 c1⇩w c1⇩n
  where "x ∉ c⇩w ∪ c⇩n"
    and "iterate_dom x c1⇩w c1⇩n infl stabl p σ Widening pinfl post"
    and "(xd, infl1, stabl', p', σ', pinfl1, post') =
          iterate x c1⇩w c1⇩n infl stabl p σ Widening pinfl post"
    and "(c1⇩w, c1⇩n) = (if x ∈ post then (c⇩w, insert x c⇩n) else (insert x c⇩w, c⇩n))"
    and "infl' = fminsert infl1 x y"
    and "pinfl' = fminsert pinfl1 x y"
  | (Lookup) "x ∈ c⇩w ∪ c⇩n"
    and "xd = mlup σ x"
    and "infl' = fminsert infl x y"
    and "stabl' = stabl"
    and "p' = insert x p"
    and "σ' = σ"
    and "post' = post"
    and "pinfl' = fminsert pinfl x y"
  using assms that dom_backwards_pinduct(1)
proof (cases "x ∈ c⇩w ∪ c⇩n")
  case True
  then show ?thesis using assms that(2) by auto
next
  case False
  obtain c1⇩w c1⇩n where "(c1⇩w, c1⇩n) = (if x ∈ post then (c⇩w, insert x c⇩n) else (insert x c⇩w, c⇩n))"
    by fastforce
  then show ?thesis
    using False assms that(1)[OF False, of c1⇩w c1⇩n] dom_backwards_pinduct(1)[OF assms(1) False]
    by (auto split: prod.splits)
qed

lemma eval_query_answer_cases[consumes 2]:
  assumes "eval_dom x t c⇩w c⇩n infl stabl p σ pinfl post"
    and "(xd, infl', stabl', p', σ', pinfl', post') = eval x t c⇩w c⇩n infl stabl p σ pinfl post"
  obtains (Query) y g yd infl1 stabl1 p1 σ1 pinfl1 post1
  where "t = Query y g"
    and "query_dom x y c⇩w c⇩n infl stabl p σ pinfl post"
    and "(yd, infl1, stabl1, p1, σ1, pinfl1, post1) = query x y c⇩w c⇩n infl stabl p σ pinfl post"
    and "eval_dom x (g yd) c⇩w c⇩n infl1 stabl1 p1 σ1 pinfl1 post1"
    and "(xd, infl', stabl', p', σ', pinfl', post') =
          eval x (g yd) c⇩w c⇩n infl1 stabl1 p1 σ1 pinfl1 post1"
  | (Answer) "t = Answer xd"
    and "infl' = infl"
    and "stabl' = stabl"
    and "p' = p"
    and "σ' = σ"
    and "post' = post"
    and "pinfl' = pinfl"
  using assms dom_backwards_pinduct(3) that
proof (cases t)
  case (Answer _)
  then show ?thesis using assms that by auto
next
  case (Query y g)
  then show ?thesis using assms that dom_backwards_pinduct(3) by (auto split: prod.splits)
qed

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


subsection ‹Partial Correctness›

context TD_wn_post
begin

subsubsection ‹Predicate for valid input state›

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 ‹Destabilize and Sigma update preserve invariant›

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 assms(1) destab_infl_stabl_relation by metis
  have x_no_dep: "∀y ∈ stabl2 - (c - {x}). x ∉ dep T σ1 y"
    using destab_x_no_dep[OF assms(1,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_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 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 destab_infl_stabl_relation[OF assms(1)] by metis+

  have "y ∈ dep T σ1 z" by (simp add: "1"(2))
  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_preserves_invariant:
  assumes "(infl2, stabl2) = destab x infl1 stabl1"
    and "post_invariant c σ1 infl1 stabl1"
    and "stabl ⊆ stabl2"
    and "c - {x} ⊆ stabl"
    and "∀y∈dep T σ1 x. x ∈ set (fmlookup_default infl1 [] y)"
    and "eq T x σ1 ≤ mlup σ1 x"
  shows "post_invariant (c - {x}) σ1 infl2 stabl2"
  using assms(2)
  unfolding post_invariant_def
proof (intro conjI, goal_cases)
  case 1
  show ?case using subset_trans[OF _ assms(3)] assms(4) by auto
next
  case 2
  have stabl2_def: "stabl2 = stabl1 - influenced_by infl1 x"
    using assms(1) destab_infl_stabl_relation by metis
  then show ?case using assms(2,6) unfolding post_invariant_def by auto
next
  case 4
  have A: "∀y∈stabl1 - (c - {x}). ∀z∈dep T σ1 y. y ∈ set (fmlookup_default infl1 [] z)"
    using 4 assms(5) by auto
  show ?case using destab_and_upd_preserves_dep_closed_in_infl'[OF assms(1) A] by blast
next
  case 3
  then show ?case using destab_preserves_infl_dom_stabl[OF assms(1)] by auto
qed

lemma destab_upd_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 subset_trans[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 blast
next
  case 3
  then show ?case using destab_preserves_infl_dom_stabl[OF assms(1)] by auto
qed


subsubsection ‹Post Solution Invariant›

definition "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}) = {}) ∧
    (∀u ∈ stabl. mlup σ u = mlup σ' u)"


subsubsection ‹Points Invariant›

definition points_inv where
  "points_inv p c infl ≡ p ⊆ c ∧ {u ∈ c. slookup infl u ≠ {}} ⊆ p"

definition points_inv_upd where
  "points_inv_upd p' p c infl' ≡ points_inv p' c infl' ∧ p ⊆ p'"

lemma add_c_to_point_inv:
  assumes "x ∉ stabl" "x ∈ c" "post_invariant (c - {x}) σ infl stabl"
    "points_inv (p - {x}) (c - {x}) infl"
  shows "points_inv p c infl"
proof -
  have "fmlookup_default infl [] x = []"
    using stabl_infl_empty assms(1,3) unfolding post_invariant_def by force
  then show ?thesis using assms(2,4) unfolding points_inv_def by auto
qed

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


subsubsection ‹Narrowing Invariant›

definition narrowing_inv :: "'x set ⇒ ('x,'d) map ⇒ ('x,'x list) fmap ⇒ 'x set
  ⇒ ('x,'x list) fmap ⇒ 'x set ⇒ bool" where
  "narrowing_inv c⇩w σ infl stabl pinfl post ≡
    eq_subsumed σ (post - c⇩w)
    ∧ stabl ⊆ post
    ∧ fset (fmdom pinfl) ⊆ post
    ∧ (∀y∈post - c⇩w. ∀x ∈ dep T σ y. y ∈ slookup pinfl x)
    ∧ (∀u. slookup infl u ⊆ slookup pinfl u)"

lemma dep_x_stabl:
  assumes "fset (fmdom infl) ⊆ stabl"
    and "(∀y∈dep T σ x. x ∈ slookup infl y)"
  shows "dep T σ x ⊆ stabl"
proof
  fix y
  assume "y ∈ dep T σ x"
  then have "slookup infl y ≠ {}" using assms(2) by auto
  then have "fmlookup infl y ≠ None"
    unfolding fmlookup_default_def by (cases "fmlookup infl y") auto
  then show "y ∈ stabl" using assms(1) by force
qed

lemma decr_eq_if_sigma_decr_on_old_deps:
  assumes "is_mono_eq T" and "∀u ∈ dep T σ x. mlup σ' u ≤ mlup σ u"
  shows "eq T x σ' ≤ eq T x σ"
proof -
  define σ⇩c where "σ⇩c = (λe. if e ∈ dep T σ x then σ e else σ' e)"
  have "eq T x σ⇩c = eq T x σ" by (metis σ⇩c_def mlup_def solution_sufficient)
  moreover have "eq T x σ' ≤ eq T x σ⇩c"
  proof -
    have "σ' ⊑⇩m σ⇩c" using assms(2) σ⇩c_def by (auto simp add: mlup_def)
    then show ?thesis using assms(1) unfolding is_mono_eq_def by auto
  qed
  ultimately show ?thesis by simp
qed


subsubsection ‹Narrowing Update Relation›

definition update_rel_nar ::
  "'x ⇒ 'x set ⇒ ('x,'d) map ⇒ ('x,'d) map ⇒ 'x set ⇒ 'x set ⇒ 'x set ⇒ ('x, 'x list) fmap
  ⇒ ('x, 'x list) fmap ⇒ bool" where
  "update_rel_nar x c⇩w σ σ' stabl post post' pinfl pinfl' ≡
    post ⊆ post' ∧
    (∀u ∈ post. mlup σ' u ≤ mlup σ u) ∧
    (∀u. slookup pinfl u ⊆ slookup pinfl' u) ∧
    (∀u. (slookup pinfl' u - slookup pinfl u) ∩ (post - (c⇩w ∩ {x})) = {})"
    (* The last condition holds only because dep T σ' u ⊆ dep T σ u for a truly post unknown u and
    and therefore newly collected influences to post unknowns will always be contained in those
    that were already collected previously in pinfl. *)


subsubsection ‹Destabilization Preserves Narrowing Invariant›

lemma subtract_set_preserves_infl_dom_stabl:
  assumes "infl' = fmdrop_set A infl"
    and "stabl' = stabl - B"
    and "B ⊆ A"
    and "fset (fmdom infl) ⊆ stabl"
  shows "fset (fmdom infl') ⊆ stabl'"
  using assms by (metis Diff_mono fmdom'_alt_def fmdom'_drop_set)

lemma nar_after_update_if_post:
  assumes "is_mono_eq T"
    and "mono_deps T"
    and x_post: "x ∈ post"
    and IH: "narrowing_inv c⇩w σ1 infl1 stabl1 pinfl1 post1"
    and post_inv: "post_invariant (c⇩w ∪ c⇩n) σ1 infl1 stabl1"
    and dep_x_in_infl1: "∀u∈dep T σ1 x. x ∈ slookup infl1 u"
    and d_geq_eq: "eq T x σ1 ≤ d"
    and d_leq_lookup: "d ≤ mlup σ1 x"
    and destab_stabl: "(infl2, stabl2) = destab x infl1 stabl1"
    and destab_post: "(pinfl2, post2) = destab_post x post pinfl1 post1 stabl2"
  shows "narrowing_inv (c⇩w - {x}) (σ1(x ↦ d)) infl2 stabl2 pinfl2 post2"
  unfolding narrowing_inv_def
proof (intro conjI, goal_cases)
  have "post2 = post1" "pinfl2 = pinfl1" using destab_post x_post unfolding destab_post_def by auto

  case 1
  have "σ1(x ↦ d) ⊑⇩m σ1" using d_leq_lookup by (simp add: fun_upd_apply mlup_def)
  then have "eq T u (σ1(x ↦ d)) ≤ eq T u σ1" for u using assms(1) unfolding is_mono_eq_def by simp
  moreover have "eq T u σ1 ≤ mlup (σ1(x ↦ d)) u" if "u ∈ post1 - (c⇩w - {x})" for u
  proof (cases "u = x")
    case True
    then show ?thesis using d_geq_eq by (auto simp add: fun_upd_same mlup_def)
  next
    case False
    then show ?thesis
      using IH that unfolding narrowing_inv_def by (auto simp add: mlup_def fun_upd_other)
  qed
  ultimately show ?case using order_trans ‹post2 = post1› by blast

  case 2
  then have "stabl1 ⊆ post1" using IH unfolding narrowing_inv_def by auto
  then show ?case using destab_infl_stabl_relation[OF destab_stabl] ‹post2 = post1› by blast

  case 3
  have "fset (fmdom pinfl1) ⊆ post1" using IH[unfolded narrowing_inv_def] by simp
  then have "fset (fmdom pinfl1) ⊆ post1" using ‹post2 = post1› by blast
  then show ?case using destab_post destab_post_def x_post by force

  case 4
  show ?case
  proof (intro ballI, goal_cases)
    case (1 u v)
    have "σ1(x ↦ d) ⊑⇩m σ1" using d_leq_lookup by (simp add: fun_upd_apply mlup_def)
    then have "dep T (σ1(x ↦ d)) u ⊆ dep T σ1 u" for u
        using ‹mono_deps T› unfolding mono_deps_def by simp
    then have "v ∈ dep T σ1 u" using 1 by blast
    have "u ∈ slookup pinfl1 v"
    proof -
      have "∀y∈post2 - (c⇩w - {x}). ∀x∈dep T σ1 y. y ∈ slookup pinfl1 x"
        using IH[unfolded narrowing_inv_def] dep_x_in_infl1 ‹post2 = post1› by blast
      then have "∀x∈dep T σ1 u. u ∈ slookup pinfl1 x" using 1(1) by simp
      then show ?thesis using ‹v ∈ dep T σ1 u› by blast
    qed
    then show ?case using destab_post destab_post_def x_post by force
  qed

  case 5
  have "slookup infl2 u ⊆ slookup infl1 u" for u
    using destab_infl_stabl_relation[OF destab_stabl]
    by (metis empty_iff empty_set fmlookup_default_drop_set subsetI)
  moreover have "stabl2 ⊆ stabl1"
    using destab_infl_stabl_relation[OF destab_stabl] by auto
  ultimately show ?case
    using ‹pinfl2 = pinfl1› IH unfolding narrowing_inv_def by blast
qed

lemma lookup_in_influenced_cutoff:
  assumes "x ∉ stabl"
  shows "slookup pinfl x ⊆ influenced_by_cutoff pinfl x stabl"
proof(intro subsetI, goal_cases)
  case (1 y)
  then show ?case
    using influenced_by_cutoff.base[of x stabl pinfl] assms
    by (cases rule: set_fmlookup_default_cases) simp
qed

lemma inf_infl_inf_cutoff_infl_or_stabl:
  assumes "u ∈ influenced_by infl1 x"
    and "x ∈ stabl1"
    and stabl2: "stabl2 = stabl1 - influenced_by infl1 x"
    and "post_invariant (c⇩w ∪ c⇩n) σ1 infl1 stabl1"
    and "narrowing_inv c⇩w σ1 infl1 stabl1 pinfl1 post1"
    and "x ∉ stabl2"
  shows "u ∈ influenced_by_cutoff pinfl1 x stabl2 - stabl2"
  using assms(1)
proof (induction rule: influenced_by.induct[consumes 1, case_names base step])
  case (base ys y)
  then have "y ∈ slookup pinfl1 x" using assms(2,5) unfolding narrowing_inv_def by fastforce
  then have "y ∈ influenced_by_cutoff pinfl1 x stabl2" if "x ∉ stabl2"
    using lookup_in_influenced_cutoff that by fastforce
  moreover have "y ∉ stabl2"
    using influenced_by.base base.hyps(1) base.hyps(2) stabl2 assms(1) by fast
  ultimately show ?case using assms(6) by blast
next
  case (step y zs z)
  have "y ∈ stabl1"
    using assms(4) step(2,3) unfolding post_invariant_def by (meson fmdomI subsetD)
  then have "z ∈ slookup pinfl1 y"
    using step(2,3) assms(5) unfolding narrowing_inv_def by fastforce

  have "y ∉ stabl2" using step(1) stabl2 by simp
  then have "y ∈ influenced_by_cutoff pinfl1 x stabl2" if "x ∉ stabl2"
    using step(4) that by blast
  then have "z ∈ influenced_by_cutoff pinfl1 x stabl2" if "x ∉ stabl2"
    using ‹y ∉ stabl2› that influenced_by_cutoff.step[of y pinfl1 x stabl2] ‹z ∈ slookup pinfl1 y›
    by (meson set_fmlookup_default_cases)

  moreover have "z ∉ stabl2" by (metis DiffD2 influenced_by.step stabl2 step.hyps(1-3))

  ultimately show ?case using assms(6) by blast
qed

lemma u_not_dep_on_x:
  assumes destab_stabl_res_2: "stabl2 = stabl1 - influenced_by infl1 x"
    and destab_post_res_2: "post2 = post1 - (influenced_by_cutoff pinfl1 x (stabl2 - {x}) - stabl2)"
    and x_not_post: "x ∉ post"
    and post_inv: "post_invariant (c⇩w ∪ c⇩n - {x}) σ infl stabl"
    and nar_inv: "narrowing_inv (c⇩w - {x}) σ infl stabl pinfl post"
    and update_rel_nar: "update_rel_nar x c⇩w σ σ1 stabl post post1 pinfl pinfl1"
    and post_inv1: "post_invariant (c⇩w ∪ c⇩n) σ1 infl1 stabl1"
    and nar_inv1: "narrowing_inv c⇩w σ1 infl1 stabl1 pinfl1 post1"
    and dep_x_infl1: "∀y ∈ dep T σ1 x. x ∈ slookup infl1 y"
    and x_no_dep: "x ∈ stabl2 ⟶ x ∉ dep T σ1 x"
    and u_in_post2: "u ∈ post2 - (c⇩w - {x})"
  shows "x ∉ dep T σ1 u"
proof (rule ccontr, goal_cases)
  case 1
  then have "u ∈ slookup infl1 x" if "u ∈ stabl1 - (c⇩w ∪ c⇩n)"
    using post_inv1 that nar_inv1 unfolding post_invariant_def narrowing_inv_def by blast

  have "u ∈ post1 - c⇩w" using u_in_post2
    using 1 dep_x_infl1 destab_post_res_2 lookup_in_influenced_cutoff x_no_dep nar_inv1
    unfolding narrowing_inv_def by force
  then have "u ∈ slookup pinfl1 x" using nar_inv1 1 unfolding narrowing_inv_def by blast
  then have u_in_cutoff_if_x_stabl: "u ∈ influenced_by_cutoff pinfl1 x (stabl2 - {x})"
    using lookup_in_influenced_cutoff[of x "stabl2 - {x}" pinfl1] by fast
  have u_notin_cutoff: "u ∉ influenced_by_cutoff pinfl1 x (stabl2 - {x}) - stabl2"
    using destab_post_res_2 u_in_post2 by blast
  then have "u ∈ stabl2" using u_in_cutoff_if_x_stabl by blast
  have "u ≠ x"
  proof (rule ccontr, goal_cases)
    case 1
    then have "x ∈ dep T σ1 x" using ‹¬ x ∉ dep T σ1 u› by simp
    then have "x ∈ slookup infl1 x" using dep_x_infl1 by fastforce
    then have "x ∈ influenced_by infl1 x" using lookup_in_influenced by fastforce
    then have "x ∉ stabl2" using destab_stabl_res_2 by auto
    then show ?case using "1" u_in_cutoff_if_x_stabl u_notin_cutoff by blast
  qed
  have "u ∈ stabl1" using ‹u ∈ stabl2› destab_stabl_res_2 by blast
  have "u ∈ c⇩n"
  proof (rule ccontr, goal_cases)
    case 1
    then have "u ∈ stabl1 - (c⇩w ∪ c⇩n)" using u_in_post2 ‹u ≠ x› ‹u ∈ stabl1› by blast
    then have "u ∈ slookup infl1 x"
      using post_inv1[unfolded post_invariant_def] ‹¬ x ∉ dep T σ1 u› by blast
    then have "u ∈ influenced_by infl1 x" using lookup_in_influenced by fastforce
    then have "u ∉ stabl2" using destab_stabl_res_2 by simp
    then show False using ‹u ∈ stabl2› by auto
  qed
  then have "u ∈ stabl"
    using ‹u ≠ x› post_inv unfolding post_invariant_def by blast
  have "slookup pinfl x = {}"
    using nar_inv x_not_post stabl_infl_empty unfolding narrowing_inv_def by metis
  then have "u ∉ post - {x}"
    using update_rel_nar ‹u ∈ slookup pinfl1 x› unfolding update_rel_nar_def by fastforce
  then have "u ∉ stabl - {x}" using nar_inv unfolding narrowing_inv_def by blast
  then have "False" using ‹u ∈ stabl› ‹u ≠ x› by blast
  then show ?case by simp
qed


lemma non_post_not_influenced:
  assumes "u ∈ influenced_by pinfl1 x"
    and x_not_post: "x ∉ post"
    and lookup_diff: "∀u. (slookup pinfl1 u - slookup pinfl u) ∩ (post - {x}) = {}"
    and pinfl_subset_post: "fset (fmdom pinfl) ⊆ post"
  shows "u ∉ post"
    using assms(1)
proof (induction rule: influenced_by.induct[consumes 1, case_names base step])
  case (base ys y)
  have "slookup pinfl x = {}" using x_not_post pinfl_subset_post stabl_infl_empty by simp
  then have "∀u ∈ slookup pinfl1 x. u ∉ post - {x}" using lookup_diff by fastforce
  then have "y ∉ post - {x}" using base by simp
  then show ?case using x_not_post by simp
next
  case (step y zs z)
  have "slookup pinfl y = {}" using pinfl_subset_post step(4) unfolding narrowing_inv_def
    by (meson stabl_infl_empty)
  then have "z ∈ slookup pinfl1 y - slookup pinfl y" by (simp add: step.hyps(2) step.hyps(3))
  then show ?case using lookup_diff x_not_post by blast
qed

lemma nar_inv_after_destab_update_if_not_post:
  assumes x_not_post: "x ∉ post"
    and post_inv: "post_invariant (c⇩w ∪ c⇩n - {x}) σ infl stabl"
    and nar_inv: "narrowing_inv (c⇩w - {x}) σ infl stabl pinfl post"
    and post_inv1: "post_invariant (c⇩w ∪ c⇩n) σ1 infl1 stabl1"
    and nar_inv1: "narrowing_inv c⇩w σ1 infl1 stabl1 pinfl1 post1"
    and update_rel: "update_rel x infl (insert x stabl) infl1 stabl1 σ σ1"
    and update_rel_nar: "update_rel_nar x c⇩w σ σ1 stabl post post1 pinfl pinfl1"
    and destab_post: "(pinfl2, post2) = destab_post x post pinfl1 post1 stabl2"
    and destab_stabl: "(infl2, stabl2) = destab x infl1 stabl1"
    and x_stabl1: "x ∈ stabl1"
    and xd1_def: "eq T x σ1 ≤ d"
    and x_no_dep: "x ∈ stabl2 ⟶ x ∉ dep T σ1 x"
    and dep_x_infl1: "∀y ∈ dep T σ1 x. x ∈ slookup infl1 y"
    and dom_subset: "post ⊆ post1"
    and stabl_subset: "stabl ⊆ stabl2"
    and post_inv2: "post_invariant (c⇩w ∪ c⇩n - {x}) (σ1(x ↦ d)) infl2 stabl2"
    and c_post_rel: "(x ∈ c⇩w ⟶ x ∉ post - stabl) ∧ (x ∈ c⇩n ⟶ x ∈ post)"
    and xcalled: "x ∈ c⇩w ∪ c⇩n"
    and called_dist: "c⇩w ∩ c⇩n = {}"
  shows "narrowing_inv (c⇩w - {x}) (σ1(x ↦ d)) infl2 stabl2 pinfl2 post2"
proof -
  have destab_post': "(pinfl2, post2) = destab_barrier x pinfl1 post1 stabl2"
    using destab_post x_not_post unfolding destab_post_def by auto
  then have destab_post_res:
    "pinfl2 = fmdrop_set (insert x (influenced_by_cutoff pinfl1 x (stabl2 - {x})) - stabl2) pinfl1"
    "post2 = post1 - (influenced_by_cutoff pinfl1 x (stabl2 - {x}) - stabl2)"
    unfolding destab_barrier_def by (auto split: prod.splits)

  have destab_stabl_res: "infl2 = fmdrop_set (insert x (influenced_by infl1 x)) infl1"
    "stabl2 = stabl1 - influenced_by infl1 x"
    using destab_stabl destab_infl_stabl_relation[of infl2 stabl2 x infl1 stabl1] by auto

  have stabl_subset_post2: "stabl2 ⊆ post2"
  proof -
    have "stabl1 ⊆ post1" using nar_inv1 unfolding narrowing_inv_def by simp
    then show ?thesis using destab_post_res(2) destab_stabl_res(2) by auto
  qed

  show ?thesis
    unfolding narrowing_inv_def
  proof (intro conjI, goal_cases)
    have dom_subset_2: "post ⊆ post1" using dom_subset by auto

    case 2
    then show ?case using stabl_subset_post2 by auto

    case 1
    have "eq T u σ1 ≤ mlup σ1 u" if "u ∈ post1 - c⇩w" for u
      using nar_inv1[unfolded narrowing_inv_def] that by simp
    have "eq T u σ1 ≤ mlup (σ1(x ↦ d)) u" if "x ≠ u" "u ∈ post1 - (c⇩w - {x})" for u
      using that ‹⋀u. u ∈ post1 - c⇩w ⟹ eq T u σ1 ≤ mlup σ1 u›
        by (auto simp add: fun_upd_other mlup_def)
    moreover have "eq T x σ1 ≤ mlup (σ1(x ↦ d)) x"
    proof -
      have "eq T x σ1 ≤ mlup (σ1(x ↦ d)) x"
        using nar_inv1 xd1_def by (auto simp add: fun_upd_same mlup_def)
      then show ?thesis by (auto simp add: fun_upd_same)
    qed
    moreover have "eq T u (σ1(x ↦ d)) = eq T u σ1" if "u ∈ post2 - (c⇩w - {x})" for u
    proof -
      have "x ∉ dep T σ1 u"
        using u_not_dep_on_x destab_stabl_res(2) destab_post_res(2) x_not_post post_inv dep_x_infl1
          nar_inv nar_inv1 post_inv1 that update_rel_nar x_no_dep by blast
      then show ?thesis using eq_mupd_no_dep by force
    qed
    ultimately show ?case using destab_post_res(2) dom_subset by (metis Diff_iff)
  next
    case 3
    show ?case
      using nar_inv1 subtract_set_preserves_infl_dom_stabl[OF destab_post_res]
      unfolding narrowing_inv_def by blast
  next
    case 4
    have "∀y∈post1 - (c⇩w - {x}). ∀x∈dep T σ1 y. y ∈ slookup pinfl1 x"
      using nar_inv1 dep_x_infl1 unfolding narrowing_inv_def by blast
    show ?case
    proof (intro ballI, goal_cases)
      case (1 y z)
      have "x ∉ dep T σ1 y"
        using u_not_dep_on_x destab_stabl_res(2) destab_post_res(2) dep_x_infl1 nar_inv nar_inv1
          post_inv post_inv1 update_rel_nar x_no_dep x_not_post 1(1) by blast
      then have "dep T (σ1(x ↦ d)) y = dep T σ1 y" by (metis dep_eq mlup_eq_mupd_set)
      then have "z ∈ dep T σ1 y" using 1(2) by blast
      then have "y ∈ slookup pinfl1 z"
      proof -
        have "∀y∈post1 - (c⇩w - {x}). ∀x∈dep T σ1 y. y ∈ slookup pinfl1 x"
          using nar_inv1 dep_x_infl1 unfolding narrowing_inv_def by blast
        moreover have "y ∈ post1 - (c⇩w - {x})" using "1"(1) destab_post_res(2) by blast
        ultimately show ?thesis using ‹z ∈ dep T σ1 y› by blast
      qed
      have "z ≠ x" using ‹z ∈ dep T σ1 y› ‹x ∉ dep T σ1 y› by auto

      have "z ∈ post1" using ‹y ∈ slookup pinfl1 z› nar_inv1 unfolding narrowing_inv_def
        by (metis stabl_infl_empty empty_iff)
      have "y ∈ post1" using "1"(1) destab_post_res(2) by blast

      have "z ∉ influenced_by_cutoff pinfl1 x (stabl2 - {x}) - stabl2"
      proof (rule ccontr, goal_cases)
        case 1
        then have "z ∉ stabl2" "z ∈ influenced_by_cutoff pinfl1 x (stabl2 - {x})" by auto
        then have "y ∈ influenced_by_cutoff pinfl1 x (stabl2 - {x})"
          using influenced_by_cutoff.step[of z pinfl1 x "stabl2 - {x}"] ‹y ∈ slookup pinfl1 z›
          by (meson Diff_iff set_fmlookup_default_cases)
        with ‹y ∈ post2 - (c⇩w - {x})› have "y ∈ stabl2" using destab_post_res(2) by blast
        have "y ∉ stabl2 - (c⇩w ∪ c⇩n - {x})"
        proof (rule ccontr, goal_cases)
          case 1
          then have "dep T σ1 y ⊆ stabl2"
            using post_inv2 dep_subset_stable ‹dep T (σ1(x ↦ d)) y = dep T σ1 y›
            unfolding post_invariant_def by blast
          then have "z ∈ stabl2" using ‹z ∈ dep T σ1 y› by auto
          then show ?case using ‹z ∉ stabl2› by simp
        qed
        then have "y ∈ c⇩n" "y ≠ x" "y ∉ c⇩w" using ‹y ∈ post2 - (c⇩w - {x})› ‹y ∈ stabl2› by auto
        then have "y ∈ stabl" using post_inv unfolding post_invariant_def by auto
        then have "y ∈ post" using nar_inv unfolding narrowing_inv_def by blast
        then have "y ∈ slookup pinfl z"
          using ‹y ∈ slookup pinfl1 z› ‹y ∈ post› ‹y ∉ c⇩w› ‹y ≠ x› update_rel_nar
          unfolding update_rel_nar_def by blast
        then have "z ∈ post"
          using nar_inv stabl_infl_empty[of z post pinfl] unfolding narrowing_inv_def
          by fastforce
        have "y ∈ influenced_by pinfl1 x"
          using influenced_cutoff_subset
            ‹y ∈ influenced_by_cutoff pinfl1 x (stabl2 - {x})› by fastforce
        have "x ∈ c⇩w" using c_post_rel x_not_post xcalled called_dist by blast
        have "y ∉ post"
          using non_post_not_influenced[OF ‹y ∈ influenced_by pinfl1 x› x_not_post] nar_inv
            update_rel_nar ‹x ∈ c⇩w› unfolding narrowing_inv_def update_rel_nar_def by auto
        then show False using ‹y ∈ post› by blast
      qed
      then have "z ∉ insert x (influenced_by_cutoff pinfl1 x (stabl2 - {x})) - stabl2"
        using ‹z ≠ x› by blast
      then have "slookup pinfl1 z = slookup pinfl2 z" using destab_post_res(1)
        by (simp add: fmlookup_default_drop_set)
      then show ?case using ‹y ∈ slookup pinfl1 z› by simp
    qed
  next
    case 5
    then show ?case
    proof (intro allI, goal_cases)
      case (1 u)
      then show ?case
      proof (cases "u ∈ stabl2")
        case True
        have "slookup infl2 u ⊆ slookup infl1 u"
          using destab_stabl_res(1) fmlookup_default_drop_set
          by (metis empty_iff empty_set subset_iff)
        moreover have "slookup pinfl2 u = slookup pinfl1 u"
          using destab_post_res(1) True fmlookup_default_drop_set
          by (metis Diff_iff)
        ultimately show ?thesis using nar_inv1 unfolding narrowing_inv_def by blast
      next
        case False
        then have "slookup infl2 u = {}"
          using stabl_infl_empty post_inv2 post_invariant_def by metis
        then show ?thesis by simp
      qed
      
    qed
  qed
qed

lemma post_dom_incr:
  assumes IH1: "insert x post ⊆ post1"
    and post_inv: "post_invariant (c⇩w ∪ c⇩n - {x}) σ infl stabl"
    and post_inv1: "post_invariant (c⇩w ∪ c⇩n) σ1 infl1 stabl1"
    and nar_inv: "narrowing_inv (c⇩w - {x}) σ infl stabl pinfl post"
    and nar_inv1: "narrowing_inv c⇩w σ1 infl1 stabl1 pinfl1 post1"
    and update_rel_nar: "update_rel_nar x c⇩w σ σ1 (insert x stabl) (insert x post) post1 pinfl pinfl1"
    and post3_def: "(pinfl2, post2) = destab_post x post pinfl1 post1 stabl2"
    and post_and_c: "(x ∈ c⇩w ⟶ x ∉ post - stabl) ∧ (x ∈ c⇩n ⟶ x ∈ post)"
    and called_disj: "c⇩w ∩ c⇩n = {}"
    and xcalled: "x ∈ c⇩w ∪ c⇩n"
    and x_not_stabl: "x ∉ stabl"
  shows "post ⊆ post2"
proof (cases "x ∈ post")
  case True
  then have "post2 = post1" using post3_def unfolding destab_post_def by simp
  then show ?thesis using IH1 by simp
next
  case False
  then have destab: "(pinfl2, post2) = destab_barrier x pinfl1 post1 stabl2"
    using post3_def unfolding destab_post_def
    by (cases "destab_barrier x pinfl1 post1 stabl2") auto

  have "x ∉ fset (fmdom pinfl)" using nar_inv False unfolding narrowing_inv_def by blast
  then have "slookup pinfl x = {}" by (simp add: stabl_infl_empty)
  then have "influenced_by pinfl x = {}"
    by (metis influenced_by_aux UN_E empty_iff equals0I)

  have post2_sub: "post ⊆ post1 - {x}" using IH1 False by blast
  have destab_post: "post2 = post1 - (influenced_by_cutoff pinfl1 x (stabl2 - {x}) - stabl2)"
    using destab unfolding destab_barrier_def by simp

  have "x ∈ c⇩w" using False post_and_c called_disj xcalled by blast
  then have U: "∀u. (slookup pinfl1 u - slookup pinfl u) ∩ (post - {x}) = {}"
    using update_rel_nar False unfolding update_rel_nar_def by simp
  have "u ∉ post" if "u ∈ influenced_by pinfl1 x" for u
    using that
  proof (induction rule: influenced_by.induct[consumes 1, case_names base step])
    case (base ys y)
    have "∀u ∈ slookup pinfl1 x. u ∉ post - {x}" using U ‹slookup pinfl x = {}› by fastforce
    then have "y ∉ post - {x}" using base by simp
    then show ?case using False by simp
  next
    case (step y zs z)
    have "slookup pinfl y = {}" using nar_inv step(4) unfolding narrowing_inv_def
      by (meson stabl_infl_empty)
    then have "z ∈ slookup pinfl1 y - slookup pinfl y" by (simp add: step.hyps(2) step.hyps(3))
    then show ?case using U False by blast
  qed

  moreover have "influenced_by_cutoff pinfl1 x (stabl2 - {x}) ⊆ influenced_by pinfl1 x"
    by (meson influenced_cutoff_subset)

  ultimately show ?thesis using post2_sub destab_post by blast
qed

lemma c_post_after_destab:
  assumes "(x ∈ c⇩w ⟶ x ∉ post - stabl) ∧ (x ∈ c⇩n ⟶ x ∈ post)"
    and "c⇩w ∩ c⇩n = {}"
    and "x ∈ c⇩w ∪ c⇩n"
    and "x ∉ stabl"
    and "(infl2, stabl2) = destab x infl1 stabl1"
    and "(pinfl2, post2) = destab_post x post pinfl1 post1 stabl2"
    and "post ⊆ post2"
    and "narrowing_inv (c⇩w - {x}) σ infl stabl pinfl post"
    and "post_invariant (c⇩w ∪ c⇩n) σ1 infl1 stabl1"
    and "narrowing_inv c⇩w σ1 infl1 stabl1 pinfl1 post1"
  shows "(x ∈ c⇩w ⟶ x ∉ post2 - stabl2) ∧ (x ∈ c⇩n ⟶ x ∈ post2)"
proof (cases "x ∈ c⇩w")
  case True
  then have "x ∉ post" using assms(1,4) by simp
  have "x ∉ post2 - stabl2"
  proof -
    have "(pinfl2, post2) = destab_barrier x pinfl1 post1 stabl2"
      using assms(6) ‹x ∉ post› unfolding destab_post_def by simp
    then have post2: "post2 = post1 - (influenced_by_cutoff pinfl1 x (stabl2 - {x}) - stabl2)"
      and stabl2: "stabl2 = stabl1 - influenced_by infl1 x"
      using destab_infl_stabl_relation assms(5) unfolding destab_barrier_def by fast+
    have "influenced_by pinfl x = {}" using assms(8) unfolding narrowing_inv_def
      by (metis Diff_disjoint Diff_empty influenced_by_aux stabl_infl_empty
          UN_E ‹x ∉ post› disjoint_iff equals0I)
    have "x ∈ stabl1" using assms(3,9) unfolding post_invariant_def by auto
    then have "u ∈ influenced_by_cutoff pinfl1 x stabl2 - stabl2 ∨ x ∈ stabl2"
      if "u ∈ influenced_by infl1 x" for u
      using inf_infl_inf_cutoff_infl_or_stabl that assms(9,10) stabl2 by force
    then show ?thesis using post2 stabl2 assms(3,9) unfolding post_invariant_def by auto
  qed
  then show ?thesis using True assms(2) by blast
next
  case False
  then have "x ∈ c⇩n" and "x ∈ post" using assms(1,3) by auto
  then show ?thesis using assms(7) False by auto
qed

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

lemma narrow_inv_add_x_stabl_and_post:
  assumes xcalled: "x ∈ c⇩w ∪ c⇩n"
      and wn_post: "(x ∈ c⇩w ⟶ x ∉ post - stabl) ∧ (x ∈ c⇩n ⟶ x ∈ post)"
      and nar_inv: "narrowing_inv (c⇩w - {x}) σ infl stabl pinfl post"
    shows "narrowing_inv c⇩w σ infl (insert x stabl) pinfl (insert x post)"
proof -
  show ?thesis using wn_post nar_inv xcalled unfolding narrowing_inv_def
    by auto
qed

lemma post_inv_after_destab:
  assumes Continue4: " d_new = (if x ∉ p then xd1 else if wn = Widening then mlup σ1 x ∇ xd1 else mlup σ1 x Δ xd1)"
    and Continue6: "(infl2, stabl2) = destab x infl1 stabl1"
    and Iterate_prems3: "post_invariant (c⇩w ∪ c⇩n - {x}) σ infl stabl"
    and Iterate_prems7: "x ∉ p ⟶ wn = Widening"
    and stabl_inc: "stabl ⊆ stabl2"
    and post1_x: "x ∈ post ⟶ eq T x σ1 ≤ mlup σ1 x"
    and in_post_N: "wn = Narrowing ⟶ x ∈ post"
    and post_inv1: "post_invariant (c⇩w ∪ c⇩n) σ1 infl1 stabl1"
    and update_rel1: "update_rel x infl stabl infl1 stabl1 σ σ1"
    and eq_x: "eq T x σ1 = xd1"
    and dep_x: "(∀y∈dep_aux σ1 (T x). x ∈ slookup infl1 y)"
    and x_no_dep: "⋀y. y ∈ stabl2 - ((c⇩w ∪ c⇩n) - {x}) ⟶ x ∉ dep T σ1 y"
  shows "post_invariant ((c⇩w ∪ c⇩n) - {x}) (σ1(x ↦ d_new)) infl2 stabl2"
    unfolding post_invariant_def update_rel_nar_def
proof(intro conjI, goal_cases)
  case 1
  define σ2 where [simp]: "σ2 = σ1(x ↦ xd1)"
  show ?case using stabl_inc
    by (meson Iterate_prems3 dual_order.trans post_invariant_def)
  case 2
  have infl_closed: "(∀x∈stabl1 - ((c⇩w ∪ c⇩n) - {x}). ∀y∈dep T σ1 x. x ∈ slookup infl1 y)"
    using post_inv1 dep_x unfolding post_invariant_def dep_def by auto
  have "eq T x σ1 ≤ d_new"
  proof (cases wn)
    case Widening
    then show ?thesis using widening_ge Continue4 eq_x by simp
  next
    case Narrowing
    then have "x ∈ p" using Iterate_prems7 by blast
    then have "d_new = mlup σ1 x Δ eq T x σ1" using Continue4 eq_x Narrowing by simp
    then have "mlup σ1 x ⊓ eq T x σ1 ≤ d_new" using narrowing_ge by simp
    then show ?thesis using inf_absorb2 post1_x in_post_N Narrowing by fastforce
  qed
  then show ?case
    using destab_upd_preserves_part_post_sol[OF Continue6 _ infl_closed, of d_new] post_inv1
    unfolding eq_def post_invariant_def by auto
  case 3
  show ?case
    using destab_preserves_infl_dom_stabl[OF Continue6] post_inv1 unfolding post_invariant_def
    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 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 Continue6
      by metis
  qed
qed

lemma narrow_inv_after_destab:
  assumes "is_mono_eq T" "mono_deps T"
      and Continue4: "d_new = (if x ∉ p then xd1 else if wn = Widening then mlup σ1 x ∇ xd1 else mlup σ1 x Δ xd1)"
      and Continue5: "d_new ≠ mlup σ1 x"
      and Continue6: "(infl2, stabl2) = destab x infl1 stabl1"
      and Continue7: "(pinfl2, post2) = destab_post x post pinfl1 post1 stabl2"
      and Iterate2: "(x ∈ c⇩w ⟶ x ∉ post - stabl) ∧ (x ∈ c⇩n ⟶ x ∈ post)"
      and Iterate3: "post_invariant (c⇩w ∪ c⇩n - {x}) σ infl stabl"
      and Iterate5: "narrowing_inv (c⇩w - {x}) σ infl stabl pinfl post"
      and Iterate6: "wn = Narrowing ⟶ x ∈ c⇩n"
      and Iterate7: "x ∉ p ⟶ wn = Widening"
      and post1_x: "x ∈ post ⟶ eq T x σ1 ≤ mlup σ1 x"
      and stabl_inc: "stabl ⊆ stabl2"
      and x_no_dep: "⋀y. y ∈ stabl2 - ((c⇩w ∪ c⇩n) - {x}) ⟶ x ∉ dep T σ1 y"
      and xcalled: "x ∈ c⇩w ∪ c⇩n"
      and called_dist: "c⇩w ∩ c⇩n = {}"
      and inv: "post_invariant ((c⇩w ∪ c⇩n) - {x}) (σ1(x ↦ d_new)) infl2 stabl2"
      and IH: "post_invariant (c⇩w ∪ c⇩n) σ1 infl1 stabl1 ∧
          update_rel x infl (insert x stabl) infl1 stabl1 σ σ1 ∧
          narrowing_inv c⇩w σ1 infl1 stabl1 pinfl1 post1 ∧
          update_rel_nar x c⇩w σ σ1 (insert x stabl) (insert x post) post1 pinfl pinfl1 ∧
          traverse_rhs (T x) σ1 = xd1 ∧ (∀y∈dep_aux σ1 (T x). x ∈ slookup infl1 y)"
    shows "narrowing_inv (c⇩w - {x}) (σ1(x ↦ d_new)) infl2 stabl2 pinfl2 post2"
proof (cases "x ∈ post")
  case True
  have d_new_leq: "eq T x σ1 ≤ d_new"
  proof (cases wn)
    case Widening
    then show ?thesis using Continue4 IH widening_ge by auto
  next
    case Narrowing
    then have "mlup σ1 x ⊓ eq T x σ1 ≤ d_new" using Continue4 IH narrowing_ge by auto
    then show ?thesis using inf.absorb2 post1_x True by fastforce
  qed
  have d_new_geq: "d_new ≤ mlup σ1 x"
  proof (cases wn)
    case Widening
    then show ?thesis using Continue4 Continue5 IH widening_bounded True post1_x by force
  next
    case Narrowing
    then show ?thesis using Continue4 IH narrowing_le Iterate7 by simp
  qed

  have "narrowing_inv (c⇩w - {x}) (σ1(x ↦ d_new)) infl2 stabl2 pinfl2 post2"
    using nar_after_update_if_post[OF assms(1,2) True _ _ _ d_new_leq d_new_geq
        Continue6] IH Continue7 unfolding destab_post_def by (metis dep_def)
  then show ?thesis using True Continue5 unfolding destab_post_def by simp
next
  case False
  then have "wn = Widening" using Iterate2 Iterate6 called_dist by (cases wn) auto
  then have "eq T x σ1 ≤ d_new"
  proof (cases "x ∈ p")
    case True
    then have "d_new = mlup σ1 x ∇ eq T x σ1" using Continue4 IH ‹wn = Widening› by simp
    then show ?thesis using widening_ge by auto
  next
    case False
    then have "d_new = xd1" using Continue4 IH by simp
    then show ?thesis using IH by auto 
  qed
    
  moreover have "x ∉ dep T σ1 x" if "x ∈ stabl2"
    using that x_no_dep by auto
  moreover have "update_rel_nar x c⇩w σ σ1 stabl post post1 pinfl pinfl1"
  proof -
    have "update_rel_nar x c⇩w σ σ1 (insert x stabl) (insert x post) post1 pinfl pinfl1"
      using IH by simp
    then show ?thesis using IH xcalled unfolding update_rel_nar_def by blast
  qed
  ultimately show ?thesis
    using nar_inv_after_destab_update_if_not_post[OF False Iterate3 Iterate5 _ _ _ _
        Continue7 Continue6] IH[folded dep_def] stabl_inc inv Iterate2 xcalled called_dist
    unfolding update_rel_nar_def update_rel_def by auto
qed


subsubsection ‹Partial Correctness Induction Proof›

lemma partial_correctness_ind:
  assumes "is_mono_eq T"
      and "mono_deps T"
    shows "query_dom y x c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ (xd, infl', stabl', p', σ', pinfl', post') = query y x c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ post_invariant (c⇩w ∪ c⇩n) σ infl stabl
      ⟹ points_inv p (c⇩w ∪ c⇩n) infl
      ⟹ narrowing_inv c⇩w σ infl stabl pinfl post
      ⟹ c⇩w ∩ c⇩n = {}
      ⟹ y ∈ c⇩w ∪ c⇩n
      ⟹ x ∈ dep T σ y
      ⟹ post_invariant (c⇩w ∪ c⇩n) σ' infl' stabl'
        ∧ update_rel y infl stabl infl' stabl' σ σ'
        ∧ points_inv_upd p' p (c⇩w ∪ c⇩n) infl'
        ∧ narrowing_inv c⇩w σ' infl' stabl' pinfl' post'
        ∧ update_rel_nar y c⇩w σ σ' stabl post post' pinfl pinfl'
        ∧ y ∈ slookup infl' x"
      and "iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post
      ⟹ (xd, infl', stabl', p', σ', pinfl', post') = iterate x c⇩w c⇩n infl stabl p σ wn pinfl post
      ⟹ (x ∈ c⇩w ⟶ x ∉ post - stabl) ∧ (x ∈ c⇩n ⟶ x ∈ post)
      ⟹ post_invariant ((c⇩w ∪ c⇩n) - {x}) σ infl stabl
      ⟹ points_inv (p - {x}) ((c⇩w ∪ c⇩n) - {x}) infl
      ⟹ narrowing_inv (c⇩w - {x}) σ infl stabl pinfl post
      ⟹ (wn = Narrowing) ⟶ (x ∈ c⇩n)
      ⟹ x ∉ p ⟶ wn = Widening
      ⟹ c⇩w ∩ c⇩n = {}
      ⟹ x ∈ c⇩w ∪ c⇩n
      ⟹ post_invariant ((c⇩w ∪ c⇩n) - {x}) σ' infl' stabl'
        ∧ update_rel x infl stabl infl' stabl' σ σ'
        ∧ points_inv_upd p' (p - {x}) ((c⇩w ∪ c⇩n) - {x}) infl'
        ∧ narrowing_inv (c⇩w - {x}) σ' infl' stabl' pinfl' post'
        ∧ update_rel_nar x (c⇩w - {x}) σ σ' stabl post post' pinfl pinfl'
        ∧ x ∈ stabl'"
      and "eval_dom x t c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ (xd, infl', stabl', p', σ', pinfl', post') = eval x t c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ x ∈ c⇩w ∪ c⇩n
      ⟹ post_invariant (c⇩w ∪ c⇩n) σ infl stabl
      ⟹ points_inv p (c⇩w ∪ c⇩n) infl
      ⟹ narrowing_inv c⇩w σ infl stabl pinfl post
      ⟹ c⇩w ∩ c⇩n = {}
      ⟹ subt_for_prefix (T x) pre σ = Some t
      ⟹ set pre ⊆ stabl
      ⟹ post_invariant (c⇩w ∪ c⇩n) σ' infl' stabl'
        ∧ update_rel x infl stabl infl' stabl' σ σ'
        ∧ points_inv_upd p' p (c⇩w ∪ c⇩n) infl'
        ∧ narrowing_inv c⇩w σ' infl' stabl' pinfl' post'
        ∧ update_rel_nar x c⇩w σ σ' stabl post post' pinfl pinfl'
        ∧ traverse_rhs t σ' = xd
        ∧ (∀y∈dep_aux σ' t. x ∈ slookup infl' y)"
proof(induction y x c⇩w c⇩n infl stabl p σ pinfl post and x c⇩w c⇩n infl stabl p σ wn pinfl post
    and y t c⇩w c⇩n infl stabl p σ pinfl post
    arbitrary: xd infl' stabl' p' σ' pinfl' post' and xd infl' stabl' p' σ' pinfl' post'
    and xd infl' stabl' p' σ' pinfl' post' pre
    rule: query_iterate_eval_pinduct)
  case (Query y x c⇩w c⇩n infl stabl p σ pinfl post)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate infl1 pinfl1 c1⇩w c1⇩n)
    have T: "x ∉ p" using Query.prems(3) Iterate(1) unfolding points_inv_def by auto
    then have S: "post_invariant (c1⇩w ∪ c1⇩n - {x}) σ infl stabl"
      using Query.prems(2) Iterate(1,4) by (auto split: if_splits)
    have Q: "x ∉ c⇩w ∪ c⇩n" using Iterate(1) by simp
    have T: "x ∈ post ∧ x ∈ p ∧ x ∉ stabl ⟶ Widening = Narrowing" using T by fastforce
    have R: "narrowing_inv (c1⇩w - {x}) σ infl stabl pinfl post"
      using Query.prems(4) ‹x ∉ c⇩w ∪ c⇩n› Iterate(4) by (auto split: if_splits)
    have Widening: "points_inv (p - {x}) (c1⇩w ∪ c1⇩n - {x}) infl"
      using Query.prems(3) ‹x ∉ c⇩w ∪ c⇩n› ‹x ∉ p› Iterate(4) by (auto split: if_splits)
    have "(x ∉ post) = (x ∈ c1⇩w) ∧ (x ∈ post) = (x ∈ c1⇩n)"
      using ‹x ∉ c⇩w ∪ c⇩n› Iterate(4) Query.prems(2) unfolding post_invariant_def
      by (auto split: if_splits)
    have T2: "(x ∈ c1⇩w ⟶ x ∉ post - stabl) ∧ (x ∈ c1⇩n ⟶ x ∈ post)"
      using ‹x ∉ c⇩w ∪ c⇩n› Iterate(4) Query.prems(2) unfolding post_invariant_def
      by (auto split: if_splits)
    have "c1⇩w ∪ c1⇩n - {x} = c⇩w ∪ c⇩n" using Iterate(4) ‹x ∉ c⇩w ∪ c⇩n› by (auto split: if_splits)
    have "c1⇩w - {x} = c⇩w" and "c1⇩n - {x} = c⇩n"
      using Iterate(4) ‹x ∉ c⇩w ∪ c⇩n› by (auto split: if_splits)
    have U: "c1⇩w ∩ c1⇩n = {}" using Iterate(1,4) Query.prems by (auto split: if_splits)
    have V: "x ∈ c1⇩w ∪ c1⇩n" using Iterate(4) by (auto split: if_splits)
    note IH = Query.IH(2)[OF Q Iterate(4) _ Iterate(3) T2 S Widening R _ _ U V, simplified]
    then show ?thesis using Iterate
    proof(intro conjI, goal_cases)
      case 1
      show ?case using 1(1,6) ‹c1⇩w ∪ c1⇩n - {x} = c⇩w ∪ c⇩n›
        unfolding post_invariant_def fmlookup_default_def fminsert_def by auto
    next
      case 2
      show ?case using 2 unfolding update_rel_def
      proof (intro conjI, goal_cases)
        case 3
        have "∀ξ. (slookup infl1 ξ - slookup infl ξ) ∩ stabl = {}"
          using 2(1,3,4) Query.prems(2)[unfolded post_invariant_def] unfolding update_rel_def
          by (cases "x ∈ stabl") fastforce+
        then show ?case using 2 infl_upd_diff[of infl1 infl stabl x] by auto
      qed (auto simp add: fmlookup_default_def fminsert_def)
    next
      case 3
      show ?case using 3 unfolding points_inv_def points_inv_upd_def
      proof (intro conjI, goal_cases)
        case 1
        then show ?case using ‹c1⇩w ∪ c1⇩n - {x} = c⇩w ∪ c⇩n› by auto
      next
        case 2
        have "{u ∈ c⇩w ∪ c⇩n. slookup infl' u ≠ {}} ⊆ p'"
        proof
          fix v
          assume "v ∈ {u ∈ c⇩w ∪ c⇩n. slookup infl' u ≠ {}}"
          then have "v ∈ c⇩w ∪ c⇩n" and "slookup (fminsert infl1 x y) v ≠ {}"
            using ‹c1⇩w ∪ c1⇩n - {x} = c⇩w ∪ c⇩n› Iterate(5) by auto
          then have "slookup infl1 v ≠ {}"
            using ‹v ∈ c⇩w ∪ c⇩n› ‹x ∉ c⇩w ∪ c⇩n› unfolding fmlookup_default_def fminsert_def
            by (metis fmupd_lookup)
          then show "v ∈ p'"
            using ‹v ∈ c⇩w ∪ c⇩n› ‹x ∉ c⇩w ∪ c⇩n› IH ‹c1⇩w ∪ c1⇩n - {x} = c⇩w ∪ c⇩n›
            unfolding points_inv_def points_inv_upd_def
            by blast
        qed
        then show ?case using IH ‹c1⇩w ∪ c1⇩n - {x} = c⇩w ∪ c⇩n› unfolding points_inv_def by auto
      next
        case 3
        then show ?case using IH ‹x ∉ p› by simp
      qed
    next
      case 4
      then have "narrowing_inv (c1⇩w - {x}) σ' infl1 stabl' pinfl1 post'" by simp
      then show ?case unfolding narrowing_inv_def
      proof (intro conjI, goal_cases)
        case 3
        have "x ∈ stabl'" using IH unfolding post_invariant_def by simp
        then have "x ∈ post'" using 3 Iterate(1) by auto
        moreover have "fset (fmdom infl') = fset (fmdom infl1) ∪ {x}"
          using Iterate(5) unfolding fminsert_def by simp
        ultimately show ?case by (simp add: "3" Iterate(6) fminsert_def)
      next
        case 4
        show ?case
          using 4 ‹c1⇩w - {x} = c⇩w›
          by (metis Iterate(6) UnCI slookup_fminsert_other slookup_fminsert_same)
      next
        case 5
        show ?case
        proof (intro allI, goal_cases)
          case (1 u)
          then show ?case using Iterate(5,6) IH 1 5
            by (cases "u = x") (auto simp add: slookup_fminsert_same slookup_fminsert_other)
        qed
      qed (auto simp add: ‹c1⇩w - {x} = c⇩w›)
    next
      case 5
      then show ?case
        unfolding update_rel_nar_def
      proof (intro conjI, goal_cases)
        case 1
        then show ?case by blast
      next
        case 2
        then show ?case by blast
      next
        case 3
        have "slookup pinfl1 v ⊆ slookup pinfl' v" for v
          using Iterate(6) unfolding fmlookup_default_def fminsert_def by auto
        then show ?case using 3 by blast
      next
        case 4
        then have A: "∀u. (slookup pinfl1 u - slookup pinfl u) ∩ post = {}" by blast
        then have B: "∀u. (slookup (fminsert pinfl1 x y) u - slookup pinfl u) ∩ (post - {y}) = {}"
          by (simp add: infl_upd_diff)
        then show ?case
        proof (cases "y ∈ c⇩w")
          case True
          then show ?thesis using B Iterate(6) by simp
        next
          case False
          then have "y ∈ c⇩n" using Query.prems(5,6) by auto
          then have "x ∈ dep T σ y" using Query.prems(7) by simp
          then have "y ∈ slookup pinfl x"
          proof -
            have "y ∈ post - c⇩w"
              using Query.prems(2,4,5) ‹y ∈ c⇩n› unfolding post_invariant_def narrowing_inv_def
              by auto
            then show ?thesis
              using Query.prems(4) ‹x ∈ dep T σ y› unfolding narrowing_inv_def by blast
          qed
          have "x ∈ post"
          proof (rule ccontr, goal_cases)
            case 1
            then have "slookup pinfl x = {}"
              using Query.prems(4) stabl_infl_empty unfolding narrowing_inv_def by metis
            then show ?case using ‹y ∈ slookup pinfl x› by simp
          qed
          then have "y ∈ slookup pinfl1 x"
            using IH ‹y ∈ slookup pinfl x› ‹x ∈ post› unfolding update_rel_nar_def by blast
          then have "slookup (fminsert pinfl1 x y) u = slookup pinfl1 u" for u
            by (cases "u = x") (auto simp add: slookup_fminsert_same slookup_fminsert_other)
          then have "∀u. (slookup (fminsert pinfl1 x y) u - slookup pinfl u) ∩ post = {}"
            using ‹∀u. (slookup pinfl1 u - slookup pinfl u) ∩ post = {}› by blast
          then show ?thesis using False Iterate(6) by blast
        qed
      qed
    qed (auto simp add: fminsert_def fmlookup_default_def)
  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 3
      have "{u ∈ c⇩w ∪ c⇩n. slookup infl' u ≠ {}} ⊆ p'"
        using Query.prems(3) Lookup(3,5) unfolding fminsert_def fmlookup_default_def points_inv_def
        by auto
      then show ?case
        using Query.prems(3) 3(1,3,5) unfolding points_inv_def points_inv_upd_def by auto
    next
      case 4
      then show ?case
        using Lookup(1,8) Query.prems(4) unfolding post_invariant_def narrowing_inv_def
      proof (intro conjI, goal_cases)
        case 5
        then show ?case
        proof (intro allI, goal_cases)
          case (1 u)
          show ?case
          proof (cases "u = x")
            case True
            then show ?thesis
              by (metis "1"(12) "5"(12) Diff_insert_absorb Lookup(3,8)
                  Un_mono diff_shunt insert_absorb insert_not_empty slookup_fminsert_same)
          next
            case False
            then show ?thesis
              by (metis "1"(12) "5"(12) Lookup(3,8) slookup_fminsert_other)
          qed
        qed
      qed (auto simp add: fminsert_def fmlookup_default_def)
    next
      case 5
      then show ?case
        unfolding update_rel_nar_def
      proof (intro conjI, goal_cases)
        case 4
        then show ?case
        proof (cases "y ∈ c⇩w")
          case True
          then show ?thesis using 4 by (auto simp add: fminsert_def fmlookup_default_def)
        next
          case False
          then have "y ∈ c⇩n" using Query.prems(5,6) by auto
          then have "x ∈ dep T σ y" using Query.prems(7) by simp
          then have "y ∈ slookup pinfl x"
          proof -
            have "y ∈ post - c⇩w"
              using Query.prems(2,4,5) ‹y ∈ c⇩n› unfolding post_invariant_def narrowing_inv_def
              by auto
            then show ?thesis using Query.prems(4) ‹x ∈ dep T σ y› unfolding narrowing_inv_def by blast
          qed
          then have "slookup (fminsert pinfl x y) u = slookup pinfl u" for u
            by (cases "u = x") (auto simp add: slookup_fminsert_same slookup_fminsert_other)
          then show ?thesis using False Lookup(8) by blast
        qed
      qed (auto simp add: fminsert_def fmlookup_default_def)
    qed (auto simp add: fminsert_def fmlookup_default_def update_rel_def)
  qed
next
  case (Iterate x c⇩w c⇩n infl stabl p σ wn pinfl post)
  have xstabl: "x ∈ insert x stabl" by simp
  have xcalled: "x ∈ c⇩w ∪ c⇩n" using Iterate.prems(9) by simp
  have called_dist: "c⇩w ∩ c⇩n = {}" using Iterate.prems(8) by simp
  have inv: "post_invariant (c⇩w ∪ c⇩n) σ infl (insert x stabl)"
    using post_invariant_simp_c_stabl eq_def Iterate.prems(2,3) xcalled by auto
  show ?case using Iterate.IH(1) Iterate.prems(1) xcalled
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    have "points_inv_upd p' (p - {x}) ((c⇩w ∪ c⇩n) - {x}) infl'"
      using Iterate.prems(4) Stable(3,5) unfolding points_inv_upd_def points_inv_def by auto
    then show ?thesis
      using Stable(1,3,4,6,7) Iterate.prems Iterate.IH(1)
      unfolding update_rel_nar_def update_rel_def by simp
  next
    case (Fixpoint p1)
    have A: "points_inv p (c⇩w ∪ c⇩n) infl"
      using Fixpoint(1) Iterate.prems(2-4) add_c_to_point_inv xcalled by (cases wn) auto
    have B: "narrowing_inv c⇩w σ infl (insert x stabl) pinfl (insert x post)"
      using Iterate.prems(2,5) xcalled unfolding narrowing_inv_def
      by auto
    have subt: "subt_for_prefix (T x) [] σ = Some (T x)" "set [] ⊆ insert x stabl" by auto

    note IH = Iterate.IH(2)[OF Fixpoint(1,4) xcalled inv A B called_dist subt, folded dep_def]

    have pinv': "post_invariant (c⇩w ∪ c⇩n - {x}) σ' infl' stabl'"
      using IH
      unfolding post_invariant_def
    proof(intro conjI, goal_cases)
      case 1
      then have "eq_subsumed σ' (stabl' - (c⇩w ∪ c⇩n - {x}))"
        using Fixpoint(5) unfolding 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

    have ninv: "narrowing_inv c⇩w σ' infl' stabl' pinfl' post'"
      using IH by auto

    show ?thesis using IH
    proof(intro conjI, goal_cases)
      case 1 then show ?case using pinv' by simp
    next
      case 2 then show ?case using Fixpoint(3) unfolding update_rel_def by (auto split: prod.splits)
    next
      case 3 then show ?case using Fixpoint(6) unfolding points_inv_upd_def points_inv_def by auto
    next
      case 4
      show ?case
        unfolding narrowing_inv_def
      proof (intro conjI, goal_cases)
        case 1
        then show ?case
        proof (intro ballI, goal_cases)
          case (1 u)
          then show ?case
          proof (cases "u = x")
            case True
            have "eq T x σ' ≤ mlup σ' x" using IH Fixpoint(5) by simp
            then show ?thesis using True by (auto simp add: fun_upd_same)
          next
            case False
            then show ?thesis using 1 4 unfolding narrowing_inv_def by simp
          qed
        qed
      next
        case 2
        then show ?case using IH unfolding narrowing_inv_def by auto
      next
        case 3
        show ?case using IH unfolding narrowing_inv_def by simp
      next
        case 4
        have "∀y∈dep T σ' x. x ∈ slookup pinfl' y"
          using IH unfolding update_rel_nar_def narrowing_inv_def by fast
        then show ?case using IH unfolding narrowing_inv_def by auto
      next
        case 5
        show ?case using IH narrowing_inv_def by fastforce
      qed
    next
      case 5
      then show ?case using 5 unfolding update_rel_nar_def
      proof (intro conjI, goal_cases)
        case 3
        then show ?case by blast
      next
        case 4
        have "post - (c⇩w - {x}) ∩ {x} = insert x post - c⇩w ∩ {x}"
          using Iterate.prems(2) Fixpoint(1) xcalled by blast
        then show ?case using 4 by auto
      qed auto
    next
      case 6
      then show ?case unfolding update_rel_def by simp
    qed
  next
    case (W_Fixpoint xd1 infl1 stabl1 p1 σ1 infl2 stabl2 pinfl1 post1)
    have A: "points_inv p (c⇩w ∪ c⇩n) infl"
      using Iterate.prems(2,3,4) W_Fixpoint(1) add_c_to_point_inv xcalled by (cases wn) auto
    have "slookup infl x = {}" using W_Fixpoint(1) Iterate.prems(3) unfolding post_invariant_def
      by (meson stabl_infl_empty)
    then have B: "narrowing_inv c⇩w σ infl (insert x stabl) pinfl (insert x post)"
      using Iterate.prems(2,5) W_Fixpoint(3) xcalled unfolding narrowing_inv_def by auto
    have subt: "subt_for_prefix (T x) [] σ = Some (T x)" "set [] ⊆ insert x stabl" by auto

    note IH = Iterate.IH(2)[OF W_Fixpoint(1,5) xcalled inv A B called_dist subt, folded dep_def]
    (* post-solution reached for x *)
    have post1_x: "eq T x σ1 ≤ mlup σ1 x"
      using IH W_Fixpoint(6) widening_ge le_sup_iff eq_def by metis

    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] W_Fixpoint(8) by auto

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

    have xd1_smaller: "xd1 ≤ mlup σ1 x" by (metis W_Fixpoint(6) le_sup_iff widening_ge)
    have sigma_narrow_smaller: "σ1(x ↦ mlup σ1 x Δ xd1) ⊑⇩m σ1"
    proof -
      have "mlup σ1 x Δ xd1 ≤ mlup σ1 x" using narrowing_le xd1_smaller by simp
      then show ?thesis 
        by (metis fun_upd_other fun_upd_same option.simps(5) order_class.order_eq_iff mlup_def)
    qed

    have "post_invariant ((c⇩w ∪ c⇩n) - {x}) σ1 infl2 stabl2"
      using destab_preserves_invariant[OF W_Fixpoint(8) _ stabl_inc] IH dep_def
        Iterate.prems(3)[unfolded post_invariant_def] post1_x
      by auto
    then have pinv1': "post_invariant ((c⇩w ∪ c⇩n) - {x}) (σ1(x ↦ mlup σ1 x Δ xd1)) infl2 stabl2"
      unfolding post_invariant_def
    proof (intro conjI, goal_cases)
      case 1
      then show ?case by simp
    next
      case 2
      have "eq T u (σ1(x ↦ mlup σ1 x Δ xd1)) ≤ eq T u σ1" for u
        using sigma_narrow_smaller assms(1) unfolding is_mono_eq_def by auto
      moreover have "eq T u σ1 ≤ mlup (σ1(x ↦ mlup σ1 x Δ xd1)) u"
        if "u ∈ stabl2 - (c⇩w ∪ c⇩n - {x})" for u
      proof (cases "u = x")
        case True
        then have "mlup (σ1(x ↦ mlup σ1 x Δ xd1)) u = mlup σ1 x Δ xd1"
          by (auto simp add: fun_upd_same mlup_def)
        moreover have "mlup σ1 x Δ xd1 ≥ xd1"
          by (metis inf.absorb_iff2 narrowing_ge xd1_smaller)
        ultimately show ?thesis using IH True by simp
      next
        case False
        then have "mlup (σ1(x ↦ mlup σ1 x Δ xd1)) u = mlup σ1 u"
          by (auto simp add: fun_upd_other mlup_def)
        then show ?thesis using that 2 by simp
      qed
      ultimately show ?case using order_trans by blast
    next
      case 3
      then show ?case by simp
    next
      case 4
      have "dep T (σ1(x ↦ mlup σ1 x Δ xd1)) y ⊆ dep T σ1 y" for y
        using sigma_narrow_smaller assms(2) unfolding mono_deps_def by auto
      moreover have "∀y∈stabl2 - (c⇩w ∪ c⇩n - {x}). ∀x∈dep T σ1 y. y ∈ slookup infl2 x"
        using Iterate.prems(2) 4 by force
      ultimately show ?case by blast
    qed

    have points_inv1: "points_inv (p1 - {x}) ((c⇩w ∪ c⇩n) - {x}) infl2"
      using IH continue_preserves_pinv W_Fixpoint(8) unfolding points_inv_upd_def by metis

    have "∀u. slookup infl2 u ⊆ slookup infl1 u" using infl2_def
      by (metis empty_iff fmlookup_default_drop_set set_empty2 subsetI)

    have "x ∈ p1" using W_Fixpoint(2) IH unfolding points_inv_upd_def by fast

    have nar_inv1: "narrowing_inv (Set.remove x c⇩w) (σ1(x ↦ mlup σ1 x Δ xd1)) infl2 stabl2 pinfl1 post1"
      using IH unfolding narrowing_inv_def
    proof (intro conjI, goal_cases)
      case 1
      then show ?case
      proof (intro ballI, goal_cases)
        case (1 u)
        have "eq T u (σ1(x ↦ mlup σ1 x Δ xd1)) ≤ eq T u σ1"
          using sigma_narrow_smaller assms(1) unfolding is_mono_eq_def by simp
        moreover have "eq T u σ1 ≤ mlup (σ1(x ↦ mlup σ1 x Δ xd1)) u"
        proof (cases "u = x")
          case True
          have "mlup (σ1(x ↦ mlup σ1 x Δ xd1)) u = mlup σ1 x Δ xd1"
            using True by (auto simp add: fun_upd_same mlup_def)
          moreover have "mlup σ1 x Δ xd1 ≥ xd1"
            using narrowing_ge xd1_smaller by (metis inf.absorb_iff2)
          ultimately show ?thesis using IH A True by simp
        next
          case False
          then have "eq T u σ1 ≤ mlup σ1 u" using 1 by simp
          then show ?thesis using False A by (auto simp add: fun_upd_other mlup_def)
        qed
        ultimately show ?case by auto
      qed
    next
      case 2
      then show ?case using W_Fixpoint(6) Iterate.prems(2) stabl2_def by auto
    next
      case 3
      then show ?case using W_Fixpoint(6) Iterate.prems(2) by auto
    next
      case 4
      have "dep T (σ1(x ↦ mlup σ1 x Δ xd1)) y ⊆ dep T σ1 y" for y
        using sigma_narrow_smaller assms(2) unfolding mono_deps_def by auto
      moreover have "∀y∈post1 - Set.remove x c⇩w. ∀x∈dep T σ1 y. y ∈ slookup pinfl1 x"
        using Iterate.prems(2) 4 by force
      ultimately show ?case by blast
    next
      case 5
      then show ?case
        by (metis subset_trans ‹∀u. slookup infl2 u ⊆ slookup infl1 u›)
    qed

    have "x ∈ post1" using IH update_rel_nar_def by force

    have A: "(x ∈ Set.remove x c⇩w ⟶ x ∉ post1 - stabl2) ∧ (x ∈ insert x c⇩n ⟶ x ∈ post1)"
      using ‹x ∈ post1› by simp
    have B: "post_invariant (Set.remove x c⇩w ∪ insert x c⇩n - {x}) (σ1(x ↦ mlup σ1 x Δ xd1)) infl2 stabl2"
      using pinv1' by (simp add: Un_Diff Set.remove_eq)
    have C: "points_inv (p1 - {x}) (Set.remove x c⇩w ∪ insert x c⇩n - {x}) infl2"
      using points_inv1 by (simp add: Un_Diff Set.remove_eq)
    have D: "narrowing_inv (Set.remove x c⇩w - {x}) (σ1(x ↦ mlup σ1 x Δ xd1)) infl2 stabl2 pinfl1 post1"
      using nar_inv1 by auto
    have E: "Set.remove x c⇩w ∩ insert x c⇩n = {}" using called_dist by auto
    have F: "x ∈ Set.remove x c⇩w ∪ insert x c⇩n" by blast
    have IH2: "post_invariant ((c⇩w ∪ c⇩n) - {x}) σ' infl' stabl' ∧ stabl2 ⊆ stabl' ∧
      update_rel x infl2 stabl2 infl' stabl' (σ1(x ↦ mlup σ1 x Δ xd1)) σ' ∧
      points_inv_upd p' (p1 - {x}) ((c⇩w ∪ c⇩n) - {x}) infl' ∧
      narrowing_inv (c⇩w - {x}) σ' infl' stabl' pinfl' post' ∧
      update_rel_nar x (c⇩w - {x}) (σ1(x ↦ mlup σ1 x Δ xd1)) σ' stabl2 post1 post' pinfl1 pinfl' ∧
      x ∈ stabl'"
      using Iterate.IH(3)[OF W_Fixpoint(1,5) _ _ _ _ _ _ _ W_Fixpoint(6) _ W_Fixpoint(7,8) _
        W_Fixpoint(10) A B C D _ _ E F, of "(infl1, stabl1, p1, σ1, pinfl1, post1)"
        "(stabl1, p1, σ1, pinfl1, post1)" "(p1, σ1, pinfl1, post1)" "(σ1, pinfl1, post1)"
        "(pinfl1, post1)", simplified] W_Fixpoint(2-3) ‹x ∈ p1› ‹x ∈ post1›
      unfolding update_rel_def by (simp add: Un_Diff Set.remove_eq)

    show ?thesis using IH IH2
    proof (intro conjI, goal_cases)
      case 2
      then show ?case unfolding update_rel_def
      proof (intro conjI, goal_cases)
        case 1
        then show ?case using IH2 stabl_inc by auto
      next
        case 2
        have "∀u∈stabl. slookup infl2 u ⊆ slookup infl' u" using stabl_inc 2(2) by auto
        moreover have "∀u∈ stabl. slookup infl1 u ⊆ slookup infl2 u"
          using fmlookup_default_drop_set[of "insert x (influenced_by infl1 x)" infl1]
            W_Fixpoint(1) infl2_def stabl2_def stabl_inc by auto
        ultimately show ?case using 2(1) by fast
      next
        case 3
        then show ?case using 2 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 W_Fixpoint(9,10) by auto
          next
            case False
            then show ?thesis
              using 1(2) inv[unfolded post_invariant_def] stabl_inc
              by fastforce
          qed
          moreover have "(slookup infl1 ξ - slookup infl ξ) ∩ stabl = {}"
            using W_Fixpoint(1) Iterate.prems(3) IH stabl_infl_empty[of x stabl infl]
            unfolding update_rel_def
            by auto
          ultimately show ?case using infl2_def stabl2_def by blast
        qed
      next
        case 4
        then have "∀ξ∈stabl. mlup (σ1(x ↦ mlup σ1 x Δ xd1)) ξ = mlup σ' ξ"
          "∀u∈stabl. mlup σ u = mlup σ1 u" using stabl_inc unfolding update_rel_def by auto
        moreover have "∀ξ∈stabl. mlup σ1 ξ = mlup (σ1(x ↦ mlup σ1 x Δ xd1)) ξ"
          using W_Fixpoint(1) by (metis fun_upd_other mlup_def)
        ultimately show ?case by auto
      qed
    next
      case 3
      then show ?case unfolding points_inv_upd_def points_inv_def by auto
    next
      case 5
      then show ?case unfolding update_rel_nar_def
      proof (intro conjI, goal_cases)
        case 1
        then have "post ⊆ post1" and "post1 ⊆ post'" by auto
        moreover have "post1 ⊆ post1" using W_Fixpoint(6) by auto
        ultimately show ?case by simp
      next
        case 2
        then have "∀u∈post. mlup σ1 u ≤ mlup σ u"
          "∀u∈post1. mlup σ' u ≤ mlup (σ1(x ↦ mlup σ1 x Δ xd1)) u"
          by auto
        moreover have "post ⊆ post1" using 2(1) W_Fixpoint(6) by auto
        moreover have "post1 ⊆ post'" using 2(2) by simp
        ultimately show ?case using sigma_narrow_smaller by (meson order.trans subset_eq)
      next
        case 3
        then show ?case by (meson insertCI stabl_inc subset_eq)
      next
        case 4
        then show ?case
        proof(intro allI, goal_cases)
          case (1 ξ)
          have "(slookup pinfl' ξ - slookup pinfl1 ξ) ∩ post = {}"
          proof (cases "x ∈ stabl2")
            case True
            then show ?thesis using W_Fixpoint(9,10) by auto
          next
            case False
            have "∀u. (slookup pinfl' u - slookup pinfl1 u) ∩ (post1 - (c⇩w - {x}) ∩ {x}) = {}"
              using 1(2) by simp
            moreover have "post ⊆ post1 - (c⇩w - {x}) ∩ {x}" using 4(1) by auto
            ultimately show ?thesis by blast
          qed
          moreover have "(slookup pinfl1 ξ - slookup pinfl ξ) ∩ post = {}"
          proof -
            have "(slookup pinfl1 ξ - slookup pinfl ξ) ∩ (insert x post - c⇩w ∩ {x}) = {}"
              using W_Fixpoint(1) Iterate.prems(3) IH stabl_infl_empty[of x post pinfl] 4(1)
              by auto
            moreover have "post ⊆ insert x post - c⇩w ∩ {x}"
            proof (cases "x ∈ post")
              case True
              then show ?thesis using Iterate.prems(2) W_Fixpoint(1) by blast
            next
              case False
              then have "x ∈ c⇩w" using Iterate.prems(2) xcalled by force
              then show ?thesis using False by simp
            qed
            ultimately show ?thesis by blast
          qed
          ultimately show ?case using infl2_def stabl2_def by blast
        qed
      qed
    qed auto
  next
    case (N_Fixpoint xd1 p1)
    have T: "points_inv p (c⇩w ∪ c⇩n) infl"
      using Iterate.prems(2-4) N_Fixpoint(1) add_c_to_point_inv xcalled by blast
    have "slookup infl x = {}" using N_Fixpoint(1) Iterate.prems(3) unfolding post_invariant_def
      by (meson stabl_infl_empty)
    then have B: "narrowing_inv c⇩w  σ infl (insert x stabl) pinfl (insert x post)"
    proof (cases "x ∈ c⇩w")
      case True
      then have "x ∉ post" using Iterate.prems(2) N_Fixpoint(1) by simp
      then show ?thesis using Iterate.prems(5) True unfolding narrowing_inv_def by blast
    next
      case False
      then have "x ∈ c⇩n" using xcalled called_dist by simp
      then show ?thesis using Iterate.prems(2,5) unfolding narrowing_inv_def by auto
    qed

    have subt: "subt_for_prefix (T x) [] σ = Some (T x)" "set [] ⊆ insert x stabl" by auto

    note IH = Iterate.IH(2)[OF N_Fixpoint(1,5) xcalled inv T B called_dist subt, folded dep_def]

    have post_x: "eq T x σ' ≤ mlup σ' x"
    proof (cases "x ∈ c⇩w")
      case True
      then have "wn = Widening" using Iterate.prems(6) called_dist by (cases wn) auto
      then have "mlup σ' x ∇ xd1 = mlup σ' x" using N_Fixpoint(3) by simp
      then have "xd1 ≤ mlup σ' x" by (metis le_sup_iff widening_ge)
      then show ?thesis using IH by auto
    next
      case False
      then have "x ∈ post' - c⇩w" using IH unfolding update_rel_nar_def by blast
      then show ?thesis using IH unfolding update_rel_nar_def narrowing_inv_def by metis
    qed

    have "post_invariant ((c⇩w ∪ c⇩n) - {x}) σ' infl' stabl'"
      using IH N_Fixpoint(2,3) post_x unfolding post_invariant_def by auto

    moreover have "points_inv_upd p' (p - {x}) ((c⇩w ∪ c⇩n) - {x}) infl'"
      using IH N_Fixpoint(8) unfolding points_inv_upd_def points_inv_def by auto

    moreover have "narrowing_inv (c⇩w - {x}) σ' infl' stabl' pinfl' post'"
      using IH
      unfolding narrowing_inv_def
    proof (intro conjI, goal_cases)
      case 1
      then show ?case
      proof (intro ballI, goal_cases)
        case (1 u)
        then show ?case
        proof (cases "u = x")
          case True
          have "eq T x σ' ≤ mlup σ' x" using post_x by simp
          then show ?thesis using N_Fixpoint(8) True by (auto simp add: fun_upd_same)
        next
          case False
          then have "u ∈ post'" using N_Fixpoint(8) 1 by simp
          then show ?thesis using 1 False by blast
        qed
      qed
    next
      case 2
      then show ?case using Iterate.prems(2) xstabl N_Fixpoint(8) by auto
    next
      case 3
      then show ?case using N_Fixpoint(8) Iterate.prems(2) by blast
    next
      case 4
      then show ?case using N_Fixpoint(8) Iterate.prems(2) by blast
    next
      case 5
      then show ?case by meson
    qed

    moreover have "post ⊆ post'" using IH N_Fixpoint(8) unfolding update_rel_nar_def by auto

    moreover have "(slookup pinfl' u - slookup pinfl u) ∩ (post - (c⇩w - {x}) ∩ {x}) = {}" for u
    proof (cases "x ∈ c⇩w")
      case True
      then have "x ∉ post" using Iterate.prems(2) N_Fixpoint(1) by simp
      then show ?thesis using IH True update_rel_nar_def by auto
    next
      case False
      then show ?thesis using IH update_rel_nar_def by auto
    qed

    ultimately show ?thesis
      using IH N_Fixpoint(8) unfolding post_invariant_def update_rel_nar_def update_rel_def by auto
  next
    case (Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2 pinfl1 post1 pinfl2 post2)
    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

    have A: "points_inv p (c⇩w ∪ c⇩n) infl"
      using Iterate.prems(2-4) Continue(1) add_c_to_point_inv xcalled by blast
    have "slookup infl x = {}" using Continue(1) Iterate.prems(3) unfolding post_invariant_def
      by (meson stabl_infl_empty)
    moreover have "insert x post - c⇩w = post - (c⇩w - {x})"
      using Iterate.prems(2) Continue(1) xcalled by blast
    ultimately have B: "narrowing_inv c⇩w σ infl (insert x stabl) pinfl (insert x post)"
      using Iterate.prems(2,5,6) xcalled unfolding narrowing_inv_def by auto
    have subt: "subt_for_prefix (T x) [] σ = Some (T x)" "set [] ⊆ insert x stabl" by auto

    note IH = Iterate.IH(2)[OF Continue(1,3) xcalled inv A B called_dist subt]

    have "p ⊆ p1" using IH Continue(2) unfolding points_inv_def points_inv_upd_def by auto

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

    have infl_closed: "(∀x∈stabl1 - ((c⇩w ∪ c⇩n) - {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⇩w ∪ c⇩n) - {x})" for y
      using that destab_x_no_dep[OF Continue(6) infl_closed] by fastforce

    have in_post_N: "x ∈ post" if "wn = Narrowing"
      using Iterate.prems(2,6) that by fastforce

    have "post ⊆ post1" using IH unfolding update_rel_nar_def by simp
    have I1: "∀z ∈ dep T σ1 x. x ∈ slookup infl1 z" using IH unfolding dep_def by auto

    have post_dom_incr: "post ⊆ post2"
      using post_dom_incr IH Iterate.prems(2,3,5) Continue(1,7) called_dist xcalled
      unfolding update_rel_nar_def
      by (smt (verit, best))

    have post1_x: "eq T x σ1 ≤ mlup σ1 x" if "x ∈ post"
    proof -
      have "x ∈ c⇩n" and "x ∉ c⇩w"
        using Iterate.prems(2) Continue(1) that xcalled by auto
      then show ?thesis using IH that unfolding update_rel_nar_def narrowing_inv_def by auto
    qed

    have "p ⊆ p1" using IH unfolding points_inv_def points_inv_upd_def by simp

    have inv: "post_invariant ((c⇩w ∪ c⇩n) - {x}) (σ1(x ↦ d_new)) infl2 stabl2"
      using post_inv_after_destab[OF Continue(4,6) Iterate.prems(3,7) stabl_inc] post1_x in_post_N
        IH x_no_dep using x_no_dep unfolding update_rel_def by auto

    have ninv1: "narrowing_inv (c⇩w - {x}) (σ1(x ↦ d_new)) infl2 stabl2 pinfl2 post2"
      using narrow_inv_after_destab[OF assms(1,2) Continue(4,5,6,7) Iterate.prems(2,3,5-7) _
          stabl_inc _ xcalled called_dist inv] in_post_N post1_x x_no_dep IH by auto

    have d_new:
        "d_new = (if x ∉ p then xd1 else if wn = Widening then mlup σ1 x ∇ xd1 else mlup σ1 x Δ xd1)"
      using Continue(4) by simp

    have pointsinv1: "points_inv (p1 - {x}) ((c⇩w ∪ c⇩n) - {x}) infl2"
      using continue_preserves_pinv[OF Continue(6)[symmetric]] IH infl2_def
      unfolding points_inv_upd_def by simp
    have P2: "x ∉ p1 ⟶ wn = Widening" using ‹p ⊆ p1› Iterate.prems(7) by blast
    have "x ∈ stabl1" "x ∈ post1" using IH unfolding update_rel_nar_def update_rel_def by auto
    then have P3: "(x ∈ c⇩w ⟶ x ∉ post2 - stabl2) ∧ (x ∈ c⇩n ⟶ x ∈ post2)"
      using c_post_after_destab[OF Iterate.prems(2) called_dist xcalled Continue(1,6,7)
          post_dom_incr Iterate.prems(5)] IH
      unfolding dep_def by auto

    have dnew_smaller_if_x_post: "d_new ≤ mlup σ1 x" if "x ∈ post - c⇩w"
      using IH Continue(4) narrowing_le post1_x widening_bounded that by force

    note ih = Iterate.IH(4)[OF Continue(1,3) _ _ _ _ _ _ d_new Continue(5,6) _
        Continue(7) _ Continue(9) P3 inv pointsinv1 ninv1 Iterate.prems(6) P2 called_dist
        xcalled, of "(infl1, stabl1, p1, σ1, pinfl1, post1)" "(stabl1, p1, σ1, pinfl1, post1)"
        "(p1, σ1, pinfl1, post1)" "(σ1, pinfl1, post1)" "(pinfl1, post1)", simplified]
    then show ?thesis using IH
    proof(intro conjI, goal_cases)
      case 1
      then show ?case by simp
    next
      case 2
      then show ?case unfolding update_rel_def
      proof (intro conjI, goal_cases)
        case 1
        then show ?case using ih stabl_inc by auto
      next
        case 2
        then have "∀u∈stabl. slookup infl2 u ⊆ slookup infl' u" using stabl_inc by auto
        moreover have "∀u ∈ stabl. slookup infl1 u ⊆ slookup infl2 u"
          using fmlookup_default_drop_set[of "insert x (influenced_by infl1 x)" infl1] infl2_def
            stabl2_def Continue(1) stabl_inc by auto
        ultimately show ?case using 2(2) by fast
      next
        case 3
        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(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 Continue(1) Iterate.prems(3) 3(2) stabl_infl_empty[of x stabl infl]
            by auto
          ultimately show ?case using infl2_def stabl2_def by blast
        qed
      next
        case 4
        then have "∀ξ∈stabl. mlup (σ1(x ↦ d_new)) ξ = mlup σ' ξ" using stabl_inc by auto
        moreover have "∀ξ∈insert x stabl. mlup σ ξ = mlup σ1 ξ" using 4(2) by simp
        moreover have "∀ξ∈stabl. mlup σ1 ξ = mlup (σ1(x ↦ d_new)) ξ"
          using Continue(1) by (simp add: mlup_eq_mupd_set)
        ultimately show ?case by auto
      qed
    next
      case 4 then show ?case using IH by auto
    next
      case 3
      then show ?case unfolding points_inv_upd_def by blast
    next
      case 5
      then show ?case unfolding update_rel_nar_def
      proof (intro conjI, goal_cases)
        case 1
        then have "post2 ⊆ post'" by simp
        then show ?case using post_dom_incr by simp
      next
        case 2
        have "∀u∈post. mlup σ1 u ≤ mlup σ u" using IH unfolding update_rel_nar_def by simp
        moreover have "∀u∈post. mlup σ' u ≤ mlup (σ1(x ↦ d_new)) u"
          using ih post_dom_incr unfolding update_rel_nar_def by blast
        moreover have "∀u∈post. mlup (σ1(x ↦ d_new)) u ≤ mlup σ1 u"
        proof (intro ballI, goal_cases)
          case (1 u)
          then show ?case
          proof (cases "u = x")
            case True
            have "x ∉ c⇩w" using 1 Iterate.prems(2,7) True Continue(1,2) by blast
            then show ?thesis
              using dnew_smaller_if_x_post True 1 by (auto simp add: fun_upd_same mlup_def)
          next
            case False
            then show ?thesis by (auto simp add: fun_upd_other mlup_def)
          qed
        qed
        ultimately show ?case by force
      next
        case 3
        show ?case
        proof(intro allI subsetI, goal_cases)
          case (1 ξ u)
          then have "ξ ∈ post"
            using Iterate.prems(5) unfolding narrowing_inv_def
            by (metis stabl_infl_empty empty_iff)
          then show ?case
          proof (cases "x ∈ post")
            case True
            then have "pinfl2 = pinfl1" "post2 = post1"
              using Continue(7) unfolding destab_post_def by auto
            moreover have "slookup pinfl ξ ⊆ slookup pinfl1 ξ" "ξ ∈ post1"
              using ‹ξ ∈ post› IH unfolding update_rel_nar_def by auto
            moreover have "slookup pinfl2 ξ ⊆ slookup pinfl' ξ"
              using ‹ξ ∈ post1› ‹post2 = post1› 3 unfolding update_rel_nar_def by auto
            ultimately show ?thesis using 1(1) by auto
          next
            case False
            have "u ∈ slookup pinfl1 ξ" using IH 1 unfolding update_rel_nar_def by blast
            have destab_post: "(pinfl2, post2) = destab_barrier x pinfl1 post1 stabl2"
              using Continue(7) False unfolding destab_post_def by simp

            have "ξ ≠ x" using ‹ξ ∈ post› False by auto
            have "ξ ∈ post2" using ‹ξ ∈ post› post_dom_incr by blast
            then have "ξ ∉ insert x (influenced_by_cutoff pinfl1 x (stabl2 - {x})) - stabl2"
              using destab_post ‹ξ ∈ post› ‹ξ ≠ x›
              unfolding destab_barrier_def by auto
            then have "slookup pinfl1 ξ = slookup pinfl2 ξ"
              using destab_post fmlookup_default_drop_set unfolding destab_barrier_def
              by (auto simp add: fmlookup_default_drop_set)
            then have "u ∈ slookup pinfl2 ξ" using ‹u ∈ slookup pinfl1 ξ› by auto
            then show ?thesis using post_dom_incr 1(1) 3 by auto
          qed
        qed
      next
        case 4
        have "∀u. slookup pinfl2 u ⊆ slookup pinfl1 u"
        proof (cases ‹x ∈ post›)
          case True
          then show ?thesis using Continue(7) unfolding destab_post_def by simp
        next
          case False
          have "pinfl2 = fmdrop_set (insert x (influenced_by_cutoff pinfl1 x (stabl2 - {x})) - stabl2) pinfl1"
            using Continue(7) False unfolding destab_post_def destab_barrier_def by simp
          then show ?thesis by (simp add: fmlookup_default_drop_set subset_eq)
        qed
        moreover have "∀u. (slookup pinfl1 u - slookup pinfl u) ∩ post = {}"
        proof -
          have "∀u. (slookup pinfl1 u - slookup pinfl u) ∩ (insert x post - c⇩w ∩ {x}) = {}"
            using 4 IH Continue(1) unfolding update_rel_nar_def by auto
          then show ?thesis using Iterate.prems(2) Continue(1) by blast
        qed
        moreover have "∀u. (slookup pinfl' u - slookup pinfl2 u) ∩ post2 = {}"
          using 4 IH Continue(1) unfolding update_rel_nar_def by auto
        moreover have "post ⊆ post2" using Continue(1) post_dom_incr by auto
        ultimately show ?case by blast
      qed
    qed auto
  qed
next
  case (Eval x t c⇩w c⇩n infl stabl p σ pinfl post)
  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 pinfl1 post1)
    have "y ∈ dep_aux σ t" using Query(1) by auto
    have "x ∈ stabl" using Eval.prems(2,3) unfolding post_invariant_def by auto
    then have "subt_for_prefix (T x) pre σ = Some t" "set pre ⊆ stabl"
      using Eval.prems(7,8) by auto
    then have "t ∈ subt T σ x"
      using subt_for_prefix_implies_subt unfolding subt_def by fast
    then have y_dep_of_x: "y ∈ dep T σ x"
      by (simp add: Query(1) dep_def subt_def subt_implies_dep)
    note IH = Eval.IH(2)[OF Query(1,3) Eval.prems(3-6,2) y_dep_of_x]
    then have inv: "post_invariant (c⇩w ∪ c⇩n) σ1 infl1 stabl1" by simp
    have D: "points_inv p1 (c⇩w ∪ c⇩n) infl1" using IH unfolding points_inv_upd_def by simp
    have E: "narrowing_inv c⇩w σ1 infl1 stabl1 pinfl1 post1" using IH by simp

    have "mlup σ1 y = yd" by (meson Query(2) Query(3) query_fmlookup)

    have "subt_for_prefix (T x) pre σ1 = Some t"
      using IH Eval.prems(7,8) subt_for_prefix_same unfolding update_rel_def by (metis subsetD)
    moreover have "subt_for_prefix t [y] σ1 = Some (g yd)" using Query(1) ‹mlup σ1 y = yd› by simp
    ultimately have F1: "subt_for_prefix (T x) (pre @ [y]) σ1 = Some (g yd)"
      using subt_for_prefix_transitive by blast
    have "y ∈ stabl1"
      using IH stabl_infl_empty unfolding post_invariant_def by (metis empty_iff)
    then have F2: "set (pre @ [y]) ⊆ stabl1"
      using ‹set pre ⊆ stabl› IH  unfolding update_rel_def by auto

    have "t ∈ subt T σ1 x"
      using subt_for_prefix_implies_subt ‹subt_for_prefix (T x) pre σ1 = Some t›
      unfolding subt_def by fast
    then have F: "g yd ∈ subt T σ1 x"
      using Query(1) subt_aux.step[of t σ1 "T x" y g] ‹mlup σ1 y = yd›
      unfolding subt_def by auto

    note ih = Eval.IH(3)[OF Query(1,3) _ _ _ _ _ _ Query(5) Eval.prems(2) inv D E Eval.prems(6) F1 F2,
        of "(infl1, stabl1, p1, σ1, pinfl1, post1)" "(stabl1, p1, σ1, pinfl1, post1)"
        "(p1, σ1, pinfl1, post1)" "(σ1, pinfl1, post1)" "(pinfl1, post1)", 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 unfolding update_rel_def by fastforce
    then have mlup: "mlup σ' y = yd"
      using Query(2,3) query_fmlookup by metis

    show ?thesis using ih IH
    proof(intro conjI, goal_cases)
      case 2
      then show ?case unfolding update_rel_def
      proof (intro conjI, goal_cases)
        case 1
        then show ?case by (metis subset_trans)
      next
        case 2
        then show ?case by (meson subset_trans in_mono)
      next
        case 3
        then show ?case using infl_diff_eval_step by (metis (no_types, opaque_lifting))
      next
        case 4
        then show ?case by (metis in_mono)
      qed
    next
      case 3
      then show ?case unfolding points_inv_def points_inv_upd_def by auto 
    next
      case 4
      show ?case using ih by simp
    next
      case 5
      then show ?case unfolding update_rel_nar_def
      proof (intro conjI, goal_cases)
        case 1
        then show ?case by (simp add: subset_iff)
      next
        case 2
        then show ?case by (meson order_trans subsetD)
      next
        case 3
        then show ?case by (meson dual_order.trans subsetD)
      next
        case 4
        then show ?case
        proof (cases "x ∈ c⇩w")
          case True
          then have A: "∀u. (slookup pinfl1 u - slookup pinfl u) ∩ (post - {x}) = {}" and
            B: "∀u. (slookup pinfl' u - slookup pinfl1 u) ∩ (post1 - {x}) = {}" using 4 by auto
          show ?thesis using infl_diff_eval_step[OF _ B A] 4(2) True by simp
        next
          case False
          then have A: "∀u. (slookup pinfl1 u - slookup pinfl u) ∩ post = {}" and
            B: "∀u. (slookup pinfl' u - slookup pinfl1 u) ∩ post1 = {}" using 4 by auto
          then show ?thesis using infl_diff_eval_step_2[OF _ B A] 4(2) False by simp
        qed
      qed
    next
      case 6
      then show ?case by (simp add: Query(1) mlup)
    next
      case 7
      then show ?case using Query(1) ‹y ∈ stabl1› mlup unfolding update_rel_def by fastforce
    qed auto
  next
    case Answer
    then show ?thesis
      using Eval.prems(2-5)
      unfolding narrowing_inv_def update_rel_nar_def update_rel_def points_inv_upd_def
      by (auto split: prod.splits)
  qed
qed

corollary partial_correctness:
  assumes "is_mono_eq T"
      and "mono_deps T"
      and "solve_dom x"
      and "solve x = (stabl, σ)"
    shows "part_post_solution T x σ stabl"
proof -
  note dom = assms(3)[unfolded solve_dom_def]
  obtain xd infl p pinfl post where app: "(xd, infl, stabl, p, σ, pinfl, post)
      = iterate x {x} {} fmempty {} {} Map.empty Widening fmempty {}"
    using assms unfolding solve_def
    by (cases "iterate x {x} {} fmempty {} {} Map.empty Widening fmempty {}") auto
  show ?thesis
    using partial_correctness_ind(2)[OF assms(1,2) dom app] dep_subset_stable[of infl stabl "{}"]
    unfolding solve_dom_def post_invariant_def points_inv_def narrowing_inv_def
    by auto
qed

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


subsection ‹Equivalence of Starting with Widening or Narrowing Phase for Post Unknowns›

context TD_wn_post
begin

lemma widening_for_narrowing_iterate:
  assumes "is_mono_eq T"
    and "mono_deps T"
    and "iterate_dom x c⇩w c⇩n infl stabl p σ Narrowing pinfl post"
    and "(xd, infl', stabl', p', σ', pinfl', post') = iterate x c⇩w c⇩n infl stabl p σ Narrowing pinfl post"
    and "post_invariant ((c⇩w ∪ c⇩n) - {x}) σ infl stabl"
    and "points_inv (p - {x}) ((c⇩w ∪ c⇩n) - {x}) infl"
    and "narrowing_inv (c⇩w - {x}) σ infl stabl pinfl post"
    and "x ∈ p"
    and "c⇩w ∩ c⇩n = {}"
    and "x ∈ c⇩n"
    and "x ∈ post"
    shows "iterate_dom x c⇩w c⇩n infl stabl p σ Widening pinfl post
      ∧ (xd, infl', stabl', p', σ', pinfl', post') = iterate x c⇩w c⇩n infl stabl p σ Widening pinfl post"
proof -
  have xcalled: "x ∈ c⇩w ∪ c⇩n" using assms(10) by simp
  show ?thesis using assms(3,4) xcalled
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then have "iterate_dom x c⇩w c⇩n infl stabl p σ Widening pinfl post"
      using query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post Widening] by auto
    then show ?thesis using iterate.psimps Stable by simp
  next
    case (Fixpoint p1)
    then have "iterate_dom x c⇩w c⇩n infl stabl p σ Widening pinfl post"
      using query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post Widening]
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") fastforce
    then show ?thesis
      using iterate.psimps[of x c⇩w c⇩n infl stabl p σ Widening pinfl post] Fixpoint
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
  next
    case (W_Fixpoint xd1 infl1 stabl1 p1 σ1 infl2 stabl2 pinfl1 post1)
    then show ?thesis by blast
  next
    case (N_Fixpoint xd1 p1)
    have narrow_fix: "mlup σ' x Δ xd1 = mlup σ' x" using N_Fixpoint(6,7) by simp

    have "post_invariant (c⇩w ∪ c⇩n) σ infl (insert x stabl)"
      using assms(5) xcalled post_invariant_simp_c_stabl by auto
    moreover have "points_inv p (c⇩w ∪ c⇩n) infl"
      using assms(5,6) N_Fixpoint(1) ‹x ∈ c⇩w ∪ c⇩n› add_c_to_point_inv by auto
    moreover have "narrowing_inv c⇩w σ infl (insert x stabl) pinfl (insert x post)"
      using xcalled assms(7,9,10,11) narrow_inv_add_x_stabl_and_post by blast
    ultimately have parCorr: "post_invariant (c⇩w ∪ c⇩n) σ' infl' stabl' ∧
      update_rel x infl (insert x stabl) infl' stabl' σ σ' ∧
      points_inv_upd p1 p (c⇩w ∪ c⇩n) infl' ∧
      narrowing_inv c⇩w σ' infl' stabl' pinfl' post' ∧
      update_rel_nar x c⇩w σ σ' (insert x stabl) (insert x post) post' pinfl pinfl' ∧
      traverse_rhs (T x) σ' = xd1 ∧ (∀y∈dep_aux σ' (T x). x ∈ slookup infl' y)"
      using partial_correctness_ind(3)[OF assms(1,2) N_Fixpoint(4,5) xcalled, of "[]"] assms(9)
      by auto
    have "xd1 ≤ mlup σ' x"
    proof -
      have "x ∉ c⇩w" using assms(9,10) by auto
      then have "x ∈ post' - c⇩w" using parCorr unfolding update_rel_nar_def by auto
      then show ?thesis using parCorr unfolding narrowing_inv_def by auto
    qed
    then have widen_fix: "mlup σ' x = mlup σ' x ∇ xd1" using widening_bounded by auto

    have "iterate_dom x c⇩w c⇩n infl stabl p σ Widening pinfl post"
      using N_Fixpoint(1,2,4,5) widen_fix narrow_fix query_iterate_eval.domintros(2)[of x stabl c⇩w
          c⇩n infl p σ pinfl post Widening] by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl
          (insert x post)", cases "destab x infl' stabl'") auto
    then show ?thesis
      using N_Fixpoint(1,2,4,5,7,8) widen_fix narrow_fix iterate.psimps[of x c⇩w c⇩n infl stabl p σ Widening
          pinfl post] by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
  next
    case (Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2 pinfl1 post1 pinfl2 post2)
    have narrow_not_fix: "mlup σ1 x Δ xd1 ≠ mlup σ1 x" using assms(8) Continue(4,5) by auto
    have d_new: "d_new = mlup σ1 x Δ xd1" using assms(8) Continue(4,5) by auto
    have "x ∈ post" using assms(5,11) by blast
    then have no_destab_post: "pinfl2 = pinfl1" "post2 = post1"
      using Continue(7) unfolding destab_post_def by auto
    have called_upd: "Set.remove x c⇩w = c⇩w" "insert x c⇩n = c⇩n" using assms(9,10) by auto

    have "post_invariant (c⇩w ∪ c⇩n) σ infl (insert x stabl)"
      using assms(5) ‹x ∈ c⇩w ∪ c⇩n› post_invariant_simp_c_stabl by auto
    moreover have "points_inv p (c⇩w ∪ c⇩n) infl"
      using assms(5,6,10) Continue(1) add_c_to_point_inv by auto
    moreover have "narrowing_inv c⇩w σ infl (insert x stabl) pinfl (insert x post)"
      using assms(7,9-11) narrow_inv_add_x_stabl_and_post by blast
    ultimately have parCorr: "post_invariant (c⇩w ∪ c⇩n) σ1 infl1 stabl1 ∧
      update_rel x infl (insert x stabl) infl1 stabl1 σ σ1 ∧
      points_inv_upd p1 p (c⇩w ∪ c⇩n) infl1 ∧
      narrowing_inv c⇩w σ1 infl1 stabl1 pinfl1 post1 ∧
      update_rel_nar x c⇩w σ σ1 (insert x stabl) (insert x post) post1 pinfl pinfl1 ∧
      traverse_rhs (T x) σ1 = xd1 ∧ (∀y∈dep_aux σ1 (T x). x ∈ slookup infl1 y)"
      using partial_correctness_ind(3)[OF assms(1,2) Continue(2,3) _, of "[]"] assms(9-10)
      by auto
    then have "xd1 ≤ mlup σ1 x"
    proof -
      have "x ∉ c⇩w" using assms(9-10) by auto
      then have "x ∈ post1 - c⇩w" using parCorr unfolding update_rel_nar_def by auto
      then show ?thesis using parCorr unfolding narrowing_inv_def by auto
    qed
    then have widen_fix: "mlup σ1 x = mlup σ1 x ∇ xd1" using widening_bounded by auto
    have "iterate_dom x c⇩w c⇩n infl stabl p σ Widening pinfl post"
      using Continue(1-3,6,8) assms(8) called_upd no_destab_post d_new widen_fix
        narrow_not_fix query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post Widening]
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
          cases "destab x infl1 stabl1") auto
    then show ?thesis
      using Continue(1,3,6,9) assms(8) iterate.psimps[of x c⇩w c⇩n infl stabl p σ Widening pinfl post]
        widen_fix narrow_not_fix d_new no_destab_post called_upd
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
          cases "destab x infl1 stabl1") auto
  qed
qed

lemma narrowing_for_widening_iterate:
  assumes "is_mono_eq T"
    and "mono_deps T"
    and "iterate_dom x c⇩w c⇩n infl stabl p σ Widening pinfl post"
    and "(xd, infl', stabl', p', σ', pinfl', post') = iterate x c⇩w c⇩n infl stabl p σ Widening pinfl post"
    and "post_invariant ((c⇩w ∪ c⇩n) - {x}) σ infl stabl"
    and "points_inv (p - {x}) ((c⇩w ∪ c⇩n) - {x}) infl"
    and "narrowing_inv (c⇩w - {x}) σ infl stabl pinfl post"
    and "x ∈ p"
    and "c⇩w ∩ c⇩n = {}"
    and "x ∈ c⇩n"
    and "x ∈ post"
    shows "iterate_dom x c⇩w c⇩n infl stabl p σ Narrowing pinfl post
    ∧ (xd, infl', stabl', p', σ', pinfl', post') = iterate x c⇩w c⇩n infl stabl p σ Narrowing pinfl post"
proof -
  have "x ∈ c⇩w ∪ c⇩n" using assms(10) by simp
  show ?thesis using assms(3,4) ‹x ∈ c⇩w ∪ c⇩n›
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then have "iterate_dom x c⇩w c⇩n infl stabl p σ Narrowing pinfl post"
      using query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post Narrowing] by auto
    then show ?thesis using iterate.psimps Stable by simp
  next
    case (Fixpoint p1)
    then have "iterate_dom x c⇩w c⇩n infl stabl p σ Narrowing pinfl post"
      using query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post Narrowing]
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") fastforce
    then show ?thesis
      using iterate.psimps[of x c⇩w c⇩n infl stabl p σ Narrowing pinfl post] Fixpoint
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
  next
    case (W_Fixpoint xd1 infl1 stabl1 p1 σ1 infl2 stabl2 pinfl1 post1)
    obtain pinfl2 post2 where destab_post: "(pinfl2, post2) = destab_post x post pinfl1 post1 stabl2"
      by (cases "destab_post x post pinfl1 post1 stabl2") auto
    have c_simp: "Set.remove x c⇩w = c⇩w" "insert x c⇩n = c⇩n" using assms(9,10) by auto
    then have i2_N_dom: "iterate_dom x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ mlup σ1 x Δ xd1)) Narrowing pinfl2 post2"
      using W_Fixpoint(9) assms(11) destab_post unfolding destab_post_def
      by (auto split: if_splits)
    then have i_dom_N: "iterate_dom x c⇩w c⇩n infl stabl p σ Narrowing pinfl post"
      using W_Fixpoint(1,4,5,6,2,8) destab_post query_iterate_eval.domintros(2)[folded dom_defs, of
          x stabl c⇩w c⇩n infl p σ pinfl post Narrowing]
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
          cases "destab x infl1 stabl1", cases "destab_post x post pinfl1 post1 stabl2")
         (auto simp del: eval.psimps)
    have i_val_N: "iterate x c⇩w c⇩n infl stabl p σ Narrowing pinfl post =
        iterate x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ mlup σ1 x Δ xd1)) Narrowing pinfl1 post1"
      using W_Fixpoint(1,5,2,7,8) destab_post assms(11) iterate.psimps[OF i_dom_N[unfolded dom_defs]]
      unfolding destab_post_def
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
          cases "destab x infl1 stabl1") auto

    have i_dom_W: "iterate_dom x c⇩w c⇩n infl stabl p σ Widening pinfl post"
      using W_Fixpoint(1,4,5,6,7,2,8,9) query_iterate_eval.domintros(2)[folded dom_defs, of x stabl c⇩w c⇩n infl p σ pinfl post Widening]
      unfolding destab_post_def
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
          cases "destab x infl1 stabl1") auto
    have "iterate x c⇩w c⇩n infl stabl p σ Widening pinfl post =
        iterate x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ mlup σ1 x Δ xd1)) Narrowing pinfl1 post1"
      using iterate.psimps[OF i_dom_W[unfolded dom_defs]] W_Fixpoint(1,2,5,6,7,8) c_simp
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
          cases "destab x infl1 stabl1") auto
    then show ?thesis using i_dom_N i_val_N assms(4) by auto
  next
    case (N_Fixpoint xd1 p1)
    have narrow_fix: "mlup σ' x Δ xd1 = mlup σ' x" using N_Fixpoint(6,7) by simp

    have "post_invariant (c⇩w ∪ c⇩n) σ infl (insert x stabl)"
      using assms(5,10) post_invariant_simp_c_stabl by auto
    moreover have "points_inv p (c⇩w ∪ c⇩n) infl"
      using assms(5,6) N_Fixpoint(1) ‹x ∈ c⇩w ∪ c⇩n› add_c_to_point_inv by auto
    moreover have "narrowing_inv c⇩w σ infl (insert x stabl) pinfl (insert x post)"
      using assms(7,9-11) narrow_inv_add_x_stabl_and_post by blast
    ultimately have parCorr: "post_invariant (c⇩w ∪ c⇩n) σ' infl' stabl' ∧
      update_rel x infl (insert x stabl) infl' stabl' σ σ' ∧
      points_inv_upd p1 p (c⇩w ∪ c⇩n) infl' ∧
      narrowing_inv c⇩w σ' infl' stabl' pinfl' post' ∧
      update_rel_nar x c⇩w σ σ' (insert x stabl) (insert x post) post' pinfl pinfl' ∧
      traverse_rhs (T x) σ' = xd1 ∧ (∀y∈dep_aux σ' (T x). x ∈ slookup infl' y)"
      using partial_correctness_ind(3)[OF assms(1,2) N_Fixpoint(4,5) _, of "[]"] assms(9,10)
      by auto
    then have "xd1 ≤ mlup σ' x"
    proof -
      have "x ∉ c⇩w" using assms(9,10) by auto
      then have "x ∈ post' - c⇩w" using parCorr unfolding update_rel_nar_def by auto
      then show ?thesis using parCorr unfolding narrowing_inv_def by auto
    qed
    then have widen_fix: "mlup σ' x = mlup σ' x ∇ xd1" using widening_bounded by auto

    have "iterate_dom x c⇩w c⇩n infl stabl p σ Narrowing pinfl post"
      using N_Fixpoint(1,2,4,5) widen_fix narrow_fix query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post Narrowing]
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)", cases "destab x infl' stabl'")
         auto
    then show ?thesis
      using N_Fixpoint(1,2,4,5,7,8) widen_fix narrow_fix iterate.psimps[of x c⇩w c⇩n infl stabl p σ Narrowing pinfl post]
      by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
  next
    case (Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2 pinfl1 post1 pinfl2 post2)
    have widen_not_fix: "mlup σ1 x ∇ xd1 ≠ mlup σ1 x" using assms(8) Continue(4,5) by auto

    have "post_invariant (c⇩w ∪ c⇩n) σ infl (insert x stabl)"
      using assms(5) ‹x ∈ c⇩w ∪ c⇩n› post_invariant_simp_c_stabl by auto
    moreover have "points_inv p (c⇩w ∪ c⇩n) infl"
      using assms(5,6,10) Continue(1) add_c_to_point_inv by auto
    moreover have "narrowing_inv c⇩w σ infl (insert x stabl) pinfl (insert x post)"
      using assms(7,9-11) narrow_inv_add_x_stabl_and_post by blast
    ultimately have parCorr: "post_invariant (c⇩w ∪ c⇩n) σ1 infl1 stabl1 ∧
      update_rel x infl (insert x stabl) infl1 stabl1 σ σ1 ∧
      points_inv_upd p1 p (c⇩w ∪ c⇩n) infl1 ∧
      narrowing_inv c⇩w σ1 infl1 stabl1 pinfl1 post1 ∧
      update_rel_nar x c⇩w σ σ1 (insert x stabl) (insert x post) post1 pinfl pinfl1 ∧
      traverse_rhs (T x) σ1 = xd1 ∧ (∀y∈dep_aux σ1 (T x). x ∈ slookup infl1 y)"
      using partial_correctness_ind(3)[OF assms(1,2) Continue(2,3) _, of "[]"] assms(9,10)
      by auto
    then have "xd1 ≤ mlup σ1 x"
    proof -
      have "x ∉ c⇩w" using assms(9,10) by auto
      then have "x ∈ post1 - c⇩w" using parCorr unfolding update_rel_nar_def by auto
      then show ?thesis using parCorr unfolding narrowing_inv_def by auto
    qed
    then have widen_fix: "mlup σ1 x = mlup σ1 x ∇ xd1" using widening_bounded by auto
    then show ?thesis using widen_not_fix by auto
  qed
qed

end ― ‹end of context for partial correctness proof›


subsection ‹Termination›

context TD_wn_post
begin

context
  assumes widening_finite: "wf {(x,y). ∃a. x ≠ y ∧ x = y ∇ a}"
    and narrowing_finite: "wf {(x,y). ∃a. x ≠ y ∧ x = y Δ a}"
    (* 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

subsection‹Construction of Wellfounded Relation for Termination Proof›

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


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 value_relation :: "((phase × 'd) × (phase × 'd)) set" where
  "value_relation = {((p2,d2),(p1,d1)). p1 = Widening ∧ p2 = Narrowing}
    ∪ {((p1,d1),(p2,d2)). p1 = Widening ∧ p2 = Widening ∧ (d1,d2) ∈ {(x,y). ∃a. x ≠ y ∧ x = y ∇ a}}
    ∪ {((p1,d1),(p2,d2)). p1 = Narrowing ∧ p2 = Narrowing ∧ (d1,d2) ∈ {(x,y). ∃a. x ≠ y ∧ x = y Δ a}}"

lemma wf_value_relation: "wf value_relation"
proof (intro wfI_min, goal_cases)
  case (1 t Q)
  define Q⇩N where qn_def: "Q⇩N = {(p,d) ∈ Q. p = Narrowing}"
  define Q⇩W where qw_def: "Q⇩W = {(p,d) ∈ Q. p = Widening}"
  have "Q = Q⇩N ∪ Q⇩W" unfolding qn_def qw_def using phase.exhaust by blast
  define Qd⇩N where qdn_def: "Qd⇩N = {d. (Narrowing,d) ∈ Q}"
  define Qd⇩W where qdw_def: "Qd⇩W = {d. (Widening,d) ∈ Q}"
  
  show ?case
  proof (cases "Qd⇩N = {}")
    case True
    then obtain dt where "t = (Widening,dt)"
      using 1 qdn_def qdw_def phase.exhaust
      by (metis (mono_tags, lifting) ex_in_conv mem_Collect_eq old.prod.exhaust)
    then have "dt ∈ Qd⇩W" using qdw_def 1 by auto
    then obtain d⇩m⇩i⇩n where d⇩m⇩i⇩n_def:
      "d⇩m⇩i⇩n ∈ Qd⇩W" "∀d'. (d',d⇩m⇩i⇩n) ∈ {(x,y). ∃a. x ≠ y ∧ x = y ∇ a} ⟶ d' ∉ Qd⇩W"
      using widening_finite wfE_min by meson
    then have "(Widening,d⇩m⇩i⇩n) ∈ Q" using qdw_def by simp 
    moreover have "((p',d'),(Widening,d⇩m⇩i⇩n)) ∈ value_relation ⟶ (p',d') ∉ Q" for p' d'
    proof (rule ccontr, goal_cases)
      case 1
      then have "((p', d'), (Widening, d⇩m⇩i⇩n)) ∈ value_relation" "(p', d') ∈ Q" by auto
      have "p' = Widening" using ‹(p', d') ∈ Q› True unfolding qdn_def by (cases p') auto
      then have "(d',d⇩m⇩i⇩n) ∈ {(x,y). ∃a. x ≠ y ∧ x = y ∇ a}"
        using ‹((p', d'), (Widening, d⇩m⇩i⇩n)) ∈ value_relation› unfolding value_relation_def by auto
      have "d' ∈ Qd⇩W" using qdw_def ‹(p', d') ∈ Q› ‹p' = Widening› by simp
      moreover have "d' ∉ Qd⇩W" using d⇩m⇩i⇩n_def ‹(d',d⇩m⇩i⇩n) ∈ {(x,y). ∃a. x ≠ y ∧ x = y ∇ a}› by auto
      ultimately show ?case by simp
    qed
    ultimately show ?thesis by auto
  next
    case False
    then obtain d⇩m⇩i⇩n where d⇩m⇩i⇩n_def: "d⇩m⇩i⇩n ∈ Qd⇩N" 
      "∀d'. (d',d⇩m⇩i⇩n) ∈ {(x,y). ∃a. x ≠ y ∧ x = y Δ a} ⟶ d' ∉ Qd⇩N"
      using narrowing_finite by (meson wfE_min')
    then have "(Narrowing,d⇩m⇩i⇩n) ∈ Q" using qdn_def by simp 
    moreover have "((p',d'),(Narrowing,d⇩m⇩i⇩n)) ∈ value_relation ⟶ (p',d') ∉ Q" for p' d'
    proof (rule ccontr, goal_cases)
      case 1
      then have "((p', d'), (Narrowing, d⇩m⇩i⇩n)) ∈ value_relation" "(p', d') ∈ Q" by auto
      then have "p' = Narrowing" "(d',d⇩m⇩i⇩n) ∈ {(x,y). ∃a. x ≠ y ∧ x = y Δ a}"
        unfolding value_relation_def by auto
      have "d' ∈ Qd⇩N" using qdn_def ‹(p', d') ∈ Q› ‹p' = Narrowing› by simp
      moreover have "d' ∉ Qd⇩N" using d⇩m⇩i⇩n_def ‹(d',d⇩m⇩i⇩n) ∈ {(x,y). ∃a. x ≠ y ∧ x = y Δ a}› by auto
      ultimately show ?case by simp
    qed
    ultimately show ?thesis by auto
  qed
qed

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

lemma wf_prod_relation: "wf prod_relation"
  unfolding prod_relation_def c_relation_def
  using widening_finite c_relation_def wf_rhs_relation wf_points_relation wf_value_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⇩w,c⇩n,infl,stabl,p,σ,pinfl,post) ⇒ (c⇩w ∪ c⇩n, 1, T x, 0, (Widening, mlup σ x))
    | Inr (Inl (x,c⇩w,c⇩n,infl,stabl,p,σ,wn,pinfl,post)) ⇒
        (c⇩w ∪ c⇩n, 3, T x, if x ∉ p then 1 else 0, (wn, mlup σ x))
    | Inr (Inr (x,t,c⇩w,c⇩n,infl,stabl,p,σ,pinfl,post)) ⇒ (c⇩w ∪ c⇩n, 2, t, 0, (Widening, mlup σ x)))"

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


subsection‹Auxiliary Lemmas›

lemma constant_vals_for_called:
  shows "query_dom y x c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ (xd, infl', stabl', p', σ', pinfl', post') = query y x c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ (∀u ∈ c⇩w ∪ c⇩n. mlup σ' u = mlup σ u)"
    and "iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post
    ⟹ (xd, infl', stabl', p', σ', pinfl', post') = iterate x c⇩w c⇩n infl stabl p σ wn pinfl post
    ⟹ x ∈ c⇩w ∪ c⇩n
    ⟹ (∀u ∈ c⇩w ∪ c⇩n - {x}. mlup σ' u = mlup σ u)"
    and "eval_dom x t c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ (xd, infl', stabl', p', σ', pinfl', post') = eval x t c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ (∀u ∈ c⇩w ∪ c⇩n. mlup σ' u = mlup σ u)"
proof(induction y x c⇩w c⇩n infl stabl p σ pinfl post and x c⇩w c⇩n infl stabl p σ wn pinfl post
    and y t c⇩w c⇩n infl stabl p σ pinfl post
    arbitrary: xd infl' stabl' p' σ' pinfl' post' and xd infl' stabl' p' σ' pinfl' post'
    and xd infl' stabl' p' σ' pinfl' post'
    rule: query_iterate_eval_pinduct)
  case (Query y x c⇩w c⇩n infl stabl p σ pinfl post)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate infl1 pinfl1 c1⇩w c1⇩n)
    show ?thesis
      using Query.IH(2)[OF Iterate(1,4) _ Iterate(3)] Iterate(1,4) by (auto split: if_splits)
  next
    case Lookup
    then show ?thesis by simp
  qed
next
  case (Iterate x c⇩w c⇩n infl stabl p σ wn pinfl post)
  show ?case using Iterate.IH(1) Iterate.prems
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis by auto
  next
    case (Fixpoint p1)
    then show ?thesis using Iterate.IH(2)[OF Fixpoint(1,4)] by simp
  next
    case (W_Fixpoint xd1 infl1 stabl1 p1 σ1 infl2 stabl2 pinfl1 post1)
    have IH1: "∀u∈c⇩w ∪ c⇩n. mlup σ1 u = mlup σ u" using Iterate.IH(2)[OF W_Fixpoint(1,5)] by simp
    have IH2: "∀u∈Set.remove x c⇩w ∪ insert x c⇩n - {x}. mlup σ' u = mlup (σ1(x ↦ mlup σ1 x Δ xd1)) u"
      using Iterate.IH(3)[OF W_Fixpoint(1,5) _ _ _ _ _ _ _ W_Fixpoint(6) _ W_Fixpoint(7,8) _
            W_Fixpoint(10)] W_Fixpoint(2,3) by fastforce
    have "∀u∈c⇩w ∪ c⇩n - {x}. mlup (σ1(x ↦ mlup σ1 x Δ xd1)) u = mlup σ1 u"
      by (auto simp add: fun_upd_other mlup_def)
    then show ?thesis using Iterate.prems(2) IH1 IH2 by auto
  next
    case (N_Fixpoint xd1 p1)
    then show ?thesis using Iterate.IH(2)[OF N_Fixpoint(1,5)] by simp
  next
    case (Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2 pinfl1 post1 pinfl2 post2)
    have IH1: "∀u∈c⇩w ∪ c⇩n. mlup σ1 u = mlup σ u" using Iterate.IH(2)[OF Continue(1,3)] by simp
    have IH2: "∀u∈c⇩w ∪ c⇩n - {x}. mlup σ' u = mlup (σ1(x ↦ d_new)) u"
      using Iterate.IH(4)[OF Continue(1,3) _ _ _ _ _ _ Continue(4-6) _ Continue(7) _
            Continue(9) Iterate.prems(2)] by auto
    then show ?thesis using Iterate.prems(2) IH1 by (auto simp add: fun_upd_other mlup_def)
  qed
next
  case (Eval x t c⇩w c⇩n infl stabl p σ pinfl post)
  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 pinfl1 post1)
    have IH1: "∀u∈c⇩w ∪ c⇩n. mlup σ1 u = mlup σ u" using Eval.IH(2)[OF Query(1,3)] by simp
    have IH2: "∀u∈c⇩w ∪ c⇩n. mlup σ' u = mlup σ1 u" 
      using Eval.IH(3)[OF Query(1,3) _ _ _ _ _ _ Query(5)] by simp
    then show ?thesis using IH1 by simp
  next
    case Answer
    then show ?thesis by auto
  qed
qed

lemma point_set_subset_c:
  shows "query_dom y x c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ (xd, infl', stabl', p', σ', pinfl', post') = query y x c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ p ⊆ c⇩w ∪ c⇩n
    ⟹ p' ⊆ c⇩w ∪ c⇩n"
    and "iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post
    ⟹ (xd, infl', stabl', p', σ', pinfl', post') = iterate x c⇩w c⇩n infl stabl p σ wn pinfl post
    ⟹ x ∈ c⇩w ∪ c⇩n
    ⟹ p ⊆ c⇩w ∪ c⇩n
    ⟹ p' ⊆ c⇩w ∪ c⇩n - {x}"
    and "eval_dom x t c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ (xd, infl', stabl', p', σ', pinfl', post') = eval x t c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ p ⊆ c⇩w ∪ c⇩n
    ⟹ p' ⊆ c⇩w ∪ c⇩n"
proof(induction y x c⇩w c⇩n infl stabl p σ pinfl post and x c⇩w c⇩n infl stabl p σ wn pinfl post
    and y t c⇩w c⇩n infl stabl p σ pinfl post
    arbitrary: xd infl' stabl' p' σ' pinfl' post' and xd infl' stabl' p' σ' pinfl' post'
    and xd infl' stabl' p' σ' pinfl' post'
    rule: query_iterate_eval_pinduct)
  case (Query y x c⇩w c⇩n infl stabl p σ pinfl post)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate infl1 pinfl1 c1⇩w c1⇩n)
    have IH: "p' ⊆ c1⇩w ∪ c1⇩n - {x}"
      using Query.IH(2)[OF Iterate(1,4) _ Iterate(3)] Iterate(4) Query.prems(2)
      by (auto split: if_splits)
    moreover have "x ∉ p" using Iterate(1,4) Query.prems(2) by auto
    ultimately show ?thesis using Iterate(4) by (auto split: if_splits)
  next
    case Lookup
    then show ?thesis using Query.prems(2) by auto
  qed
next
  case (Iterate x c⇩w c⇩n infl stabl p σ wn pinfl post)
  show ?case using Iterate.IH(1) Iterate.prems
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Iterate.prems(3) by auto
  next
    case (Fixpoint p1)
    show ?thesis using Iterate.IH(2)[OF Fixpoint(1,4)] Fixpoint(6) Iterate.prems(3) by auto
  next
    case (W_Fixpoint xd1 infl1 stabl1 p1 σ1 infl2 stabl2 pinfl1 post1)
    have IH1: "p1 ⊆ c⇩w ∪ c⇩n"
      using Iterate.IH(2)[OF W_Fixpoint(1,5)] Iterate.prems(3) by auto
    have IH2: "p' ⊆ Set.remove x c⇩w ∪ insert x c⇩n - {x}"
      using Iterate.IH(3)[OF W_Fixpoint(1,5) _ _ _ _ _ _ _ W_Fixpoint(6) _ W_Fixpoint(7,8) _
            W_Fixpoint(10)] W_Fixpoint(2,3) IH1(1) Iterate.prems(2) by fastforce
    then show ?thesis using IH1 by force
  next
    case (N_Fixpoint xd1 p1)
    show ?thesis using Iterate.IH(2)[OF N_Fixpoint(1,5)] N_Fixpoint(8) Iterate.prems(3) by auto
  next
    case (Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2 pinfl1 post1 pinfl2 post2)
    have IH1: "p1 ⊆ c⇩w ∪ c⇩n"
      using Iterate.IH(2)[OF Continue(1,3)] Iterate.prems(3) by auto
    have IH2: "p' ⊆ c⇩w ∪ c⇩n - {x}"
      using Iterate.IH(4)[OF Continue(1,3) _ _ _ _ _ _ Continue(4-6) _ Continue(7) _
            Continue(9) Iterate.prems(2)] IH1(1) by auto
    then show ?thesis using IH1 by force
  qed
next
  case (Eval x t c⇩w c⇩n infl stabl p σ pinfl post)
  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 pinfl1 post1)
    have IH1: "p1 ⊆ c⇩w ∪ c⇩n" using Eval.IH(2)[OF Query(1,3)] Eval.prems(2) by auto
    have IH2: "p' ⊆ c⇩w ∪ c⇩n"
      using Eval.IH(3)[OF Query(1,3) _ _ _ _ _ _ Query(5)] IH1(1) by auto
    then show ?thesis using IH1 by simp
  next
    case Answer
    then show ?thesis using Eval.prems(2) by auto
  qed
qed

lemma point_set_incr:
  shows "query_dom y x c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ (xd, infl', stabl', p', σ', pinfl', post') = query y x c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ p ⊆ c⇩w ∪ c⇩n
    ⟹ p' ⊆ c⇩w ∪ c⇩n ∧ p ⊆ p'"
    and "iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post
    ⟹ (xd, infl', stabl', p', σ', pinfl', post') = iterate x c⇩w c⇩n infl stabl p σ wn pinfl post
    ⟹ x ∈ c⇩w ∪ c⇩n
    ⟹ p ⊆ c⇩w ∪ c⇩n
    ⟹ p' ⊆ c⇩w ∪ c⇩n - {x} ∧ Set.remove x p ⊆ p'"
    and "eval_dom x t c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ (xd, infl', stabl', p', σ', pinfl', post') = eval x t c⇩w c⇩n infl stabl p σ pinfl post
    ⟹ p ⊆ c⇩w ∪ c⇩n
    ⟹ p' ⊆ c⇩w ∪ c⇩n ∧ p ⊆ p'"
proof(induction y x c⇩w c⇩n infl stabl p σ pinfl post and x c⇩w c⇩n infl stabl p σ wn pinfl post
    and y t c⇩w c⇩n infl stabl p σ pinfl post
    arbitrary: xd infl' stabl' p' σ' pinfl' post' and xd infl' stabl' p' σ' pinfl' post'
    and xd infl' stabl' p' σ' pinfl' post'
    rule: query_iterate_eval_pinduct)
  case (Query y x c⇩w c⇩n infl stabl p σ pinfl post)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate infl1 pinfl1 c1⇩w c1⇩n)
    have IH: "p' ⊆ c1⇩w ∪ c1⇩n - {x}" "Set.remove x p ⊆ p'"
      using Query.IH(2)[OF Iterate(1,4) _ Iterate(3)] Iterate(4) Query.prems(2)
      by (auto split: if_splits)
    moreover have "x ∉ p" using Iterate(1,4) Query.prems(2) by auto
    ultimately show ?thesis using Iterate(4) by (auto split: if_splits)
  next
    case Lookup
    then show ?thesis using Query.prems(2) by auto
  qed
next
  case (Iterate x c⇩w c⇩n infl stabl p σ wn pinfl post)
  show ?case using Iterate.IH(1) Iterate.prems
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Iterate.prems(3) by auto
  next
    case (Fixpoint p1)
    show ?thesis using Iterate.IH(2)[OF Fixpoint(1,4)] Fixpoint(6) Iterate.prems(3) by auto
  next
    case (W_Fixpoint xd1 infl1 stabl1 p1 σ1 infl2 stabl2 pinfl1 post1)
    have IH1: "p1 ⊆ c⇩w ∪ c⇩n" "p ⊆ p1"
      using Iterate.IH(2)[OF W_Fixpoint(1,5)] Iterate.prems(3) by auto
    have IH2: "p' ⊆ Set.remove x c⇩w ∪ insert x c⇩n - {x}" "Set.remove x p1 ⊆ p'"
      using Iterate.IH(3)[OF W_Fixpoint(1,5) _ _ _ _ _ _ _ W_Fixpoint(6) _ W_Fixpoint(7,8) _
            W_Fixpoint(10)] W_Fixpoint(2,3) IH1(1) Iterate.prems(2) by fastforce+
    then show ?thesis using IH1 by force
  next
    case (N_Fixpoint xd1 p1)
    show ?thesis using Iterate.IH(2)[OF N_Fixpoint(1,5)] N_Fixpoint(8) Iterate.prems(3) by auto
  next
    case (Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2 pinfl1 post1 pinfl2 post2)
    have IH1: "p1 ⊆ c⇩w ∪ c⇩n" "p ⊆ p1"
      using Iterate.IH(2)[OF Continue(1,3)] Iterate.prems(3) by auto
    have IH2: "p' ⊆ c⇩w ∪ c⇩n - {x}" "Set.remove x p1 ⊆ p'"
      using Iterate.IH(4)[OF Continue(1,3) _ _ _ _ _ _ Continue(4-6) _ Continue(7) _
            Continue(9) Iterate.prems(2)] IH1(1) by auto
    then show ?thesis using IH1 by force
  qed
next
  case (Eval x t c⇩w c⇩n infl stabl p σ pinfl post)
  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 pinfl1 post1)
    have IH1: "p1 ⊆ c⇩w ∪ c⇩n" "p ⊆ p1" using Eval.IH(2)[OF Query(1,3)] Eval.prems(2) by auto
    have IH2: "p' ⊆ c⇩w ∪ c⇩n" "p1 ⊆ p'" 
      using Eval.IH(3)[OF Query(1,3) _ _ _ _ _ _ Query(5)] IH1(1) by auto
    then show ?thesis using IH1 by simp
  next
    case Answer
    then show ?thesis using Eval.prems(2) by auto
  qed
qed

text‹While originally meant to prove that x is stable after iterating it, this lemma proves 
  a couple of helpful properties about the relation between the datastructures
  @{term c⇩w}, @{term c⇩n}, @{term infl} and @{term stabl} through necessary invariants along the way.›

lemma stabl_infl_properties:
    shows "query_dom y x c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ (xd, infl', stabl', p', σ', pinfl', post') = query y x c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ c⇩w ∪ c⇩n ⊆ stabl
      ⟹ fset (fmdom infl) ⊆ stabl
      ⟹ stabl ⊆ stabl' ∧ fset (fmdom infl') ⊆ stabl'
          ∧ (∀u. (slookup infl' u - slookup infl u) ∩ (stabl - {y}) = {})"
      and "iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post
      ⟹ (xd, infl', stabl', p', σ', pinfl', post') = iterate x c⇩w c⇩n infl stabl p σ wn pinfl post
      ⟹ x ∈ c⇩w ∪ c⇩n
      ⟹ c⇩w ∪ c⇩n - {x} ⊆ stabl
      ⟹ fset (fmdom infl) ⊆ stabl
      ⟹ insert x stabl ⊆ stabl' ∧ fset (fmdom infl') ⊆ stabl'
          ∧ (∀u. (slookup infl' u - slookup infl u) ∩ (stabl - {x}) = {})"
      and "eval_dom x t c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ (xd, infl', stabl', p', σ', pinfl', post') = eval x t c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ c⇩w ∪ c⇩n ⊆ stabl
      ⟹ fset (fmdom infl) ⊆ stabl
      ⟹ stabl ⊆ stabl' ∧ fset (fmdom infl') ⊆ stabl'
          ∧ (∀u. (slookup infl' u - slookup infl u) ∩ (stabl - {x}) = {})"
proof(induction y x c⇩w c⇩n infl stabl p σ pinfl post and x c⇩w c⇩n infl stabl p σ wn pinfl post
    and y t c⇩w c⇩n infl stabl p σ pinfl post
    arbitrary: xd infl' stabl' p' σ' pinfl' post' and xd infl' stabl' p' σ' pinfl' post'
    and xd infl' stabl' p' σ' pinfl' post'
    rule: query_iterate_eval_pinduct)
  case (Query y x c⇩w c⇩n infl stabl p σ pinfl post)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate infl1 pinfl1 c1⇩w c1⇩n)
    have "x ∈ c1⇩w ∪ c1⇩n" "c1⇩w ∪ c1⇩n - {x} ⊆ stabl"
      using Iterate(4) Query.prems(2) by (auto split: if_splits) 
    then have IH: "insert x stabl ⊆ stabl'" "fset (fmdom infl1) ⊆ stabl'"
      "∀u. (slookup infl1 u - slookup infl u) ∩ (stabl - {x}) = {}"
      using Query.IH(2)[OF Iterate(1,4) _ Iterate(3)] Query.prems(3) by auto
    show ?thesis
    proof (intro conjI, goal_cases)
      case 1
      then show ?case using IH(1) Iterate(4) by (auto split: if_splits)
    next
      case 2
      then show ?case using IH(1,2) Iterate(5) fmdom_fmupd unfolding fminsert_def by auto
    next
      case 3
      have IH': "∀u. (slookup infl1 u - slookup infl u) ∩ stabl = {}"
        using IH(3) Iterate(2,3) by (cases "x ∈ stabl") auto
      then have "(slookup infl' u - slookup infl u) ∩ (stabl - {y}) = {}" for u
        using Iterate(5)
        by (cases "u = x") (auto simp add: slookup_fminsert_same slookup_fminsert_other)
      then show ?case by auto
    qed
  next
    case Lookup
    have "x ∈ stabl'" using Lookup(1,4) Query(4) by blast
    moreover have "(slookup infl' u - slookup infl u) ∩ (stabl - {y}) = {}" for u
      using Lookup(3,4)
      by (cases "u = x") (auto simp add: slookup_fminsert_same slookup_fminsert_other)
    ultimately show ?thesis using Query(4,5) Lookup(3,4) unfolding fminsert_def by simp
  qed
next
  case (Iterate x c⇩w c⇩n infl stabl p σ wn pinfl post)
  show ?case using Iterate.IH(1) Iterate.prems
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    show ?thesis using Iterate.prems(3,4) Stable(1,3,4) by auto
  next
    case (Fixpoint p1)
    have "insert x stabl ⊆ stabl'" "fset (fmdom infl') ⊆ stabl'"
      "∀u. (slookup infl' u - slookup infl u) ∩ stabl = {}"
      using Iterate.IH(2) Iterate.prems(3,4) Fixpoint(1,4) by blast+
    then show ?thesis by auto
  next
    case (W_Fixpoint xd1 infl1 stabl1 p1 σ1 infl2 stabl2 pinfl1 post1)
    have IH1: "stabl ⊆ stabl1" "fset (fmdom infl1) ⊆ stabl1"
      "∀u. (slookup infl1 u - slookup infl u) ∩ stabl = {}"
      using Iterate.IH(2) Iterate.prems(3,4) W_Fixpoint(1,5) by blast+
    then have "influenced_by infl1 x ∩ stabl = {}"
      using new_lookup_to_infl_not_stabl[of infl1 infl stabl x] W_Fixpoint(1) Iterate.prems(4)
      by blast
    then have "stabl ⊆ stabl2"
        using destab_infl_stabl_relation[OF W_Fixpoint(8)] ‹stabl ⊆ stabl1› by auto
    then have "c⇩w ∪ c⇩n - {x} ⊆ stabl2" using Iterate.prems(3) by blast
    then have "Set.remove x c⇩w ∪ insert x c⇩n - {x} ⊆ stabl2"
      using Iterate.prems(2) by (cases "x ∈ c⇩w") auto
    moreover have "fset (fmdom infl2) ⊆ stabl2"
      by (simp add: IH1(2) destab_preserves_infl_dom_stabl W_Fixpoint(8))
    ultimately have IH2: "insert x stabl2 ⊆ stabl'" "fset (fmdom infl') ⊆ stabl'"
      "∀u. (slookup infl' u - slookup infl2 u) ∩ (stabl2 - {x}) = {}"
      using Iterate.IH(3)[OF W_Fixpoint(1,5) _ _ _ _ _ _ _ W_Fixpoint(6) _ W_Fixpoint(7,8) _
            W_Fixpoint(10)] W_Fixpoint(2,3) Iterate.prems(2) by auto
    have "(slookup infl' u - slookup infl u) ∩ (stabl - {x}) = {}" for u
    proof -
      have "slookup infl2 u ⊆ slookup infl1 u"
        using destab_infl_stabl_relation[OF W_Fixpoint(8)]
        by (metis empty_iff empty_set fmlookup_default_drop_set subset_iff)
      then show ?thesis using IH2(3) IH1(3) ‹stabl ⊆ stabl2› by blast
    qed
    then show ?thesis using IH2 ‹stabl ⊆ stabl2› by (cases "x ∈ c⇩w") auto
  next
    case (N_Fixpoint xd1 p1)
    show ?thesis using Iterate.IH(2)[OF N_Fixpoint(1,5)] N_Fixpoint(8) Iterate.prems(3,4) by blast
  next
    case (Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2 pinfl1 post1 pinfl2 post2)
    have IH1: "insert x stabl ⊆ stabl1" "fset (fmdom infl1) ⊆ stabl1"
        "∀u. (slookup infl1 u - slookup infl u) ∩ (insert x stabl - {x}) = {}"
      using Iterate.IH(2)[OF Continue(1) Continue(3)] Iterate.prems(3,4) by blast+
    then have "influenced_by infl1 x ∩ stabl = {}"
      using new_lookup_to_infl_not_stabl[of infl1 infl stabl x] Continue(1) Iterate.prems(4)
      by blast
    then have "stabl ⊆ stabl2"
      using ‹insert x stabl ⊆ stabl1› destab_infl_stabl_relation[OF Continue(6)] by blast
    then have "c⇩w ∪ c⇩n - {x} ⊆ stabl2" using Iterate.prems(3) by blast
    moreover have "fset (fmdom infl2) ⊆ stabl2"
      by (simp add: IH1(2) destab_preserves_infl_dom_stabl Continue(6))
    ultimately have IH2: "insert x stabl2 ⊆ stabl'" "fset (fmdom infl') ⊆ stabl'"
      "∀u. (slookup infl' u - slookup infl2 u) ∩ (stabl2 - {x}) = {}"
      using Iterate.IH(4)[OF Continue(1,3) _ _ _ _ _ _ Continue(4,5,6) _ Continue(7) _
            Continue(9)] Iterate.prems(2) by auto
    have "(slookup infl' u - slookup infl u) ∩ (stabl - {x}) = {}" for u
    proof -
      have "slookup infl2 u ⊆ slookup infl1 u"
        using destab_infl_stabl_relation[OF Continue(6)]
        by (metis empty_iff empty_set fmlookup_default_drop_set subset_iff)
      then show ?thesis using IH2(3) IH1(3) ‹stabl ⊆ stabl2› by blast
    qed
    then show ?thesis using IH2 ‹stabl ⊆ stabl2› by auto
  qed
next
  case (Eval x t c⇩w c⇩n infl stabl p σ pinfl post)
  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 pinfl1 post1)
    have IH1: "stabl ⊆ stabl1" "fset (fmdom infl1) ⊆ stabl1"
        "∀u. (slookup infl1 u - slookup infl u) ∩ (stabl - {x}) = {}"
      using Eval.IH(2)[OF Query(1,3)] Eval.prems(2,3) by auto
    have "c⇩w ∪ c⇩n ⊆ stabl1" using IH1(1) Eval.prems(2) by auto
    then have IH2: "stabl1 ⊆ stabl'" "fset (fmdom infl') ⊆ stabl'"
        "∀u. (slookup infl' u - slookup infl1 u) ∩ (stabl1 - {x}) = {}"
      using Eval.IH(3)[OF Query(1,3) _ _ _ _ _ _ Query(5)] IH1(2,3) by auto
    then show ?thesis using IH1 ‹stabl ⊆ stabl1› by blast
  next
    case Answer
    then show ?thesis using Eval.prems(2,3) by auto
  qed
qed

lemma called_with_non_empty_infl_in_point:
    shows "query_dom y x c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ (xd, infl', stabl', p', σ', pinfl', post') = query y x c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ c⇩w ∪ c⇩n ⊆ stabl
      ⟹ fset (fmdom infl) ⊆ stabl
      ⟹ {u ∈ c⇩w ∪ c⇩n. slookup infl u ≠ {}} ⊆ p
      ⟹ {u ∈ c⇩w ∪ c⇩n. slookup infl' u ≠ {}} ⊆ p'"
      and "iterate_dom x c⇩w c⇩n infl stabl p σ wn pinfl post
      ⟹ (xd, infl', stabl', p', σ', pinfl', post') = iterate x c⇩w c⇩n infl stabl p σ wn pinfl post
      ⟹ x ∈ c⇩w ∪ c⇩n
      ⟹ c⇩w ∪ c⇩n - {x} ⊆ stabl
      ⟹ fset (fmdom infl) ⊆ stabl
      ⟹ {u ∈ c⇩w ∪ c⇩n - {x}. slookup infl u ≠ {}} ⊆ p - {x}
      ⟹ {u ∈ c⇩w ∪ c⇩n - {x}. slookup infl' u ≠ {}} ⊆ p'"
      and "eval_dom x t c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ (xd, infl', stabl', p', σ', pinfl', post') = eval x t c⇩w c⇩n infl stabl p σ pinfl post
      ⟹ c⇩w ∪ c⇩n ⊆ stabl
      ⟹ fset (fmdom infl) ⊆ stabl
      ⟹ {u ∈ c⇩w ∪ c⇩n. slookup infl u ≠ {}} ⊆ p
      ⟹ {u ∈ c⇩w ∪ c⇩n. slookup infl' u ≠ {}} ⊆ p'"
proof(induction y x c⇩w c⇩n infl stabl p σ pinfl post and x c⇩w c⇩n infl stabl p σ wn pinfl post
    and y t c⇩w c⇩n infl stabl p σ pinfl post
    arbitrary: xd infl' stabl' p' σ' pinfl' post' and xd infl' stabl' p' σ' pinfl' post'
    and xd infl' stabl' p' σ' pinfl' post'
    rule: query_iterate_eval_pinduct)
  case (Query y x c⇩w c⇩n infl stabl p σ pinfl post)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate infl1 pinfl1 c1⇩w c1⇩n)
    have IH: "{u ∈ c1⇩w ∪ c1⇩n - {x}. slookup infl1 u ≠ {}} ⊆ p'"
      using Query.IH(2)[OF Iterate(1,4) _ Iterate(3)] Iterate(4) Query.prems(2-4)
      by (auto split: if_splits)
    moreover have "c1⇩w ∪ c1⇩n - {x} = c⇩w ∪ c⇩n" using Iterate(1,4) by (auto split: if_splits)
    ultimately show ?thesis using Iterate(1,5) slookup_fminsert_other[of _ x infl1 y] by force
  next
    case Lookup
    show ?thesis using Query.prems(2-4) Lookup(3,5) slookup_fminsert_other[of _ x infl y] by force
  qed
next
  case (Iterate x c⇩w c⇩n infl stabl p σ wn pinfl post)
  show ?case using Iterate.IH(1) Iterate.prems
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Iterate.prems(5) by auto
  next
    case (Fixpoint p1)
    have "slookup infl x = {}" using Fixpoint(1) Iterate.prems(4) stabl_infl_empty by fast
    then have "{u ∈ c⇩w ∪ c⇩n. slookup infl u ≠ {}} ⊆ p" using Iterate.prems(5) by blast
    then show ?thesis using Iterate.IH(2)[OF Fixpoint(1,4)] Fixpoint(6) Iterate.prems(3-4) by force
  next
    case (W_Fixpoint xd1 infl1 stabl1 p1 σ1 infl2 stabl2 pinfl1 post1)
    have "slookup infl x = {}" using W_Fixpoint(1) Iterate.prems(4) stabl_infl_empty by fast
    then have "{u ∈ c⇩w ∪ c⇩n. slookup infl u ≠ {}} ⊆ p" using Iterate.prems(5) by blast
    then have IH1: "{u ∈ c⇩w ∪ c⇩n. slookup infl1 u ≠ {}} ⊆ p1"
      using Iterate.IH(2)[OF W_Fixpoint(1,5)] Iterate.prems(2-4) by auto
    have stabl_infl_props: "insert x stabl ⊆ stabl1" "fset (fmdom infl1) ⊆ stabl1"
      "∀u. (slookup infl1 u - slookup infl u) ∩ (insert x stabl - {x}) = {}"
      using stabl_infl_properties(3)[OF W_Fixpoint(4,5)] Iterate.prems(3-4) by auto
    have "slookup infl2 u ⊆ slookup infl1 u" for u
      using destab_infl_stabl_relation[OF W_Fixpoint(8)]
      by (metis empty_iff empty_set fmlookup_default_drop_set subsetI)
    then have "slookup infl1 u ≠ {}" if "slookup infl2 u ≠ {}" for u
      using that by (metis subset_empty)
    then have "{u ∈ c⇩w ∪ c⇩n - {x}. slookup infl2 u ≠ {}} ⊆ p1 - {x}"
      using IH1 Iterate.prems(2) by blast
    then have "{u ∈ Set.remove x c⇩w ∪ insert x c⇩n - {x}. slookup infl2 u ≠ {}} ⊆ p1 - {x}"
      using Iterate.prems(2) by auto
    moreover have "fset (fmdom infl2) ⊆ stabl2"
      using destab_preserves_infl_dom_stabl[OF W_Fixpoint(8)] stabl_infl_props(2) by blast
    moreover have "Set.remove x c⇩w ∪ insert x c⇩n - {x} ⊆ stabl2"
    proof -
      have "influenced_by infl1 x ∩ stabl = {}"
        using new_lookup_to_infl_not_stabl[of infl1 infl stabl x] W_Fixpoint(1)
          Iterate.prems(4) stabl_infl_props(3) by blast
      then have "stabl ⊆ stabl2"
        using ‹insert x stabl ⊆ stabl1› destab_infl_stabl_relation[OF W_Fixpoint(8)] by blast
      then show ?thesis using Iterate.prems(3) by auto
    qed
    ultimately have IH2: "{u ∈ Set.remove x c⇩w ∪ insert x c⇩n - {x}. slookup infl' u ≠ {}} ⊆ p'"
      using Iterate.IH(3)[OF W_Fixpoint(1,5) _ _ _ _ _ _ _ W_Fixpoint(6) _ W_Fixpoint(7,8) _
            W_Fixpoint(10)] W_Fixpoint(2,3) Iterate.prems(2) by auto
    then show ?thesis using IH1 by force
  next
    case (N_Fixpoint xd1 p1)
    have "slookup infl x = {}" using N_Fixpoint(1) Iterate.prems(4) stabl_infl_empty by fast
    then have "{u ∈ c⇩w ∪ c⇩n. slookup infl u ≠ {}} ⊆ p" using Iterate.prems(5) by blast
    then have "{u ∈ c⇩w ∪ c⇩n. slookup infl' u ≠ {}} ⊆ p1"
      using Iterate.IH(2)[OF N_Fixpoint(1,5)] Iterate.prems(3,4) by auto
    then show ?thesis using N_Fixpoint(8) Iterate.prems(2) by auto
  next
    case (Continue xd1 infl1 stabl1 p1 σ1 d_new infl2 stabl2 pinfl1 post1 pinfl2 post2)
    have "slookup infl x = {}" using Continue(1) Iterate.prems(4) stabl_infl_empty by fast
    then have "{u ∈ c⇩w ∪ c⇩n. slookup infl u ≠ {}} ⊆ p" using Iterate.prems(5) by blast
    then have IH1: "{u ∈ c⇩w ∪ c⇩n. slookup infl1 u ≠ {}} ⊆ p1"
      using Iterate.IH(2)[OF Continue(1,3)] Iterate.prems(3-5) by auto
    have stabl_infl_props: "insert x stabl ⊆ stabl1" "fset (fmdom infl1) ⊆ stabl1"
      "∀u. (slookup infl1 u - slookup infl u) ∩ (insert x stabl - {x}) = {}"
      using stabl_infl_properties(3)[OF Continue(2,3)] Iterate.prems(3,4) by auto
    have "slookup infl2 u ⊆ slookup infl1 u" for u
      using destab_infl_stabl_relation[OF Continue(6)]
      by (metis empty_iff empty_set fmlookup_default_drop_set subsetI)
    then have "slookup infl1 u ≠ {}" if "slookup infl2 u ≠ {}" for u
      by (metis subset_empty that)
    then have "{u ∈ c⇩w ∪ c⇩n - {x}. slookup infl2 u ≠ {}} ⊆ p1 - {x}" using IH1 by blast
    moreover have "fset (fmdom infl2) ⊆ stabl2"
      using destab_preserves_infl_dom_stabl[OF Continue(6)] using stabl_infl_props(2) by simp
    moreover have "c⇩w ∪ c⇩n - {x} ⊆ stabl2"
    proof -
      have "influenced_by infl1 x ∩ stabl = {}"
        using new_lookup_to_infl_not_stabl[of infl1 infl stabl x] Continue(1)
          Iterate.prems(4) stabl_infl_props(3) by blast
      then have "stabl ⊆ stabl2"
        using ‹insert x stabl ⊆ stabl1› destab_infl_stabl_relation[OF Continue(6)] by blast
      then show ?thesis using Iterate.prems(3) by simp
    qed
    ultimately have IH2: "{u ∈ c⇩w ∪ c⇩n - {x}. slookup infl' u ≠ {}} ⊆ p'"
      using Iterate.IH(4)[OF Continue(1,3) _ _ _ _ _ _ Continue(4-6) _ Continue(7) _
            Continue(9) Iterate.prems(2)] IH1(1) by auto
    then show ?thesis using IH1 by force
  qed
next
  case (Eval x t c⇩w c⇩n infl stabl p σ pinfl post)
  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 pinfl1 post1)
    have IH1: "{u ∈ c⇩w ∪ c⇩n. slookup infl1 u ≠ {}} ⊆ p1"
      using Eval.IH(2)[OF Query(1,3)] Eval.prems(2-4) by auto
    have stabl_infl_props: "stabl ⊆ stabl1" "fset (fmdom infl1) ⊆ stabl1"
      "∀u. (slookup infl1 u - slookup infl u) ∩ (insert x stabl - {x}) = {}"
      using stabl_infl_properties(1)[OF Query(2,3)] Eval.prems(2,3) by auto
    have IH2: "{u ∈ c⇩w ∪ c⇩n. slookup infl' u ≠ {}} ⊆ p'" 
      using Eval.IH(3)[OF Query(1,3) _ _ _ _ _ _ Query(5)] IH1(1) stabl_infl_props(1,2)
        Eval.prems(2) by fast
    then show ?thesis using IH1 by simp
  next
    case Answer
    then show ?thesis using Eval.prems(2-4) by auto
  qed
qed


subsection‹Conditional Termination Proof›

abbreviation term_cond_aux where
  "term_cond_aux c infl stabl p ≡
    p ⊆ c ∧ c ⊆ stabl ∧ fset (fmdom infl) ⊆ stabl ∧ {u ∈ c. slookup infl u ≠ {}} ⊆ p"

abbreviation term_cond where
  "term_cond st ≡ (case st of
      Inl (_, _, c⇩w, c⇩n, infl, stabl, p, _, _, _) ⇒ term_cond_aux (c⇩w ∪ c⇩n) infl stabl p
    | Inr (Inl (x, c⇩w, c⇩n, infl, stabl, p, _, _, _, _)) ⇒ x ∈ c⇩w ∪ c⇩n
      ∧ term_cond_aux (c⇩w ∪ c⇩n - {x}) infl stabl (p - {x})
    | Inr (Inr (_, _, c⇩w, c⇩n, infl, stabl, p, _, _, _)) ⇒ term_cond_aux (c⇩w ∪ c⇩n) infl stabl p)"

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⇩w c⇩n infl stabl p σ pinfl post where
      "st = Inl (x, y, c⇩w, c⇩n, infl, stabl, p, σ, pinfl, post)"
    | (Iterate) x c⇩w c⇩n infl stabl p σ wn pinfl post where
      "st = Inr (Inl (x, c⇩w, c⇩n, infl, stabl, p, σ, wn, pinfl, post))"
    | (Eval) x t c⇩w c⇩n infl stabl p σ pinfl post where
      "st = Inr (Inr (x, t, c⇩w, c⇩n, infl, stabl, p, σ, pinfl, post))"
    by (metis (no_types, opaque_lifting) sumE surj_pair)
  then show ?case
  proof cases
    case Query
    show ?thesis
    proof (cases "y ∈ c⇩w ∪ c⇩n")
      case True
      then show ?thesis using Query query_iterate_eval.domintros(1)[of y post c⇩w c⇩n] by blast
    next
      case False
      have "p ⊆ c⇩w ∪ c⇩n" using less(2) Query by simp
      obtain c1⇩w c1⇩n where c1_def:
        "(c1⇩w, c1⇩n) = (if y ∈ post then (c⇩w, insert y c⇩n) else (insert y c⇩w, c⇩n))"
        by fastforce
      then have "c1⇩w ∪ c1⇩n = insert y (c⇩w ∪ c⇩n)" using False by (auto split: if_splits)
      then have "card (UNIV - (c1⇩w ∪ c1⇩n)) < card (UNIV - (c⇩w ∪ c⇩n))"
        using finite_vars False
        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 "(c1⇩w ∪ c1⇩n, (c⇩w ∪ c⇩n)) ∈ c_relation"
        unfolding c_relation_def by (meson in_measure)
      then have "(Inr (Inl (y, c1⇩w, c1⇩n, infl, stabl, p, σ, Widening, pinfl, post)), st) ∈ term_relation"
        unfolding term_relation_def prod_relation_def Query by force
      moreover have "term_cond (Inr (Inl (y, c1⇩w, c1⇩n, infl, stabl, p, σ, Widening, pinfl, post)))"
        using c1_def less(2) Query by (auto split: if_splits)
      ultimately have "iterate_dom y c1⇩w c1⇩n infl stabl p σ Widening pinfl post"
        using less(1)[of "Inr (Inl (y, c1⇩w, c1⇩n, infl, stabl, p, σ, Widening, pinfl, post))"] by auto
      then show ?thesis
        using Query query_iterate_eval.domintros(1)[of y post c⇩w c⇩n infl stabl p σ] c1_def False
        by (auto split: if_splits)
      qed
  next
    case Iterate
    have xcalled: "x ∈ c⇩w ∪ c⇩n" and p_sub_called: "p ⊆ c⇩w ∪ c⇩n" using Iterate less(2) by auto
    show ?thesis
    proof (cases "x ∈ stabl")
      case True
      then show ?thesis using Iterate query_iterate_eval.domintros(2) by blast
    next
      case False
      have "(Inr (Inr (x, T x, c⇩w, c⇩n, infl, insert x stabl, p, σ, pinfl, insert x post)), st) ∈
        term_relation"
        using Iterate unfolding term_relation_def prod_relation_def by simp
      moreover have "term_cond (Inr (Inr (x, T x, c⇩w, c⇩n, infl, insert x stabl, p, σ, pinfl,
        insert x post)))"
      proof -
        have "slookup infl x = {}" using less.prems Iterate stabl_infl_empty[OF False] by auto
        then show ?thesis using Iterate less.prems by auto
      qed
      ultimately have eval_dom:
        "eval_dom x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
        using less.IH by auto
      then obtain xd infl1 stabl1  p1 σ1 pinfl1 post1 where
          eval: "(xd, infl1, stabl1, p1, σ1, pinfl1, post1) = 
                 eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)"
        by (metis surj_pair)
      have "p1 ⊆ c⇩w ∪ c⇩n" "p ⊆ p1" using point_set_incr(3)[OF eval_dom eval p_sub_called] by auto
      have stabl_infl_props1: "insert x stabl ⊆ stabl1" "fset (fmdom infl1) ⊆ stabl1"
          "∀u. (slookup infl1 u - slookup infl u) ∩ (insert x stabl - {x}) = {}"
        using stabl_infl_properties(3)[OF eval_dom eval] less.prems Iterate
        by auto
      have non_empty_infl_point1: "{u ∈ c⇩w ∪ c⇩n. slookup infl1 u ≠ {}} ⊆ p1"
      proof -
        have "slookup infl x = {}" using False less.prems Iterate stabl_infl_empty by auto
        then have "{u ∈ c⇩w ∪ c⇩n. slookup infl u ≠ {}} ⊆ p" using less.prems Iterate by auto
        then show ?thesis
          using called_with_non_empty_infl_in_point(3)[OF eval_dom eval] less.prems Iterate by auto
      qed

      obtain infl2 stabl2 where destab_stabl: "(infl2, stabl2) = destab x infl1 stabl1"
        by (cases "destab x infl1 stabl1") simp
      have term_cond2: "p1 ⊆ c⇩w ∪ c⇩n"
          "c⇩w ∪ c⇩n - {x} ⊆ stabl2" "fset (fmdom infl2) ⊆ stabl2"
          "{u ∈ c⇩w ∪ c⇩n - {x}. slookup infl2 u ≠ {}} ⊆ p1 - {x}"
      proof (goal_cases)
        case 1
        then show ?case using Iterate less.prems point_set_incr(3)[OF eval_dom eval] by auto
      next
        case 2
        have "influenced_by infl1 x ∩ stabl = {}"
          using new_lookup_to_infl_not_stabl[of infl1 infl stabl x] False
            stabl_infl_props1(3) less.prems Iterate by auto
        then have "stabl ⊆ stabl2"
          using ‹insert x stabl ⊆ stabl1› destab_infl_stabl_relation[OF destab_stabl]
          by blast
        then show ?case using Iterate less.prems by auto
      next
        case 3
        then show ?case
          using destab_preserves_infl_dom_stabl[OF destab_stabl] stabl_infl_props1(2)
          by simp
      next
        case 4
        have "slookup infl2 u ⊆ slookup infl1 u" for u
          using destab_infl_stabl_relation[OF destab_stabl]
          by (metis empty_iff empty_set fmlookup_default_drop_set subsetI)
        then show ?case using non_empty_infl_point1 subset_empty by fastforce
      qed

      show ?thesis
      proof (cases "x ∈ p")
        case True
        then show ?thesis
        proof (cases wn)
          case Widening
          show ?thesis
          proof (cases "mlup σ1 x = mlup σ1 x ∇ xd")
            case True
            show ?thesis
            proof (cases "mlup σ1 x Δ xd = mlup σ1 x")
              case True
              then show ?thesis
                using Iterate ‹x ∉ stabl› ‹x ∈ p› eval_dom eval ‹mlup σ1 x = mlup σ1 x ∇ xd› Widening
                  query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post wn]
                by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
            next
              case False
              define st' where st': "st' :: ('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in ≡
                Inr (Inl (x, Set.remove x c⇩w, insert x c⇩n, infl2, stabl2, p1, σ1(x ↦ mlup σ1 x Δ xd), Narrowing, pinfl1, post1))"
              have "insert x (Set.remove x c⇩w ∪ c⇩n) = c⇩w ∪ c⇩n" using less(2) Iterate by auto
              moreover have "x ∈ p1" using ‹x ∈ p› ‹p ⊆ p1› by auto
              ultimately have "(st', st) ∈ term_relation"
                using st' Iterate ‹x ∈ p› Widening
                unfolding term_relation_def prod_relation_def value_relation_def by auto
              moreover have "term_cond st'" using term_cond2 st' by auto
              ultimately have
                "iterate_dom x (Set.remove x c⇩w) (insert x c⇩n) infl2 stabl2 p1 (σ1(x ↦ mlup σ1 x Δ xd)) Narrowing pinfl1 post1"
                using less(1)[OF ‹(st', st) ∈ term_relation›] st' ‹p1 ⊆ c⇩w ∪ c⇩n› xcalled by force
              then show ?thesis
                using Iterate ‹x ∉ stabl› ‹x ∈ p› eval_dom eval True destab_stabl Widening
                  query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post]
                by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
                    cases "destab x infl1 stabl1", cases wn) auto
            qed
          next
            case False
            obtain pinfl2 post2 where
              destab_post: "(pinfl2, post2) = destab_post x post pinfl1 post1 stabl2"
              by (cases "destab_post x post pinfl1 post1 stabl2") simp

            define st' where st': "st' :: ('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in ≡
              Inr (Inl (x, c⇩w, c⇩n, infl2, stabl2, p1, σ1(x ↦ mlup σ1 x ∇ xd), wn, pinfl2, post2))"
            have "x ∈ p1" using ‹x ∈ p› ‹p ⊆ p1› by auto
            moreover have
              "(mlup (σ1(x ↦ mlup σ1 x ∇ xd)) x, mlup σ x) ∈ {(x,y). ∃a. x ≠ y ∧ x = y ∇ a}"
            proof -
              have "mlup (σ1(x ↦ mlup σ1 x ∇ xd)) x = mlup σ1 x ∇ xd"
                unfolding mlup_def by (simp add: fun_upd_same)
              moreover have "mlup σ1 x = mlup σ x"
                using constant_vals_for_called(3)[OF eval_dom eval] xcalled by blast
              moreover have "mlup σ x ∇ xd ≠ mlup σ x" using False ‹mlup σ1 x = mlup σ x› by simp
              ultimately show ?thesis by auto
            qed
            ultimately have "(st', st) ∈ term_relation"
              using st' Iterate ‹x ∈ p› Widening
              unfolding term_relation_def prod_relation_def value_relation_def by auto
            moreover have "term_cond st'" using term_cond2 st' xcalled by auto
            ultimately have
              "iterate_dom x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ mlup σ1 x ∇ xd)) wn pinfl2 post2"
              using less st' Iterate ‹p1 ⊆ c⇩w ∪ c⇩n› xcalled by force
            then show ?thesis
              using Iterate ‹x ∉ stabl› ‹x ∈ p› eval_dom eval False destab_stabl destab_post Widening
                query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post]
              by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
                  cases "destab x infl1 stabl1", cases "destab_post x post pinfl1 post1 stabl2",
                  cases wn) auto
          qed
        next
          case Narrowing
          show ?thesis
          proof (cases "mlup σ1 x = mlup σ1 x Δ xd")
            case True
            then show ?thesis
              using Iterate ‹x ∉ stabl› ‹x ∈ p› eval_dom eval Narrowing
              query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post]
            by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
          next
            case False
            obtain pinfl2 post2 where
              destab_post: "(pinfl2, post2) = destab_post x post pinfl1 post1 stabl2"
              by (cases "destab_post x post pinfl1 post1 stabl2") simp

            define st' where st': "st' :: ('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in ≡
              Inr (Inl (x, c⇩w, c⇩n, infl2, stabl2, p1, σ1(x ↦ mlup σ1 x Δ xd), wn, pinfl2, post2))"
            have "x ∈ p1" using ‹x ∈ p› ‹p ⊆ p1› by auto
            moreover have
              "(mlup (σ1(x ↦ mlup σ1 x Δ xd)) x, mlup σ x) ∈ {(x,y). ∃a. x ≠ y ∧ x = y Δ a}"
            proof -
              have "mlup (σ1(x ↦ mlup σ1 x Δ xd)) x = mlup σ1 x Δ xd"
                unfolding mlup_def by (simp add: fun_upd_same)
              moreover have "mlup σ1 x = mlup σ x"
                using constant_vals_for_called(3)[OF eval_dom eval] xcalled by blast
              moreover have "mlup σ x Δ xd ≠ mlup σ x" using False ‹mlup σ1 x = mlup σ x› by auto
              ultimately show ?thesis by auto
            qed
            ultimately have "(st', st) ∈ term_relation"
              using Iterate st' Narrowing unfolding term_relation_def prod_relation_def value_relation_def
              by auto
            moreover have "term_cond st'" using term_cond2 st' xcalled by auto
            ultimately have
              "iterate_dom x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ mlup σ1 x Δ xd)) wn pinfl2 post2"
              using less st' Iterate ‹p1 ⊆ c⇩w ∪ c⇩n› xcalled by force
            then show ?thesis
              using Iterate ‹x ∉ stabl› ‹x ∈ p› eval_dom eval False destab_stabl destab_post Narrowing
                query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post]
              by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
                  cases "destab x infl1 stabl1", cases "destab_post x post pinfl1 post1 stabl2",
                  cases wn) auto
          qed
        qed
      next
        case False
        show ?thesis
        proof (cases "mlup σ1 x = xd")
          case True
          then show ?thesis
            using Iterate ‹x ∉ stabl› ‹x ∉ p› eval_dom eval
              query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post]
            by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)") auto
        next
          case False
          obtain pinfl2 post2 where
            destab_post: "(pinfl2, post2) = destab_post x post pinfl1 post1 stabl2"
            by (cases "destab_post x post pinfl1 post1 stabl2") simp

          define st' where st': "st' :: ('x,'d) query_in + ('x,'d) iterate_in + ('x,'d) eval_in ≡
            Inr (Inl (x, c⇩w, c⇩n, infl2, stabl2, p1, σ1(x ↦ xd), wn, pinfl2, post2))"

          have "iterate_dom x c⇩w c⇩n infl2 stabl2 p1 (σ1(x ↦ xd)) wn pinfl2 post2"
          proof (cases "x ∈ p1")
            case True
            then have "(st', st) ∈ term_relation"
              using st' Iterate ‹x ∉ p› unfolding term_relation_def prod_relation_def by auto
            moreover have "term_cond st'" using term_cond2 st' xcalled by auto
            ultimately show ?thesis using less st' Iterate ‹p1 ⊆ c⇩w ∪ c⇩n› xcalled by force
          next
            case False
            have prems: "c⇩w ∪ c⇩n ⊆ insert x stabl" "fset (fmdom infl) ⊆ stabl"
                "{u ∈ c⇩w ∪ c⇩n - {x}. slookup infl u ≠ {}} ⊆ p - {x}"
              using less.prems Iterate by auto
            have "c⇩w ∪ c⇩n ⊆ stabl1"
              using stabl_infl_properties(3)[OF eval_dom eval] prems(1,2) by fast
            have "{u ∈ c⇩w ∪ c⇩n. slookup infl u ≠ {}} ⊆ p"
            proof -
              have "slookup infl x = {}" using ‹x ∉ stabl› prems(2) stabl_infl_empty by simp
              then show ?thesis using prems(3) by auto
            qed
            then have "{u ∈ c⇩w ∪ c⇩n. slookup infl1 u ≠ {}} ⊆ p1"
              using called_with_non_empty_infl_in_point(3)[OF eval_dom eval] prems(1,2) by auto
            then have "slookup infl1 x = {}" using False xcalled by blast
            then have "influenced_by infl1 x = {}" using influenced_by_aux by force
            then have "stabl1 = stabl2" using destab_infl_stabl_relation[OF destab_stabl] by simp
            then have "x ∈ stabl2" using xcalled ‹c⇩w ∪ c⇩n ⊆ stabl1› by blast
            then show ?thesis using query_iterate_eval.domintros(2) by force
          qed
          then show ?thesis
            using Iterate ‹x ∉ stabl› ‹x ∉ p› eval_dom eval False destab_stabl destab_post
              query_iterate_eval.domintros(2)[of x stabl c⇩w c⇩n infl p σ pinfl post]
            by (cases "eval x (T x) c⇩w c⇩n infl (insert x stabl) p σ pinfl (insert x post)",
                cases "destab x infl1 stabl1", cases "destab_post x post pinfl1 post1 stabl2",
                cases wn) auto
        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)
      have "p ⊆ c⇩w ∪ c⇩n" using Eval less(2) by simp
      have "(Inl (x, y, c⇩w, c⇩n, infl, stabl, p, σ, pinfl, post), st) ∈ term_relation"
        unfolding term_relation_def prod_relation_def Eval by simp
      moreover have "term_cond (Inl (x, y, c⇩w, c⇩n, infl, stabl, p, σ, pinfl, post))"
        using less.prems Eval by simp
      ultimately have query_dom: "query_dom x y c⇩w c⇩n infl stabl p σ pinfl post"
        using less.IH ‹p ⊆ c⇩w ∪ c⇩n› by simp
      then obtain σ' infl' stabl' p' d' pinfl' post' where query:
        "(d', infl', stabl', p', σ', pinfl', post') = query x y c⇩w c⇩n infl stabl p σ pinfl post"
        by (metis surj_pair)
      have "p' ⊆ c⇩w ∪ c⇩n" using point_set_incr(1)[OF query_dom query] ‹p ⊆ c⇩w ∪ c⇩n› by simp

      have "eval_dom x (g d') c⇩w c⇩n infl' stabl' p' σ' pinfl' post'"
      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⇩w, c⇩n, infl', stabl', p', σ', pinfl', post')), st)
          ∈ term_relation"
          using Eval unfolding term_relation_def prod_relation_def by simp
        moreover have
          "term_cond (Inr (Inr (x, g d', c⇩w, c⇩n, infl', stabl', p', σ', pinfl', post')))"
        proof -
          have "p' ⊆ c⇩w ∪ c⇩n"
            using Eval point_set_incr(1)[OF query_dom query] less.prems Eval by simp
          moreover have "stabl ⊆ stabl'" "fset (fmdom infl') ⊆ stabl'"
              "(∀u. (slookup infl' u - slookup infl u) ∩ (stabl - {x}) = {})"
            using less.prems Eval stabl_infl_properties(1)[OF query_dom query] by auto
          moreover have "c⇩w ∪ c⇩n ⊆ stabl" using less.prems Eval by simp
          moreover have "{u ∈ c⇩w ∪ c⇩n. slookup infl' u ≠ {}} ⊆ p'"
            using less.prems Eval called_with_non_empty_infl_in_point(1)[OF query_dom query]
            by simp
          ultimately show ?thesis by auto
        qed
        ultimately show ?thesis using less.IH ‹p' ⊆ c⇩w ∪ c⇩n› unfolding eval_dom_def by auto
      qed
      then show ?thesis
        using query_iterate_eval.domintros(3)[of t x c⇩w c⇩n 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 solve_termination: "solve_dom x"
  unfolding solve_dom_def using cond_termination by auto

end
end ― ‹end of context for termination proof›

end