Theory SAS_Plus_STRIPS

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory SAS_Plus_STRIPS
  imports "STRIPS_Semantics" "SAS_Plus_Semantics" 
    "Map_Supplement"
begin

section "SAS+/STRIPS Equivalence"

text ‹ The following part is concerned with showing the equivalent expressiveness of SAS+ and
STRIPS as discussed in \autoref{sub:equivalence-sas-plus-strips}. ›

subsection "Translation of SAS+ Problems to STRIPS Problems"

definition possible_assignments_for 
  :: "('variable, 'domain) sas_plus_problem ⇒ 'variable ⇒ ('variable × 'domain) list" 
  where "possible_assignments_for Ψ v ≡ [(v, a). a ← the (range_of Ψ v)]"

definition all_possible_assignments_for
  :: "('variable, 'domain) sas_plus_problem ⇒ ('variable × 'domain) list"
  where "all_possible_assignments_for Ψ 
    ≡ concat [possible_assignments_for Ψ v. v ← variables_of Ψ]" 

definition state_to_strips_state
  :: "('variable, 'domain) sas_plus_problem 
    ⇒ ('variable, 'domain) state 
    ⇒ ('variable, 'domain) assignment strips_state" 
  ("φ⇩S _ _" 99)
  where "state_to_strips_state Ψ s 
    ≡ let defined = filter (λv. s v ≠ None) (variables_of Ψ) in
      map_of (map (λ(v, a). ((v, a), the (s v) = a)) 
        (concat [possible_assignments_for Ψ v. v ← defined]))"

definition sasp_op_to_strips
  :: "('variable, 'domain) sas_plus_problem
    ⇒ ('variable, 'domain) sas_plus_operator
    ⇒ ('variable, 'domain) assignment strips_operator" 
  ("φ⇩O _ _" 99)
  where "sasp_op_to_strips Ψ op ≡ let
      pre = precondition_of op
      ; add = effect_of op
      ; delete = [(v, a'). (v, a) ← effect_of op, a' ← filter ((≠) a) (the (range_of Ψ v))]
    in STRIPS_Representation.operator_for pre add delete"

definition sas_plus_problem_to_strips_problem
  :: "('variable, 'domain) sas_plus_problem ⇒ ('variable, 'domain) assignment strips_problem" 
  ("φ _ " 99)
  where "sas_plus_problem_to_strips_problem Ψ ≡ let 
      vs = [as. v ← variables_of Ψ, as ← (possible_assignments_for Ψ) v]
      ; ops = map (sasp_op_to_strips Ψ) (operators_of Ψ)
      ; I = state_to_strips_state Ψ (initial_of Ψ)
      ; G = state_to_strips_state Ψ (goal_of Ψ)
    in STRIPS_Representation.problem_for vs ops I G"

definition sas_plus_parallel_plan_to_strips_parallel_plan
  :: "('variable, 'domain) sas_plus_problem
    ⇒ ('variable, 'domain) sas_plus_parallel_plan
    ⇒ ('variable × 'domain) strips_parallel_plan" 
  ("φ⇩P _ _" 99)
  where "sas_plus_parallel_plan_to_strips_parallel_plan Ψ ψ
    ≡ [[sasp_op_to_strips Ψ op. op ← ops]. ops ← ψ]"

(* TODO first argument should be ('variable, 'domain) strips_problem *)
definition strips_state_to_state
  :: "('variable, 'domain) sas_plus_problem
    ⇒ ('variable, 'domain) assignment strips_state
    ⇒ ('variable, 'domain) state" 
  ("φ⇩S¯ _ _" 99)
  where "strips_state_to_state Ψ s 
    ≡ map_of (filter (λ(v, a). s (v, a) = Some True) (all_possible_assignments_for Ψ))"

(* TODO remove problem argument *)
definition strips_op_to_sasp 
  :: "('variable, 'domain) sas_plus_problem 
    ⇒ ('variable × 'domain) strips_operator
    ⇒ ('variable, 'domain) sas_plus_operator"
  ("φ⇩O¯ _ _" 99)
  where "strips_op_to_sasp Ψ op 
    ≡ let 
        precondition = strips_operator.precondition_of op
        ; effect = strips_operator.add_effects_of op 
      in ⦇ precondition_of = precondition, effect_of = effect ⦈" 

(* TODO ‹strips_parallel_plan_to_sas_plus_parallel_plan ↝ φ_P¯› and 
‹strips_op_to_sasp ↝ φ_O¯› *)
definition strips_parallel_plan_to_sas_plus_parallel_plan
  :: "('variable, 'domain) sas_plus_problem
    ⇒ ('variable × 'domain) strips_parallel_plan
    ⇒ ('variable, 'domain) sas_plus_parallel_plan" 
  ("φ⇩P¯ _ _" 99)
  where "strips_parallel_plan_to_sas_plus_parallel_plan Π π
    ≡ [[strips_op_to_sasp Π op. op ← ops]. ops ← π]"

text ‹ To set up the equivalence proof context, we declare a common locale 
\isaname{sas_plus_strips_equivalence} for both the STRIPS and SAS+ formalisms and make it a 
sublocale of both locale \isaname{strips} as well as \isaname{sas_plus}.
The declaration itself is omitted for brevity since it basically just joins locales 
\isaname{sas_plus} and \isaname{strips} while renaming the locale parameter to avoid name clashes.
The sublocale proofs are shown below.
\footnote{We append a suffix identifying the respective formalism to the the parameter names 
passed to the parameter names in the locale. This is necessary to avoid ambiguous names in the 
sublocale declarations. For example, without addition of suffixes the type for ‹initial_of› is 
ambiguous and will therefore not be bound to either ‹strips_problem.initial_of› or 
‹sas_plus_problem.initial_of›. 
Isabelle in fact considers it to be a a free variable in this case. We also qualify the parent 
locales in the sublocale declarations by adding \texttt{strips:} and \texttt{sas\_plus:} before 
the respective parent locale identifiers. } ›

definition "range_of_strips Π x ≡ { True, False }"

context
begin

― ‹ Set-up simp rules. ›
lemma[simp]: 
  "(φ Ψ) = (let 
      vs = [as. v ← variables_of Ψ, as ← (possible_assignments_for Ψ) v]
      ; ops = map (sasp_op_to_strips Ψ) (operators_of Ψ)
      ; I = state_to_strips_state Ψ (initial_of Ψ)
      ; G = state_to_strips_state Ψ (goal_of Ψ)
    in STRIPS_Representation.problem_for vs ops I G)"
  and "(φ⇩S Ψ s)
    = (let defined = filter (λv. s v ≠ None) (variables_of Ψ) in
      map_of (map (λ(v, a). ((v, a), the (s v) = a)) 
        (concat [possible_assignments_for Ψ v. v ← defined])))"
  and "(φ⇩O Ψ op)
    = (let
      pre = precondition_of op
      ; add = effect_of op
      ; delete = [(v, a'). (v, a) ← effect_of op, a' ← filter ((≠) a) (the (range_of Ψ v))]
    in STRIPS_Representation.operator_for pre add delete)" 
  and "(φ⇩P Ψ ψ) = [[φ⇩O Ψ op. op ← ops]. ops ← ψ]"
  and "(φ⇩S¯ Ψ s')= map_of (filter (λ(v, a). s' (v, a) = Some True) 
    (all_possible_assignments_for Ψ))" 
  and "(φ⇩O¯ Ψ op') = (let 
        precondition = strips_operator.precondition_of op'
        ; effect = strips_operator.add_effects_of op' 
      in ⦇ precondition_of = precondition, effect_of = effect ⦈)" 
  and "(φ⇩P¯ Ψ π) = [[φ⇩O¯ Ψ op. op ← ops]. ops ← π]"
  unfolding
    SAS_Plus_STRIPS.sas_plus_problem_to_strips_problem_def
    sas_plus_problem_to_strips_problem_def
    SAS_Plus_STRIPS.state_to_strips_state_def
    state_to_strips_state_def
    SAS_Plus_STRIPS.sasp_op_to_strips_def
    sasp_op_to_strips_def
    SAS_Plus_STRIPS.sas_plus_parallel_plan_to_strips_parallel_plan_def
    sas_plus_parallel_plan_to_strips_parallel_plan_def
    SAS_Plus_STRIPS.strips_state_to_state_def
    strips_state_to_state_def 
    SAS_Plus_STRIPS.strips_op_to_sasp_def
    strips_op_to_sasp_def 
    SAS_Plus_STRIPS.strips_parallel_plan_to_sas_plus_parallel_plan_def
    strips_parallel_plan_to_sas_plus_parallel_plan_def 
  by blast+

lemmas [simp] = range_of'_def

lemma is_valid_problem_sas_plus_dom_sas_plus_problem_range_of:
  assumes "is_valid_problem_sas_plus Ψ" 
  shows "∀v ∈ set ((Ψ)⇩𝒱⇩+). v ∈ dom (sas_plus_problem.range_of Ψ)"
  using assms(1) is_valid_problem_sas_plus_then(1)
  unfolding is_valid_problem_sas_plus_def
  by (meson domIff list.pred_set)

lemma possible_assignments_for_set_is:
  assumes "v ∈ dom (sas_plus_problem.range_of Ψ)"
  shows "set (possible_assignments_for Ψ v) 
    = { (v, a) | a. a ∈ ℛ⇩+ Ψ v }" 
proof -
  have "sas_plus_problem.range_of Ψ v ≠ None"
    using assms(1) 
    by auto
  thus  ?thesis 
    unfolding possible_assignments_for_def
    by fastforce
qed

lemma all_possible_assignments_for_set_is:
  assumes "∀v ∈ set ((Ψ)⇩𝒱⇩+). range_of Ψ v ≠ None" 
  shows "set (all_possible_assignments_for Ψ)
    = (⋃v ∈ set ((Ψ)⇩𝒱⇩+). { (v, a) | a. a ∈ ℛ⇩+ Ψ v })" 
proof -
  let ?vs = "variables_of Ψ"
  have "set (all_possible_assignments_for Ψ) = 
    (⋃(set ` (λv. map (λ(v, a). (v, a)) (possible_assignments_for Ψ v)) ` set ?vs))"
    unfolding all_possible_assignments_for_def set_concat
    using set_map 
    by auto
  also have "… = (⋃((λv. set (possible_assignments_for Ψ v)) ` set ?vs))"
    using image_comp set_map
    by simp
  (* TODO slow *)
  also have "… = (⋃((λv. { (v, a) | a. a ∈ ℛ⇩+ Ψ v }) ` set ?vs))"
    using possible_assignments_for_set_is assms 
    by fastforce
  finally show ?thesis
    by force
qed

lemma state_to_strips_state_dom_is_i[simp]:
  assumes "∀v ∈ set ((Ψ)⇩𝒱⇩+). v ∈ dom (sas_plus_problem.range_of Ψ)"
  shows "set (concat 
      [possible_assignments_for Ψ v. v ← filter (λv. s v ≠ None) (variables_of Ψ)])
    = (⋃v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None }. 
      { (v, a) | a. a ∈ ℛ⇩+ Ψ v })" 
proof -
  let ?vs = "variables_of Ψ"
  let ?defined = "filter (λv. s v ≠ None) ?vs"
  let ?l = "concat [possible_assignments_for Ψ v. v ← ?defined]"
  have nb: "set ?defined = { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None }" 
    unfolding set_filter
    by force
  have "set ?l = ⋃(set ` set (map (possible_assignments_for Ψ) ?defined ))" 
    unfolding set_concat image_Union
    by blast
  also have "… = ⋃(set ` (possible_assignments_for Ψ) ` set ?defined)" 
    unfolding set_map
    by blast
  also have "… = (⋃v ∈ set ?defined. set (possible_assignments_for Ψ v))"
    by blast
  also have "… = (⋃v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None }.
    set (possible_assignments_for Ψ v))"
    using nb 
    by argo
  finally show ?thesis
    using possible_assignments_for_set_is 
      is_valid_problem_sas_plus_dom_sas_plus_problem_range_of assms(1)
    by fastforce
qed

lemma state_to_strips_state_dom_is:
  ― ‹ NOTE A transformed state is defined on all possible assignments for all variables defined 
in the original state. ›
  assumes "is_valid_problem_sas_plus Ψ"
  shows "dom (φ⇩S Ψ s) 
    = (⋃v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None }. 
      { (v, a) | a. a ∈ ℛ⇩+ Ψ v })"
proof -
  let ?vs = "variables_of Ψ"
  let ?l = "concat [possible_assignments_for Ψ v. v ← filter (λv. s v ≠ None) ?vs]"
  have nb: "∀v ∈ set ((Ψ)⇩𝒱⇩+). v ∈ dom (sas_plus_problem.range_of Ψ)"
    using is_valid_problem_sas_plus_dom_sas_plus_problem_range_of assms(1)
    by fastforce
  have "dom (φ⇩S Ψ s) = fst ` set (map (λ(v, a). ((v, a), the (s v) = a)) ?l)" 
    unfolding state_to_strips_state_def 
      SAS_Plus_STRIPS.state_to_strips_state_def 
    using dom_map_of_conv_image_fst[of "map (λ(v, a). ((v, a), the (s v) = a)) ?l"]
    by presburger
  also have "… = fst ` (λ(v, a). ((v, a), the (s v) = a)) ` set ?l" 
    unfolding set_map
    by blast
  also have "… = (λ(v, a). fst  ((v, a), the (s v) = a)) ` set ?l"
    unfolding image_comp[of fst "λ(v, a). ((v, a), the (s v) = a)"] comp_apply[of 
        fst "λ(v, a). ((v, a), the (s v) = a)"] prod.case_distrib
    by blast
  finally show ?thesis
    unfolding state_to_strips_state_dom_is_i[OF nb]
    by force
qed

corollary state_to_strips_state_dom_element_iff:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "(v, a) ∈ dom (φ⇩S Ψ s) ⟷ v ∈ set ((Ψ)⇩𝒱⇩+)
    ∧ s v ≠ None
    ∧ a ∈ ℛ⇩+ Ψ v"
proof -
  let ?vs = "variables_of Ψ"
    and ?s' = "φ⇩S Ψ s"
  show ?thesis 
    proof (rule iffI)
      assume "(v, a) ∈ dom (φ⇩S Ψ s)" 
      then have "v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None }"
          and "a ∈ ℛ⇩+ Ψ v"
        unfolding state_to_strips_state_dom_is[OF assms(1)]
        by force+
      moreover have "v ∈ set ?vs" and "s v ≠ None" 
        using calculation(1) 
        by fastforce+
      ultimately show 
        "v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None ∧ a ∈ ℛ⇩+ Ψ v"
        by force
    next 
      assume "v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None ∧ a ∈ ℛ⇩+ Ψ v"
      then have "v ∈ set ((Ψ)⇩𝒱⇩+)" 
        and "s v ≠ None"
        and a_in_range_of_v: "a ∈ ℛ⇩+ Ψ v" 
        by simp+
      then have "v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None }"
        by force
      thus "(v, a) ∈ dom (φ⇩S Ψ s)"
        unfolding state_to_strips_state_dom_is[OF assms(1)]
        using a_in_range_of_v
        by blast
    qed
qed

lemma state_to_strips_state_range_is:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "(v, a) ∈ dom (φ⇩S Ψ s)" 
  shows "(φ⇩S Ψ s) (v, a) = Some (the (s v) = a)"
proof -
  let ?vs = "variables_of Ψ" 
  let ?s' = "φ⇩S Ψ s"
    and ?defined = "filter (λv. s v ≠ None) ?vs"
  let ?l = "concat [possible_assignments_for Ψ v. v ← ?defined]"
  have v_in_set_vs: "v ∈ set ?vs" 
    and s_of_v_is_not_None: "s v ≠ None" 
    and a_in_range_of_v: "a ∈ ℛ⇩+ Ψ v" 
    using assms(2)
    unfolding state_to_strips_state_dom_is[OF assms(1)]
    by fastforce+
  moreover {
    have "∀v ∈ set ((Ψ)⇩𝒱⇩+). v ∈ dom (sas_plus_problem.range_of Ψ)"
      using assms(1) is_valid_problem_sas_plus_then(1)
      unfolding is_valid_problem_sas_plus_def
      by fastforce
    moreover have "(v, a) ∈ set ?l" 
      unfolding state_to_strips_state_dom_is_i[OF calculation(1)]
      using s_of_v_is_not_None a_in_range_of_v v_in_set_vs
      by fastforce
    moreover have "set ?l ≠ {}" 
      using calculation
      by fastforce
    ― ‹ TODO slow. ›
    ultimately have "(φ⇩S Ψ s) (v, a) = Some (the (s v) = a)"
      using map_of_from_function_graph_is_some_if[of 
          ?l "(v, a)" "λ(v, a). the (s v) = a"] 
      unfolding SAS_Plus_STRIPS.state_to_strips_state_def
        state_to_strips_state_def Let_def case_prod_beta'
      by fastforce
  }
  thus ?thesis.
qed


― ‹ Show that a STRIPS state corresponding to a SAS+ state via transformation is consistent
w.r.t. to the variable subset with same left component (i.e. the original SAS+ variable). This is
the consistency notion corresponding to SAS+ consistency: i.e. if no two assignments with different
values for the same variable exist in the SAS+ state, then assigning the corresponding assignment
both to @{text "True"} is impossible. Vice versa, if both are assigned to @{text "True"} then the
assignment variables must be the same SAS+ variable/SAS+ value pair. ›
lemma state_to_strips_state_effect_consistent:
  assumes "is_valid_problem_sas_plus Ψ"
    and "(v, a) ∈ dom (φ⇩S Ψ s)"
    and "(v, a') ∈ dom (φ⇩S Ψ s)"
    and "(φ⇩S Ψ s) (v, a) = Some True"
    and  "(φ⇩S Ψ s) (v, a') = Some True"
  shows "(v, a) = (v, a')" 
proof -
  have "the (s v) = a" and "the (s v) = a'"
    using state_to_strips_state_range_is[OF assms(1)] assms(2, 3, 4, 5)
    by fastforce+
  thus ?thesis 
    by argo
qed


lemma sasp_op_to_strips_set_delete_effects_is:
  assumes "is_valid_operator_sas_plus Ψ op" 
  shows "set (strips_operator.delete_effects_of (φ⇩O Ψ op)) 
    = (⋃(v, a) ∈ set (effect_of op). { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })"
proof -
  let ?D = "range_of Ψ"
    and ?effect = "effect_of op" 
  let ?delete = "[(v, a'). (v, a) ← ?effect, a' ← filter ((≠) a) (the (?D v))]"
  {
    fix v a
    assume "(v, a) ∈ set ?effect"
    then have "(ℛ⇩+ Ψ v) = set (the (?D v))"
      using assms 
      using is_valid_operator_sas_plus_then_range_of_sas_plus_op_is_set_range_of_op
      by fastforce
    hence "set (filter ((≠) a) (the (?D v))) = { a' ∈ ℛ⇩+ Ψ v. a' ≠ a }"
      unfolding set_filter 
      by blast
  } note nb = this
  {
    ― ‹ TODO slow. ›
    have "set ?delete = ⋃(set ` (λ(v, a). map (Pair v) (filter ((≠) a) (the (?D v)))) 
      ` (set ?effect))" 
      using set_concat
      by simp
    also have "… = ⋃((λ(v, a). Pair v ` set (filter ((≠) a) (the (?D v)))) 
      ` (set ?effect))"
      unfolding image_comp[of set] set_map 
      by auto
    ― ‹ TODO slow. ›
    also have "… = (⋃(v, a) ∈ set ?effect. Pair v ` { a' ∈ ℛ⇩+ Ψ v. a' ≠ a })" 
      using nb 
      by fast
    finally have "set ?delete = (⋃(v, a) ∈ set ?effect.
      { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })" 
      by blast
  }
  thus ?thesis
    unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def
      sasp_op_to_strips_def Let_def
    by force 
qed

lemma sas_plus_problem_to_strips_problem_variable_set_is:
  ― ‹ The variable set of ‹Π› is the set of all possible 
assignments that are possible using the variables of ‹𝒱› and the corresponding domains. ›
  assumes "is_valid_problem_sas_plus Ψ" 
  shows "set ((φ Ψ)⇩𝒱) = (⋃v ∈ set ((Ψ)⇩𝒱⇩+). { (v, a) | a. a ∈ ℛ⇩+ Ψ v })"
proof -
  let ?Π = "φ Ψ"
    and ?vs = "variables_of Ψ"
  {
    have "set (strips_problem.variables_of ?Π) 
      = set [as. v ← ?vs, as ← possible_assignments_for Ψ v]"
      unfolding sas_plus_problem_to_strips_problem_def 
        SAS_Plus_STRIPS.sas_plus_problem_to_strips_problem_def
      by force
    also have "… = (⋃(set ` (λv. possible_assignments_for Ψ v) ` set ?vs))" 
      using set_concat
      by auto
    also have "… = (⋃((set ∘ possible_assignments_for Ψ) ` set ?vs))" 
      using image_comp[of set "λv. possible_assignments_for Ψ v" "set ?vs"]
      by argo
    finally have "set (strips_problem.variables_of ?Π) 
      = (⋃v ∈ set ?vs. set (possible_assignments_for Ψ v))"
      unfolding o_apply
      by blast
  }
  moreover have "∀v ∈ set ?vs. v ∈ dom (sas_plus_problem.range_of Ψ)"
    using is_valid_problem_sas_plus_dom_sas_plus_problem_range_of assms
    by force
  ultimately show ?thesis
    using possible_assignments_for_set_is
    by force 
qed

corollary sas_plus_problem_to_strips_problem_variable_set_element_iff:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "(v, a) ∈ set ((φ Ψ)⇩𝒱)  ⟷ v ∈ set ((Ψ)⇩𝒱⇩+) ∧ a ∈ ℛ⇩+ Ψ v"
  unfolding sas_plus_problem_to_strips_problem_variable_set_is[OF assms]
  by fast

lemma sasp_op_to_strips_effect_consistent:
  assumes "op = φ⇩O Ψ op'" 
    and "op' ∈ set ((Ψ)⇩𝒪⇩+)"
    and "is_valid_operator_sas_plus Ψ op'"
  shows "(v, a) ∈ set (add_effects_of op) ⟶ (v, a) ∉ set (delete_effects_of op)"
    and "(v, a) ∈ set (delete_effects_of op) ⟶ (v, a) ∉ set (add_effects_of op)"
proof -
  have nb: "(∀(v, a) ∈ set (effect_of op'). ∀(v', a') ∈ set (effect_of op'). v ≠ v' ∨ a = a')" 
    using assms(3)
    unfolding is_valid_operator_sas_plus_def 
      SAS_Plus_Representation.is_valid_operator_sas_plus_def list_all_iff ListMem_iff Let_def
    by argo
  {
    fix v a
    assume v_a_in_add_effects_of_op: "(v, a) ∈ set (add_effects_of op)" 
    have "(v, a) ∉ set (delete_effects_of op)" 
      proof (rule ccontr)
        assume "¬(v, a) ∉ set (delete_effects_of op)" 
        moreover have "(v, a) ∈ 
          (⋃(v, a') ∈ set (effect_of op'). { (v, a'') 
            | a''. a'' ∈ (ℛ⇩+ Ψ v) ∧ a'' ≠ a' })"
          using calculation sasp_op_to_strips_set_delete_effects_is 
            assms 
          by blast
        moreover obtain a' where "(v, a') ∈ set (effect_of op')" and "a ≠ a'" 
          using calculation
          by blast
        moreover have "(v, a') ∈ set (add_effects_of op)" 
          using assms(1) calculation(3)
          unfolding sasp_op_to_strips_def
            SAS_Plus_STRIPS.sasp_op_to_strips_def
            Let_def
          by fastforce
        moreover have "(v, a) ∈ set (effect_of op')" and "(v, a') ∈ set (effect_of op')" 
          using assms(1) v_a_in_add_effects_of_op calculation(5)
          unfolding sasp_op_to_strips_def 
            SAS_Plus_STRIPS.sasp_op_to_strips_def
            Let_def 
          by force+
        ultimately show False 
          using nb 
          by fast
      qed
  }
  moreover {
    fix v a
    assume v_a_in_delete_effects_of_op: "(v, a) ∈ set (delete_effects_of op)" 
    have "(v, a) ∉ set (add_effects_of op)" 
      proof (rule ccontr)
        assume "¬(v, a) ∉ set (add_effects_of op)" 
        moreover have "(v, a) ∈ set (add_effects_of op)" 
          using calculation 
          by blast
        moreover have "(v, a) ∈ 
          (⋃(v, a') ∈ set (effect_of op'). { (v, a'') 
            | a''. a'' ∈ (ℛ⇩+ Ψ v) ∧ a'' ≠ a' })"
          using sasp_op_to_strips_set_delete_effects_is  
            nb assms(1, 3) v_a_in_delete_effects_of_op
          by force
        moreover obtain a' where "(v, a') ∈ set (effect_of op')" and "a ≠ a'" 
          using calculation
          by blast
        moreover have "(v, a') ∈ set (add_effects_of op)" 
          using assms(1) calculation(4)
          unfolding sasp_op_to_strips_def 
            SAS_Plus_STRIPS.sasp_op_to_strips_def
            Let_def
          by fastforce
        moreover have "(v, a) ∈ set (effect_of op')" and "(v, a') ∈ set (effect_of op')" 
          using assms(1) calculation(2, 6)
          unfolding sasp_op_to_strips_def 
            SAS_Plus_STRIPS.sasp_op_to_strips_def Let_def 
          by force+
        ultimately show False 
          using nb 
          by fast
      qed
    }
    ultimately show "(v, a) ∈ set (add_effects_of op) 
      ⟶ (v, a) ∉ set (delete_effects_of op)"
      and "(v, a) ∈ set (delete_effects_of op) 
      ⟶ (v, a) ∉ set (add_effects_of op)"
      by blast+
  qed

lemma is_valid_problem_sas_plus_then_strips_transformation_too_iii:
  assumes "is_valid_problem_sas_plus Ψ" 
  shows "list_all (is_valid_operator_strips (φ Ψ))
    (strips_problem.operators_of (φ Ψ))"
proof -
  let ?Π = "φ Ψ"
  let ?vs = "strips_problem.variables_of ?Π"
  {
    fix op
    assume "op ∈ set (strips_problem.operators_of ?Π)" 
    ― ‹ TODO slow. ›
    then obtain op' 
      where op_is: "op = φ⇩O Ψ op'" 
        and op'_in_operators: "op' ∈ set ((Ψ)⇩𝒪⇩+)" 
      unfolding SAS_Plus_STRIPS.sas_plus_problem_to_strips_problem_def
        sas_plus_problem_to_strips_problem_def 
        sasp_op_to_strips_def 
      by auto
    then have is_valid_op': "is_valid_operator_sas_plus Ψ op'"
      using sublocale_sas_plus_finite_domain_representation_ii(2)[OF assms]
      by blast
    moreover {
      fix v a
      assume "(v, a) ∈ set (strips_operator.precondition_of op)"
      ― ‹ TODO slow. ›
      then have "(v, a) ∈ set (sas_plus_operator.precondition_of op')" 
        using op_is
        unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def 
          sasp_op_to_strips_def
        by force
      moreover have "v ∈ set ((Ψ)⇩𝒱⇩+)" 
        using is_valid_op' calculation
        using is_valid_operator_sas_plus_then(1)
        by fastforce 
      moreover have  "a ∈ ℛ⇩+ Ψ v" 
        using is_valid_op' calculation(1)
        using is_valid_operator_sas_plus_then(2) 
        by fast
      ultimately have "(v, a) ∈ set ?vs" 
        using sas_plus_problem_to_strips_problem_variable_set_element_iff[OF assms(1)]
        by force
    }
    moreover {
      fix v a
      assume "(v, a) ∈ set (strips_operator.add_effects_of op)"
      then have "(v, a) ∈ set (effect_of op')" 
        using op_is
        unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def
          sasp_op_to_strips_def
        by force
      then have "v ∈ set ((Ψ)⇩𝒱⇩+)" and "a ∈ ℛ⇩+ Ψ v" 
        using is_valid_operator_sas_plus_then is_valid_op'
        by fastforce+
      hence "(v, a) ∈ set ?vs" 
        using sas_plus_problem_to_strips_problem_variable_set_element_iff[OF assms(1)]
        by force
    }
    moreover {
      fix v a'
      assume v_a'_in_delete_effects: "(v, a') ∈ set (strips_operator.delete_effects_of op)"
      moreover have "set (strips_operator.delete_effects_of op) 
        =  (⋃(v, a) ∈ set (effect_of op'). 
          { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })"
        using sasp_op_to_strips_set_delete_effects_is[OF is_valid_op']
          op_is
        by simp
      ― ‹ TODO slow. ›
      ultimately obtain a 
        where "(v, a) ∈ set (effect_of op')" 
          and a'_in: "a' ∈ { a' ∈ ℛ⇩+ Ψ v. a' ≠ a }"
        by blast 
      moreover have "is_valid_operator_sas_plus Ψ op'"
        using op'_in_operators assms(1) 
          is_valid_problem_sas_plus_then(2)
        by blast
      moreover have "v ∈ set ((Ψ)⇩𝒱⇩+)"
        using is_valid_operator_sas_plus_then calculation(1, 3)
        by fast
      moreover have "a' ∈ ℛ⇩+ Ψ v"
        using a'_in 
        by blast
      ultimately have "(v, a') ∈ set ?vs" 
        using sas_plus_problem_to_strips_problem_variable_set_element_iff[OF assms(1)]
        by force
    }
    ultimately have "set (strips_operator.precondition_of op) ⊆ set ?vs
      ∧ set (strips_operator.add_effects_of op) ⊆ set ?vs
      ∧ set (strips_operator.delete_effects_of op) ⊆ set ?vs
      ∧ (∀v∈set (add_effects_of op). v ∉ set (delete_effects_of op))
      ∧ (∀v∈set (delete_effects_of op). v ∉ set (add_effects_of op))"
      using sasp_op_to_strips_effect_consistent[OF 
          op_is op'_in_operators is_valid_op']
      by fast+
  }
  thus ?thesis
    unfolding is_valid_operator_strips_def STRIPS_Representation.is_valid_operator_strips_def 
      list_all_iff ListMem_iff Let_def 
    by blast
qed

lemma is_valid_problem_sas_plus_then_strips_transformation_too_iv:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "∀x. ((φ Ψ)⇩I) x ≠ None
    ⟷ ListMem x (strips_problem.variables_of (φ Ψ))"
proof -
  let ?vs = "variables_of Ψ"
    and ?I = "initial_of Ψ"
    and ?Π = "φ Ψ"
  let ?vs' = "strips_problem.variables_of ?Π"
    and ?I' = "strips_problem.initial_of ?Π"
  {
    fix x
    have "?I' x ≠ None ⟷ ListMem x ?vs'" 
      proof (rule iffI)
        assume I'_of_x_is_not_None: "?I' x ≠ None"
        then have "x ∈ dom ?I'" 
          by blast
        moreover obtain v a where x_is: "x = (v, a)" 
          by fastforce
        ultimately have "(v, a) ∈ dom ?I'" 
          by blast
        then have "v ∈ set ?vs" 
            and "?I v ≠ None"
            and "a ∈ ℛ⇩+ Ψ v"
          using state_to_strips_state_dom_element_iff[OF assms(1), of v a  ?I] 
          unfolding sas_plus_problem_to_strips_problem_def 
            SAS_Plus_STRIPS.sas_plus_problem_to_strips_problem_def 
            state_to_strips_state_def
            SAS_Plus_STRIPS.state_to_strips_state_def 
          by simp+
        thus "ListMem x ?vs'"
          unfolding ListMem_iff
          using sas_plus_problem_to_strips_problem_variable_set_element_iff[OF assms(1)] 
            x_is
          by auto
      next 
        assume list_mem_x_vs': "ListMem x ?vs'"
        then obtain v a where x_is: "x = (v, a)" 
          by fastforce
        then have "(v, a) ∈ set ?vs'" 
          using list_mem_x_vs'
          unfolding ListMem_iff
          by blast
        then have "v ∈ set ?vs" and "a ∈ ℛ⇩+ Ψ v" 
          using sas_plus_problem_to_strips_problem_variable_set_element_iff[OF assms(1)]
          by force+
        moreover have "?I v ≠ None" 
          using is_valid_problem_sas_plus_then(3) assms(1) calculation(1)
          by auto
        ultimately have "(v, a) ∈ dom ?I'" 
          using state_to_strips_state_dom_element_iff[OF assms(1), of v a ?I]
          unfolding SAS_Plus_STRIPS.sas_plus_problem_to_strips_problem_def 
            sas_plus_problem_to_strips_problem_def
            SAS_Plus_STRIPS.state_to_strips_state_def
            state_to_strips_state_def
          by force 
        thus "?I' x ≠ None"
          using x_is 
          by fastforce
      qed
  }
  thus ?thesis
    by simp
qed

private lemma is_valid_problem_sas_plus_then_strips_transformation_too_v:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "∀x. ((φ Ψ)⇩G) x ≠ None
    ⟶ ListMem x (strips_problem.variables_of (φ Ψ))"
proof -
  let ?vs = "variables_of Ψ"
    and ?D = "range_of Ψ"
    and ?G = "goal_of Ψ"
  let ?Π = "φ Ψ"
  let ?vs' = "strips_problem.variables_of ?Π"
    and ?G' = "strips_problem.goal_of ?Π" 
  have nb: "?G' = φ⇩S Ψ ?G" 
    by simp
  {
    fix x
    assume "?G' x ≠ None" 
    moreover obtain v a where "x = (v, a)" 
      by fastforce
    moreover have "(v, a) ∈ dom ?G'" 
      using domIff calculation(1, 2)
      by blast
    moreover have "v ∈ set ?vs" and "a ∈ ℛ⇩+ Ψ v"
      using state_to_strips_state_dom_is[OF assms(1), of ?G] nb calculation(3)
      by auto+
    ultimately have "x ∈ set ?vs'"
      using sas_plus_problem_to_strips_problem_variable_set_element_iff[OF assms(1)]
      by auto
  }
  thus ?thesis 
    unfolding ListMem_iff
    by simp
qed

text ‹ We now show that given \<^term>‹Ψ› is a valid SASPlus problem, then \<^term>‹Π ≡ φ Ψ› is a valid
STRIPS problem as well. 
The proof unfolds the definition of \<^term>‹is_valid_problem_strips› and then shows each of the conjuncts 
for \<^term>‹Π›. These are:
\begin{itemize}
  \item \<^term>‹Π› has at least one variable;
  \item \<^term>‹Π› has at least one operator;
  \item all operators are valid STRIPS operators;
  \item \<^term>‹(Π::'a strips_problem)⇩I› is defined for all variables in \<^term>‹(Π::'a strips_problem)⇩𝒱›; and finally,
  \item if \<^term>‹((Π::'a strips_problem)⇩G) x› is defined, then \<^term>‹x› is in \<^term>‹(Π::'a strips_problem)⇩𝒱›.
\end{itemize} ›

theorem
  is_valid_problem_sas_plus_then_strips_transformation_too:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "is_valid_problem_strips (φ Ψ)" 
proof -
  let ?Π = "φ Ψ"
  have "list_all (is_valid_operator_strips (φ Ψ))
   (strips_problem.operators_of (φ Ψ))" 
    using is_valid_problem_sas_plus_then_strips_transformation_too_iii[OF assms].
  moreover have "∀x. (((φ Ψ)⇩I) x ≠ None) =
    ListMem x (strips_problem.variables_of (φ Ψ))" 
    using is_valid_problem_sas_plus_then_strips_transformation_too_iv[OF assms].
  moreover have "∀x. ((φ Ψ)⇩G) x ≠ None ⟶
    ListMem x (strips_problem.variables_of (φ Ψ))" 
    using is_valid_problem_sas_plus_then_strips_transformation_too_v[OF assms].
  ultimately show ?thesis 
    using is_valid_problem_strips_def 
    unfolding STRIPS_Representation.is_valid_problem_strips_def
    by fastforce
qed 

lemma set_filter_all_possible_assignments_true_is:
  assumes "is_valid_problem_sas_plus Ψ" 
  shows "set (filter (λ(v, a). s (v, a) = Some True) 
      (all_possible_assignments_for Ψ))
    =  (⋃v ∈ set ((Ψ)⇩𝒱⇩+). Pair v ` { a ∈ ℛ⇩+ Ψ v. s (v, a) = Some True })"
proof -
  let ?vs = "sas_plus_problem.variables_of Ψ"
    and ?P = "(λ(v, a). s (v, a) = Some True)"
  let ?l = "filter ?P (all_possible_assignments_for Ψ)"
  have "set ?l = set (concat (map (filter ?P) (map (possible_assignments_for Ψ) ?vs)))" 
    unfolding all_possible_assignments_for_def
      filter_concat[of ?P "map (possible_assignments_for Ψ) (sas_plus_problem.variables_of Ψ)"]
    by simp
  also have "… = set (concat (map (λv. filter ?P (possible_assignments_for Ψ v)) ?vs))" 
    unfolding map_map comp_apply 
    by blast
  also have "… = set (concat (map (λv. map (Pair v) 
    (filter (?P ∘ Pair v) (the (range_of Ψ v)))) ?vs))" 
    unfolding possible_assignments_for_def filter_map
    by blast
  also have "… = set (concat (map (λv. map (Pair v) (filter (λa. s (v, a) = Some True) 
    (the (range_of Ψ v)))) ?vs))" 
    unfolding comp_apply
    by fast
  also have "… = ⋃(set ` ((λv. map (Pair v) (filter (λa. s (v, a) = Some True) 
    (the (range_of Ψ v)))) ` set ?vs))"
    unfolding set_concat set_map..
  also have "… = (⋃v ∈ set ?vs. Pair v ` set (filter (λa. s (v, a) = Some True) 
    (the (range_of Ψ v))))" 
    unfolding image_comp[of set] comp_apply set_map..
  also have "… = (⋃v ∈ set ?vs. Pair v 
    ` { a ∈ set (the (range_of Ψ v)). s (v, a) = Some True })"
    unfolding set_filter..
  finally show ?thesis 
    using set_the_range_of_is_range_of_sas_plus_if[OF assms(1)]
    by auto
qed

lemma strips_state_to_state_dom_is: 
  assumes "is_valid_problem_sas_plus Ψ" 
  shows "dom (φ⇩S¯ Ψ s) 
    = (⋃v ∈ set ((Ψ)⇩𝒱⇩+). 
      { v | a. a ∈ (ℛ⇩+ Ψ v) ∧ s (v, a) = Some True })"
proof -
  let ?vs = "variables_of Ψ"
    and ?s' = "φ⇩S¯ Ψ s" 
    and ?P = "(λ(v, a). s (v, a) = Some True)"
  let ?l = "filter ?P (all_possible_assignments_for Ψ)"
  { 
    have "fst ` set ?l = fst ` (⋃v ∈ set ?vs. Pair v 
      ` { a ∈ ℛ⇩+ Ψ v. s (v, a) = Some True })"
      unfolding set_filter_all_possible_assignments_true_is[OF assms]
      by auto
    also have "… = (⋃v ∈ set ?vs. fst ` Pair v 
      ` { a ∈ ℛ⇩+ Ψ v. s (v, a) = Some True })" 
      by blast
    also have "… = (⋃v ∈ set ?vs. (λa. fst (Pair v a)) ` 
      { a ∈ ℛ⇩+ Ψ v. s (v, a) = Some True })" 
      unfolding image_comp[of fst] comp_apply
      by blast
    finally have "fst ` set ?l = (⋃v ∈ set ((Ψ)⇩𝒱⇩+). 
      { v | a. a ∈ (ℛ⇩+ Ψ v) ∧ s (v, a) = Some True })" 
      unfolding setcompr_eq_image fst_conv 
      by simp
  }
  thus ?thesis
    unfolding SAS_Plus_STRIPS.strips_state_to_state_def 
      strips_state_to_state_def dom_map_of_conv_image_fst
    by blast
qed

lemma strips_state_to_state_range_is: 
  assumes "is_valid_problem_sas_plus Ψ" 
    and "v ∈ set ((Ψ)⇩𝒱⇩+)"
    and "a ∈ ℛ⇩+ Ψ v" 
    and "(v, a) ∈ dom s'"
    and "∀(v, a) ∈ dom s'. ∀(v, a') ∈ dom s'. s' (v, a) = Some True ∧ s' (v, a') = Some True 
      ⟶ (v, a) = (v, a')" 
  shows "(φ⇩S¯ Ψ s') v = Some a ⟷ the (s' (v, a))" 
proof -
  let ?vs = "variables_of Ψ"
    and ?D = "range_of Ψ"
    and ?s = "φ⇩S¯ Ψ s'"
  let ?as = "all_possible_assignments_for Ψ"
  let ?l = "filter (λ(v, a). s' (v, a) = Some True) ?as"
  show ?thesis 
    proof (rule iffI)
      assume s_of_v_is_Some_a: "?s v = Some a" 
      {
        have "(v, a) ∈ set ?l" 
          using s_of_v_is_Some_a 
          unfolding SAS_Plus_STRIPS.strips_state_to_state_def 
            strips_state_to_state_def 
          using map_of_SomeD
          by fast
        hence "s' (v, a) = Some True"
          unfolding all_possible_assignments_for_set_is set_filter
          by blast
      }
      thus "the (s' (v, a))"
        by simp
    next 
      assume the_of_s'_of_v_a_is: "the (s' (v, a))"
      then have s'_of_v_a_is_Some_true: "s' (v, a) = Some True"
        using assms(4) domIff 
        by force
      ― ‹ TODO slow. ›
      moreover {
        fix v v' a a'
        assume "(v, a) ∈ set ?l" and "(v', a') ∈ set ?l"
        then have "v ≠ v' ∨ a = a'" 
        using assms(5)
        by fastforce
      }
      moreover {
        have "∀v ∈ set ((Ψ)⇩𝒱⇩+). sas_plus_problem.range_of Ψ v ≠ None"  
          using is_valid_problem_sas_plus_then(1) assms(1)
            range_of_not_empty 
          by force
        (* TODO slow. *)
        moreover have "set ?l = Set.filter (λ(v, a). s' (v, a) = Some True) 
          (⋃v ∈ set ((Ψ)⇩𝒱⇩+). { (v, a) | a.  a ∈ ℛ⇩+ Ψ v })"
          using all_possible_assignments_for_set_is calculation
          by force
        ultimately have "(v, a) ∈ set ?l" 
          using assms(2, 3) s'_of_v_a_is_Some_true
          by simp
      }
      ultimately show "?s v = Some a"  
        using map_of_constant_assignments_defined_if[of ?l v a]
        unfolding SAS_Plus_STRIPS.strips_state_to_state_def
          strips_state_to_state_def
        by blast
    qed
qed

― ‹ NOTE A technical lemma which characterizes the return values for possible assignments 
@{text "(v, a)"} when used as variables on a state @{text "s"} which was transformed from. › 
lemma strips_state_to_state_inverse_is_i:
assumes "is_valid_problem_sas_plus Ψ"
  and "v ∈ set ((Ψ)⇩𝒱⇩+)"
  and "s v ≠ None" 
  and "a ∈ ℛ⇩+ Ψ v" 
shows "(φ⇩S Ψ s) (v, a) = Some (the (s v) = a)"
proof -
   let ?vs = "sas_plus_problem.variables_of Ψ"
  let ?s' = "φ⇩S Ψ s"
    and ?f = "λ(v, a). the (s v) = a"
    and ?l = "concat (map (possible_assignments_for Ψ) (filter (λv. s v ≠ None) ?vs))"
  have "(v, a) ∈ dom ?s'" 
    using state_to_strips_state_dom_element_iff[
        OF assms(1)] assms(2, 3, 4)
    by presburger
  {
    have "v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None }"
      using assms(2, 3)
      by blast
    moreover have "∀v ∈ set ((Ψ)⇩𝒱⇩+). v ∈ dom (sas_plus_problem.range_of Ψ)"
      using is_valid_problem_sas_plus_dom_sas_plus_problem_range_of[OF assms(1)]. 
    moreover have "set ?l = (⋃v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None }. 
      { (v, a) |a. a ∈ ℛ⇩+ Ψ v })"
      unfolding state_to_strips_state_dom_is_i[OF calculation(2)]
      by blast
    ultimately have "(v, a) ∈ set ?l" 
      using assms(4)
      by blast
  }
  moreover have "set ?l ≠ {}" 
    using calculation
    by force
  ― ‹ TODO slow.›
  ultimately show ?thesis 
    unfolding SAS_Plus_STRIPS.state_to_strips_state_def
      state_to_strips_state_def 
    using map_of_from_function_graph_is_some_if[of ?l "(v, a)" ?f] 
    unfolding split_def
    by fastforce
qed

― ‹ NOTE Show that the transformed strips state is consistent for pairs of assignments 
@{text "(v, a)"} and @{text "(v, a')"} in the same variable domain. ›
(* TODO make private. *)
corollary strips_state_to_state_inverse_is_ii:
assumes "is_valid_problem_sas_plus Ψ"
  and "v ∈ set ((Ψ)⇩𝒱⇩+)"
  and "s v = Some a"  
  and "a ∈ ℛ⇩+ Ψ v" 
  and "a' ∈ ℛ⇩+ Ψ v" 
  and "a' ≠ a"
shows "(φ⇩S Ψ s) (v, a') = Some False"
proof -
  have "s v ≠ None" 
    using assms(3) 
    by simp
  moreover have "the (s v) ≠ a'" 
    using assms(3, 6) 
    by simp 
  ultimately show ?thesis 
    using strips_state_to_state_inverse_is_i[OF assms(1, 2) _ assms(5)]
    by force
qed

― ‹ NOTE Follows from the corollary above by contraposition. ›
(* TODO make private. *)
corollary strips_state_to_state_inverse_is_iii:
assumes "is_valid_problem_sas_plus Ψ"
  and "v ∈ set ((Ψ)⇩𝒱⇩+)"
  and "s v = Some a" 
  and "a ∈ ℛ⇩+ Ψ v" 
  and "a' ∈ ℛ⇩+ Ψ v" 
  and "(φ⇩S Ψ s) (v, a) = Some True"
  and "(φ⇩S Ψ s) (v, a') = Some True"
shows "a = a'"
proof -
  have "s v ≠ None" 
    using assms(3)
    by blast
  thus ?thesis 
    using strips_state_to_state_inverse_is_i[OF assms(1, 2)] assms(4, 5, 6, 7)
    by auto
qed

(* TODO make private. *)
lemma strips_state_to_state_inverse_is_iv:
  assumes "is_valid_problem_sas_plus Ψ"
    and "dom s ⊆ set ((Ψ)⇩𝒱⇩+)"
    and "v ∈ set ((Ψ)⇩𝒱⇩+)" 
    and "s v = Some a" 
    and "a ∈ ℛ⇩+ Ψ v" 
  shows "(φ⇩S¯ Ψ (φ⇩S Ψ s)) v = Some a"
proof -
  let ?vs = "variables_of Ψ"
    and ?s' = "φ⇩S Ψ s"
  let ?s'' = "φ⇩S¯ Ψ ?s'" 
  let ?P = "λ(v, a). ?s' (v, a) = Some True"
  let ?as = "filter ?P (all_possible_assignments_for Ψ)" 
    and ?As = "Set.filter ?P (⋃v ∈ set ((Ψ)⇩𝒱⇩+). 
      { (v, a) | a. a ∈ ℛ⇩+ Ψ v })"
  {
    have "∀v ∈ set ((Ψ)⇩𝒱⇩+). range_of Ψ v ≠ None"
      using sublocale_sas_plus_finite_domain_representation_ii(1)[OF assms(1)] 
        range_of_not_empty
      by force
    (* TODO slow. *)
    hence "set ?as = ?As"
      unfolding set_filter 
      using all_possible_assignments_for_set_is
      by force
  } note nb = this
  moreover {
    {
      fix v v' a a' 
      assume "(v, a) ∈ set ?as" 
        and "(v', a') ∈ set ?as" 
      then have "(v, a) ∈ ?As" and "(v', a') ∈ ?As" 
        using nb 
        by blast+
      then have v_in_set_vs: "v ∈ set ?vs" and v'_in_set_vs: "v' ∈ set ?vs"
        and a_in_range_of_v: "a ∈ ℛ⇩+ Ψ v" 
        and a'_in_range_of_v: "a' ∈ ℛ⇩+ Ψ v'" 
        and s'_of_v_a_is: "?s' (v, a) = Some True" and s'_of_v'_a'_is: "?s' (v', a') = Some True" 
        by fastforce+
      then have "(v, a) ∈ dom ?s'"  
        by blast
      then have s_of_v_is_Some_a: "s v = Some a"  
        using state_to_strips_state_dom_element_iff[OF assms(1)]
          state_to_strips_state_range_is[OF assms(1)] s'_of_v_a_is 
           by auto
      have "v ≠ v' ∨ a = a'"
        proof (rule ccontr)
          assume "¬(v ≠ v' ∨ a = a')"
          then have "v = v'" and "a ≠ a'" 
            by simp+
          thus False
            using a'_in_range_of_v a_in_range_of_v assms(1) v'_in_set_vs s'_of_v'_a'_is 
              s'_of_v_a_is s_of_v_is_Some_a strips_state_to_state_inverse_is_iii
            by force
        qed
    }
    moreover {
      have "s v ≠ None" 
        using assms(4)
        by simp
      then have "?s' (v, a) = Some True" 
        using strips_state_to_state_inverse_is_i[OF assms(1, 3) _ assms(5)] 
          assms(4)
        by simp
      (* TODO slow *)
      hence "(v, a) ∈ set ?as" 
        using all_possible_assignments_for_set_is assms(3, 5) nb
        by simp
    }
    ultimately have "map_of ?as v = Some a" 
      using map_of_constant_assignments_defined_if[of ?as v a] 
      by blast
  }
  ― ‹ TODO slow. ›
  thus ?thesis
    unfolding SAS_Plus_STRIPS.strips_state_to_state_def
      strips_state_to_state_def all_possible_assignments_for_def
    by simp
qed

(* TODO the constraints on the state @{text "s"} could be refactored into a definition of valid 
states for a problem description. *)
(* TODO The proof is not very elegant. Should be simplified. *)
― ‹ Show that that ‹φ⇩S¯ Ψ› is the inverse of ‹φ⇩S Ψ›. The additional constraints 
\<^term>‹dom s = set ((Ψ)⇩𝒱⇩+)› and \<^term>‹∀v ∈ dom s. the (s v) ∈ ℛ⇩+ Ψ v› are needed because the 
transformation functions only take into account variables and domains declared in the problem 
description. They also sufficiently characterize a state that was transformed from SAS+ to STRIPS. ›
lemma strips_state_to_state_inverse_is:
  assumes "is_valid_problem_sas_plus Ψ"
    and "dom s ⊆ set ((Ψ)⇩𝒱⇩+)"
    and "∀v ∈ dom s. the (s v) ∈ ℛ⇩+ Ψ v" 
  shows "s = (φ⇩S¯ Ψ (φ⇩S Ψ s))"
proof -
  let ?vs = "variables_of Ψ"
    and ?D = "range_of Ψ"
  let ?s' = "φ⇩S Ψ s" 
  let ?s'' = "φ⇩S¯ Ψ ?s'"
  ― ‹ NOTE Show the thesis by proving that @{text "s"} and @{text "?s'"} are mutual submaps. ›
  {
    fix v
    assume v_in_dom_s: "v ∈ dom s"
    then have v_in_set_vs: "v ∈ set ?vs" 
      using assms(2) 
      by auto
    then obtain a 
      where the_s_v_is_a: "s v = Some a" 
        and a_in_dom_v: "a ∈ ℛ⇩+ Ψ v" 
      using assms(2, 3) v_in_dom_s
      by force
    moreover have "?s'' v = Some a" 
      using strips_state_to_state_inverse_is_iv[OF assms(1, 2)] v_in_set_vs
        the_s_v_is_a a_in_dom_v 
      by force
    ultimately have "s v = ?s'' v"
      by argo
  } note nb = this
  moreover {
    fix v
    assume "v ∈ dom ?s''"
    then obtain a 
      where "a ∈ ℛ⇩+ Ψ v" 
        and "?s' (v, a) = Some True" 
      using strips_state_to_state_dom_is[OF assms(1)]
      by blast
    then have "(v, a) ∈ dom ?s'" 
      by blast
    then have "s v ≠ None" 
      using state_to_strips_state_dom_is[OF assms(1)]
      by simp
    then obtain a where "s v = Some a" 
      by blast
    hence "?s'' v = s v"
      using nb 
      by fastforce
  }
  ― ‹ TODO slow.›
  ultimately show ?thesis 
    using map_le_antisym[of s ?s''] map_le_def
    unfolding strips_state_to_state_def 
      state_to_strips_state_def
    by blast
qed

― ‹ An important lemma which shows that the submap relation does not change if we transform the 
states on either side from SAS+ to STRIPS. 
% TODO what is this called generally? Predicate monotony?? ›
lemma state_to_strips_state_map_le_iff:
  assumes "is_valid_problem_sas_plus Ψ"
    and "dom s ⊆ set ((Ψ)⇩𝒱⇩+)" 
    and "∀v ∈ dom s. the (s v) ∈ ℛ⇩+ Ψ v" 
  shows "s ⊆⇩m t ⟷ (φ⇩S Ψ s) ⊆⇩m (φ⇩S Ψ t)"
proof -
  let ?vs = "variables_of Ψ"
    and ?D = "range_of Ψ"
    and ?s' = "φ⇩S Ψ s" 
    and ?t' = "φ⇩S Ψ t" 
  show ?thesis
    proof (rule iffI)
      assume s_map_le_t: "s ⊆⇩m t"
      {
        fix v a
        assume "(v, a) ∈ dom ?s'" 
        moreover have "v ∈ set ((Ψ)⇩𝒱⇩+)" and "s v ≠ None" and "a ∈ ℛ⇩+ Ψ v"
          using state_to_strips_state_dom_is[OF assms(1)] calculation 
          by blast+
        moreover have "?s' (v, a) = Some (the (s v) = a)"
          using state_to_strips_state_range_is[OF assms(1)] calculation(1) 
          by meson
        moreover have "v ∈ dom s" 
          using calculation(3)
          by auto 
        moreover have "s v = t v" 
          using s_map_le_t calculation(6) 
          unfolding map_le_def
          by blast
        moreover have "t v ≠ None" 
          using calculation(3, 7)
          by argo
        moreover have "(v, a) ∈ dom ?t'" 
          using state_to_strips_state_dom_is[OF assms(1)] calculation(2, 4, 8) 
          by blast
        moreover have "?t' (v, a) = Some (the (t v) = a)" 
          using state_to_strips_state_range_is[OF assms(1)] calculation(9)
          by simp
        ultimately have "?s' (v, a) = ?t' (v, a)"
          by presburger
      }
      thus "?s' ⊆⇩m ?t'" 
        unfolding map_le_def 
        by fast
    next
      assume s'_map_le_t': "?s' ⊆⇩m ?t'"
      {
        fix v 
        assume v_in_dom_s: "v ∈ dom s" 
        moreover obtain a where the_of_s_of_v_is_a: "the (s v) = a" 
          by blast
        moreover have v_in_vs: "v ∈ set ((Ψ)⇩𝒱⇩+)" 
          and s_of_v_is_not_None: "s v ≠ None" 
          and a_in_range_of_v: "a ∈ ℛ⇩+ Ψ v"
          using assms(2, 3) v_in_dom_s calculation
          by blast+
        moreover have "(v, a) ∈ dom ?s'"  
          using state_to_strips_state_dom_is[OF assms(1)] 
            calculation(3, 4, 5)
          by simp
        moreover have "?s' (v, a) = ?t' (v, a)"
          using s'_map_le_t' calculation
          unfolding map_le_def 
          by blast
        moreover have "(v, a) ∈ dom ?t'" 
          using calculation 
          unfolding domIff
          by argo
        moreover have "?s' (v, a) = Some (the (s v) = a)"
          and "?t' (v, a) = Some (the (t v) = a)" 
          using state_to_strips_state_range_is[OF assms(1)] calculation
          by fast+
        moreover have "s v = Some a" 
          using calculation(2, 4) 
          by force
        moreover have "?s' (v, a) = Some True" 
          using calculation(9, 11)
          by fastforce
        moreover have "?t' (v, a) = Some True" 
          using calculation(7, 12)
          by argo
        moreover have "the (t v) = a" 
          using calculation(10, 13) try0
          by force
        moreover {
          have "v ∈ dom t" 
            using state_to_strips_state_dom_element_iff[OF assms(1)] 
              calculation(8) 
            by auto
          hence "t v = Some a"
            using calculation(14)
            by force
        }
        ultimately have "s v = t v"
          by argo
      }
      thus "s ⊆⇩m t"
        unfolding map_le_def
        by simp
    qed
qed

― ‹ We also show that ‹φ⇩O¯ Π› is the inverse of ‹φ⇩O Ψ›. Note that this proof is completely 
mechanical since both the precondition and effect lists are simply being copied when transforming 
from SAS+ to STRIPS and when transforming back from STRIPS to SAS+. ›
(* TODO rename ‹sasp_op_to_strips_inverse_is› *)
(* TODO prune assumptions (not required) *)
lemma sas_plus_operator_inverse_is:
  assumes "is_valid_problem_sas_plus Ψ"
    and "op ∈ set ((Ψ)⇩𝒪⇩+)" 
  shows "(φ⇩O¯ Ψ (φ⇩O Ψ op)) = op"
proof -
  let ?op = "φ⇩O¯ Ψ (φ⇩O Ψ op)"
  have "precondition_of ?op = precondition_of op"
    unfolding SAS_Plus_STRIPS.strips_op_to_sasp_def
      strips_op_to_sasp_def
      SAS_Plus_STRIPS.sasp_op_to_strips_def
      sasp_op_to_strips_def
    by fastforce
  moreover have "effect_of ?op = effect_of op" 
    unfolding SAS_Plus_STRIPS.strips_op_to_sasp_def
      strips_op_to_sasp_def
      SAS_Plus_STRIPS.sasp_op_to_strips_def
      sasp_op_to_strips_def
    by force
  ultimately show ?thesis 
    by simp
qed

― ‹ Note that we have to make the assumption that ‹op'› is a member of the operator set of the 
induced STRIPS problem ‹φ Ψ›. This implies that ‹op'› was transformed from an 
‹op ∈ operators_of Ψ›. If we don't make this assumption, then multiple STRIPS operators of the 
form  ‹⦇ precondition_of = [], add_effects_of = [], delete_effects_of = [(v, a), ...] ⦈› correspond 
to one SAS+ operator (since the delete effects are being discarded in the transformation function). 
›
lemma strips_operator_inverse_is:
  assumes "is_valid_problem_sas_plus Ψ"
    and "op' ∈ set ((φ Ψ)⇩𝒪)" 
  shows "(φ⇩O Ψ (φ⇩O¯ Ψ op')) = op'" 
  proof -
    let ?Π = "φ Ψ"
    obtain op where "op ∈ set ((Ψ)⇩𝒪⇩+)" and "op' = φ⇩O Ψ op" 
      using assms 
      by auto
    moreover have "φ⇩O¯ Ψ op' = op" 
      using sas_plus_operator_inverse_is[OF assms(1) calculation(1)] calculation(2)
      by blast
    ultimately show ?thesis
      by argo
  qed

(* 
  ▪ TODO Simplify | refactor proof. 
  ▪ TODO make private. *)
lemma sas_plus_equivalent_to_strips_i_a_I:
  assumes "is_valid_problem_sas_plus Ψ"
    and "set ops' ⊆ set ((φ Ψ)⇩𝒪)"
    and "STRIPS_Semantics.are_all_operators_applicable (φ⇩S Ψ s) ops'"
    and "op ∈ set [φ⇩O¯ Ψ op'. op' ← ops']" 
  shows "map_of (precondition_of op) ⊆⇩m (φ⇩S¯ Ψ (φ⇩S Ψ s))" 
proof -
  let ?Π = "φ Ψ"
    and ?s' = "φ⇩S Ψ s" 
  let ?s = "φ⇩S¯ Ψ ?s'" 
    and ?D = "range_of Ψ"
    and ?ops = "[φ⇩O¯ Ψ op'. op' ← ops']" 
    and ?pre = "precondition_of op" 
  have nb⇩1: "∀(v, a) ∈ dom ?s'. 
    ∀(v, a') ∈ dom ?s'. 
      ?s' (v, a) = Some True ∧ ?s' (v, a') = Some True
      ⟶ (v, a) = (v, a')" 
    using state_to_strips_state_effect_consistent[OF assms(1)] 
    by blast
  {
    fix op'
    assume "op' ∈ set ops'" 
    moreover have "op' ∈ set ((?Π)⇩𝒪)"
      using assms(2) calculation 
      by blast
    ultimately have "∃op ∈ set ((Ψ)⇩𝒪⇩+). op' = (φ⇩O Ψ op)" 
      by auto
  } note nb⇩2 = this
  {
    fix op
    assume "op ∈ set ?ops" 
    then obtain op' where "op' ∈ set ops'" and "op = φ⇩O¯ Ψ op'" 
      using assms(4) 
      by auto
    moreover obtain op'' where "op'' ∈ set ((Ψ)⇩𝒪⇩+)" and "op' = φ⇩O Ψ op''" 
      using nb⇩2 calculation(1)
      by blast
    moreover have "op = op''"
      using sas_plus_operator_inverse_is[OF assms(1) calculation(3)] calculation(2, 4)  
      by blast
    ultimately have "op ∈ set ((Ψ)⇩𝒪⇩+)"
      by blast
  } note nb⇩3 = this
  {
    fix op v a
    assume "op ∈ set ?ops" 
      and v_a_in_precondition_of_op': "(v, a) ∈ set (precondition_of op)"
    moreover obtain op' where "op' ∈ set ops'" and "op = φ⇩O¯ Ψ op'" 
      using calculation(1) 
      by auto
    moreover have "strips_operator.precondition_of op' = precondition_of op" 
      using calculation(4) 
      unfolding SAS_Plus_STRIPS.strips_op_to_sasp_def
        strips_op_to_sasp_def
      by simp
    ultimately have "∃op' ∈ set ops'. op = (φ⇩O¯ Ψ op')
      ∧ (v, a) ∈ set (strips_operator.precondition_of op')" 
      by metis
  } note nb⇩4 = this
  {
    fix op' v a
    assume "op' ∈ set ops'" 
      and v_a_in_precondition_of_op': "(v, a) ∈ set (strips_operator.precondition_of op')"
    moreover have s'_of_v_a_is_Some_True: "?s' (v, a) = Some True" 
      using assms(3) calculation(1, 2) 
      unfolding are_all_operators_applicable_set
      by blast
    moreover {
      obtain op where "op ∈ set ((Ψ)⇩𝒪⇩+)" and "op' = φ⇩O Ψ op" 
        using nb⇩2 calculation(1) 
        by blast
      moreover have "strips_operator.precondition_of op' = precondition_of op" 
        using calculation(2) 
        unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def
          sasp_op_to_strips_def
        by simp
      moreover have "(v, a) ∈ set (precondition_of op)"
        using v_a_in_precondition_of_op' calculation(3)
        by argo
      moreover have "is_valid_operator_sas_plus Ψ op" 
        using is_valid_problem_sas_plus_then(2) assms(1) calculation(1)
        unfolding is_valid_operator_sas_plus_def
        by auto
      moreover have "v ∈ set ((Ψ)⇩𝒱⇩+)" and "a ∈ ℛ⇩+ Ψ v" 
        using is_valid_operator_sas_plus_then(1,2) calculation(4, 5)
        unfolding is_valid_operator_sas_plus_def
        by fastforce+
      moreover have "v ∈ dom ?s" 
        using strips_state_to_state_dom_is[OF assms(1), of ?s'] 
          s'_of_v_a_is_Some_True calculation(6, 7)
        by blast
      moreover have "(v, a) ∈ dom ?s'" 
        using s'_of_v_a_is_Some_True domIff 
        by blast
      ultimately have "?s v = Some a"
        using strips_state_to_state_range_is[OF assms(1) _ _ _ nb⇩1] 
          s'_of_v_a_is_Some_True 
        by simp
    }
    hence "?s v = Some a".
  } note nb⇩5 = this
  {
    fix v
    assume "v ∈ dom (map_of ?pre)"
    then obtain a where "map_of ?pre v = Some a"
      by fast
    moreover have "(v, a) ∈ set ?pre" 
      using map_of_SomeD calculation
      by fast
    moreover {
      have "op ∈ set ((Ψ)⇩𝒪⇩+)" 
        using assms(4) nb⇩3
        by blast
      then have "is_valid_operator_sas_plus Ψ op" 
        using is_valid_problem_sas_plus_then(2) assms(1)
        unfolding is_valid_operator_sas_plus_def
        by auto
      hence "∀(v, a) ∈ set ?pre. ∀(v', a') ∈ set ?pre. v ≠ v' ∨ a = a'"
        using is_valid_operator_sas_plus_then(5)
        unfolding is_valid_operator_sas_plus_def
        by fast
    }
    moreover have "map_of ?pre v = Some a"
      using map_of_constant_assignments_defined_if[of ?pre] calculation(2, 3)
      by blast
    moreover obtain op' where "op' ∈ set ops'" 
      and "(v, a) ∈ set (strips_operator.precondition_of op')" 
      using nb⇩4[OF assms(4) calculation(2)]
      by blast
    moreover have "?s v = Some a" 
      using nb⇩5 calculation(5, 6) 
      by fast
    ultimately have "map_of ?pre v = ?s v"
      by argo
  }
  thus ?thesis 
    unfolding map_le_def
    by blast
qed

lemma to_sas_plus_list_of_transformed_sas_plus_problem_operators_structure:
  assumes "is_valid_problem_sas_plus Ψ"
    and "set ops' ⊆ set ((φ Ψ)⇩𝒪)"
    and "op ∈ set [φ⇩O¯ Ψ op'. op' ← ops']" 
  shows "op ∈ set ((Ψ)⇩𝒪⇩+) ∧ (∃op' ∈ set ops'. op' = φ⇩O Ψ op)"
proof - 
  let ?Π = "φ Ψ"
  obtain op' where "op' ∈ set ops'" and "op = φ⇩O¯ Ψ op'" 
    using assms(3) 
    by auto
  moreover have "op' ∈ set ((?Π)⇩𝒪)"
    using assms(2) calculation(1) 
    by blast
  moreover obtain op'' where "op'' ∈ set ((Ψ)⇩𝒪⇩+)" and "op' = φ⇩O Ψ op''" 
    using calculation(3) 
    by auto
  moreover have "op = op''" 
    using sas_plus_operator_inverse_is[OF assms(1) calculation(4)] calculation(2, 5) 
    by presburger
  ultimately show ?thesis 
    by blast
qed

(* ▪ TODO Prune premises (2nd premise and ‹are_all_operators_applicable s' ops'› can be removed?). 
   ▪ TODO make private. 
   ▪ TODO adjust nb indexes *)
lemma sas_plus_equivalent_to_strips_i_a_II:
  fixes Ψ :: "('variable, 'domain) sas_plus_problem"
  fixes s :: "('variable, 'domain) state" 
  assumes "is_valid_problem_sas_plus Ψ"
    and "set ops' ⊆ set ((φ Ψ)⇩𝒪)"
    and "STRIPS_Semantics.are_all_operators_applicable (φ⇩s Ψ s) ops' 
      ∧ STRIPS_Semantics.are_all_operator_effects_consistent ops'"
  shows "are_all_operator_effects_consistent [φ⇩O¯ Ψ op'. op' ← ops']" 
proof -
  let ?s' = "φ⇩S Ψ s"
  let ?s = "φ⇩S¯ Ψ ?s'"
    and ?ops = "[φ⇩O¯ Ψ op'. op' ← ops']"
    and ?Π = "φ Ψ"
  have nb: "∀(v, a) ∈ dom ?s'. 
    ∀(v, a') ∈ dom ?s'. 
      ?s' (v, a) = Some True ∧ ?s' (v, a') = Some True
      ⟶ (v, a) = (v, a')" 
    using state_to_strips_state_effect_consistent[OF assms(1)] 
    by blast
  {
    fix op⇩1' op⇩2'
    assume "op⇩1' ∈ set ops'" and "op⇩2' ∈ set ops'"
    hence "STRIPS_Semantics.are_operator_effects_consistent op⇩1' op⇩2'" 
      using assms(3)
      unfolding STRIPS_Semantics.are_all_operator_effects_consistent_def list_all_iff
      by blast
  } note nb⇩1 = this
  {
    fix op⇩1 op⇩1' op⇩2 op⇩2'
    assume op⇩1_in_ops: "op⇩1 ∈ set ?ops"
      and op⇩1'_in_ops': "op⇩1' ∈ set ops'" 
      and op⇩1'_is: "op⇩1' = φ⇩O Ψ op⇩1" 
      and is_valid_op⇩1: "is_valid_operator_sas_plus Ψ op⇩1"
      and op⇩2_in_ops: "op⇩2 ∈ set ?ops"
      and op⇩2'_in_ops': "op⇩2' ∈ set ops'" 
      and op⇩2'_is: "op⇩2' = φ⇩O Ψ op⇩2"
      and is_valid_op⇩2: "is_valid_operator_sas_plus Ψ op⇩2"
    have "∀(v, a) ∈ set (add_effects_of op⇩1'). ∀(v', a') ∈ set (add_effects_of op⇩2').
          v ≠ v' ∨ a = a'" 
      proof (rule ccontr)
        assume "¬(∀(v, a) ∈ set (add_effects_of op⇩1'). ∀(v', a') ∈ set (add_effects_of op⇩2'). 
        v ≠ v' ∨ a = a')"
        then obtain v v' a a' where "(v, a) ∈ set (add_effects_of op⇩1')" 
          and "(v', a') ∈ set (add_effects_of op⇩2')" 
          and "v = v'" 
          and "a ≠ a'" 
          by blast
        ― ‹ TODO slow. ›
        moreover have "(v, a) ∈ set (effect_of op⇩1)"  
          using op⇩1'_is op⇩2'_is calculation(1, 2)
          unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def
            sasp_op_to_strips_def 
          by force
        moreover {
          have "(v', a') ∈ set (effect_of op⇩2)" 
            using op⇩2'_is calculation(2) 
            unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def
              sasp_op_to_strips_def
            by force
          hence "a' ∈ ℛ⇩+ Ψ v"
            using is_valid_operator_sas_plus_then is_valid_op⇩2 calculation(3)
            by fastforce
        }
        moreover have "(v, a') ∈ set (delete_effects_of op⇩1')" 
          using sasp_op_to_strips_set_delete_effects_is
            op⇩1'_is is_valid_op⇩1 calculation(3, 4, 5, 6)
          by blast
        moreover have "¬STRIPS_Semantics.are_operator_effects_consistent op⇩1' op⇩2'" 
          unfolding STRIPS_Semantics.are_operator_effects_consistent_def list_ex_iff 
          using calculation(2, 3, 7)
          by meson
        ultimately show False 
          using assms(3) op⇩1'_in_ops' op⇩2'_in_ops'
          unfolding STRIPS_Semantics.are_all_operator_effects_consistent_def list_all_iff
          by blast
      qed
  } note nb⇩3 = this
  {
    fix op⇩1 op⇩2
    assume op⇩1_in_ops: "op⇩1 ∈ set ?ops" and op⇩2_in_ops: "op⇩2 ∈ set ?ops" 
    moreover have op⇩1_in_operators_of_Ψ: "op⇩1 ∈ set ((Ψ)⇩𝒪⇩+)" 
      and op⇩2_in_operators_of_Ψ: "op⇩2 ∈ set ((Ψ)⇩𝒪⇩+)" 
      using to_sas_plus_list_of_transformed_sas_plus_problem_operators_structure[OF 
          assms(1, 2)] calculation
      by blast+
    moreover have is_valid_operator_op⇩1: "is_valid_operator_sas_plus Ψ op⇩1" 
      and is_valid_operator_op⇩2: "is_valid_operator_sas_plus Ψ op⇩2" 
      using is_valid_problem_sas_plus_then(2) op⇩1_in_operators_of_Ψ op⇩2_in_operators_of_Ψ
        assms(1)
      unfolding is_valid_operator_sas_plus_def
      by auto+
    moreover obtain op⇩1' op⇩2' 
      where op⇩1_in_ops': "op⇩1' ∈ set ops'" 
        and op⇩1_is: "op⇩1' = φ⇩O Ψ op⇩1"
        and op⇩2_in_ops': "op⇩2' ∈ set ops'"
        and op⇩2_is: "op⇩2' = φ⇩O Ψ op⇩2"
      using to_sas_plus_list_of_transformed_sas_plus_problem_operators_structure[OF 
          assms(1, 2)] op⇩1_in_ops op⇩2_in_ops
      by blast
    ― ‹ TODO slow.›
    ultimately have "∀(v, a) ∈ set (add_effects_of op⇩1'). ∀(v', a') ∈ set (add_effects_of op⇩2').
          v ≠ v' ∨ a = a'" 
      using nb⇩3 
      by auto
    hence "are_operator_effects_consistent op⇩1 op⇩2"
      using op⇩1_is op⇩2_is 
      unfolding are_operator_effects_consistent_def
        sasp_op_to_strips_def 
        SAS_Plus_STRIPS.sasp_op_to_strips_def
        list_all_iff Let_def
      by simp
  }
  thus ?thesis 
    unfolding are_all_operator_effects_consistent_def list_all_iff 
    by fast
qed

― ‹ A technical lemmas used in ‹sas_plus_equivalent_to_strips_i_a› showing that 
the execution precondition is linear w.r.t. to STRIPS transformation to SAS+. 

The second premise states that the given STRIPS state corresponds to a consistent SAS+ state (i.e.
no two assignments of the same variable to different values exist). ›
(* 
  ▪ TODO make private. 
  ▪ TODO decrement suffix *)
lemma sas_plus_equivalent_to_strips_i_a_IV: 
  assumes "is_valid_problem_sas_plus Ψ"
    and "set ops' ⊆ set ((φ Ψ)⇩𝒪)"
    and "STRIPS_Semantics.are_all_operators_applicable (φ⇩S Ψ s) ops' 
      ∧ STRIPS_Semantics.are_all_operator_effects_consistent ops'"
  shows "are_all_operators_applicable_in (φ⇩S¯ Ψ (φ⇩S Ψ s)) [φ⇩O¯ Ψ op'. op' ← ops'] ∧
    are_all_operator_effects_consistent [φ⇩O¯ Ψ op'. op' ← ops']" 
proof -
  let ?Π = "φ Ψ"
    and ?s' = "φ⇩S Ψ s"
  let ?vs' = "strips_problem.variables_of ?Π"
    and ?ops' = "strips_problem.operators_of ?Π" 
    and ?vs = "variables_of Ψ"
    and ?D = "range_of Ψ"
    and ?s = "φ⇩S¯ Ψ ?s'"
    and ?ops = "[φ⇩O¯ Ψ op'. op' ← ops']"
  have nb: "∀(v, a) ∈ dom ?s'. 
    ∀(v, a') ∈ dom (φ⇩S Ψ s). 
      ?s' (v, a) = Some True ∧ ?s' (v, a') = Some True
      ⟶ (v, a) = (v, a')" 
    using state_to_strips_state_effect_consistent[OF assms(1)] 
    by blast
  {
    have "STRIPS_Semantics.are_all_operators_applicable ?s' ops'" 
      using assms(3)
      by simp
    moreover have "list_all (λop. map_of (precondition_of op) ⊆⇩m ?s) ?ops"
      using sas_plus_equivalent_to_strips_i_a_I[OF assms(1) assms(2)] calculation
      unfolding list_all_iff
      by blast
    moreover have "list_all (λop. list_all (are_operator_effects_consistent op) ?ops) ?ops" 
      using sas_plus_equivalent_to_strips_i_a_II assms nb
      unfolding are_all_operator_effects_consistent_def is_valid_operator_sas_plus_def list_all_iff 
      by blast
    ultimately have "are_all_operators_applicable_in ?s ?ops" 
      unfolding are_all_operators_applicable_in_def is_operator_applicable_in_def list_all_iff
      by argo
  }
  moreover have "are_all_operator_effects_consistent ?ops" 
    using sas_plus_equivalent_to_strips_i_a_II assms nb
    by simp
  ultimately show ?thesis
    by simp
qed

(* TODO:
  ▪ prune premises + make private. 
  ▪ decrement suffixes 
*)
lemma sas_plus_equivalent_to_strips_i_a_VI:
  assumes "is_valid_problem_sas_plus Ψ"
    and "dom s ⊆ set ((Ψ)⇩𝒱⇩+)"
    and "∀v ∈ dom s. the (s v) ∈ ℛ⇩+ Ψ v" 
    and "set ops' ⊆ set ((φ Ψ)⇩𝒪)"
    and "are_all_operators_applicable_in s [φ⇩O¯ Ψ op'. op' ← ops'] ∧
      are_all_operator_effects_consistent [φ⇩O¯ Ψ op'. op' ← ops']"  
  shows "STRIPS_Semantics.are_all_operators_applicable (φ⇩S Ψ s) ops'"
proof -   
  let ?vs = "variables_of Ψ" 
    and ?D = "range_of Ψ"
    and ?Π = "φ Ψ" 
    and ?ops = "[φ⇩O¯ Ψ op'. op' ← ops']" 
    and ?s' = "φ⇩S Ψ s"
  ― ‹ TODO refactor. ›
  {
    fix op' 
    assume "op' ∈ set ops'" 
    moreover obtain op where "op ∈ set ?ops" and "op = φ⇩O¯ Ψ op'" 
      using calculation
      by force
    moreover obtain op'' where "op'' ∈ set ((Ψ)⇩𝒪⇩+)" and "op' = φ⇩O Ψ op''" 
      using assms(4) calculation(1) 
      by auto
    moreover have "is_valid_operator_sas_plus Ψ op''" 
      using is_valid_problem_sas_plus_then(2) assms(1) calculation(4)
      unfolding is_valid_operator_sas_plus_def
      by auto
    moreover have "op = op''" 
      using sas_plus_operator_inverse_is[OF assms(1)] calculation(3, 4, 5)
      by blast
    ultimately have "∃op ∈ set ?ops. op ∈ set ?ops ∧ op = (φ⇩O¯ Ψ op') 
      ∧ is_valid_operator_sas_plus Ψ op"
      by blast
  } note nb⇩1 = this
  have nb⇩2: "∀(v, a) ∈ dom ?s'. 
    ∀(v, a') ∈ dom ?s'. 
      ?s' (v, a) = Some True ∧ ?s' (v, a') = Some True
      ⟶ (v, a) = (v, a')" 
    using state_to_strips_state_effect_consistent[OF assms(1), of _ _ s]
    by blast
  {
    fix op
    assume "op ∈ set ?ops" 
    hence "map_of (precondition_of op) ⊆⇩m s" 
      using assms(5) 
      unfolding are_all_operators_applicable_in_def 
        is_operator_applicable_in_def list_all_iff
      by blast
  } note nb⇩3 = this
  {
    fix op'
    assume "op' ∈ set ops'" 
    then obtain op where op_in_ops: "op ∈ set ?ops" 
      and op_is: "op = (φ⇩O¯ Ψ op')" 
      and is_valid_operator_op: "is_valid_operator_sas_plus Ψ op" 
      using nb⇩1
      by force
    moreover have preconditions_are_consistent: 
      "∀(v, a) ∈ set (precondition_of op). ∀(v', a') ∈ set (precondition_of op). v ≠ v' ∨ a = a'" 
      using is_valid_operator_sas_plus_then(5) calculation(3) 
      unfolding is_valid_operator_sas_plus_def
      by fast
    moreover {
      fix v a
      assume "(v, a) ∈ set (strips_operator.precondition_of op')"
      moreover have v_a_in_precondition_of_op: "(v, a) ∈ set (precondition_of op)" 
        using op_is calculation 
        unfolding SAS_Plus_STRIPS.strips_op_to_sasp_def
          strips_op_to_sasp_def
        by auto
      moreover have "map_of (precondition_of op) v = Some a" 
        using map_of_constant_assignments_defined_if[OF 
            preconditions_are_consistent calculation(2)]
        by blast
      moreover have s_of_v_is: "s v = Some a" 
        using nb⇩3[OF op_in_ops] calculation(3) 
        unfolding map_le_def 
        by force
      moreover have "v ∈ set ((Ψ)⇩𝒱⇩+)" and "a ∈ ℛ⇩+ Ψ v" 
        using is_valid_operator_sas_plus_then(1, 2) is_valid_operator_op
          v_a_in_precondition_of_op 
        unfolding is_valid_operator_sas_plus_def 
          SAS_Plus_Representation.is_valid_operator_sas_plus_def Let_def list_all_iff ListMem_iff
        by auto+
      moreover have "(v, a) ∈ dom ?s'" 
        using state_to_strips_state_dom_is[OF assms(1)] s_of_v_is 
        calculation 
        by simp
      moreover have "(φ⇩S¯ Ψ ?s') v = Some a" 
        using strips_state_to_state_inverse_is[OF assms(1, 2, 3)] s_of_v_is
        by argo
      ― ‹ TODO slow. ›
      ultimately have "?s' (v, a) = Some True" 
        using strips_state_to_state_range_is[OF assms(1)] nb⇩2 
        by auto
    }
    ultimately have "∀(v, a) ∈ set (strips_operator.precondition_of op'). ?s' (v, a) = Some True" 
      by fast
  }
  thus ?thesis 
    unfolding are_all_operators_applicable_def is_operator_applicable_in_def 
      STRIPS_Representation.is_operator_applicable_in_def list_all_iff
    by simp
qed

(* TODO Prune premises. *)
lemma sas_plus_equivalent_to_strips_i_a_VII:
  assumes "is_valid_problem_sas_plus Ψ"
    and "dom s ⊆ set ((Ψ)⇩𝒱⇩+)" 
    and "∀v ∈ dom s. the (s v) ∈ ℛ⇩+ Ψ v" 
    and "set ops' ⊆ set ((φ Ψ)⇩𝒪)"
    and "are_all_operators_applicable_in s [φ⇩O¯ Ψ op'. op' ← ops'] ∧
    are_all_operator_effects_consistent [φ⇩O¯ Ψ op'. op' ← ops']"  
  shows "STRIPS_Semantics.are_all_operator_effects_consistent ops'"
proof - 
  let ?s' = "φ⇩S Ψ s" 
    and ?ops = "[φ⇩O¯ Ψ op'. op' ← ops']"
    and ?D = "range_of Ψ"
    and ?Π = "φ Ψ"
  ― ‹ TODO refactor. ›
  {
    fix op' 
    assume "op' ∈ set ops'" 
    moreover obtain op where "op ∈ set ?ops" and "op = φ⇩O¯ Ψ op'" 
      using calculation
      by force
    moreover obtain op'' where "op'' ∈ set ((Ψ)⇩𝒪⇩+)" and "op' = φ⇩O Ψ op''" 
      using assms(4) calculation(1) 
      by auto
    moreover have "is_valid_operator_sas_plus Ψ op''" 
      using is_valid_problem_sas_plus_then(2) assms(1) calculation(4)
      unfolding is_valid_operator_sas_plus_def
      by auto
    moreover have "op = op''" 
      using sas_plus_operator_inverse_is[OF assms(1)] calculation(3, 4, 5)
      by blast
    ultimately have "∃op ∈ set ?ops. op ∈ set ?ops ∧ op' = (φ⇩O Ψ op)
      ∧ is_valid_operator_sas_plus Ψ op"
      by blast
  } note nb⇩1 = this  
  {
    fix op⇩1' op⇩2'
    assume "op⇩1' ∈ set ops'" 
      and "op⇩2' ∈ set ops'" 
      and "∃(v, a) ∈ set (add_effects_of op⇩1'). ∃(v', a') ∈ set (delete_effects_of op⇩2').
        (v, a) = (v', a')" 
    moreover obtain op⇩1 op⇩2
      where "op⇩1 ∈ set ?ops" 
          and "op⇩1' = φ⇩O Ψ op⇩1" 
          and "is_valid_operator_sas_plus Ψ op⇩1"
        and "op⇩2 ∈ set ?ops" 
          and "op⇩2' = φ⇩O Ψ op⇩2" 
          and is_valid_op⇩2: "is_valid_operator_sas_plus Ψ op⇩2"
      using nb⇩1 calculation(1, 2)
      by meson
    moreover obtain v v' a a' 
      where "(v, a) ∈ set (add_effects_of op⇩1')" 
        and "(v', a') ∈ set (delete_effects_of op⇩2')"
        and "(v, a) = (v', a')" 
      using calculation
      by blast
    moreover have "(v, a) ∈ set (effect_of op⇩1)" 
      using calculation(5, 10) 
      unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def
        sasp_op_to_strips_def
      by fastforce
    moreover have "v = v'" and "a = a'"
      using calculation(12) 
      by simp+
    ― ‹ The next proof block shows that ‹(v', a')› is constructed from an effect ‹(v'', a'')›
      s.t. ‹a' ≠ a''›.  ›
    moreover {
      (* TODO slow. *)
      have "(v', a') ∈ (⋃(v'', a'') ∈ set (effect_of op⇩2). 
        { (v'', a''') | a'''. a''' ∈ (ℛ⇩+ Ψ v'') ∧  a''' ≠ a'' })"
        using sasp_op_to_strips_set_delete_effects_is 
          calculation(8, 11) is_valid_op⇩2 
        by blast
      then obtain v'' a'' where "(v'', a'') ∈ set (effect_of op⇩2)" 
        and "(v', a') ∈ { (v'', a''') | a'''. a''' ∈ (ℛ⇩+ Ψ v'') ∧  a''' ≠ a'' }"
        by blast
      moreover have "(v', a'') ∈ set (effect_of op⇩2)" 
        using calculation 
        by blast
      moreover have "a' ∈ ℛ⇩+ Ψ v''" and "a' ≠ a''"
        using calculation(1, 2) 
        by fast+
      ultimately have "∃a''. (v', a'') ∈ set (effect_of op⇩2) ∧ a' ∈ (ℛ⇩+ Ψ v') 
        ∧ a' ≠ a''" 
        by blast
    }
    moreover obtain a'' where "(v', a'') ∈ set (effect_of op⇩2)" 
      and "a' ∈ ℛ⇩+ Ψ v'"
      and "a' ≠ a''"
      using calculation(16) 
      by blast
    moreover have "∃(v, a) ∈ set (effect_of op⇩1). (∃(v', a') ∈ set (effect_of op⇩2). 
      v = v' ∧ a ≠ a')"
      using calculation(13, 14, 15, 17, 19)
      by blast
    moreover have "¬are_operator_effects_consistent op⇩1 op⇩2"
      unfolding are_operator_effects_consistent_def list_all_iff
      using calculation(20)
      by fastforce
    ultimately have "¬are_all_operator_effects_consistent ?ops" 
      unfolding are_all_operator_effects_consistent_def list_all_iff
      by meson
  } note nb⇩2 = this
  {
    fix op⇩1' op⇩2'
    assume op⇩1'_in_ops: "op⇩1' ∈ set ops'" and op⇩2'_in_ops: "op⇩2' ∈ set ops'" 
    have "STRIPS_Semantics.are_operator_effects_consistent op⇩1' op⇩2'"
      proof (rule ccontr)
        assume "¬STRIPS_Semantics.are_operator_effects_consistent op⇩1' op⇩2'"
        then consider (A) "∃(v, a) ∈ set (add_effects_of op⇩1'). 
          ∃(v', a') ∈ set (delete_effects_of op⇩2'). (v, a) = (v', a')"
          | (B) "∃(v, a) ∈ set (add_effects_of op⇩2'). 
          ∃(v', a') ∈ set (delete_effects_of op⇩1'). (v, a) = (v', a')"
          unfolding STRIPS_Semantics.are_operator_effects_consistent_def list_ex_iff
          by fastforce
        thus False 
          using nb⇩2[OF op⇩1'_in_ops op⇩2'_in_ops] nb⇩2[OF op⇩2'_in_ops op⇩1'_in_ops] assms(5)
          by (cases, argo, force)
      qed
  }
  thus ?thesis 
    unfolding STRIPS_Semantics.are_all_operator_effects_consistent_def 
      STRIPS_Semantics.are_operator_effects_consistent_def list_all_iff
    by blast
qed

lemma sas_plus_equivalent_to_strips_i_a_VIII:
  assumes "is_valid_problem_sas_plus Ψ"
    and "dom s ⊆ set ((Ψ)⇩𝒱⇩+)" 
    and "∀v ∈ dom s. the (s v) ∈ ℛ⇩+ Ψ v" 
    and "set ops' ⊆ set ((φ Ψ)⇩𝒪)"
    and "are_all_operators_applicable_in s [φ⇩O¯ Ψ op'. op' ← ops'] ∧
    are_all_operator_effects_consistent [φ⇩O¯ Ψ op'. op' ← ops']"  
  shows "STRIPS_Semantics.are_all_operators_applicable (φ⇩S Ψ s) ops' 
    ∧ STRIPS_Semantics.are_all_operator_effects_consistent ops'"
  using sas_plus_equivalent_to_strips_i_a_VI sas_plus_equivalent_to_strips_i_a_VII assms
  by fastforce

(* TODO refactor. *)
lemma sas_plus_equivalent_to_strips_i_a_IX:
  assumes "dom s ⊆ V"
    and "∀op ∈ set ops. ∀(v, a) ∈ set (effect_of op). v ∈ V" 
  shows "dom (execute_parallel_operator_sas_plus s ops) ⊆ V"  
proof -
  show ?thesis 
    using assms
    proof (induction ops arbitrary: s)
      case Nil 
      then show ?case
        unfolding execute_parallel_operator_sas_plus_def
        by simp 
    next
      case (Cons op ops)
      let ?s' = "s ++ map_of (effect_of op)" 
      ― ‹ TODO Wrap IH instantiation in block. ›
      {
        have "∀(v, a) ∈ set (effect_of op). v ∈ V" 
          using Cons.prems(2)
          by fastforce
        moreover have "fst ` set (effect_of op) ⊆ V" 
          using calculation
          by fastforce
        ultimately have "dom ?s' ⊆ V" 
          unfolding dom_map_add dom_map_of_conv_image_fst
          using Cons.prems(1)
          by blast
      }
      moreover have "∀op ∈ set ops. ∀(v, a) ∈ set (effect_of op). v ∈ V"
        using Cons.prems(2)
        by fastforce
      ultimately have "dom (execute_parallel_operator_sas_plus ?s' ops) ⊆ V"
        using Cons.IH[of ?s']
        by fast
      thus ?case 
        unfolding execute_parallel_operator_sas_plus_cons.
    qed
qed

― ‹ NOTE Show that the domain value constraint on states is monotonous w.r.t. to valid operator 
execution. I.e. if a parallel operator is executed on a state for which the domain value constraint 
holds, the domain value constraint will also hold on the resultant state. ›
(* TODO refactor. 
  TODO Rewrite lemma without domain function, i.e. ‹set (the (D v)) ↝ D› *)
lemma sas_plus_equivalent_to_strips_i_a_X:
  assumes "dom s ⊆ V"
    and "V ⊆ dom D"
    and "∀v ∈ dom s. the (s v) ∈ set (the (D v))" 
    and "∀op ∈ set ops. ∀(v, a) ∈ set (effect_of op). v ∈ V ∧ a ∈ set (the (D v))" 
  shows "∀v ∈ dom (execute_parallel_operator_sas_plus s ops). 
    the (execute_parallel_operator_sas_plus s ops v) ∈ set (the (D v))"  
proof -
  show ?thesis 
    using assms
    proof (induction ops arbitrary: s)
      case Nil 
      then show ?case
        unfolding execute_parallel_operator_sas_plus_def
        by simp 
    next
      case (Cons op ops)
      let ?s' = "s ++ map_of (effect_of op)" 
      {
        {
          have "∀(v, a) ∈ set (effect_of op). v ∈ V" 
            using Cons.prems(4)
            by fastforce
          moreover have "fst ` set (effect_of op) ⊆ V" 
            using calculation
            by fastforce
          ultimately have "dom ?s' ⊆ V" 
            unfolding dom_map_add dom_map_of_conv_image_fst
            using Cons.prems(1)
            by blast
        }
        moreover {
          fix v
          assume v_in_dom_s': "v ∈ dom ?s'"
          hence "the (?s' v) ∈ set (the (D v))" 
            proof (cases "v ∈ dom (map_of (effect_of op))")
              case True
              moreover have "?s' v = (map_of (effect_of op)) v"
                unfolding map_add_dom_app_simps(1)[OF True]
                by blast
              moreover obtain a where "(map_of (effect_of op)) v = Some a" 
                using calculation(1) 
                by fast
              moreover have "(v, a) ∈ set (effect_of op)" 
                using map_of_SomeD calculation(3)
                by fast
              moreover have "a ∈ set (the (D v))"
                using Cons.prems(4) calculation(4)
                by fastforce
              ultimately show ?thesis
                by force
            next
              case False
              then show ?thesis
                unfolding map_add_dom_app_simps(3)[OF False]
                using Cons.prems(3) v_in_dom_s'
                by fast
            qed
        }
        moreover have "∀op ∈ set ops. ∀(v, a) ∈ set (effect_of op). v ∈ V ∧ a ∈ set (the (D v))" 
          using Cons.prems(4)
          by auto
        ultimately have "∀v ∈ dom (execute_parallel_operator_sas_plus ?s' ops).
          the (execute_parallel_operator_sas_plus ?s' ops v) ∈ set (the (D v))" 
          using Cons.IH[of "s ++ map_of (effect_of op)", OF _ Cons.prems(2)]
          by meson
      }
      thus ?case 
        unfolding execute_parallel_operator_sas_plus_cons
        by blast
    qed
qed

lemma transfom_sas_plus_problem_to_strips_problem_operators_valid:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "op' ∈ set ((φ Ψ)⇩𝒪)"
  obtains op 
  where "op ∈ set ((Ψ)⇩𝒪⇩+)"
    and "op' = (φ⇩O Ψ op)" "is_valid_operator_sas_plus Ψ op" 
proof -
  {
    obtain op where "op ∈ set ((Ψ)⇩𝒪⇩+)" and "op' = φ⇩O Ψ op" 
      using assms 
      by auto
    moreover have "is_valid_operator_sas_plus Ψ op" 
      using is_valid_problem_sas_plus_then(2) assms(1) calculation(1)
      by auto
    ultimately have "∃op ∈ set ((Ψ)⇩𝒪⇩+). op' = (φ⇩O Ψ op)
      ∧ is_valid_operator_sas_plus Ψ op"
      by blast
  } 
  thus ?thesis 
    using that
    by blast
qed

lemma sas_plus_equivalent_to_strips_i_a_XI:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "op' ∈ set ((φ Ψ)⇩𝒪)" 
  shows "(φ⇩S Ψ s) ++ map_of (effect_to_assignments op') 
    = φ⇩S Ψ (s ++ map_of (effect_of (φ⇩O¯ Ψ op')))"
proof -
  let ?Π = "φ Ψ" 
  let ?vs = "variables_of Ψ"
    and?ops = "operators_of Ψ" 
    and ?ops' = "strips_problem.operators_of ?Π"
  let ?s' = "φ⇩S Ψ s"                 
  let ?t = "?s' ++ map_of (effect_to_assignments op')"
    and ?t' = "φ⇩S Ψ (s ++ map_of (effect_of (φ⇩O¯ Ψ op')))"
  obtain op where op'_is: "op' = (φ⇩O Ψ op)" 
    and op_in_ops: "op ∈ set ((Ψ)⇩𝒪⇩+)" 
    and is_valid_operator_op: "is_valid_operator_sas_plus Ψ op"
    using transfom_sas_plus_problem_to_strips_problem_operators_valid[OF assms]
    by auto
  have nb⇩1: "(φ⇩O¯ Ψ op') = op" 
    using sas_plus_operator_inverse_is[OF assms(1)] op'_is op_in_ops 
    by blast
  ― ‹ TODO refactor. ›
  {

    (*have "fst ` set (effect_to_assignments op') ≡
fst ` ((λv. (v, True)) ` set (add_effects_of op') ∪ (λv. (v, False)) ` set (delete_effects_of op'))"
      
      by auto
    then*) have "dom (map_of (effect_to_assignments op')) 
      = set (strips_operator.add_effects_of op') ∪ set (strips_operator.delete_effects_of op')"
      unfolding dom_map_of_conv_image_fst
      by force
    ― ‹ TODO slow.›
    also have "… = set (effect_of op) ∪ set (strips_operator.delete_effects_of op')" 
      using op'_is 
      unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def
        sasp_op_to_strips_def 
      by auto
    ― ‹ TODO slow.›
    finally have "dom (map_of (effect_to_assignments op')) = set (effect_of op)
      ∪ (⋃(v, a) ∈ set (effect_of op). { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })" 
      using sasp_op_to_strips_set_delete_effects_is[OF 
          is_valid_operator_op] op'_is
      by argo
  } note nb⇩2 = this
  have nb⇩3: "dom ?t = dom ?s' ∪ set (effect_of op)
    ∪ (⋃(v, a) ∈ set (effect_of op). { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })" 
    unfolding nb⇩2 dom_map_add
    by blast
  ― ‹ TODO refactor. ›
  have nb⇩4: "dom (s ++ map_of (effect_of (φ⇩O¯ Ψ op'))) 
    = dom s ∪ fst ` set (effect_of op)"
    unfolding dom_map_add dom_map_of_conv_image_fst nb⇩1
    by fast
  {
    let ?u = "s ++ map_of (effect_of (φ⇩O¯ Ψ op'))"
    have "dom ?t' = (⋃v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ ?u v ≠ None }. 
      { (v, a) | a. a ∈ ℛ⇩+ Ψ v })" 
      using state_to_strips_state_dom_is[OF assms(1)]
      by presburger
  } note nb⇩5 = this
  ― ‹ TODO refactor. ›
  have nb⇩6: "set (add_effects_of op') = set (effect_of op)"
    using op'_is 
    unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def
      sasp_op_to_strips_def
    by auto
  ― ‹ TODO refactor. ›
  have nb⇩7: "set (delete_effects_of op') = (⋃(v, a) ∈ set (effect_of op). 
      { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })" 
    using sasp_op_to_strips_set_delete_effects_is[OF 
        is_valid_operator_op] op'_is
    by argo
  ― ‹ TODO refactor. ›
  {
    let ?Add = "set (effect_of op)" 
    let ?Delete = "(⋃(v, a) ∈ set (effect_of op). 
      { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })" 
    have dom_add: "dom (map_of (map (λv. (v, True)) (add_effects_of op'))) = ?Add" 
      unfolding dom_map_of_conv_image_fst set_map image_comp comp_apply 
      using nb⇩6
      by simp
    have dom_delete: "dom (map_of (map (λv. (v, False)) (delete_effects_of op'))) = ?Delete"
      unfolding dom_map_of_conv_image_fst set_map image_comp comp_apply 
      using nb⇩7
      by auto
    {
      {
        fix v a 
        assume v_a_in_dom_add: "(v, a) ∈ dom (map_of (map (λv. (v, True)) (add_effects_of op')))"
        have "(v, a) ∉ dom (map_of (map (λv. (v, False)) (delete_effects_of op')))" 
          proof (rule ccontr) 
            assume "¬((v, a) ∉ dom (map_of (map (λv. (v, False)) (delete_effects_of op'))))"
            then have "(v, a) ∈ ?Delete" and "(v, a) ∈ ?Add"
              using dom_add dom_delete v_a_in_dom_add
              by argo+   
            moreover have "∀(v', a') ∈ ?Add. v ≠ v' ∨ a = a'"
              using is_valid_operator_sas_plus_then(6) is_valid_operator_op
                calculation(2)
              unfolding is_valid_operator_sas_plus_def
              by fast
            ultimately show False
              by fast
          qed
      }
      hence "disjnt (dom (map_of (map (λv. (v, True)) (add_effects_of op')))) 
        (dom (map_of (map (λv. (v, False)) (delete_effects_of op'))))"
        unfolding disjnt_def Int_def
        using nb⇩7
        by simp
    }
    hence "dom (map_of (map (λv. (v, True)) (add_effects_of op'))) = ?Add"
      and "dom (map_of (map (λv. (v, False)) (delete_effects_of op'))) = ?Delete"
      and "disjnt (dom (map_of (map (λv. (v, True)) (add_effects_of op')))) 
        (dom (map_of (map (λv. (v, False)) (delete_effects_of op'))))" 
      using dom_add dom_delete
      by blast+
  } note nb⇩8 = this
  ― ‹ TODO refactor. ›
  {
    let ?Add = "set (effect_of op)" 
    let ?Delete = "(⋃(v, a) ∈ set (effect_of op). 
      { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })" 
    ― ‹ TODO slow.›
    have "∀(v, a) ∈ ?Add. map_of (effect_to_assignments op') (v, a) = Some True" 
      and "∀(v, a) ∈ ?Delete. map_of (effect_to_assignments op') (v, a) = Some False"
      proof -
        {
          fix v a
          assume "(v, a) ∈ ?Add" 
          hence "map_of (effect_to_assignments op') (v, a) = Some True"
            unfolding effect_to_assignments_simp
            using  nb⇩6 map_of_defined_if_constructed_from_list_of_constant_assignments[of 
                "map (λv. (v, True)) (add_effects_of op')" True "add_effects_of op'"]
            by force
        }
        moreover {
          fix v a
          assume "(v, a) ∈ ?Delete"
          moreover have "(v, a) ∈ dom (map_of (map (λv. (v, False)) (delete_effects_of op')))"
            using nb⇩8(2) calculation(1)
            by argo
          moreover have "(v, a) ∉ dom (map_of (map (λv. (v, True)) (add_effects_of op')))" 
            using nb⇩8
            unfolding disjnt_def 
            using calculation(1)
            by blast
          moreover have "map_of (effect_to_assignments op') (v, a) 
            = map_of (map (λv. (v, False)) (delete_effects_of op')) (v, a)"
            unfolding effect_to_assignments_simp map_of_append 
            using map_add_dom_app_simps(3)[OF calculation(3)]
            by presburger 
          ― ‹ TODO slow. ›
          ultimately have "map_of (effect_to_assignments op') (v, a) = Some False"
            using map_of_defined_if_constructed_from_list_of_constant_assignments[
                of "map (λv. (v, False)) (delete_effects_of op')" False "delete_effects_of op'"]
               nb⇩7
            by auto
        }
        ultimately show "∀(v, a) ∈ ?Add. map_of (effect_to_assignments op') (v, a) = Some True" 
          and "∀(v, a) ∈ ?Delete. map_of (effect_to_assignments op') (v, a) = Some False" 
          by blast+
      qed
  } note nb⇩9 = this
  {
    fix v a
    assume "(v, a) ∈ set (effect_of op)"
    moreover have "∀(v, a) ∈ set (effect_of op). ∀(v', a') ∈ set (effect_of op). v ≠ v' ∨ a = a'"
      using is_valid_operator_sas_plus_then is_valid_operator_op
      unfolding is_valid_operator_sas_plus_def
      by fast
    ultimately have "map_of (effect_of op) v = Some a" 
      using map_of_constant_assignments_defined_if[of "effect_of op"]
      by presburger
  } note nb⇩1⇩0 = this
  {
    fix v a
    assume v_a_in_effect_of_op: "(v, a) ∈ set (effect_of op)"
      and "(s ++ map_of (effect_of (φ⇩O¯ Ψ op'))) v ≠ None"
    moreover have "v ∈ set ?vs"
        using is_valid_operator_op is_valid_operator_sas_plus_then(3) calculation(1)
        by fastforce 
    moreover {
      have "is_valid_problem_strips ?Π"
        using is_valid_problem_sas_plus_then_strips_transformation_too 
          assms(1) 
        by blast
      thm calculation(1) nb⇩6 assms(2)
      moreover have "set (add_effects_of op') ⊆ set ((?Π)⇩𝒱)" 
        using assms(2) is_valid_problem_strips_operator_variable_sets(2)
          calculation 
        by blast
      moreover have "(v, a) ∈ set ((?Π)⇩𝒱)"
        using v_a_in_effect_of_op nb⇩6 calculation(2) 
        by blast
      ultimately have "a ∈ ℛ⇩+ Ψ v"
        using sas_plus_problem_to_strips_problem_variable_set_element_iff[OF 
            assms(1)]
        by fast
    }
    ― ‹ TODO slow. ›
    ultimately have "(v, a) ∈ dom (φ⇩S Ψ (s ++ map_of (effect_of (φ⇩O¯ Ψ op'))))"  
      using state_to_strips_state_dom_is[OF assms(1), of 
          "s ++ map_of (effect_of (φ⇩O¯ Ψ op'))"]
      by simp
  } note nb⇩1⇩1 = this
  {
    fix v a
    assume "(v, a) ∈ set (effect_of op)"
    moreover have "v ∈ dom (map_of (effect_of op))" 
      unfolding dom_map_of_conv_image_fst 
      using calculation
      by force 
    moreover have "(s ++ map_of (effect_of (φ⇩O¯ Ψ op'))) v = Some a" 
      unfolding map_add_dom_app_simps(1)[OF calculation(2)] nb⇩1
      using nb⇩1⇩0 calculation(1)
      by blast
    moreover have "(s ++ map_of (effect_of (φ⇩O¯ Ψ op'))) v ≠ None" 
      using calculation(3)
      by auto
    moreover have "(v, a) ∈ dom (φ⇩S Ψ (s ++ map_of (effect_of (φ⇩O¯ Ψ op'))))"
      using nb⇩1⇩1 calculation(1, 4)
      by presburger
    ultimately have "(φ⇩S Ψ (s ++ map_of (effect_of (φ⇩O¯ Ψ op')))) (v, a) = Some True" 
      using state_to_strips_state_range_is[OF assms(1)]
      by simp
  } note nb⇩1⇩2 = this
  {
    fix v a'
    assume "(v, a') ∈ dom (map_of (effect_to_assignments op'))"   
      and "(v, a') ∈  (⋃(v, a) ∈ set (effect_of op).
        { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })"
    moreover have "v ∈ dom (map_of (effect_of op))" 
      unfolding dom_map_of_conv_image_fst 
      using calculation(2)
      by force
    moreover have "v ∈ set ?vs"
      using calculation(3) is_valid_operator_sas_plus_then(3) is_valid_operator_op
      unfolding dom_map_of_conv_image_fst is_valid_operator_sas_plus_def
      by fastforce
    moreover obtain a where "(v, a) ∈ set (effect_of op)" 
      and "a' ∈ ℛ⇩+ Ψ v" 
      and "a' ≠ a" 
      using calculation(2)
      by blast
    moreover have "(s ++ map_of (effect_of (φ⇩O¯ Ψ op'))) v = Some a" 
      unfolding map_add_dom_app_simps(1)[OF calculation(3)] nb⇩1
      using nb⇩1⇩0 calculation(5)
      by blast
    moreover have "(s ++ map_of (effect_of (φ⇩O¯ Ψ op'))) v ≠ None" 
      using calculation(8) 
      by auto
    ― ‹ TODO slow. ›
    moreover have "(v, a') ∈ dom (φ⇩S Ψ (s ++ map_of (effect_of (φ⇩O¯ Ψ op'))))"
      using state_to_strips_state_dom_is[OF assms(1), of 
        "s ++ map_of (effect_of (φ⇩O¯ Ψ op'))"] calculation(4, 6, 9)
      by simp
    ― ‹ TODO slow. ›
    ultimately have "(φ⇩S Ψ (s ++ map_of (effect_of (φ⇩O¯ Ψ op')))) (v, a') = Some False" 
      using state_to_strips_state_range_is[OF assms(1), 
          of v a' "s ++ map_of (effect_of (φ⇩O¯ Ψ op'))"]
      by simp
  } note nb⇩1⇩3 = this
  {
    fix v a
    assume "(v, a) ∈ dom ?t" 
      and "(v, a) ∉ dom (map_of (effect_to_assignments op'))"
    moreover have "(v, a) ∈ dom ?s'" 
      using calculation(1, 2)
      unfolding dom_map_add
      by blast
    moreover have "?t (v, a) = ?s' (v, a)" 
      unfolding map_add_dom_app_simps(3)[OF calculation(2)]..
    ultimately have "?t (v, a) = Some (the (s v) = a)"
      using state_to_strips_state_range_is[OF assms(1)] 
      by presburger
  } note nb⇩1⇩4 = this
  {
    fix v a
    assume "(v, a) ∈ dom ?t" 
      and v_a_not_in: "(v, a) ∉ dom (map_of (effect_to_assignments op'))"
    moreover have "(v, a) ∈ dom ?s'" 
      using calculation(1, 2)
      unfolding dom_map_add
      by blast
    moreover have "(v, a) ∈ (⋃ v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None }.
      { (v, a) | a. a ∈ ℛ⇩+ Ψ v })"
      using state_to_strips_state_dom_is[OF assms(1)] calculation(3)
      by presburger
    moreover have "v ∈ set ((Ψ)⇩𝒱⇩+)" and "s v ≠ None" and "a ∈ ℛ⇩+ Ψ v" 
      using calculation(4)
      by blast+
    ― ‹ NOTE Hasn't this been proved before? ›
    moreover {
      have "dom (map_of (effect_to_assignments op')) = (⋃(v, a) ∈ set (effect_of op). { (v, a) }) 
        ∪ (⋃(v, a) ∈ set (effect_of op). 
          { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })"
        unfolding nb⇩2
        by blast
      also have "… = (⋃(v, a) ∈ set (effect_of op). { (v, a) } 
          ∪ { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })" 
        by blast
      finally have "dom (map_of (effect_to_assignments op')) 
        = (⋃(v, a) ∈ set (effect_of op). { (v, a) } 
          ∪ { (v, a) | a. a ∈ ℛ⇩+ Ψ v })"
        by auto
      then have "(v, a) ∉ (⋃(v, a) ∈ set (effect_of op). 
        { (v, a) | a. a ∈ ℛ⇩+ Ψ v })" 
        using v_a_not_in
        by blast
    }
    ― ‹ TODO slow. ›
    moreover have "v ∉ dom (map_of (effect_of op))" 
      using dom_map_of_conv_image_fst calculation 
      by fastforce
    moreover have "(s ++ map_of (effect_of (φ⇩O¯ Ψ op'))) v = s v" 
      unfolding nb⇩1 map_add_dom_app_simps(3)[OF calculation(9)]
      by simp
    ― ‹ TODO slow. ›
    moreover have "(v, a) ∈ dom ?t'" 
      using state_to_strips_state_dom_is[OF assms(1), of 
        "s ++ map_of (effect_of (φ⇩O¯ Ψ op'))"] calculation(5, 6, 7, 8, 10)
      by simp
    ultimately have "?t' (v, a) = Some (the (s v) = a)" 
      using state_to_strips_state_range_is[OF assms(1)]
      by presburger
  } note nb⇩1⇩5 = this
  ― ‹ TODO refactor. ›
  have nb⇩1⇩6: "dom ?t = (⋃ v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None }. 
      { (v, a) | a. a ∈ (ℛ⇩+ Ψ v) }) 
    ∪ set (effect_of op) 
    ∪ (⋃(v, a)∈set (effect_of op).
      {(v, a') |a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a})"
    unfolding dom_map_add nb⇩2
    using state_to_strips_state_dom_is[OF assms(1), of s]
    by auto
  {
    {
      fix v a
      assume "(v, a) ∈ dom ?t"
      then consider (A) "(v, a) ∈ dom (φ⇩S Ψ s)" 
        | (B) "(v, a) ∈ dom (map_of (effect_to_assignments op'))" 
        by fast
      hence "(v, a) ∈ dom ?t'" 
        proof (cases)
          case A
          then have "v ∈ set ((Ψ)⇩𝒱⇩+)" and "s v ≠ None" and "a ∈ ℛ⇩+ Ψ v"
            unfolding state_to_strips_state_dom_element_iff[OF assms(1)]
            by blast+
          thm map_add_None state_to_strips_state_dom_element_iff[OF assms(1)]
          moreover have "(s ++ map_of (effect_of (φ⇩O¯ Ψ op'))) v ≠ None" 
            using calculation(2)
            by simp
          ultimately show ?thesis 
            unfolding state_to_strips_state_dom_element_iff[OF assms(1)]
            by blast
        next
          case B
          then have "(v, a) ∈ 
              set (effect_of op) 
              ∪ (⋃(v, a)∈set (effect_of op). { (v, a') | a'. a' ∈ ℛ⇩+ Ψ v ∧ a' ≠ a })" 
            unfolding nb⇩2
            by blast
          then consider (B⇩1) "(v, a) ∈ set (effect_of op)" 
            | (B⇩2) "(v, a) ∈ (⋃(v, a)∈set (effect_of op). 
            { (v, a') | a'. a' ∈ ℛ⇩+ Ψ v ∧ a' ≠ a })"
            by blast
          thm nb⇩1⇩2 nb⇩1⇩3 nb⇩2
          thus ?thesis
            proof (cases)
              case B⇩1
              then show ?thesis
                using nb⇩1⇩2
                by fast
            next
              case B⇩2
              then show ?thesis
                using nb⇩1⇩3 B
                by blast
            qed 
        qed 
    } 
    moreover {
      let ?u = "s ++ map_of (effect_of (φ⇩O¯ Ψ op'))"
      fix v a
      assume v_a_in_dom_t': "(v, a) ∈ dom ?t'"
      thm nb⇩5
      then have v_in_vs: "v ∈ set ((Ψ)⇩𝒱⇩+)" 
        and u_of_v_is_not_None: "?u v ≠ None" 
        and a_in_range_of_v: "a ∈ ℛ⇩+ Ψ v" 
        using state_to_strips_state_dom_element_iff[OF assms(1)]
          v_a_in_dom_t'
        by meson+
      {
        assume "(v, a) ∉ dom ?t" 
        then have contradiction: "(v, a) ∉ 
          (⋃v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None}. { (v, a) |a. a ∈ ℛ⇩+ Ψ v }) 
          ∪ set (effect_of op) 
          ∪ (⋃(v, a)∈set (effect_of op). {(v, a') |a'. a' ∈ ℛ⇩+ Ψ v ∧ a' ≠ a})" 
          unfolding nb⇩1⇩6
          by fast
        hence False 
          proof (cases "map_of (effect_of (φ⇩O¯ Ψ op')) v = None")
            case True
            then have "s v ≠ None" 
              using u_of_v_is_not_None
              by simp
            then have "(v, a) ∈ (⋃v ∈ { v | v. v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None}. 
              { (v, a) |a. a ∈ ℛ⇩+ Ψ v })" 
              using v_in_vs a_in_range_of_v 
              by blast
            thus ?thesis 
              using contradiction
              by blast
          next
            case False
            then have "v ∈ dom (map_of (effect_of op))" 
              using u_of_v_is_not_None nb⇩1 
              by blast
            then obtain a' where map_of_effect_of_op_v_is: "map_of (effect_of op) v = Some a'" 
              by blast
            then have v_a'_in: "(v, a') ∈ set (effect_of op)" 
              using map_of_SomeD 
              by fast
            then show ?thesis
              proof (cases "a = a'")
                case True
                then have "(v, a) ∈ set (effect_of op)" 
                  using v_a'_in
                  by blast
                then show ?thesis 
                  using contradiction
                  by blast
              next
                case False
                then have "(v, a) ∈ (⋃(v, a)∈set (effect_of op). 
                  {(v, a') |a'. a' ∈ ℛ⇩+ Ψ v ∧ a' ≠ a})" 
                  using v_a'_in calculation a_in_range_of_v
                  by blast
                thus ?thesis
                  using contradiction
                  by fast
              qed
          qed
      }
      hence "(v, a) ∈ dom ?t"
        by argo
    }
    moreover have "dom ?t ⊆ dom ?t'" and "dom ?t' ⊆ dom ?t" 
      subgoal 
        using calculation(1) subrelI[of "dom ?t" "dom ?t'"]
        by fast
      subgoal
        using calculation(2) subrelI[of "dom ?t'" "dom ?t"]
        by argo
      done
    ultimately have "dom ?t = dom ?t'"
      by force
  } note nb⇩1⇩7 = this
  {
    fix v a
    assume v_a_in_dom_t: "(v, a) ∈ dom ?t" 
    hence "?t (v, a) = ?t' (v, a)"
      proof (cases "(v, a) ∈ dom (map_of (effect_to_assignments op'))")
        case True
        ― ‹ TODO slow. ›
        ― ‹ NOTE Split on the (disjunct) domain variable sets of 
          @{text "map_of (effect_to_assignments op')"}. › 
        then consider (A1) "(v, a) ∈ set (effect_of op)" 
          | (A2) "(v, a) ∈ (⋃(v, a) ∈ set (effect_of op).
            { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧ a' ≠ a })"
          using nb⇩2
          by fastforce
        then show ?thesis 
          proof (cases)
            case A1
            then have "?t (v, a) = Some True" 
              unfolding map_add_dom_app_simps(1)[OF True]
              using nb⇩9(1)
              by fast
            moreover have "?t' (v, a) = Some True"
              using nb⇩1⇩2[OF A1].
            ultimately show ?thesis..
          next
            case A2
            then have "?t (v, a) = Some False" 
              unfolding map_add_dom_app_simps(1)[OF True]
              using nb⇩9(2)
              by blast
            moreover have "?t' (v, a) = Some False"
              using nb⇩1⇩3[OF True A2].
            ultimately show ?thesis..
          qed
      next
        case False
        moreover have "?t (v, a) = Some (the (s v) = a)" 
          using nb⇩1⇩4[OF v_a_in_dom_t False].
        moreover have "?t' (v, a) = Some (the (s v) = a)" 
          using nb⇩1⇩5[OF v_a_in_dom_t False].
        ultimately show ?thesis 
          by argo
      qed
  } note nb⇩1⇩8 = this
  moreover {
    fix v a
    assume "(v, a) ∈ dom ?t'" 
    hence "?t (v, a) = ?t' (v, a)" 
      using nb⇩1⇩7 nb⇩1⇩8
      by presburger
  }
  ― ‹ TODO slow.›
  ultimately have "?t ⊆⇩m ?t'" and "?t' ⊆⇩m ?t" 
    unfolding map_le_def 
    by fastforce+
  thus ?thesis
    using map_le_antisym[of ?t ?t'] 
    by fast
qed

― ‹ NOTE This is the essential step in the SAS+/STRIPS equivalence theorem. We show that executing
a given parallel STRIPS operator @{text "ops'"} on the corresponding STRIPS state 
@{text "s' = φ⇩S Ψ s"} yields the same state as executing the transformed SAS+ parallel operator
@{text "ops = [φ⇩O¯ (φ Ψ) op'. op' ← ops']"} on the original SAS+ state @{text "s"} and the 
transforming the resultant SAS+ state to its corresponding STRIPS state. ›
(* TODO refactor. *)
lemma sas_plus_equivalent_to_strips_i_a_XII:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "∀op' ∈ set ops'. op' ∈ set ((φ Ψ)⇩𝒪)" 
  shows "execute_parallel_operator (φ⇩S Ψ s) ops' 
    = φ⇩S Ψ (execute_parallel_operator_sas_plus s [φ⇩O¯ Ψ op'. op' ← ops'])" 
using assms
proof (induction ops' arbitrary: s)
  case Nil
  then show ?case 
    unfolding execute_parallel_operator_def execute_parallel_operator_sas_plus_def 
    by simp
next
  case (Cons op' ops')
  let ?Π = "φ Ψ"
  let ?t' = "(φ⇩S Ψ s) ++ map_of (effect_to_assignments op')"
    and ?t = "s ++ map_of (effect_of (φ⇩O¯ Ψ op'))"
  have nb⇩1: "?t' = φ⇩S Ψ ?t" 
    using sas_plus_equivalent_to_strips_i_a_XI[OF assms(1)] Cons.prems(2)
    by force
  {
    have "∀op' ∈ set ops'. op' ∈ set (strips_problem.operators_of ?Π)" 
      using Cons.prems(2) 
      by simp
    then have "execute_parallel_operator (φ⇩S Ψ ?t) ops' 
      = φ⇩S Ψ (execute_parallel_operator_sas_plus ?t [φ⇩O¯ Ψ x. x ← ops'])"
      using Cons.IH[OF Cons.prems(1), of ?t]
      by fastforce
    hence "execute_parallel_operator ?t' ops'
      = φ⇩S Ψ (execute_parallel_operator_sas_plus ?t [φ⇩O¯ Ψ x. x ← ops'])" 
      using nb⇩1
      by argo
  }
  thus ?case 
    by simp
qed

lemma sas_plus_equivalent_to_strips_i_a_XIII: 
  assumes "is_valid_problem_sas_plus Ψ"
    and "∀op' ∈ set ops'. op' ∈ set ((φ Ψ)⇩𝒪)"
    and "(φ⇩S Ψ G) ⊆⇩m execute_parallel_plan 
      (execute_parallel_operator (φ⇩S Ψ I) ops') π"
  shows "(φ⇩S Ψ G) ⊆⇩m execute_parallel_plan 
    (φ⇩S Ψ (execute_parallel_operator_sas_plus I [φ⇩O¯ Ψ op'. op' ← ops'])) π"
proof -
  let ?I' = "(φ⇩S Ψ I)"
    and ?G' = "φ⇩S Ψ G" 
    and ?ops = "[φ⇩O¯ Ψ op'. op' ← ops']" 
    and ?Π = "φ Ψ"
  let ?J = "execute_parallel_operator_sas_plus I ?ops"
  {
    fix v a
    assume "(v, a) ∈ dom ?G'"
    then have "?G' (v, a) = execute_parallel_plan 
      (execute_parallel_operator ?I' ops') π (v, a)"
      using assms(3) 
      unfolding map_le_def
      by auto
    hence "?G' (v, a) = execute_parallel_plan (φ⇩S Ψ ?J) π (v, a)" 
      using sas_plus_equivalent_to_strips_i_a_XII[OF assms(1, 2)]
      by simp
  }
  thus ?thesis 
    unfolding map_le_def
    by fast
qed

― ‹ NOTE This is a more abstract formulation of the proposition in 
‹sas_plus_equivalent_to_strips_i› which is better suited for induction proofs. We essentially claim 
that given a plan the execution in STRIPS semantics of which solves the problem of reaching a 
transformed goal state ‹φ⇩S Ψ G› from a transformed initial state ‹φ⇩S Ψ I›---such as 
the goal and initial state of an induced STRIPS problem for a SAS+ problem---is equivalent to an
execution in SAS+ semantics of the transformed plan ‹φ⇩P¯ (φ Ψ) π› w.r.t to the original 
initial state ‹I› and original goal state ‹G›. › 
lemma sas_plus_equivalent_to_strips_i_a:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "dom I ⊆ set ((Ψ)⇩𝒱⇩+)"
    and "∀v ∈ dom I. the (I v) ∈ ℛ⇩+ Ψ v" 
    and "dom G ⊆ set ((Ψ)⇩𝒱⇩+)" 
    and "∀v ∈ dom G. the (G v) ∈ ℛ⇩+ Ψ v" 
    and "∀ops' ∈ set π. ∀op' ∈ set ops'. op' ∈ set ((φ Ψ)⇩𝒪)"
    and "(φ⇩S Ψ G) ⊆⇩m execute_parallel_plan (φ⇩S Ψ I) π"
  shows "G ⊆⇩m execute_parallel_plan_sas_plus I (φ⇩P¯ Ψ π)"
proof -
  let ?vs = "variables_of Ψ"
    and ?ψ = "φ⇩P¯ Ψ π"
  show ?thesis 
    using assms
    proof (induction π arbitrary: I)
      case Nil
      then have "(φ⇩S Ψ G) ⊆⇩m (φ⇩S Ψ I)" 
        by fastforce
      then have "G ⊆⇩m I" 
        using state_to_strips_state_map_le_iff[OF assms(1, 4, 5)]
        by blast
      thus ?case 
        unfolding SAS_Plus_STRIPS.strips_parallel_plan_to_sas_plus_parallel_plan_def
          strips_parallel_plan_to_sas_plus_parallel_plan_def 
        by fastforce
    next
      case (Cons ops' π)
      let ?D = "range_of Ψ"
        and ?Π = "φ Ψ" 
        and ?I' = "φ⇩S Ψ I"
        and ?G' = "φ⇩S Ψ G"
      let ?ops = "[φ⇩O¯ Ψ op'. op' ← ops']" 
      let ?J = "execute_parallel_operator_sas_plus I ?ops"
        and ?J' = "execute_parallel_operator ?I' ops'" 
      have nb⇩1: "set ops' ⊆ set ((?Π)⇩𝒪)" 
        using Cons.prems(6)
        unfolding STRIPS_Semantics.is_parallel_solution_for_problem_def list_all_iff ListMem_iff
        by fastforce
      {
        fix op 
        assume "op ∈ set ?ops" 
        moreover obtain op' where "op' ∈ set ops'" and "op = φ⇩O¯ Ψ op'" 
          using calculation 
          by auto
        moreover have "op' ∈ set ((?Π)⇩𝒪)"
          using nb⇩1 calculation(2)
          by blast
        moreover obtain op'' where "op'' ∈ set ((Ψ)⇩𝒪⇩+)" and "op' = φ⇩O Ψ op''" 
          using calculation(4) 
          by auto
        moreover have "op = op''" 
          using sas_plus_operator_inverse_is[OF assms(1) calculation(5)] calculation(3, 6) 
          by presburger
        ultimately have "op ∈ set ((Ψ)⇩𝒪⇩+) ∧ (∃op' ∈ set ops'. op' = φ⇩O Ψ op)" 
          by blast
      } note nb⇩2 = this
      {
        fix op v a
        assume "op ∈ set ((Ψ)⇩𝒪⇩+)" and "(v, a) ∈ set (effect_of op)" 
        moreover have "op ∈ set ((Ψ)⇩𝒪⇩+)" 
          using nb⇩2 calculation(1)
          by blast
        moreover have "is_valid_operator_sas_plus Ψ op"
          using is_valid_problem_sas_plus_then(2) Cons.prems(1) calculation(3) 
          by blast
        ultimately have "v ∈ set ((Ψ)⇩𝒱⇩+)"
          using is_valid_operator_sas_plus_then(3) 
          by fastforce
      } note nb⇩3 = this
      {
        fix op
        assume "op ∈ set ?ops" 
        then have "op ∈ set ((Ψ)⇩𝒪⇩+)" 
          using nb⇩2 
          by blast
        then have "is_valid_operator_sas_plus Ψ op"
          using is_valid_problem_sas_plus_then(2) Cons.prems(1)
          by blast
        hence "∀(v, a) ∈ set (effect_of op). v ∈ set ((Ψ)⇩𝒱⇩+) 
          ∧ a ∈ ℛ⇩+ Ψ v"
          using is_valid_operator_sas_plus_then(3,4) 
          by fast
      } note nb⇩4 = this
      show ?case 
        proof (cases "STRIPS_Semantics.are_all_operators_applicable ?I' ops' 
          ∧ STRIPS_Semantics.are_all_operator_effects_consistent ops'")
          case True
          {
            {
              have "dom I ⊆ set ((Ψ)⇩𝒱⇩+)" 
                using Cons.prems(2)
                by blast
              hence "(φ⇩S¯ Ψ ?I') = I"
                using strips_state_to_state_inverse_is[OF 
                    Cons.prems(1) _ Cons.prems(3)]
                by argo
            }
            then have "are_all_operators_applicable_in I ?ops
              ∧ are_all_operator_effects_consistent ?ops" 
              using sas_plus_equivalent_to_strips_i_a_IV[OF assms(1) nb⇩1, of I] True
              by simp
            moreover have "(φ⇩P¯ Ψ (ops' # π)) = ?ops # (φ⇩P¯ Ψ π)" 
              unfolding SAS_Plus_STRIPS.strips_parallel_plan_to_sas_plus_parallel_plan_def
                strips_parallel_plan_to_sas_plus_parallel_plan_def
                SAS_Plus_STRIPS.strips_op_to_sasp_def
                  strips_op_to_sasp_def  
              by simp
            ultimately have "execute_parallel_plan_sas_plus I (φ⇩P¯ Ψ (ops' # π)) 
              = execute_parallel_plan_sas_plus ?J (φ⇩P¯ Ψ π)" 
              by force
          } note nb⇩5 = this
          ― ‹ Show the goal using the IH. ›
          {
            have dom_J_subset_eq_vs: "dom ?J ⊆ set ((Ψ)⇩𝒱⇩+)"
              using sas_plus_equivalent_to_strips_i_a_IX[OF Cons.prems(2)] nb⇩2 nb⇩4
              by blast
            moreover {
              have "set ((Ψ)⇩𝒱⇩+) ⊆ dom (range_of Ψ)"
                using is_valid_problem_sas_plus_then(1)[OF assms(1)]
                by fastforce
              moreover have "∀v ∈ dom I. the (I v) ∈ set (the (range_of Ψ v))"
                using Cons.prems(2, 3) assms(1) set_the_range_of_is_range_of_sas_plus_if 
                by force
              moreover have "∀op ∈ set ?ops. ∀(v, a) ∈ set (effect_of op).
                v ∈ set ((Ψ)⇩𝒱⇩+) ∧ a ∈ set (the (?D v))" 
                using set_the_range_of_is_range_of_sas_plus_if assms(1) nb⇩4 
                by fastforce
              moreover have v_in_dom_J_range: "∀v ∈ dom ?J. the (?J v) ∈ set (the (?D v))" 
                using sas_plus_equivalent_to_strips_i_a_X[of 
                    I "set ((Ψ)⇩𝒱⇩+)" ?D ?ops, OF Cons.prems(2)] calculation(1, 2, 3)
                by fastforce
              {
                fix v 
                assume "v ∈ dom ?J"
                moreover have "v ∈ set ((Ψ)⇩𝒱⇩+)"
                  using nb⇩2 calculation dom_J_subset_eq_vs 
                  by blast
                moreover have "set (the (range_of Ψ v)) = ℛ⇩+ Ψ v" 
                  using set_the_range_of_is_range_of_sas_plus_if[OF assms(1)] 
                    calculation(2)
                  by presburger
                ultimately have "the (?J v) ∈ ℛ⇩+ Ψ v" 
                  using nb⇩3 v_in_dom_J_range
                  by blast
              }
              ultimately have "∀v ∈ dom ?J. the (?J v) ∈ ℛ⇩+ Ψ v"
                by fast
            }
            moreover have "∀ops' ∈ set π. ∀op'∈set ops'. op' ∈ set ((φ Ψ)⇩𝒪)"
              using Cons.prems(6)
              by simp
            moreover {
              have "?G' ⊆⇩m execute_parallel_plan ?J' π" 
                using Cons.prems(7) True
                by auto
              hence "(φ⇩S Ψ G) ⊆⇩m execute_parallel_plan (φ⇩S Ψ ?J) π"
                using sas_plus_equivalent_to_strips_i_a_XIII[OF Cons.prems(1)] nb⇩1
                by blast
            }
            ultimately have "G ⊆⇩m execute_parallel_plan_sas_plus I (φ⇩P¯ Ψ (ops' # π))"
              using Cons.IH[of ?J, OF Cons.prems(1) _ _ Cons.prems(4, 5)] Cons.prems(6) nb⇩5 
              by presburger
          }
          thus ?thesis.
        next
          case False
          then have "?G' ⊆⇩m ?I'" 
            using Cons.prems(7)
            by force
          moreover {
            have "dom I ⊆ set ?vs" 
              using Cons.prems(2)
              by simp
            hence "¬(are_all_operators_applicable_in I ?ops
              ∧ are_all_operator_effects_consistent ?ops)" 
              using sas_plus_equivalent_to_strips_i_a_VIII[OF Cons.prems(1) _ Cons.prems(3) nb⇩1] 
                False
              by force
          }
          moreover {
            have "(φ⇩P¯ Ψ (ops' # π)) = ?ops # (φ⇩P¯ Ψ π)" 
              unfolding SAS_Plus_STRIPS.strips_parallel_plan_to_sas_plus_parallel_plan_def
                strips_parallel_plan_to_sas_plus_parallel_plan_def
                SAS_Plus_STRIPS.strips_op_to_sasp_def
                strips_op_to_sasp_def
              by simp
            hence "G ⊆⇩m execute_parallel_plan_sas_plus I (?ops # (φ⇩P¯ Ψ π))
              ⟷ G ⊆⇩m I" 
              using calculation(2)
              by force
          }
          ultimately show ?thesis 
            using state_to_strips_state_map_le_iff[OF Cons.prems(1, 4, 5)] 
            unfolding SAS_Plus_STRIPS.strips_parallel_plan_to_sas_plus_parallel_plan_def
              strips_parallel_plan_to_sas_plus_parallel_plan_def
              SAS_Plus_STRIPS.strips_op_to_sasp_def
              strips_op_to_sasp_def
            by force
        qed
    qed
qed

― ‹ NOTE Show that a solution for the induced STRIPS problem for the given valid SAS+ problem, 
  corresponds to a solution for the given SAS+ problem.

Note that in the context of the SAS+ problem solving pipeline, we
\begin{enumerate}
  \item convert the given valid SAS+ @{text "Ψ"} problem to the corresponding STRIPS problem 
@{text "Π"} (this is implicitely also valid by lemma 
@{text "is_valid_problem_sas_plus_then_strips_transformation_too"}); then,
  \item get a solution @{text "π"}---if it exists---for the induced STRIPS problem by executing 
SATPlan; and finally,
  \item convert @{text "π"} back to a solution @{text "ψ"} for the SAS+ problem.
\end{enumerate} ›
lemma sas_plus_equivalent_to_strips_i:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "STRIPS_Semantics.is_parallel_solution_for_problem 
    (φ Ψ) π"
  shows "goal_of Ψ ⊆⇩m execute_parallel_plan_sas_plus 
    (sas_plus_problem.initial_of Ψ) (φ⇩P¯ Ψ π)"
proof -
  let ?vs = "variables_of Ψ"
    and ?I = "initial_of Ψ" 
    and ?G = "goal_of Ψ"
  let ?Π = "φ Ψ"
  let ?G' = "strips_problem.goal_of ?Π"
    and ?I' = "strips_problem.initial_of ?Π"
  let ?ψ = "φ⇩P¯ Ψ π"
  have "dom ?I ⊆ set ?vs" 
    using is_valid_problem_sas_plus_then(3) assms(1)
    by auto
  moreover have "∀v ∈ dom ?I. the (?I v) ∈ ℛ⇩+ Ψ v" 
    using is_valid_problem_sas_plus_then(4) assms(1) calculation
    by auto
  moreover have "dom ?G ⊆ set ?vs"  and "∀v ∈ dom ?G. the (?G v) ∈ ℛ⇩+ Ψ v" 
    using is_valid_problem_sas_plus_then(5, 6) assms(1)
    by blast+
  moreover have "∀ops'∈set π. ∀op'∈set ops'. op' ∈ set ((?Π)⇩𝒪)"
    using is_parallel_solution_for_problem_operator_set[OF assms(2)]
    by simp
  moreover {
    have "?G' ⊆⇩m execute_parallel_plan ?I' π"
      using assms(2) 
      unfolding STRIPS_Semantics.is_parallel_solution_for_problem_def..
    moreover have "?G' = φ⇩S Ψ ?G" and "?I' = φ⇩S Ψ ?I" 
      by simp+
    ultimately have "(φ⇩S Ψ ?G) ⊆⇩m execute_parallel_plan (φ⇩S Ψ ?I) π"
      by simp
  }
  ultimately show ?thesis 
    using sas_plus_equivalent_to_strips_i_a[OF assms(1)]
    by simp
qed

― ‹ NOTE Show that the operators for a given solution @{text "π"} to the induced STRIPS problem 
for a given SAS+ problem correspond to operators of the SAS+ problem. ›
lemma sas_plus_equivalent_to_strips_ii:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "STRIPS_Semantics.is_parallel_solution_for_problem (φ Ψ) π"
  shows "list_all (list_all (λop. ListMem op (operators_of Ψ))) (φ⇩P¯ Ψ π)" 
proof -
  let ?Π = "φ Ψ" 
  let ?ops = "operators_of Ψ" 
    and ?ψ = "φ⇩P¯ Ψ π"
  have "is_valid_problem_strips ?Π" 
    using is_valid_problem_sas_plus_then_strips_transformation_too[OF assms(1)]
    by simp 
  have nb⇩1: "∀op' ∈ set ((?Π)⇩𝒪). (∃op ∈ set ?ops. op' = (φ⇩O Ψ op))"  
    by auto
  {
    fix ops' op' op
    assume "ops' ∈ set π" and "op' ∈ set ops'" 
    then have "op' ∈ set (strips_problem.operators_of ?Π)"
      using is_parallel_solution_for_problem_operator_set[OF assms(2)]
      by simp
    then obtain op where "op ∈ set ((Ψ)⇩𝒪⇩+)" and "op' = (φ⇩O Ψ op)" 
      by auto
    then have "(φ⇩O¯ Ψ op') ∈ set ((Ψ)⇩𝒪⇩+)"
      using sas_plus_operator_inverse_is[OF assms(1)]
      by presburger
  }
  thus ?thesis 
    unfolding list_all_iff ListMem_iff 
      strips_parallel_plan_to_sas_plus_parallel_plan_def
      SAS_Plus_STRIPS.strips_parallel_plan_to_sas_plus_parallel_plan_def
      SAS_Plus_STRIPS.strips_op_to_sasp_def
      strips_op_to_sasp_def
    by auto
qed

text ‹ We now show that for a parallel solution \<^term>‹π› of \<^term>‹Π› the SAS+ plan 
\<^term>‹ψ ≡ φ⇩P¯ Ψ π› yielded by the STRIPS to SAS+ plan transformation is a solution for 
\<^term>‹Ψ›. The proof uses the definition of parallel STRIPS solutions and shows that the 
execution of \<^term>‹ψ› on the initial state of the SAS+ problem yields a state satisfying the 
problem's goal state, i.e.
  @{text[display, indent=4]"G ⊆⇩m execute_parallel_plan_sas_plus I ψ"}
and by showing that all operators in all parallel operators of \<^term>‹ψ› are operators of the 
problem. ›

theorem
  sas_plus_equivalent_to_strips:
  assumes "is_valid_problem_sas_plus Ψ"
    and "STRIPS_Semantics.is_parallel_solution_for_problem (φ Ψ) π" 
  shows "is_parallel_solution_for_problem Ψ (φ⇩P¯ Ψ π)"
proof -
  let ?I = "initial_of Ψ"
    and ?G = "goal_of Ψ" 
    and ?ops = "operators_of Ψ"
    and ?ψ = "φ⇩P¯ Ψ π"
  show ?thesis
    unfolding is_parallel_solution_for_problem_def Let_def
    proof (rule conjI)
      show "?G ⊆⇩m execute_parallel_plan_sas_plus ?I ?ψ"
        using sas_plus_equivalent_to_strips_i[OF assms].
    next 
      show "list_all (list_all (λop. ListMem op ?ops)) ?ψ" 
        using sas_plus_equivalent_to_strips_ii[OF assms].
    qed
qed

private lemma strips_equivalent_to_sas_plus_i_a_I:
  assumes "is_valid_problem_sas_plus Ψ"
    and "∀op ∈ set ops. op ∈ set ((Ψ)⇩𝒪⇩+)" 
    and "op' ∈ set [φ⇩O Ψ op. op ← ops]"
  obtains op where "op ∈ set ops" 
    and "op' = φ⇩O Ψ op"
proof -
  let ?Π = "φ Ψ" 
  let ?ops = "operators_of Ψ"
  obtain op where "op ∈ set ops" and "op' = φ⇩O Ψ op" 
    using assms(3) 
    by auto
  thus ?thesis 
    using that
    by blast
qed

private corollary strips_equivalent_to_sas_plus_i_a_II:
  assumes"is_valid_problem_sas_plus Ψ"
    and "∀op ∈ set ops. op ∈ set ((Ψ)⇩𝒪⇩+)" 
    and "op' ∈ set [φ⇩O Ψ op. op ← ops]"
  shows "op' ∈ set ((φ Ψ)⇩𝒪)"
    and "is_valid_operator_strips (φ Ψ) op'"
proof -
  let ?Π = "φ Ψ" 
  let ?ops = "operators_of Ψ"
    and ?ops' = "strips_problem.operators_of ?Π"
  obtain op where op_in: "op ∈ set ops" and op'_is: "op' = φ⇩O Ψ op" 
    using strips_equivalent_to_sas_plus_i_a_I[OF assms].
  then have nb: "op' ∈ set ((φ Ψ)⇩𝒪)"
    using assms(2) op_in op'_is 
    by fastforce
  thus "op' ∈ set ((φ Ψ)⇩𝒪)"
    and "is_valid_operator_strips ?Π op'" 
    proof -
      have "∀op' ∈ set ?ops'. is_valid_operator_strips ?Π op'"
        using is_valid_problem_sas_plus_then_strips_transformation_too_iii[OF assms(1)]
        unfolding list_all_iff. 
      thus "is_valid_operator_strips ?Π op'" 
        using nb
        by fastforce
    qed fastforce
qed

(* TODO make private *)
lemma strips_equivalent_to_sas_plus_i_a_III:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "∀op ∈ set ops. op ∈ set ((Ψ)⇩𝒪⇩+)"
  shows "execute_parallel_operator (φ⇩S Ψ s) [φ⇩O Ψ op. op ← ops]
    = (φ⇩S Ψ (execute_parallel_operator_sas_plus s ops))"
proof -
  {
    fix op s
    assume "op ∈ set ((Ψ)⇩𝒪⇩+)" 
    moreover have "(φ⇩O Ψ op) ∈ set ((φ Ψ)⇩𝒪)"
      using calculation 
      by simp
    moreover have "(φ⇩S Ψ s) ++ map_of (effect_to_assignments (φ⇩O Ψ op))
      = (φ⇩S Ψ (s ++ map_of (effect_of (φ⇩O¯ Ψ (φ⇩O Ψ op)))))"
      using sas_plus_equivalent_to_strips_i_a_XI[OF assms(1) calculation(2)]
      by blast
    moreover have "(φ⇩O¯ Ψ (φ⇩O Ψ op)) = op"
      using sas_plus_operator_inverse_is[OF assms(1) calculation(1)].
    ultimately have "(φ⇩S Ψ s) ⪢ (φ⇩O Ψ op)
      = (φ⇩S Ψ (s ⪢⇩+ op))" 
      unfolding execute_operator_def execute_operator_sas_plus_def 
      by simp
  } note nb⇩1 = this
  show ?thesis 
    using assms
    proof (induction ops arbitrary: s)
      case Nil
      then show ?case 
        unfolding execute_parallel_operator_def execute_parallel_operator_sas_plus_def 
        by simp
    next
      case (Cons op ops)
      let ?t = "s ⪢⇩+ op"
      let ?s' = "φ⇩S Ψ s" 
        and ?ops' = "[φ⇩O Ψ op. op ← op # ops]"
      let ?t' = "?s' ⪢ (φ⇩O Ψ op)"
      have "execute_parallel_operator ?s' ?ops' 
        = execute_parallel_operator ?t' [φ⇩O Ψ x. x ← ops]"
        unfolding execute_operator_def
        by simp
      moreover have "(φ⇩S Ψ (execute_parallel_operator_sas_plus s (op # ops)))
        = (φ⇩S Ψ (execute_parallel_operator_sas_plus ?t ops))" 
        unfolding execute_operator_sas_plus_def
        by simp
      moreover {
        have "?t' = (φ⇩S Ψ ?t)"
          using nb⇩1 Cons.prems(2)
          by simp
        hence "execute_parallel_operator ?t'[φ⇩O Ψ x. x ← ops] 
          = (φ⇩S Ψ (execute_parallel_operator_sas_plus ?t ops))" 
          using Cons.IH[of ?t] Cons.prems
          by simp
      }
      ultimately show ?case 
        by argo
    qed
qed

private lemma strips_equivalent_to_sas_plus_i_a_IV:
  assumes "is_valid_problem_sas_plus Ψ"
    and "∀op ∈ set ops. op ∈ set ((Ψ)⇩𝒪⇩+)"
    and "are_all_operators_applicable_in I ops 
    ∧ are_all_operator_effects_consistent ops"
  shows "STRIPS_Semantics.are_all_operators_applicable (φ⇩S Ψ I) [φ⇩O Ψ op. op ← ops]
    ∧ STRIPS_Semantics.are_all_operator_effects_consistent [φ⇩O Ψ op. op ← ops]"
proof -
  let ?vs = "variables_of Ψ" 
    and ?ops = "operators_of Ψ" 
  let ?I' = "φ⇩S Ψ I" 
    and ?ops' = "[φ⇩O Ψ op. op ← ops]"
  have nb⇩1: "∀op ∈ set ops. is_operator_applicable_in I op"
    using assms(3) 
    unfolding are_all_operators_applicable_in_def list_all_iff
    by blast
  have nb⇩2: "∀op ∈ set ops. is_valid_operator_sas_plus Ψ op"
    using is_valid_problem_sas_plus_then(2) assms(1, 2)
    unfolding is_valid_operator_sas_plus_def
    by auto
  have nb⇩3: "∀op ∈ set ops. map_of (precondition_of op) ⊆⇩m I" 
    using nb⇩1 
    unfolding is_operator_applicable_in_def list_all_iff 
    by blast
  {
    fix op⇩1 op⇩2
    assume "op⇩1 ∈ set ops" and "op⇩2 ∈ set ops" 
    hence "are_operator_effects_consistent op⇩1 op⇩2" 
      using assms(3)
      unfolding are_all_operator_effects_consistent_def list_all_iff 
      by blast
  } note nb⇩4 = this
  {
    fix op⇩1 op⇩2
    assume "op⇩1 ∈ set ops" and "op⇩2 ∈ set ops"
    hence "∀(v, a) ∈ set (effect_of op⇩1). ∀(v', a') ∈ set (effect_of op⇩2).
      v ≠ v' ∨ a = a'"
      using nb⇩4
      unfolding are_operator_effects_consistent_def Let_def list_all_iff
      by presburger
  } note nb⇩5 = this
  {
    fix op⇩1' op⇩2' I
    assume "op⇩1' ∈ set ?ops'" 
      and "op⇩2' ∈ set ?ops'" 
      and "∃(v, a) ∈ set (add_effects_of op⇩1'). ∃(v', a') ∈ set (delete_effects_of op⇩2').
        (v, a) = (v', a')" 
    moreover obtain op⇩1 op⇩2
      where "op⇩1 ∈ set ops" 
          and "op⇩1' = φ⇩O Ψ op⇩1" 
        and "op⇩2 ∈ set ops" 
          and "op⇩2' = φ⇩O Ψ op⇩2" 
      using strips_equivalent_to_sas_plus_i_a_I[OF assms(1, 2)] calculation(1, 2) 
      by auto
    moreover have "is_valid_operator_sas_plus Ψ op⇩1"
       and is_valid_operator_op⇩2: "is_valid_operator_sas_plus Ψ op⇩2"
      using calculation(4, 6) nb⇩2 
       by blast+
    moreover obtain v v' a a' 
      where "(v, a) ∈ set (add_effects_of op⇩1')" 
        and "(v', a') ∈ set (delete_effects_of op⇩2')"
        and "(v, a) = (v', a')" 
      using calculation
      by blast
    moreover have "(v, a) ∈ set (effect_of op⇩1)" 
      using calculation(5, 10) 
      unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def
        sasp_op_to_strips_def Let_def
      by fastforce
    moreover have "v = v'" and "a = a'"
      using calculation(12) 
      by simp+
    moreover {
      have "(v', a') ∈ (⋃(v, a) ∈ set (effect_of op⇩2). 
        { (v, a') | a'. a' ∈ (ℛ⇩+ Ψ v) ∧  a' ≠ a })"
        using sasp_op_to_strips_set_delete_effects_is 
          calculation(7, 9, 11)
        by blast
      then obtain v'' a'' where "(v'', a'') ∈ set (effect_of op⇩2)" 
        and "(v', a') ∈ { (v'', a''') | a'''. a''' ∈ (ℛ⇩+ Ψ v'') ∧  a''' ≠ a'' }"
        by blast
      moreover have "(v', a'') ∈ set (effect_of op⇩2)" 
        using calculation 
        by blast
      moreover have "a' ∈ ℛ⇩+ Ψ v''" and "a' ≠ a''"
        using calculation(1, 2) 
        by fast+
      ultimately have "∃a''. (v', a'') ∈ set (effect_of op⇩2) ∧ a' ∈ (ℛ⇩+ Ψ v') 
        ∧ a' ≠ a''" 
        by blast
    }
    moreover obtain a'' where "a' ∈ ℛ⇩+ Ψ v'" 
      and "(v', a'') ∈ set (effect_of op⇩2)" 
      and "a' ≠ a''"
      using calculation(16)
      by blast
    moreover have "∃(v, a) ∈ set (effect_of op⇩1). (∃(v', a') ∈ set (effect_of op⇩2). 
      v = v' ∧ a ≠ a')"
      using calculation(13, 14, 15, 17, 18, 19)
      by blast
    ― ‹ TODO slow. ›
    ultimately have "∃op⇩1 ∈ set ops. ∃op⇩2 ∈ set ops. ¬are_operator_effects_consistent op⇩1 op⇩2"
      unfolding are_operator_effects_consistent_def list_all_iff
      by fastforce
  } note nb⇩6 = this
  show ?thesis
    proof (rule conjI)
      {
        fix op' 
        assume "op' ∈ set ?ops'" 
        moreover obtain op where op_in: "op ∈ set ops" 
          and op'_is: "op' = φ⇩O Ψ op"
          and op'_in: "op' ∈ set ((φ Ψ)⇩𝒪)"
          and is_valid_op': "is_valid_operator_strips (φ Ψ) op'"
          using strips_equivalent_to_sas_plus_i_a_I[OF assms(1, 2)]
            strips_equivalent_to_sas_plus_i_a_II[OF assms(1, 2)] calculation 
          by metis
        moreover have is_valid_op: "is_valid_operator_sas_plus Ψ op"
          using nb⇩2 calculation(2)..
        {
          fix v a
          assume v_a_in_preconditions': "(v, a) ∈ set (strips_operator.precondition_of op')"
          have v_a_in_preconditions: "(v, a) ∈ set (precondition_of op)" 
            using op'_is
            unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def
              sasp_op_to_strips_def Let_def
            using v_a_in_preconditions' 
            by force
          moreover have "v ∈ set ?vs" and "a ∈ ℛ⇩+ Ψ v"
            using is_valid_operator_sas_plus_then(1,2) is_valid_op calculation(1)
            by fastforce+
          moreover {
            have "∀(v, a) ∈ set (precondition_of op). ∀(v', a') ∈ set (precondition_of op).
              v ≠ v' ∨ a = a'" 
              using is_valid_operator_sas_plus_then(5) is_valid_op
              by fast
            hence "map_of (precondition_of op) v = Some a" 
              using map_of_constant_assignments_defined_if[OF _ v_a_in_preconditions]
              by blast
          }
          moreover have "v ∈ dom (map_of (precondition_of op))" 
            using calculation(4)
            by blast
          moreover have "I v = Some a" 
            using nb⇩3 
            unfolding map_le_def 
            using op_in calculation(4, 5)
            by metis
          moreover have "(v, a) ∈ dom ?I'" 
            using state_to_strips_state_dom_element_iff[OF assms(1)] 
              calculation(2, 3, 6)
            by simp
          ultimately have "?I' (v, a) = Some True" 
            using state_to_strips_state_range_is[OF assms(1)]
            by simp
        }
        hence "STRIPS_Representation.is_operator_applicable_in ?I' op'" 
          unfolding 
            STRIPS_Representation.is_operator_applicable_in_def 
            Let_def list_all_iff 
          by fast
      }
      thus "are_all_operators_applicable ?I' ?ops'"
        unfolding are_all_operators_applicable_def list_all_iff
        by blast
    next 
      {
        fix op⇩1' op⇩2'
        assume op⇩1'_in_ops': "op⇩1' ∈ set ?ops'" and op⇩2'_in_ops': "op⇩2' ∈ set ?ops'" 
        have "STRIPS_Semantics.are_operator_effects_consistent op⇩1' op⇩2'" 
          unfolding STRIPS_Semantics.are_operator_effects_consistent_def Let_def
          ― ‹ TODO proof is symmetrical... refactor into nb. ›
          proof (rule conjI)          
            show "¬list_ex (λx. list_ex ((=) x) (delete_effects_of op⇩2')) 
              (add_effects_of op⇩1')"
              proof (rule ccontr)
                assume "¬¬list_ex (λv. list_ex ((=) v) (delete_effects_of op⇩2')) 
                  (add_effects_of op⇩1')" 
                then have "∃(v, a) ∈ set (delete_effects_of op⇩2'). 
                  ∃(v', a') ∈ set (add_effects_of op⇩1'). (v, a) = (v', a')" 
                  unfolding list_ex_iff 
                  by fastforce
                then obtain op⇩1 op⇩2 where "op⇩1 ∈ set ops"
                  and "op⇩2 ∈ set ops" 
                  and "¬are_operator_effects_consistent op⇩1 op⇩2" 
                  using nb⇩6[OF op⇩1'_in_ops' op⇩2'_in_ops']
                  by blast
                thus False 
                  using nb⇩4
                  by blast              
              qed
          next
            show "¬list_ex (λv. list_ex ((=) v) (add_effects_of op⇩2')) (delete_effects_of op⇩1')" 
              proof (rule ccontr)
                assume "¬¬list_ex (λv. list_ex ((=) v) (add_effects_of op⇩2')) 
                  (delete_effects_of op⇩1')" 
                then have "∃(v, a) ∈ set (delete_effects_of op⇩1'). 
                  ∃(v', a') ∈ set (add_effects_of op⇩2'). (v, a) = (v', a')" 
                  unfolding list_ex_iff
                  by fastforce
                then obtain op⇩1 op⇩2 where "op⇩1 ∈ set ops"
                  and "op⇩2 ∈ set ops" 
                  and "¬are_operator_effects_consistent op⇩1 op⇩2" 
                  using nb⇩6[OF op⇩2'_in_ops' op⇩1'_in_ops']
                  by blast
                thus False 
                  using nb⇩4
                  by blast
              qed
          qed
      }
      thus "STRIPS_Semantics.are_all_operator_effects_consistent ?ops'" 
        unfolding STRIPS_Semantics.are_all_operator_effects_consistent_def list_all_iff
        by blast
    qed
qed

private lemma strips_equivalent_to_sas_plus_i_a_V:
  assumes "is_valid_problem_sas_plus Ψ"
    and "∀op ∈ set ops. op ∈ set ((Ψ)⇩𝒪⇩+)"
    and "¬(are_all_operators_applicable_in s ops 
    ∧ are_all_operator_effects_consistent ops)"
  shows "¬(STRIPS_Semantics.are_all_operators_applicable (φ⇩S Ψ s) [φ⇩O Ψ op. op ← ops]
    ∧ STRIPS_Semantics.are_all_operator_effects_consistent [φ⇩O Ψ op. op ← ops])"
proof -
  let ?vs = "variables_of Ψ"
    and ?ops = "operators_of Ψ" 
  let ?s' = "φ⇩S Ψ s"
    and ?ops' = "[φ⇩O Ψ op. op ← ops]"
  {
    fix op
    assume "op ∈ set ops" 
    hence "∃op' ∈ set ?ops'. op' = φ⇩O Ψ op" 
      by simp
  } note nb⇩1 = this
  {
    fix op
    assume "op ∈ set ops" 
    then have "op ∈ set ((Ψ)⇩𝒪⇩+)" 
      using assms(2) 
      by blast
    then have "is_valid_operator_sas_plus Ψ op"
      using is_valid_problem_sas_plus_then(2) assms(1)
      unfolding is_valid_operator_sas_plus_def
      by auto
    hence "∀(v, a) ∈ set (precondition_of op). ∀(v', a') ∈ set (precondition_of op).
      v ≠ v' ∨ a = a'" 
      using is_valid_operator_sas_plus_then(5)
      unfolding is_valid_operator_sas_plus_def
      by fast
  } note nb⇩2 = this
  {
    consider (A) "¬are_all_operators_applicable_in s ops" 
      | (B) "¬are_all_operator_effects_consistent ops" 
      using assms(3)
      by blast
    hence "¬STRIPS_Semantics.are_all_operators_applicable ?s' ?ops' 
      ∨ ¬STRIPS_Semantics.are_all_operator_effects_consistent ?ops'"
      proof (cases)
        case A
        then obtain op where op_in: "op ∈ set ops" 
          and not_precondition_map_le_s: "¬(map_of (precondition_of op) ⊆⇩m s)"
          using A
          unfolding are_all_operators_applicable_in_def list_all_iff 
            is_operator_applicable_in_def
          by blast
        then obtain op' where op'_in: "op' ∈ set ?ops'" and op'_is: "op' = φ⇩O Ψ op" 
          using nb⇩1
          by blast
        have "¬are_all_operators_applicable ?s' ?ops'" 
          proof (rule ccontr)
            assume "¬¬are_all_operators_applicable ?s' ?ops'"
            then have all_operators_applicable: "are_all_operators_applicable ?s' ?ops'"
              by simp
            moreover {
              fix v 
              assume "v ∈ dom (map_of (precondition_of op))" 
              moreover obtain a where "map_of (precondition_of op) v = Some a" 
                using calculation
                by blast
              moreover have "(v, a) ∈ set (precondition_of op)"
                using map_of_SomeD[OF calculation(2)].
              moreover have "(v, a) ∈ set (strips_operator.precondition_of op')"
                using op'_is 
                unfolding sasp_op_to_strips_def
                  SAS_Plus_STRIPS.sasp_op_to_strips_def
                using calculation(3) 
                by auto 
              moreover have "?s' (v, a) = Some True"
                using all_operators_applicable calculation 
                unfolding are_all_operators_applicable_def 
                    STRIPS_Representation.is_operator_applicable_in_def 
                    is_operator_applicable_in_def Let_def list_all_iff 
                using op'_in
                by fast
              moreover have "(v, a) ∈ dom ?s'" 
                using calculation(5)
                by blast
              moreover have "(v, a) ∈ set (precondition_of op)" 
                using op'_is calculation(3)
                unfolding sasp_op_to_strips_def Let_def
                by fastforce
              moreover have "v ∈ set ?vs" 
                and "a ∈ ℛ⇩+ Ψ v" 
                and "s v ≠ None" 
                using state_to_strips_state_dom_element_iff[OF assms(1)]
                  calculation(6)
                by simp+
              moreover have "?s' (v, a) = Some (the (s v) = a)" 
                using state_to_strips_state_range_is[OF 
                    assms(1) calculation(6)].
              moreover have "the (s v) = a" 
                using calculation(5, 11)
                by fastforce
              moreover have "s v = Some a" 
                using calculation(12) option.collapse[OF calculation(10)]
                by argo
              moreover have "map_of (precondition_of op) v = Some a"
                using map_of_constant_assignments_defined_if[OF nb⇩2[OF op_in] calculation(7)].
              ultimately have "map_of (precondition_of op) v = s v"
                by argo
            }
            then have "map_of (precondition_of op) ⊆⇩m s" 
              unfolding map_le_def
              by blast
            thus False 
              using not_precondition_map_le_s
              by simp
          qed
        thus ?thesis 
          by simp
      next
        case B
        {
          obtain op⇩1 op⇩2 v v' a a' 
            where "op⇩1 ∈ set ops"
              and op⇩2_in: "op⇩2 ∈ set ops"
              and v_a_in: "(v, a) ∈ set (effect_of op⇩1)"
              and v'_a'_in: "(v', a') ∈ set (effect_of op⇩2)" 
              and v_is: "v = v'" and a_is: "a ≠ a'"  
            using B 
            unfolding are_all_operator_effects_consistent_def 
              are_operator_effects_consistent_def list_all_iff Let_def
            by blast
          moreover obtain op⇩1' op⇩2' where "op⇩1' ∈ set ?ops'" and "op⇩1' = φ⇩O Ψ op⇩1"
            and "op⇩1' ∈ set ?ops'" and op⇩2'_is: "op⇩2' = φ⇩O Ψ op⇩2"
            using nb⇩1[OF calculation(1)] nb⇩1[OF calculation(2)]
            by blast
          moreover have "(v, a) ∈ set (add_effects_of op⇩1')"
            using calculation(3, 8)
            unfolding SAS_Plus_STRIPS.sasp_op_to_strips_def
              sasp_op_to_strips_def Let_def
            by force
          moreover {
            have "is_valid_operator_sas_plus Ψ op⇩1" 
              using assms(2) calculation(1) is_valid_problem_sas_plus_then(2) assms(1)
              unfolding is_valid_operator_sas_plus_def 
              by auto
            moreover have "is_valid_operator_sas_plus Ψ op⇩2"
              using sublocale_sas_plus_finite_domain_representation_ii(2)[
                  OF assms(1)] assms(2) op⇩2_in 
              by blast 
            moreover have "a ∈ ℛ⇩+ Ψ v" 
              using is_valid_operator_sas_plus_then(4) calculation v_a_in
              unfolding is_valid_operator_sas_plus_def
              by fastforce
            ultimately have "(v, a) ∈ set (delete_effects_of op⇩2')" 
              using sasp_op_to_strips_set_delete_effects_is[of Ψ op⇩2]
                v'_a'_in v_is a_is 
              using op⇩2'_is 
              by blast
          }
          ― ‹ TODO slow. ›
          ultimately have "∃op⇩1' ∈ set ?ops'. ∃op⇩2' ∈ set ?ops'. 
            ∃(v, a) ∈ set (delete_effects_of op⇩2'). ∃(v', a') ∈ set (add_effects_of op⇩1').
            (v, a) = (v', a')"
            by fastforce
        }
        then have "¬STRIPS_Semantics.are_all_operator_effects_consistent ?ops'" 
          unfolding STRIPS_Semantics.are_all_operator_effects_consistent_def 
            STRIPS_Semantics.are_operator_effects_consistent_def list_all_iff list_ex_iff Let_def 
          by blast
        thus ?thesis 
          by simp 
      qed
  }
  thus ?thesis 
    by blast
qed

(* TODO make private *)
lemma strips_equivalent_to_sas_plus_i_a:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "dom I ⊆ set ((Ψ)⇩𝒱⇩+)"
    and "∀v ∈ dom I. the (I v) ∈ ℛ⇩+ Ψ v" 
    and "dom G ⊆ set ((Ψ)⇩𝒱⇩+)" 
    and "∀v ∈ dom G. the (G v) ∈ ℛ⇩+ Ψ v" 
    and "∀ops ∈ set ψ. ∀op ∈ set ops. op ∈ set ((Ψ)⇩𝒪⇩+)"
    and "G ⊆⇩m execute_parallel_plan_sas_plus I ψ" 
  shows "(φ⇩S Ψ G) ⊆⇩m execute_parallel_plan (φ⇩S Ψ I) (φ⇩P Ψ ψ)" 
proof -
  let ?Π = "φ Ψ"
    and ?G' = "φ⇩S Ψ G"
  show ?thesis 
    using assms
    proof (induction ψ arbitrary: I)
      case Nil
      let ?I' = "φ⇩S Ψ I"
      have "G ⊆⇩m I" 
        using Nil
        by simp
      moreover have "?G' ⊆⇩m ?I'"
        using state_to_strips_state_map_le_iff[OF Nil.prems(1, 4, 5)] 
          calculation..
      ultimately show ?case 
        unfolding SAS_Plus_STRIPS.sas_plus_parallel_plan_to_strips_parallel_plan_def
          sas_plus_parallel_plan_to_strips_parallel_plan_def
        by simp
    next
      case (Cons ops ψ)
      let ?vs = "variables_of Ψ"
        and ?ops = "operators_of Ψ"
        and ?J = "execute_parallel_operator_sas_plus I ops" 
        and ?π = "φ⇩P Ψ (ops # ψ)"
      let ?I' = "φ⇩S Ψ I"
        and ?J' = "φ⇩S Ψ ?J"
        and ?ops' = "[φ⇩O Ψ op. op ← ops]"
      {
        fix op v a
        assume "op ∈ set ops" and "(v, a) ∈ set (effect_of op)" 
        moreover have "op ∈ set ?ops"
          using Cons.prems(6) calculation(1)
          by simp
        moreover have "is_valid_operator_sas_plus Ψ op" 
          using is_valid_problem_sas_plus_then(2) Cons.prems(1) calculation(3)
          unfolding is_valid_operator_sas_plus_def
          by auto
        ultimately have "v ∈ set ((Ψ)⇩𝒱⇩+)" 
          and "a ∈ ℛ⇩+ Ψ v"
          using is_valid_operator_sas_plus_then(3,4)
          by fastforce+
      } note nb⇩1 = this
      show ?case
      proof (cases "are_all_operators_applicable_in I ops 
        ∧ are_all_operator_effects_consistent ops")
        case True
        {
          have "(φ⇩P Ψ (ops # ψ)) = ?ops' # (φ⇩P Ψ ψ)"
            unfolding sas_plus_parallel_plan_to_strips_parallel_plan_def
              SAS_Plus_STRIPS.sas_plus_parallel_plan_to_strips_parallel_plan_def 
              sasp_op_to_strips_def
              SAS_Plus_STRIPS.sasp_op_to_strips_def
            by simp
          moreover have "∀op ∈ set ops. op ∈ set ((Ψ)⇩𝒪⇩+)" 
            using Cons.prems(6)
            by simp
          moreover have "STRIPS_Semantics.are_all_operators_applicable ?I' ?ops'" 
            and "STRIPS_Semantics.are_all_operator_effects_consistent ?ops'" 
            using strips_equivalent_to_sas_plus_i_a_IV[OF Cons.prems(1) _ True] calculation
            by blast+
          ultimately have "execute_parallel_plan ?I' ?π 
            = execute_parallel_plan (execute_parallel_operator ?I' ?ops') (φ⇩P Ψ ψ)"
            by fastforce
        }
        ― ‹ NOTE Instantiate the IH on the next state of the SAS+ execution 
          ‹execute_parallel_operator_sas_plus I ops›. ›
        moreover
        {
          {
            have "dom I ⊆ set (sas_plus_problem.variables_of Ψ)"
              using Cons.prems(2)
              by blast
            moreover have "∀op ∈ set ops. ∀(v, a) ∈ set (effect_of op). 
              v ∈ set ((Ψ)⇩𝒱⇩+)" 
              using nb⇩1(1) 
              by blast
            ultimately have "dom ?J ⊆ set ((Ψ)⇩𝒱⇩+)" 
              using sas_plus_equivalent_to_strips_i_a_IX[of I "set ?vs"]
              by simp
          } note nb⇩2 = this
          moreover {
            have "dom I ⊆ set (sas_plus_problem.variables_of Ψ)"
              using Cons.prems(2)
              by blast
            moreover have "set (sas_plus_problem.variables_of Ψ)
              ⊆ dom (range_of Ψ)"
              using is_valid_problem_sas_plus_dom_sas_plus_problem_range_of assms(1)
              by auto
           moreover {
              fix v 
              assume "v ∈ dom I"  
              moreover have "v ∈ set ((Ψ)⇩𝒱⇩+)" 
                using Cons.prems(2) calculation
                by blast
              ultimately have "the (I v) ∈ set (the (range_of Ψ v))" 
                using Cons.prems(3)
                using set_the_range_of_is_range_of_sas_plus_if[OF assms(1)]
                by blast
            }
            moreover have "∀op∈set ops. ∀(v, a)∈set (effect_of op).
              v ∈ set (sas_plus_problem.variables_of Ψ) ∧ a ∈ set (the (range_of Ψ v))"
              using set_the_range_of_is_range_of_sas_plus_if[OF assms(1)] nb⇩1(1) nb⇩1(2)
              by force
            moreover have nb⇩3: "∀v ∈ dom ?J. the (?J v) ∈ set (the (range_of Ψ v))" 
              using sas_plus_equivalent_to_strips_i_a_X[of I "set ?vs" "range_of Ψ" ops] 
                calculation
              by fast
            moreover {
              fix v
              assume "v ∈ dom ?J"
              moreover have "v ∈ set ((Ψ)⇩𝒱⇩+)"
                using nb⇩2 calculation
                by blast
              moreover have "set (the (range_of Ψ v)) = ℛ⇩+ Ψ v" 
                using set_the_range_of_is_range_of_sas_plus_if[OF assms(1)] 
                  calculation(2)
                by presburger
              ultimately have "the (?J v) ∈ ℛ⇩+ Ψ v" 
                using nb⇩3
                by blast
            }
            ultimately have "∀v ∈ dom ?J. the (?J v) ∈ ℛ⇩+ Ψ v"
              by fast
          }
          moreover have "∀ops∈set ψ. ∀op∈set ops. op ∈ set ?ops" 
            using Cons.prems(6)
            by auto
          moreover have "G ⊆⇩m execute_parallel_plan_sas_plus ?J ψ" 
            using Cons.prems(7) True
            by simp
          ultimately have "(φ⇩S Ψ G) ⊆⇩m execute_parallel_plan ?J' (φ⇩P Ψ ψ)"
            using Cons.IH[of ?J, OF Cons.prems(1) _ _ Cons.prems(4, 5)]
            by fastforce
        }
        moreover have "execute_parallel_operator ?I' ?ops' = ?J'" 
          using assms(1) strips_equivalent_to_sas_plus_i_a_III[OF assms(1)] Cons.prems(6)
          by auto
        ultimately show ?thesis
          by argo
      next
        case False
        then have nb: "G ⊆⇩m I" 
          using Cons.prems(7)
          by force
        moreover {
          have "?π = ?ops' # (φ⇩P Ψ ψ)"
            unfolding sas_plus_parallel_plan_to_strips_parallel_plan_def
              SAS_Plus_STRIPS.sas_plus_parallel_plan_to_strips_parallel_plan_def 
              sasp_op_to_strips_def
              SAS_Plus_STRIPS.sasp_op_to_strips_def Let_def
            by auto
          moreover have "set ?ops' ⊆ set (strips_problem.operators_of ?Π)"
            using strips_equivalent_to_sas_plus_i_a_II(1)[OF assms(1)] Cons.prems(6)
            by auto
          moreover have "¬(STRIPS_Semantics.are_all_operators_applicable ?I' ?ops' 
            ∧ STRIPS_Semantics.are_all_operator_effects_consistent ?ops')"
            using strips_equivalent_to_sas_plus_i_a_V[OF assms(1) _ False] Cons.prems(6)
            by force 
          ultimately have "execute_parallel_plan ?I' ?π = ?I'"
            by auto
        }
        moreover have "?G' ⊆⇩m ?I'" 
          using state_to_strips_state_map_le_iff[OF Cons.prems(1, 4, 5)] nb
          by blast
        ultimately show ?thesis 
          by presburger
        qed 
    qed
qed

(* TODO make private *)
lemma strips_equivalent_to_sas_plus_i:
  assumes "is_valid_problem_sas_plus Ψ"
    and "is_parallel_solution_for_problem Ψ ψ"
  shows "(strips_problem.goal_of (φ Ψ)) ⊆⇩m execute_parallel_plan 
    (strips_problem.initial_of (φ Ψ)) (φ⇩P Ψ ψ)" 
proof -
  let ?vs = "variables_of Ψ"
    and ?ops = "operators_of Ψ"
    and ?I = "initial_of Ψ"
    and ?G = "goal_of Ψ"
  let ?Π = "φ Ψ"
  let ?I' = "strips_problem.initial_of ?Π"
    and ?G' = "strips_problem.goal_of ?Π"
  have "dom ?I ⊆ set ?vs"
    using is_valid_problem_sas_plus_then(3) assms(1)
    by auto
  moreover have "∀v∈dom ?I. the (?I v) ∈ ℛ⇩+ Ψ v" 
    using is_valid_problem_sas_plus_then(4) assms(1) calculation
    by auto
  moreover have "dom ?G ⊆ set ((Ψ)⇩𝒱⇩+)" 
    using is_valid_problem_sas_plus_then(5) assms(1)
    by auto
  moreover have "∀v ∈ dom ?G. the (?G v) ∈ ℛ⇩+ Ψ v"
    using is_valid_problem_sas_plus_then(6) assms(1)
    by auto
  moreover have "∀ops ∈ set ψ. ∀op ∈ set ops. op ∈ set ?ops"
    using is_parallel_solution_for_problem_plan_operator_set[OF assms(2)]
    by fastforce
  moreover have "?G ⊆⇩m execute_parallel_plan_sas_plus ?I ψ" 
    using assms(2) 
    unfolding is_parallel_solution_for_problem_def
    by simp
  (* TODO slow *)
  ultimately show ?thesis
    using strips_equivalent_to_sas_plus_i_a[OF assms(1), of ?I ?G ψ]
    unfolding sas_plus_problem_to_strips_problem_def
      SAS_Plus_STRIPS.sas_plus_problem_to_strips_problem_def 
      state_to_strips_state_def
      SAS_Plus_STRIPS.state_to_strips_state_def
    by force
qed

(* TODO make private *)
lemma strips_equivalent_to_sas_plus_ii:
  assumes "is_valid_problem_sas_plus Ψ"
    and "is_parallel_solution_for_problem Ψ ψ"
  shows "list_all (list_all (λop. ListMem op (strips_problem.operators_of (φ Ψ)))) (φ⇩P Ψ ψ)" 
proof -
  let ?ops = "operators_of Ψ"
  let ?Π = "φ Ψ"
  let ?ops' = "strips_problem.operators_of ?Π"
    and ?π = "φ⇩P Ψ ψ"
  have "is_valid_problem_strips ?Π" 
    using is_valid_problem_sas_plus_then_strips_transformation_too[OF assms(1)]
    by simp 
  have nb⇩1: "∀op ∈ set ?ops. (∃op' ∈ set ?ops'. op' = (φ⇩O Ψ op))" 
    unfolding sas_plus_problem_to_strips_problem_def
      SAS_Plus_STRIPS.sas_plus_problem_to_strips_problem_def Let_def 
      sasp_op_to_strips_def
    by force
  {
    fix ops op op'
    assume "ops ∈ set ψ" and "op ∈ set ops" 
    moreover have "op ∈ set ((Ψ)⇩𝒪⇩+)"
      using is_parallel_solution_for_problem_plan_operator_set[OF assms(2)] 
        calculation
      by blast
    moreover obtain op' where "op' ∈ set ?ops'" and "op' = (φ⇩O Ψ op)" 
      using nb⇩1 calculation(3)
      by auto
    ultimately have "(φ⇩O Ψ op) ∈ set ?ops'"
      by blast
  }
  thus ?thesis 
    unfolding list_all_iff ListMem_iff Let_def  
      sas_plus_problem_to_strips_problem_def
      SAS_Plus_STRIPS.sas_plus_problem_to_strips_problem_def
      sas_plus_parallel_plan_to_strips_parallel_plan_def
      SAS_Plus_STRIPS.sas_plus_parallel_plan_to_strips_parallel_plan_def 
      sasp_op_to_strips_def
      SAS_Plus_STRIPS.sasp_op_to_strips_def 
      Let_def 
    by auto
qed

text ‹ The following lemma proves the complementary proposition to theorem 
\ref{isathm:equivalence-parallel-strips-parallel-sas-plus}. Namely, given a parallel solution
\<^term>‹ψ› for a SAS+ problem, the transformation to a STRIPS plan \<^term>‹φ⇩P Ψ ψ› also is a solution 
to the corresponding STRIPS problem \<^term>‹Π ≡ (φ Ψ)›. In this direction, we have to show that the 
execution of the transformed plan reaches the goal state \<^term>‹G' ≡ strips_problem.goal_of Π› 
of the corresponding STRIPS problem, i.e.
  @{text[display, indent=4] "G' ⊆⇩m execute_parallel_plan I' π"} 
and that all operators in the transformed plan \<^term>‹π› are operators of \<^term>‹Π›. ›

theorem
  strips_equivalent_to_sas_plus:
  assumes "is_valid_problem_sas_plus Ψ"
    and "is_parallel_solution_for_problem Ψ ψ"
  shows "STRIPS_Semantics.is_parallel_solution_for_problem (φ Ψ) (φ⇩P Ψ ψ)"
proof -
  let ?Π = "φ Ψ"
  let ?I' = "strips_problem.initial_of ?Π"
    and ?G' = "strips_problem.goal_of ?Π"
    and ?ops' = "strips_problem.operators_of ?Π"
    and ?π = "φ⇩P Ψ ψ"
  show ?thesis
    unfolding STRIPS_Semantics.is_parallel_solution_for_problem_def 
    proof (rule conjI)
      show "?G' ⊆⇩m execute_parallel_plan ?I' ?π"
        using strips_equivalent_to_sas_plus_i[OF assms]
        by simp
    next 
      show "list_all (list_all (λop. ListMem op ?ops')) ?π" 
        using strips_equivalent_to_sas_plus_ii[OF assms].
    qed
qed

lemma embedded_serial_sas_plus_plan_operator_structure:
  assumes "ops ∈ set (embed ψ)"
  obtains op 
  where "op ∈ set ψ" 
    and "[φ⇩O Ψ op. op ← ops] = [φ⇩O Ψ op]"
proof -
  let ?ψ' = "embed ψ"
  {
    have "?ψ' = [[op]. op ← ψ]"
      by (induction ψ; force)
    moreover obtain op where "ops = [op]" and "op ∈ set ψ" 
      using assms calculation 
      by fastforce
    ultimately have "∃op ∈ set ψ. [φ⇩O Ψ op. op ← ops] = [φ⇩O Ψ op]"
      by auto
  }
  thus ?thesis 
    using that
    by meson
qed

private lemma serial_sas_plus_equivalent_to_serial_strips_i: 
  assumes "ops ∈ set (φ⇩P Ψ (embed ψ))"
  obtains op where "op ∈ set ψ" and "ops = [φ⇩O Ψ op]"  
proof -
  let ?ψ' = "embed ψ" 
  {
    have "set (φ⇩P Ψ (embed ψ)) = { [φ⇩O Ψ op. op ← ops]  | ops. ops ∈ set ?ψ' }"
      
      unfolding sas_plus_parallel_plan_to_strips_parallel_plan_def  
        SAS_Plus_STRIPS.sas_plus_parallel_plan_to_strips_parallel_plan_def
        sasp_op_to_strips_def set_map
      using setcompr_eq_image  
      by blast
    moreover obtain ops' where "ops' ∈ set ?ψ'" and "ops = [φ⇩O Ψ op. op ← ops']" 
      using assms(1) calculation
      by blast
    moreover obtain op where "op ∈ set ψ" and "ops = [φ⇩O Ψ op]" 
      using embedded_serial_sas_plus_plan_operator_structure calculation(2, 3)
      by blast
    ultimately have "∃op ∈ set ψ. ops = [φ⇩O Ψ op]"
      by meson
  }
  thus ?thesis 
    using that..
qed

private lemma serial_sas_plus_equivalent_to_serial_strips_ii[simp]:
  "concat (φ⇩P Ψ (embed ψ)) = [φ⇩O Ψ op. op ← ψ]" 
proof -
  let ?ψ' = "List_Supplement.embed ψ"
  have "concat (φ⇩P Ψ ?ψ') = map (λop. φ⇩O Ψ op) (concat ?ψ')" 
    unfolding sas_plus_parallel_plan_to_strips_parallel_plan_def
      SAS_Plus_STRIPS.sas_plus_parallel_plan_to_strips_parallel_plan_def
      sasp_op_to_strips_def
      SAS_Plus_STRIPS.sasp_op_to_strips_def Let_def
      map_concat
    by blast
  also have "… = map (λop. φ⇩O Ψ op) ψ" 
    unfolding concat_is_inverse_of_embed[of ψ]..
  finally show "concat (φ⇩P Ψ (embed ψ)) = [φ⇩O Ψ op. op ← ψ]".
qed

text ‹ Having established the equivalence of parallel STRIPS and SAS+, we can now show the 
equivalence in the serial case. The proof combines the 
embedding theorem for serial SAS+ solutions (\ref{isathm:serial-sas-plus-embedding}), the parallel 
plan equivalence theorem \ref{isathm:equivalence-parallel-sas-plus-parallel-strips}, and the 
flattening theorem for parallel STRIPS plans (\ref{isathm:embedded-serial-plan-flattening-strips}).
More precisely, given a serial SAS+ solution \<^term>‹ψ› for a SAS+ problem \<^term>‹Ψ›, the embedding 
theorem confirms that the embedded plan \<^term>‹embed ψ› is an equivalent parallel solution to
\<^term>‹Ψ›. By parallel plan equivalence, \<^term>‹π ≡ φ⇩P Ψ (embed ψ)› is a parallel solution for the 
corresponding STRIPS problem \<^term>‹φ Ψ›. Moreover, since \<^term>‹embed ψ› is a plan consisting of 
singleton parallel operators, the same is true for \<^term>‹π›. Hence, the flattening lemma applies 
and \<^term>‹concat π› is a serial solution for \<^term>‹φ Ψ›. Since \<^term>‹concat› moreover can be shown 
to be the inverse of \<^term>‹embed›, the term 
  @{text[display, indent=4] "concat π = concat (φ⇩P Ψ (embed ψ))"}
can be reduced to the intuitive form 
  @{text[display, indent=4] "π = [φ⇩O Ψ op. op ← ψ]"}
which concludes the proof. ›

theorem 
  serial_sas_plus_equivalent_to_serial_strips:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "SAS_Plus_Semantics.is_serial_solution_for_problem Ψ ψ"
  shows "STRIPS_Semantics.is_serial_solution_for_problem (φ Ψ) [φ⇩O Ψ op. op ← ψ]" 
proof -
  let ?ψ' = "embed ψ"
    and ?Π = "φ Ψ"
  let ?π' = "φ⇩P Ψ ?ψ'"
  let ?π = "concat ?π'"
  {
    have "SAS_Plus_Semantics.is_parallel_solution_for_problem Ψ ?ψ'"
      using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus[OF assms]
      by simp
    hence "STRIPS_Semantics.is_parallel_solution_for_problem ?Π ?π'"
      using strips_equivalent_to_sas_plus[OF assms(1)]
      by simp
  }
  moreover have "?π = [φ⇩O Ψ op. op ← ψ]"
    by simp
  moreover have "is_valid_problem_strips ?Π"
      using is_valid_problem_sas_plus_then_strips_transformation_too[OF assms(1)].
  moreover have "∀ops ∈ set ?π'. ∃op ∈ set ψ. ops = [φ⇩O Ψ op]" 
    using serial_sas_plus_equivalent_to_serial_strips_i[of _ Ψ ψ]
    by metis
  ultimately show ?thesis
    using STRIPS_Semantics.flattening_lemma[of ?Π]
    by metis
qed


lemma embedded_serial_strips_plan_operator_structure:
  assumes "ops' ∈ set (embed π)"
  obtains op 
    where "op ∈ set π" and "[φ⇩O¯ Π op. op ← ops'] = [φ⇩O¯ Π op]"
proof -
  let ?π' = "embed π" 
  {
    have "?π' = [[op]. op ← π]"
      by (induction π; force)
    moreover obtain op where "ops' = [op]" and "op ∈ set π" 
      using calculation assms 
      by fastforce
    ultimately have "∃op ∈ set π. [φ⇩O¯ Π op. op ← ops'] = [φ⇩O¯ Π op]"
      by auto
  }
  thus ?thesis 
    using that
    by meson
qed

private lemma serial_strips_equivalent_to_serial_sas_plus_i: 
  assumes "ops ∈ set (φ⇩P¯ Π (embed π))"
  obtains op where "op ∈ set π" and "ops = [φ⇩O¯ Π op]"  
proof -
  let ?π' = "embed π" 
  {
    have "set (φ⇩P¯ Π (embed π)) = { [φ⇩O¯ Π op. op ← ops]  | ops. ops ∈ set ?π' }"
      unfolding strips_parallel_plan_to_sas_plus_parallel_plan_def
        SAS_Plus_STRIPS.strips_parallel_plan_to_sas_plus_parallel_plan_def
        strips_op_to_sasp_def set_map
      using setcompr_eq_image 
      by blast
    moreover obtain ops' where "ops' ∈ set ?π'" and "ops = [φ⇩O¯ Π op. op ← ops']" 
      using assms(1) calculation
      by blast
    moreover obtain op where "op ∈ set π" and "ops = [φ⇩O¯ Π op]" 
      using embedded_serial_strips_plan_operator_structure calculation(2, 3)
      by blast
    ultimately have "∃op ∈ set π. ops = [φ⇩O¯ Π op]" 
      by meson
  }
  thus ?thesis 
    using that..
qed

private lemma serial_strips_equivalent_to_serial_sas_plus_ii[simp]:
  "concat (φ⇩P¯ Π (embed π)) = [φ⇩O¯ Π op. op ← π]" 
proof -
  let ?π' = "List_Supplement.embed π"
  have "concat (φ⇩P¯ Π ?π') = map (λop. φ⇩O¯ Π op) (concat ?π')" 
    unfolding strips_parallel_plan_to_sas_plus_parallel_plan_def
      SAS_Plus_STRIPS.strips_parallel_plan_to_sas_plus_parallel_plan_def
      strips_op_to_sasp_def
      SAS_Plus_STRIPS.strips_op_to_sasp_def Let_def
      map_concat 
    by simp
  also have "… = map (λop. φ⇩O¯ Π op) π" 
    unfolding concat_is_inverse_of_embed[of π]..
  finally show "concat (φ⇩P¯ Π (embed π)) = [φ⇩O¯ Π op. op ← π]".
qed

text ‹ Using the analogous lemmas for the opposite direction, we can show the counterpart to 
theorem \ref{isathm:equivalence-serial-sas-plus-serial-strips} which shows that serial solutions 
to STRIPS solutions can be transformed to serial SAS+ solutions via composition of embedding, 
transformation and flattening. ›

theorem 
  serial_strips_equivalent_to_serial_sas_plus:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "STRIPS_Semantics.is_serial_solution_for_problem (φ Ψ) π"
  shows "SAS_Plus_Semantics.is_serial_solution_for_problem Ψ [φ⇩O¯ Ψ op. op ← π]" 
proof -
  let ?π' = "embed π"
    and ?Π = "φ Ψ"
  let ?ψ' = "φ⇩P¯ Ψ ?π'"
  let ?ψ = "concat ?ψ'"
  {
    have "STRIPS_Semantics.is_parallel_solution_for_problem ?Π ?π'"
      using embedding_lemma[OF 
          is_valid_problem_sas_plus_then_strips_transformation_too[OF assms(1)] assms(2)].
    hence "SAS_Plus_Semantics.is_parallel_solution_for_problem Ψ ?ψ'"
      using sas_plus_equivalent_to_strips[OF assms(1)]
      by simp
  }
  moreover have "?ψ = [φ⇩O¯ Ψ op. op ← π]"
    by simp
  moreover have "is_valid_problem_strips ?Π"
      using is_valid_problem_sas_plus_then_strips_transformation_too[OF assms(1)].
  moreover have "∀ops ∈ set ?ψ'. ∃op ∈ set π. ops = [φ⇩O¯ Ψ op]" 
    using serial_strips_equivalent_to_serial_sas_plus_i
    by metis
  ultimately show ?thesis
    using flattening_lemma[OF assms(1)]
    by metis
qed

subsection "Equivalence of SAS+ and STRIPS" 

― ‹ Define the sets of plans with upper length bound as well as the sets of solutions with 
upper length bound for  SAS problems and induced STRIPS problems.

 We keep this polymorphic by not specifying concrete types so it applies to both STRIPS and 
SAS+ plans. ›
abbreviation bounded_plan_set 
  where "bounded_plan_set ops k ≡ { π. set π ⊆ set ops ∧ length π = k }"

definition bounded_solution_set_sas_plus' 
  :: "('variable, 'domain) sas_plus_problem 
    ⇒ nat
    ⇒ ('variable, 'domain) sas_plus_plan set" 
  where "bounded_solution_set_sas_plus' Ψ k 
    ≡ { ψ. is_serial_solution_for_problem Ψ ψ ∧ length ψ = k}"

abbreviation bounded_solution_set_sas_plus
  :: "('variable, 'domain) sas_plus_problem 
    ⇒ nat
    ⇒ ('variable, 'domain) sas_plus_plan set" 
  where "bounded_solution_set_sas_plus Ψ N 
    ≡ (⋃k ∈ {0..N}. bounded_solution_set_sas_plus' Ψ k)"

definition bounded_solution_set_strips'
  :: "('variable × 'domain) strips_problem 
    ⇒ nat
    ⇒ ('variable × 'domain) strips_plan set" 
  where "bounded_solution_set_strips' Π k
    ≡ { π. STRIPS_Semantics.is_serial_solution_for_problem Π π ∧ length π = k }"

abbreviation bounded_solution_set_strips
  :: "('variable × 'domain) strips_problem 
    ⇒ nat 
    ⇒ ('variable × 'domain) strips_plan set" 
  where "bounded_solution_set_strips Π N ≡ (⋃k ∈ {0..N}. bounded_solution_set_strips' Π k)"

― ‹ Show that plan transformation for all SAS Plus solutions yields a STRIPS solution for the
induced STRIPS problem with same length. 

We first show injectiveness of plan transformation ‹λψ. [φ⇩O Ψ op. op ← ψ]› on the set of plans 
‹P⇩k ≡ bounded_plan_set (operators_of Ψ) k› with length bound ‹k›. The injectiveness of 
‹Sol⇩k ≡ bounded_solution_set_sas_plus Ψ k›---the set of solutions with length bound ‹k›--then 
follows from the subset relation ‹Sol⇩k ⊆ P⇩k›. ›
lemma sasp_op_to_strips_injective:
  assumes "(φ⇩O Ψ op⇩1) = (φ⇩O Ψ op⇩2)"
  shows "op⇩1 = op⇩2" 
  proof  -
    let ?op⇩1' = "φ⇩O Ψ op⇩1" 
      and ?op⇩2' = "φ⇩O Ψ op⇩2" 
    {
      have "strips_operator.precondition_of ?op⇩1' = strips_operator.precondition_of ?op⇩2'"
        using assms 
        by argo
      hence "sas_plus_operator.precondition_of op⇩1 = sas_plus_operator.precondition_of op⇩2"
        unfolding sasp_op_to_strips_def
          SAS_Plus_STRIPS.sasp_op_to_strips_def
          Let_def 
        by simp
    }
    moreover {
      have "strips_operator.add_effects_of ?op⇩1' = strips_operator.add_effects_of ?op⇩2'"
        using assms 
        unfolding sasp_op_to_strips_def Let_def 
        by argo
      hence "sas_plus_operator.effect_of op⇩1 = sas_plus_operator.effect_of op⇩2"
        unfolding sasp_op_to_strips_def Let_def
          SAS_Plus_STRIPS.sasp_op_to_strips_def
        by simp
    }
    ultimately show ?thesis 
      by simp
  qed

lemma sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_i_a:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "inj_on (λψ. [φ⇩O Ψ op. op ← ψ]) (bounded_plan_set (sas_plus_problem.operators_of Ψ) k)" 
  proof -
    let ?ops = "sas_plus_problem.operators_of Ψ"
      (* TODO refactor transformation definitions *)
      and ?φ⇩P = "λψ. [φ⇩O Ψ op. op ← ψ]"
    let ?P = "bounded_plan_set ?ops"
    {
      fix ψ⇩1 ψ⇩2
      assume ψ⇩1_in: "ψ⇩1 ∈ ?P k" 
        and ψ⇩2_in: "ψ⇩2 ∈ ?P k" 
        and φ⇩P_of_ψ⇩1_is_φ⇩P_of_ψ⇩2: "(?φ⇩P ψ⇩1) = (?φ⇩P ψ⇩2)"
      hence "ψ⇩1 = ψ⇩2"
        proof (induction k arbitrary: ψ⇩1 ψ⇩2)
          case 0
          then have "length ψ⇩1 = 0" 
            and "length ψ⇩2 = 0" 
            using ψ⇩1_in ψ⇩2_in
            unfolding bounded_solution_set_sas_plus'_def 
            by blast+
          then show ?case 
            by blast
        next
          case (Suc k)
          moreover have "length ψ⇩1 = Suc k" and "length ψ⇩2 = Suc k"
            using length_Suc_conv Suc(2, 3) 
            unfolding bounded_solution_set_sas_plus'_def
            by blast+
          moreover obtain op⇩1 ψ⇩1' where "ψ⇩1 = op⇩1 # ψ⇩1'" 
            and "set (op⇩1 # ψ⇩1') ⊆ set ?ops"
            and "length ψ⇩1' = k" 
            using calculation(5) Suc(2)
            unfolding length_Suc_conv
            by blast
          moreover obtain op⇩2 ψ⇩2' where "ψ⇩2 = op⇩2 # ψ⇩2'" 
            and "set (op⇩2 # ψ⇩2') ⊆ set ?ops" 
            and "length ψ⇩2' = k"
            using calculation(6) Suc(3)
            unfolding length_Suc_conv
            by blast
          moreover have "set ψ⇩1' ⊆ set ?ops" and "set ψ⇩2' ⊆ set ?ops" 
            using calculation(8, 11) 
            by auto+
          moreover have "ψ⇩1' ∈ ?P k" and "ψ⇩2' ∈ ?P k"
            using calculation(9, 12, 13, 14)
            by fast+
          moreover have "?φ⇩P ψ⇩1' = ?φ⇩P ψ⇩2'" 
            using Suc.prems(3) calculation(7, 10) 
            by fastforce
          moreover have "ψ⇩1' = ψ⇩2'" 
            using Suc.IH[of ψ⇩1' ψ⇩2', OF calculation(15, 16, 17)]
            by simp
          moreover have "?φ⇩P ψ⇩1 = (φ⇩O Ψ op⇩1) # ?φ⇩P ψ⇩1'" 
            and "?φ⇩P ψ⇩2 = (φ⇩O Ψ op⇩2) # ?φ⇩P ψ⇩2'"
            using Suc.prems(3) calculation(7, 10) 
            by fastforce+
          moreover have "(φ⇩O Ψ op⇩1) = (φ⇩O Ψ op⇩2)" 
            using Suc.prems(3) calculation(17, 19, 20)
            by simp
          moreover have "op⇩1 = op⇩2" 
            using sasp_op_to_strips_injective[OF calculation(21)].
          ultimately show ?case 
            by argo
        qed
    }
    thus ?thesis 
      unfolding inj_on_def 
      by blast
  qed

private corollary sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_i_b:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "inj_on (λψ. [φ⇩O Ψ op. op ← ψ]) (bounded_solution_set_sas_plus' Ψ k)"
  proof -
    let ?ops = "sas_plus_problem.operators_of Ψ"
      and ?φ⇩P = "λψ. [φ⇩O Ψ op. op ← ψ]"
    {
      fix ψ
      assume "ψ ∈ bounded_solution_set_sas_plus' Ψ k" 
      then have "set ψ ⊆ set ?ops" 
        and "length ψ = k" 
        unfolding bounded_solution_set_sas_plus'_def is_serial_solution_for_problem_def Let_def 
          list_all_iff ListMem_iff 
        by fast+
      hence "ψ ∈ bounded_plan_set ?ops k" 
         by blast
    }
    hence "bounded_solution_set_sas_plus' Ψ k ⊆ bounded_plan_set ?ops k" 
      by blast
    moreover have "inj_on ?φ⇩P (bounded_plan_set ?ops k)" 
      using sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_i_a[OF assms(1)].
    ultimately show ?thesis
      using inj_on_subset[of ?φ⇩P "bounded_plan_set ?ops k" "bounded_solution_set_sas_plus' Ψ k"]
      by fast
  qed

(*
lemma "card ((λψ. [φ⇩O Ψ op. op ← ψ]) ` (bounded_solution_set_sas_plus' Ψ k)) 
  = card (bounded_solution_set_strips' (φ Ψ) k)"  sorry
*)

― ‹ Show that mapping plan transformation ‹λψ. [φ⇩O Ψ op. op ← ψ]› over the solution set for a 
given SAS+ problem yields the solution set for the induced STRIPS problem. ›
private lemma sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_i_c:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "(λψ. [φ⇩O Ψ op. op ← ψ]) ` (bounded_solution_set_sas_plus' Ψ k) 
    = bounded_solution_set_strips' (φ Ψ) k" 
 proof -
   let ?Π = "φ Ψ"
     and ?φ⇩P = "λψ. [φ⇩O Ψ op. op ← ψ]"
   let ?Sol⇩k = "bounded_solution_set_sas_plus' Ψ k"
    and ?Sol⇩k' = "bounded_solution_set_strips' ?Π k"
   {
     assume "?φ⇩P ` ?Sol⇩k ≠ ?Sol⇩k'" 
     then consider (A) "∃π ∈ ?φ⇩P ` ?Sol⇩k. π ∉ ?Sol⇩k'"
       | (B) "∃π ∈ ?Sol⇩k'. π ∉  ?φ⇩P ` ?Sol⇩k"
       by blast
     hence False 
       proof (cases)
         case A
         moreover obtain π where "π ∈ ?φ⇩P ` ?Sol⇩k" and "π ∉ ?Sol⇩k'"
           using calculation
           by blast
         moreover obtain ψ where "length ψ = k" 
           and "SAS_Plus_Semantics.is_serial_solution_for_problem Ψ ψ" 
           and "π = ?φ⇩P ψ" 
           using calculation(2)
           unfolding bounded_solution_set_sas_plus'_def 
           by blast
         moreover have "length π = k" and "STRIPS_Semantics.is_serial_solution_for_problem ?Π π"
           subgoal 
             using calculation(4, 6) by auto
           subgoal
             using serial_sas_plus_equivalent_to_serial_strips
               assms(1) calculation(5) calculation(6) 
             by blast
           done
         moreover have "π ∈ ?Sol⇩k'" 
           unfolding bounded_solution_set_strips'_def 
           using calculation(7, 8) 
           by simp
         ultimately show ?thesis
           by fast
       next
         case B
         moreover obtain π where "π ∈ ?Sol⇩k'" and "π ∉ ?φ⇩P ` ?Sol⇩k"
           using calculation
           by blast
         moreover have "STRIPS_Semantics.is_serial_solution_for_problem ?Π π"
           and "length π = k"
           using calculation(2)
           unfolding bounded_solution_set_strips'_def 
           by simp+
         ― ‹ Construct the counter example ‹ψ ≡ [φ⇩O¯ ?Π op. op ← π]› and show that ‹ψ ∈ ?Sol⇩k›
            as well as ‹?φ⇩P ψ = π› hence ‹π ∈ ?φ⇩P ` ?Sol⇩k›. ›
         moreover have "length [φ⇩O¯ Ψ op. op ← π] = k"
           and "SAS_Plus_Semantics.is_serial_solution_for_problem Ψ [φ⇩O¯ Ψ op. op ← π]" 
           subgoal 
             using calculation(5) 
             by simp
           subgoal 
             using serial_strips_equivalent_to_serial_sas_plus[OF assms(1)] 
               calculation(4)
             by simp
           done
         moreover have "[φ⇩O¯ Ψ op. op ← π] ∈ ?Sol⇩k" 
           unfolding bounded_solution_set_sas_plus'_def 
           using calculation(6, 7) 
           by blast
         (* TODO refactor transformation lemmas *)
         moreover {
           have "∀op ∈ set π. op ∈ set ((?Π)⇩𝒪)"
             using calculation(4)
             unfolding STRIPS_Semantics.is_serial_solution_for_problem_def list_all_iff ListMem_iff
             by simp
           hence "?φ⇩P [φ⇩O¯ Ψ op. op ← π] = π" 
             proof (induction π)
               case (Cons op π)
               moreover have "?φ⇩P [φ⇩O¯ Ψ op. op ← op # π] 
                = (φ⇩O Ψ (φ⇩O¯ Ψ op)) # ?φ⇩P [φ⇩O¯ Ψ op. op ← π]"
                 by simp
               moreover have "op ∈  set ((?Π)⇩𝒪)" 
                 using Cons.prems
                 by simp
               moreover have "(φ⇩O Ψ (φ⇩O¯ Ψ op)) = op"
                 using strips_operator_inverse_is[OF assms(1) calculation(4)].
               moreover have "?φ⇩P [φ⇩O¯ Ψ op. op ← π] = π" 
                 using Cons.IH Cons.prems 
                 by auto
               ultimately show ?case 
                 by argo
             qed simp
         }
         moreover have "π ∈ ?φ⇩P ` ?Sol⇩k" 
           using calculation(8, 9) 
           by force
         ultimately show ?thesis
           by blast
      qed
   }
   thus ?thesis 
     by blast
  qed

private lemma sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_i_d:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "card (bounded_solution_set_sas_plus' Ψ k) ≤ card (bounded_solution_set_strips' (φ Ψ) k)"
  proof -
    let ?Π = "φ Ψ"
      and ?φ⇩P = "λψ. [φ⇩O Ψ op. op ← ψ]"
    let ?Sol⇩k = "bounded_solution_set_sas_plus' Ψ k"
      and ?Sol⇩k' = "bounded_solution_set_strips' ?Π k"
    have "card (?φ⇩P ` ?Sol⇩k) = card (?Sol⇩k)"
     using sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_i_b[OF assms(1)] 
       card_image 
     by blast
    moreover have "?φ⇩P ` ?Sol⇩k = ?Sol⇩k'"
     using sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_i_c[OF assms(1)].
    ultimately show ?thesis 
     by simp
  qed

― ‹ The set of fixed length plans with operators in a given operator set is finite. ›
lemma bounded_plan_set_finite:
  shows "finite { π. set π ⊆ set ops ∧ length π = k }"
  proof (induction k)
    case (Suc k)
    let ?P = "{ π. set π ⊆ set ops ∧ length π = k }"
      and ?P' = "{ π. set π ⊆ set ops ∧ length π = Suc k }"  
    let ?P'' = "(⋃op ∈ set ops. (⋃π ∈ ?P. { op # π }))" 
    {
      have "∀op π. finite { op # π }"
        by simp
      then have "∀op. finite (⋃π ∈ ?P. { op # π })" 
        using finite_UN[of ?P] Suc 
        by blast
      hence "finite ?P''" 
        using finite_UN[of "set ops"]
        by blast
    }
    moreover {
      {
        fix π
        assume "π ∈ ?P'"
        moreover have "set π ⊆ set ops" 
          and "length π = Suc k" 
          using calculation 
          by simp+
        moreover obtain op π' where "π = op # π'" 
          using calculation (3)
          unfolding length_Suc_conv 
          by fast
        moreover have "set π' ⊆ set ops" and "op ∈ set ops"
          using calculation(2, 4) 
          by simp+
        moreover have "length π' = k"
          using calculation(3, 4) 
          by auto
        moreover have "π' ∈ ?P" 
          using calculation(5, 7)
          by blast
        ultimately have "π ∈ ?P''"
          by blast
      }
      hence "?P' ⊆ ?P''"
        by blast
    }
    ultimately show ?case 
      using rev_finite_subset[of ?P'' ?P']
      by blast
  qed force

― ‹ The set of fixed length SAS+ solutions are subsets of the set of plans with fixed length and 
therefore also finite. ›
private lemma sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_ii_a:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "finite (bounded_solution_set_sas_plus' Ψ k)"
proof -
  let ?Ops = "set ((Ψ)⇩𝒪⇩+)"
  let ?Sol⇩k = "bounded_solution_set_sas_plus' Ψ k"
    and ?P⇩k = "{ π. set π ⊆ ?Ops ∧ length π = k }"
  {
    fix ψ
    assume "ψ ∈ ?Sol⇩k"
    then have "length ψ = k" and "set ψ ⊆ ?Ops"
      unfolding bounded_solution_set_sas_plus'_def 
        SAS_Plus_Semantics.is_serial_solution_for_problem_def Let_def list_all_iff ListMem_iff
      by fastforce+
    hence "ψ ∈ ?P⇩k" 
      by blast
  }
  then have "?Sol⇩k ⊆ ?P⇩k" 
    by force
  thus ?thesis
    using bounded_plan_set_finite rev_finite_subset[of ?P⇩k ?Sol⇩k]
    by auto
qed

― ‹ The set of fixed length STRIPS solutions are subsets of the set of plans with fixed length and 
therefore also finite. ›
private lemma sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_ii_b:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "finite (bounded_solution_set_strips' (φ Ψ) k)"
proof -
  let ?Π = "φ Ψ"
  let ?Ops = "set ((?Π)⇩𝒪)"
  let ?Sol⇩k = "bounded_solution_set_strips' ?Π k"
    and ?P⇩k = "{ π. set π ⊆ ?Ops ∧ length π = k }"
  {
    fix π
    assume "π ∈ ?Sol⇩k"
    then have "length π = k" and "set π ⊆ ?Ops"
      unfolding bounded_solution_set_strips'_def 
        STRIPS_Semantics.is_serial_solution_for_problem_def Let_def list_all_iff ListMem_iff
      by fastforce+
    hence "π ∈ ?P⇩k" 
      by blast
  }
  then have "?Sol⇩k ⊆ ?P⇩k" 
    by force
  thus ?thesis
    using bounded_plan_set_finite rev_finite_subset[of ?P⇩k ?Sol⇩k] 
    unfolding state_to_strips_state_def
      SAS_Plus_STRIPS.state_to_strips_state_def operators_of_def
    by blast
qed

text ‹ With the results on the equivalence of SAS+ and STRIPS solutions, we can now show that given 
problems in both formalisms, the solution sets have the same size.
This is the property required by the definition of planning formalism equivalence presented earlier 
in theorem \ref{thm:solution-sets-sas-plus-strips-f} (\autoref{sub:equivalence-sas-plus-strips}) and 
thus end up with the desired equivalence result.

The proof uses the finiteness and disjunctiveness of the solution sets for either problem to be 
able to equivalently transform the set cardinality over the union of sets of solutions with bounded 
lengths into a sum over the cardinality of the sets of solutions with bounded length. Moreover, 
since we know that for each SAS+ solution with a given length an equivalent STRIPS solution exists 
in the solution set of the transformed problem with the same length, both sets must have the same 
cardinality. 

Hence the cardinality of the  SAS+ solution set over all lengths up to a given upper bound \<^term>‹N› 
has the same size as the solution set of the corresponding STRIPS problem over all length up to a 
given upper bound \<^term>‹N›. ›

theorem
  assumes "is_valid_problem_sas_plus Ψ"
  shows "card (bounded_solution_set_sas_plus Ψ N) 
    = card (bounded_solution_set_strips (φ Ψ) N)" 
  proof -
    let ?Π = "φ Ψ"
      and ?R = "{0..N}" 
    ― ‹ Due to the disjoint nature of the bounded solution sets for fixed plan length for different 
    lengths, we can sum the individual set cardinality to obtain the cardinality of the overall SAS+ 
    resp. STRIPS solution sets. ›
    have finite_R: "finite ?R" 
      by simp
    moreover {
      have "∀k ∈ ?R. finite (bounded_solution_set_sas_plus' Ψ k)" 
        using sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_ii_a[OF 
            assms(1)]..
      moreover have "∀j ∈ ?R. ∀k ∈ ?R. j ≠ k 
        ⟶ bounded_solution_set_sas_plus' Ψ j 
          ∩ bounded_solution_set_sas_plus' Ψ k = {}"
        unfolding bounded_solution_set_sas_plus'_def 
        by blast
      (* TODO slow. *)
      ultimately have "card (bounded_solution_set_sas_plus Ψ N)
        = (∑k ∈ ?R. card (bounded_solution_set_sas_plus' Ψ k))"
        using card_UN_disjoint 
        by blast
    }
    moreover {
      have "∀k ∈ ?R. finite (bounded_solution_set_strips' ?Π k)" 
        using sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_ii_b[OF 
            assms(1)]..
      moreover have "∀j ∈ ?R. ∀k ∈ ?R. j ≠ k 
        ⟶ bounded_solution_set_strips' ?Π j 
          ∩ bounded_solution_set_strips' ?Π k = {}"
        unfolding bounded_solution_set_strips'_def
        by blast
      (* TODO slow. *)
      ultimately have "card (bounded_solution_set_strips ?Π N)
        = (∑k ∈ ?R. card (bounded_solution_set_strips' ?Π k))"
        using card_UN_disjoint
        by blast
    }
    moreover {
      fix k
      have "card (bounded_solution_set_sas_plus' Ψ k)
        = card ((λψ. [φ⇩O Ψ op. op ← ψ]) 
          ` bounded_solution_set_sas_plus' Ψ k)"
        using sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_i_b[OF assms]
          card_image[symmetric] 
        by blast
      hence "card (bounded_solution_set_sas_plus' Ψ k)
        = card (bounded_solution_set_strips' ?Π k)" 
        using sas_plus_formalism_and_induced_strips_formalism_are_equally_expressive_i_c[OF assms]
        by presburger
    } 
    ultimately show ?thesis
      by presburger
  qed


end

end