Theory Coincidence

theory "Coincidence" 
imports
  "Lib"
  "Syntax"
  "Denotational_Semantics"
  "Static_Semantics"
  "HOL.Finite_Set"
begin
section ‹Static Semantics Properties›

subsection Auxiliaries

text ‹The state interpolating ‹stateinterpol ν ω S› between ‹ν› and ‹ω› that is ‹ν› on ‹S› and ‹ω› elsewhere›

definition stateinterpol:: "state ⇒ state ⇒ variable set ⇒ state"
  where
  "stateinterpol ν ω S = (λx. if (x∈S) then ν(x) else ω(x))"

definition statediff:: "state ⇒ state ⇒ variable set"
  where "statediff ν ω = {x. ν(x)≠ω(x)}"

lemma nostatediff: "x∉statediff ν ω ⟹ ν(x)=ω(x)"
  by (simp add: statediff_def)

lemma stateinterpol_empty: "stateinterpol ν ω {} = ω"
proof
  fix x
  have empty: "⋀x. ¬(x∈{})" by auto
  show "⋀x. stateinterpol ν ω {} x = ω x" using empty by (simp add: stateinterpol_def)
qed

lemma stateinterpol_left [simp]: "x∈S ⟹ (stateinterpol ν ω S)(x)=ν(x)"
  by (simp add: stateinterpol_def)

lemma stateinterpol_right [simp]: "x∉S ⟹ (stateinterpol ν ω S)(x)=ω(x)"
  by (simp add: stateinterpol_def)

lemma Vagree_stateinterpol [simp]: "Vagree (stateinterpol ν ω S) ν S"
  and "Vagree (stateinterpol ν ω S) ω (-S)"
  unfolding Vagree_def by auto

lemma Vagree_ror: "Vagree ν ν' (V∩W) ⟹ (∃ω. (Vagree ν ω V ∧ Vagree ω ν' W))"
proof -
  assume "Vagree ν ν' (V∩W)"
  hence "∀x. x∈V∩W ⟶ ν(x)=ν'(x)" by (simp add: Vagree_def)
  let ?w="stateinterpol ν ν' V"
  have l: "Vagree ν ?w V" by (simp add: Vagree_def)
  have r: "Vagree ?w ν' W ∧ Vagree ?w ν' W" by (simp add: Vagree_def stateinterpol_def ‹∀x. x∈V∩W ⟶ ν x = ν' x›)
  have "Vagree ν ?w V ∧ Vagree ?w ν' W" using l and r by blast
  thus ?thesis by auto
qed


text ‹Remark 8 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15› about simple properties of projections›

lemma restrictto_extends [simp]: "restrictto X V ⊇ X"
  by (auto simp add: restrictto_def)

lemma restrictto_compose [simp]: "restrictto (restrictto X V) W = restrictto X (V∩W)"
proof
  show "restrictto (restrictto X V) W ⊆ restrictto X (V∩W)"
    by (auto simp add: restrictto_def Vagree_def)
next
  show "restrictto X (V∩W) ⊆ restrictto (restrictto X V) W" 
  (*by (smt Vagree_ror mem_Collect_eq restrictto_def subsetI)*)
  proof - (* sledgehammer *)
  obtain rr :: "(variable ⇒ real) set ⇒ (variable ⇒ real) set ⇒ variable ⇒ real" where
  "∀x0 x1. (∃v2. v2 ∈ x1 ∧ v2 ∉ x0) = (rr x0 x1 ∈ x1 ∧ rr x0 x1 ∉ x0)"
    by moura
  then have f1: "∀F Fa. rr Fa F ∈ F ∧ rr Fa F ∉ Fa ∨ F ⊆ Fa"
  by (meson subsetI)
  obtain rra :: "(variable ⇒ real) ⇒ variable set ⇒ (variable ⇒ real) set ⇒ variable ⇒ real" where
  "∀x0 x1 x2. (∃v3. v3 ∈ x2 ∧ Vagree v3 x0 x1) = (rra x0 x1 x2 ∈ x2 ∧ Vagree (rra x0 x1 x2) x0 x1)"
  by moura
  then have f2: "∀F V f. (f ∉ {f. ∃fa. fa ∈ F ∧ Vagree fa f V} ∨ rra f V F ∈ F ∧ Vagree (rra f V F) f V) ∧ (f ∈ {f. ∃fa. fa ∈ F ∧ Vagree fa f V} ∨ (∀fa. fa ∉ F ∨ ¬ Vagree fa f V))"
  by blast
  moreover
  { assume "∃f. f ∈ X ∧ Vagree f (v4_1 W V (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (rra (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (V ∩ W) X)) V"
    moreover
    { assume "∃f. f ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree f (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) W"
      then have "rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ∉ {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ∨ rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ∈ {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W}"
      by blast
      then have "{f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ⊆ {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W}"
      using f1 by meson }
    ultimately have "(¬ Vagree (rra (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (V ∩ W) X) (v4_1 W V (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (rra (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (V ∩ W) X)) V ∨ ¬ Vagree (v4_1 W V (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (rra (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) (V ∩ W) X)) (rr {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W} {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)}) W) ∨ {f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ⊆ {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W}"
    using f2 by meson }
  ultimately have "{f. ∃fa. fa ∈ X ∧ Vagree fa f (V ∩ W)} ⊆ {f. ∃fa. fa ∈ {f. ∃fa. fa ∈ X ∧ Vagree fa f V} ∧ Vagree fa f W}"
  using f1 by (meson Vagree_ror)
  then show ?thesis
  using restrictto_def by presburger
  qed 
qed

lemma restrictto_antimon [simp]: "W⊇V ⟹ restrictto X W ⊆ restrictto X V"
proof -
  assume "W⊇V"
  then have "∃U. V=W∩U" by auto
  then obtain U where "V=W∩U" by auto
  hence "restrictto X V = restrictto (restrictto X W) U" by simp
  hence "restrictto X V ⊇ restrictto X W" using restrictto_extends by blast
  thus ?thesis by auto
qed

lemma restrictto_empty [simp]: "X≠{} ⟹ restrictto X {} = worlds"
  by (auto simp add: restrictto_def worlds_def)

lemma selectlike_shrinks [simp]: "selectlike X ν V ⊆ X"
  by (auto simp add: selectlike_def)

lemma selectlike_compose [simp]: "selectlike (selectlike X ν V) ν W = selectlike X ν (V∪W)"
  by (auto simp add: selectlike_def)

lemma selectlike_antimon [simp]: "W⊇V ⟹ selectlike X ν W ⊆ selectlike X ν V"
  by (auto simp add: selectlike_def)

lemma selectlike_empty [simp]: "selectlike X ν {} = X"
  by (auto simp add: selectlike_def)

lemma selectlike_self [simp]: "(ν ∈ selectlike X ν V) = (ν∈X)"
  by (auto simp add: selectlike_def)

lemma selectlike_complement [simp]: "selectlike (-X) ν V ⊆ -selectlike X ν V"
  by (auto simp add: selectlike_def)

lemma selectlike_union: "selectlike (X∪Y) ν V = selectlike X ν V ∪ selectlike Y ν V"
  by (auto simp add: selectlike_def)

lemma selectlike_Sup: "selectlike (Sup M) ν V = Sup {selectlike X ν V | X. X∈M}"
  using selectlike_def by auto

lemma selectlike_equal_cond: "(selectlike X ν V = selectlike Y ν V) = (∀μ. Uvariation μ ν (-V) ⟶ (μ∈X) = (μ∈Y))"
  unfolding selectlike_def using Uvariation_Vagree by auto

lemma selectlike_equal_cocond: "(selectlike X ν (-V) = selectlike Y ν (-V)) = (∀μ. Uvariation μ ν V ⟶ (μ∈X) = (μ∈Y))"
  using selectlike_equal_cond[where V=‹-V›] by simp

lemma selectlike_equal_cocond_rule: "(⋀μ. Uvariation μ ν (-V) ⟹ (μ∈X) = (μ∈Y))
  ⟹ (selectlike X ν V = selectlike Y ν V)"
  using selectlike_equal_cond[where V=‹V›] by simp

lemma selectlike_equal_cocond_corule: "(⋀μ. Uvariation μ ν V ⟹ (μ∈X) = (μ∈Y))
  ⟹ (selectlike X ν (-V) = selectlike Y ν (-V))"
  using selectlike_equal_cond[where V=‹-V›] by simp

lemma co_selectlike: "-(selectlike X ν V) = (-X) ∪ {ω. ¬Vagree ω ν V}"
  unfolding selectlike_def by auto

lemma selectlike_co_selectlike: "selectlike (-(selectlike X ν V)) ν V = selectlike (-X) ν V"
  unfolding selectlike_def by auto

lemma selectlike_Vagree: "Vagree ν ω V ⟹ selectlike X ν V = selectlike X ω V"
  using Vagree_def selectlike_def by auto  

lemma similar_selectlike_mem: "Vagree ν ω V ⟹ (ν∈selectlike X ω V) = (ν∈X)"
  unfolding selectlike_def using Vagree_sym_rel by blast  

(* also see nonBVG_rule *)
lemma BVG_nonelem [simp] :"(x∉BVG α) = (∀I ω X. (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω {x})))"
  using BVG_elem monotone selectlike_shrinks
  by (metis subset_iff)


text ‹‹statediff› interoperability›

lemma Vagree_statediff [simp]: "Vagree ω ω' S ⟹ statediff ω ω' ⊆ -S"
  by (auto simp add: Vagree_def statediff_def)

lemma stateinterpol_diff [simp]: "stateinterpol ν ω (statediff ν ω) = ν"
proof
  fix x
  show sp: "(stateinterpol ν ω (statediff ν ω))(x) = ν(x)"
  proof (cases "x∈statediff ν ω")
    case True
    then show ?thesis by simp
  next
    case False
    then show ?thesis by (simp add: stateinterpol_def nostatediff)
  qed
qed

lemma stateinterpol_insert: "Vagree (stateinterpol v w S) (stateinterpol v w (insert z S)) (-{z})"
   by (simp add: Vagree_def stateinterpol_def)


lemma stateinterpol_FVT [simp]: "z∉FVT(t) ⟹ term_sem I t (stateinterpol ω ω' S) = term_sem I t (stateinterpol ω ω' (insert z S))"
proof -
  assume a: "z∉FVT(t)"
  have fvc: "⋀v. ⋀w. Vagree v w (-{z}) ⟹ (term_sem I t v = term_sem I t w)" using a by (simp add: FVT_def)
  then show "term_sem I t (stateinterpol ω ω' S) = term_sem I t (stateinterpol ω ω' (insert z S))"
    using fvc and stateinterpol_insert by blast
qed

subsection ‹Coincidence Lemmas›

paragraph ‹Coincidence for Terms›

text ‹Lemma 10 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15››

theorem coincidence_term: "Vagree ω ω' (FVT θ) ⟹ term_sem I θ ω = term_sem I θ ω'"
proof -
  assume a: "Vagree ω ω' (FVT θ)"
  have isS: "statediff ω ω' ⊆ -FVT(θ)" using a and Vagree_statediff by simp
  have gen: "S⊆-FVT(θ) ⟹ (term_sem I θ ω' = term_sem I θ (stateinterpol ω ω' S))" if "finite S" for S
    using that
  proof (induction S)
    case empty
    show ?case by (simp add: stateinterpol_empty)
  next
    case (insert z S)
    thus ?case by auto
    qed
  from isS have finS: "finite (statediff ω ω')" using allvars_finite by (metis FVT_finite UNIV_def finite_compl rev_finite_subset)
  show ?thesis using gen[where S=‹statediff ω ω'›, OF finS, OF isS] by simp
qed

corollary coincidence_term_cor: "Uvariation ω ω' U ⟹ (FVT θ)∩U={} ⟹ term_sem I θ ω = term_sem I θ ω'"
using coincidence_term Uvariation_Vagree
  by (metis Vagree_antimon disjoint_eq_subset_Compl double_compl)

  
lemma stateinterpol_FVF [simp]: "z∉FVF(e) ⟹ 
  ((stateinterpol ω ω' S) ∈ fml_sem I e ⟷ (stateinterpol ω ω' (insert z S)) ∈ fml_sem I e)"
proof -
  assume a: "z∉FVF(e)"
  have agr: "Vagree (stateinterpol ω ω' S) (stateinterpol ω ω' (insert z S)) (-{z})" by (simp add: Vagree_def stateinterpol_def)
  have fvc: "⋀v. ⋀w. (Vagree v w (-{z}) ⟹ (v∈fml_sem I e ⟹ w∈fml_sem I e))" using a by (simp add: FVF_def)
  then have fvce: "⋀v. ⋀w. (Vagree v w (-{z}) ⟹ ((v∈fml_sem I e) = (w∈fml_sem I e)))"  using Vagree_sym_rel by blast
  then show "(stateinterpol ω ω' S) ∈ fml_sem I e ⟷ (stateinterpol ω ω' (insert z S)) ∈ fml_sem I e"
    using agr by simp
qed


paragraph ‹Coincidence for Formulas›

text ‹Lemma 11 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15››

theorem coincidence_formula: "Vagree ω ω' (FVF φ) ⟹ (ω ∈ fml_sem I φ ⟷ ω' ∈ fml_sem I φ)"
proof -
  assume a: "Vagree ω ω' (FVF φ)"
  have isS: "statediff ω ω' ⊆ -FVF(φ)" using a and Vagree_statediff by simp
  have gen: "S⊆-FVF(φ) ⟹ (ω' ∈ fml_sem I φ ⟷ (stateinterpol ω ω' S) ∈ fml_sem I φ)" if "finite S" for S
    using that
  proof (induction S)
    case empty
    show ?case by (simp add: stateinterpol_empty)
  next
    case (insert z S)
    thus ?case by auto
  qed
  from isS have finS: "finite (statediff ω ω')" using allvars_finite by (metis FVF_finite UNIV_def finite_compl rev_finite_subset)
  show ?thesis using gen[where S=‹statediff ω ω'›, OF finS, OF isS] by simp
qed

corollary coincidence_formula_cor: "Uvariation ω ω' U ⟹ (FVF φ)∩U={} ⟹ (ω ∈ fml_sem I φ ⟷ ω' ∈ fml_sem I φ)"
  using coincidence_formula Uvariation_Vagree 
  by (metis Uvariation_def disjoint_eq_subset_Compl inf.commute subsetCE)


paragraph ‹Coincidence for Games›

text ‹‹Cignorabimus α V› is the set of all sets of variables that can be ignored for the coincidence game lemma›
definition Cignorabimus:: "game ⇒ variable set ⇒ variable set set"
  where
"Cignorabimus α V = {M. ∀I.∀ω.∀ω'.∀X. (Vagree ω ω' (-M) ⟶ (ω∈game_sem I α (restrictto X V)) ⟶ (ω'∈game_sem I α (restrictto X V)))}"

lemma Cignorabimus_finite [simp]: "finite (Cignorabimus α V)"
  unfolding Cignorabimus_def using finite_powerset[OF allvars_finite] finite_subset using Finite_Set.finite_subset by fastforce 

lemma Cignorabimus_equiv [simp]: "Cignorabimus α V = {M. ∀I.∀ω.∀ω'.∀X. (Vagree ω ω' (-M) ⟶ (ω∈game_sem I α (restrictto X V)) = (ω'∈game_sem I α (restrictto X V)))}"
  unfolding Cignorabimus_def by (metis (no_types, lifting) Vagree_sym_rel)

lemma Cignorabimus_antimon [simp]: "M ∈ Cignorabimus α V ∧ N⊆M ⟹ N ∈ Cignorabimus α V"
  unfolding Cignorabimus_def
  using Vagree_antimon by blast 

lemma coempty: "-{}=allvars"
  by simp

lemma Cignorabimus_empty [simp]: "{} ∈ Cignorabimus α V"
  unfolding Cignorabimus_def using coempty Vagree_univ
  by simp

text ‹Cignorabimus contains nonfree variables›
lemma Cignorabimus_init: "V⊇FVG(α) ⟹ x∉V ⟹ {x}∈Cignorabimus α V"
proof-
  assume "V⊇FVG(α)"
  assume a0: "x∉V"
  hence a1: "x∉FVG(α)" using ‹FVG α ⊆ V› by blast
  hence "⋀I v w. Vagree v w (-{x}) ⟹ (v ∈ game_sem I α (restrictto X (-{x})) ⟷ w ∈ game_sem I α (restrictto X (-{x})))" 
  by (metis (mono_tags, lifting) CollectI FVG_def Vagree_sym_rel)
  show "{x}∈Cignorabimus α V"
  proof-
    {
      fix I ω ω' X
      have "Vagree ω ω' (-{x}) ⟶ (ω∈game_sem I α (restrictto X V)) ⟶ (ω'∈game_sem I α (restrictto X V))"
      proof
        assume a2: "Vagree ω ω' (-{x})"
        show "(ω∈game_sem I α (restrictto X V)) ⟶ (ω'∈game_sem I α (restrictto X V))"
        proof
          assume "ω∈game_sem I α (restrictto X V)"
          hence "ω∈game_sem I α (restrictto (restrictto X V) (-{x}))" by (simp add: Int_absorb2 ‹x∉V›)
          hence "ω'∈game_sem I α (restrictto (restrictto X V) (-{x}))" using FVG_def a1 a2 by blast
          hence "ω'∈game_sem I α (restrictto X (V∩-{x}))" by simp
          show "ω'∈game_sem I α (restrictto X V)" using a0
            by (metis Int_absorb2 ‹ω' ∈ game_sem I α (restrictto X (V ∩ - {x}))› subset_Compl_singleton)
        qed
      qed
    }
    thus ?thesis
      unfolding Cignorabimus_def
      by auto
  qed
qed


text ‹Cignorabimus is closed under union›
lemma Cignorabimus_union: "M∈Cignorabimus α V ⟹ N∈Cignorabimus α V ⟹ (M∪N)∈Cignorabimus α V"
proof-
  assume a1: "M∈Cignorabimus α V"
  assume a2: "N∈Cignorabimus α V"
  show "(M∪N)∈Cignorabimus α V" (*using a1 a2 unfolding Cignorabimus_def *)
  proof-
    {
      fix I ω ω' X
    assume a3: "Vagree ω ω' (-(M∪N))"
    have h1: "⋀I ω ω'.⋀X. (Vagree ω ω' (-M) ⟹  (ω∈game_sem I α (restrictto X V)) ⟹ (ω'∈game_sem I α (restrictto X V)))" using a1 by simp
    have h2: "⋀I ω ω'.⋀X. (Vagree ω ω' (-N) ⟹  (ω∈game_sem I α (restrictto X V)) ⟹ (ω'∈game_sem I α (restrictto X V)))" using a2 by simp
    let ?s = "stateinterpol ω' ω M"
    have v1: "Vagree ω ?s (-(M∪N))" using a3 by (simp add: Vagree_def)
    have v2: "Vagree ?s ω' (-(M∪N))" using a3 by (simp add: Vagree_def)
    have r1: "ω∈game_sem I α (restrictto X V) ⟹ ?s∈game_sem I α (restrictto X V)"
      by (metis ComplD Vagree_def h1 stateinterpol_right)
    have r2: "?s∈game_sem I α (restrictto X V) ⟹ ω'∈game_sem I α (restrictto X V)"
      by (metis Vagree_ror compl_sup h1 h2 v2)
    have res: "ω∈game_sem I α (restrictto X V) ⟹ ω'∈game_sem I α (restrictto X V)" using r1 r2 by blast
    }
    thus ?thesis
      unfolding Cignorabimus_def
      by auto
  qed
qed


lemma powersetup_induct [case_names Base Cup]:
   "⋀C. (⋀M. M∈C ⟹ P M) ⟹
    (⋀S. (⋀M. M∈S ⟹ P M) ⟹ P (⋃S)) ⟹
     P (⋃C)"
  by simp

lemma Union_insert: "⋃(insert x S) = x∪⋃S"
  by simp

lemma powerset2up_induct [case_names Finite Nonempty Base Cup]:
   "(finite C) ⟹ (C≠{}) ⟹ (⋀M. M∈C ⟹ P M) ⟹
    (⋀M N. P M ⟹ P N ⟹ P (M∪N)) ⟹
     P (⋃C)"
proof (induction rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert x F)
  then show ?case by force
qed

lemma Cignorabimus_step: "(⋀M. M∈S ⟹ M∈Cignorabimus α V) ⟹ (⋃S)∈Cignorabimus α V"
proof (cases "S={}")
  case True
  then show ?thesis using Cignorabimus_empty by simp
next
  case nonem: False
  then show "⋃S∈Cignorabimus α V" if "⋀M. M∈S ⟹ M∈Cignorabimus α V" and nonemp:"S≠{}" for S
  proof (induction rule: powerset2up_induct)
    case Finite                                                   
    then show ?case using Cignorabimus_finite by (meson infinite_super subset_eq that(1))  
  next
    case Nonempty
    then show ?case using nonemp by simp
  next
    case (Base M)
    then show ?case using that by simp
  next
    case (Cup S)
    then show ?case using that Cignorabimus_union by blast
  qed
qed

text ‹Lemma 12 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15››

theorem coincidence_game: "Vagree ω ω' V ⟹ V⊇FVG(α) ⟹ (ω ∈ game_sem I α (restrictto X V)) = (ω' ∈ game_sem I α (restrictto X V))"
proof-
  assume a1: "Vagree ω ω' V"
  assume a2: "V ⊇ FVG α"
  have base: "{x}∈Cignorabimus α V" if a3: "x∉V" and a4: "V ⊇ FVG α" for x V
    using a3 and a4 and Cignorabimus_init by simp
  have h: "-V = ⋃{xx. ∃x. xx={x} ∧ x∉V}" by auto (* finite *)
  have "(-V)∈Cignorabimus α V" using a2 base h using Cignorabimus_step
  proof - (*sledgehammer*)
    have f1: "∀v V. v ∈ V ∨ ¬ FVG α ⊆ V ∨ {v} ∈ Cignorabimus α V"
      using base by satx
    obtain VV :: "variable set ⇒ game ⇒ variable set set ⇒ variable set" where
      f2: "∀x0 x1 x2. (∃v3. v3 ∈ x2 ∧ v3 ∉ Cignorabimus x1 x0) = (VV x0 x1 x2 ∈ x2 ∧ VV x0 x1 x2 ∉ Cignorabimus x1 x0)"
      by moura
    obtain vv :: "variable set ⇒ variable" where
      f3: "((∄v. VV V α {{v} |v. v ∉ V} = {v} ∧ v ∉ V) ∨ VV V α {{v} |v. v ∉ V} = {vv (VV V α {{v} |v. v ∉ V})} ∧ vv (VV V α {{v} |v. v ∉ V}) ∉ V) ∧ ((∃v. VV V α {{v} |v. v ∉ V} = {v} ∧ v ∉ V) ∨ (∀v. VV V α {{v} |v. v ∉ V} ≠ {v} ∨ v ∈ V))"
      by fastforce
    moreover
    { assume "{vv (VV V α {{v} |v. v ∉ V})} ∈ Cignorabimus α V"
      then have "(VV V α {{v} |v. v ∉ V} ≠ {vv (VV V α {{v} |v. v ∉ V})} ∨ vv (VV V α {{v} |v. v ∉ V}) ∈ V) ∨ VV V α {{v} |v. v ∉ V} ∉ {{v} |v. v ∉ V} ∨ VV V α {{v} |v. v ∉ V} ∈ Cignorabimus α V"
        by metis
      then have "(∃v. VV V α {{v} |v. v ∉ V} = {v} ∧ v ∉ V) ⟶ VV V α {{v} |v. v ∉ V} ∉ {{v} |v. v ∉ V} ∨ VV V α {{v} |v. v ∉ V} ∈ Cignorabimus α V"
        using f3 by blast }
    ultimately have "VV V α {{v} |v. v ∉ V} ∉ {{v} |v. v ∉ V} ∨ VV V α {{v} |v. v ∉ V} ∈ Cignorabimus α V"
      using f1 a2 by blast
    then have "⋃{{v} |v. v ∉ V} ∈ Cignorabimus α V"
      using f2 by (meson Cignorabimus_step)
    then show ?thesis
      using h by presburger
  qed
  from this show ?thesis by (simp add: a1)
qed

corollary coincidence_game_cor: "Uvariation ω ω' U ⟹ U∩FVG(α)={} ⟹ (ω ∈ game_sem I α (restrictto X (-U))) = (ω' ∈ game_sem I α (restrictto X (-U)))"
  using coincidence_game Uvariation_Vagree 
  by (metis Uvariation_Vagree coincidence_game compl_le_swap1 disjoint_eq_subset_Compl double_compl)

  
subsection ‹Bound Effect Lemmas›

text ‹‹Bignorabimus α V› is the set of all sets of variables that can be ignored for boundeffect›
definition Bignorabimus:: "game ⇒ variable set set"
  where
  "Bignorabimus α = {M. ∀I.∀ω.∀X. ω∈game_sem I α X ⟷ ω∈game_sem I α (selectlike X ω M)}"

lemma Bignorabimus_finite [simp]: "finite (Bignorabimus α)"
  unfolding Bignorabimus_def using finite_powerset[OF allvars_finite] finite_subset using Finite_Set.finite_subset by fastforce 

lemma Bignorabimus_single [simp]: "game_sem I α (selectlike X ω M) ⊆ game_sem I α X"
  by (meson monotone selectlike_shrinks subsetCE)

lemma Bignorabimus_equiv [simp]: "Bignorabimus α = {M. ∀I.∀ω.∀X. (ω∈game_sem I α X ⟶ ω∈game_sem I α (selectlike X ω M))}"
  (*by (smt Bignorabimus_def Bignorabimus_single Collect_cong subsetCE)*)
proof - (*sledgehammer transformed*)
  obtain VV :: "(variable set ⇒ bool) ⇒ (variable set ⇒ bool) ⇒ variable set" where
    f1: "∀p pa. (¬ p (VV pa p)) = pa (VV pa p) ∨ Collect p = Collect pa"
    by (metis (no_types) Collect_cong)
  obtain rr :: "variable set ⇒ game ⇒ variable ⇒ real" and ii :: "variable set ⇒ game ⇒ interp" and FF :: "variable set ⇒ game ⇒ (variable ⇒ real) set" where
    f2: "∀x0 x1. (∃v2 v3 v4. (v3 ∈ game_sem v2 x1 v4) ≠ (v3 ∈ game_sem v2 x1 (selectlike v4 v3 x0))) = ((rr x0 x1 ∈ game_sem (ii x0 x1) x1 (FF x0 x1)) ≠ (rr x0 x1 ∈ game_sem (ii x0 x1) x1 (selectlike (FF x0 x1) (rr x0 x1) x0)))"
    by moura
    have fact: "{V. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))} = {V. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)}"
        using f1 by (metis (no_types, opaque_lifting) Bignorabimus_single subsetCE)
  have f3: "rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∉ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (selectlike (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))) ∨ rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∈ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α)"
    using Bignorabimus_single by blast
  have f4: "(¬ (∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))) ∨ (∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))))) ∧ ((∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))) ∨ (rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∉ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α)) = (rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∈ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (selectlike (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))))"
    using f2 by blast
  have "rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∈ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) ⟶ (∃i f F. f ∈ game_sem i α F ∧ f ∉ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))) ∨ rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α ∈ game_sem (ii (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) α (selectlike (FF (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (rr (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))) α) (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))"
    by blast
  moreover
  { assume "∃i f F. f ∈ game_sem i α F ∧ f ∉ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))"
    then have "¬ (∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))"
      by blast
    moreover
    { assume "(¬ (∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))) ≠ (∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))))"
      then have "{V. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))} = {V. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)}"
        using fact by simp }
    ultimately have "(∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))) ∨ {V. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))} = {V. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)}"
      by satx }
  moreover
  { assume "∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))"
    then have "(¬ (∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)))))) ≠ (∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f (VV (λV. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))) (λV. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V))))))"
      by blast
    then have "{V. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))} = {V. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)}"
      using fact by simp}
  ultimately have "{V. ∀i f F. (f ∈ game_sem i α F) = (f ∈ game_sem i α (selectlike F f V))} = {V. ∀i f F. f ∈ game_sem i α F ⟶ f ∈ game_sem i α (selectlike F f V)}"
    using f4 f3 by satx
  then show ?thesis
    using Bignorabimus_def by presburger
qed 

lemma Bignorabimus_empty [simp]: "{} ∈ Bignorabimus α"
  unfolding Bignorabimus_def using coempty selectlike_empty
  by simp

lemma Bignorabimus_init: "x∉BVG(α) ⟹ {x}∈Bignorabimus α"
  unfolding Bignorabimus_def BVG_def
proof-
  assume "x ∉ {x. ∃I ω X. ω ∈ game_sem I α X ∧ ω ∉ game_sem I α (selectlike X ω {x})}"
  hence "¬(∃I ω X. ω ∈ game_sem I α X ∧ ω ∉ game_sem I α (selectlike X ω {x}))" by simp
  hence "∀I ω X. (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω {x}))" using Bignorabimus_single by blast
  thus "{x} ∈ {M. ∀I ω X. (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω M))}" by simp
qed

text ‹Bignorabimus is closed under union›
lemma Bignorabimus_union: "M∈Bignorabimus α ⟹ N∈Bignorabimus α ⟹ (M∪N)∈Bignorabimus α"
proof -
  assume a1: "M∈Bignorabimus α"
  assume a2: "N∈Bignorabimus α"
  have h1: "∀I.∀ω.∀X. (ω∈game_sem I α X) ⟷ (ω∈game_sem I α (selectlike X ω M))" using a1
    using Bignorabimus_equiv Bignorabimus_single by blast
  have h2: "∀I.∀ω.∀X. (ω∈game_sem I α X) ⟷ (ω∈game_sem I α (selectlike X ω N))" using a2
    using Bignorabimus_equiv Bignorabimus_single by blast
  have c: "∀I.∀ω.∀X. (ω∈game_sem I α X) ⟷ (ω∈game_sem I α (selectlike X ω (M∪N)))" by (metis h1 h2 selectlike_compose)
  then show "(M∪N)∈Bignorabimus α" unfolding Bignorabimus_def using c by fastforce 
qed

lemma Bignorabimus_step: "(⋀M. M∈S ⟹ M∈Bignorabimus α) ⟹ (⋃S)∈Bignorabimus α"
proof (cases "S={}")
  case True
  then show ?thesis using Bignorabimus_empty by simp
next
  case nonem: False
  then show "⋃S∈Bignorabimus α" if "⋀M. M∈S ⟹ M∈Bignorabimus α" and nonemp:"S≠{}" for S
  proof (induction rule: powerset2up_induct)
    case Finite
    then show ?case using Bignorabimus_finite by (meson infinite_super subset_eq that(1))  
  next
    case Nonempty
    then show ?case using nonemp by simp
  next
    case (Base M)
    then show ?case using that by simp
  next
    case (Cup S)
    then show ?case using that Bignorabimus_union by blast
  qed
qed


text ‹Lemma 13 🌐‹https://doi.org/10.1007/978-3-319-94205-6_15››

theorem boundeffect: "(ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω (-BVG(α))))"
proof-
  have base: "{x}∈Bignorabimus α" if a3: "x∉BVG α" for x using a3 and Bignorabimus_init by simp
  have h: "-BVG α = ⋃{xx. ∃x. xx={x} ∧ x∉BVG α}" by blast (* finite *)
  have "(-BVG α)∈Bignorabimus α" using base h
  (*by (smt Bignorabimus_step mem_Collect_eq)*)
  proof - (*sledgehammer*)
    obtain VV :: "game ⇒ variable set set ⇒ variable set" where
      f1: "∀x0 x1. (∃v2. v2 ∈ x1 ∧ v2 ∉ Bignorabimus x0) = (VV x0 x1 ∈ x1 ∧ VV x0 x1 ∉ Bignorabimus x0)"
      by moura
    have "VV α {{v} |v. v ∉ BVG α} ∉ {{v} |v. v ∉ BVG α} ∨ VV α {{v} |v. v ∉ BVG α} ∈ Bignorabimus α"
      by fastforce
    then have "⋃{{v} |v. v ∉ BVG α} ∈ Bignorabimus α"
      using f1 by (meson Bignorabimus_step)
    then show ?thesis
      using h by presburger
  qed
  from this show ?thesis using Bignorabimus_def by blast
qed

corollary boundeffect_cor: "V∩BVG(α)={} ⟹ (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω V))"
  using boundeffect
  by (metis disjoint_eq_subset_Compl selectlike_compose sup.absorb_iff2)


subsection ‹Static Analysis Observations›

lemma BVG_equiv: "game_equiv α β ⟹ BVG(α) = BVG(β)"
proof-
  assume a: "game_equiv α β" 
  show "BVG(α) = BVG(β)" unfolding BVG_def using game_equiv_subst_eq[OF a] by metis
qed

lemmas union_or = Set.Un_iff

lemma not_union_or: "(x∉A∪B) = (x∉A ∧ x∉B)"
  by simp

lemma repv_selectlike_self: "(repv ω x d ∈ selectlike X ω {x}) = (d=ω(x) ∧ ω ∈ X)"
  unfolding selectlike_def using Vagree_repv_self Vagree_sym
  by (metis (no_types, lifting) mem_Collect_eq repv_self)

lemma repv_selectlike_other: "x≠y ⟹ (repv ω x d ∈ selectlike X ω {y}) = (repv ω x d ∈ X)"
proof
  assume a: "x≠y"
  then have h: "{y}⊆-{x}" by simp
  show "(repv ω x d ∈ selectlike X ω {y}) ⟹ (repv ω x d ∈ X)" using a selectlike_def Vagree_repv[of ω x d] 
  by auto
  show "(repv ω x d ∈ X) ⟹ (repv ω x d ∈ selectlike X ω {y})" 
  using selectlike_def[where X=X and ν=ω and V=‹-{x}›] Vagree_repv[where ω=ω and x=x and d=d]
  selectlike_antimon[where X=X and ν=ω and V=‹{y}› and W=‹-{x}›, OF h] Vagree_sym[where ν=‹repv ω x d› and V=‹-{x}›]
  by auto
qed

lemma repv_selectlike_other_converse: "x≠y ⟹ (repv ω x d ∈ X) = (repv ω x d ∈ selectlike X ω {y})"
  using repv_selectlike_other HOL.eq_commute by blast


lemma BVG_assign_other: "x≠y ⟹ y∉BVG(Assign x θ)"
  using repv_selectlike_other_converse[where x=x and y=y] by simp

lemma BVG_assign_meta: "(⋀I ω. term_sem I θ ω = ω(x)) ⟹ BVG(Assign x θ) = {}"
  and "term_sem I θ ω ≠ ω(x) ⟹ BVG(Assign x θ) = {x}"
  (*using repv_selectlike_self BVG_assign_other BVG_def BVG_elem*)
proof-
  have fact: "BVG(Assign x θ) ⊆ {x}" using BVG_assign_other by (metis singleton_iff subsetI)
  from fact show "(⋀I ω. term_sem I θ ω = ω(x)) ⟹ BVG(Assign x θ) = {}" using BVG_def by simp
  have h2: "∃I ω. term_sem I θ ω ≠ ω(x) ⟹ x ∈ BVG(Assign x θ)" using repv_selectlike_self by auto
  from fact show "term_sem I θ ω ≠ ω(x) ⟹ BVG(Assign x θ) = {x}" using BVG_elem h2 by blast 
qed

lemma BVG_assign: "BVG(Assign x θ) = (if (∀I ω. term_sem I θ ω = ω(x)) then {} else {x})"
using repv_selectlike_self repv_selectlike_other BVG_assign_other 
proof-
  have c0: "BVG(Assign x θ) ⊆ {x}" using BVG_assign_other by (metis singletonI subsetI)
  have c1: "∀I ω. term_sem I θ ω = ω(x) ⟹ BVG(Assign x θ) = {}" using BVG_assign_other by auto
  have h2: "∃I ω. term_sem I θ ω ≠ ω(x) ⟹ x ∈ BVG(Assign x θ)" using repv_selectlike_self by auto
  have c2: "∃I ω. term_sem I θ ω ≠ ω(x) ⟹ BVG(Assign x θ) = {x}" using c0 h2 by blast 
  from c1 and c2 show ?thesis by simp
qed

lemma BVG_ODE_other: "y≠RVar x ⟹ y≠DVar x ⟹ y∉BVG(ODE x θ)"
  (*using nonBVG_rule selectlike_equal_cocond_rule solves_ODE_def*)
proof-
  assume yx: "y≠RVar x"
  assume yxp: "y≠DVar x"
  show "y∉BVG(ODE x θ)"
  proof (rule nonBVG_inc_rule)
    fix I ω X
    assume "ω ∈ game_sem I (ODE x θ) X"
    then have "∃F T. Vagree ω (F(0)) (-{DVar x}) ∧ F(T) ∈ X ∧ solves_ODE I F x θ" by simp
    then obtain F T where "Vagree ω (F(0)) (-{DVar x}) ∧ F(T) ∈ X ∧ solves_ODE I F x θ" by blast
    then have "Vagree ω (F(0)) (-{DVar x}) ∧ F(T) ∈ (selectlike X ω {y}) ∧ solves_ODE I F x θ"
    using yx yxp solves_Vagree Vagree_def similar_selectlike_mem by auto 
    then have "∃F T. Vagree ω (F(0)) (-{DVar x}) ∧ F(T) ∈ (selectlike X ω {y}) ∧ solves_ODE I F x θ" by blast 
    then show "ω ∈ game_sem I (ODE x θ) (selectlike X ω {y})" by simp
  qed
qed

text ‹This result could be strengthened to a conditional equality based on the RHS values›

lemma BVG_ODE: "BVG(ODE x θ) ⊆ {RVar x,DVar x}"
  using BVG_ODE_other by blast


lemma BVG_test: "BVG(Test φ) = {}"
  unfolding BVG_def game_sem.simps by auto


lemma BVG_choice: "BVG(Choice α β) ⊆ BVG(α) ∪ BVG(β)"
  unfolding BVG_def game_sem.simps using not_union_or by auto
(*proof-
  have f1: "⋀ω I X. (ω ∈ game_sem I α X ∪ game_sem I β X) = 
  (ω ∈ game_sem I α X ∨ ω ∈ game_sem I β X)" by (rule union_or)
  have f2: "⋀ω I X. (ω ∉ game_sem I α (selectlike X ω {x}) ∪ game_sem I β (selectlike X ω {x})) =
  (ω ∉ game_sem I α (selectlike X ω {x}) ∧ ω ∉ game_sem I β (selectlike X ω {x}))" by (rule not_union_or)
  let ?lhs = "{x. ∃I ω X.
           ω ∈ game_sem I α X ∪ game_sem I β X ∧
           ω ∉ game_sem I α (selectlike X ω {x}) ∪ game_sem I β (selectlike X ω {x})}"
  let ?rhs = "{x. ∃I ω X. ω ∈ game_sem I α X ∧ ω ∉ game_sem I α (selectlike X ω {x})} ∪
       {x. ∃I ω X. ω ∈ game_sem I β X ∧ ω ∉ game_sem I β (selectlike X ω {x})}"
  show "?lhs⊆?rhs" using f1 f2 by auto
qed*)

lemma select_nonBV: "x∉BVG(α) ⟹ selectlike (game_sem I α (selectlike X ω {x})) ω {x} = selectlike (game_sem I α X) ω {x}"
proof
  show "selectlike (game_sem I α (selectlike X ω {x})) ω {x} ⊆ selectlike (game_sem I α X) ω {x}" 
  using game_sem_mono selectlike_shrinks selectlike_antimon Bignorabimus_single
  by (metis selectlike_union sup.absorb_iff1) 
  next
  assume nonbound: "x∉BVG(α)"
  then have fact: "{x}∩BVG(α)={}" by auto
  show "selectlike (game_sem I α X) ω {x} ⊆ selectlike (game_sem I α (selectlike X ω {x})) ω {x}"
  proof
    fix μ
    assume "μ ∈ selectlike (game_sem I α X) ω {x}"
    (* "V∩BVG(α)={} ⟹ (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω V))" *)
    then have "μ ∈ selectlike (game_sem I α (selectlike X μ {x})) ω {x}"
    using boundeffect_cor[where ω=μ and V=‹{x}› and α=α, OF fact] nonbound
    by (metis ComplD ComplI co_selectlike not_union_or)
    then show "μ ∈ selectlike (game_sem I α (selectlike X ω {x})) ω {x}" using selectlike_Vagree selectlike_def by fastforce 
  qed
qed

lemma BVG_compose: "BVG(Compose α β) ⊆ BVG(α) ∪ BVG(β)"
  (*unfolding BVG_def game_sem.simps using game_union union_or not_union_or selectlike_shrinks monotone selectlike_compose*)
proof
  fix x
  assume a: "x∈BVG(Compose α β)"
  show "x ∈ BVG α ∪ BVG β"
  proof (rule ccontr)
    assume "x∉BVG α ∪ BVG(β)"
    then have nβ: "x∉BVG(β)"
    and nα: "x∉BVG(α)" by simp_all
    from a have "∃I.∃ω.∃X. ω ∈ game_sem I (Compose α β) X ∧ ω ∉ game_sem I (Compose α β) (selectlike X ω {x})" by simp
    then obtain I ω X where adef: "ω ∈ game_sem I (Compose α β) X ∧ ω ∉ game_sem I (Compose α β) (selectlike X ω {x})" by blast
    from adef have a1: "ω ∈ game_sem I α (game_sem I β X)" by simp
    from adef have a2: "ω ∉ game_sem I α (game_sem I β (selectlike X ω {x}))" by simp
    let ?Y = "selectlike X ω {x}"
    from nα have nαc: "⋀I ω X. (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω {x}))" using BVG_nonelem by simp
    from nβ have nβc: "⋀I ω X. (ω ∈ game_sem I β X) = (ω ∈ game_sem I β (selectlike X ω {x}))" using BVG_nonelem by simp
    have c1: "ω ∈ game_sem I α (selectlike (game_sem I β X) ω {x})" using a1 nαc[where I=I and ω=ω and X=‹game_sem I β X›] by blast
    have c2: "ω ∉ game_sem I α (selectlike (game_sem I β ?Y) ω {x})" using a2 nαc[where I=I and ω=ω and X=‹game_sem I β ?Y›] by blast
    from c2 have c3: "ω ∉ game_sem I α (selectlike (game_sem I β X) ω {x})" using nβ selectlike_Vagree
    proof-
      have "selectlike (game_sem I β ?Y) ω {x} = selectlike (game_sem I β X) ω {x}" using nβ by (rule select_nonBV) 
      thus ?thesis using c2 by simp
    qed
    show "False" using c1 c3 nβc[where I=I] by auto
  qed
qed


text ‹The converse inclusion does not hold generally, because
   ‹BVG(x := x+1; x:= x-1) = {} ≠ BVG(x := x+1) ∪ BVG(x := x-1) = {x}››

lemma "BVG(Compose (Assign x (Plus (Var x) (Number 1))) (Assign x (Plus (Var x) (Number (-1))))) 
    ≠ BVG(Assign x (Plus (Var x) (Number 1))) ∪ BVG(Assign x (Plus (Var x) (Number (-1))))"
    unfolding BVG_def selectlike_def repv_def Vagree_def by auto


lemma BVG_loop: "BVG(Loop α) ⊆ BVG(α)"
proof
  fix x
  assume a: "x∈BVG(Loop α)"
  show "x ∈ BVG(α)"
  proof (rule ccontr)
    assume "¬ (x ∈ BVG(α))"
    then have nα: "x∉BVG α" by simp
    from nα have nαc: "⋀I ω X. (ω ∈ game_sem I α X) = (ω ∈ game_sem I α (selectlike X ω {x}))" using BVG_nonelem by simp
    have "x∉BVG(Loop α)" (*using BVG_nonelem*)
    proof (rule nonBVG_rule)
      fix I ω X
      let ?f = "λZ. X ∪ game_sem I α Z"
      let ?g = "λY. (selectlike X ω {x}) ∪ game_sem I α Y"
      let ?R = "λZ Y. selectlike Z ω {x} = selectlike Y ω {x}"
      have "?R (lfp ?f) (lfp ?g)"
      proof (induction rule: lfp_lockstep_induct[where f=‹?f› and g=‹?g› and R=‹?R›])
        case monof
        then show ?case using game_sem_loop_fixpoint_mono by simp
      next
        case monog
        then show ?case using game_sem_loop_fixpoint_mono by simp
      next
        case (step A B)
        then have IH: "selectlike A ω {x} = selectlike B ω {x}" by simp
        then show ?case
        (* using selectlike_union nα select_nonBV IH by (smt insert_absorb2 insert_def selectlike_compose singleton_conv smt_solver=cvc4)  *)
        proof-
          have "selectlike (X ∪ game_sem I α A) ω {x} = selectlike X ω {x} ∪ selectlike (game_sem I α A) ω {x}" using selectlike_union by simp
          also have "... = selectlike X ω {x} ∪ selectlike (game_sem I α (selectlike A ω {x})) ω {x}" using nα select_nonBV by blast 
          also have "... = selectlike X ω {x} ∪ selectlike (game_sem I α (selectlike B ω {x})) ω {x}" using IH by simp
          also have "... = selectlike (selectlike X ω {x} ∪ game_sem I α B) ω {x}" using selectlike_union nα select_nonBV by auto 
          finally show "selectlike (X ∪ game_sem I α A) ω {x} = selectlike (selectlike X ω {x} ∪ game_sem I α B) ω {x}" .
        qed
        next
        case (union M)
        then have IH: "∀(A,B)∈M. selectlike A ω {x} = selectlike B ω {x}" .
        then show ?case
        using fst_proj_mem[where M=M] snd_proj_mem[where M=M] 
        selectlike_Sup[where ν=ω and V=‹{x}›] sup_corr_eq_chain by simp
        (*proof-
          have "selectlike (⋃fst_proj M) ω {x} = ⋃{selectlike A ω {x} | A. A∈fst_proj M}" using selectlike_Sup by simp
          also have "... = ⋃{selectlike B ω {x} | B. B∈snd_proj M}" using sup_corr_eq_chain[OF IH] by simp
          also have "... = selectlike (⋃snd_proj M) ω {x}" using selectlike_Sup by simp
          finally show "selectlike (⋃fst_proj M) ω {x} = selectlike (⋃snd_proj M) ω {x}" .
        qed*)
      qed
      from this show "(ω ∈ game_sem I (Loop α) X) = (ω ∈ game_sem I (Loop α) (selectlike X ω {x}))"
      by (metis (mono_tags) game_sem.simps(6) lfp_def selectlike_self) 
      (*by (simp add: selectlike_self game_sem_loop_back)*)
    qed
  then show "False" using a by blast  
  qed
qed


lemma BVG_dual: "BVG(Dual α) ⊆ BVG(α)"
  (*unfolding game_sem.simps using BVG_elem selectlike_co_selectlike co_selectlike selectlike_complement selectlike_antimon*)
proof
  fix x
  assume a: "x∈BVG(Dual α)"
  show "x∈BVG α"
  proof-
    from a have "∃I.∃ω.∃X. ω ∈ game_sem I (Dual α) X ∧ ω ∉ game_sem I (Dual α) (selectlike X ω {x})" by simp
    then obtain I ω X where adef: "ω ∈ game_sem I (Dual α) X ∧ ω ∉ game_sem I (Dual α) (selectlike X ω {x})" by blast
    from adef have a1: "ω ∉ game_sem I α (- X)" by simp
    from adef have a2: "ω ∈ game_sem I α (- selectlike X ω {x})" by simp
    let ?Y = "- selectlike X ω {x}"
    have f1: "ω ∈ game_sem I α ?Y" by (rule a2)
    have f2: "ω ∉ game_sem I α (selectlike ?Y ω {x})" using a1 selectlike_co_selectlike
    by (metis (no_types, lifting) selectlike_shrinks monotone dual_order.trans subset_Compl_singleton)
    show "x∈BVG(α)" using f1 f2 by auto
  qed
qed
  
end