Theory SAT_Plan_Base

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory SAT_Plan_Base
  imports  "List-Index.List_Index"
    "Propositional_Proof_Systems.Formulas"
    "STRIPS_Semantics"
    "Map_Supplement" "List_Supplement"
    "CNF_Semantics_Supplement" "CNF_Supplement"
begin

― ‹ Hide constant and notation for \isaname{Orderings.bot_class.bot} (‹⊥›) to prevent warnings. ›
hide_const (open) Orderings.bot_class.bot
no_notation Orderings.bot_class.bot ("⊥")

― ‹ Hide constant and notation for \isaname{Transitive_Closure.trancl} (‹(_⇧+)›) to prevent
warnings. ›
hide_const (open) Transitive_Closure.trancl
no_notation Transitive_Closure.trancl ("(_⇧+)" [1000] 999)

― ‹ Hide constant and notation for \isaname{Relation.converse} (‹(_⇧+)›) to prevent
warnings. ›
hide_const (open) Relation.converse
no_notation Relation.converse  ("(_¯)" [1000] 999)

section "The Basic SATPlan Encoding"
text ‹ We now move on to the formalization of the basic SATPlan encoding (see
\autoref{def:basic-sat-plan-encoding-strips-problem}).

The two major results that we will obtain here are the soundness and completeness result outlined
in \autoref{thm:soundness-and-completeness-satplan-base} in
\autoref{sub:soundness-completeness-satplan}.

Let in the following ‹Φ ≡ encode_to_sat Π t› denote the SATPlan encoding for a STRIPS problem ‹Π›
and makespan ‹t›. Let \<^term>‹k < t› and ‹I ≡ (Π)⇩I› be the initial state of ‹Π›, ‹G ≡ (Π)⇩G› be
its goal state, ‹𝒱 ≡ (Π)⇩𝒱› its variable set, and ‹𝒪 ≡ (Π)⇩𝒪› its operator set. ›
subsection "Encoding Function Definitions"
text ‹ Since the SATPlan encoding uses propositional variables for both operators and state
variables of the problem as well as time points, we define a datatype using separate constructors
---\<^term>‹State k n› for state variables resp. \<^term>‹Operator k n› for operator activation---to
facilitate case distinction.
The natural number values store the time index resp. the indexes of the variable or operator
within their lists in the problem representation.
% TODO Note on why formulas are used instead of CNF (simple representation and good basis; e.g.
% export to cnf lists using CNF_Formulas.cnf_lists) ›

datatype  sat_plan_variable =
  State nat nat
  | Operator nat nat

text ‹ A SATPlan formula is a regular propositional formula over SATPlan variables. We add a type
synonym to improve readability. ›

type_synonym  sat_plan_formula = "sat_plan_variable formula"

text ‹ We now continue with the concrete definitions used in the implementation of the SATPlan
encoding.  State variables are encoded as literals over SATPlan variables using the ‹State›
constructor of \isaname{sat_plan_variable}. ›

definition  encode_state_variable
  :: "nat ⇒ nat ⇒ bool option ⇒ sat_plan_variable formula"
  where "encode_state_variable t k v ≡ case v of
    Some True ⇒ Atom (State t k)
    | Some False ⇒ ❙¬ (Atom (State t k))"

text ‹ The initial state encoding (definition \ref{isadef:initial-state-encoding}) is a conjunction
of state variable encodings \<^term>‹A ≡ encode_state_variable 0 n b› with ‹n ≡ index vs v› and
\<^term>‹b ≡ I v = Some True› for all \<^term>‹v ∈ 𝒱›. As we can see below, the same function but
substituting the initial state with the goal state and zero with the makespan \<^term>‹t› produces the
goal state encoding (\ref{isadef:goal-state-encoding}).
Note that both functions construct a conjunction of clauses ‹A ❙∨ ⊥› for which it
is easy to show that we can normalize to conjunctive normal form (CNF). ›

definition  encode_initial_state
  :: "'variable strips_problem ⇒ sat_plan_variable formula" ("Φ⇩I _" 99)
  where "encode_initial_state Π
    ≡ let I = initial_of Π
        ; vs = variables_of Π
      in ❙⋀(map (λv. encode_state_variable 0 (index vs v) (I v) ❙∨ ⊥)
    (filter (λv. I v ≠ None) vs))"

definition  encode_goal_state
  :: "'variable strips_problem ⇒ nat ⇒ sat_plan_variable formula" ("Φ⇩G _" 99)
  where "encode_goal_state Π t
    ≡ let
      vs = variables_of Π
      ; G = goal_of Π
    in ❙⋀(map (λv. encode_state_variable t (index vs v) (G v) ❙∨ ⊥)
      (filter (λv. G v ≠ None) vs))"

text ‹ Operator preconditions are encoded using activation-implies-precondition formulation as
mentioned in \autoref{subsub:basic-sat-plan-encoding}: i.e. for each
operator \<^term>‹op ∈ 𝒪› and \<^term>‹p ∈ set (precondition_of op)› we have to encode
  @{text[display, indent=4] "Atom (Operator k (index ops op)) ❙→ Atom (State k (index vs v))"}
We use the equivalent disjunction in the formalization to simplify conversion to CNF.

›

definition encode_operator_precondition
  :: "'variable strips_problem
    ⇒ nat
    ⇒ 'variable strips_operator
    ⇒ sat_plan_variable formula"
  where "encode_operator_precondition Π t op ≡ let
      vs = variables_of Π
      ; ops = operators_of Π
    in ❙⋀(map (λv.
        ❙¬ (Atom (Operator t (index ops op))) ❙∨ Atom (State t (index vs v)))
      (precondition_of op))"

definition  encode_all_operator_preconditions
  :: "'variable strips_problem
    ⇒ 'variable strips_operator list
    ⇒ nat
    ⇒ sat_plan_variable formula"
  where "encode_all_operator_preconditions Π ops t ≡ let
      l = List.product [0..<t] ops
    in foldr (❙∧) (map (λ(t, op). encode_operator_precondition Π t op) l) (❙¬⊥)"

text ‹ Analogously to the operator precondition, add and delete effects of operators have to be
implied by operator activation. That being said, we have to encode both positive and negative
effects and the effect must be active at the following time point: i.e.
  @{text[display, indent=4] "Atom (Operator k m) ❙→ Atom (State (Suc k) n)"}
for add effects respectively
  @{text[display, indent=4] "Atom (Operator k m) ❙→ ❙¬Atom (State (Suc k) n)"}
for delete effects. We again encode the implications as their equivalent disjunctions in
definition \ref{isadef:operator-effect-encoding}. ›

definition  encode_operator_effect
  :: "'variable strips_problem
    ⇒ nat
    ⇒ 'variable strips_operator
    ⇒ sat_plan_variable formula"
  where "encode_operator_effect Π t op
    ≡ let
        vs = variables_of Π
        ; ops = operators_of Π
      in ❙⋀(map (λv.
              ❙¬(Atom (Operator t (index ops op)))
              ❙∨ Atom (State (Suc t) (index vs v)))
            (add_effects_of op)
          @ map (λv.
              ❙¬(Atom (Operator t (index ops op)))
               ❙∨ ❙¬ (Atom (State (Suc t) (index vs v))))
            (delete_effects_of op))"

definition encode_all_operator_effects
  :: "'variable strips_problem
    ⇒ 'variable strips_operator list
    ⇒ nat
    ⇒ sat_plan_variable formula"
  where "encode_all_operator_effects Π ops t
    ≡ let l = List.product [0..<t] ops
      in foldr (❙∧) (map (λ(t, op). encode_operator_effect Π t op) l) (❙¬⊥)"

definition encode_operators
  :: "'variable strips_problem ⇒ nat ⇒ sat_plan_variable formula"
  where "encode_operators Π t
    ≡ let ops = operators_of Π
      in encode_all_operator_preconditions Π ops t ❙∧ encode_all_operator_effects Π ops t"

text ‹

Definitions \ref{isadef:negative-transition-frame-axiom-encoding} and
\ref{isadef:positive-transition-frame-axiom-encoding} similarly encode the negative resp. positive
transition frame axioms as disjunctions.  ›

definition  encode_negative_transition_frame_axiom
  :: "'variable strips_problem
    ⇒ nat
    ⇒ 'variable
    ⇒ sat_plan_variable formula"
  where "encode_negative_transition_frame_axiom Π t v
    ≡ let vs = variables_of Π
        ; ops = operators_of Π
        ; deleting_operators = filter (λop. ListMem v (delete_effects_of op)) ops
      in ❙¬(Atom (State t (index vs v)))
          ❙∨ (Atom (State (Suc t) (index vs v))
          ❙∨ ❙⋁ (map (λop. Atom (Operator t (index ops op))) deleting_operators))"

definition  encode_positive_transition_frame_axiom
  :: "'variable strips_problem
    ⇒ nat
    ⇒ 'variable
    ⇒ sat_plan_variable formula"
  where "encode_positive_transition_frame_axiom Π t v
    ≡ let vs = variables_of Π
        ; ops = operators_of Π
        ; adding_operators = filter (λop. ListMem v (add_effects_of op)) ops
      in (Atom (State t (index vs v))
          ❙∨ (❙¬(Atom (State (Suc t) (index vs v)))
          ❙∨ ❙⋁(map (λop. Atom (Operator t (index ops op))) adding_operators)))"

definition encode_all_frame_axioms
  :: "'variable strips_problem ⇒ nat ⇒ sat_plan_variable formula"
  where "encode_all_frame_axioms Π t
    ≡ let l = List.product [0..<t] (variables_of Π)
      in ❙⋀(map (λ(k, v). encode_negative_transition_frame_axiom Π k v) l
            @ map (λ(k, v). encode_positive_transition_frame_axiom Π k v) l)"

text ‹ Finally, the basic SATPlan encoding is the
conjunction of the initial state, goal state, operator and frame axiom encoding for all time steps.
The functions \isaname{encode_operators} and \isaname{encode_all_frame_axioms}\footnote{Not shown.}
take care of mapping the operator precondition, effect and frame axiom encoding over all possible
combinations of time point and operators resp. time points, variables, and operators. ›

definition  encode_problem ("Φ _ _" 99)
  where "encode_problem Π t
    ≡ encode_initial_state Π
      ❙∧ (encode_operators Π t
      ❙∧ (encode_all_frame_axioms Π t
      ❙∧ (encode_goal_state Π t)))"

subsection "Decoding Function Definitions"
text ‹ Decoding plans from a valuation \<^term>‹𝒜› of a
SATPlan encoding entails extracting all activated operators for all
time points except the last one. We implement this by mapping over all \<^term>‹k < t›
 and extracting activated operators---i.e. operators for which the model valuates the respective
operator encoding at time \<^term>‹k› to true---into a parallel operator (see definition
\ref{isadef:satplan-plan-decoding}).
\footnote{This is handled by function \texttt{decode\_plan'} (not shown).} ›

― ‹ Note that due to the implementation based on lists, we have to address the problem of duplicate
operator declarations in the operator list of the problem. Since \<^term>‹index op = index op'› for equal
operators, the parallel operator obtained from \isaname{decode_plan'} will contain
duplicates in case the problem's operator list does. We therefore remove duplicates first using
\<^term>‹remdups ops› and then filter out activated operators. ›
definition decode_plan'
  :: "'variable strips_problem
    ⇒ sat_plan_variable valuation
    ⇒ nat
    ⇒ 'variable strips_operator list"
  where "decode_plan' Π 𝒜 i
    ≡ let ops = operators_of Π
        ; vs = map (λop. Operator i (index ops op)) (remdups ops)
      in map (λv. case v of Operator _ k ⇒ ops ! k) (filter 𝒜 vs)"


― ‹ We decode maps over range ‹0, …, t - 1› because the last operator takes effect in \<^term>‹t› and
must therefore have been applied in step \<^term>‹t - 1›. ›

definition  decode_plan
  :: "'variable strips_problem
    ⇒ sat_plan_variable valuation
    ⇒ nat
    ⇒ 'variable strips_parallel_plan" ("Φ¯ _ _ _" 99)
  where "decode_plan Π 𝒜 t ≡ map (decode_plan' Π 𝒜) [0..<t]"

text ‹ Similarly to the operator decoding, we can decode a state at time \<^term>‹k› from a valuation
of of the SATPlan encoding \<^term>‹𝒜› by constructing a map from list of assignments
\<^term>‹(v, 𝒜 (State k (index vs v)))› for all \<^term>‹v ∈ 𝒱›. ›

definition  decode_state_at
  :: "'variable strips_problem
    ⇒ sat_plan_variable valuation
    ⇒ nat
    ⇒ 'variable strips_state" ("Φ⇩S¯ _ _ _" 99)
  where "decode_state_at Π 𝒜 k
    ≡ let
      vs = variables_of Π
      ; state_encoding_to_assignment = λv. (v, 𝒜 (State k (index vs v)))
    in map_of (map state_encoding_to_assignment vs)"

text ‹ We continue by setting up the \isaname{sat_plan} context for the proofs of soundness and
completeness. ›

definition encode_transitions ::"'variable strips_problem ⇒ nat ⇒ sat_plan_variable formula" ("Φ⇩T _ _" 99) where
  "encode_transitions Π t
      ≡ SAT_Plan_Base.encode_operators Π t ❙∧
        SAT_Plan_Base.encode_all_frame_axioms Π t"

― ‹ Immediately proof the sublocale proposition for strips in order to gain access to definitions
and lemmas. ›

― ‹ Setup simp rules. ›
lemma   [simp]:
  "encode_transitions Π t
    = SAT_Plan_Base.encode_operators Π t ❙∧
      SAT_Plan_Base.encode_all_frame_axioms Π t"
  unfolding encode_problem_def encode_initial_state_def encode_transitions_def
    encode_goal_state_def decode_plan_def decode_state_at_def
  by simp+

context
begin

lemma encode_state_variable_is_lit_plus_if:
  assumes "is_valid_problem_strips Π"
    and "v ∈ dom s"
  shows "is_lit_plus (encode_state_variable k (index (strips_problem.variables_of Π) v) (s v))"
proof -
  have "s v ≠ None"
    using is_valid_problem_strips_initial_of_dom assms(2)
    by blast
  then consider (s_of_v_is_some_true) "s v = Some True"
    | (s_of_v_is_some_false) "s v = Some False"
    by fastforce
  thus ?thesis
    unfolding encode_state_variable_def
    by (cases, simp+)
qed

lemma is_cnf_encode_initial_state:
  assumes "is_valid_problem_strips Π"
  shows "is_cnf (Φ⇩I Π)"
proof -
  let ?I = "(Π)⇩I"
    and ?vs = "strips_problem.variables_of Π"
  let ?l = "map (λv. encode_state_variable 0 (index ?vs v) (?I v) ❙∨ ⊥)
    (filter (λv. ?I v ≠ None) ?vs)"
  {
    fix C
    assume c_in_set_l:"C ∈ set ?l"
    have "set ?l = (λv. encode_state_variable 0 (index ?vs v) (?I v) ❙∨ ⊥) `
      set (filter (λv. ?I v ≠ None) ?vs)"
      using set_map[of "λv. encode_state_variable 0 (index ?vs v) (?I v) ❙∨ ⊥"
          "filter (λv. ?I v ≠ None) ?vs"]
      by blast
    then have "set ?l = (λv. encode_state_variable 0 (index ?vs v) (?I v) ❙∨ ⊥) `
      {v ∈ set ?vs. ?I v ≠ None}"
      using set_filter[of "λv. ?I v ≠ None" ?vs]
      by argo
    then obtain v
      where c_is: "C = encode_state_variable 0 (index ?vs v) (?I v) ❙∨ ⊥"
      and v_in_set_vs: "v ∈ set ?vs"
      and I_of_v_is_not_None: "?I v ≠ None"
      using c_in_set_l
      by auto
    (* TODO refactor. *)
    {
      have "v ∈ dom ?I"
        using I_of_v_is_not_None
        by blast
      moreover have "is_lit_plus (encode_state_variable 0 (index ?vs v) (?I v))"
        using encode_state_variable_is_lit_plus_if[OF _ calculation] assms(1)
        by blast
      moreover have "is_lit_plus ⊥"
        by simp
      ultimately have "is_disj C"
        using c_is
        by force
    }
    hence "is_cnf C"
      unfolding encode_state_variable_def
      using c_is
      by fastforce
  }
  thus ?thesis
    unfolding encode_initial_state_def SAT_Plan_Base.encode_initial_state_def Let_def initial_of_def
    using is_cnf_BigAnd[of ?l]
      by (smt is_cnf_BigAnd)
qed

lemma encode_goal_state_is_cnf:
  assumes "is_valid_problem_strips Π"
  shows "is_cnf (encode_goal_state Π t)"
proof -
  let ?I = "(Π)⇩I"
    and ?G = "(Π)⇩G"
    and ?vs = "strips_problem.variables_of Π"
  let ?l = "map (λv. encode_state_variable t (index ?vs v) (?G v) ❙∨ ⊥)
      (filter (λv. ?G v ≠ None) ?vs)"
  {
    fix C
    assume "C ∈ set ?l"
    (* TODO refactor (lemma ‹encode_goal_state_is_cnf_i›) *)
    moreover {
      have "set ?l = (λv. encode_state_variable t (index ?vs v) (?G v) ❙∨ ⊥)
        ` set (filter (λv. ?G v ≠ None) ?vs)"
        unfolding set_map
        by blast
      then have "set ?l = { encode_state_variable t (index ?vs v) (?G v) ❙∨ ⊥
        | v. v ∈ set ?vs ∧ ?G v ≠ None }"
        by auto
    }
    moreover obtain v where C_is: "C = encode_state_variable t (index ?vs v) (?G v) ❙∨ ⊥ "
      and "v ∈ set ?vs"
      and G_of_v_is_not_None: "?G v ≠ None"
      using calculation(1)
      by auto
    (* TODO refactor. *)
    moreover {
      have "v ∈ dom ?G"
        using G_of_v_is_not_None
        by blast
      moreover have "is_lit_plus (encode_state_variable t (index ?vs v) (?G v))"
        using assms(1) calculation
        by (simp add: encode_state_variable_is_lit_plus_if)
      moreover have "is_lit_plus ⊥"
        by simp
      ultimately have "is_disj C"
        unfolding C_is
        by force
    }
    ultimately have "is_cnf C"
      by simp
  }
  thus ?thesis
    unfolding encode_goal_state_def SAT_Plan_Base.encode_goal_state_def Let_def
    using is_cnf_BigAnd[of ?l]
    by simp
qed

private lemma encode_operator_precondition_is_cnf:
  "is_cnf (encode_operator_precondition Π k op)"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
  let ?l = "map (λv. ❙¬ (Atom (Operator k (index ?ops op))) ❙∨ Atom (State k (index ?vs v)))
    (precondition_of op)"
  {
    have "set ?l = (λv. ❙¬(Atom (Operator k (index ?ops op))) ❙∨ Atom (State k (index ?vs v)))
      ` set (precondition_of op)"
      using set_map
      by force
    then have "set ?l = { ❙¬(Atom (Operator k (index ?ops op))) ❙∨ Atom (State k (index ?vs v))
      | v. v ∈ set (precondition_of op) }"
      using setcompr_eq_image[of
        "λv. ❙¬(Atom (Operator k (index ?ops op))) ❙∨ Atom (State k (index ?vs v))"
        "λv. v ∈ set (precondition_of op)"]
      by simp
  } note set_l_is = this
  {
    fix C
    assume "C ∈ set ?l"
    then obtain v
      where "v ∈ set (precondition_of op)"
      and "C = ❙¬(Atom (Operator k (index ?ops op))) ❙∨ Atom (State k (index ?vs v))"
      using set_l_is
      by blast
    hence "is_cnf C"
      by simp
  }
  thus ?thesis
    unfolding encode_operator_precondition_def
    using is_cnf_BigAnd[of ?l]
    by meson
qed

private lemma set_map_operator_precondition[simp]:
  "set (map (λ(k, op). encode_operator_precondition Π k op) (List.product [0..<t] ops))
    = { encode_operator_precondition Π k op | k op. (k, op) ∈ ({0..<t} × set ops) }"
proof -
  let ?l' = "List.product [0..<t] ops"
  let ?fs = "map (λ(k, op). encode_operator_precondition Π k op) ?l'"
  have set_l'_is: "set ?l' = {0..<t} × set ops"
    by simp
  moreover {
    have "set ?fs = (λ(k, op). encode_operator_precondition Π k op)
      ` ({0..<t} × set ops)"
      using set_map set_l'_is
      by simp
    also have "… = { encode_operator_precondition Π k op | k op. (k, op) ∈ {0..<t} × set ops}"
      using setcompr_eq_image
      by fast
    finally have "set ?fs  = { encode_operator_precondition Π k op
      | k op. (k, op) ∈ ({0..<t} × set ops) }"
      by blast
  }
  thus ?thesis
    by blast
qed

private lemma is_cnf_encode_all_operator_preconditions:
  "is_cnf (encode_all_operator_preconditions Π (strips_problem.operators_of Π) t)"
proof -
  let ?l' = "List.product [0..<t] (strips_problem.operators_of Π)"
  let ?fs = "map (λ(k, op). encode_operator_precondition Π k op) ?l'"
  have "∀f ∈ set ?fs. is_cnf f"
    using encode_operator_precondition_is_cnf
    by fastforce
  thus ?thesis
    unfolding encode_all_operator_preconditions_def
    using is_cnf_foldr_and_if[of ?fs]
    by presburger
qed

(* TODO refactor Appendix *)
private lemma set_map_or[simp]:
  "set (map (λv. A v ❙∨ B v) vs) = { A v ❙∨ B v | v. v ∈ set vs }"
proof -
  let ?l = "map (λv. A v ❙∨ B v) vs"
  have "set ?l = (λv. A v ❙∨ B v) ` set vs"
    using set_map
    by force
  thus ?thesis
    using setcompr_eq_image
    by auto
qed

private lemma encode_operator_effects_is_cnf_i:
  "is_cnf (❙⋀(map (λv. (❙¬ (Atom (Operator t (index (strips_problem.operators_of Π) op))))
    ❙∨ Atom (State (Suc t) (index (strips_problem.variables_of Π) v))) (add_effects_of op)))"
proof -
  let ?fs = "map (λv. ❙¬ (Atom (Operator t (index (strips_problem.operators_of Π) op)))
    ❙∨ Atom (State (Suc t) (index (strips_problem.variables_of Π) v))) (add_effects_of op)"
  {
    fix C
    assume "C ∈ set ?fs"
    then obtain v
      where "v ∈ set (add_effects_of op)"
        and "C = ❙¬(Atom (Operator t (index (strips_problem.operators_of Π) op)))
          ❙∨ Atom (State (Suc t) (index (strips_problem.variables_of Π) v))"
      by auto
    hence "is_cnf C"
      by fastforce
  }
  thus ?thesis
    using is_cnf_BigAnd
    by blast
qed

private lemma encode_operator_effects_is_cnf_ii:
  "is_cnf (❙⋀(map (λv. ❙¬(Atom (Operator t (index (strips_problem.operators_of Π) op)))
    ❙∨ ❙¬(Atom (State (Suc t) (index (strips_problem.variables_of Π) v)))) (delete_effects_of op)))"
proof -
  let ?fs = "map (λv. ❙¬(Atom (Operator t (index (strips_problem.operators_of Π) op)))
    ❙∨ ❙¬(Atom (State (Suc t) (index (strips_problem.variables_of Π) v)))) (delete_effects_of op)"
  {
    fix C
    assume "C ∈ set ?fs"
    then obtain v
      where "v ∈ set (delete_effects_of op)"
        and "C = ❙¬(Atom (Operator t (index (strips_problem.operators_of Π) op)))
          ❙∨ ❙¬(Atom (State (Suc t) (index (strips_problem.variables_of Π) v)))"
      by auto
    hence "is_cnf C"
      by fastforce
  }
  thus ?thesis
    using is_cnf_BigAnd
    by blast
qed

private lemma encode_operator_effect_is_cnf:
  shows "is_cnf (encode_operator_effect Π t op)"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?vs = "strips_problem.variables_of Π"
  let ?fs = "map (λv. ❙¬(Atom (Operator t (index ?ops op)))
      ❙∨ Atom (State (Suc t) (index ?vs v)))
    (add_effects_of op)"
    and ?fs' = "map (λv. ❙¬(Atom (Operator t (index ?ops op)))
        ❙∨ ❙¬(Atom (State (Suc t) (index ?vs v))))
      (delete_effects_of op)"
  have "encode_operator_effect Π t op = ❙⋀(?fs @ ?fs')"
    unfolding encode_operator_effect_def[of Π t op]
    by metis
  moreover {
    have "∀f ∈ set ?fs. is_cnf f" "∀f ∈ set ?fs'. is_cnf f"
      using encode_operator_effects_is_cnf_i[of t Π op]
        encode_operator_effects_is_cnf_ii[of t Π op]
      by (simp+)
    (* TODO slow. *)
    hence "∀f ∈ set (?fs @ ?fs'). is_cnf f"
      by auto
  }
  ultimately show ?thesis
    using is_cnf_BigAnd[of "?fs @ ?fs'"]
    by presburger
qed

private lemma set_map_encode_operator_effect[simp]:
  "set (map (λ(t, op). encode_operator_effect Π t op) (List.product [0..<t]
      (strips_problem.operators_of Π)))
    = { encode_operator_effect Π k op
      | k op. (k, op) ∈ ({0..<t} × set (strips_problem.operators_of Π)) }"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?vs = "strips_problem.variables_of Π"
  let ?fs = "map (λ(t, op). encode_operator_effect Π t op) (List.product [0..<t] ?ops)"
  have "set ?fs = (λ(t, op). encode_operator_effect Π t op) ` ({0..<t} × set ?ops)"
    unfolding encode_operator_effect_def[of Π t]
    by force
  thus ?thesis
    using setcompr_eq_image[of "λ(t, op). encode_operator_effect Π t op"
        "λ(k, op). (k, op) ∈ {0..<t} × set ?ops"]
    by force
qed

private lemma encode_all_operator_effects_is_cnf:
  assumes "is_valid_problem_strips Π"
  shows "is_cnf (encode_all_operator_effects Π (strips_problem.operators_of Π) t)"
proof -
  let ?ops = "strips_problem.operators_of Π"
  let ?l = "List.product [0..<t] ?ops"
  let ?fs = "map (λ(t, op). encode_operator_effect Π t op) ?l"
  have "∀f ∈ set ?fs. is_cnf f"
    using encode_operator_effect_is_cnf
    by force
  thus ?thesis
    unfolding encode_all_operator_effects_def
    using is_cnf_foldr_and_if[of ?fs]
    by presburger
qed

lemma encode_operators_is_cnf:
  assumes "is_valid_problem_strips Π"
  shows "is_cnf (encode_operators Π t)"
  unfolding encode_operators_def
  using is_cnf_encode_all_operator_preconditions[of Π t]
    encode_all_operator_effects_is_cnf[OF assms, of t]
    is_cnf.simps(1)[of "encode_all_operator_preconditions Π (strips_problem.operators_of Π) t"
      "encode_all_operator_effects Π (strips_problem.operators_of Π) t"]
  by meson

― ‹ Simp flag alone did not do it, so we have to assign a name to this lemma as well. ›
private lemma set_map_to_operator_atom[simp]:
  "set (map (λop. Atom (Operator t (index (strips_problem.operators_of Π) op)))
      (filter (λop. ListMem v vs) (strips_problem.operators_of Π)))
    = { Atom (Operator t (index (strips_problem.operators_of Π) op))
      | op. op ∈ set (strips_problem.operators_of Π) ∧ v ∈ set vs }"
proof -
  let ?ops = "strips_problem.operators_of Π"
  {
    have "set (filter (λop. ListMem v vs) ?ops)
      = { op ∈ set ?ops. ListMem v vs }"
      using set_filter
      by force
    then have "set (filter (λop. ListMem v vs) ?ops)
      = { op. op ∈ set ?ops ∧ v ∈ set vs }"
      using ListMem_iff[of v]
      by blast
  }
  then have "set (map (λop. Atom (Operator t (index ?ops op)))
      (filter (λop. ListMem v vs) ?ops))
    = (λop. Atom (Operator t (index ?ops op))) ` { op ∈ set ?ops. v ∈ set vs }"
    using set_map[of "λop. Atom (Operator t (index ?ops op))"]
    by presburger
  thus ?thesis
    by blast
qed

(* TODO refactor ‹Formula_Supplement› *)
lemma is_disj_big_or_if:
  assumes "∀f ∈ set fs. is_lit_plus f"
  shows "is_disj ❙⋁fs"
  using assms
proof (induction fs)
  case (Cons f fs)
  have "is_lit_plus f"
    using Cons.prems
    by simp
  moreover have "is_disj ❙⋁fs"
    using Cons
    by fastforce
  ultimately show ?case
    by simp
qed simp

lemma is_cnf_encode_negative_transition_frame_axiom:
  shows "is_cnf (encode_negative_transition_frame_axiom Π t v)"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
  let ?deleting = "filter (λop. ListMem v (delete_effects_of op)) ?ops"
  let ?fs = "map (λop. Atom (Operator t (index ?ops op))) ?deleting"
    and ?A = "(❙¬(Atom (State t (index ?vs v))))"
    and ?B = "Atom (State (Suc t) (index ?vs v))"
  {
    fix f
    assume "f ∈ set ?fs"
    (* TODO slow. *)
    then obtain op
      where "op ∈ set ?ops"
        and "v ∈ set (delete_effects_of op)"
        and "f = Atom (Operator t (index ?ops op))"
      using set_map_to_operator_atom[of t Π v]
      by fastforce
    hence "is_lit_plus f"
      by simp
  } note nb = this
  {
    have "is_disj ❙⋁?fs"
      using is_disj_big_or_if nb
      by blast
    then have "is_disj (?B ❙∨ ❙⋁?fs)"
      by force
    then have "is_disj (?A ❙∨ (?B ❙∨ ❙⋁?fs))"
      by fastforce
    hence "is_cnf (?A ❙∨ (?B ❙∨ ❙⋁?fs))"
      by fastforce
  }
  thus ?thesis
    unfolding encode_negative_transition_frame_axiom_def
    by meson
qed

lemma is_cnf_encode_positive_transition_frame_axiom:
  shows "is_cnf (encode_positive_transition_frame_axiom Π t v)"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
  let ?adding = "filter (λop. ListMem v (add_effects_of op)) ?ops"
  let ?fs = "map (λop. Atom (Operator t (index ?ops op))) ?adding"
    and ?A = "Atom (State t (index ?vs v))"
    and ?B = "❙¬(Atom (State (Suc t) (index ?vs v)))"
  {
    fix f
    assume "f ∈ set ?fs"
    (* TODO slow. *)
    then obtain op
      where "op ∈ set ?ops"
        and "v ∈ set (add_effects_of op)"
        and "f = Atom (Operator t (index ?ops op))"
      using set_map_to_operator_atom[of t Π v]
      by fastforce
    hence "is_lit_plus f"
      by simp
  } note nb = this
  {
    have "is_disj ❙⋁?fs"
      using is_disj_big_or_if nb
      by blast
    then have "is_disj (?B ❙∨ ❙⋁?fs)"
      by force
    then have "is_disj (?A ❙∨ (?B ❙∨ ❙⋁?fs))"
      by fastforce
    hence "is_cnf (?A ❙∨ (?B ❙∨ ❙⋁?fs))"
      by fastforce
  }
  thus ?thesis
    unfolding encode_positive_transition_frame_axiom_def
    by meson
qed

private lemma encode_all_frame_axioms_set[simp]:
  "set (map (λ(k, v). encode_negative_transition_frame_axiom Π k v)
        (List.product [0..<t] (strips_problem.variables_of Π))
      @ (map (λ(k, v). encode_positive_transition_frame_axiom Π k v)
        (List.product [0..<t] (strips_problem.variables_of Π))))
    = { encode_negative_transition_frame_axiom Π k v
        | k v. (k, v) ∈ ({0..<t} × set (strips_problem.variables_of Π)) }
      ∪ { encode_positive_transition_frame_axiom Π k v
        | k v. (k, v) ∈ ({0..<t} × set (strips_problem.variables_of Π)) }"
proof -
  let ?l = "List.product [0..<t] (strips_problem.variables_of Π)"
  let ?A = "(λ(k, v). encode_negative_transition_frame_axiom Π k v) ` set ?l"
    and ?B = "(λ(k, v). encode_positive_transition_frame_axiom Π k v) ` set ?l"
    and ?fs = "map (λ(k, v). encode_negative_transition_frame_axiom Π k v) ?l
      @ (map (λ(k, v). encode_positive_transition_frame_axiom Π k v) ?l)"
    and ?vs = "strips_problem.variables_of Π"
  have set_l_is: "set ?l = {0..<t} × set ?vs"
    by simp
  have "set ?fs = ?A ∪ ?B"
    using set_append
    by force
  moreover have "?A = { encode_negative_transition_frame_axiom Π k v
    | k v. (k, v) ∈ ({0..<t} × set ?vs) }"
    using set_l_is setcompr_eq_image[of "λ(k, v). encode_negative_transition_frame_axiom Π k v"
        "λ(k, v). (k, v) ∈ ({0..<t} × set ?vs)"]
    by fast
  moreover have "?B = { encode_positive_transition_frame_axiom Π k v
    | k v. (k, v) ∈ ({0..<t} × set ?vs) }"
    using set_l_is setcompr_eq_image[of "λ(k, v). encode_positive_transition_frame_axiom Π k v"
        "λ(k, v). (k, v) ∈ ({0..<t} × set ?vs)"]
    by fast
  ultimately show ?thesis
    by argo
qed

(* rename ‹is_cnf_encode_all_frame_axioms›. *)
lemma encode_frame_axioms_is_cnf:
  shows "is_cnf (encode_all_frame_axioms Π t)"
proof -
  let ?l = "List.product [0..<t] (strips_problem.variables_of Π)"
    and ?vs = "strips_problem.variables_of Π"
  let ?A = "{ encode_negative_transition_frame_axiom Π k v
    | k v. (k, v) ∈ ({0..<t} × set ?vs) }"
    and ?B = "{ encode_positive_transition_frame_axiom Π k v
    | k v. (k, v) ∈ ({0..<t} × set ?vs) }"
    and ?fs = "map (λ(k, v). encode_negative_transition_frame_axiom Π k v) ?l
      @ (map (λ(k, v). encode_positive_transition_frame_axiom Π k v) ?l)"
  {
    fix f
    assume "f ∈ set ?fs"
    (* TODO slow. *)
    then consider (f_encodes_negative_frame_axiom) "f ∈ ?A"
      | (f_encodes_positive_frame_axiom) "f ∈ ?B"
      by fastforce
    hence "is_cnf f"
      using is_cnf_encode_negative_transition_frame_axiom
        is_cnf_encode_positive_transition_frame_axiom
      by (smt mem_Collect_eq)
  }
  thus ?thesis
    unfolding encode_all_frame_axioms_def
    using is_cnf_BigAnd[of ?fs]
    by meson
qed

lemma is_cnf_encode_problem:
  assumes "is_valid_problem_strips Π"
  shows "is_cnf (Φ Π t)"
proof -
  have "is_cnf (Φ⇩I Π)"
    using is_cnf_encode_initial_state assms
    by auto
  moreover have "is_cnf (encode_goal_state Π t)"
    using encode_goal_state_is_cnf[OF assms]
    by simp
  moreover have "is_cnf (encode_operators Π t ❙∧ encode_all_frame_axioms Π t)"
    using encode_operators_is_cnf[OF assms] encode_frame_axioms_is_cnf
    unfolding encode_transitions_def
    by simp
  ultimately show ?thesis
    unfolding encode_problem_def SAT_Plan_Base.encode_problem_def
      encode_transitions_def encode_initial_state_def[symmetric] encode_goal_state_def[symmetric]
    by simp
qed

lemma encode_problem_has_model_then_also_partial_encodings:
  assumes "𝒜 ⊨ SAT_Plan_Base.encode_problem Π t"
  shows "𝒜 ⊨ SAT_Plan_Base.encode_initial_state Π"
    and "𝒜 ⊨ SAT_Plan_Base.encode_goal_state Π t"
    and "𝒜 ⊨ SAT_Plan_Base.encode_operators Π t"
    and "𝒜 ⊨ SAT_Plan_Base.encode_all_frame_axioms Π t"
  using assms
  unfolding SAT_Plan_Base.encode_problem_def
  by simp+

lemma cnf_of_encode_problem_structure:
  shows "cnf (SAT_Plan_Base.encode_initial_state Π)
    ⊆ cnf (SAT_Plan_Base.encode_problem Π t)"
    and "cnf (SAT_Plan_Base.encode_goal_state Π t)
      ⊆ cnf (SAT_Plan_Base.encode_problem Π t)"
    and "cnf (SAT_Plan_Base.encode_operators Π t)
      ⊆ cnf (SAT_Plan_Base.encode_problem Π t)"
    and "cnf (SAT_Plan_Base.encode_all_frame_axioms Π t)
      ⊆ cnf (SAT_Plan_Base.encode_problem Π t)"
  unfolding SAT_Plan_Base.encode_problem_def
    SAT_Plan_Base.encode_problem_def[of Π t] SAT_Plan_Base.encode_initial_state_def[of Π]
    SAT_Plan_Base.encode_goal_state_def[of Π t] SAT_Plan_Base.encode_operators_def
    SAT_Plan_Base.encode_all_frame_axioms_def[of Π t]
  subgoal by auto
  subgoal by force
  subgoal by auto
  subgoal by force
  done

― ‹ A technical lemma which shows a simpler form of the CNF of the initial state encoding. ›
(* TODO generalize for more encodings? *)
private lemma cnf_of_encode_initial_state_set_i:
  shows "cnf (Φ⇩I Π) = ⋃ { cnf (encode_state_variable 0
    (index (strips_problem.variables_of Π) v) (((Π)⇩I) v))
      | v. v ∈ set (strips_problem.variables_of Π) ∧ ((Π)⇩I) v ≠ None }"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?I = "strips_problem.initial_of Π"
  let ?ls = "map (λv. encode_state_variable 0 (index ?vs v) (?I v) ❙∨ ⊥)
    (filter (λv. ?I v ≠ None) ?vs)"
  {
    have "cnf ` set ?ls = cnf ` (λv. encode_state_variable 0 (index ?vs v) (?I v) ❙∨ ⊥)
      ` set (filter (λv. ?I v ≠ None) ?vs)"
      using set_map[of "λv. encode_state_variable 0 (index ?vs v) (?I v) ❙∨ ⊥"]
      by presburger
    also have "… = (λv. cnf (encode_state_variable 0 (index ?vs v) (?I v) ❙∨ ⊥))
      ` set (filter (λv. ?I v ≠ None) ?vs)"
      using image_comp
      by blast
    also have "… = (λv. cnf (encode_state_variable 0 (index ?vs v) (?I v)))
      ` { v ∈ set ?vs. ?I v ≠ None }"
      using set_filter[of "λv. ?I v ≠ None" ?vs]
      by auto
    finally have "cnf ` set ?ls = { cnf (encode_state_variable 0 (index ?vs v) (?I v))
      | v. v ∈ set ?vs ∧ ?I v ≠ None }"
      using setcompr_eq_image[of "λv. cnf (encode_state_variable 0 (index ?vs v) (?I v))"]
      by presburger
  }
  moreover have "cnf (Φ⇩I Π) = ⋃ (cnf ` set ?ls)"
    unfolding encode_initial_state_def SAT_Plan_Base.encode_initial_state_def
    using cnf_BigAnd[of ?ls]
    by meson
  ultimately show ?thesis
    by auto
qed

― ‹ A simplification lemma for the above one. ›
(* TODO Replace above lemma with this?. *)
corollary cnf_of_encode_initial_state_set_ii:
  assumes "is_valid_problem_strips Π"
  shows "cnf (Φ⇩I Π) = (⋃v ∈ set (strips_problem.variables_of Π). {{
    literal_formula_to_literal (encode_state_variable 0 (index (strips_problem.variables_of Π) v)
      (strips_problem.initial_of Π v)) }})"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?I = "strips_problem.initial_of Π"
  have nb⇩1: "{ v. v ∈ set ?vs ∧ ?I v ≠ None } = set ?vs"
    using is_valid_problem_strips_initial_of_dom assms(1)
    by auto
  (* TODO generalize and refactor. *)
  {
    fix v
    assume "v ∈ set ?vs"
    then have "?I v ≠ None"
      using is_valid_problem_strips_initial_of_dom assms(1)
      by auto
    then consider (I_v_is_Some_True) "?I v = Some True"
      | (I_v_is_Some_False) "?I v = Some False"
      by fastforce
    hence "cnf (encode_state_variable 0 (index ?vs v) (?I v))
      = {{ literal_formula_to_literal (encode_state_variable 0 (index ?vs v) (?I v)) }}"
      unfolding encode_state_variable_def
      by (cases, simp+)
  } note nb⇩2 = this
  {
    have "{ cnf (encode_state_variable 0 (index ?vs v) (?I v)) | v. v ∈ set ?vs ∧ ?I v ≠ None }
       = (λv. cnf (encode_state_variable 0 (index ?vs v) (?I v))) ` set ?vs"
    using setcompr_eq_image[of "λv. cnf (encode_state_variable 0 (index ?vs v) (?I v))"
        "λv. v ∈ set ?vs ∧ ?I v ≠ None"] using nb⇩1
    by presburger
    hence "{ cnf (encode_state_variable 0 (index ?vs v) (?I v)) | v. v ∈ set ?vs ∧ ?I v ≠ None }
      = (λv. {{ literal_formula_to_literal (encode_state_variable 0 (index ?vs v) (?I v)) }})
        ` set ?vs"
      using nb⇩2
      by force
  }
  thus ?thesis
    using cnf_of_encode_initial_state_set_i
    by (smt Collect_cong)
qed

(* TODO ‹∃!› is superfluous now? rm? + Above lemma basically covers this one. *)
lemma  cnf_of_encode_initial_state_set:
  assumes "is_valid_problem_strips Π"
    and "v ∈ dom (strips_problem.initial_of Π)"
  shows "strips_problem.initial_of Π v = Some True ⟶ (∃!C. C ∈ cnf (Φ⇩I Π)
      ∧ C = { (State 0 (index (strips_problem.variables_of Π) v))⇧+ })"
    and "strips_problem.initial_of Π v = Some False ⟶ (∃!C. C ∈ cnf (Φ⇩I Π)
      ∧ C = { (State 0 (index (strips_problem.variables_of Π) v))¯ })"
proof -
  let ?I = "(Π)⇩I"
  let ?vs = "strips_problem.variables_of Π"
  let ?Φ⇩I = "Φ⇩I Π"
  have nb⇩1: "cnf (Φ⇩I Π) = ⋃ { cnf (encode_state_variable 0 (index ?vs v)
      (strips_problem.initial_of Π v)) | v. v ∈ set ?vs ∧ ?I v ≠ None }"
    using cnf_of_encode_initial_state_set_i
    by blast
  {
    have "v ∈ set ?vs"
      using is_valid_problem_strips_initial_of_dom assms(1, 2)
      by blast
    hence "v ∈ { v. v ∈ set ?vs ∧ ?I v ≠ None }"
      using assms(2)
      by auto
  } note nb⇩2 = this
  show "strips_problem.initial_of Π v = Some True ⟶ (∃!C. C ∈ cnf (Φ⇩I Π)
      ∧ C = { (State 0 (index (strips_problem.variables_of Π) v))⇧+ })"
    and "strips_problem.initial_of Π v = Some False ⟶ (∃!C. C ∈ cnf (Φ⇩I Π)
      ∧ C = { (State 0 (index (strips_problem.variables_of Π) v))¯ })"
    proof (auto)
      assume i_v_is_some_true: "strips_problem.initial_of Π v = Some True"
      then have "{ (State 0 (index (strips_problem.variables_of Π) v))⇧+ }
        ∈ cnf (encode_state_variable 0 (index (strips_problem.variables_of Π) v) (?I v))"
        unfolding encode_state_variable_def
        using i_v_is_some_true
        by auto
      thus "{ (State 0 (index (strips_problem.variables_of Π) v))⇧+ }
        ∈ cnf (Φ⇩I Π)"
        using nb⇩1 nb⇩2
        by auto
    next
      assume i_v_is_some_false: "strips_problem.initial_of Π v = Some False"
      then have "{ (State 0 (index (strips_problem.variables_of Π) v))¯ }
        ∈ cnf (encode_state_variable 0 (index (strips_problem.variables_of Π) v) (?I v))"
        unfolding encode_state_variable_def
        using i_v_is_some_false
        by auto
      thus "{ (State 0 (index (strips_problem.variables_of Π) v))¯ }
        ∈ cnf (Φ⇩I Π)"
        using nb⇩1 nb⇩2
        by auto
    qed
qed

lemma cnf_of_operator_encoding_structure:
  "cnf (encode_operators Π t) = cnf (encode_all_operator_preconditions Π
      (strips_problem.operators_of Π) t)
    ∪ cnf (encode_all_operator_effects Π (strips_problem.operators_of Π) t)"
  unfolding encode_operators_def
  using cnf.simps(5)
  by metis

corollary cnf_of_operator_precondition_encoding_subset_encoding:
  "cnf (encode_all_operator_preconditions Π (strips_problem.operators_of Π) t)
    ⊆ cnf (Φ Π t)"
  using cnf_of_operator_encoding_structure cnf_of_encode_problem_structure subset_trans
  unfolding encode_problem_def
  by blast

(* TODO refactor ‹CNF_Supplement› *)
lemma  cnf_foldr_and[simp]:
  "cnf (foldr (❙∧) fs (❙¬⊥)) = (⋃f ∈ set fs. cnf f)"
proof (induction fs)
  case (Cons f fs)
  have ih: "cnf (foldr (❙∧) fs (❙¬⊥)) = (⋃f ∈ set fs. cnf f)"
    using Cons.IH
    by blast
  {
    have "cnf (foldr (❙∧) (f # fs) (❙¬⊥)) = cnf (f ❙∧ foldr (❙∧) fs (❙¬⊥))"
      by simp
    also have "… = cnf f ∪ cnf (foldr (❙∧) fs (❙¬⊥))"
      by force
    finally have "cnf (foldr (❙∧) (f # fs) (❙¬⊥)) = cnf f ∪ (⋃f ∈ set fs. cnf f)"
      using ih
      by argo
  }
  thus ?case
    by auto
qed simp

(* TODO rm (unused)? *)
private lemma cnf_of_encode_operator_precondition[simp]:
  "cnf (encode_operator_precondition Π t op) = (⋃v ∈ set (precondition_of op).
    {{(Operator t (index (strips_problem.operators_of Π) op))¯
      , (State t (index (strips_problem.variables_of Π) v))⇧+}})"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
    and ?Φ⇩P = "encode_operator_precondition Π t op"
  let ?fs = "map (λv. ❙¬ (Atom (Operator t (index ?ops op))) ❙∨ Atom (State t (index ?vs v)))
    (precondition_of op)"
    and ?A = "(λv. ❙¬ (Atom (Operator t (index ?ops op))) ❙∨ Atom (State t (index ?vs v)))
      ` set (precondition_of op)"
  have "cnf (encode_operator_precondition Π t op) = cnf (❙⋀?fs)"
    unfolding encode_operator_precondition_def
    by presburger
  also have "… = ⋃ (cnf ` set ?fs)"
    using cnf_BigAnd
    by blast
  also have "… = ⋃(cnf ` ?A)"
    using set_map[of "λv. ❙¬ (Atom (Operator t (index ?ops op))) ❙∨ Atom (State t (index ?vs v))"
        "precondition_of op"]
    by argo
  also have "… = (⋃v ∈ set (precondition_of op).
    cnf (❙¬(Atom (Operator t (index ?ops op))) ❙∨ Atom (State t (index ?vs v))))"
    by blast
  (* TODO slow. *)
  finally show ?thesis
    by auto
qed

(* TODO Shorten proof. *)
lemma cnf_of_encode_all_operator_preconditions_structure[simp]:
  "cnf (encode_all_operator_preconditions Π (strips_problem.operators_of Π) t)
    = (⋃(t, op) ∈ ({..<t} × set (operators_of Π)).
      (⋃v ∈ set (precondition_of op).
        {{(Operator t (index (strips_problem.operators_of Π) op))¯
          , (State t (index (strips_problem.variables_of Π) v))⇧+}}))"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
  let ?l = "List.product [0..<t] ?ops"
    and ?Φ⇩P = "encode_all_operator_preconditions Π (strips_problem.operators_of Π) t"
  let ?A = "set (map (λ(t, op). encode_operator_precondition Π t op) ?l)"
  {
    have "set ?l = {0..<t} × set ((Π)⇩𝒪)"
      by auto
    then have "?A = (λ(t, op). encode_operator_precondition Π t op) ` ({0..<t} × set ((Π)⇩𝒪))"
      using set_map
      by force
  } note nb = this
  have "cnf ?Φ⇩P = cnf (foldr (❙∧) (map (λ(t, op). encode_operator_precondition Π t op) ?l) (❙¬⊥))"
    unfolding encode_all_operator_preconditions_def
    by presburger
  also have "… = (⋃f ∈ ?A. cnf f)"
    by simp
  (* TODO slow. *)
  also have "… = (⋃(k, op) ∈ ({0..<t} × set ((Π)⇩𝒪)).
    cnf (encode_operator_precondition Π k op))"
    using nb
    by fastforce
  (* TODO very slow. *)
  finally show ?thesis
     by fastforce
 qed

corollary cnf_of_encode_all_operator_preconditions_contains_clause_if:
  fixes Π::"'variable STRIPS_Representation.strips_problem"
  assumes "is_valid_problem_strips (Π::'variable STRIPS_Representation.strips_problem)"
    and "k < t"
    and "op ∈ set ((Π)⇩𝒪)"
    and "v ∈ set (precondition_of op)"
  shows "{ (Operator k (index (strips_problem.operators_of Π) op))¯
    , (State k (index (strips_problem.variables_of Π) v))⇧+ }
  ∈ cnf (encode_all_operator_preconditions Π (strips_problem.operators_of Π) t)"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?vs = "strips_problem.variables_of Π"
  let ?Φ⇩P = "encode_all_operator_preconditions Π ?ops t"
    and ?C = "{ (Operator k (index (strips_problem.operators_of Π) op))¯
      , (State k (index (strips_problem.variables_of Π) v))⇧+ }"
  {
    have nb: "(k, op) ∈ {..<t} × set ((Π)⇩𝒪)"
      using assms(2, 3)
      by blast
    moreover {
      have "?C ∈ (⋃v∈set (precondition_of op).
        {{(Operator k (index (strips_problem.operators_of Π) op))¯,
          (State k (index (strips_problem.variables_of Π) v))⇧+}})"
        using UN_iff[where A="set (precondition_of op)"
          and B="λv. {{(Operator t (index (strips_problem.operators_of Π) op))¯,
          (State t (index (strips_problem.variables_of Π) v))⇧+}}"] assms(4)
        by blast
      hence "∃x∈{..<t} × set ((Π)⇩𝒪).
        ?C ∈ (case x of (k, op) ⇒ ⋃v∈set (precondition_of op).
        {{(Operator k (index (strips_problem.operators_of Π) op))¯,
          (State k (index (strips_problem.variables_of Π) v))⇧+}})"
        using nb
        by blast
    }
    ultimately have "?C ∈ (⋃(t, op) ∈ ({..<t} × set ((Π)⇩𝒪)).
      (⋃v ∈ set (precondition_of op).
        {{ (Operator t (index ?ops op))¯, (State t (index ?vs v))⇧+ }}))"
      by blast
  }
  thus ?thesis
    using cnf_of_encode_all_operator_preconditions_structure[of Π t]
    by argo
qed

corollary cnf_of_encode_all_operator_effects_subset_cnf_of_encode_problem:
  "cnf (encode_all_operator_effects Π (strips_problem.operators_of Π) t)
    ⊆ cnf (Φ Π t)"
  using cnf_of_encode_problem_structure(3) cnf_of_operator_encoding_structure
  unfolding encode_problem_def
  by blast

private lemma cnf_of_encode_operator_effect_structure[simp]:
  "cnf (encode_operator_effect Π t op)
    = (⋃v ∈ set (add_effects_of op). {{ (Operator t (index (strips_problem.operators_of Π) op))¯
        , (State (Suc t) (index (strips_problem.variables_of Π) v))⇧+ }})
      ∪ (⋃v ∈ set (delete_effects_of op).
        {{ (Operator t (index (strips_problem.operators_of Π) op))¯
          , (State (Suc t) (index (strips_problem.variables_of Π) v))¯ }})"
proof -
  let ?fs⇩1 = "map (λv. ❙¬(Atom (Operator t (index (strips_problem.operators_of Π) op)))
    ❙∨ Atom (State (Suc t) (index (strips_problem.variables_of Π) v)))
    (add_effects_of op)"
    and ?fs⇩2 = "map (λv. ❙¬(Atom (Operator t (index (strips_problem.operators_of Π) op)))
      ❙∨ ❙¬ (Atom (State (Suc t) (index (strips_problem.variables_of Π) v))))
      (delete_effects_of op)"
  {
    have "cnf ` set ?fs⇩1 = cnf
        ` (λv. ❙¬(Atom (Operator t (index (strips_problem.operators_of Π) op)))
      ❙∨ Atom (State (Suc t) (index (strips_problem.variables_of Π) v))) ` set (add_effects_of op)"
      using set_map
      by force
    also have "… = (λv. cnf (❙¬(Atom (Operator t (index (strips_problem.operators_of Π) op)))
      ❙∨ Atom (State (Suc t) (index (strips_problem.variables_of Π) v))))
        ` set (add_effects_of op)"
      using image_comp
      by blast
    (* TODO slow. *)
    finally have "cnf ` set ?fs⇩1 = (λv. {{ (Operator t (index (strips_problem.operators_of Π) op))¯
      , (State (Suc t) (index (strips_problem.variables_of Π) v))⇧+ }}) ` set (add_effects_of op)"
      by auto
  } note nb⇩1 = this
  {
    have "cnf ` set ?fs⇩2 = cnf ` (λv. ❙¬(Atom (Operator t (index (strips_problem.operators_of Π) op)))
      ❙∨ ❙¬(Atom (State (Suc t) (index (strips_problem.variables_of Π) v))))
        ` set (delete_effects_of op)"
      using set_map
      by force
    also have "… = (λv. cnf (❙¬(Atom (Operator t (index (strips_problem.operators_of Π) op)))
      ❙∨ ❙¬ (Atom (State (Suc t) (index (strips_problem.variables_of Π) v)))))
        ` set (delete_effects_of op)"
      using image_comp
      by blast
    (* TODO slow. *)
    finally have "cnf ` set ?fs⇩2 = (λv. {{ (Operator t (index (strips_problem.operators_of Π) op))¯
      , (State (Suc t) (index (strips_problem.variables_of Π) v))¯ }})
        ` set (delete_effects_of op)"
      by auto
  } note nb⇩2 = this
  {
    have "cnf (encode_operator_effect Π t op) = ⋃(cnf ` set (?fs⇩1 @ ?fs⇩2))"
      unfolding encode_operator_effect_def
      using cnf_BigAnd[of "?fs⇩1 @ ?fs⇩2"]
      by meson
    also have "… = ⋃(cnf ` set ?fs⇩1 ∪ cnf ` set ?fs⇩2)"
      using set_append[of "?fs⇩1" "?fs⇩2"] image_Un[of cnf "set ?fs⇩1" "set ?fs⇩2"]
      by argo
    also have "… = ⋃(cnf ` set ?fs⇩1) ∪ ⋃(cnf ` set ?fs⇩2)"
      using Union_Un_distrib[of "cnf ` set ?fs⇩1" "cnf ` set ?fs⇩2"]
      by argo
    (* TODO slow. *)
    finally have "cnf (encode_operator_effect Π t op)
        = (⋃v ∈ set (add_effects_of op).
          {{ (Operator t (index (strips_problem.operators_of Π) op))¯
            , (State (Suc t) (index (strips_problem.variables_of Π) v))⇧+ }})
        ∪ (⋃v ∈ set (delete_effects_of op).
          {{ (Operator t (index (strips_problem.operators_of Π) op))¯
            , (State (Suc t) (index (strips_problem.variables_of Π) v))¯ }})"
      using nb⇩1 nb⇩2
      by argo
  }
  thus ?thesis
    by blast
qed

lemma cnf_of_encode_all_operator_effects_structure:
  "cnf (encode_all_operator_effects Π (strips_problem.operators_of Π) t)
    = (⋃(k, op) ∈ ({0..<t} × set ((Π)⇩𝒪)).
        (⋃v ∈ set (add_effects_of op).
          {{ (Operator k (index (strips_problem.operators_of Π) op))¯
            , (State (Suc k) (index (strips_problem.variables_of Π) v))⇧+ }}))
      ∪ (⋃(k, op) ∈ ({0..<t} × set ((Π)⇩𝒪)).
        (⋃v ∈ set (delete_effects_of op).
          {{ (Operator k (index (strips_problem.operators_of Π) op))¯
            , (State (Suc k) (index (strips_problem.variables_of Π) v))¯ }}))"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?vs = "strips_problem.variables_of Π"
  let ?Φ⇩E = "encode_all_operator_effects Π ?ops t"
    and ?l = "List.product [0..<t] ?ops"
  let ?fs = "map (λ(t, op). encode_operator_effect Π t op) ?l"
  have nb: "set (List.product [0..<t] ?ops) = {0..<t} × set ?ops"
    by simp
  {
    have "cnf ` set ?fs = cnf ` (λ(k, op). encode_operator_effect Π k op) ` ({0..<t} × set ?ops)"
      by force
    also have "… = (λ(k, op). cnf (encode_operator_effect Π k op)) ` ({0..<t} × set ?ops)"
      using image_comp
      by fast
    (* TODO slow. *)
    finally have "cnf ` set ?fs = (λ(k, op).
          (⋃v ∈ set (add_effects_of op).
            {{ (Operator k (index (strips_problem.operators_of Π) op))¯
              , (State (Suc k) (index (strips_problem.variables_of Π) v))⇧+ }})
        ∪ (⋃v ∈ set (delete_effects_of op).
            {{ (Operator k (index (strips_problem.operators_of Π) op))¯
              , (State (Suc k) (index (strips_problem.variables_of Π) v))¯ }}))
      ` ({0..<t} × set ?ops)"
      using cnf_of_encode_operator_effect_structure
      by auto
  }
  (* TODO slow. *)
  thus ?thesis
    unfolding encode_all_operator_effects_def
    using cnf_BigAnd[of ?fs]
    by auto
qed

corollary cnf_of_operator_effect_encoding_contains_add_effect_clause_if:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "k < t"
    and "op ∈ set ((Π)⇩𝒪)"
    and "v ∈ set (add_effects_of op)"
  shows "{ (Operator k (index (strips_problem.operators_of Π) op))¯
      , (State (Suc k) (index (strips_problem.variables_of Π) v))⇧+ }
    ∈ cnf (encode_all_operator_effects Π (strips_problem.operators_of Π) t)"
proof -
  let ?Φ⇩E = "encode_all_operator_effects Π (strips_problem.operators_of Π) t"
    and ?ops = "strips_problem.operators_of Π"
    and ?vs = "strips_problem.variables_of Π"
  let ?Add = "⋃(k, op)∈{0..<t} × set ((Π)⇩𝒪).
    ⋃v∈set (add_effects_of op). {{ (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+}}"
  let ?C = "{ (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+ }"
  have "?Add ⊆ cnf ?Φ⇩E"
    using cnf_of_encode_all_operator_effects_structure[of Π t] Un_upper1[of "?Add"]
    by presburger
  moreover {
    have "?C  ∈ {{ (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+ }}"
        using assms(4)
        by blast
      then have "?C ∈ (⋃v∈set (add_effects_of op).
        {{ (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+}})"
        using Complete_Lattices.UN_iff[of "?C" "λv. {{ (Operator k (index ?ops op))¯
          , (State (Suc k) (index ?vs v))⇧+}}" "set (add_effects_of op)"]
      using assms(4)
      by blast
    moreover have "(k, op) ∈ ({0..<t} × set ((Π)⇩𝒪))"
      using assms(2, 3)
      by fastforce
    (* TODO slow step. *)
    ultimately have "?C ∈ ?Add"
      by blast
  }
  ultimately show ?thesis
    using subset_eq[of "?Add" "cnf ?Φ⇩E"]
    by meson
qed

corollary cnf_of_operator_effect_encoding_contains_delete_effect_clause_if:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "k < t"
    and "op ∈ set ((Π)⇩𝒪)"
    and "v ∈ set (delete_effects_of op)"
  shows "{ (Operator k (index (strips_problem.operators_of Π) op))¯
      , (State (Suc k) (index (strips_problem.variables_of Π) v))¯ }
    ∈ cnf (encode_all_operator_effects Π (strips_problem.operators_of Π) t)"
proof -
  let ?Φ⇩E = "encode_all_operator_effects Π (strips_problem.operators_of Π) t"
    and ?ops = "strips_problem.operators_of Π"
    and ?vs = "strips_problem.variables_of Π"
  let ?Delete = "(⋃(k, op)∈{0..<t} × set ((Π)⇩𝒪).
    ⋃v∈set (delete_effects_of op).
      {{ (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯ }})"
  let ?C = "{ (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯ }"
  have "?Delete ⊆ cnf ?Φ⇩E"
    using cnf_of_encode_all_operator_effects_structure[of Π t] Un_upper2[of "?Delete"]
    by presburger
  moreover {
    have "?C ∈ (⋃v ∈ set (delete_effects_of op).
      {{ (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯ }})"
      using assms(4)
      by blast
    moreover have "(k, op) ∈ {0..<t} × set ?ops"
    using assms(2, 3)
    by force
    (* TODO slow step. *)
    ultimately have "?C ∈ ?Delete"
      by fastforce
  }
  (* TODO slow step. *)
  ultimately show ?thesis
    using subset_eq[of "?Delete" "cnf ?Φ⇩E"]
    by meson
qed

(* TODO refactor ‹CNF_Supplement›. *)
private lemma cnf_of_big_or_of_literal_formulas_is[simp]:
  assumes "∀f ∈ set fs. is_literal_formula f"
  shows "cnf (❙⋁fs) = {{ literal_formula_to_literal f | f. f ∈ set fs }}"
  using assms
proof (induction fs)
  case (Cons f fs)
  {
    have is_literal_formula_f: "is_literal_formula f"
      using Cons.prems(1)
      by simp
    then have "cnf f = {{ literal_formula_to_literal f }}"
      using cnf_of_literal_formula
      by blast
  } note nb⇩1 = this
  {
    have "∀f' ∈ set fs. is_literal_formula f'"
      using Cons.prems
      by fastforce
    hence "cnf (❙⋁fs) = {{ literal_formula_to_literal f | f. f ∈ set fs }}"
      using Cons.IH
      by argo
  } note nb⇩2 = this
  {
    have "cnf (❙⋁(f # fs)) = (λ(g, h). g ∪ h)
      ` ({{ literal_formula_to_literal f}}
        × {{ literal_formula_to_literal f' | f'. f' ∈ set fs }})"
      using nb⇩1 nb⇩2
      by simp
    also have "… = {{ literal_formula_to_literal f}
      ∪ { literal_formula_to_literal f' | f'. f' ∈ set fs }}"
      by fast
    finally have "cnf (❙⋁(f # fs)) = {{ literal_formula_to_literal f' | f'. f' ∈ set (f # fs) }}"
      by fastforce
  }
  thus ?case .
qed simp

private lemma set_filter_op_list_mem_vs[simp]:
  "set (filter (λop. ListMem v vs) ops) = { op. op ∈ set ops ∧ v ∈ set vs }"
  using set_filter[of "λop. ListMem v vs" ops] ListMem_iff
  by force

private lemma  cnf_of_positive_transition_frame_axiom:
  "cnf (encode_positive_transition_frame_axiom Π k v)
    = {{ (State k (index (strips_problem.variables_of Π) v))⇧+
        , (State (Suc k) (index (strips_problem.variables_of Π) v))¯ }
      ∪ { (Operator k (index (strips_problem.operators_of Π) op))⇧+
        | op. op ∈ set (strips_problem.operators_of Π) ∧ v ∈ set (add_effects_of op) }}"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
  let ?adding_operators = "filter (λop. ListMem v (add_effects_of op)) ?ops"
  let ?fs = "map (λop. Atom (Operator k (index ?ops op))) ?adding_operators"
  {
    have "set ?fs = (λop. Atom (Operator k (index ?ops op))) ` set ?adding_operators"
      using set_map[of "λop. Atom (Operator k (index ?ops op))" "?adding_operators"]
      by blast
    (* TODO slow. *)
    then have "literal_formula_to_literal ` set ?fs
      = (λop. (Operator k (index ?ops op))⇧+) ` set ?adding_operators"
      using image_comp[of literal_formula_to_literal "λop. Atom (Operator k (index ?ops op))"
          "set ?adding_operators"]
      by simp
    also have "… = (λop. (Operator k (index ?ops op))⇧+)
        ` { op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }"
      using set_filter_op_list_mem_vs[of v _  ?ops]
      by auto
    (* TODO slow. *)
    finally have "literal_formula_to_literal ` set ?fs
      = { (Operator k (index ?ops op))⇧+ | op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }"
      using setcompr_eq_image[of "λop. (Operator k (index ?ops op))⇧+"
          "λop. op ∈set ?adding_operators"]
      by blast
    (* TODO slow. *)
    hence "cnf (❙⋁?fs) = {{ (Operator k (index ?ops op))⇧+
      | op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }}"
      using cnf_of_big_or_of_literal_formulas_is[of ?fs]
        setcompr_eq_image[of literal_formula_to_literal "λf. f ∈ set ?fs"]
      by force
  }
  (* TODO slow. *)
  then have "cnf (❙¬(Atom (State (Suc k) (index ?vs v))) ❙∨ ❙⋁?fs)
  = {{ (State (Suc k) (index ?vs v))¯  } ∪ { (Operator k (index ?ops op))⇧+
    | op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }}"
    by force
  (* TODO slow. *)
  then have "cnf ((Atom (State k (index ?vs v)) ❙∨ (❙¬(Atom (State (Suc k) (index ?vs v))) ❙∨ ❙⋁?fs)))
    = {{ (State k (index ?vs v))⇧+ }
      ∪ { (State (Suc k) (index ?vs v))¯ }
      ∪ { (Operator k (index ?ops op))⇧+ | op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }}"
    by simp
  (* TODO No idea why this is necessary (apparently only metis unfolds the definition properly). *)
  moreover have "cnf (encode_positive_transition_frame_axiom Π k v)
    = cnf ((Atom (State k (index ?vs v)) ❙∨ (❙¬(Atom (State (Suc k) (index ?vs v))) ❙∨ ❙⋁?fs)))"
    unfolding encode_positive_transition_frame_axiom_def
    by metis
  (* TODO slow. *)
  ultimately show ?thesis
    by blast
qed

private lemma cnf_of_negative_transition_frame_axiom:
  "cnf (encode_negative_transition_frame_axiom Π k v)
    = {{ (State k (index (strips_problem.variables_of Π) v))¯
        , (State (Suc k) (index (strips_problem.variables_of Π) v))⇧+  }
      ∪ { (Operator k (index (strips_problem.operators_of Π) op))⇧+
        | op. op ∈ set (strips_problem.operators_of Π) ∧ v ∈ set (delete_effects_of op) }}"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
  let ?deleting_operators = "filter (λop. ListMem v (delete_effects_of op)) ?ops"
  let ?fs = "map (λop. Atom (Operator k (index ?ops op))) ?deleting_operators"
  {
    have "set ?fs = (λop. Atom (Operator k (index ?ops op))) ` set ?deleting_operators"
      using set_map[of "λop. Atom (Operator k (index ?ops op))" "?deleting_operators"]
      by blast
    (* TODO slow. *)
    then have "literal_formula_to_literal ` set ?fs
      = (λop. (Operator k (index ?ops op))⇧+) ` set ?deleting_operators"
      using image_comp[of literal_formula_to_literal "λop. Atom (Operator k (index ?ops op))"
          "set ?deleting_operators"]
      by simp
    also have "… = (λop. (Operator k (index ?ops op))⇧+)
        ` { op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op) }"
      using set_filter_op_list_mem_vs[of v _  ?ops]
      by auto
    (* TODO slow. *)
    finally have "literal_formula_to_literal ` set ?fs
      = { (Operator k (index ?ops op))⇧+ | op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op) }"
      using setcompr_eq_image[of "λop. (Operator k (index ?ops op))⇧+"
          "λop. op ∈set ?deleting_operators"]
      by blast
    (* TODO slow. *)
    hence "cnf (❙⋁?fs) = {{ (Operator k (index ?ops op))⇧+
      | op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op) }}"
      using cnf_of_big_or_of_literal_formulas_is[of ?fs]
        setcompr_eq_image[of literal_formula_to_literal "λf. f ∈ set ?fs"]
      by force
  }
  (* TODO slow. *)
  then have "cnf (Atom (State (Suc k) (index ?vs v)) ❙∨ ❙⋁?fs)
  = {{ (State (Suc k) (index ?vs v))⇧+  } ∪ { (Operator k (index ?ops op))⇧+
    | op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op) }}"
    by force
  (* TODO slow. *)
  then have "cnf ((❙¬(Atom (State k (index ?vs v))) ❙∨ (Atom (State (Suc k) (index ?vs v)) ❙∨ ❙⋁?fs)))
    = {{ (State k (index ?vs v))¯ }
      ∪ { (State (Suc k) (index ?vs v))⇧+ }
      ∪ { (Operator k (index ?ops op))⇧+ | op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op) }}"
    by simp
  (* TODO unfold Let_def + remove metis. *)
  moreover have "cnf (encode_negative_transition_frame_axiom Π k v)
    = cnf ((❙¬(Atom (State k (index ?vs v))) ❙∨ (Atom (State (Suc k) (index ?vs v)) ❙∨ ❙⋁?fs)))"
    unfolding encode_negative_transition_frame_axiom_def
    by metis
  (* TODO slow. *)
  ultimately show ?thesis
    by blast
qed

lemma cnf_of_encode_all_frame_axioms_structure:
  "cnf (encode_all_frame_axioms Π t)
    = ⋃(⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        {{{ (State k (index (strips_problem.variables_of  Π) v))⇧+
            , (State (Suc k) (index (strips_problem.variables_of  Π) v))¯  }
          ∪ {(Operator k (index (strips_problem.operators_of  Π) op))⇧+
            | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (add_effects_of op) }}})
      ∪ ⋃(⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        {{{ (State k (index (strips_problem.variables_of Π) v))¯
            , (State (Suc k) (index (strips_problem.variables_of Π) v))⇧+ }
          ∪ { (Operator k (index (strips_problem.operators_of Π) op))⇧+
            | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (delete_effects_of op) }}})"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
    and ?Φ⇩F = "encode_all_frame_axioms Π t"
  let ?l = "List.product [0..<t] ?vs"
  let ?fs = "map (λ(k, v). encode_negative_transition_frame_axiom Π k v) ?l
    @ map (λ(k, v). encode_positive_transition_frame_axiom Π k v) ?l"
  {
    let ?A = "{ encode_negative_transition_frame_axiom Π k v
        | k v. (k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)) }"
      and ?B = "{ encode_positive_transition_frame_axiom Π k v
        | k v. (k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)) }"
    have set_l: "set ?l = {..<t} × set ((Π)⇩𝒱)"
      using set_product
      by force
    (* TODO slow *)
    have "set ?fs = ?A ∪ ?B"
      unfolding set_append set_map
      using encode_all_frame_axioms_set
      by force
    then have "cnf ` set ?fs = cnf ` ?A ∪ cnf ` ?B"
      using image_Un[of cnf "?A" "?B"]
      by argo
    moreover {
      have "?A = (⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        { encode_negative_transition_frame_axiom Π k v })"
        by blast
      then have  "cnf ` ?A  = (⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        { cnf (encode_negative_transition_frame_axiom Π k v) })"
        by blast
      hence "cnf ` ?A = (⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        {{{ (State k (index ?vs v))¯
            , (State (Suc k) (index ?vs v))⇧+ }
          ∪ {(Operator k (index ?ops op))⇧+
            | op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op)}}})"
        using cnf_of_negative_transition_frame_axiom[of Π]
        by presburger
    }
    moreover {
      have "?B = (⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        { encode_positive_transition_frame_axiom Π k v})"
        by blast
      then have  "cnf ` ?B = (⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        { cnf (encode_positive_transition_frame_axiom Π k v)  })"
        by blast
      hence "cnf ` ?B = (⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        {{{ (State k (index ?vs v))⇧+
            , (State (Suc k) (index ?vs v))¯ }
          ∪ {(Operator k (index ?ops op))⇧+
            | op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }}})"
        using cnf_of_positive_transition_frame_axiom[of Π]
        by presburger
    }
    (* TODO slow *)
    ultimately have "cnf ` set ?fs
      = (⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        {{{ (State k (index ?vs v))⇧+
            , (State (Suc k) (index ?vs v))¯ }
          ∪ {(Operator k (index ?ops op))⇧+
            | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (add_effects_of op) }}})
      ∪ (⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        {{{ (State k (index ?vs v))¯
            , (State (Suc k) (index ?vs v))⇧+ }
          ∪ {(Operator k (index ?ops op))⇧+
            | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (delete_effects_of op)}}})"
      unfolding set_append set_map
      by force
  }
  then have "cnf (encode_all_frame_axioms Π t)
    = ⋃((⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        {{{ (State k (index ?vs v))⇧+
            , (State (Suc k) (index ?vs v))¯ }
          ∪ {(Operator k (index ?ops op))⇧+
            | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (add_effects_of op) }}})
      ∪ (⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        {{{ (State k (index ?vs v))¯
            , (State (Suc k) (index ?vs v))⇧+ }
          ∪ {(Operator k (index ?ops op))⇧+
            | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (delete_effects_of op)}}}))"
    unfolding encode_all_frame_axioms_def Let_def
    using cnf_BigAnd[of ?fs]
    by argo
  thus ?thesis
    using Union_Un_distrib[of
        "(⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        {{{ (State k (index ?vs v))⇧+
            ,  (State (Suc k) (index ?vs v))¯ }
          ∪ {(Operator k (index ?ops op))⇧+
            | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (add_effects_of op) }}})"
        "(⋃(k, v) ∈ ({0..<t} × set ((Π)⇩𝒱)).
        {{{ (State k (index ?vs v))¯
            , (State (Suc k) (index ?vs v))⇧+ }
          ∪ {(Operator k (index ?ops op))⇧+
            | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (delete_effects_of op)}}})"]
    by argo
qed

― ‹ A technical lemma used in \isaname{cnf_of_encode_goal_state_set}. ›
private lemma cnf_of_encode_goal_state_set_i:
    "cnf ((Φ⇩G Π) t ) = ⋃({ cnf (encode_state_variable t
      (index (strips_problem.variables_of Π) v) (((Π)⇩G) v))
    | v. v ∈ set ((Π)⇩𝒱) ∧ ((Π)⇩G) v ≠ None })"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?G = "(Π)⇩G"
    and ?Φ⇩G = "(Φ⇩G Π) t"
  let ?fs = "map (λv. encode_state_variable t (index ?vs v) (?G v) ❙∨ ⊥)
      (filter (λv. ?G v ≠ None) ?vs)"
  {
    have "cnf ` set ?fs  = cnf ` (λv. encode_state_variable t (index ?vs v) (?G v) ❙∨ ⊥)
      ` { v | v. v ∈ set ?vs ∧ ?G v ≠ None }"
      unfolding set_map
      by force
    also have "… = (λv. cnf (encode_state_variable t (index ?vs v) (?G v) ❙∨ ⊥))
      ` { v | v. v ∈ set ?vs ∧ ?G v ≠ None }"
      using image_comp[of cnf "(λv. encode_state_variable t (index ?vs v) (?G v) ❙∨ ⊥)"
          "{ v | v. v ∈ set ?vs ∧ ?G v ≠ None }"]
      by fast
    finally have "cnf ` set ?fs = { cnf (encode_state_variable t (index ?vs v) (?G v))
        | v. v ∈ set ?vs ∧ ?G v ≠ None }"
      unfolding setcompr_eq_image[of "λv. cnf (encode_state_variable t (index ?vs v) (?G v) ❙∨ ⊥)"]
      by auto
  }
  moreover have "cnf ((Φ⇩G Π) t) = ⋃ (cnf ` set ?fs)"
    unfolding encode_goal_state_def SAT_Plan_Base.encode_goal_state_def Let_def
    using cnf_BigAnd[of ?fs]
    by force
  ultimately show ?thesis
    by simp
qed

― ‹ A simplification lemma for the above one. ›
(* TODO Replace above lemma with this?. *)
corollary cnf_of_encode_goal_state_set_ii:
  assumes "is_valid_problem_strips Π"
  shows "cnf ((Φ⇩G Π) t) = ⋃({{{ literal_formula_to_literal
      (encode_state_variable t (index (strips_problem.variables_of Π) v) (((Π)⇩G) v)) }}
    | v. v ∈ set ((Π)⇩𝒱) ∧ ((Π)⇩G) v ≠ None })"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?G = "(Π)⇩G"
    and ?Φ⇩G = "(Φ⇩G Π) t"
  {
    fix v
    assume "v ∈ { v | v. v ∈ set ((Π)⇩𝒱) ∧ ?G v ≠ None }"
    then have "v ∈ set ((Π)⇩𝒱)" and G_of_v_is_not_None: "?G v ≠ None"
      by fast+
    then consider (A) "?G v = Some True"
      | (B) "?G v = Some False"
      by fastforce
    hence "cnf (encode_state_variable t (index ?vs v) (?G v))
      = {{ literal_formula_to_literal (encode_state_variable t (index ?vs v) (?G v))  }}"
      unfolding encode_state_variable_def
      by (cases, force+)
  } note nb = this
  have  "cnf ?Φ⇩G = ⋃({ cnf (encode_state_variable t (index ?vs v) (?G v))
    | v. v ∈ set ((Π)⇩𝒱) ∧ ?G v ≠ None })"
    unfolding cnf_of_encode_goal_state_set_i
    by blast
  also have "… = ⋃((λv. cnf (encode_state_variable t (index ?vs v) (((Π)⇩G) v)))
    ` { v | v. v ∈ set ((Π)⇩𝒱) ∧ ((Π)⇩G) v ≠ None })"
    using setcompr_eq_image[of
        "λv. cnf (encode_state_variable t (index ?vs v) (((Π)⇩G) v))"
        "λv. v ∈ set ((Π)⇩𝒱) ∧ ((Π)⇩G) v ≠ None"]
    by presburger
  also have "… = ⋃((λv. {{ literal_formula_to_literal
      (encode_state_variable t (index ?vs v) (?G v)) }})
    `  { v. v ∈ set ((Π)⇩𝒱) ∧ ((Π)⇩G) v ≠ None })"
    using nb
    by simp
  finally show ?thesis
    unfolding nb
    by auto
qed

― ‹ This lemma essentially states that the cnf for the cnf formula for the encoding has a
clause for each variable whose state is defined in the goal state with the corresponding literal. ›
(* TODO is ‹∃!› still needed? *)
lemma cnf_of_encode_goal_state_set:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "v ∈ dom ((Π)⇩G)"
  shows "((Π)⇩G) v = Some True ⟶ (∃!C. C ∈ cnf ((Φ⇩G Π) t)
      ∧ C = { (State t (index (strips_problem.variables_of Π) v))⇧+ })"
    and "((Π)⇩G) v = Some False ⟶ (∃!C. C ∈ cnf ((Φ⇩G Π) t)
      ∧ C = { (State t (index (strips_problem.variables_of Π) v))¯ })"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?G = "(Π)⇩G"
    and ?Φ⇩G = "(Φ⇩G Π) t"
  have nb⇩1: "cnf ?Φ⇩G  = ⋃ { cnf (encode_state_variable t (index ?vs v)
      (?G v)) | v. v ∈ set ((Π)⇩𝒱) ∧ ?G v ≠ None }"
    unfolding cnf_of_encode_goal_state_set_i
    by auto
  have nb⇩2: "v ∈ { v. v ∈ set ((Π)⇩𝒱) ∧ ?G v ≠ None }"
    using is_valid_problem_dom_of_goal_state_is assms(1, 2)
    by auto
  have nb⇩3: "cnf (encode_state_variable t (index (strips_problem.variables_of Π) v) (((Π)⇩G) v))
    ⊆ (⋃{ cnf (encode_state_variable t (index ?vs v)
      (?G v)) | v. v ∈ set ((Π)⇩𝒱) ∧ ?G v ≠ None })"
    using UN_upper[OF nb⇩2, of "λv. cnf (encode_state_variable t (index ?vs v) (?G v))"] nb⇩2
    by blast
  show "((Π)⇩G) v = Some True ⟶ (∃!C. C ∈ cnf ((Φ⇩G Π) t)
      ∧ C = { (State t (index (strips_problem.variables_of Π) v))⇧+ })"
    and "((Π)⇩G) v = Some False ⟶ (∃!C. C ∈ cnf ((Φ⇩G Π) t)
      ∧ C = { (State t (index (strips_problem.variables_of Π) v))¯ })"
    using nb⇩3
    unfolding nb⇩1 encode_state_variable_def
    by auto+
qed

end


text ‹ We omit the proofs that the partial encoding functions produce formulas in CNF form due to
their more technical nature.
The following sublocale proof confirms that definition \ref{isadef:encode-problem-sat-plan-base}
encodes a valid problem \<^term>‹Π› into a formula that can be transformed to CNF
(\<^term>‹is_cnf (Φ Π t)›) and that its CNF has the required form. ›


subsection "Soundness of the Basic SATPlan Algorithm"


lemma valuation_models_encoding_cnf_formula_equals:
  assumes "is_valid_problem_strips Π"
  shows "𝒜 ⊨ Φ Π t = cnf_semantics 𝒜 (cnf (Φ Π t))"
proof -
  let ?Φ = "Φ Π t"
  {
    have "is_cnf ?Φ"
      using is_cnf_encode_problem[OF assms].
    hence "is_nnf ?Φ"
      using is_nnf_cnf
      by blast
  }
  thus ?thesis
    using cnf_semantics[of ?Φ 𝒜]
    by blast
qed

(* TODO refactor *)
corollary valuation_models_encoding_cnf_formula_equals_corollary:
  assumes "is_valid_problem_strips Π"
  shows "𝒜 ⊨ (Φ Π t)
    = (∀C ∈ cnf (Φ Π t). ∃L ∈ C. lit_semantics 𝒜 L)"
  using valuation_models_encoding_cnf_formula_equals[OF assms]
  unfolding cnf_semantics_def clause_semantics_def encode_problem_def
  by presburger

― ‹ A couple of technical lemmas about ‹decode_plan›. ›
lemma decode_plan_length:
  assumes "π = Φ¯ Π ν t"
  shows "length π = t"
  using assms
  unfolding decode_plan_def SAT_Plan_Base.decode_plan_def
  by simp

lemma decode_plan'_set_is[simp]:
  "set (decode_plan' Π 𝒜 k)
    = { (strips_problem.operators_of Π) ! (index (strips_problem.operators_of Π) op)
      | op. op ∈ set (strips_problem.operators_of Π)
        ∧ 𝒜 (Operator k (index (strips_problem.operators_of Π) op)) }"
proof -
  let ?ops = "strips_problem.operators_of Π"
  let ?f = "λop. Operator k (index ?ops op)"
  let ?vs = "map ?f ?ops"
  {
    have "set (filter 𝒜 ?vs) = set (map ?f (filter (𝒜 ∘ ?f) ?ops))"
      unfolding filter_map[of 𝒜 "λop. Operator k (index ?ops op)" ?ops]..
    hence "set (filter 𝒜 ?vs) = (λop. Operator k (index ?ops op)) `
      { op ∈ set ?ops. 𝒜 (Operator k (index ?ops op)) }"
      unfolding set_map set_filter
      by simp
  }
  have "set (decode_plan' Π 𝒜 k) = (λv. case v of Operator k i ⇒ ?ops ! i)
    ` (λop. Operator k (index ?ops op)) ` { op ∈ set ?ops. 𝒜 (Operator k (index ?ops op)) }"
    unfolding decode_plan'_def set_map Let_def
    by auto
  also have "… = (λop. case Operator k (index ?ops op) of Operator k i ⇒ ?ops ! i)
    ` { op ∈ set ?ops. 𝒜 (Operator k (index ?ops op)) }"
    unfolding image_comp comp_apply
    by argo
  also have "… = (λop. ?ops ! (index ?ops op))
    ` { op ∈ set ?ops. 𝒜 (Operator k (index ?ops op)) }"
    by force
  finally show ?thesis
    by blast
qed

lemma decode_plan_set_is[simp]:
  "set (Φ¯ Π 𝒜 t) = (⋃k ∈ {..<t}. { decode_plan' Π 𝒜 k })"
  unfolding decode_plan_def SAT_Plan_Base.decode_plan_def set_map
  using atLeast_upt
  by blast

lemma decode_plan_step_element_then_i:
  assumes "k < t"
  shows "set ((Φ¯ Π 𝒜 t) ! k)
    = { (strips_problem.operators_of Π) ! (index (strips_problem.operators_of Π) op)
      | op. op ∈ set ((Π)⇩𝒪) ∧ 𝒜 (Operator k (index (strips_problem.operators_of Π) op)) }"
proof -
  have "(Φ¯ Π 𝒜 t) ! k = decode_plan' Π 𝒜 k"
    unfolding decode_plan_def SAT_Plan_Base.decode_plan_def
    using assms
    by simp
  thus ?thesis
    by force
qed

― ‹ Show that each operator $op$ in the $k$-th parallel operator in a decoded parallel plan is
contained within the problem's operator set and the valuation is true for the corresponding SATPlan
variable. ›
lemma decode_plan_step_element_then:
  fixes Π::"'a strips_problem"
  assumes "k < t"
    and "op ∈ set ((Φ¯ Π 𝒜 t) ! k)"
  shows "op ∈ set ((Π)⇩𝒪)"
    and "𝒜 (Operator k (index (strips_problem.operators_of Π) op))"
proof -
  let ?ops = "strips_problem.operators_of Π"
  let ?Ops = "{ ?ops ! (index ?ops op)
    | op. op ∈ set ((Π)⇩𝒪) ∧ 𝒜 (Operator k (index ?ops op)) }"
  have "op ∈ ?Ops"
    using assms(2)
    unfolding decode_plan_step_element_then_i[OF assms(1)] assms
    by blast
  moreover have "op ∈ set ((Π)⇩𝒪)"
    and "𝒜 (Operator k (index ?ops op))"
    using calculation
    by fastforce+
  ultimately show "op ∈ set ((Π)⇩𝒪)"
    and "𝒜 (Operator k (index ?ops op))"
    by blast+
qed

― ‹ Show that the ‹k›-th parallel operators of the decoded plan are distinct lists (i.e. do not
contain duplicates). ›
lemma decode_plan_step_distinct:
  assumes "k < t"
  shows "distinct ((Φ¯ Π 𝒜 t) ! k)"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?π⇩k = "(Φ¯ Π 𝒜 t) ! k"
  let ?f = "λop. Operator k (index ?ops op)"
    and ?g = "λv. case v of Operator _ k ⇒ ?ops ! k"
  let ?vs = "map ?f (remdups ?ops)"
  have nb⇩1: "?π⇩k = decode_plan' Π 𝒜 k"
    unfolding decode_plan_def SAT_Plan_Base.decode_plan_def
    using assms
    by fastforce
  {
    have "distinct (remdups ?ops)"
      by blast
    moreover have "inj_on ?f (set (remdups ?ops))"
      unfolding inj_on_def
      by fastforce
    ultimately have "distinct ?vs"
      using distinct_map
      by blast
  } note nb⇩2 = this
  {
    have "inj_on ?g (set ?vs)"
      unfolding inj_on_def
      by fastforce
    hence "distinct (map ?g ?vs)"
      using distinct_map nb⇩2
      by blast
  }
  thus ?thesis
    using distinct_map_filter[of ?g ?vs 𝒜]
    unfolding nb⇩1 decode_plan'_def Let_def
    by argo
qed

lemma decode_state_at_valid_variable:
  fixes Π :: "'a strips_problem"
  assumes "(Φ⇩S¯ Π 𝒜 k) v ≠ None"
  shows "v ∈ set ((Π)⇩𝒱)"
proof -
  let ?vs = "strips_problem.variables_of Π"
  let ?f = "λv. (v,𝒜 (State k (index ?vs v)))"
  {
    have "fst ` set (map ?f ?vs) = fst ` (λv. (v,𝒜 (State k (index ?vs v)))) ` set ?vs"
      by force
    also have "… = (λv. fst (v,𝒜 (State k (index ?vs v)))) ` set ?vs"
      by blast
    finally have "fst ` set (map ?f ?vs) = set ?vs"
      by auto
  }
  moreover have "¬v ∉ fst ` set (map ?f ?vs)"
    using map_of_eq_None_iff[of "map ?f ?vs" v] assms
    unfolding decode_state_at_def SAT_Plan_Base.decode_state_at_def
    by meson
  ultimately show ?thesis
    by fastforce
qed

― ‹ Show that there exists an equivalence between a model ‹𝒜› of the (CNF of the) encoded
problem and the state at step ‹k› decoded from the encoded problem. ›
lemma decode_state_at_encoding_variables_equals_some_of_valuation_if:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
    and "k ≤ t"
    and "v ∈ set ((Π)⇩𝒱)"
  shows "(Φ⇩S¯ Π 𝒜 k) v
    = Some (𝒜 (State k (index (strips_problem.variables_of Π) v)))"
proof -
  let ?vs = "strips_problem.variables_of Π"
  let ?l = "map (λx. (x,𝒜 (State k (index ?vs x)))) ?vs"
  have "set ?vs ≠ {}"
    using assms(4)
    by fastforce
  then have "map_of ?l v = Some (𝒜 (State k (index ?vs v)))"
    using map_of_from_function_graph_is_some_if[of ?vs v
        "λv. 𝒜 (State k (index ?vs v))"] assms(4)
    by fastforce
  thus ?thesis
    unfolding decode_state_at_def SAT_Plan_Base.decode_state_at_def
    by meson
qed

lemma decode_state_at_dom:
  assumes "is_valid_problem_strips Π"
  shows "dom (Φ⇩S¯ Π 𝒜 k) = set ((Π)⇩𝒱)"
proof-
  let ?s = "Φ⇩S¯ Π 𝒜 k"
    and ?vs = "strips_problem.variables_of Π"
  have "dom ?s = fst ` set (map (λv. (v, 𝒜 (State k (index ?vs v)))) ?vs)"
    unfolding decode_state_at_def SAT_Plan_Base.decode_state_at_def
    using dom_map_of_conv_image_fst[of "(map (λv. (v, 𝒜 (State k (index ?vs v)))) ?vs)"]
    by meson
  also have "… = fst ` (λv. (v, 𝒜 (State k (index ?vs v)))) ` set ((Π)⇩𝒱)"
    using set_map[of "(λv. (v, 𝒜 (State k (index ?vs v))))" ?vs]
    by simp
  also have "… = (fst ∘ (λv. (v, 𝒜 (State k (index ?vs v))))) ` set ((Π)⇩𝒱)"
    using image_comp[of fst "(λv. (v, 𝒜 (State k (index ?vs v))))"]
    by presburger
  finally show ?thesis
    by force
qed

(* TODO shorten the proof (there are a lot of duplicate parts still!). *)
lemma decode_state_at_initial_state:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
  shows "(Φ⇩S¯ Π 𝒜 0) = (Π)⇩I"
proof -
  let ?I = "(Π)⇩I"
  let ?s = "Φ⇩S¯ Π 𝒜 0"
  let ?vs = "strips_problem.variables_of Π"
  let ?Φ = "Φ Π t"
  let ?Φ⇩I = "Φ⇩I Π"
  {
    have "is_cnf ?Φ⇩I" and "cnf ?Φ⇩I ⊆ cnf ?Φ"
      subgoal
        using is_cnf_encode_initial_state[OF assms(1)]
        by simp
      subgoal
        using cnf_of_encode_problem_structure(1)
        unfolding encode_initial_state_def encode_problem_def
        by blast
      done
    then have "cnf_semantics 𝒜 (cnf ?Φ⇩I)"
      using cnf_semantics_monotonous_in_cnf_subsets_if is_cnf_encode_problem[OF assms(1)]
        assms(2)
      by blast
    hence "∀C ∈ cnf ?Φ⇩I. clause_semantics 𝒜 C"
      unfolding cnf_semantics_def encode_initial_state_def
      by blast
  } note nb⇩1 = this
  {
    (* TODO refactor. *)
    {
      fix v
      assume v_in_dom_i: "v ∈ dom ?I"
      moreover  {
        have v_in_variable_set: "v ∈ set ((Π)⇩𝒱)"
          using is_valid_problem_strips_initial_of_dom assms(1) v_in_dom_i
          by auto
        hence "(Φ⇩S¯ Π 𝒜 0) v = Some (𝒜 (State 0 (index ?vs v)))"
          using decode_state_at_encoding_variables_equals_some_of_valuation_if[OF
              assms(1, 2) _ v_in_variable_set]
          by fast
      } note nb⇩2 = this
      consider (v_initially_true) "?I v = Some True"
        | (v_initially_false) "?I v = Some False"
        using v_in_dom_i
        by fastforce
      hence "?I v = ?s v"
        proof (cases)
          case v_initially_true
          then obtain C
            where "C ∈ cnf ?Φ⇩I"
              and c_is: "C = { (State 0 (index ?vs v))⇧+ }"
            using cnf_of_encode_initial_state_set v_in_dom_i assms(1)
            by fastforce
          hence "𝒜 (State 0 (index ?vs v)) = True"
            using nb⇩1
            unfolding clause_semantics_def
            by fastforce
          thus ?thesis
            using nb⇩2 v_initially_true
            by presburger
        next
          case v_initially_false
          (* TODO slow *)
          then obtain C
            where "C ∈ cnf ?Φ⇩I"
              and c_is: "C = { (State 0 (index ?vs v))¯ }"
            using cnf_of_encode_initial_state_set assms(1) v_in_dom_i
            by fastforce
          hence "𝒜 (State 0 (index ?vs v)) = False"
            using nb⇩1
            unfolding clause_semantics_def
            by fastforce
          thus ?thesis
            using nb⇩2 v_initially_false
            by presburger
        qed
    }
    hence "?I ⊆⇩m ?s"
      using map_le_def
      by blast
  } moreover {
    {
      fix v
      assume v_in_dom_s: "v ∈ dom ?s"
      then have v_in_set_vs: "v ∈ set ?vs"
        using decode_state_at_dom[OF assms(1)]
        by simp
      have v_in_dom_I: "v ∈ dom ?I"
        using is_valid_problem_strips_initial_of_dom assms(1) v_in_set_vs
        by auto
      have s_v_is: "(Φ⇩S¯ Π 𝒜 0) v = Some (𝒜 (State 0 (index ?vs v)))"
        using decode_state_at_encoding_variables_equals_some_of_valuation_if assms(1, 2)
          v_in_set_vs
        by (metis le0)
      consider (s_v_is_some_true) "?s v = Some True"
        | (s_v_is_some_false) "?s v = Some False"
        using v_in_dom_s
        by fastforce
      hence "?s v = ?I v"
        proof (cases)
          case s_v_is_some_true
          then have 𝒜_of_s_v: "lit_semantics 𝒜 ((State 0 (index ?vs v))⇧+)"
            using s_v_is
            by fastforce
          consider (I_v_is_some_true) "?I v = Some True"
            | (I_v_is_some_false) "?I v = Some False"
            using v_in_dom_I
            by fastforce
          thus ?thesis
            proof (cases)
              case I_v_is_some_true
              then show ?thesis
                using s_v_is_some_true
                by argo
            next
              case I_v_is_some_false
              (* TODO slow *)
              then obtain C
                where C_in_encode_initial_state: "C ∈ cnf ?Φ⇩I"
                  and C_is: "C = { (State 0 (index ?vs v))¯  }"
                using cnf_of_encode_initial_state_set assms(1) v_in_dom_I
                by fastforce
              hence "lit_semantics 𝒜 ((State 0 (index ?vs v))¯)"
                using nb⇩1
                unfolding clause_semantics_def
                by fast
              thus ?thesis
                using 𝒜_of_s_v
                by fastforce
            qed
        next
          case s_v_is_some_false
          then have 𝒜_of_s_v: "lit_semantics 𝒜 ((State 0 (index ?vs v))¯)"
            using s_v_is
            by fastforce
          consider (I_v_is_some_true) "?I v = Some True"
            | (I_v_is_some_false) "?I v = Some False"
            using v_in_dom_I
            by fastforce
          thus ?thesis
            proof (cases)
              case I_v_is_some_true
              then obtain C
                where C_in_encode_initial_state: "C ∈ cnf ?Φ⇩I"
                  and C_is: "C = { (State 0 (index ?vs v))⇧+  }"
                using cnf_of_encode_initial_state_set assms(1) v_in_dom_I
                by fastforce
              hence "lit_semantics 𝒜 ((State 0 (index ?vs v))⇧+)"
                using nb⇩1
                unfolding clause_semantics_def
                by fast
              thus ?thesis
                using 𝒜_of_s_v
                by fastforce
            next
              case I_v_is_some_false
              thus ?thesis
                using s_v_is_some_false
                by presburger
            qed
        qed
    }
    hence "?s ⊆⇩m ?I"
      using map_le_def
      by blast
  } ultimately show ?thesis
    using map_le_antisym
    by blast
qed

lemma decode_state_at_goal_state:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
  shows "(Π)⇩G ⊆⇩m Φ⇩S¯ Π 𝒜 t"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?G = "(Π)⇩G"
    and ?G' = "Φ⇩S¯ Π 𝒜 t"
    and ?Φ = "Φ Π t"
    and ?Φ⇩G = "(Φ⇩G Π) t"
  {
    have "is_cnf ?Φ⇩G" and "cnf ?Φ⇩G ⊆ cnf ?Φ"
      subgoal
        using encode_goal_state_is_cnf[OF assms(1)]
        by simp
      subgoal
        using cnf_of_encode_problem_structure(2)
        unfolding encode_goal_state_def encode_problem_def
        by blast
      done
    then have "cnf_semantics 𝒜 (cnf ?Φ⇩G)"
      using cnf_semantics_monotonous_in_cnf_subsets_if is_cnf_encode_problem[OF assms(1)]
        assms(2)
      by blast
    hence "∀C ∈ cnf ?Φ⇩G. clause_semantics 𝒜 C"
      unfolding cnf_semantics_def encode_initial_state_def
      by blast
  } note nb⇩1 = this
  (* TODO refactor. *)
  {
    fix v
    assume "v ∈ set ((Π)⇩𝒱)"
    moreover have "set ?vs ≠ {}"
      using calculation(1)
      by fastforce
    moreover have "(Φ⇩S¯ Π 𝒜 t)
      = map_of (map (λv. (v, 𝒜 (State t (index ?vs v)))) ?vs)"
      unfolding decode_state_at_def SAT_Plan_Base.decode_state_at_def
      by metis
    (* TODO slow. *)
    ultimately have "(Φ⇩S¯ Π 𝒜 t) v = Some (𝒜 (State t (index ?vs v)))"
      using map_of_from_function_graph_is_some_if
      by fastforce
  } note nb⇩2 = this
  {
    fix v
    assume v_in_dom_G: "v ∈ dom ?G"
    then have v_in_vs: "v ∈ set ?vs"
      using is_valid_problem_dom_of_goal_state_is assms(1)
      by auto
    then have decode_state_at_is: "(Φ⇩S¯ Π 𝒜 t) v = Some (𝒜 (State t (index ?vs v)))"
      using nb⇩2
      by fastforce
    consider (A) "?G v = Some True"
      | (B) "?G v = Some False"
      using v_in_dom_G
      by fastforce
    hence "?G v = ?G' v"
      proof (cases)
        case A
        {
          obtain C where "C ⊆ cnf ?Φ⇩G" and "C = {{ (State t (index ?vs v))⇧+ }}"
            using cnf_of_encode_goal_state_set(1)[OF assms(1) v_in_dom_G] A
            by auto
          then have "{ (State t (index ?vs v))⇧+ } ∈ cnf ?Φ⇩G"
            by blast
          then have "clause_semantics 𝒜 { (State t (index ?vs v))⇧+ }"
            using nb⇩1
            by blast
          then have "lit_semantics 𝒜 ((State t (index ?vs v))⇧+)"
            unfolding clause_semantics_def
            by blast
          hence "𝒜 (State t (index ?vs v)) = True"
            by force
        }
        thus ?thesis
          using decode_state_at_is A
          by presburger
      next
        case B
        {
          obtain C where "C ⊆ cnf ?Φ⇩G" and "C = {{ (State t (index ?vs v))¯ }}"
            using cnf_of_encode_goal_state_set(2)[OF assms(1) v_in_dom_G] B
            by auto
          then have "{ (State t (index ?vs v))¯ } ∈ cnf ?Φ⇩G"
            by blast
          then have "clause_semantics 𝒜 { (State t (index ?vs v))¯ }"
            using nb⇩1
            by blast
          then have "lit_semantics 𝒜 ((State t (index ?vs v))¯)"
            unfolding clause_semantics_def
            by blast
          hence "𝒜 (State t (index ?vs v)) = False"
            by simp
        }
        thus ?thesis
          using decode_state_at_is B
          by presburger
    qed
  }
  thus ?thesis
    using map_le_def
    by blast
qed

― ‹ Show that the operator activation implies precondition constraints hold at every time step
of the decoded plan. ›
lemma decode_state_at_preconditions:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
    and "k < t"
    and "op ∈ set ((Φ¯ Π 𝒜 t) ! k)"
    and "v ∈ set (precondition_of op)"
  shows "𝒜 (State k (index (strips_problem.variables_of Π) v))"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?vs = "strips_problem.variables_of Π"
  let ?Φ = "Φ Π t"
    and ?Φ⇩O = "encode_operators Π t"
    and ?Φ⇩P = "encode_all_operator_preconditions Π ?ops t"
  {
    have "𝒜 (Operator k (index ?ops op))"
      and "op ∈ set ((Π)⇩𝒪)"
      using decode_plan_step_element_then[OF assms(3, 4)]
      by blast+
    moreover obtain C
      where clause_is_in_operator_encoding: "C ∈ cnf ?Φ⇩P"
        and "C = { (Operator k (index ?ops op))¯,
        (State k (index ?vs v))⇧+ }"
      using cnf_of_encode_all_operator_preconditions_contains_clause_if[OF assms(1, 3)
          calculation(2) assms(5)]
      by blast
    moreover have clause_semantics_𝒜_Φ⇩P: "∀C ∈ cnf ?Φ⇩P. clause_semantics 𝒜 C"
      using cnf_semantics_monotonous_in_cnf_subsets_if[OF assms(2)
          is_cnf_encode_problem[OF assms(1)]
        cnf_of_operator_precondition_encoding_subset_encoding]
      unfolding cnf_semantics_def
      by blast
    (* TODO slow step *)
    ultimately have "lit_semantics 𝒜 (Pos (State k (index ?vs v)))"
      unfolding clause_semantics_def
      by fastforce
  }
  thus ?thesis
    unfolding lit_semantics_def
    by fastforce
qed

― ‹ This lemma shows that for a problem encoding with makespan zero for which a model exists,
the goal state encoding must be subset of the initial state encoding. In this case, the state
variable encodings for the goal state are included in the initial state encoding. ›
(* TODO simplify/refactor proof. *)
lemma encode_problem_parallel_correct_i:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π 0"
  shows "cnf ((Φ⇩G Π) 0) ⊆ cnf (Φ⇩I Π)"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?I = "(Π)⇩I"
    and ?G = "(Π)⇩G"
    and ?Φ⇩I = "Φ⇩I Π"
    and ?Φ⇩G = "(Φ⇩G Π) 0"
    and ?Φ = "Φ Π 0"
  (* TODO refactor and generalize for all partial encodings? *)
  ― ‹ Show that the model of the encoding is also a model of the partial encodings. ›
  have 𝒜_models_Φ⇩I: "𝒜 ⊨ ?Φ⇩I" and 𝒜_models_Φ⇩G: "𝒜 ⊨ ?Φ⇩G"
    using assms(2) encode_problem_has_model_then_also_partial_encodings(1, 2)
    unfolding encode_problem_def encode_initial_state_def encode_goal_state_def
    by blast+
  ― ‹ Show that every clause in the CNF of the goal state encoding @{text "Φ⇩G"} is also in
  the CNF of the initial state encoding @{text "Φ⇩I"} thus making it a subset. We can conclude this
  from the fact that both @{text "Φ⇩I"} and @{text "Φ⇩G"} contain singleton clauses---which must all
  be evaluated to true by the given model ‹𝒜›---and the similar structure of the clauses in both
  partial encodings.

  By extension, if we decode the goal state @{text "G"} and the initial state @{text "I"} from a
  model of the encoding,  @{text "G v = I v"} must hold for variable @{text "v"} in the domain of
  the goal state. ›
  {
    fix C'
    assume C'_in_cnf_Φ⇩G: "C' ∈ cnf ?Φ⇩G"
    then obtain v
      where v_in_vs: "v ∈ set ?vs"
        and G_of_v_is_not_None: "?G v ≠ None"
        and C'_is: "C' = { literal_formula_to_literal (encode_state_variable 0 (index ?vs v)
          (?G v)) }"
      using cnf_of_encode_goal_state_set_ii[OF assms(1)]
      by auto
    obtain C
      where C_in_cnf_Φ⇩I: "C ∈ cnf ?Φ⇩I"
        and C_is: "C = { literal_formula_to_literal (encode_state_variable 0 (index ?vs v)
          (?I v)) }"
      using cnf_of_encode_initial_state_set_ii[OF assms(1)] v_in_vs
      by auto
    {
      let ?L = "literal_formula_to_literal (encode_state_variable 0 (index ?vs v) (?I v))"
      have "{ ?L } ∈ cnf ?Φ⇩I"
        using C_in_cnf_Φ⇩I C_is
        by blast
      hence "lit_semantics 𝒜 ?L"
        using model_then_all_singleton_clauses_modelled[OF
            is_cnf_encode_initial_state[OF assms(1)]_ 𝒜_models_Φ⇩I]
        by blast
    } note lit_semantics_𝒜_L = this
    {
      let ?L' = "literal_formula_to_literal (encode_state_variable 0 (index ?vs v) (?G v))"
      have "{ ?L' } ∈ cnf ?Φ⇩G"
        using C'_in_cnf_Φ⇩G C'_is
        by blast
      hence "lit_semantics 𝒜 ?L'"
        using model_then_all_singleton_clauses_modelled[OF
            encode_goal_state_is_cnf[OF assms(1)]_ 𝒜_models_Φ⇩G]
        by blast
    } note lit_semantics_𝒜_L' = this
    {
      have "?I v = ?G v"
        proof (rule ccontr)
          assume contradiction: "?I v ≠ ?G v"
          moreover have "?I v ≠ None"
            using v_in_vs is_valid_problem_strips_initial_of_dom assms(1)
            by auto
          ultimately consider (A) "?I v = Some True ∧ ?G v = Some False"
            | (B) "?I v = Some False ∧ ?G v = Some True"
            using G_of_v_is_not_None
            by force
          thus False
            using lit_semantics_𝒜_L lit_semantics_𝒜_L'
            unfolding encode_state_variable_def
            by (cases, fastforce+)
        qed
    }
    hence "C' ∈ cnf ?Φ⇩I"
      using C_is C_in_cnf_Φ⇩I C'_is C'_in_cnf_Φ⇩G
      by argo
  }
  thus ?thesis
    by blast
qed

― ‹ Show that the encoding secures that for every parallel operator ‹ops›
decoded from the plan at every time step ‹t < length pi› the following hold:
\begin{enumerate}
\item  ‹ops› is applicable, and
\item the effects of ‹ops› are consistent.
\end{enumerate}›
lemma encode_problem_parallel_correct_ii:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
    and "k < length (Φ¯ Π 𝒜 t)"
  shows "are_all_operators_applicable (Φ⇩S¯ Π 𝒜 k)
    ((Φ¯ Π 𝒜 t) ! k)"
    and "are_all_operator_effects_consistent ((Φ¯ Π 𝒜 t) ! k)"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
    and ?π = "Φ¯ Π 𝒜 t"
    and ?s = "Φ⇩S¯ Π 𝒜 k"
  let ?Φ = "Φ Π t"
    and ?Φ⇩E = "encode_all_operator_effects Π ?ops t"
  have k_lt_t: "k < t"
    using decode_plan_length assms(3)
    by metis
  {
    {
      fix op v
      assume op_in_kth_of_decoded_plan_set: "op ∈ set (?π ! k)"
        and v_in_precondition_set: "v ∈ set (precondition_of op)"
      {
        have "𝒜 (Operator k (index ?ops op))"
          using decode_plan_step_element_then[OF k_lt_t op_in_kth_of_decoded_plan_set]
          by blast
        hence "𝒜 (State k (index ?vs v))"
          using decode_state_at_preconditions[
              OF assms(1, 2) _ op_in_kth_of_decoded_plan_set v_in_precondition_set] k_lt_t
          by blast
      }
      moreover have "k ≤ t"
        using k_lt_t
        by auto
      moreover {
        have "op ∈ set ((Π)⇩𝒪)"
          using decode_plan_step_element_then[OF k_lt_t op_in_kth_of_decoded_plan_set]
          by simp
        then have  "v ∈ set ((Π)⇩𝒱)"
          using is_valid_problem_strips_operator_variable_sets(1) assms(1)
            v_in_precondition_set
          by auto
      }
      ultimately have "(Φ⇩S¯ Π 𝒜 k) v = Some True"
        using decode_state_at_encoding_variables_equals_some_of_valuation_if[OF assms(1, 2)]
        by presburger
    }
    hence "are_all_operators_applicable ?s (?π ! k)"
      using are_all_operators_applicable_set[of ?s "?π ! k"]
      by blast
  } moreover {
    {
      fix op⇩1 op⇩2
      assume op⇩1_in_k_th_of_decoded_plan: "op⇩1 ∈ set ((Φ¯ Π 𝒜 t) ! k)"
        and op⇩2_in_k_th_of_decoded_plan: "op⇩2 ∈ set ((Φ¯ Π 𝒜 t) ! k)"
      have op⇩1_in_set_ops: "op⇩1 ∈ set ((Π)⇩𝒪)"
        and op⇩2_in_set_ops: "op⇩2 ∈ set ((Π)⇩𝒪)"
        and op⇩1_active_at_k: "¬lit_semantics 𝒜 ((Operator k (index ?ops op⇩1))¯)"
        and op⇩2_active_at_k: "¬lit_semantics 𝒜 ((Operator k (index ?ops op⇩2))¯)"
        subgoal
          using decode_plan_step_element_then[OF k_lt_t op⇩1_in_k_th_of_decoded_plan]
          by simp
        subgoal
          using decode_plan_step_element_then[OF k_lt_t op⇩2_in_k_th_of_decoded_plan]
          by force
        subgoal
          using decode_plan_step_element_then[OF k_lt_t op⇩1_in_k_th_of_decoded_plan]
          by simp
        subgoal
          using decode_plan_step_element_then[OF k_lt_t op⇩2_in_k_th_of_decoded_plan]
          by simp
        done
      (* TODO the following two blocks could be contracted and refactored into a single lemma. *)
      {
        fix v
        assume v_in_add_effects_set_of_op⇩1: "v ∈ set (add_effects_of op⇩1)"
          and  v_in_delete_effects_set_of_op⇩2: "v ∈ set (delete_effects_of op⇩2)"
        let ?C⇩1 = "{(Operator k (index ?ops op⇩1))¯,
          (State (Suc k) (index ?vs v))⇧+}"
          and ?C⇩2 = "{(Operator k (index ?ops op⇩2))¯,
          (State (Suc k) (index ?vs v))¯}"
        have "?C⇩1 ∈ cnf ?Φ⇩E" and "?C⇩2 ∈ cnf ?Φ⇩E"
          subgoal
            using cnf_of_operator_effect_encoding_contains_add_effect_clause_if[OF
                assms(1) k_lt_t op⇩1_in_set_ops v_in_add_effects_set_of_op⇩1]
            by blast
          subgoal
            using cnf_of_operator_effect_encoding_contains_delete_effect_clause_if[OF
                assms(1) k_lt_t op⇩2_in_set_ops v_in_delete_effects_set_of_op⇩2]
            by blast
          done
        then have "?C⇩1 ∈ cnf ?Φ" and "?C⇩2 ∈ cnf ?Φ"
          using cnf_of_encode_all_operator_effects_subset_cnf_of_encode_problem
          by blast+
        then have C⇩1_true: "clause_semantics 𝒜 ?C⇩1" and C⇩2_true: "clause_semantics 𝒜 ?C⇩2"
          using valuation_models_encoding_cnf_formula_equals[OF assms(1)] assms(2)
          unfolding cnf_semantics_def
          by blast+
        have "lit_semantics 𝒜 ((State (Suc k) (index ?vs v))⇧+)"
          and "lit_semantics 𝒜 ((State (k + 1) (index ?vs v))¯)"
          subgoal
            using op⇩1_active_at_k C⇩1_true
            unfolding clause_semantics_def
            by blast
          subgoal
            using op⇩2_active_at_k C⇩2_true
            unfolding clause_semantics_def
            by fastforce
          done
        hence False
          by auto
      } moreover {
        fix v
        assume v_in_delete_effects_set_of_op⇩1: "v ∈ set (delete_effects_of op⇩1)"
          and  v_in_add_effects_set_of_op⇩2: "v ∈ set (add_effects_of op⇩2)"
        let ?C⇩1 = "{(Operator k (index ?ops op⇩1))¯, (State (Suc k) (index ?vs v))¯}"
          and ?C⇩2 = "{(Operator k (index ?ops op⇩2))¯, (State (Suc k) (index ?vs v))⇧+}"
        have "?C⇩1 ∈ cnf ?Φ⇩E" and "?C⇩2 ∈ cnf ?Φ⇩E"
          subgoal
            using cnf_of_operator_effect_encoding_contains_delete_effect_clause_if[OF
                assms(1) k_lt_t op⇩1_in_set_ops v_in_delete_effects_set_of_op⇩1]
            by fastforce
          subgoal
            using cnf_of_operator_effect_encoding_contains_add_effect_clause_if[OF
                assms(1) k_lt_t op⇩2_in_set_ops v_in_add_effects_set_of_op⇩2]
            by simp
          done
        then have "?C⇩1 ∈ cnf ?Φ" and "?C⇩2 ∈ cnf ?Φ"
          using cnf_of_encode_all_operator_effects_subset_cnf_of_encode_problem
          by blast+
        then have C⇩1_true: "clause_semantics 𝒜 ?C⇩1" and C⇩2_true: "clause_semantics 𝒜 ?C⇩2"
          using valuation_models_encoding_cnf_formula_equals[OF assms(1)] assms(2)
          unfolding cnf_semantics_def
          by blast+
        have "lit_semantics 𝒜 ((State (Suc k) (index ?vs v))¯)"
          and "lit_semantics 𝒜 ((State (k + 1) (index ?vs v))⇧+)"
          subgoal
            using op⇩1_active_at_k C⇩1_true
            unfolding clause_semantics_def
            by blast
          subgoal
            using op⇩2_active_at_k  C⇩2_true
            unfolding clause_semantics_def
            by fastforce
          done
        hence False
          by simp
      }
      ultimately have "set (add_effects_of op⇩1) ∩ set (delete_effects_of op⇩2) = {}"
        and "set (delete_effects_of op⇩1) ∩ set (add_effects_of op⇩2) = {}"
        by blast+
    }
    hence "are_all_operator_effects_consistent (?π ! k)"
      using are_all_operator_effects_consistent_set[of "?π ! k"]
      by blast
  }
  ultimately show "are_all_operators_applicable ?s (?π ! k)"
    and "are_all_operator_effects_consistent (?π ! k)"
    by blast+
qed

― ‹ Show that for all operators ‹op› at timestep ‹k› of the plan
‹Φ¯ Π 𝒜 t› decoded from the model ‹𝒜›, both add effects as
well as delete effects will hold in the next timestep ‹Suc k›. ›
lemma encode_problem_parallel_correct_iii:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
    and "k < length (Φ¯ Π 𝒜 t)"
    and "op ∈ set ((Φ¯ Π 𝒜 t) ! k)"
  shows "v ∈ set (add_effects_of op)
    ⟶ (Φ⇩S¯ Π 𝒜 (Suc k)) v = Some True"
  and "v ∈ set (delete_effects_of op)
    ⟶ (Φ⇩S¯ Π 𝒜 (Suc k)) v = Some False"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?vs = "strips_problem.variables_of Π"
  let ?Φ⇩F = "encode_all_operator_effects Π ?ops t"
    and ?A = "(⋃(t, op)∈{0..<t} × set ((Π)⇩𝒪).
      {{{ (Operator t (index ?ops op))¯, (State (Suc t) (index ?vs v))⇧+ }}
        | v. v ∈ set (add_effects_of op)})"
    and ?B = "(⋃(t, op)∈{0..<t} × set ((Π)⇩𝒪).
       {{{ (Operator t (index ?ops op))¯,
          (State (Suc t) (index ?vs v))¯ }}
        | v. v ∈ set (delete_effects_of op)})"
  have k_lt_t: "k < t"
    using decode_plan_length assms(3)
    by metis
  have op_is_valid: "op ∈ set ((Π)⇩𝒪)"
    using decode_plan_step_element_then[OF k_lt_t assms(4)]
    by blast
  have k_op_included: "(k, op) ∈ ({0..<t} × set ((Π)⇩𝒪))"
    using k_lt_t op_is_valid
    by fastforce
  thus  "v ∈ set (add_effects_of op)
    ⟶ (Φ⇩S¯ Π 𝒜 (Suc k)) v = Some True"
    and "v ∈ set (delete_effects_of op)
      ⟶ (Φ⇩S¯ Π 𝒜 (Suc k)) v = Some False"
    proof (auto)
      assume v_is_add_effect: "v ∈ set (add_effects_of op)"
      have "𝒜 (Operator k (index ?ops op))"
        using decode_plan_step_element_then[OF k_lt_t assms(4)]
        by blast
      moreover {
        have "{{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+}}
          ∈ {{{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+}}
            | v. v ∈ set (add_effects_of op)}"
          using v_is_add_effect
          by blast
        (* TODO slow. *)
        then have "{{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+}} ∈ ?A"
          using k_op_included cnf_of_operator_encoding_structure
            UN_iff[of "{{(Operator t (index ?ops op))¯, (State (Suc t) (index ?vs v))⇧+}}"
              _ "{0..<t} × set ((Π)⇩𝒪)"]
          by blast
        (* TODO slow. *)
        then have "{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+} ∈ ⋃ ?A"
          using Union_iff[of "{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+}"]
          by blast
        (* TODO slow. *)
        moreover have "⋃?A ⊆ cnf ?Φ⇩F"
          using cnf_of_encode_all_operator_effects_structure
          by blast
        ultimately have "{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+} ∈ cnf ?Φ⇩F"
          using in_mono[of "⋃?A" "cnf ?Φ⇩F"]
          by presburger
      }
      (* TODO slow. *)
      ultimately have "𝒜 (State (Suc k) (index ?vs v))"
        using cnf_of_encode_all_operator_effects_subset_cnf_of_encode_problem
              assms(2)[unfolded valuation_models_encoding_cnf_formula_equals_corollary[OF assms(1)]]
        unfolding Bex_def
        by fastforce
      thus "(Φ⇩S¯ Π 𝒜 (Suc k)) v = Some True"
        using assms(1) assms(2)
          decode_state_at_encoding_variables_equals_some_of_valuation_if
          is_valid_problem_strips_operator_variable_sets(2) k_lt_t op_is_valid subsetD
          v_is_add_effect
        by fastforce
    next
      assume v_is_delete_effect: "v ∈ set (delete_effects_of op)"
      have "𝒜 (Operator k (index ?ops op))"
        using decode_plan_step_element_then[OF k_lt_t assms(4)]
        by blast
      moreover {
        have "{{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯}}
          ∈ {{{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯}}
            | v. v ∈ set (delete_effects_of op)}"
          using v_is_delete_effect
          by blast
        (* TODO slow. *)
        then have "{{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯}} ∈ ?B"
          using k_op_included cnf_of_encode_all_operator_effects_structure
            UN_iff[of "{{(Operator t (index ?ops op))¯, (State (Suc t) (index ?vs v))⇧+}}"
              _ "{0..<t} × set ((Π)⇩𝒪)"]
          by blast
        (* TODO slow. *)
        then have "{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯} ∈ ⋃ ?B"
          using Union_iff[of "{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯}"]
          by blast
        (* TODO slow. *)
        moreover have "⋃?B ⊆ cnf ?Φ⇩F"
          using cnf_of_encode_all_operator_effects_structure Un_upper2[of "⋃?B" "⋃?A"]
          by fast
        ultimately have "{(Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯} ∈ cnf ?Φ⇩F"
          using in_mono[of "⋃?B" "cnf ?Φ⇩F"]
          by presburger
      }
      (* TODO slow. *)
      ultimately have "¬𝒜 (State (Suc k) (index ?vs v))"
        using cnf_of_encode_all_operator_effects_subset_cnf_of_encode_problem
          valuation_models_encoding_cnf_formula_equals_corollary[OF assms(1)] assms(2)
        by fastforce
      moreover have "Suc k ≤ t"
        using k_lt_t
        by fastforce
      moreover have "v ∈ set((Π)⇩𝒱)"
        using v_is_delete_effect is_valid_problem_strips_operator_variable_sets(3) assms(1)
            op_is_valid
        by auto
      ultimately show "(Φ⇩S¯ Π 𝒜 (Suc k)) v = Some False"
        using decode_state_at_encoding_variables_equals_some_of_valuation_if[OF assms(1, 2)]
        by auto
    qed
qed

― ‹ In broad strokes, this lemma shows that the operator frame axioms ensure that state is
propagated---i.e. the valuation of a variable does not change inbetween time steps---, if there is
no operator active which has an effect on a given variable a: i.e.

  \begin{align*}
    \mathcal A &\vDash (\lnot a_i \land a_{i+1})
      \longrightarrow \bigvee\{op_i, k: op_i \text{ has add effect } a\}\\
    \mathcal A &\vDash (a_i \land \lnot a_{i+1})
      \longrightarrow \bigvee\{op_i, k: op_i \text{ has delete effect } a\}
  \end{align*}

Now, if the disjunctions are empty---i.e. if no operator which is activated at time step $k$ has
either a positive or negative effect---, we have by simplification

  \begin{align*}
    \mathcal A \vDash \lnot(\lnot a_i \land a_{i+1})
      &\equiv \mathcal A \vDash a_i \lor \lnot a_{i+1}\\
    \mathcal A \vDash \lnot(a_i \land \lnot a_{i+1})
      &\equiv \mathcal A \vDash \lnot a_i \lor a_{i+1}
  \end{align*}

hence

   \begin{align*}
      \mathcal A &\vDash (\lnot a_i \lor a_{i+1}) \land (a_i \lor \lnot a_{i+1})\\
      \leadsto \mathcal A &\vDash \{\{\lnot a_i, a_{i+1}\}, \{a_i, \lnot a_{i+1}\}\}
    \end{align*}

The lemma characterizes this simplification.
\footnote{This part of the soundness proof is only treated very briefly in
\cite[theorem 3.1, p.1044]{DBLP:journals/ai/RintanenHN06}} ›
lemma encode_problem_parallel_correct_iv:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
    and "k < t"
    and "v ∈ set ((Π)⇩𝒱)"
    and "¬(∃op ∈ set ((Φ¯ Π 𝒜 t) ! k).
      v ∈ set (add_effects_of op) ∨ v ∈ set (delete_effects_of op))"
  shows "cnf_semantics 𝒜 {{ (State k (index (strips_problem.variables_of Π) v))¯
    , (State (Suc k) (index (strips_problem.variables_of Π) v))⇧+ }}"
    and "cnf_semantics 𝒜 {{ (State k (index (strips_problem.variables_of Π) v))⇧+
      , (State (Suc k) (index (strips_problem.variables_of Π) v))¯ }}"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
  let ?Φ = "Φ Π t"
    and ?Φ⇩F = "encode_all_frame_axioms Π t"
    and ?π⇩k = "(Φ¯ Π 𝒜 t) ! k"
    and ?A = "⋃(k, v) ∈ ({0..<t} × set ?vs).
      {{{ (State k (index ?vs v))⇧+, (State (Suc k) (index ?vs v))¯  }
        ∪ {(Operator k (index ?ops op))⇧+ | op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }}}"
    and ?B = "⋃(k, v) ∈ ({0..<t} × set ?vs).
      {{{ (State k (index ?vs v))¯, (State (Suc k) (index ?vs v))⇧+ }
        ∪ { (Operator k (index ?ops op))⇧+ | op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op) }}}"
    and ?C = "{ (State k (index ?vs v))⇧+, (State (Suc k) (index ?vs v))¯  }
        ∪ {(Operator k (index ?ops op))⇧+ | op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }"
    and ?C' = "{ (State k (index ?vs v))¯, (State (Suc k) (index ?vs v))⇧+ }
        ∪ { (Operator k (index ?ops op))⇧+ | op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op) }"
    (* TODO refactor (next two blocks)? *)
  have k_v_included: "(k, v) ∈ ({..<t} × set ((Π)⇩𝒱))"
    using assms(3, 4)
    by blast
  have operator_encoding_subset_encoding: "cnf ?Φ⇩F ⊆ cnf ?Φ"
    using cnf_of_encode_problem_structure(4)
    unfolding encode_problem_def
    by fast
  ― ‹ Given the premise that no operator in ‹π⇩k› exists with add-effect respectively delete
effect ‹v›, we have the following situation for the EPC (effect precondition) sets:
  \begin{itemize}
    \item assuming ‹op› is in ‹set ?ops›, either ‹op› is in ‹π⇩k› (then it doesn't have effect on ‹v›
      and therefore is not in either of the sets), or if is not, then
      ‹𝒜 (Operator k (index ?ops op) = ⊥› by definition of ‹decode_plan›; moreover,
    \item assuming ‹op› is not in ‹set ?ops›---this is implicitely encoded as ‹Operator k
      (length ?ops)› and ‹𝒜 (Operator k (length ?ops))› may or may not be true---, then it's not
      in either of the sets.
  \end{itemize}.
Altogether, we have the situation that the sets only have members ‹Operator k (index ?ops op)›
with ‹𝒜 (Operator k (index ?ops op)) = ⊥›, hence the clause can be reduced to the state
variable literals.

More concretely, the following proof block shows that the following two conditions hold for the
operators:

  @{text[display, indent=4] "∀op. op ∈ { ((Operator k (index ?ops op))⇧+)
      | op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op)}
    ⟶ ¬lit_semantics 𝒜 op" }

and

  @{text[display, indent=4] "∀op. op ∈ { ((Operator k (index ?ops op))⇧+)
      | op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op)}
    ⟶ ¬lit_semantics 𝒜 op" }

Hence, the operators are irrelevant for ‹cnf_semantics 𝒜 { C }› where ‹C› is
a clause encoding a positive or negative transition frame axiom for a given variable ‹v› of the
problem. ›
  (* TODO refactor. *)
  {
    let ?add = "{ ((Operator k (index ?ops op))⇧+)
        | op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }"
      and ?delete = "{ ((Operator k (index ?ops op))⇧+)
        | op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op) }"
    {
      fix op
      assume operator_encoding_in_add: "(Operator k (index ?ops op))⇧+ ∈ ?add"
      hence "¬lit_semantics 𝒜 ((Operator k (index ?ops op))⇧+)"
        proof (cases "op ∈ set ?π⇩k")
          case True
          then have "v ∉ set (add_effects_of op)"
            using assms(5)
            by simp
          then have "(Operator k (index ?ops op))⇧+ ∉ ?add"
            by fastforce
          thus ?thesis
            using operator_encoding_in_add
            by blast
        next
          case False
          then show ?thesis
            proof (cases "op ∈ set ?ops")
              case True
              {
                let ?A = "{ ?ops ! index ?ops op |op.
                   op ∈ set ((Π)⇩𝒪) ∧ 𝒜 (Operator k (index ?ops op))}"
                assume "lit_semantics 𝒜 ((Operator k (index ?ops op))⇧+)"
                moreover have operator_active_at_k: "𝒜 (Operator k (index ?ops op))"
                  using calculation
                  by auto
                moreover have "op ∈ set ((Π)⇩𝒪)"
                  using True
                  by force
                moreover have "(?ops ! index ?ops op) ∈ ?A"
                  using calculation(2, 3)
                  by blast
                ultimately have "op ∈ set ?π⇩k"
                  using decode_plan_step_element_then_i[OF assms(3)]
                  by auto
                hence False
                  using False
                  by blast
              }
              thus ?thesis
                by blast
            next
              case False
              then have "op ∉ {op ∈ set ?ops. v ∈ set (add_effects_of op)}"
                by blast
              moreover have "?add =
                (λop. (Operator k (index ?ops op))⇧+)
                  ` { op ∈ set ?ops. v ∈ set (add_effects_of op) }"
                using setcompr_eq_image[of "λop. (Operator k (index ?ops op))⇧+"
                    "λop. op ∈ set ?ops ∧ v ∈ set (add_effects_of op)"]
                by blast
              (* TODO slow. *)
              ultimately have "(Operator k (index ?ops op))⇧+ ∉ ?add"
                by force
              thus ?thesis using operator_encoding_in_add
                by blast
            qed
        qed
    } moreover {
      fix op
      assume operator_encoding_in_delete: "((Operator k (index ?ops op))⇧+) ∈ ?delete"
      hence "¬lit_semantics 𝒜 ((Operator k (index ?ops op))⇧+)"
        proof (cases "op ∈ set ?π⇩k")
          case True
          then have "v ∉ set (delete_effects_of op)"
            using assms(5)
            by simp
          then have "(Operator k (index ?ops op))⇧+ ∉ ?delete"
            by fastforce
          thus ?thesis
            using operator_encoding_in_delete
            by blast
        next
          case False
          then show ?thesis
            proof (cases "op ∈ set ?ops")
              case True
              {
                let ?A = "{ ?ops ! index ?ops op |op.
                   op ∈ set ((Π)⇩𝒪) ∧ 𝒜 (Operator k (index ?ops op))}"
                assume "lit_semantics 𝒜 ((Operator k (index ?ops op))⇧+)"
                moreover have operator_active_at_k: "𝒜 (Operator k (index ?ops op))"
                  using calculation
                  by auto
                moreover have "op ∈ set ((Π)⇩𝒪)"
                  using True
                  by force
                moreover have "(?ops ! index ?ops op) ∈ ?A"
                  using calculation(2, 3)
                  by blast
                ultimately have "op ∈ set ?π⇩k"
                  using decode_plan_step_element_then_i[OF assms(3)]
                  by auto
                hence False
                  using False
                  by blast
              }
              thus ?thesis
                by blast
            next
              case False
              then have "op ∉ { op ∈ set ?ops. v ∈ set (delete_effects_of op) }"
                by blast
              moreover have "?delete =
                (λop. (Operator k (index ?ops op))⇧+)
                  ` { op ∈ set ?ops. v ∈ set (delete_effects_of op) }"
                using setcompr_eq_image[of "λop. (Operator k (index ?ops op))⇧+"
                    "λop. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op)"]
                by blast
              (* TODO slow. *)
              ultimately have "(Operator k (index ?ops op))⇧+ ∉ ?delete"
                by force
              thus ?thesis using operator_encoding_in_delete
                by blast
            qed
        qed
    }
    ultimately have "∀op. op ∈ ?add ⟶ ¬lit_semantics 𝒜 op"
    and "∀op. op ∈ ?delete ⟶ ¬lit_semantics 𝒜 op"
      by blast+
  } note nb = this
  {
    let ?Ops = "{ (Operator k (index ?ops op))⇧+
      | op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }"
    have "?Ops ⊆ ?C"
      by blast
    moreover have "?C - ?Ops = { (State k (index ?vs v))⇧+ , (State (Suc k) (index ?vs v))¯  }"
      by fast
    moreover have "∀L ∈ ?Ops. ¬ lit_semantics 𝒜 L"
      using nb(1)
      by blast
    (* TODO slow. *)
    ultimately have "clause_semantics 𝒜 ?C
      = clause_semantics 𝒜 { (State k (index ?vs v))⇧+, (State (Suc k) (index ?vs v))¯ }"
      using lit_semantics_reducible_to_subset_if[of ?Ops ?C]
      by presburger
  }  moreover {
    let ?Ops' = "{ (Operator k (index ?ops op))⇧+
      | op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op) }"
    have "?Ops' ⊆ ?C'"
      by blast
    moreover have "?C' - ?Ops' = { (State k (index ?vs v))¯ , (State (Suc k) (index ?vs v))⇧+ }"
      by fast
    moreover have "∀L ∈ ?Ops'. ¬ lit_semantics 𝒜 L"
      using nb(2)
      by blast
    (* TODO slow. *)
    ultimately have "clause_semantics 𝒜 ?C'
      = clause_semantics 𝒜 { (State k (index ?vs v))¯, (State (Suc k) (index ?vs v))⇧+ }"
      using lit_semantics_reducible_to_subset_if[of ?Ops' ?C']
      by presburger
  }  moreover {
    have cnf_semantics_𝒜_Φ:"cnf_semantics 𝒜 (cnf ?Φ)"
      using valuation_models_encoding_cnf_formula_equals[OF assms(1)] assms(2)
      by blast
    have k_v_included: "(k, v) ∈ ({..<t} × set ((Π)⇩𝒱))"
      using assms(3, 4)
      by blast
    (* TODO slow. *)
    have c_in_un_a: "?C ∈ ⋃?A" and c'_in_un_b: "?C' ∈ ⋃?B"
      using k_v_included
      by force+
    (* TODO slow. *)
    then have "?C ∈ cnf ?Φ⇩F" and "?C' ∈ cnf ?Φ⇩F"
      subgoal
        using cnf_of_encode_all_frame_axioms_structure UnI1[of "?C" "⋃?A" "⋃?B"] c_in_un_a
        by metis
      subgoal
        using cnf_of_encode_all_frame_axioms_structure UnI2[of "?C'" "⋃?B" "⋃?A"] c'_in_un_b
        by metis
      done
    then have "{ ?C } ⊆ cnf ?Φ⇩F" and c'_subset_frame_axiom_encoding: "{ ?C' } ⊆ cnf ?Φ⇩F"
      by blast+
    then have "{ ?C } ⊆ cnf ?Φ" and "{ ?C' } ⊆ cnf ?Φ"
      subgoal
        using operator_encoding_subset_encoding
        by fast
      subgoal
        using c'_subset_frame_axiom_encoding operator_encoding_subset_encoding
        by fast
      done
    (* TODO slow. *)
    hence "cnf_semantics 𝒜 { ?C }" and "cnf_semantics 𝒜 { ?C' }"
      using cnf_semantics_𝒜_Φ model_for_cnf_is_model_of_all_subsets
      by fastforce+
  }
  ultimately show "cnf_semantics 𝒜 {{ (State k (index ?vs v))¯, (State (Suc k) (index ?vs v))⇧+ }}"
    and "cnf_semantics 𝒜 {{ (State k (index ?vs v))⇧+, (State (Suc k) (index ?vs v))¯ }}"
    unfolding cnf_semantics_def
    by blast+
qed

lemma encode_problem_parallel_correct_v:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
    and "k < length (Φ¯ Π 𝒜 t)"
  shows "(Φ⇩S¯ Π 𝒜 (Suc k)) = execute_parallel_operator (Φ⇩S¯ Π 𝒜 k) ((Φ¯ Π 𝒜 t) ! k)"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
    and ?π = "Φ¯ Π 𝒜 t"
    and ?s⇩k = "Φ⇩S¯ Π 𝒜 k"
    and ?s⇩k' = "Φ⇩S¯ Π 𝒜 (Suc k)"
  let ?t⇩k' = "execute_parallel_operator ?s⇩k (?π ! k)"
    and ?π⇩k = "?π ! k"
  have k_lt_t: "k < t" and k_lte_t: "k ≤ t" and suc_k_lte_t: "Suc k ≤ t"
    using decode_plan_length[of ?π Π 𝒜 t] assms(3)
    by (argo, fastforce+)
  then have operator_preconditions_hold:
    "are_all_operators_applicable ?s⇩k ?π⇩k ∧ are_all_operator_effects_consistent ?π⇩k"
    using encode_problem_parallel_correct_ii[OF assms(1, 2, 3)]
    by blast
  ― ‹ We show the goal in classical fashion by proving that
      @{text[display, indent=4] "Φ⇩S¯ Π 𝒜 (Suc k) v
        = execute_parallel_operator (Φ⇩S¯ Π 𝒜 k)
          ((Φ¯ Π 𝒜 t) ! k) v"}
    ---i.e. the state decoded at time ‹k + 1› is equivalent to the state obtained by executing the
    parallel operator ‹(Φ¯ Π 𝒜 t) ! k› on the previous state
    ‹Φ⇩S¯ Π 𝒜 k›---for all variables ‹v› given ‹k < t›, a model ‹𝒜›,
    and makespan ‹t›. ›
  moreover {
    {
      fix v
      assume v_in_dom_s⇩k':"v ∈ dom ?s⇩k'"
      then have s⇩k'_not_none: "?s⇩k' v ≠ None"
        by blast
      hence "?s⇩k' v = ?t⇩k' v"
        proof (cases "∃op ∈ set ?π⇩k. v ∈ set (add_effects_of op) ∨ v ∈ set (delete_effects_of op)")
          case True
          then obtain op
            where op_in_π⇩k: "op ∈ set ?π⇩k"
            and "v ∈ set (add_effects_of op) ∨ v ∈ set (delete_effects_of op)"
            by blast
          then consider (v_is_add_effect) "v ∈ set (add_effects_of op)"
            | (v_is_delete_effect) "v ∈ set (delete_effects_of op)"
            by blast
          then show ?thesis
            proof (cases)
              case v_is_add_effect
              then have "?s⇩k' v = Some True"
                using encode_problem_parallel_correct_iii(1)[OF assms(1, 2, 3) op_in_π⇩k]
                  v_is_add_effect
                by blast
              moreover have "are_all_operators_applicable (Φ⇩S¯ Π 𝒜 k) ((Φ¯ Π 𝒜 t) ! k)"
                and "are_all_operator_effects_consistent ((Φ¯ Π 𝒜 t) ! k)"
                using operator_preconditions_hold v_is_add_effect
                by blast+
              moreover have "?t⇩k' v = Some True"
                using execute_parallel_operator_positive_effect_if[of
                    "Φ⇩S¯ Π 𝒜 k" "(Φ¯ Π 𝒜 t) ! k"] op_in_π⇩k
                  v_is_add_effect calculation(2, 3)
                by blast
              ultimately show ?thesis
                by argo
            next
              case v_is_delete_effect
              then have "?s⇩k' v = Some False"
                using encode_problem_parallel_correct_iii(2)[OF assms(1, 2, 3) op_in_π⇩k]
                  v_is_delete_effect
                by blast
              moreover have "are_all_operators_applicable (Φ⇩S¯ Π 𝒜 k) ((Φ¯ Π 𝒜 t) ! k)"
                and "are_all_operator_effects_consistent ((Φ¯ Π 𝒜 t) ! k)"
                using operator_preconditions_hold
                by blast+
              moreover have "?t⇩k' v = Some False"
                using execute_parallel_operator_effect(2) op_in_π⇩k
                  v_is_delete_effect calculation(2, 3)
                by fast
              moreover have "?t⇩k' v = Some False"
                by (meson execute_parallel_operator_negative_effect_if op_in_π⇩k operator_preconditions_hold v_is_delete_effect)
              ultimately show ?thesis
                by argo
            qed
        next
          case False
          (* TODO slow. *)
          then have "?t⇩k' v = ?s⇩k v"
            using execute_parallel_operator_no_effect_if
            by fastforce
          moreover {
            have v_in_set_vs: "v ∈ set ((Π)⇩𝒱)"
              using decode_state_at_valid_variable[OF s⇩k'_not_none].
            then have state_propagation_positive:
              "cnf_semantics 𝒜 {{(State k (index ?vs v))¯
                , (State (Suc k) (index ?vs v))⇧+}}"
            and state_propagation_negative:
              "cnf_semantics 𝒜 {{(State k (index ?vs v))⇧+
                , (State (Suc k) (index ?vs v))¯}}"
              using encode_problem_parallel_correct_iv[OF assms(1, 2) k_lt_t _ False]
              by fastforce+
            consider (s⇩k'_v_positive) "?s⇩k' v = Some True"
              | (s⇩k'_v_negative) "?s⇩k' v = Some False"
              using s⇩k'_not_none
              by fastforce
            hence "?s⇩k' v = ?s⇩k v"
              proof (cases)
                case s⇩k'_v_positive
                then have "lit_semantics 𝒜 ((State (Suc k) (index ?vs v))⇧+)"
                  using decode_state_at_encoding_variables_equals_some_of_valuation_if[OF
                      assms(1, 2) suc_k_lte_t v_in_set_vs]
                  by fastforce
                (* TODO slow. *)
                then have "lit_semantics 𝒜 ((State k (index ?vs v))⇧+)"
                  using state_propagation_negative
                  unfolding cnf_semantics_def clause_semantics_def
                  by fastforce
                then show ?thesis
                  using decode_state_at_encoding_variables_equals_some_of_valuation_if[OF
                      assms(1, 2) k_lte_t v_in_set_vs] s⇩k'_v_positive
                  by fastforce
              next
                case s⇩k'_v_negative
                then have "¬lit_semantics 𝒜 ((State (Suc k) (index ?vs v))⇧+)"
                  using decode_state_at_encoding_variables_equals_some_of_valuation_if[
                      OF assms(1, 2) suc_k_lte_t v_in_set_vs]
                  by fastforce
                (* TODO slow. *)
                then have "¬lit_semantics 𝒜 ((State k (index ?vs v))⇧+)"
                  using state_propagation_positive
                  unfolding cnf_semantics_def clause_semantics_def
                  by fastforce
                then show ?thesis
                  using decode_state_at_encoding_variables_equals_some_of_valuation_if[OF
                      assms(1, 2) k_lte_t v_in_set_vs] s⇩k'_v_negative
                  by fastforce
              qed
          }
          ultimately show ?thesis
            by argo
        qed
      }
    hence "?s⇩k' ⊆⇩m ?t⇩k'"
      using map_le_def
      by blast
  }
  moreover {
    {
      fix v
      assume "v ∈ dom ?t⇩k'"
      then have t⇩k'_not_none: "?t⇩k' v ≠ None"
        by blast
      {
        {
          assume contradiction: "v ∉ set ((Π)⇩𝒱)"
          then have "(Φ⇩S¯ Π 𝒜 k) v = None"
            using decode_state_at_valid_variable
            by fastforce
          then obtain op
            where op_in: "op ∈ set ((Φ¯ Π 𝒜 t) ! k)"
              and v_is_or: "v ∈ set (add_effects_of op)
                ∨ v ∈ set (delete_effects_of op)"
            using execute_parallel_operators_strips_none_if_contraposition[OF
                t⇩k'_not_none]
            by blast
          have op_in: "op ∈ set ((Π)⇩𝒪)"
              using op_in decode_plan_step_element_then(1) k_lt_t
              by blast
          consider (A) "v ∈ set (add_effects_of op)"
            | (B) "v ∈ set (delete_effects_of op)"
            using v_is_or
            by blast
          hence False
            proof (cases)
              case A
              then have "v ∈ set ((Π)⇩𝒱)"
                using is_valid_problem_strips_operator_variable_sets(2)[OF
                    assms(1)] op_in A
                by blast
              thus False
                using contradiction
                by blast
            next
              case B
              then have "v ∈ set ((Π)⇩𝒱)"
                using is_valid_problem_strips_operator_variable_sets(3)[OF
                    assms(1)] op_in B
                by blast
              thus False
                using contradiction
                by blast
            qed
          }
      }
      hence v_in_set_vs: "v ∈ set ((Π)⇩𝒱)"
        by blast
      hence "?t⇩k' v = ?s⇩k' v"
        proof (cases "(∃op∈set ?π⇩k. v ∈ set (add_effects_of op) ∨ v ∈ set (delete_effects_of op))")
          case True
          then obtain op
            where op_in_set_π⇩k: "op ∈ set ?π⇩k"
            and v_options: "v ∈ set (add_effects_of op) ∨ v ∈ set (delete_effects_of op)"
            by blast
          then have "op ∈ set ((Π)⇩𝒪)"
            using decode_plan_step_element_then[OF k_lt_t]
            by blast
          then consider (v_is_add_effect) "v ∈ set (add_effects_of op)"
            | (v_is_delete_effect) "v ∈ set (delete_effects_of op)"
            using v_options
            by blast
          thus ?thesis
            proof (cases)
              case v_is_add_effect
              then have "?t⇩k' v = Some True"
                using execute_parallel_operator_positive_effect_if[OF _ _ op_in_set_π⇩k]
                  operator_preconditions_hold
                by blast
              moreover have "?s⇩k' v = Some True"
                using encode_problem_parallel_correct_iii(1)[OF assms(1, 2, 3) op_in_set_π⇩k]
                  v_is_add_effect
                by blast
              ultimately show ?thesis
                by argo
            next
              case v_is_delete_effect
              then have "?t⇩k' v = Some False"
                using execute_parallel_operator_negative_effect_if[OF _ _ op_in_set_π⇩k]
                  operator_preconditions_hold
                by blast
              moreover have "?s⇩k' v = Some False"
                using encode_problem_parallel_correct_iii(2)[OF assms(1, 2, 3) op_in_set_π⇩k]
                  v_is_delete_effect
                by blast
              ultimately show ?thesis
                by argo
            qed
        next
          case False
          have state_propagation_positive:
            "cnf_semantics 𝒜 {{(State k (index ?vs v))¯, (State (Suc k) (index ?vs v))⇧+}}"
          and state_propagation_negative:
            "cnf_semantics 𝒜 {{(State k (index ?vs v))⇧+, (State (Suc k) (index ?vs v))¯}}"
            using encode_problem_parallel_correct_iv[OF assms(1, 2) k_lt_t v_in_set_vs
                False]
            by blast+
          {
            have all_op_in_set_π⇩k_have_no_effect:
              "∀op ∈ set ?π⇩k. v ∉ set (add_effects_of op) ∧ v ∉ set (delete_effects_of op)"
              using False
              by blast
            then have "?t⇩k' v = ?s⇩k v"
              using execute_parallel_operator_no_effect_if[OF all_op_in_set_π⇩k_have_no_effect]
              by blast
          } note t⇩k'_equals_s⇩k = this
          {
            have "?s⇩k v ≠ None"
              using t⇩k'_not_none t⇩k'_equals_s⇩k
              by argo
            then consider (s⇩k_v_is_some_true) "?s⇩k v = Some True"
              | (s⇩k_v_is_some_false) "?s⇩k v = Some False"
              by fastforce
          }
          then show ?thesis
            proof (cases)
              case s⇩k_v_is_some_true
              moreover {
                have "lit_semantics 𝒜 ((State k (index ?vs v))⇧+)"
                  using decode_state_at_encoding_variables_equals_some_of_valuation_if[OF
                      assms(1, 2) k_lte_t v_in_set_vs] s⇩k_v_is_some_true
                  by simp
                then have "lit_semantics 𝒜 ((State (Suc k) (index ?vs v))⇧+)"
                  using state_propagation_positive
                  unfolding cnf_semantics_def clause_semantics_def
                  by fastforce
                then have "?s⇩k' v = Some True"
                  using decode_state_at_encoding_variables_equals_some_of_valuation_if[OF
                      assms(1, 2) suc_k_lte_t v_in_set_vs]
                  by fastforce
              }
              ultimately show ?thesis
                using t⇩k'_equals_s⇩k
                by simp
            next
              case s⇩k_v_is_some_false
              moreover {
                have "lit_semantics 𝒜 ((State k (index ?vs v))¯)"
                  using decode_state_at_encoding_variables_equals_some_of_valuation_if[OF
                      assms(1, 2) k_lte_t v_in_set_vs] s⇩k_v_is_some_false
                  by simp
                then have "lit_semantics 𝒜 ((State (Suc k) (index ?vs v))¯)"
                  using state_propagation_negative
                  unfolding cnf_semantics_def clause_semantics_def
                  by fastforce
                then have "?s⇩k' v = Some False"
                  using decode_state_at_encoding_variables_equals_some_of_valuation_if[OF
                      assms(1, 2) suc_k_lte_t v_in_set_vs]
                  by fastforce
              }
              ultimately show ?thesis
                using t⇩k'_equals_s⇩k
                by simp
            qed
        qed
    }
    hence "?t⇩k' ⊆⇩m ?s⇩k'"
    using map_le_def
    by blast
  }
  ultimately show ?thesis
    using map_le_antisym
    by blast
qed

lemma encode_problem_parallel_correct_vi:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
    and "k < length (trace_parallel_plan_strips ((Π)⇩I) (Φ¯ Π 𝒜 t))"
  shows "trace_parallel_plan_strips ((Π)⇩I) (Φ¯ Π 𝒜 t) ! k
    = Φ⇩S¯ Π 𝒜 k"
  using assms
proof -
  let ?I = "(Π)⇩I"
    and ?π = "Φ¯ Π 𝒜 t"
  let ?τ = "trace_parallel_plan_strips ?I ?π"
  show ?thesis
    using assms
    proof (induction k)
      case 0
      hence "?τ ! 0 = ?I"
        using trace_parallel_plan_strips_head_is_initial_state
        by blast
      moreover have "Φ⇩S¯ Π 𝒜 0 = ?I"
        using decode_state_at_initial_state[OF assms(1, 2)]
        by simp
      ultimately show ?case
        by simp
    next
      case (Suc k)
      let ?τ⇩k = "trace_parallel_plan_strips ?I ?π ! k"
        and ?s⇩k = "Φ⇩S¯ Π 𝒜 k"
      have k_lt_length_τ_minus_one: "k < length ?τ - 1" and k_lt_length_τ: "k < length ?τ"
        using Suc.prems(3)
        by linarith+
      ― ‹ Use the induction hypothesis to obtain the proposition for the previous step $k$.
        Then, show that applying the $k$-th parallel operator in the plan $\pi$ on either the state
        obtained from the trace or decoded from the model yields the same successor state. ›
      {
        have "?τ ! k = execute_parallel_plan ?I (take k ?π)"
          using trace_parallel_plan_plan_prefix k_lt_length_τ
          by blast
        hence "?τ⇩k = ?s⇩k"
          using Suc.IH[OF assms(1, 2) k_lt_length_τ]
          by blast
      }
      moreover have "trace_parallel_plan_strips ?I ?π ! Suc k
        = execute_parallel_operator ?τ⇩k (?π ! k)"
        using trace_parallel_plan_step_effect_is[OF k_lt_length_τ_minus_one]
        by blast
      moreover {
        thm Suc.prems(3)
        have "length (trace_parallel_plan_strips ?I ?π) ≤ length ?π + 1"
          using length_trace_parallel_plan_strips_lte_length_plan_plus_one
          by blast
        then have "k < length ?π"
          using Suc.prems(3)
          unfolding Suc_eq_plus1
          by linarith
        hence "Φ⇩S¯ Π 𝒜 (Suc k)
          = execute_parallel_operator ?s⇩k (?π ! k)"
          using encode_problem_parallel_correct_v[OF assms(1, 2)]
          by simp
      }
      ultimately show ?case
        by argo
    qed
qed

lemma encode_problem_parallel_correct_vii:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
  shows "length (map (decode_state_at Π 𝒜)
      [0..<Suc (length (Φ¯ Π 𝒜 t))])
    = length (trace_parallel_plan_strips ((Π)⇩I) (Φ¯ Π 𝒜 t))"
proof -
  let ?I = "(Π)⇩I"
    and ?π = "Φ¯ Π 𝒜 t"
  let ?σ = "map (decode_state_at Π 𝒜) [0..<Suc (length ?π)]"
    and ?τ = "trace_parallel_plan_strips ?I ?π"
  let ?l = "length ?τ "
  let ?k = "?l - 1"
  show ?thesis
    proof (rule ccontr)
      assume length_σ_neq_length_τ: "length ?σ ≠ length ?τ"
      {
        have "length ?σ = length ?π + 1"
          by fastforce
        moreover have "length ?τ ≤ length ?π + 1"
          using length_trace_parallel_plan_strips_lte_length_plan_plus_one
          by blast
        moreover have "length ?τ < length ?π + 1"
          using length_σ_neq_length_τ calculation
          by linarith
      } note nb⇩1 = this
      {
        have "0 < length ?τ"
          using trace_parallel_plan_strips_not_nil..
        then have "length ?τ - 1 < length ?π"
          using nb⇩1
          by linarith
      } note nb⇩2 = this
      {
        obtain k' where "length ?τ = Suc k'"
          using less_imp_Suc_add[OF length_trace_parallel_plan_gt_0]
          by blast
        hence "?k < length ?π"
          using nb⇩2
          by blast
      } note nb⇩3 = this
      {
        have "?τ ! ?k = execute_parallel_plan ?I (take ?k ?π)"
          using trace_parallel_plan_plan_prefix[of ?k]
            length_trace_minus_one_lt_length_trace
          by blast
        thm encode_problem_parallel_correct_vi[OF assms(1, 2)] nb⇩3
        moreover have "(Φ⇩S¯ Π 𝒜 ?k) = ?τ ! ?k"
          using encode_problem_parallel_correct_vi[OF assms(1, 2)
              length_trace_minus_one_lt_length_trace]..
        ultimately have "(Φ⇩S¯ Π 𝒜 ?k)  = execute_parallel_plan ?I (take ?k ?π)"
          by argo
      } note nb⇩4 = this
      {
        have "are_all_operators_applicable (Φ⇩S¯ Π 𝒜 ?k) (?π ! ?k)"
          and "are_all_operator_effects_consistent (?π ! ?k)"
          using encode_problem_parallel_correct_ii(1, 2)[OF assms(1, 2)] nb⇩3
          by blast+
        ― ‹ Unsure why ‹calculation(1, 2)› is needed for this proof step. Should just require the
          default proof. ›
        moreover have "¬are_all_operators_applicable (Φ⇩S¯ Π 𝒜 ?k) (?π ! ?k)"
          and "¬are_all_operator_effects_consistent (?π ! ?k)"
          using length_trace_parallel_plan_strips_lt_length_plan_plus_one_then[OF nb⇩1]
            calculation(1, 2)
          unfolding nb⇩3 nb⇩4
          by blast+
        ultimately have False
          by blast
      }
      thus False.
    qed
qed

lemma encode_problem_parallel_correct_x:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
  shows "map (decode_state_at Π 𝒜)
      [0..<Suc (length (Φ¯ Π 𝒜 t))]
    = trace_parallel_plan_strips ((Π)⇩I) (Φ¯ Π 𝒜 t)"
proof -
  let ?I = "(Π)⇩I"
    and ?π = "Φ¯ Π 𝒜 t"
  let ?σ = "map (decode_state_at Π 𝒜) [0..<Suc (length ?π)]"
    and ?τ = "trace_parallel_plan_strips ?I ?π"
  {
    have "length ?τ = length ?σ"
      using encode_problem_parallel_correct_vii[OF assms]..
    moreover {
      fix k
      assume k_lt_length_τ: "k < length ?τ"
      then have "trace_parallel_plan_strips ((Π)⇩I) (Φ¯ Π 𝒜 t) ! k
        = Φ⇩S¯ Π 𝒜 k"
        using encode_problem_parallel_correct_vi[OF assms]
        by blast
      moreover {
        have "length ?τ ≤ length ?π + 1"
          using length_trace_parallel_plan_strips_lte_length_plan_plus_one
          by blast
        then have "k < length ?π + 1"
          using k_lt_length_τ
          by linarith
        then have "k < Suc (length ?π) - 0"
          by simp
        hence "?σ ! k = Φ⇩S¯ Π 𝒜 k"
          using nth_map_upt[of k "Suc (length ?π)" 0]
          by auto
      }
      ultimately have "?τ ! k = ?σ ! k"
        by argo
    }
    ultimately have "?τ = ?σ"
      using list_eq_iff_nth_eq[of ?τ ?σ]
      by blast
  }
  thus ?thesis
    by argo
qed

lemma encode_problem_parallel_correct_xi:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
   and "𝒜 ⊨ Φ Π t"
   and "ops ∈ set (Φ¯ Π 𝒜 t)"
   and "op ∈ set ops"
 shows "op ∈ set ((Π)⇩𝒪)"
proof -
  let ?π = "Φ¯ Π 𝒜 t"
  have "length ?π = t"
    using decode_plan_length
    by force
  moreover obtain k where "k < length ?π" and "ops = ?π ! k"
    using in_set_conv_nth[of ops ?π] assms(3)
    unfolding calculation
    by blast
  ultimately show ?thesis
    using assms(4) decode_plan_step_element_then(1)
    by force
qed


text ‹ To show soundness, we have to prove the following: given the existence of a model
\<^term>‹𝒜› of the basic SATPlan encoding \<^term>‹encode_problem Π t› for a given valid problem \<^term>‹Π›
and hypothesized plan length \<^term>‹t›, the decoded plan \<^term>‹π ≡ Φ¯ Π 𝒜 t› is a parallel solution
for \<^term>‹Π›.

We show this theorem by showing equivalence between the execution trace of the decoded plan and the
sequence of states

  @{text[display, indent=4] "σ = map (λ k. Φ⇩S¯ Π 𝒜 k) [0..<Suc (length ?π)]" }

decoded from the model \<^term>‹𝒜›. Let

  @{text[display, indent=4] "τ ≡ trace_parallel_plan_strips I π"}

be the trace of \<^term>‹π›. Theorem \ref{isathm:soundness-satplan-encoding} first establishes the
equality \<^term>‹σ = τ› of the decoded state sequence and the trace of \<^term>‹π›.
We can then derive that \<^term>‹G ⊆⇩m last σ› by lemma \ref{isathm:parallel-solution-trace-strips}, i.e. the last
state reached by plan execution (and moreover the last state decoded from the model), satisfies the
goal state \<^term>‹G› defined by the problem. By lemma \ref{isathm:parallel-solution-trace-strips}, we
can conclude that \<^term>‹π› is a solution for \<^term>‹I› and \<^term>‹G›.

Moreover, we show that all operators \<^term>‹op› in all parallel operators \<^term>‹ops ∈ set π›
are also contained in \<^term>‹𝒪›. This is the case because the plan decoding function reverses the
encoding function (which only encodes operators in \<^term>‹𝒪›).

By definition \ref{isadef:parallel-solution-strips} this means that \<^term>‹π› is a parallel solution
for \<^term>‹Π›. Moreover \<^term>‹π› has length \<^term>‹t› as confirmed by lemma
\isaname{decode_plan_length}.
\footnote{This lemma is used in the proof but not shown.} ›

theorem  encode_problem_parallel_sound:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ Π t"
  shows "is_parallel_solution_for_problem Π (Φ¯ Π 𝒜 t)"
  proof -
    let ?ops = "strips_problem.operators_of Π"
      and ?I = "(Π)⇩I"
      and ?G = "(Π)⇩G"
      and ?π = "Φ¯ Π 𝒜 t"
    let ?σ = "map (λ k. Φ⇩S¯ Π 𝒜 k) [0..<Suc (length ?π)]"
      and ?τ = "trace_parallel_plan_strips ?I ?π"
    {
      have "?σ = ?τ"
        using encode_problem_parallel_correct_x[OF assms].
      moreover {
        have "length ?π = t"
          using decode_plan_length
          by auto
        then have "?G ⊆⇩m last ?σ"
          using decode_state_at_goal_state[OF assms]
          by simp
      }
      ultimately have "((Π)⇩G) ⊆⇩m execute_parallel_plan ((Π)⇩I) (Φ¯ Π 𝒜 t)"
        using execute_parallel_plan_reaches_goal_iff_goal_is_last_element_of_trace
        by auto
    }
    moreover have "∀ops ∈ set ?π. ∀op ∈ set ops. op ∈ set ((Π)⇩𝒪)"
      using encode_problem_parallel_correct_xi[OF assms(1, 2)]
      by auto
    ultimately show ?thesis
      unfolding is_parallel_solution_for_problem_def
      unfolding list_all_iff ListMem_iff operators_of_def STRIPS_Representation.operators_of_def
      by fastforce
  qed

value  "stop" (* Tell document preparation to stop collecting for the last tag *)



subsection "Completeness"

(* TODO make abbreviation *)
definition empty_valuation :: "sat_plan_variable valuation" ("𝒜⇩0")
  where "empty_valuation ≡  (λ_. False)"

abbreviation valuation_for_state
  :: "'variable list
    ⇒'variable strips_state
    ⇒ nat
    ⇒ 'variable
    ⇒ sat_plan_variable valuation
    ⇒ sat_plan_variable valuation"
  where "valuation_for_state vs s k v 𝒜
    ≡ 𝒜(State k (index vs v) := (s v = Some True))"

― ‹ Since the trace may be shorter than the plan length even though the last trace element
subsumes the goal state---namely in case plan execution is impossible due to violation of the
execution condition but the reached state serendipitously subsumes the goal state---, we also have
to repeat the valuation for all time steps \<^term>‹k' ∈ {length τ..(length π + 1)}› for all \
\<^term>‹v ∈ 𝒱› (see \<^term>‹𝒜⇩2›). ›
definition valuation_for_state_variables
  :: "'variable strips_problem
    ⇒ 'variable strips_operator list list
    ⇒ 'variable strips_state list
    ⇒ sat_plan_variable valuation"
  where "valuation_for_state_variables Π π τ ≡ let
      t' = length τ
      ; τ⇩Ω = τ ! (t' - 1)
      ; vs = variables_of Π
      ; V⇩1 = { State k (index vs v) | k v. k ∈ {0..<t'} ∧ v ∈ set vs }
      ; V⇩2 = { State k (index vs v) | k v. k ∈ {t'..(length π + 1)} ∧ v ∈ set vs }
      ; 𝒜⇩1 = foldr
        (λ(k, v) 𝒜. valuation_for_state (variables_of Π) (τ ! k) k v 𝒜)
        (List.product [0..<t'] vs)
        𝒜⇩0
      ; 𝒜⇩2 = foldr
        (λ(k, v) 𝒜. valuation_for_state (variables_of Π) τ⇩Ω k v 𝒜)
        (List.product [t'..<length π + 2] vs)
        𝒜⇩0
    in override_on (override_on 𝒜⇩0 𝒜⇩1 V⇩1) 𝒜⇩2 V⇩2"

― ‹ The valuation is left to yield false for the potentially remaining
\<^term>‹k' ∈ {length τ..(length π + 1)}› since no more operators are executed after the trace ends
anyway. The definition of \<^term>‹𝒜⇩0› as the valuation that is false for every argument ensures
this implicitely. ›
definition valuation_for_operator_variables
  :: "'variable strips_problem
    ⇒ 'variable strips_operator list list
    ⇒ 'variable strips_state list
    ⇒ sat_plan_variable valuation"
  where "valuation_for_operator_variables Π π τ ≡ let
      ops = operators_of Π
      ; Op = { Operator k (index ops op) | k op. k ∈ {0..<length τ - 1} ∧ op ∈ set ops }
    in override_on
      𝒜⇩0
      (foldr
        (λ(k, op) 𝒜. 𝒜(Operator k (index ops op) := True))
        (concat (map (λk. map (Pair k) (π ! k)) [0..<length τ - 1]))
        𝒜⇩0)
      Op"


text ‹ The completeness proof requires that we show that the SATPlan encoding \<^term>‹Φ Π t› of a
problem \<^term>‹Π› has a model \<^term>‹𝒜› in case a solution \<^term>‹π› with length \<^term>‹t› exists.
Since a plan corresponds to a state trace \<^term>‹τ ≡ trace_parallel_plan_strips I π› with
  @{text[display, indent=4] "τ ! k = execute_parallel_plan I (take k π)"}
for all \<^term>‹k < length τ› we can construct a valuation \<^term>‹𝒜⇩V› modeling the state sequence in
\<^term>‹τ› by letting
  @{text[display, indent=4] "𝒜(State k (index vs v) := (s v = Some True))"}
or all \<^term>‹v ∈ 𝒱› where \<^term>‹s ≡ τ ! k› .
\footnote{It is helpful to remember at this point, that the trace elements of a solution contain
the states reached by plan prefix execution (lemma \ref{isathm:trace-elements-and-plan-prefixes}).}

Similarly to \<^term>‹𝒜⇩V›, we obtain an operator valuation \<^term>‹𝒜⇩O› by defining
  @{text[display, indent=4] "𝒜(Operator k (index ops op) := True)"}
for all operators \<^term>‹op ∈ 𝒪› s.t. \<^term>‹op ∈ set (π ! k)› for all \<^term>‹k < length τ - 1›.

The overall valuation for the plan execution \<^term>‹𝒜› can now be constructed by combining the
state variable valuation \<^term>‹𝒜⇩V› and operator valuation \<^term>‹𝒜⇩O›. ›

definition  valuation_for_plan
  :: "'variable strips_problem
    ⇒ 'variable strips_operator list list
    ⇒ sat_plan_variable valuation"
  where "valuation_for_plan Π π ≡ let
      vs = variables_of Π
      ; ops = operators_of Π
      ; τ = trace_parallel_plan_strips (initial_of Π) π
      ; t = length π
      ; t' = length τ
      ; 𝒜⇩V = valuation_for_state_variables Π π τ
      ; 𝒜⇩O = valuation_for_operator_variables Π π τ
      ; V = { State k (index vs v)
        | k v. k ∈ {0..<t + 1} ∧ v ∈ set vs }
      ; Op = { Operator k (index ops op)
        | k op. k ∈ {0..<t} ∧ op ∈ set ops }
    in override_on (override_on 𝒜⇩0 𝒜⇩V V) 𝒜⇩O Op"


― ‹ Show that in case of an encoding with makespan zero, it suffices to show that a given
model satisfies the initial state and goal state encodings. ›
(* TODO refactor. *)
lemma model_of_encode_problem_makespan_zero_iff:
  "𝒜 ⊨ Φ Π 0 ⟷ 𝒜 ⊨ Φ⇩I Π ❙∧ (Φ⇩G Π) 0"
proof -
  have "encode_operators Π 0 = ❙¬⊥ ❙∧ ❙¬⊥"
    unfolding encode_operators_def encode_all_operator_effects_def
      encode_all_operator_preconditions_def
    by simp
  moreover have "encode_all_frame_axioms Π 0 = ❙¬⊥"
    unfolding encode_all_frame_axioms_def
    by simp
  ultimately show ?thesis
    unfolding encode_problem_def SAT_Plan_Base.encode_problem_def encode_initial_state_def
      encode_goal_state_def
    by simp
qed

(* TODO refactor. *)
lemma empty_valution_is_False[simp]: "𝒜⇩0 v = False"
  unfolding empty_valuation_def..

lemma  model_initial_state_set_valuations:
  assumes "is_valid_problem_strips Π"
  shows "set (map (λv. case ((Π)⇩I) v of Some b
          ⇒ 𝒜⇩0(State 0 (index (strips_problem.variables_of Π) v) := b)
        | _ ⇒ 𝒜⇩0)
      (strips_problem.variables_of Π))
    = { 𝒜⇩0(State 0 (index (strips_problem.variables_of Π) v) := the (((Π)⇩I) v))
      | v. v ∈ set ((Π)⇩𝒱) }"
proof -
  let ?I = "(Π)⇩I"
    and ?vs = "strips_problem.variables_of Π"
  let ?f = "λv. case ((Π)⇩I) v of Some b
    ⇒ 𝒜⇩0(State 0 (index ?vs v) := b) | _ ⇒ 𝒜⇩0"
    and ?g = "λv. 𝒜⇩0(State 0 (index ?vs v) := the (?I v))"
  let ?𝒜s = "map ?f ?vs"
  have nb⇩1: "dom ?I = set ((Π)⇩𝒱)"
    using is_valid_problem_strips_initial_of_dom assms
    by fastforce
  {
    {
      fix v
      assume "v ∈ dom ?I"
      hence "?f v = ?g v"
        using nb⇩1
        by fastforce
    }
    hence "?f ` set ((Π)⇩𝒱) = ?g ` set ((Π)⇩𝒱)"
      using nb⇩1
      by force
  }
  then have "set ?𝒜s = ?g ` set ((Π)⇩𝒱)"
    unfolding set_map
    by simp
  thus ?thesis
    by blast
qed

(* TODO refactor *)
lemma valuation_of_state_variable_implies_lit_semantics_if:
  assumes "v ∈ dom S"
    and "𝒜 (State k (index vs v)) = the (S v)"
  shows "lit_semantics 𝒜 (literal_formula_to_literal (encode_state_variable k (index vs v) (S v)))"
proof -
  let ?L = "literal_formula_to_literal (encode_state_variable k (index vs v) (S v))"
  consider (True) "S v = Some True"
    | (False) "S v = Some False"
    using assms(1)
    by fastforce
  thus ?thesis
    unfolding encode_state_variable_def
    using assms(2)
    by (cases, force+)
qed

(* TODO refactor ‹Fun_Supplement›? *)
lemma foldr_fun_upd:
  assumes "inj_on f (set xs)"
    and "x ∈ set xs"
  shows "foldr (λx 𝒜. 𝒜(f x := g x)) xs 𝒜 (f x) = g x"
  using assms
proof (induction xs)
  case (Cons a xs)
  then show ?case
    proof (cases "xs = []")
      case True
      then have "x = a"
        using Cons.prems(2)
        by simp
      thus ?thesis
        by simp
    next
      case False
      thus ?thesis
        proof (cases "a = x")
        next
          case False
          {
            from False
            have "x ∈ set xs"
              using Cons.prems(2)
              by simp
            moreover have "inj_on f (set xs)"
              using Cons.prems(1)
              by fastforce
            ultimately have "(foldr (λx 𝒜. 𝒜(f x := g x)) xs 𝒜) (f x) = g x"
              using Cons.IH
              by blast
          } moreover {
            ― ‹ Follows from modus tollens on the definition of @{text "inj_on"}. ›
            have "f a ≠ f x"
              using Cons.prems False
              by force
            moreover have "foldr (λx 𝒜. 𝒜(f x := g x)) (a # xs) 𝒜
              = (foldr (λx 𝒜. 𝒜(f x := g x)) xs 𝒜)(f a := g a)"
              by simp
            ultimately have "foldr (λx 𝒜. 𝒜(f x := g x)) (a # xs) 𝒜 (f x)
              = (foldr (λx 𝒜. 𝒜(f x := g x)) xs 𝒜) (f x)"
              unfolding fun_upd_def
              by presburger
          } ultimately show ?thesis
            by argo
       qed simp
   qed
qed fastforce

lemma foldr_fun_no_upd:
  assumes "inj_on f (set xs)"
    and "y ∉ f ` set xs"
  shows "foldr (λx 𝒜. 𝒜(f x := g x)) xs 𝒜 y = 𝒜 y"
  using assms
proof (induction xs)
  case (Cons a xs)
  {
    have "inj_on f (set xs)" and "y ∉ f ` set xs"
      using Cons.prems
      by (fastforce, simp)
    hence "foldr (λx 𝒜. 𝒜(f x := g x)) xs 𝒜 y = 𝒜 y"
      using Cons.IH
      by blast
  }
  moreover {
    have "f a ≠ y"
      using Cons.prems(2)
      by auto
    moreover have "foldr (λx 𝒜. 𝒜(f x := g x)) (a # xs) 𝒜
      = (foldr (λx 𝒜. 𝒜(f x := g x)) xs 𝒜)(f a := g a)"
      by simp
    ultimately have "foldr (λx 𝒜. 𝒜(f x := g x)) (a # xs) 𝒜 y
      = (foldr (λx 𝒜. 𝒜(f x := g x)) xs 𝒜) y"
      unfolding fun_upd_def
      by presburger
  }
  ultimately show ?case
    by argo
qed simp

― ‹ We only use the part of the characterization of ‹𝒜› which pertains to the state
variables here. ›
lemma encode_problem_parallel_complete_i:
  fixes Π::"'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "(Π)⇩G ⊆⇩m execute_parallel_plan ((Π)⇩I) π"
     "∀v k. k < length (trace_parallel_plan_strips ((Π)⇩I) π)
      ⟶  (𝒜 (State k (index (strips_problem.variables_of Π) v))
          ⟷ (trace_parallel_plan_strips ((Π)⇩I) π ! k) v = Some True)
        ∧ (¬𝒜 (State k (index (strips_problem.variables_of Π) v))
          ⟷ ((trace_parallel_plan_strips ((Π)⇩I) π ! k) v ≠ Some True))"
  shows "𝒜 ⊨ Φ⇩I Π"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?I = "(Π)⇩I"
    and ?G = "(Π)⇩G"
    and ?Φ⇩I = "Φ⇩I Π"
  let ?τ = "trace_parallel_plan_strips ?I π"
  {
    fix C
    assume "C ∈ cnf ?Φ⇩I"
    then obtain v
      where v_in_set_vs: "v ∈ set ?vs"
      and C_is: "C = { literal_formula_to_literal (encode_state_variable 0 (index ?vs v) (?I v)) }"
      using cnf_of_encode_initial_state_set_ii[OF assms(1)]
      by auto
    {
      have "0 < length ?τ"
        using trace_parallel_plan_strips_not_nil
        by blast
      then have "𝒜 (State 0 (index (strips_problem.variables_of Π) v))
          ⟷ (trace_parallel_plan_strips ((Π)⇩I) π ! 0) v = Some True"
        and "¬𝒜 (State 0 (index (strips_problem.variables_of Π) v))
          ⟷ ((trace_parallel_plan_strips ((Π)⇩I) π ! 0) v ≠ Some True)"
        using assms(3)
        by (presburger+)
    } note nb = this
    {
      let ?L = "literal_formula_to_literal (encode_state_variable 0 (index ?vs v) (?I v))"
      have τ_0_is: "?τ ! 0 = ?I"
        using trace_parallel_plan_strips_head_is_initial_state
        by blast
      have v_in_dom_I: "v ∈ dom ?I"
        using is_valid_problem_strips_initial_of_dom assms(1) v_in_set_vs
        by fastforce
      then consider (I_v_is_Some_True) "?I v = Some True"
        | (I_v_is_Some_False) "?I v = Some False"
        by fastforce
      hence "lit_semantics 𝒜 ?L"
          unfolding encode_state_variable_def
          using assms(3) τ_0_is nb
          by (cases, force+)
    }
    hence "clause_semantics 𝒜 C"
      unfolding clause_semantics_def C_is
      by blast
  }
  thus ?thesis
    using is_cnf_encode_initial_state[OF assms(1)] is_nnf_cnf cnf_semantics
    unfolding cnf_semantics_def
    by blast
qed

― ‹ Plans may terminate early (i.e. by reaching a state satisfying the goal state before
reaching the time point corresponding to the plan length). We therefore have to show the goal by
splitting cases on whether the plan successfully terminated early.
If not, we can just derive the goal from the assumptions pertaining to ‹𝒜› Otherwise, we
have to first show that the goal was reached (albeit early) and that our valuation ‹𝒜›
reflects the termination of plan execution after the time point at which the goal was reached. ›
lemma encode_problem_parallel_complete_ii:
  fixes Π::"'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "(Π)⇩G ⊆⇩m execute_parallel_plan ((Π)⇩I) π"
    and "∀v k. k < length (trace_parallel_plan_strips ((Π)⇩I) π)
      ⟶ (𝒜 (State k (index (strips_problem.variables_of Π) v))
          ⟷ (trace_parallel_plan_strips ((Π)⇩I) π ! k) v = Some True)"
    and "∀v l. l ≥ length (trace_parallel_plan_strips ((Π)⇩I) π) ∧ l < length π + 1
      ⟶ 𝒜 (State l (index (strips_problem.variables_of Π) v))
        = 𝒜 (State (length (trace_parallel_plan_strips ((Π)⇩I) π) - 1)
          (index (strips_problem.variables_of Π) v))"
  shows "𝒜 ⊨ (Φ⇩G Π)(length π)"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?I = "(Π)⇩I"
    and ?G = "(Π)⇩G"
    and ?Φ⇩I = "Φ⇩I Π"
    and ?t = "length π"
    and ?Φ⇩G = "(Φ⇩G Π) (length π)"
  let ?τ = "trace_parallel_plan_strips ?I π"
  let ?t' = "length ?τ"
  {
    fix v
    assume G_of_v_is_not_None: "?G v ≠ None"
    have "?G ⊆⇩m last ?τ"
      using execute_parallel_plan_reaches_goal_iff_goal_is_last_element_of_trace assms(2)
      by blast
    also have "… = ?τ ! (?t' - 1)"
      using last_conv_nth[OF trace_parallel_plan_strips_not_nil].
    finally have "?G ⊆⇩m ?τ ! (?t' - 1)"
      by argo
    hence "(?τ ! (?t' - 1)) v = ?G v"
      using G_of_v_is_not_None
      unfolding map_le_def
      by force
  } note nb⇩1 = this
  (* TODO refactor. *)
  ― ‹ Discriminate on whether the trace has full length or not and show that the model
  valuation of the state variables always correspond to the (defined) goal state values. ›
  {
    fix v
    assume G_of_v_is_not_None: "?G v ≠ None"
    hence "𝒜 (State ?t (index ?vs v)) ⟷ ?G v = Some True"
      proof (cases "?t' = ?t + 1")
        case True
        moreover have "?t < ?t'"
          using calculation
          by fastforce
        moreover have "𝒜 (State ?t (index ?vs v)) ⟷ (?τ ! ?t) v = Some True"
          using assms(3) calculation(2)
          by blast
        ultimately show ?thesis
          using nb⇩1[OF G_of_v_is_not_None]
          by force
      next
        case False
        {
          have "?t' < ?t + 1"
            using length_trace_parallel_plan_strips_lte_length_plan_plus_one False
              le_neq_implies_less
            by blast
          moreover have "𝒜 (State ?t (index ?vs v)) = 𝒜 (State (?t' - 1) (index ?vs v))"
            using assms(4) calculation
            by simp
          moreover have "?t' - 1 < ?t'"
            using trace_parallel_plan_strips_not_nil length_greater_0_conv[of ?τ]
              less_diff_conv2[of 1 ?t' ?t']
            by force
          moreover have "𝒜 (State (?t' - 1) (index ?vs v)) ⟷ (?τ ! (?t' - 1)) v = Some True"
            using assms(3) calculation(3)
            by blast
          ultimately have "𝒜 (State ?t (index ?vs v)) ⟷ (?τ ! (?t' - 1)) v = Some True"
            by blast
        }
        thus ?thesis
          using nb⇩1[OF G_of_v_is_not_None]
          by presburger
      qed
  } note nb⇩2 = this
  {
    fix C
    assume C_in_cnf_of_Φ⇩G: "C ∈ cnf ?Φ⇩G"

    moreover obtain v
      where "v ∈ set ?vs"
        and G_of_v_is_not_None: "?G v ≠ None"
      and C_is: "C = { literal_formula_to_literal (encode_state_variable ?t (index ?vs v)
        (?G v)) }"
      using cnf_of_encode_goal_state_set_ii[OF assms(1)] calculation
      by auto
    consider (G_of_v_is_Some_True) "?G v = Some True"
      | (G_of_v_is_Some_False) "?G v = Some False"
      using G_of_v_is_not_None
      by fastforce
    then have "clause_semantics 𝒜 C"
      using nb⇩2 C_is
      unfolding clause_semantics_def encode_state_variable_def
      by (cases, force+)
  }
  thus ?thesis
    using cnf_semantics[OF is_nnf_cnf[OF encode_goal_state_is_cnf[OF assms(1)]]]
    unfolding cnf_semantics_def
    by blast
qed

― ‹ We are not using the full characterization of ‹𝒜› here since it's not needed. ›
(* TODO make private *)
lemma encode_problem_parallel_complete_iii_a:
  fixes Π::"'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "(Π)⇩G ⊆⇩m execute_parallel_plan ((Π)⇩I) π"
    and "C ∈ cnf (encode_all_operator_preconditions Π (strips_problem.operators_of Π) (length π))"
    and "∀k op. k < length (trace_parallel_plan_strips ((Π)⇩I) π) - 1
      ⟶ 𝒜 (Operator k (index (strips_problem.operators_of Π) op)) = (op ∈ set (π ! k))"
    and "∀l op. l ≥ length (trace_parallel_plan_strips ((Π)⇩I) π) - 1 ∧ l < length π
      ⟶ ¬𝒜 (Operator l (index (strips_problem.operators_of Π) op))"
    and "∀v k. k < length (trace_parallel_plan_strips ((Π)⇩I) π)
      ⟶  (𝒜 (State k (index (strips_problem.variables_of Π) v))
          ⟷ (trace_parallel_plan_strips ((Π)⇩I) π ! k) v = Some True)"
  shows "clause_semantics 𝒜 C"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?vs = "strips_problem.variables_of Π"
    and ?t = "length π"
  let ?τ = "trace_parallel_plan_strips ((Π)⇩I) π"
  (* TODO slow. *)
  obtain k op
    where k_and_op_are: "(k, op) ∈ ({0..<?t} × set ((Π)⇩𝒪))"
      and "C ∈ (⋃v ∈ set (precondition_of op). {{ (Operator k (index ?ops op))¯
        , (State k (index ?vs v))⇧+ }})"
    using cnf_of_encode_all_operator_preconditions_structure assms(3)
      UN_E[of C ]
    by auto
  then obtain v
    where v_in_preconditions_of_op: "v ∈ set (precondition_of op)"
      and C_is: "C = { (Operator k (index ?ops op))¯, (State k (index ?vs v))⇧+ }"
    by blast
  thus ?thesis
    proof (cases "k < length ?τ - 1")
      case k_lt_length_τ_minus_one: True
      thus ?thesis
        proof (cases "op ∈ set (π ! k)")
          case True
          {
            have "are_all_operators_applicable (?τ ! k) (π ! k)"
              using trace_parallel_plan_strips_operator_preconditions k_lt_length_τ_minus_one
              by blast
            then have "(?τ ! k) v = Some True"
              using are_all_operators_applicable_set v_in_preconditions_of_op True
              by fast
            hence "𝒜 (State k (index ?vs v))"
              using assms(6) k_lt_length_τ_minus_one
              by force
          }
          thus ?thesis
            using C_is
            unfolding clause_semantics_def
            by fastforce
        next
          case False
          then have "¬𝒜 (Operator k (index ?ops op))"
            using assms(4) k_lt_length_τ_minus_one
            by blast
          thus ?thesis
            using C_is
            unfolding clause_semantics_def
            by fastforce
        qed
    next
      case False
      then have "k ≥ length ?τ - 1" "k < ?t"
        using k_and_op_are
        by(force, simp)
      then have "¬𝒜 (Operator k (index ?ops op))"
        using assms(5)
        by blast
      thus ?thesis
        unfolding clause_semantics_def
        using C_is
        by fastforce
    qed
qed

― ‹ We are not using the full characterization of ‹𝒜› here since it's not needed. ›
(* TODO make private *)
lemma encode_problem_parallel_complete_iii_b:
  fixes Π::"'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "(Π)⇩G ⊆⇩m execute_parallel_plan ((Π)⇩I) π"
    and "C ∈ cnf (encode_all_operator_effects Π (strips_problem.operators_of Π) (length π))"
    and "∀k op. k < length (trace_parallel_plan_strips ((Π)⇩I) π) - 1
      ⟶ 𝒜 (Operator k (index (strips_problem.operators_of Π) op)) = (op ∈ set (π ! k))"
    and "∀l op. l ≥ length (trace_parallel_plan_strips ((Π)⇩I) π) - 1 ∧ l < length π
      ⟶ ¬𝒜 (Operator l (index (strips_problem.operators_of Π) op))"
    and "∀v k. k < length (trace_parallel_plan_strips ((Π)⇩I) π)
      ⟶  (𝒜 (State k (index (strips_problem.variables_of Π) v))
          ⟷ (trace_parallel_plan_strips ((Π)⇩I) π ! k) v = Some True)"
  shows "clause_semantics 𝒜 C"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?vs = "strips_problem.variables_of Π"
    and ?t = "length π"
  let ?τ = "trace_parallel_plan_strips ((Π)⇩I) π"
  let ?A = "(⋃(k, op) ∈ {0..<?t} × set ((Π)⇩𝒪).
    ⋃v ∈ set (add_effects_of op).
      {{ (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+ }})"
    and ?B = "(⋃(k, op) ∈ {0..<?t} × set ((Π)⇩𝒪).
      ⋃v ∈ set (delete_effects_of op).
         {{ (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯ }})"
  consider (C_in_A) "C ∈ ?A"
    | (C_in_B) "C ∈ ?B"
    using Un_iff[of C ?A ?B] cnf_of_encode_all_operator_effects_structure assms(3)
     by (metis C_in_A C_in_B)
  thus ?thesis
    proof (cases)
      case C_in_A
      then obtain k op
        where k_and_op_are: "(k, op) ∈ {0..<?t} × set((Π)⇩𝒪)"
          and "C ∈ (⋃v ∈ set (add_effects_of op).
            {{ (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+ }})"
        by blast
      then obtain v where v_in_add_effects_of_op: "v ∈ set (add_effects_of op)"
        and C_is: "C = { (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))⇧+ }"
        by blast
      thus ?thesis
        proof (cases "k < length ?τ - 1")
          case k_lt_length_τ_minus_one: True
          thus ?thesis
            proof (cases "op ∈ set (π ! k)")
              case True
              {
                then have "are_all_operators_applicable (?τ ! k) (π ! k)"
                  and "are_all_operator_effects_consistent (π ! k)"
                  using trace_parallel_plan_strips_operator_preconditions k_lt_length_τ_minus_one
                  by blast+
                hence "execute_parallel_operator (?τ ! k) (π ! k) v = Some True"
                  using execute_parallel_operator_positive_effect_if[
                    OF _ _ True v_in_add_effects_of_op, of "?τ ! k"]
                  by blast
              }
              then have τ_Suc_k_is_Some_True: "(?τ ! Suc k) v = Some True"
                using trace_parallel_plan_step_effect_is[OF k_lt_length_τ_minus_one]
                by argo
              have "𝒜 (State (Suc k) (index ?vs v))"
                using assms(6) k_lt_length_τ_minus_one τ_Suc_k_is_Some_True
                by fastforce
              thus ?thesis
                using C_is
                unfolding clause_semantics_def
                by fastforce
            next
              case False
              then have "¬𝒜 (Operator k (index ?ops op))"
                using assms(4) k_lt_length_τ_minus_one
                by blast
              thus ?thesis
                using C_is
                unfolding clause_semantics_def
                by force
            qed
        next
          case False
          then have "k ≥ length ?τ - 1" and "k < ?t"
            using k_and_op_are
            by auto
          then have "¬𝒜 (Operator k (index ?ops op))"
            using assms(5)
            by blast
          thus ?thesis
            using C_is
            unfolding clause_semantics_def
            by fastforce
        qed
    next
      ― ‹ This case is completely symmetrical to the one above. ›
      case C_in_B
      then obtain k op
        where k_and_op_are: "(k, op) ∈ {0..<?t} × set ((Π)⇩𝒪)"
          and "C ∈ (⋃v ∈ set (delete_effects_of op).
            {{ (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯ }})"
        by blast
      then obtain v where v_in_delete_effects_of_op: "v ∈ set (delete_effects_of op)"
        and C_is: "C = { (Operator k (index ?ops op))¯, (State (Suc k) (index ?vs v))¯ }"
        by blast
      thus ?thesis
        proof (cases "k < length ?τ - 1")
          case k_lt_length_τ_minus_one: True
          thus ?thesis
            proof (cases "op ∈ set (π ! k)")
              case True
              {
                then have "are_all_operators_applicable (?τ ! k) (π ! k)"
                  and "are_all_operator_effects_consistent (π ! k)"
                  using trace_parallel_plan_strips_operator_preconditions k_lt_length_τ_minus_one
                  by blast+
                hence "execute_parallel_operator (?τ ! k) (π ! k) v = Some False"
                  using execute_parallel_operator_negative_effect_if[
                    OF _ _ True v_in_delete_effects_of_op, of "?τ ! k"]
                  by blast
              }
              then have τ_Suc_k_is_Some_True: "(?τ ! Suc k) v = Some False"
                using trace_parallel_plan_step_effect_is[OF k_lt_length_τ_minus_one]
                by argo
              have "¬𝒜 (State (Suc k) (index ?vs v))"
                using assms(6) k_lt_length_τ_minus_one τ_Suc_k_is_Some_True
                by fastforce
              thus ?thesis
                using C_is
                unfolding clause_semantics_def
                by fastforce
            next
              case False
              then have "¬𝒜 (Operator k (index ?ops op))"
                using assms(4) k_lt_length_τ_minus_one
                by blast
              thus ?thesis
                using C_is
                unfolding clause_semantics_def
                by force
            qed
        next
          case False
          then have "k ≥ length ?τ - 1" and "k < ?t"
            using k_and_op_are
            by auto
          then have "¬𝒜 (Operator k (index ?ops op))"
            using assms(5)
            by blast
          thus ?thesis
            using C_is
            unfolding clause_semantics_def
            by fastforce
        qed
    qed
qed

(* TODO make private *)
lemma encode_problem_parallel_complete_iii:
  fixes Π::"'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "(Π)⇩G ⊆⇩m execute_parallel_plan ((Π)⇩I) π"
    and "∀k op. k < length (trace_parallel_plan_strips ((Π)⇩I) π) - 1
      ⟶ 𝒜 (Operator k (index (strips_problem.operators_of Π) op)) = (op ∈ set (π ! k))"
    and "∀l op. l ≥ length (trace_parallel_plan_strips ((Π)⇩I) π) - 1 ∧ l < length π
      ⟶ ¬𝒜 (Operator l (index (strips_problem.operators_of Π) op))"
    and "∀v k. k < length (trace_parallel_plan_strips ((Π)⇩I) π)
      ⟶  (𝒜 (State k (index (strips_problem.variables_of Π) v))
          ⟷ (trace_parallel_plan_strips ((Π)⇩I) π ! k) v = Some True)"
  shows "𝒜 ⊨ encode_operators Π (length π)"
proof -
  let ?t = "length π"
    and ?ops = "strips_problem.operators_of Π"
  let ?Φ⇩O = "encode_operators Π ?t"
    and ?Φ⇩P = "encode_all_operator_preconditions Π ?ops?t"
    and ?Φ⇩E = "encode_all_operator_effects Π ?ops ?t"
  {
    fix C
    assume "C ∈ cnf ?Φ⇩O"
    then consider (C_in_precondition_encoding) "C ∈ cnf ?Φ⇩P"
      | (C_in_effect_encoding) "C ∈ cnf ?Φ⇩E"
      using cnf_of_operator_encoding_structure
      by blast
    hence "clause_semantics 𝒜 C"
      proof (cases)
        case C_in_precondition_encoding
        thus ?thesis
          using encode_problem_parallel_complete_iii_a[OF assms(1, 2) _ assms(3, 4, 5)]
          by blast
      next
        case C_in_effect_encoding
        thus ?thesis
          using encode_problem_parallel_complete_iii_b[OF assms(1, 2) _ assms(3, 4, 5)]
          by blast
      qed
  }
  thus ?thesis
    using encode_operators_is_cnf[OF assms(1)] is_nnf_cnf cnf_semantics
    unfolding cnf_semantics_def
    by blast
qed

(* TODO make private *)
lemma encode_problem_parallel_complete_iv_a:
  fixes Π :: "'a strips_problem"
  assumes "STRIPS_Semantics.is_parallel_solution_for_problem Π π"
    and "∀k op. k < length (trace_parallel_plan_strips ((Π)⇩I) π) - 1
      ⟶ 𝒜 (Operator k (index (strips_problem.operators_of Π) op)) = (op ∈ set (π ! k))"
    and "∀v k. k < length (trace_parallel_plan_strips ((Π)⇩I) π)
      ⟶  (𝒜 (State k (index (strips_problem.variables_of Π) v))
          ⟷ (trace_parallel_plan_strips ((Π)⇩I) π ! k) v = Some True)"
    and "∀v l. l ≥ length (trace_parallel_plan_strips ((Π)⇩I) π) ∧ l < length π + 1
      ⟶ 𝒜 (State l (index (strips_problem.variables_of Π) v))
        = 𝒜 (State
          (length (trace_parallel_plan_strips ((Π)⇩I) π) - 1)
          (index (strips_problem.variables_of Π) v))"
    and "C ∈ ⋃ (⋃(k, v) ∈ {0..<length π} × set ((Π)⇩𝒱).
      {{{ (State k (index (strips_problem.variables_of Π) v))⇧+
          , (State (Suc k) (index (strips_problem.variables_of Π) v))¯ }
        ∪ { (Operator k (index (strips_problem.operators_of Π) op))⇧+
          |op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (add_effects_of op) }}})"
  shows "clause_semantics 𝒜 C"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
    and ?t = "length π"
  let ?τ = "trace_parallel_plan_strips ((Π)⇩I) π"
  let ?A = "(⋃(k, v) ∈ {0..<?t} × set ?vs.
    {{{ (State k (index ?vs v))⇧+, (State (Suc k) (index ?vs v))¯ }
      ∪ { (Operator k (index ?ops op))⇧+ |op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }}})"
  (* TODO refactor *)
  {
    (* TODO slow *)
    obtain C' where "C' ∈ ?A" and C_in_C': "C ∈ C'"
      using Union_iff assms(5)
      by auto
    then obtain k v
      where "(k, v) ∈ {0..<?t} × set ?vs"
      and "C' ∈ {{{ (State k (index ?vs v))⇧+, (State (Suc k) (index ?vs v))¯ }
        ∪ { (Operator k (index ?ops op))⇧+ |op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }}}"
      using UN_E
      by blast
    hence "∃k v.
      k ∈ {0..<?t}
      ∧ v ∈ set ?vs
      ∧ C = { (State k (index ?vs v))⇧+, (State (Suc k) (index ?vs v))¯ }
        ∪ { (Operator k (index ?ops op))⇧+ |op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }"
      using C_in_C'
      by blast
  }
  then obtain k v
    where k_in: "k ∈ {0..<?t}"
      and v_in_vs: "v ∈ set ?vs"
      and C_is: "C = { (State k (index ?vs v))⇧+, (State (Suc k) (index ?vs v))¯ }
        ∪ { (Operator k (index ?ops op))⇧+ |op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }"
    by blast
  show ?thesis
    proof (cases "k < length ?τ - 1")
      case k_lt_length_τ_minus_one: True
      then have k_lt_t: "k < ?t"
        using k_in
        by force
      have all_operators_applicable: "are_all_operators_applicable (?τ ! k) (π ! k)"
        and all_operator_effects_consistent: "are_all_operator_effects_consistent (π ! k)"
        using trace_parallel_plan_strips_operator_preconditions[OF k_lt_length_τ_minus_one]
        by simp+
      then consider (A) "∃op ∈ set (π ! k). v ∈ set (add_effects_of op)"
        | (B) "∃op ∈ set (π ! k). v ∈ set (delete_effects_of op)"
        | (C) "∀op ∈ set (π ! k). v ∉ set (add_effects_of op) ∧ v ∉ set (delete_effects_of op)"
        by blast
      thus ?thesis
        proof (cases)
          case A
          moreover obtain op
            where op_in_π⇩k: "op ∈ set (π ! k)"
              and v_is_add_effect: "v ∈ set (add_effects_of op)"
            using A
            by blast
          moreover {
            have "(π ! k) ∈ set π"
              using k_lt_t
              by simp
            hence "op ∈ set ?ops"
              using is_parallel_solution_for_problem_operator_set[OF assms(1) _ op_in_π⇩k]
              by blast
          }
          ultimately have "(Operator k (index ?ops op))⇧+
            ∈ { (Operator k (index ?ops op))⇧+ | op. op ∈ set ?ops ∧ v ∈ set (add_effects_of op) }"
            using v_is_add_effect
            by blast
          then have "(Operator k (index ?ops op))⇧+ ∈ C"
            using C_is
            by auto
          moreover have "𝒜 (Operator k (index ?ops op))"
            using assms(2) k_lt_length_τ_minus_one op_in_π⇩k
            by blast
          ultimately show ?thesis
            unfolding clause_semantics_def
            by force
        next
          case B
          then obtain op
            where op_in_π⇩k: "op ∈ set (π ! k)"
              and v_is_delete_effect: "v ∈ set (delete_effects_of op)"..
          then have "¬(∃op ∈ set (π ! k). v ∈ set (add_effects_of op))"
            using all_operator_effects_consistent are_all_operator_effects_consistent_set
            by fast
          then have "execute_parallel_operator (?τ ! k) (π ! k) v
             = Some False"
            using execute_parallel_operator_negative_effect_if[OF all_operators_applicable
                all_operator_effects_consistent op_in_π⇩k v_is_delete_effect]
            by blast
          moreover have "(?τ ! Suc k) v = execute_parallel_operator (?τ ! k) (π ! k) v"
            using trace_parallel_plan_step_effect_is[OF k_lt_length_τ_minus_one]
            by simp
          ultimately have "¬𝒜 (State (Suc k) (index ?vs v))"
            using assms(3) k_lt_length_τ_minus_one
            by simp
          thus ?thesis
            using C_is
            unfolding clause_semantics_def
            by simp
        next
          case C
          show ?thesis
            proof (cases "(?τ ! k) v = Some True")
              case True
              then have "𝒜 (State k (index ?vs v))"
                using assms(3) k_lt_length_τ_minus_one
                by force
              thus ?thesis
                using C_is
                unfolding clause_semantics_def
                by fastforce
            next
              case False
              {
                have "(?τ ! Suc k) = execute_parallel_operator (?τ ! k) (π ! k)"
                  using trace_parallel_plan_step_effect_is[OF k_lt_length_τ_minus_one].
                then have "(?τ ! Suc k) v = (?τ ! k) v"
                  using execute_parallel_operator_no_effect_if C
                  by fastforce
                hence "(?τ ! Suc k) v ≠ Some True"
                  using False
                  by argo
              }
              then have "¬𝒜 (State (Suc k) (index ?vs v))"
                using assms(3) k_lt_length_τ_minus_one
                by auto
              thus ?thesis
                using C_is
                unfolding clause_semantics_def
                by fastforce
            qed
        qed
    next
      case k_gte_length_τ_minus_one: False
      show ?thesis
        proof (cases "𝒜 (State (length ?τ - 1) (index ?vs v))")
          case True
          {
            have "𝒜 (State k (index ?vs v)) = 𝒜 (State (length ?τ - 1) (index ?vs v))"
              proof (cases "k = length ?τ - 1")
                case False
                then have "length ?τ ≤ k" and "k < ?t + 1"
                  using k_gte_length_τ_minus_one k_in
                  by fastforce+
                thus ?thesis
                  using assms(4)
                  by blast
              qed blast
            hence "𝒜 (State k (index ?vs v))"
              using True
              by blast
          }
          thus ?thesis
            using C_is
            unfolding clause_semantics_def
            by simp
        next
          case False
          {
            have "length ?τ ≤ Suc k" and "Suc k < ?t + 1"
              using k_gte_length_τ_minus_one k_in
              by fastforce+
            then have "𝒜 (State (Suc k) (index ?vs v)) = 𝒜 (State (length ?τ - 1) (index ?vs v))"
              using assms(4)
              by blast
            hence "¬𝒜 (State (Suc k) (index ?vs v))"
              using False
              by blast
          }
          thus ?thesis
            using C_is
            unfolding clause_semantics_def
            by fastforce
        qed
    qed
qed

(* TODO make private *)
lemma encode_problem_parallel_complete_iv_b:
  fixes Π :: "'a strips_problem"
  assumes "is_parallel_solution_for_problem Π π"
    and "∀k op. k < length (trace_parallel_plan_strips ((Π)⇩I) π) - 1
      ⟶ 𝒜 (Operator k (index (strips_problem.operators_of Π) op)) = (op ∈ set (π ! k))"
    and "∀v k. k < length (trace_parallel_plan_strips ((Π)⇩I) π)
      ⟶  (𝒜 (State k (index (strips_problem.variables_of Π) v))
          ⟷ (trace_parallel_plan_strips ((Π)⇩I) π ! k) v = Some True)"
    and "∀v l. l ≥ length (trace_parallel_plan_strips ((Π)⇩I) π) ∧ l < length π + 1
      ⟶ 𝒜 (State l (index (strips_problem.variables_of Π) v))
        = 𝒜 (State
          (length (trace_parallel_plan_strips ((Π)⇩I) π) - 1)
          (index (strips_problem.variables_of Π) v))"
    and "C ∈ ⋃ (⋃(k, v) ∈ {0..<length π} × set ((Π)⇩𝒱).
      {{{ (State k (index (strips_problem.variables_of Π) v))¯
          , (State (Suc k) (index (strips_problem.variables_of Π) v))⇧+ }
        ∪ { (Operator k (index (strips_problem.operators_of Π) op))⇧+
          |op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (delete_effects_of op) }}})"
  shows "clause_semantics 𝒜 C"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
    and ?t = "length π"
  let ?τ = "trace_parallel_plan_strips (initial_of Π) π"
  let ?A = "(⋃(k, v) ∈ {0..<?t} × set ?vs.
    {{{ (State k (index ?vs v))¯, (State (Suc k) (index ?vs v))⇧+ }
      ∪ { (Operator k (index ?ops op))⇧+
        | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (delete_effects_of op) }}})"
  (* TODO refactor *)
  {
    (* TODO slow *)
    obtain C' where "C' ∈ ?A" and C_in_C': "C ∈ C'"
      using Union_iff assms(5)
      by auto
    (* TODO slow *)
    then obtain k v
      where "(k, v) ∈ {0..<?t} × set ?vs"
      and "C' ∈ {{{ (State k (index ?vs v))¯, (State (Suc k) (index ?vs v))⇧+ }
        ∪ { (Operator k (index ?ops op))⇧+ |op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op) }}}"
      using UN_E
      by fastforce
    hence "∃k v.
      k ∈ {0..<?t}
      ∧ v ∈ set ?vs
      ∧ C = { (State k (index ?vs v))¯, (State (Suc k) (index ?vs v))⇧+ }
        ∪ { (Operator k (index ?ops op))⇧+
          | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (delete_effects_of op) }"
      using C_in_C'
      by auto
  }
  then obtain k v
    where k_in: "k ∈ {0..<?t}"
      and v_in_vs: "v ∈ set ((Π)⇩𝒱)"
      and C_is: "C = { (State k (index ?vs v))¯, (State (Suc k) (index ?vs v))⇧+ }
        ∪ { (Operator k (index ?ops op))⇧+
          | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (delete_effects_of op) }"
    by auto
  show ?thesis
    proof (cases "k < length ?τ - 1")
      case k_lt_length_τ_minus_one: True
      then have k_lt_t: "k < ?t"
        using k_in
        by force
      have all_operators_applicable: "are_all_operators_applicable (?τ ! k) (π ! k)"
        and all_operator_effects_consistent: "are_all_operator_effects_consistent (π ! k)"
        using trace_parallel_plan_strips_operator_preconditions[OF k_lt_length_τ_minus_one]
        by simp+
      then consider (A) "∃op ∈ set (π ! k). v ∈ set (delete_effects_of op)"
        | (B) "∃op ∈ set (π ! k). v ∈ set (add_effects_of op)"
        | (C) "∀op ∈ set (π ! k). v ∉ set (add_effects_of op) ∧ v ∉ set (delete_effects_of op)"
        by blast
      thus ?thesis
        proof (cases)
          case A
          moreover obtain op
            where op_in_π⇩k: "op ∈ set (π ! k)"
              and v_is_delete_effect: "v ∈ set (delete_effects_of op)"
            using A
            by blast
          moreover {
            have "(π ! k) ∈ set π"
              using k_lt_t
              by simp
            hence "op ∈ set ?ops"
              using is_parallel_solution_for_problem_operator_set[OF assms(1) _ op_in_π⇩k]
              by auto
          }
          ultimately have "(Operator k (index ?ops op))⇧+
            ∈ { (Operator k (index ?ops op))⇧+
              | op. op ∈ set ?ops ∧ v ∈ set (delete_effects_of op) }"
            using v_is_delete_effect
            by blast
          then have "(Operator k (index ?ops op))⇧+ ∈ C"
            using C_is
            by auto
          moreover have "𝒜 (Operator k (index ?ops op))"
            using assms(2) k_lt_length_τ_minus_one op_in_π⇩k
            by blast
          ultimately show ?thesis
            unfolding clause_semantics_def
            by force
        next
          case B
          then obtain op
            where op_in_π⇩k: "op ∈ set (π ! k)"
              and v_is_add_effect: "v ∈ set (add_effects_of op)"..
          then have "¬(∃op ∈ set (π ! k). v ∈ set (delete_effects_of op))"
            using all_operator_effects_consistent are_all_operator_effects_consistent_set
            by fast
          then have "execute_parallel_operator (?τ ! k) (π ! k) v = Some True"
            using execute_parallel_operator_positive_effect_if[OF all_operators_applicable
                all_operator_effects_consistent op_in_π⇩k v_is_add_effect]
            by blast
          moreover have "(?τ ! Suc k) v = execute_parallel_operator (?τ ! k) (π ! k) v"
            using trace_parallel_plan_step_effect_is[OF k_lt_length_τ_minus_one]
            by simp
          ultimately have "𝒜 (State (Suc k) (index ?vs v))"
            using assms(3) k_lt_length_τ_minus_one
            by simp
          thus ?thesis
            using C_is
            unfolding clause_semantics_def
            by simp
        next
          case C
          show ?thesis
            ― ‹ We split on cases for @{text "(?τ ! k) v = Some True"} here to avoid having to
              proof @{text "(?τ ! k) v ≠ None"}. ›
            proof (cases "(?τ ! k) v = Some True")
              case True
              {
                have "(?τ ! Suc k) = execute_parallel_operator (?τ ! k) (π ! k)"
                  using trace_parallel_plan_step_effect_is[OF k_lt_length_τ_minus_one].
                then have "(?τ ! Suc k) v = (?τ ! k) v"
                  using execute_parallel_operator_no_effect_if C
                  by fastforce
                then have "(?τ ! Suc k) v = Some True"
                  using True
                  by argo
                hence "𝒜 (State (Suc k) (index ?vs v))"
                  using assms(3) k_lt_length_τ_minus_one
                  by fastforce
              }
              thus ?thesis
                using C_is
                unfolding clause_semantics_def
                by fastforce
            next
              case False
              then have "¬𝒜 (State k (index ?vs v))"
                using assms(3) k_lt_length_τ_minus_one
                by simp
              thus ?thesis
                using C_is
                unfolding clause_semantics_def
                by fastforce
            qed
        qed
    next
      case k_gte_length_τ_minus_one: False
      show ?thesis
        proof (cases "𝒜 (State (length ?τ - 1) (index ?vs v))")
          case True
          {
            have "length ?τ ≤ Suc k" and "Suc k < ?t + 1"
              using k_gte_length_τ_minus_one k_in
              by fastforce+
            then have "𝒜 (State (Suc k) (index ?vs v)) = 𝒜 (State (length ?τ - 1) (index ?vs v))"
              using assms(4)
              by blast
            hence "𝒜 (State (Suc k) (index ?vs v))"
              using True
              by blast
          }
          thus ?thesis
            using C_is
            unfolding clause_semantics_def
            by fastforce
        next
          case False
          {
            have "𝒜 (State k (index ?vs v)) = 𝒜 (State (length ?τ - 1) (index ?vs v))"
              proof (cases "k = length ?τ - 1")
                case False
                then have "length ?τ ≤ k" and "k < ?t + 1"
                  using k_gte_length_τ_minus_one k_in
                  by fastforce+
                thus ?thesis
                  using assms(4)
                  by blast
              qed blast
            hence "¬𝒜 (State k (index ?vs v))"
              using False
              by blast
          }
          thus ?thesis
            using C_is
            unfolding clause_semantics_def
            by simp
        qed
    qed
qed

(* TODO make private *)
lemma encode_problem_parallel_complete_iv:
  fixes Π::"'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "is_parallel_solution_for_problem Π π"
    and "∀k op. k < length (trace_parallel_plan_strips ((Π)⇩I) π) - 1
      ⟶ 𝒜 (Operator k (index (strips_problem.operators_of Π) op)) = (op ∈ set (π ! k))"
    and "∀v k. k < length (trace_parallel_plan_strips ((Π)⇩I) π)
      ⟶  (𝒜 (State k (index (strips_problem.variables_of Π) v))
          ⟷ (trace_parallel_plan_strips ((Π)⇩I) π ! k) v = Some True)"
    and "∀v l. l ≥ length (trace_parallel_plan_strips ((Π)⇩I) π) ∧ l < length π + 1
      ⟶ 𝒜 (State l (index (strips_problem.variables_of Π) v))
        = 𝒜 (State
          (length (trace_parallel_plan_strips ((Π)⇩I) π) - 1)
          (index (strips_problem.variables_of Π) v))"
  shows "𝒜 ⊨ encode_all_frame_axioms Π (length π)"
proof -
  let ?Φ⇩F = "encode_all_frame_axioms Π (length π)"
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
    and ?t = "length π"
  let ?A = "⋃ (⋃(k, v) ∈ {0..<?t} × set ((Π)⇩𝒱).
    {{{ (State k (index ?vs v))⇧+, (State (Suc k) (index ?vs v))¯ }
      ∪ { (Operator k (index ?ops op))⇧+
        | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (add_effects_of op) }}})"
    and ?B = "⋃ (⋃(k, v) ∈ {0..<?t} × set ((Π)⇩𝒱).
      {{{ (State k (index ?vs v))¯, (State (Suc k) (index ?vs v))⇧+ }
        ∪ { (Operator k (index ?ops op))⇧+
          | op. op ∈ set ((Π)⇩𝒪) ∧ v ∈ set (delete_effects_of op) }}})"
  (* TODO slow (and why can only metis do this?). *)
  have cnf_Φ⇩F_is_A_union_B: "cnf ?Φ⇩F = ?A ∪ ?B"
    using cnf_of_encode_all_frame_axioms_structure
    by (simp add: cnf_of_encode_all_frame_axioms_structure)
  {
    fix C
    assume "C ∈ cnf ?Φ⇩F"
    then consider (C_in_A) "C ∈ ?A"
      | (C_in_B) "C ∈ ?B"
      using Un_iff[of C ?A ?B] cnf_Φ⇩F_is_A_union_B
      by argo
    hence "clause_semantics 𝒜 C"
      proof (cases)
        case C_in_A
        then show ?thesis
          using encode_problem_parallel_complete_iv_a[OF assms(2, 3, 4, 5) C_in_A]
          by blast
      next
        case C_in_B
        then show ?thesis
          using encode_problem_parallel_complete_iv_b[OF assms(2, 3, 4, 5) C_in_B]
          by blast
      qed
  }
  thus ?thesis
    using encode_frame_axioms_is_cnf is_nnf_cnf cnf_semantics
    unfolding cnf_semantics_def
    by blast
qed

(* TODO refactor. *)
lemma valuation_for_operator_variables_is:
  fixes Π :: "'a strips_problem"
  assumes "is_parallel_solution_for_problem Π π"
    and "k < length (trace_parallel_plan_strips ((Π)⇩I) π) - 1"
    and "op ∈ set ((Π)⇩𝒪)"
  shows "valuation_for_operator_variables Π π (trace_parallel_plan_strips ((Π)⇩I) π)
      (Operator k (index (strips_problem.operators_of Π) op))
    = (op ∈ set (π ! k))"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?τ = "trace_parallel_plan_strips ((Π)⇩I) π"
  let ?v = "Operator k (index ?ops op)"
    and ?Op = "{ Operator k (index ?ops op)
      | k op. k ∈ {0..<length ?τ - 1} ∧ op ∈ set ((Π)⇩𝒪) }"
  let ?l = "concat (map (λk. map (Pair k) (π ! k)) [0..<length ?τ - 1])"
    and ?f = "λx. Operator (fst x) (index ?ops (snd x))"
  ― ‹ show that our operator construction function is injective on
    @{text "set (concat (map (λk. map (Pair k) (π ! k)) [0..<length ?τ - 1]))"}. ›
  have k_in: "k ∈ {0..<length ?τ - 1}"
    using assms(2)
    by fastforce
  {
    (* TODO refactor. *)
    {
      fix k k' op op'
      assume k_op_in: "(k, op) ∈ set ?l" and k'_op'_in: "(k', op') ∈ set ?l"
      have "Operator k (index ?ops op) = Operator k' (index ?ops op') ⟷ (k, op) = (k', op')"
        proof (rule iffI)
          assume index_op_is_index_op': "Operator k (index ?ops op) = Operator k' (index ?ops op')"
          then have k_is_k': "k = k'"
            by fast
          moreover {
            have k'_lt: "k' < length ?τ - 1"
              using k'_op'_in
              by fastforce
            (* TODO slow *)
            have op_in: "op ∈ set (π ! k)"
              using k_op_in
              by force
            (* TODO slow *)
            then have op'_in: "op' ∈ set (π ! k)"
              using k'_op'_in k_is_k'
              by auto
            {
              have length_τ_gt_1: "length ?τ > 1"
                using assms(2)
                by linarith
              have "length ?τ - Suc 0 ≤ length π + 1 - Suc 0"
                using length_trace_parallel_plan_strips_lte_length_plan_plus_one
                using diff_le_mono
                by blast
              then have "length ?τ - 1 ≤ length π"
                by fastforce
              then have "k' < length π"
                using length_τ_gt_1 k'_lt
                by linarith
              hence "π ! k' ∈ set π"
                by simp
            }
            moreover have "op ∈ set ?ops" and "op' ∈ set ?ops"
              using is_parallel_solution_for_problem_operator_set[OF assms(1)] op_in op'_in k_is_k'
                calculation
              by auto
            ultimately have "op = op'"
              using index_op_is_index_op'
              by force
          }
          ultimately show "(k, op) = (k', op')"
            by blast
        qed fast
    }
    (* TODO slow *)
    hence "inj_on ?f (set ?l)"
      unfolding inj_on_def fst_def snd_def
      by fast
  } note inj_on_f_set_l = this
  (* TODO refactor. *)
  {
    have "set ?l = ⋃ (set ` set (map (λk. map (Pair k) (π ! k)) [0..<length ?τ - 1]))"
      using set_concat
      by metis
    also have "… = ⋃ (set ` (λk. map (Pair k) (π ! k)) ` {0..<length ?τ - 1})"
      by force
    also have "… = ⋃ ((λk. (Pair k) ` set (π ! k)) ` {0..<length ?τ - 1})"
      by force
    also have "… = ⋃((λk. { (k, op) | op. op ∈ set (π ! k) }) ` {0..<length ?τ - 1})"
      by blast
    also have "… = ⋃({{ (k, op) } | k op. k ∈ {0..<length ?τ - 1} ∧ op ∈ set (π ! k) })"
      by blast
    (* TODO slow. *)
    finally have "set ?l = ⋃((λ(k, op). { (k, op) })
      ` { (k, op). k ∈ {0..<length ?τ - 1} ∧ op ∈ set (π ! k) })"
      using setcompr_eq_image[of "λ(k, op). { (k, op) }" _]
      by auto
  } note set_l_is = this
  {
    have "Operator k (index ?ops op) ∈ ?Op"
      using assms(3) k_in
      by blast
    (* TODO slow *)
    hence "valuation_for_operator_variables Π π ?τ ?v
      = foldr (λ(k, op) 𝒜. 𝒜(Operator k (index ?ops op) := True)) ?l 𝒜⇩0 ?v"
      unfolding valuation_for_operator_variables_def override_on_def Let_def
      by auto
  } note nb = this
  show ?thesis
    proof (cases "op ∈ set (π ! k)")
      case True
      moreover have k_op_in: "(k, op) ∈ set ?l"
        using set_l_is k_in calculation
        by blast
      ― ‹ There is some problem with the pattern match in the lambda in fact \isaname{nb}, sow
        we have to do some extra work to convince Isabelle of the truth of the statement. ›
      moreover {
        let ?g = "λ_. True"
        thm foldr_fun_upd[OF inj_on_f_set_l k_op_in]
        have "?v = Operator (fst (k, op)) (index ?ops (snd (k, op)))"
          by simp
        moreover have "(λ(k, op) 𝒜. 𝒜(Operator k (index ?ops op) := True))
          = (λx 𝒜. 𝒜(Operator (fst x) (index ?ops  (snd x)) := True))"
          by fastforce
        moreover have "foldr (λx 𝒜. 𝒜(Operator (fst x) (index ?ops  (snd x)) := ?g x))
          ?l 𝒜⇩0 (Operator (fst (k, op)) (index ?ops (snd (k, op)))) = True"
          unfolding foldr_fun_upd[OF inj_on_f_set_l k_op_in]..
        ultimately have "valuation_for_operator_variables Π π ?τ ?v = True"
          using nb
          by argo
      }
      thus ?thesis
        using True
        by blast
    next
      case False
      {
        have "(k, op) ∉ set ?l"
          using False set_l_is
          by fast
        moreover {
          fix k' op'
          assume "(k', op') ∈ set ?l"
            and "?f (k', op') = ?f (k, op)"
          (* TODO slow. *)
          hence "(k', op') = (k, op)"
            using inj_on_f_set_l assms(3)
            by simp
        }
        (* TODO slow. *)
        ultimately have "Operator k (index ?ops op) ∉ ?f ` set ?l"
          using image_iff
          by force
      } note operator_not_in_f_image_set_l = this
      {
        have "𝒜⇩0 (Operator k (index ?ops op)) = False"
          by simp
        moreover have "(λ(k, op) 𝒜. 𝒜(Operator k (index ?ops op) := True))
          = (λx 𝒜. 𝒜(Operator (fst x) (index ?ops (snd x)) := True))"
          by fastforce
        ultimately have "foldr (λ(k, op) 𝒜. 𝒜(Operator k (index ?ops op) := True)) ?l 𝒜⇩0 ?v = False"
          using foldr_fun_no_upd[OF inj_on_f_set_l operator_not_in_f_image_set_l, of "λ_. True" 𝒜⇩0]
          by presburger
      }
      thus ?thesis
      using nb False
      by blast
    qed
qed

(* TODO refactor (also used in proof of completeness for ∀-step 1 encoding)
  TODO make private *)
lemma encode_problem_parallel_complete_vi_a:
  fixes Π :: "'a strips_problem"
  assumes "is_parallel_solution_for_problem Π π"
    and "k < length (trace_parallel_plan_strips ((Π)⇩I) π) - 1"
  shows "valuation_for_plan Π π (Operator k (index (strips_problem.operators_of Π) op))
    = (op ∈ set (π ! k))"
proof -
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
    and ?t = "length π"
    and ?τ = "trace_parallel_plan_strips ((Π)⇩I) π"
  let ?𝒜⇩π = "valuation_for_plan Π π"
    and ?𝒜⇩O = "valuation_for_operator_variables Π π ?τ"
    and ?Op = "{ Operator k (index ?ops op) | k op. k ∈ {0..<?t} ∧ op ∈ set ?ops }"
    and ?V = "{ State k (index ?vs v) | k v. k ∈ {0..<?t + 1} ∧ v ∈ set ?vs }"
    and ?v = "Operator k (index ?ops op)"
  {
    have "length ?τ ≤ length π + 1"
      using length_trace_parallel_plan_strips_lte_length_plan_plus_one.
    then have "length ?τ - 1 ≤ length π"
      by simp
    then have "k < ?t"
      using assms
      by fastforce
  } note k_lt_length_π = this
  show ?thesis
    proof (cases "op ∈ set ((Π)⇩𝒪)")
      case True
      {
        have "?v ∈ ?Op"
          using k_lt_length_π True
          by auto
        (* TODO slow. *)
        hence "?𝒜⇩π ?v = ?𝒜⇩O ?v"
          unfolding valuation_for_plan_def override_on_def Let_def
          by force
      }
      then show ?thesis
        using valuation_for_operator_variables_is[OF assms(1, 2) True]
        by blast
    next
      (* TODO refactor (used in the lemma below as well). *)
      case False
      {
        {
          ― ‹ We have @{text "¬index ?ops op < length ?ops"} due to the assumption that
            @{text "¬op ∈ set ?ops"}. Hence @{text "¬k ∈ {0..<?t"} and therefore
            @{text "?v ∉ ?Op"}. ›
          have "?Op = (λ(k, op). Operator k (index ?ops op)) ` ({0..<?t} × set ?ops)"
            by fast
          moreover have "¬index ?ops op < length ?ops"
            using False
            by simp
          ultimately have "?v ∉ ?Op"
            by fastforce
        }
        moreover have "?v ∉ ?V"
          by force
        (* TODO slow. *)
        ultimately have "?𝒜⇩π ?v = 𝒜⇩0 ?v"
          unfolding valuation_for_plan_def override_on_def
          by metis
        hence "¬?𝒜⇩π ?v"
          unfolding empty_valuation_def
          by blast
      }
      moreover have "(π ! k) ∈ set π"
        using k_lt_length_π
        by simp
      moreover have "op ∉ set (π ! k)"
        using is_parallel_solution_for_problem_operator_set[OF assms(1) calculation(2)] False
        by blast
      ultimately show ?thesis
        by blast
    qed
qed

(* TODO make private *)
lemma encode_problem_parallel_complete_vi_b:
  fixes Π :: "'a strips_problem"
  assumes "is_parallel_solution_for_problem Π π"
    and "l ≥ length (trace_parallel_plan_strips ((Π)⇩I) π) - 1"
    and "l < length π"
  shows "¬valuation_for_plan Π π (Operator l (index (strips_problem.operators_of Π) op))"
proof -
  (* TODO prune variables *)
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
    and ?t = "length π"
    and ?τ = "trace_parallel_plan_strips ((Π)⇩I) π"
  let ?𝒜⇩π = "valuation_for_plan Π π"
    and ?𝒜⇩O = "valuation_for_operator_variables Π π ?τ"
    and ?Op = "{ Operator k (index ?ops op) | k op. k ∈ {0..<?t} ∧ op ∈ set ?ops }"
    and ?Op' = "{ Operator k (index ?ops op) | k op. k ∈ {0..<length ?τ - 1} ∧ op ∈ set ?ops }"
    and ?V = "{ State k (index ?vs v) | k v. k ∈ {0..<?t + 1} ∧ v ∈ set ?vs }"
    and ?v = "Operator l (index ?ops op)"
  show ?thesis
    proof (cases "op ∈ set ((Π)⇩𝒪)")
      case True
      {
        {
          have "?v ∈ ?Op"
            using assms(3) True
            by auto
          (* TODO slow. *)
          hence "?𝒜⇩π ?v = ?𝒜⇩O ?v"
            unfolding valuation_for_plan_def override_on_def Let_def
            by simp
        }
        moreover {
          have "l ∉ {0..<length ?τ - 1}"
            using assms(2)
            by simp
          then have "?v ∉ ?Op'"
            by blast
          hence "?𝒜⇩O ?v = 𝒜⇩0 ?v"
            unfolding valuation_for_operator_variables_def override_on_def
            by meson
        }
        ultimately have "¬?𝒜⇩π ?v"
          unfolding empty_valuation_def
          by blast
      }
      then show ?thesis
        by blast
    next
      (* TODO refactor (used in the lemma above as well). *)
      case False
      {
        {
          ― ‹ We have @{text "¬index ?ops op < length ?ops"} due to the assumption that
            @{text "¬op ∈ set ?ops"}. Hence @{text "¬k ∈ {0..<?t"} and therefore
            @{text "?v ∉ ?Op"}. ›
          have "?Op = (λ(k, op). Operator k (index ?ops op)) ` ({0..<?t} × set ?ops)"
            by fast
          moreover have "¬index ?ops op < length ?ops"
            using False
            by simp
          ultimately have "?v ∉ ?Op"
            by fastforce
        }
        moreover have "?v ∉ ?V"
          by force
        (* TODO slow. *)
        ultimately have "?𝒜⇩π ?v = 𝒜⇩0 ?v"
          unfolding valuation_for_plan_def override_on_def
          by metis
        hence "¬?𝒜⇩π ?v"
          unfolding empty_valuation_def
          by blast
      }
      thus ?thesis
        by blast
    qed
qed

― ‹ As a corollary from lemmas \isaname{encode_problem_parallel_complete_vi_a} and
\isaname{encode_problem_parallel_complete_vi_b} we obtain the result that the constructed
valuation \<^term>‹𝒜 ≡ valuation_for_plan Π π› valuates SATPlan operator variables as false if
they are not contained in any operator set \<^term>‹π ! k› for any time point \<^term>‹k < length π›. ›
corollary encode_problem_parallel_complete_vi_d:
  (* TODO why is this necessary? *)
  fixes Π :: "'variable strips_problem"
  assumes "is_parallel_solution_for_problem Π π"
    and "k < length π"
    and "op ∉ set (π ! k)"
  shows "¬valuation_for_plan Π π (Operator k (index (strips_problem.operators_of Π) op))"
  using encode_problem_parallel_complete_vi_a[OF assms(1)] assms(3)
    encode_problem_parallel_complete_vi_b[OF assms(1) _ assms(2)] assms(3)
  by (cases "k < length (trace_parallel_plan_strips ((Π)⇩I) π) - 1"; fastforce)

(* TODO refactor List_Supplement OR rm (unused) *)
lemma list_product_is_nil_iff: "List.product xs ys = [] ⟷ xs = [] ∨ ys = []"
proof (rule iffI)
  assume product_xs_ys_is_Nil: "List.product xs ys = []"
  show "xs = [] ∨ ys = []"
    proof (rule ccontr)
      assume "¬(xs = [] ∨ ys = [])"
      then have "xs ≠ []" and "ys ≠ []"
        by simp+
      then obtain x xs' y ys' where "xs = x # xs'" and "ys = y # ys'"
        using list.exhaust
        by metis
      then have "List.product xs ys = (x, y) # map (Pair x) ys' @ List.product xs' (y # ys')"
        by simp
      thus False
        using product_xs_ys_is_Nil
        by simp
    qed
next
  assume "xs = [] ∨ ys = []"
  thus "List.product xs ys = []"
  ― ‹ First cases in the next two proof blocks follow from definition of List.product. ›
  proof (rule disjE)
    assume ys_is_Nil: "ys = []"
    show "List.product xs ys = []"
      proof (induction xs)
        case (Cons x xs)
        have "List.product (x # xs) ys = map (Pair x) ys @ List.product xs ys"
          by simp
        also have "… = [] @ List.product xs ys"
          using Nil_is_map_conv ys_is_Nil
          by blast
        finally show ?case
          using Cons.IH
          by force
      qed auto
  qed simp
qed

― ‹ We keep the state abstract by requiring a function ‹s› which takes the index
‹k› and returns state. This makes the lemma cover both cases, i.e. dynamic (e.g. the ‹k›-th
trace state) as well as static state (e.g. final trace state). ›
lemma valuation_for_state_variables_is:
  assumes "k ∈ set ks"
    and "v ∈ set vs"
  shows "foldr (λ(k, v) 𝒜. valuation_for_state vs (s k) k v 𝒜) (List.product ks vs) 𝒜⇩0
      (State k (index vs v))
    ⟷ (s k) v = Some True"
proof -
  let ?v = "State k (index vs v)"
    and ?ps = "List.product ks vs"
  let ?𝒜 = "foldr (λ(k, v) 𝒜. valuation_for_state vs (s k) k v 𝒜) ?ps 𝒜⇩0"
    and ?f = "λx. State (fst x) (index vs (snd x))"
    and ?g = "λx. (s (fst x)) (snd x) = Some True"
  have nb⇩1: "(k, v) ∈ set ?ps"
    using assms(1, 2) set_product
    by simp
  (* TODO refactor (State construction is injective on List.product ks vs). *)
  moreover {
    {
      fix x y
      assume x_in_ps: "x ∈ set ?ps" and y_in_ps: "y ∈ set ?ps"
        and "¬(?f x = ?f y ⟶ x = y)"
      then have f_x_is_f_y: "?f x = ?f y" and x_is_not_y: "x ≠ y"
        by blast+
      then obtain k' k'' v' v''
        where x_is: "x = (k', v')"
          and y_is: "y = (k'', v'')"
        by fastforce
      then consider (A) "k' ≠ k''"
        | (B) "v' ≠ v''"
        using x_is_not_y
        by blast
      hence False
        proof (cases)
          case A
          then have "?f x ≠ ?f y"
            using x_is y_is
            by simp
          thus ?thesis
            using f_x_is_f_y
            by argo
        next
          case B
          have "v' ∈ set vs" and "v'' ∈ set vs"
            using x_in_ps x_is y_in_ps y_is set_product
            by blast+
          then have "index vs v' ≠ index vs v''"
            using B
            by force
          then have "?f x ≠ ?f y"
            using x_is y_is
            by simp
          thus False
            using f_x_is_f_y
            by blast
        qed
    }
    hence "inj_on ?f (set ?ps)"
      using inj_on_def
      by blast
  } note nb⇩2 = this
  {
    have "foldr (λx. valuation_for_state vs (s (fst x)) (fst x) (snd x))
     (List.product ks vs) 𝒜⇩0 (State (fst (k, v)) (index vs (snd (k, v)))) =
    (s (fst (k, v)) (snd (k, v)) = Some True)"
      using foldr_fun_upd[OF nb⇩2 nb⇩1, of ?g 𝒜⇩0]
      by blast
    moreover have "(λx. valuation_for_state vs (s (fst x)) (fst x) (snd x))
      = (λ(k, v). valuation_for_state vs (s k) k v)"
      by fastforce
    ultimately have "?𝒜 (?f (k, v)) = ?g (k, v)"
      by simp
  }
  thus ?thesis
    by simp
qed

(* TODO make private *)
lemma encode_problem_parallel_complete_vi_c:
  fixes Π :: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "is_parallel_solution_for_problem Π π"
    and "k < length (trace_parallel_plan_strips ((Π)⇩I) π)"
  shows "valuation_for_plan Π π (State k (index (strips_problem.variables_of Π) v))
    ⟷ (trace_parallel_plan_strips ((Π)⇩I) π ! k) v = Some True"
proof -
  (* TODO prune variables *)
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
    and ?τ = "trace_parallel_plan_strips ((Π)⇩I) π"
  let ?t = "length π"
    and ?t' = "length ?τ"
  let ?𝒜⇩π = "valuation_for_plan Π π"
    and ?𝒜⇩V = "valuation_for_state_variables Π π ?τ"
    and ?𝒜⇩O = "valuation_for_state_variables Π π ?τ"
    and ?𝒜⇩1 = "foldr
      (λ(k, v) 𝒜. valuation_for_state ?vs (?τ ! k) k v 𝒜)
      (List.product [0..<?t'] ?vs) 𝒜⇩0"
    and ?Op = "{ Operator k (index ?ops op) | k op. k ∈ {0..<?t} ∧ op ∈ set ((Π)⇩𝒪) }"
    and ?Op' = "{ Operator k (index ?ops op) | k op. k ∈ {0..<?t' - 1} ∧ op ∈ set ((Π)⇩𝒪) }"
    and ?V = "{ State k (index ?vs v) | k v. k ∈ {0..<?t + 1} ∧ v ∈ set ((Π)⇩𝒱) }"
    and ?V⇩1 = "{ State k (index ?vs v) | k v. k ∈ {0..<?t'} ∧ v ∈ set ((Π)⇩𝒱) }"
    and ?V⇩2 = "{ State k (index ?vs v) | k v. k ∈ {?t'..(?t + 1)} ∧ v ∈ set ((Π)⇩𝒱) }"
    and ?v = "State k (index ?vs v)"
  have v_notin_Op: "?v ∉ ?Op"
    by blast
  have k_lte_length_π_plus_one: "k < length π + 1"
    using less_le_trans length_trace_parallel_plan_strips_lte_length_plan_plus_one assms(3)
    by blast
  show ?thesis
    proof (cases "v ∈ set ((Π)⇩𝒱)")
      case True
      {
        (* TODO refactor. *)
        {
          have "?v ∈ ?V" "?v ∉ ?Op"
            using k_lte_length_π_plus_one True
            by force+
          hence "?𝒜⇩π ?v = ?𝒜⇩V ?v"
            unfolding valuation_for_plan_def override_on_def Let_def
            by simp
        }
        moreover {
          have "?v ∈ ?V⇩1" "?v ∉ ?V⇩2"
            using assms(3) True
            by fastforce+
          hence "?𝒜⇩V ?v = ?𝒜⇩1 ?v"
            unfolding valuation_for_state_variables_def override_on_def Let_def
            by force
        }
        ultimately have "?𝒜⇩π ?v = ?𝒜⇩1 ?v"
          by blast
      }
      moreover have "k ∈ set [0..<?t']"
        using assms(3)
        by simp
      moreover have "v ∈ set (strips_problem.variables_of Π)"
        using True
        by simp
      (* TODO slow *)
      ultimately show ?thesis
        using valuation_for_state_variables_is[of k "[0..<?t']"]
        by fastforce
    next
      case False
      {
        {
          have "¬ index ?vs v < length ?vs"
            using False index_less_size_conv
            by simp
          hence "?v ∉ ?V"
            by fastforce
        }
        then have "¬?𝒜⇩π ?v"
          using v_notin_Op
          unfolding valuation_for_plan_def override_on_def empty_valuation_def Let_def
             variables_of_def operators_of_def
          by presburger
      }
      moreover have "¬(?τ ! k) v = Some True"
        using trace_parallel_plan_strips_none_if[of Π π k v] assms(1, 2, 3) False
        unfolding initial_of_def
        by force
      ultimately show ?thesis
        by blast
    qed
qed

(* TODO make private *)
lemma encode_problem_parallel_complete_vi_f:
  fixes Π :: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "is_parallel_solution_for_problem Π π"
    and "l ≥ length (trace_parallel_plan_strips ((Π)⇩I) π)"
    and "l < length π + 1"
  shows "valuation_for_plan Π π (State l (index (strips_problem.variables_of Π) v))
    = valuation_for_plan Π π
      (State (length (trace_parallel_plan_strips ((Π)⇩I) π) - 1)
      (index (strips_problem.variables_of Π) v))"
proof -
  (* TODO prune variables *)
  let ?vs = "strips_problem.variables_of Π"
    and ?ops = "strips_problem.operators_of Π"
    and ?τ = "trace_parallel_plan_strips ((Π)⇩I) π"
  let ?t = "length π"
    and ?t' = "length ?τ"
  let ?τ⇩Ω = "?τ ! (?t' - 1)"
    and ?𝒜⇩π = "valuation_for_plan Π π"
    and ?𝒜⇩V = "valuation_for_state_variables Π π ?τ"
    and ?𝒜⇩O = "valuation_for_state_variables Π π ?τ"
  let ?𝒜⇩2 = "foldr
    (λ(k, v) 𝒜. valuation_for_state (strips_problem.variables_of Π) ?τ⇩Ω k v 𝒜)
    (List.product [?t'..<length π + 2] ?vs)
    𝒜⇩0"
    and ?Op = "{ Operator k (index ?ops op) | k op. k ∈ {0..<?t} ∧ op ∈ set ((Π)⇩𝒪) }"
    and ?Op' = "{ Operator k (index ?ops op) | k op. k ∈ {0..<?t' - 1} ∧ op ∈ set ((Π)⇩𝒪) }"
    and ?V = "{ State k (index ?vs v) | k v. k ∈ {0..<?t + 1} ∧ v ∈ set ((Π)⇩𝒱) }"
    and ?V⇩1 = "{ State k (index ?vs v) | k v. k ∈ {0..<?t'} ∧ v ∈ set ((Π)⇩𝒱) }"
    and ?V⇩2 = "{ State k (index ?vs v) | k v. k ∈ {?t'..(?t + 1)} ∧ v ∈ set ((Π)⇩𝒱) }"
    and ?v = "State l (index ?vs v)"
  have v_notin_Op: "?v ∉ ?Op"
    by blast
  show ?thesis
    proof (cases "v ∈ set ((Π)⇩𝒱)")
      case True
      {
        (* TODO refactor. *)
        {
          have "?v ∈ ?V" "?v ∉ ?Op"
            using assms(4) True
            by force+
          (* TODO slow. *)
          hence "?𝒜⇩π ?v = ?𝒜⇩V ?v"
            unfolding valuation_for_plan_def override_on_def Let_def
            by simp
        }
        moreover {
          have "?v ∉ ?V⇩1" "?v ∈ ?V⇩2"
            using assms(3, 4) True
            by force+
          (* TODO slow. *)
          hence "?𝒜⇩V ?v = ?𝒜⇩2 ?v"
            unfolding valuation_for_state_variables_def override_on_def Let_def
            by auto
        }
        ultimately have "?𝒜⇩π ?v = ?𝒜⇩2 ?v"
          by blast
      } note nb = this
      moreover
      {
        have "l ∈ set [?t'..<?t + 2]"
          using assms(3, 4)
          by auto
        (* TODO slow *)
        hence "?𝒜⇩2 ?v ⟷ ?τ⇩Ω v = Some True"
          using valuation_for_state_variables_is[of l "[?t'..<?t + 2]"] True nb
          by fastforce
      }
      ultimately have "?𝒜⇩π ?v ⟷ ?τ⇩Ω v = Some True"
        by fast
      moreover {
        have "0 < ?t'"
          using trace_parallel_plan_strips_not_nil
          by blast
        then have "?t' - 1 < ?t'"
          using diff_less
          by presburger
      }
      ultimately show ?thesis
        using encode_problem_parallel_complete_vi_c[of _ _ "?t' - 1", OF assms(1, 2)]
        by blast
    next
      case False
      {
        {
          have "¬ index ?vs v < length ?vs"
            using False index_less_size_conv
            by auto
          hence "?v ∉ ?V"
            by fastforce
        }
        then have "¬?𝒜⇩π ?v"
          using v_notin_Op
          unfolding valuation_for_plan_def override_on_def empty_valuation_def Let_def
            variables_of_def operators_of_def
          by presburger
      }
      moreover {
        have "0 < ?t'"
          using trace_parallel_plan_strips_not_nil
          by blast
        then have "?t' - 1 < ?t'"
          by simp
      }
      moreover have  "¬((?τ ! (?t' - 1)) v = Some True)"
        using trace_parallel_plan_strips_none_if[of _ _ "?t' - 1" v, OF _ assms(2) calculation(2)]
          assms(1) False
        by simp
      ultimately show ?thesis
        using encode_problem_parallel_complete_vi_c[of _ _ "?t' - 1", OF assms(1, 2)]
        by blast
    qed
qed


text ‹ Let now \<^term>‹τ ≡ trace_parallel_plan_strips I π› be the trace of the plan \<^term>‹π›, \<^term>‹t ≡ length π›, and
\<^term>‹t' ≡ length τ›.

Any model of the SATPlan encoding \<^term>‹𝒜› must satisfy the following properties:
\footnote{Cf. \<^cite>‹‹Theorem 3.1, p. 1044› in "DBLP:journals/ai/RintanenHN06"› for the construction
of \<^term>‹𝒜›.}

  \begin{enumerate}
    \item for all \<^term>‹k› and for all \<^term>‹op› with \<^term>‹k < t' - 1›

      @{text[display, indent=4] "𝒜 (Operator k (index (operators_of Π) op)) = op ∈ set (π ! k)"}
    \item for all \<^term>‹l› and for all \<^term>‹op› with \<^term>‹l ≥ t' - 1› and
      \<^term>‹l < length π› we require

      @{text[display, indent=4] "𝒜 (Operator l (index (operators_of Π) op))"}
    \item for all \<^term>‹v› and for all \<^term>‹k› with \<^term>‹k < t'› we require

      @{text[display, indent=4] "𝒜 (State k (index (variables_of Π) v)) ⟶ ((τ ! k) v = Some True)"}
    \item and finally for all \<^term>‹v› and for all \<^term>‹l› with \<^term>‹l ≥ t'› and \<^term>‹l < t + 1› we require

      @{text[display, indent=4] "𝒜 (State l (index (variables_of Π) v))
        = 𝒜 (State (t' - 1) (index (variables_of Π) v))"}
  \end{enumerate}

Condition ``1.'' states that the model must reflect operator activation for all operators in the
parallel operator lists \<^term>‹π ! k› of the plan \<^term>‹π› for each time step \<^term>‹k < t' - 1› s.t. there is a
successor state in the trace. Moreover ``3.''
requires that the model is consistent with the states reached during plan execution (i.e. the
elements \<^term>‹τ ! k› for \<^term>‹k < t'› of the trace \<^term>‹τ›). Meaning that
\<^term>‹𝒜 (State k (index (strips_problem.variables_of Π) v))› for the SAT plan variable of
every state variable \<^term>‹v› at time point \<^term>‹k› if and only if \<^term>‹(τ ! k) v = Some True›
for the corresponding state \<^term>‹τ ! k› at time \<^term>‹k› (and
\<^term>‹¬𝒜 (State k (index (strips_problem.variables_of Π) v))› otherwise).

The second respectively fourth condition cover early plan termination by negating operator
activation and propagating the last reached state. Note that in the state propagation constraint,
the index is incremented by one compared to the similar constraint for operators, since operator
activations are always followed by at least one successor state.
Hence the last state in the trace has index
\<^term>‹length (trace_parallel_plan_strips ((Π::'variable strips_problem)⇩I) π) - 1› and the remaining states
take up the indexes to \<^term>‹length π + 1›.

% TODO Comments on how the partial encoding modeling follows from the construction (lemmas ...). ›

value  "stop" (* Tell document preparation to stop collecting for the last tag *)

― ‹ To show completeness---i.e. every valid parallel plan ‹π› corresponds to a model
for the SATPlan encoding ‹Φ Π (length π)›---, we simply split the
conjunction defined by the encoding into partial encodings and show that the model satisfies each
of them. ›
theorem
  encode_problem_parallel_complete:
  assumes "is_valid_problem_strips Π"
    and "is_parallel_solution_for_problem Π π"
  shows "valuation_for_plan Π π ⊨ Φ Π (length π)"
proof -
  let ?t = "length π"
    and ?I = "(Π)⇩I"
    and ?G = "(Π)⇩G"
    and ?𝒜 = "valuation_for_plan Π π"
  have nb: "?G ⊆⇩m execute_parallel_plan ?I π"
    using assms(2)
    unfolding is_parallel_solution_for_problem_def
    by force
  have "?𝒜 ⊨ Φ⇩I Π"
    using encode_problem_parallel_complete_i[OF assms(1) nb]
      encode_problem_parallel_complete_vi_c[OF assms(1, 2)]
    by presburger
  moreover have "?𝒜 ⊨ (Φ⇩G Π) ?t"
    using encode_problem_parallel_complete_ii[OF assms(1) nb]
      encode_problem_parallel_complete_vi_c[OF assms(1, 2)]
      encode_problem_parallel_complete_vi_f[OF assms(1, 2)]
    by presburger
  moreover have "?𝒜 ⊨ encode_operators Π ?t"
    using encode_problem_parallel_complete_iii[OF assms(1) nb]
      encode_problem_parallel_complete_vi_a[OF assms(2)]
      encode_problem_parallel_complete_vi_b[OF assms(2)]
      encode_problem_parallel_complete_vi_c[OF assms(1, 2)]
    by presburger
  moreover have "?𝒜 ⊨ encode_all_frame_axioms Π ?t"
    using encode_problem_parallel_complete_iv[OF assms(1, 2)]
      encode_problem_parallel_complete_vi_a[OF assms(2)]
      encode_problem_parallel_complete_vi_c[OF assms(1, 2)]
      encode_problem_parallel_complete_vi_f[OF assms(1, 2)]
    by presburger
  ultimately show ?thesis
    unfolding encode_problem_def SAT_Plan_Base.encode_problem_def
      encode_initial_state_def encode_goal_state_def
    by auto
qed

end