[STATEMENT]
lemma encode_problem_serializable_sound_i:
  assumes "is_valid_problem_strips \<Pi>"
    and "\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t"
    and "k < t"
    and "ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))"
  shows "are_all_operators_non_interfering ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
let ?ops = "strips_problem.operators_of \<Pi>"
    and ?\<pi> = "\<Phi>\<inverse> \<Pi> \<A> t"
    and ?\<Phi>\<^sub>X = "encode_interfering_operator_exclusion \<Pi> t"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
let ?\<pi>\<^sub>k = "(\<Phi>\<inverse> \<Pi> \<A> t) ! k"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
(* TODO refactor *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
assume C_in: "C \<in> cnf ?\<Phi>\<^sub>X"
[PROOF STATE]
proof (state)
this:
C \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
have "cnf_semantics \<A> (cnf ?\<Phi>\<^sub>X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf_semantics \<A> (cnf (encode_interfering_operator_exclusion \<Pi> t))
[PROOF STEP]
using cnf_semantics_monotonous_in_cnf_subsets_if[OF assms(2)
        is_cnf_encode_problem_with_operator_interference_exclusion[OF assms(1)]
        cnf_of_encode_problem_with_operator_interference_exclusion_structure(5)]
[PROOF STATE]
proof (prove)
using this:
cnf_semantics \<A> (cnf (encode_interfering_operator_exclusion \<Pi> t))

goal (1 subgoal):
 1. cnf_semantics \<A> (cnf (encode_interfering_operator_exclusion \<Pi> t))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cnf_semantics \<A> (cnf (encode_interfering_operator_exclusion \<Pi> t))

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
hence "clause_semantics \<A> C"
[PROOF STATE]
proof (prove)
using this:
cnf_semantics \<A> (cnf (encode_interfering_operator_exclusion \<Pi> t))

goal (1 subgoal):
 1. clause_semantics \<A> C
[PROOF STEP]
unfolding cnf_semantics_def
[PROOF STATE]
proof (prove)
using this:
\<forall>C\<in>cnf (encode_interfering_operator_exclusion \<Pi> t). clause_semantics \<A> C

goal (1 subgoal):
 1. clause_semantics \<A> C
[PROOF STEP]
using C_in
[PROOF STATE]
proof (prove)
using this:
\<forall>C\<in>cnf (encode_interfering_operator_exclusion \<Pi> t). clause_semantics \<A> C
C \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)

goal (1 subgoal):
 1. clause_semantics \<A> C
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
clause_semantics \<A> C

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?C2 \<in> cnf (encode_interfering_operator_exclusion \<Pi> t) \<Longrightarrow> clause_semantics \<A> ?C2

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
note nb\<^sub>1 = this
[PROOF STATE]
proof (state)
this:
?C2 \<in> cnf (encode_interfering_operator_exclusion \<Pi> t) \<Longrightarrow> clause_semantics \<A> ?C2

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?C2 \<in> cnf (encode_interfering_operator_exclusion \<Pi> t) \<Longrightarrow> clause_semantics \<A> ?C2

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
fix op\<^sub>1 op\<^sub>2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
assume "op\<^sub>1 \<in> set ?\<pi>\<^sub>k" and "op\<^sub>2 \<in> set ?\<pi>\<^sub>k"
      and index_op\<^sub>1_is_not_index_op\<^sub>2: "index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2"
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
have op\<^sub>1_in: "op\<^sub>1 \<in> set ?ops" and \<A>_models_op\<^sub>1:"\<A> (Operator k (index ?ops op\<^sub>1))"
      and op\<^sub>2_in: "op\<^sub>2 \<in> set ?ops" and \<A>_models_op\<^sub>2: "\<A> (Operator k (index ?ops op\<^sub>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>) &&& \<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) &&& op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>) &&& \<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))
[PROOF STEP]
using decode_plan_step_element_then[OF assms(3)] calculation
[PROOF STATE]
proof (prove)
using this:
?op \<in> set ((\<Phi>\<inverse> ?\<Pi> ?\<A> t) ! k) \<Longrightarrow> ?op \<in> set (?\<Pi>\<^sub>\<O>)
?op \<in> set ((\<Phi>\<inverse> ?\<Pi> ?\<A> t) ! k) \<Longrightarrow> ?\<A> (Operator k (index (?\<Pi>\<^sub>\<O>) ?op))
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2

goal (1 subgoal):
 1. (op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>) &&& \<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) &&& op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>) &&& \<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))
[PROOF STEP]
unfolding decode_plan_def
[PROOF STATE]
proof (prove)
using this:
?op \<in> set (map (decode_plan' ?\<Pi> ?\<A>) [0..<t] ! k) \<Longrightarrow> ?op \<in> set (?\<Pi>\<^sub>\<O>)
?op \<in> set (map (decode_plan' ?\<Pi> ?\<A>) [0..<t] ! k) \<Longrightarrow> ?\<A> (Operator k (index (?\<Pi>\<^sub>\<O>) ?op))
op\<^sub>1 \<in> set (map (decode_plan' \<Pi> \<A>) [0..<t] ! k)
op\<^sub>2 \<in> set (map (decode_plan' \<Pi> \<A>) [0..<t] ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2

goal (1 subgoal):
 1. (op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>) &&& \<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) &&& op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>) &&& \<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>)
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>)
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>)
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
let ?C = "{ (Operator k (index ?ops op\<^sub>1))\<inverse>, (Operator k (index ?ops op\<^sub>2))\<inverse> }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
assume "are_operators_interfering op\<^sub>1 op\<^sub>2"
[PROOF STATE]
proof (state)
this:
are_operators_interfering op\<^sub>1 op\<^sub>2

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
are_operators_interfering op\<^sub>1 op\<^sub>2

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
have "?C \<in> cnf ?\<Phi>\<^sub>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
using cnf_of_encode_interfering_operator_exclusion_contains_clause_if[OF
            assms(3) op\<^sub>1_in op\<^sub>2_in index_op\<^sub>1_is_not_index_op\<^sub>2] calculation
[PROOF STATE]
proof (prove)
using this:
are_operators_interfering op\<^sub>1 op\<^sub>2 \<Longrightarrow> {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
are_operators_interfering op\<^sub>1 op\<^sub>2

goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
have "\<not>clause_semantics \<A> ?C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> clause_semantics \<A> {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}
[PROOF STEP]
using \<A>_models_op\<^sub>1 \<A>_models_op\<^sub>2
[PROOF STATE]
proof (prove)
using this:
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))

goal (1 subgoal):
 1. \<not> clause_semantics \<A> {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}
[PROOF STEP]
unfolding clause_semantics_def
[PROOF STATE]
proof (prove)
using this:
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))

goal (1 subgoal):
 1. \<not> (\<exists>L\<in>{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}. lit_semantics \<A> L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> clause_semantics \<A> {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
are_operators_interfering op\<^sub>1 op\<^sub>2
{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
\<not> clause_semantics \<A> {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
are_operators_interfering op\<^sub>1 op\<^sub>2
{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
\<not> clause_semantics \<A> {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}

goal (1 subgoal):
 1. False
[PROOF STEP]
using nb\<^sub>1
[PROOF STATE]
proof (prove)
using this:
are_operators_interfering op\<^sub>1 op\<^sub>2
{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
\<not> clause_semantics \<A> {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}
?C2 \<in> cnf (encode_interfering_operator_exclusion \<Pi> t) \<Longrightarrow> clause_semantics \<A> ?C2

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
are_operators_interfering op\<^sub>1 op\<^sub>2 \<Longrightarrow> False

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>)
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))
are_operators_interfering op\<^sub>1 op\<^sub>2 \<Longrightarrow> False
[PROOF STEP]
have "\<not>are_operators_interfering op\<^sub>1 op\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>)
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)
\<A> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))
are_operators_interfering op\<^sub>1 op\<^sub>2 \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> are_operators_interfering op\<^sub>1 op\<^sub>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> are_operators_interfering op\<^sub>1 op\<^sub>2

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?op\<^sub>12 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k); ?op\<^sub>22 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k); index (\<Pi>\<^sub>\<O>) ?op\<^sub>12 \<noteq> index (\<Pi>\<^sub>\<O>) ?op\<^sub>22\<rbrakk> \<Longrightarrow> \<not> are_operators_interfering ?op\<^sub>12 ?op\<^sub>22

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
note nb\<^sub>3 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?op\<^sub>12 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k); ?op\<^sub>22 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k); index (\<Pi>\<^sub>\<O>) ?op\<^sub>12 \<noteq> index (\<Pi>\<^sub>\<O>) ?op\<^sub>22\<rbrakk> \<Longrightarrow> \<not> are_operators_interfering ?op\<^sub>12 ?op\<^sub>22

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_valid_problem_strips \<Pi>
\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t
k < t
ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
proof (induction ops)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
case (Cons op\<^sub>1 ops)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops
is_valid_problem_strips \<Pi>
\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t
k < t
op\<^sub>1 # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
have "are_all_operators_non_interfering ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
using Cons.IH[OF Cons.prems(1, 2, 3) Cons_in_subseqsD[OF Cons.prems(4)]]
[PROOF STATE]
proof (prove)
using this:
are_all_operators_non_interfering ops

goal (1 subgoal):
 1. are_all_operators_non_interfering ops
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
are_all_operators_non_interfering ops

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
are_all_operators_non_interfering ops

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
are_all_operators_non_interfering ops

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
fix op\<^sub>2
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
assume op\<^sub>2_in_ops: "op\<^sub>2 \<in> set ops"
[PROOF STATE]
proof (state)
this:
op\<^sub>2 \<in> set ops

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
op\<^sub>2 \<in> set ops

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
have op\<^sub>1_in_\<pi>\<^sub>k: "op\<^sub>1 \<in> set ?\<pi>\<^sub>k" and op\<^sub>2_in_\<pi>\<^sub>k: "op\<^sub>2 \<in> set ?\<pi>\<^sub>k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k) &&& op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
using element_of_subseqs_then_subset[OF Cons.prems(4)] calculation(1)
[PROOF STATE]
proof (prove)
using this:
set (op\<^sub>1 # ops) \<subseteq> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ops

goal (1 subgoal):
 1. op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k) &&& op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
by auto+
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
have "distinct (op\<^sub>1 # ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (op\<^sub>1 # ops)
[PROOF STEP]
using subseqs_distinctD[OF Cons.prems(4)]
              decode_plan_step_distinct[OF Cons.prems(3)]
[PROOF STATE]
proof (prove)
using this:
distinct ((\<Phi>\<inverse> \<Pi> \<A> t) ! k) \<Longrightarrow> distinct (op\<^sub>1 # ops)
distinct ((\<Phi>\<inverse> ?\<Pi> ?\<A> t) ! k)

goal (1 subgoal):
 1. distinct (op\<^sub>1 # ops)
[PROOF STEP]
unfolding decode_plan_def
[PROOF STATE]
proof (prove)
using this:
distinct (map (decode_plan' \<Pi> \<A>) [0..<t] ! k) \<Longrightarrow> distinct (op\<^sub>1 # ops)
distinct (map (decode_plan' ?\<Pi> ?\<A>) [0..<t] ! k)

goal (1 subgoal):
 1. distinct (op\<^sub>1 # ops)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (op\<^sub>1 # ops)

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (op\<^sub>1 # ops)

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
have "op\<^sub>1 \<in> set ?ops" and "op\<^sub>2 \<in> set ?ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>) &&& op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)
[PROOF STEP]
using decode_plan_step_element_then(1)[OF Cons.prems(3)] op\<^sub>1_in_\<pi>\<^sub>k op\<^sub>2_in_\<pi>\<^sub>k
[PROOF STATE]
proof (prove)
using this:
?op \<in> set ((\<Phi>\<inverse> ?\<Pi> ?\<A> t) ! k) \<Longrightarrow> ?op \<in> set (?\<Pi>\<^sub>\<O>)
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)

goal (1 subgoal):
 1. op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>) &&& op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)
[PROOF STEP]
unfolding decode_plan_def
[PROOF STATE]
proof (prove)
using this:
?op \<in> set (map (decode_plan' ?\<Pi> ?\<A>) [0..<t] ! k) \<Longrightarrow> ?op \<in> set (?\<Pi>\<^sub>\<O>)
op\<^sub>1 \<in> set (map (decode_plan' \<Pi> \<A>) [0..<t] ! k)
op\<^sub>2 \<in> set (map (decode_plan' \<Pi> \<A>) [0..<t] ! k)

goal (1 subgoal):
 1. op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>) &&& op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>)
op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>)
op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
have "op\<^sub>1 \<noteq> op\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op\<^sub>1 \<noteq> op\<^sub>2
[PROOF STEP]
using op\<^sub>2_in_ops calculation(1)
[PROOF STATE]
proof (prove)
using this:
op\<^sub>2 \<in> set ops
distinct (op\<^sub>1 # ops)

goal (1 subgoal):
 1. op\<^sub>1 \<noteq> op\<^sub>2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<noteq> op\<^sub>2

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct (op\<^sub>1 # ops)
op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>)
op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)
op\<^sub>1 \<noteq> op\<^sub>2
[PROOF STEP]
have "index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
distinct (op\<^sub>1 # ops)
op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>)
op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)
op\<^sub>1 \<noteq> op\<^sub>2

goal (1 subgoal):
 1. index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
[PROOF STEP]
using index_eq_index_conv
[PROOF STATE]
proof (prove)
using this:
distinct (op\<^sub>1 # ops)
op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>)
op\<^sub>2 \<in> set (\<Pi>\<^sub>\<O>)
op\<^sub>1 \<noteq> op\<^sub>2
?x \<in> set ?xs \<or> ?y \<in> set ?xs \<Longrightarrow> (index ?xs ?x = index ?xs ?y) = (?x = ?y)

goal (1 subgoal):
 1. index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
op\<^sub>2 \<in> set ops
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
[PROOF STEP]
have "\<not>are_operators_interfering op\<^sub>1 op\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
op\<^sub>2 \<in> set ops
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2

goal (1 subgoal):
 1. \<not> are_operators_interfering op\<^sub>1 op\<^sub>2
[PROOF STEP]
using nb\<^sub>3
[PROOF STATE]
proof (prove)
using this:
op\<^sub>2 \<in> set ops
op\<^sub>1 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
op\<^sub>2 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
\<lbrakk>?op\<^sub>12 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k); ?op\<^sub>22 \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k); index (\<Pi>\<^sub>\<O>) ?op\<^sub>12 \<noteq> index (\<Pi>\<^sub>\<O>) ?op\<^sub>22\<rbrakk> \<Longrightarrow> \<not> are_operators_interfering ?op\<^sub>12 ?op\<^sub>22

goal (1 subgoal):
 1. \<not> are_operators_interfering op\<^sub>1 op\<^sub>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> are_operators_interfering op\<^sub>1 op\<^sub>2

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?op\<^sub>22 \<in> set ops \<Longrightarrow> \<not> are_operators_interfering op\<^sub>1 ?op\<^sub>22

goal (2 subgoals):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
 2. \<And>a ops. \<lbrakk>\<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ops; is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; a # ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering (a # ops)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
are_all_operators_non_interfering ops
?op\<^sub>22 \<in> set ops \<Longrightarrow> \<not> are_operators_interfering op\<^sub>1 ?op\<^sub>22
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
are_all_operators_non_interfering ops
?op\<^sub>22 \<in> set ops \<Longrightarrow> \<not> are_operators_interfering op\<^sub>1 ?op\<^sub>22

goal (1 subgoal):
 1. are_all_operators_non_interfering (op\<^sub>1 # ops)
[PROOF STEP]
using list_all_iff
[PROOF STATE]
proof (prove)
using this:
are_all_operators_non_interfering ops
?op\<^sub>22 \<in> set ops \<Longrightarrow> \<not> are_operators_interfering op\<^sub>1 ?op\<^sub>22
list_all ?P ?x = Ball (set ?x) ?P

goal (1 subgoal):
 1. are_all_operators_non_interfering (op\<^sub>1 # ops)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
are_all_operators_non_interfering (op\<^sub>1 # ops)

goal (1 subgoal):
 1. \<lbrakk>is_valid_problem_strips \<Pi>; \<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t; k < t; [] \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering []
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
are_all_operators_non_interfering ops

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem encode_problem_serializable_sound:
  assumes "is_valid_problem_strips \<Pi>"
    and "\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t"
  shows "is_parallel_solution_for_problem \<Pi> (\<Phi>\<inverse> \<Pi> \<A> t)"
    and "\<forall>k < length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_parallel_solution_for_problem \<Pi> (\<Phi>\<inverse> \<Pi> \<A> t) &&& \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_parallel_solution_for_problem \<Pi> (\<Phi>\<inverse> \<Pi> \<A> t)
 2. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_parallel_solution_for_problem \<Pi> (\<Phi>\<inverse> \<Pi> \<A> t)
 2. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
have "\<A> \<Turnstile> SAT_Plan_Base.encode_initial_state \<Pi>"
      and "\<A> \<Turnstile> SAT_Plan_Base.encode_operators \<Pi> t"
      and "\<A> \<Turnstile> SAT_Plan_Base.encode_all_frame_axioms \<Pi> t"
      and "\<A> \<Turnstile> SAT_Plan_Base.encode_goal_state \<Pi> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<A> \<Turnstile> \<Phi>\<^sub>I \<Pi> &&& \<A> \<Turnstile> encode_operators \<Pi> t) &&& \<A> \<Turnstile> encode_all_frame_axioms \<Pi> t &&& \<A> \<Turnstile> (\<Phi>\<^sub>G \<Pi>) t
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t

goal (1 subgoal):
 1. (\<A> \<Turnstile> \<Phi>\<^sub>I \<Pi> &&& \<A> \<Turnstile> encode_operators \<Pi> t) &&& \<A> \<Turnstile> encode_all_frame_axioms \<Pi> t &&& \<A> \<Turnstile> (\<Phi>\<^sub>G \<Pi>) t
[PROOF STEP]
unfolding encode_problem_with_operator_interference_exclusion_def
[PROOF STATE]
proof (prove)
using this:
\<A> \<Turnstile> \<Phi>\<^sub>I \<Pi> \<^bold>\<and> (encode_operators \<Pi> t \<^bold>\<and> (encode_all_frame_axioms \<Pi> t \<^bold>\<and> (encode_interfering_operator_exclusion \<Pi> t \<^bold>\<and> (\<Phi>\<^sub>G \<Pi>) t)))

goal (1 subgoal):
 1. (\<A> \<Turnstile> \<Phi>\<^sub>I \<Pi> &&& \<A> \<Turnstile> encode_operators \<Pi> t) &&& \<A> \<Turnstile> encode_all_frame_axioms \<Pi> t &&& \<A> \<Turnstile> (\<Phi>\<^sub>G \<Pi>) t
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
\<A> \<Turnstile> \<Phi>\<^sub>I \<Pi>
\<A> \<Turnstile> encode_operators \<Pi> t
\<A> \<Turnstile> encode_all_frame_axioms \<Pi> t
\<A> \<Turnstile> (\<Phi>\<^sub>G \<Pi>) t

goal (2 subgoals):
 1. is_parallel_solution_for_problem \<Pi> (\<Phi>\<inverse> \<Pi> \<A> t)
 2. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<A> \<Turnstile> \<Phi>\<^sub>I \<Pi>
\<A> \<Turnstile> encode_operators \<Pi> t
\<A> \<Turnstile> encode_all_frame_axioms \<Pi> t
\<A> \<Turnstile> (\<Phi>\<^sub>G \<Pi>) t
[PROOF STEP]
have "\<A> \<Turnstile> SAT_Plan_Base.encode_problem \<Pi> t"
[PROOF STATE]
proof (prove)
using this:
\<A> \<Turnstile> \<Phi>\<^sub>I \<Pi>
\<A> \<Turnstile> encode_operators \<Pi> t
\<A> \<Turnstile> encode_all_frame_axioms \<Pi> t
\<A> \<Turnstile> (\<Phi>\<^sub>G \<Pi>) t

goal (1 subgoal):
 1. \<A> \<Turnstile> \<Phi> \<Pi> t
[PROOF STEP]
unfolding SAT_Plan_Base.encode_problem_def
[PROOF STATE]
proof (prove)
using this:
\<A> \<Turnstile> \<Phi>\<^sub>I \<Pi>
\<A> \<Turnstile> encode_operators \<Pi> t
\<A> \<Turnstile> encode_all_frame_axioms \<Pi> t
\<A> \<Turnstile> (\<Phi>\<^sub>G \<Pi>) t

goal (1 subgoal):
 1. \<A> \<Turnstile> \<Phi>\<^sub>I \<Pi> \<^bold>\<and> (encode_operators \<Pi> t \<^bold>\<and> (encode_all_frame_axioms \<Pi> t \<^bold>\<and> (\<Phi>\<^sub>G \<Pi>) t))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<A> \<Turnstile> \<Phi> \<Pi> t

goal (2 subgoals):
 1. is_parallel_solution_for_problem \<Pi> (\<Phi>\<inverse> \<Pi> \<A> t)
 2. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<A> \<Turnstile> \<Phi> \<Pi> t

goal (2 subgoals):
 1. is_parallel_solution_for_problem \<Pi> (\<Phi>\<inverse> \<Pi> \<A> t)
 2. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
thus "is_parallel_solution_for_problem \<Pi> (\<Phi>\<inverse> \<Pi> \<A> t)"
[PROOF STATE]
proof (prove)
using this:
\<A> \<Turnstile> \<Phi> \<Pi> t

goal (1 subgoal):
 1. is_parallel_solution_for_problem \<Pi> (\<Phi>\<inverse> \<Pi> \<A> t)
[PROOF STEP]
using encode_problem_parallel_sound assms(1, 2)
[PROOF STATE]
proof (prove)
using this:
\<A> \<Turnstile> \<Phi> \<Pi> t
\<lbrakk>is_valid_problem_strips ?\<Pi>; ?\<A> \<Turnstile> \<Phi> ?\<Pi> ?t\<rbrakk> \<Longrightarrow> is_parallel_solution_for_problem ?\<Pi> (\<Phi>\<inverse> ?\<Pi> ?\<A> ?t)
is_valid_problem_strips \<Pi>
\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t

goal (1 subgoal):
 1. is_parallel_solution_for_problem \<Pi> (\<Phi>\<inverse> \<Pi> \<A> t)
[PROOF STEP]
unfolding decode_plan_def
[PROOF STATE]
proof (prove)
using this:
\<A> \<Turnstile> \<Phi> \<Pi> t
\<lbrakk>is_valid_problem_strips ?\<Pi>; ?\<A> \<Turnstile> \<Phi> ?\<Pi> ?t\<rbrakk> \<Longrightarrow> is_parallel_solution_for_problem ?\<Pi> (map (decode_plan' ?\<Pi> ?\<A>) [0..<?t])
is_valid_problem_strips \<Pi>
\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t

goal (1 subgoal):
 1. is_parallel_solution_for_problem \<Pi> (map (decode_plan' \<Pi> \<A>) [0..<t])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_parallel_solution_for_problem \<Pi> (\<Phi>\<inverse> \<Pi> \<A> t)

goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
let ?\<pi> = "\<Phi>\<inverse> \<Pi> \<A> t"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
assume "k < t"
[PROOF STATE]
proof (state)
this:
k < t

goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < t

goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
have "?\<pi> ! k \<in> set (subseqs (?\<pi> ! k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Phi>\<inverse> \<Pi> \<A> t) ! k \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))
[PROOF STEP]
using subseqs_refl
[PROOF STATE]
proof (prove)
using this:
?xs \<in> set (subseqs ?xs)

goal (1 subgoal):
 1. (\<Phi>\<inverse> \<Pi> \<A> t) ! k \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Phi>\<inverse> \<Pi> \<A> t) ! k \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))

goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k < t
(\<Phi>\<inverse> \<Pi> \<A> t) ! k \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))
[PROOF STEP]
have "are_all_operators_non_interfering (?\<pi> ! k)"
[PROOF STATE]
proof (prove)
using this:
k < t
(\<Phi>\<inverse> \<Pi> \<A> t) ! k \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))

goal (1 subgoal):
 1. are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
using encode_problem_serializable_sound_i[OF assms]
[PROOF STATE]
proof (prove)
using this:
k < t
(\<Phi>\<inverse> \<Pi> \<A> t) ! k \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! k))
\<lbrakk>?k < t; ?ops \<in> set (subseqs ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ?ops

goal (1 subgoal):
 1. are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
unfolding SAT_Plan_Base.decode_plan_def decode_plan_def
[PROOF STATE]
proof (prove)
using this:
k < t
map (decode_plan' \<Pi> \<A>) [0..<t] ! k \<in> set (subseqs (map (decode_plan' \<Pi> \<A>) [0..<t] ! k))
\<lbrakk>?k < t; ?ops \<in> set (subseqs (map (decode_plan' \<Pi> \<A>) [0..<t] ! ?k))\<rbrakk> \<Longrightarrow> are_all_operators_non_interfering ?ops

goal (1 subgoal):
 1. are_all_operators_non_interfering (map (decode_plan' \<Pi> \<A>) [0..<t] ! k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)

goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?k2 < t \<Longrightarrow> are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)

goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?k2 < t \<Longrightarrow> are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)

goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
have "length ?\<pi> = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (\<Phi>\<inverse> \<Pi> \<A> t) = t
[PROOF STEP]
unfolding SAT_Plan_Base.decode_plan_def decode_plan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (decode_plan' \<Pi> \<A>) [0..<t]) = t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (\<Phi>\<inverse> \<Pi> \<A> t) = t

goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?k2 < t \<Longrightarrow> are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
length (\<Phi>\<inverse> \<Pi> \<A> t) = t
[PROOF STEP]
show "\<forall>k < length ?\<pi>. are_all_operators_non_interfering (?\<pi> ! k)"
[PROOF STATE]
proof (prove)
using this:
?k2 < t \<Longrightarrow> are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
length (\<Phi>\<inverse> \<Pi> \<A> t) = t

goal (1 subgoal):
 1. \<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)

goal:
No subgoals!
[PROOF STEP]
qed