[STATEMENT]
lemma encode_problem_with_operator_interference_exclusion_complete_i:
  assumes "is_valid_problem_strips \<Pi>"
    and "is_parallel_solution_for_problem \<Pi> \<pi>"
    and "\<forall>k < length \<pi>. are_all_operators_non_interfering (\<pi> ! k)"
  shows "valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
let ?\<A> = "valuation_for_plan \<Pi> \<pi>"
    and ?\<Phi>\<^sub>X = "encode_interfering_operator_exclusion \<Pi> (length \<pi>)"
    and ?ops = "strips_problem.operators_of \<Pi>"
    and ?t = "length \<pi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
let ?\<tau> = "trace_parallel_plan_strips ((\<Pi>)\<^sub>I) \<pi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
let ?Ops = "{ (op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (operators_of \<Pi>) \<times> set (operators_of \<Pi>)
    \<and> index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2
    \<and> are_operators_interfering op\<^sub>1 op\<^sub>2 }"
    and ?f = "\<lambda>(op\<^sub>1, op\<^sub>2). {{{ (Operator k (index ?ops op\<^sub>1))\<inverse>, (Operator k (index ?ops op\<^sub>2))\<inverse> }}
      | k. k \<in> {0..<length \<pi>} }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
let ?A = "\<Union>(?f ` ?Ops)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
let ?B = "\<Union>?A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
have nb\<^sub>1: "\<forall>ops \<in> set \<pi>. \<forall>op \<in> set ops. op \<in> set (operators_of \<Pi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ops\<in>set \<pi>. \<forall>op\<in>set ops. op \<in> set (\<Pi>\<^sub>\<O>)
[PROOF STEP]
using is_parallel_solution_for_problem_operator_set[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?ops \<in> set \<pi>; ?op \<in> set ?ops\<rbrakk> \<Longrightarrow> ?op \<in> set (\<Pi>\<^sub>\<O>)

goal (1 subgoal):
 1. \<forall>ops\<in>set \<pi>. \<forall>op\<in>set ops. op \<in> set (\<Pi>\<^sub>\<O>)
[PROOF STEP]
unfolding operators_of_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?ops \<in> set \<pi>; ?op \<in> set ?ops\<rbrakk> \<Longrightarrow> ?op \<in> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>)

goal (1 subgoal):
 1. \<forall>ops\<in>set \<pi>. \<forall>op\<in>set ops. op \<in> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>ops\<in>set \<pi>. \<forall>op\<in>set ops. op \<in> set (\<Pi>\<^sub>\<O>)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
(* TODO refactor (characterization of \<A>) *)
[PROOF STATE]
proof (state)
this:
\<forall>ops\<in>set \<pi>. \<forall>op\<in>set ops. op \<in> set (\<Pi>\<^sub>\<O>)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>ops\<in>set \<pi>. \<forall>op\<in>set ops. op \<in> set (\<Pi>\<^sub>\<O>)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
fix k op
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
assume "k < length \<pi>" and "op \<in> set (\<pi> ! k)"
[PROOF STATE]
proof (state)
this:
k < length \<pi>
op \<in> set (\<pi> ! k)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
hence "lit_semantics ?\<A> ((Operator k (index ?ops op))\<^sup>+) = (k < length ?\<tau> - 1)"
[PROOF STATE]
proof (prove)
using this:
k < length \<pi>
op \<in> set (\<pi> ! k)

goal (1 subgoal):
 1. lit_semantics (valuation_for_plan \<Pi> \<pi>) ((Operator k (index (\<Pi>\<^sub>\<O>) op))\<^sup>+) = (k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) \<pi>) - 1)
[PROOF STEP]
using encode_problem_parallel_complete_vi_a[OF assms(2)]
        encode_problem_parallel_complete_vi_b[OF assms(2)] initial_of_def
[PROOF STATE]
proof (prove)
using this:
k < length \<pi>
op \<in> set (\<pi> ! k)
?k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) \<pi>) - 1 \<Longrightarrow> valuation_for_plan \<Pi> \<pi> (Operator ?k (index (\<Pi>\<^sub>\<O>) ?op)) = (?op \<in> set (\<pi> ! ?k))
\<lbrakk>length (trace_parallel_plan_strips (\<Pi>\<^sub>I) \<pi>) - 1 \<le> ?l; ?l < length \<pi>\<rbrakk> \<Longrightarrow> \<not> valuation_for_plan \<Pi> \<pi> (Operator ?l (index (\<Pi>\<^sub>\<O>) ?op))
initial_of \<equiv> id \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso

goal (1 subgoal):
 1. lit_semantics (valuation_for_plan \<Pi> \<pi>) ((Operator k (index (\<Pi>\<^sub>\<O>) op))\<^sup>+) = (k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) \<pi>) - 1)
[PROOF STEP]
by(cases "k < length ?\<tau> - 1"; simp)
[PROOF STATE]
proof (state)
this:
lit_semantics (valuation_for_plan \<Pi> \<pi>) ((Operator k (index (\<Pi>\<^sub>\<O>) op))\<^sup>+) = (k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) \<pi>) - 1)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?k2 < length \<pi>; ?op2 \<in> set (\<pi> ! ?k2)\<rbrakk> \<Longrightarrow> lit_semantics (valuation_for_plan \<Pi> \<pi>) ((Operator ?k2 (index (\<Pi>\<^sub>\<O>) ?op2))\<^sup>+) = (?k2 < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) \<pi>) - 1)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
note nb\<^sub>2 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?k2 < length \<pi>; ?op2 \<in> set (\<pi> ! ?k2)\<rbrakk> \<Longrightarrow> lit_semantics (valuation_for_plan \<Pi> \<pi>) ((Operator ?k2 (index (\<Pi>\<^sub>\<O>) ?op2))\<^sup>+) = (?k2 < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) \<pi>) - 1)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?k2 < length \<pi>; ?op2 \<in> set (\<pi> ! ?k2)\<rbrakk> \<Longrightarrow> lit_semantics (valuation_for_plan \<Pi> \<pi>) ((Operator ?k2 (index (\<Pi>\<^sub>\<O>) ?op2))\<^sup>+) = (?k2 < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) \<pi>) - 1)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
fix k op\<^sub>1 op\<^sub>2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
assume "k < length \<pi>"
      and "op\<^sub>1 \<in> set (\<pi> ! k)"
      and "index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2"
      and "are_operators_interfering op\<^sub>1 op\<^sub>2"
[PROOF STATE]
proof (state)
this:
k < length \<pi>
op\<^sub>1 \<in> set (\<pi> ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < length \<pi>
op\<^sub>1 \<in> set (\<pi> ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
have "are_all_operators_non_interfering (\<pi> ! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. are_all_operators_non_interfering (\<pi> ! k)
[PROOF STEP]
using assms(3) calculation(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>k<length \<pi>. are_all_operators_non_interfering (\<pi> ! k)
k < length \<pi>

goal (1 subgoal):
 1. are_all_operators_non_interfering (\<pi> ! k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
are_all_operators_non_interfering (\<pi> ! k)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
are_all_operators_non_interfering (\<pi> ! k)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[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 calculation(3)
[PROOF STATE]
proof (prove)
using this:
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2

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

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k < length \<pi>
op\<^sub>1 \<in> set (\<pi> ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2
are_all_operators_non_interfering (\<pi> ! k)
op\<^sub>1 \<noteq> op\<^sub>2
[PROOF STEP]
have "op\<^sub>2 \<notin> set (\<pi> ! k)"
[PROOF STATE]
proof (prove)
using this:
k < length \<pi>
op\<^sub>1 \<in> set (\<pi> ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2
are_all_operators_non_interfering (\<pi> ! k)
op\<^sub>1 \<noteq> op\<^sub>2

goal (1 subgoal):
 1. op\<^sub>2 \<notin> set (\<pi> ! k)
[PROOF STEP]
using are_all_operators_non_interfering_set_contains_no_distinct_interfering_operator_pairs
        assms(3)
[PROOF STATE]
proof (prove)
using this:
k < length \<pi>
op\<^sub>1 \<in> set (\<pi> ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2
are_all_operators_non_interfering (\<pi> ! k)
op\<^sub>1 \<noteq> op\<^sub>2
\<lbrakk>are_all_operators_non_interfering ?ops; are_operators_interfering ?op\<^sub>1 ?op\<^sub>2; ?op\<^sub>1 \<noteq> ?op\<^sub>2\<rbrakk> \<Longrightarrow> ?op\<^sub>1 \<notin> set ?ops \<or> ?op\<^sub>2 \<notin> set ?ops
\<forall>k<length \<pi>. are_all_operators_non_interfering (\<pi> ! k)

goal (1 subgoal):
 1. op\<^sub>2 \<notin> set (\<pi> ! k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
op\<^sub>2 \<notin> set (\<pi> ! k)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?k2 < length \<pi>; ?op\<^sub>12 \<in> set (\<pi> ! ?k2); index (\<Pi>\<^sub>\<O>) ?op\<^sub>12 \<noteq> index (\<Pi>\<^sub>\<O>) ?op\<^sub>22; are_operators_interfering ?op\<^sub>12 ?op\<^sub>22\<rbrakk> \<Longrightarrow> ?op\<^sub>22 \<notin> set (\<pi> ! ?k2)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
note nb\<^sub>3 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?k2 < length \<pi>; ?op\<^sub>12 \<in> set (\<pi> ! ?k2); index (\<Pi>\<^sub>\<O>) ?op\<^sub>12 \<noteq> index (\<Pi>\<^sub>\<O>) ?op\<^sub>22; are_operators_interfering ?op\<^sub>12 ?op\<^sub>22\<rbrakk> \<Longrightarrow> ?op\<^sub>22 \<notin> set (\<pi> ! ?k2)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?k2 < length \<pi>; ?op\<^sub>12 \<in> set (\<pi> ! ?k2); index (\<Pi>\<^sub>\<O>) ?op\<^sub>12 \<noteq> index (\<Pi>\<^sub>\<O>) ?op\<^sub>22; are_operators_interfering ?op\<^sub>12 ?op\<^sub>22\<rbrakk> \<Longrightarrow> ?op\<^sub>22 \<notin> set (\<pi> ! ?k2)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
assume "C \<in> cnf ?\<Phi>\<^sub>X"
[PROOF STATE]
proof (state)
this:
C \<in> cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>))

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>))
[PROOF STEP]
have "C \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
C \<in> cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>))

goal (1 subgoal):
 1. C \<in> \<Union> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})
[PROOF STEP]
using cnf_of_encode_interfering_operator_exclusion_is[of \<Pi> "length \<pi>"]
[PROOF STATE]
proof (prove)
using this:
C \<in> cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>))
cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>)) = \<Union> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})

goal (1 subgoal):
 1. C \<in> \<Union> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
C \<in> \<Union> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> \<Union> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})
[PROOF STEP]
obtain C' where "C' \<in> ?A" and C_in: "C \<in> C'"
[PROOF STATE]
proof (prove)
using this:
C \<in> \<Union> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})

goal (1 subgoal):
 1. (\<And>C'. \<lbrakk>C' \<in> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}}); C \<in> C'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Union_iff[of C ?A]
[PROOF STATE]
proof (prove)
using this:
C \<in> \<Union> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})
(C \<in> \<Union> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})) = (\<exists>X\<in>\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}}. C \<in> X)

goal (1 subgoal):
 1. (\<And>C'. \<lbrakk>C' \<in> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}}); C \<in> C'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
C' \<in> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})
C \<in> C'

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C' \<in> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})
C \<in> C'
[PROOF STEP]
obtain op\<^sub>1 op\<^sub>2 where "(op\<^sub>1, op\<^sub>2) \<in> set (operators_of \<Pi>) \<times> set (operators_of \<Pi>)"
      and index_op\<^sub>1_is_not_index_op\<^sub>2: "index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2"
      and are_operators_interfering_op\<^sub>1_op\<^sub>2: "are_operators_interfering op\<^sub>1 op\<^sub>2"
      and C'_in: "C' \<in> {{{(Operator k (index ?ops op\<^sub>1))\<inverse>, (Operator k (index ?ops op\<^sub>2))\<inverse>}}
        | k. k \<in> {0..<length \<pi>}}"
[PROOF STATE]
proof (prove)
using this:
C' \<in> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})
C \<in> C'

goal (1 subgoal):
 1. (\<And>op\<^sub>1 op\<^sub>2. \<lbrakk>(op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>); index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2; are_operators_interfering op\<^sub>1 op\<^sub>2; C' \<in> {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<length \<pi>}}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using UN_iff[of C' ?f ?Ops]
[PROOF STATE]
proof (prove)
using this:
C' \<in> (\<Union>(op\<^sub>1, op\<^sub>2)\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> 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>}} |k. k \<in> {0..<length \<pi>}})
C \<in> C'
(C' \<in> (\<Union>x\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. case x of (op\<^sub>1, op\<^sub>2) \<Rightarrow> {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<length \<pi>}})) = (\<exists>x\<in>{(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>) \<and> index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}. C' \<in> (case x of (op\<^sub>1, op\<^sub>2) \<Rightarrow> {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<length \<pi>}}))

goal (1 subgoal):
 1. (\<And>op\<^sub>1 op\<^sub>2. \<lbrakk>(op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>); index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2; are_operators_interfering op\<^sub>1 op\<^sub>2; C' \<in> {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<length \<pi>}}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2
C' \<in> {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<length \<pi>}}

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2
C' \<in> {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<length \<pi>}}
[PROOF STEP]
obtain k where "k \<in> {0..<length \<pi>}"
      and C_is: "C = { (Operator k (index ?ops op\<^sub>1))\<inverse>, (Operator k (index ?ops op\<^sub>2))\<inverse> }"
[PROOF STATE]
proof (prove)
using this:
(op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2
C' \<in> {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<length \<pi>}}

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<in> {0..<length \<pi>}; C = {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_in C'_in
[PROOF STATE]
proof (prove)
using this:
(op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2
C' \<in> {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<length \<pi>}}
C \<in> C'
C' \<in> {{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} |k. k \<in> {0..<length \<pi>}}

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<in> {0..<length \<pi>}; C = {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<in> {0..<length \<pi>}
C = {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<in> {0..<length \<pi>}
C = {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}
[PROOF STEP]
have k_lt_length_\<pi>: "k < length \<pi>"
[PROOF STATE]
proof (prove)
using this:
k \<in> {0..<length \<pi>}
C = {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}

goal (1 subgoal):
 1. k < length \<pi>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k < length \<pi>

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
consider (A) "op\<^sub>1 \<in> set (\<pi> ! k)"
     | (B) "op\<^sub>2 \<in> set (\<pi> ! k)"
     | (C) "\<not>op\<^sub>1 \<in> set (\<pi> ! k) \<or> \<not>op\<^sub>2 \<in> set (\<pi> ! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>op\<^sub>1 \<in> set (\<pi> ! k) \<Longrightarrow> thesis; op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> thesis; op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<lbrakk>op\<^sub>1 \<in> set (\<pi> ! k) \<Longrightarrow> ?thesis; op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> ?thesis; op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
hence "clause_semantics ?\<A> C"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>op\<^sub>1 \<in> set (\<pi> ! k) \<Longrightarrow> ?thesis; op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> ?thesis; op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. op\<^sub>1 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 3. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
case A
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set (\<pi> ! k)

goal (3 subgoals):
 1. op\<^sub>1 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 3. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<in> set (\<pi> ! k)

goal (3 subgoals):
 1. op\<^sub>1 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 3. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
have "op\<^sub>2 \<notin> set (\<pi> ! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op\<^sub>2 \<notin> set (\<pi> ! k)
[PROOF STEP]
using nb\<^sub>3 k_lt_length_\<pi> calculation index_op\<^sub>1_is_not_index_op\<^sub>2 are_operators_interfering_op\<^sub>1_op\<^sub>2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k2 < length \<pi>; ?op\<^sub>12 \<in> set (\<pi> ! ?k2); index (\<Pi>\<^sub>\<O>) ?op\<^sub>12 \<noteq> index (\<Pi>\<^sub>\<O>) ?op\<^sub>22; are_operators_interfering ?op\<^sub>12 ?op\<^sub>22\<rbrakk> \<Longrightarrow> ?op\<^sub>22 \<notin> set (\<pi> ! ?k2)
k < length \<pi>
op\<^sub>1 \<in> set (\<pi> ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2

goal (1 subgoal):
 1. op\<^sub>2 \<notin> set (\<pi> ! k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
op\<^sub>2 \<notin> set (\<pi> ! k)

goal (3 subgoals):
 1. op\<^sub>1 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 3. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
op\<^sub>2 \<notin> set (\<pi> ! k)

goal (3 subgoals):
 1. op\<^sub>1 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 3. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
have "\<not>?\<A> (Operator k (index ?ops op\<^sub>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))
[PROOF STEP]
using encode_problem_parallel_complete_vi_d[OF assms(2) k_lt_length_\<pi>]
            calculation(2)
[PROOF STATE]
proof (prove)
using this:
?op \<notin> set (\<pi> ! k) \<Longrightarrow> \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) ?op))
op\<^sub>2 \<notin> set (\<pi> ! k)

goal (1 subgoal):
 1. \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))

goal (3 subgoals):
 1. op\<^sub>1 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 3. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
op\<^sub>1 \<in> set (\<pi> ! k)
op\<^sub>2 \<notin> set (\<pi> ! k)
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
op\<^sub>1 \<in> set (\<pi> ! k)
op\<^sub>2 \<notin> set (\<pi> ! k)
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))

goal (1 subgoal):
 1. clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
using C_is
[PROOF STATE]
proof (prove)
using this:
op\<^sub>1 \<in> set (\<pi> ! k)
op\<^sub>2 \<notin> set (\<pi> ! k)
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))
C = {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}

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

goal (1 subgoal):
 1. \<exists>L\<in>C. lit_semantics (valuation_for_plan \<Pi> \<pi>) L
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
clause_semantics (valuation_for_plan \<Pi> \<pi>) C

goal (2 subgoals):
 1. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
case B
[PROOF STATE]
proof (state)
this:
op\<^sub>2 \<in> set (\<pi> ! k)

goal (2 subgoals):
 1. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
op\<^sub>2 \<in> set (\<pi> ! k)

goal (2 subgoals):
 1. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
have "op\<^sub>1 \<notin> set (\<pi> ! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op\<^sub>1 \<notin> set (\<pi> ! k)
[PROOF STEP]
using nb\<^sub>3 k_lt_length_\<pi> calculation index_op\<^sub>1_is_not_index_op\<^sub>2 are_operators_interfering_op\<^sub>1_op\<^sub>2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k2 < length \<pi>; ?op\<^sub>12 \<in> set (\<pi> ! ?k2); index (\<Pi>\<^sub>\<O>) ?op\<^sub>12 \<noteq> index (\<Pi>\<^sub>\<O>) ?op\<^sub>22; are_operators_interfering ?op\<^sub>12 ?op\<^sub>22\<rbrakk> \<Longrightarrow> ?op\<^sub>22 \<notin> set (\<pi> ! ?k2)
k < length \<pi>
op\<^sub>2 \<in> set (\<pi> ! k)
index (\<Pi>\<^sub>\<O>) op\<^sub>1 \<noteq> index (\<Pi>\<^sub>\<O>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2

goal (1 subgoal):
 1. op\<^sub>1 \<notin> set (\<pi> ! k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<notin> set (\<pi> ! k)

goal (2 subgoals):
 1. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<notin> set (\<pi> ! k)

goal (2 subgoals):
 1. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
have "\<not>?\<A> (Operator k (index ?ops op\<^sub>1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
[PROOF STEP]
using encode_problem_parallel_complete_vi_d[OF assms(2) k_lt_length_\<pi>]
            calculation(2)
[PROOF STATE]
proof (prove)
using this:
?op \<notin> set (\<pi> ! k) \<Longrightarrow> \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) ?op))
op\<^sub>1 \<notin> set (\<pi> ! k)

goal (1 subgoal):
 1. \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))

goal (2 subgoals):
 1. op\<^sub>2 \<in> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
op\<^sub>2 \<in> set (\<pi> ! k)
op\<^sub>1 \<notin> set (\<pi> ! k)
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
op\<^sub>2 \<in> set (\<pi> ! k)
op\<^sub>1 \<notin> set (\<pi> ! k)
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))

goal (1 subgoal):
 1. clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
using C_is
[PROOF STATE]
proof (prove)
using this:
op\<^sub>2 \<in> set (\<pi> ! k)
op\<^sub>1 \<notin> set (\<pi> ! k)
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
C = {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}

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

goal (1 subgoal):
 1. \<exists>L\<in>C. lit_semantics (valuation_for_plan \<Pi> \<pi>) L
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
clause_semantics (valuation_for_plan \<Pi> \<pi>) C

goal (1 subgoal):
 1. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
case C
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k)

goal (1 subgoal):
 1. op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
op\<^sub>1 \<notin> set (\<pi> ! k) \<or> op\<^sub>2 \<notin> set (\<pi> ! k)

goal (1 subgoal):
 1. clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
proof (rule disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op\<^sub>1 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
assume "op\<^sub>1 \<notin> set (\<pi> ! k)"
[PROOF STATE]
proof (state)
this:
op\<^sub>1 \<notin> set (\<pi> ! k)

goal (2 subgoals):
 1. op\<^sub>1 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
op\<^sub>1 \<notin> set (\<pi> ! k)
[PROOF STEP]
have "\<not>?\<A> (Operator k (index ?ops op\<^sub>1))"
[PROOF STATE]
proof (prove)
using this:
op\<^sub>1 \<notin> set (\<pi> ! k)

goal (1 subgoal):
 1. \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
[PROOF STEP]
using encode_problem_parallel_complete_vi_d[OF assms(2) k_lt_length_\<pi>]
[PROOF STATE]
proof (prove)
using this:
op\<^sub>1 \<notin> set (\<pi> ! k)
?op \<notin> set (\<pi> ! k) \<Longrightarrow> \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) ?op))

goal (1 subgoal):
 1. \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))

goal (2 subgoals):
 1. op\<^sub>1 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
 2. op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
thus "clause_semantics (valuation_for_plan \<Pi> \<pi>) C"
[PROOF STATE]
proof (prove)
using this:
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))

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

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

goal (1 subgoal):
 1. \<exists>L\<in>C. lit_semantics (valuation_for_plan \<Pi> \<pi>) L
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
clause_semantics (valuation_for_plan \<Pi> \<pi>) C

goal (1 subgoal):
 1. op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
assume "op\<^sub>2 \<notin> set (\<pi> ! k)"
[PROOF STATE]
proof (state)
this:
op\<^sub>2 \<notin> set (\<pi> ! k)

goal (1 subgoal):
 1. op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
op\<^sub>2 \<notin> set (\<pi> ! k)
[PROOF STEP]
have "\<not>?\<A> (Operator k (index ?ops op\<^sub>2))"
[PROOF STATE]
proof (prove)
using this:
op\<^sub>2 \<notin> set (\<pi> ! k)

goal (1 subgoal):
 1. \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))
[PROOF STEP]
using encode_problem_parallel_complete_vi_d[OF assms(2) k_lt_length_\<pi>]
[PROOF STATE]
proof (prove)
using this:
op\<^sub>2 \<notin> set (\<pi> ! k)
?op \<notin> set (\<pi> ! k) \<Longrightarrow> \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) ?op))

goal (1 subgoal):
 1. \<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))

goal (1 subgoal):
 1. op\<^sub>2 \<notin> set (\<pi> ! k) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
thus "clause_semantics (valuation_for_plan \<Pi> \<pi>) C"
[PROOF STATE]
proof (prove)
using this:
\<not> valuation_for_plan \<Pi> \<pi> (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))

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

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

goal (1 subgoal):
 1. \<exists>L\<in>C. lit_semantics (valuation_for_plan \<Pi> \<pi>) L
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
clause_semantics (valuation_for_plan \<Pi> \<pi>) C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
clause_semantics (valuation_for_plan \<Pi> \<pi>) C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
clause_semantics (valuation_for_plan \<Pi> \<pi>) C

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?C2 \<in> cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>)) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) ?C2

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?C2 \<in> cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>)) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) ?C2
[PROOF STEP]
have "cnf_semantics ?\<A> (cnf ?\<Phi>\<^sub>X)"
[PROOF STATE]
proof (prove)
using this:
?C2 \<in> cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>)) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) ?C2

goal (1 subgoal):
 1. cnf_semantics (valuation_for_plan \<Pi> \<pi>) (cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>)))
[PROOF STEP]
unfolding cnf_semantics_def
[PROOF STATE]
proof (prove)
using this:
?C2 \<in> cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>)) \<Longrightarrow> clause_semantics (valuation_for_plan \<Pi> \<pi>) ?C2

goal (1 subgoal):
 1. \<forall>C\<in>cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>)). clause_semantics (valuation_for_plan \<Pi> \<pi>) C
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
cnf_semantics (valuation_for_plan \<Pi> \<pi>) (cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>)))

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cnf_semantics (valuation_for_plan \<Pi> \<pi>) (cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>)))

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
using cnf_semantics[OF is_nnf_cnf[OF is_cnf_encode_interfering_operator_exclusion]]
[PROOF STATE]
proof (prove)
using this:
cnf_semantics (valuation_for_plan \<Pi> \<pi>) (cnf (encode_interfering_operator_exclusion \<Pi> (length \<pi>)))
cnf_semantics ?\<A> (cnf (encode_interfering_operator_exclusion ?\<Pi>2 ?t2)) = ?\<A> \<Turnstile> encode_interfering_operator_exclusion ?\<Pi>2 ?t2

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem encode_problem_serializable_complete:
  assumes "is_valid_problem_strips \<Pi>"
    and "is_parallel_solution_for_problem \<Pi> \<pi>"
    and "\<forall>k < length \<pi>. are_all_operators_non_interfering (\<pi> ! k)"
  shows "valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> (length \<pi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> length \<pi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> length \<pi>
[PROOF STEP]
let ?\<A> = "valuation_for_plan \<Pi> \<pi>"
    and ?\<Phi>\<^sub>X = "encode_interfering_operator_exclusion \<Pi> (length \<pi>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> length \<pi>
[PROOF STEP]
have "?\<A> \<Turnstile> SAT_Plan_Base.encode_problem \<Pi> (length \<pi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi> \<Pi> length \<pi>
[PROOF STEP]
using assms(1, 2) encode_problem_parallel_complete
[PROOF STATE]
proof (prove)
using this:
is_valid_problem_strips \<Pi>
is_parallel_solution_for_problem \<Pi> \<pi>
\<lbrakk>is_valid_problem_strips ?\<Pi>; is_parallel_solution_for_problem ?\<Pi> ?\<pi>\<rbrakk> \<Longrightarrow> valuation_for_plan ?\<Pi> ?\<pi> \<Turnstile> \<Phi> ?\<Pi> length ?\<pi>

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi> \<Pi> length \<pi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi> \<Pi> length \<pi>

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> length \<pi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi> \<Pi> length \<pi>

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> length \<pi>
[PROOF STEP]
have "?\<A> \<Turnstile> ?\<Phi>\<^sub>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
using encode_problem_with_operator_interference_exclusion_complete_i[OF assms]
[PROOF STATE]
proof (prove)
using this:
valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> length \<pi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi> \<Pi> length \<pi>
valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi> \<Pi> length \<pi>
valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> length \<pi>
[PROOF STEP]
unfolding encode_problem_with_operator_interference_exclusion_def encode_problem_def
      SAT_Plan_Base.encode_problem_def
[PROOF STATE]
proof (prove)
using this:
valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi>\<^sub>I \<Pi> \<^bold>\<and> (encode_operators \<Pi> (length \<pi>) \<^bold>\<and> (encode_all_frame_axioms \<Pi> (length \<pi>) \<^bold>\<and> (\<Phi>\<^sub>G \<Pi>) (length \<pi>)))
valuation_for_plan \<Pi> \<pi> \<Turnstile> encode_interfering_operator_exclusion \<Pi> (length \<pi>)

goal (1 subgoal):
 1. valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi>\<^sub>I \<Pi> \<^bold>\<and> (encode_operators \<Pi> (length \<pi>) \<^bold>\<and> (encode_all_frame_axioms \<Pi> (length \<pi>) \<^bold>\<and> (encode_interfering_operator_exclusion \<Pi> (length \<pi>) \<^bold>\<and> (\<Phi>\<^sub>G \<Pi>) (length \<pi>))))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
valuation_for_plan \<Pi> \<pi> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> length \<pi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma encode_problem_forall_step_decoded_plan_is_serializable_i:
  assumes "is_valid_problem_strips \<Pi>"
    and "\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t"
  shows "(\<Pi>)\<^sub>G \<subseteq>\<^sub>m execute_serial_plan ((\<Pi>)\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
let ?G = "(\<Pi>)\<^sub>G"
    and ?I = "(\<Pi>)\<^sub>I"
    and ?\<pi> = "\<Phi>\<inverse> \<Pi> \<A> t"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
let ?\<pi>' = "concat (\<Phi>\<inverse> \<Pi> \<A> t)"
    and ?\<tau> = "trace_parallel_plan_strips ?I ?\<pi>"
    and ?\<sigma> = "map (decode_state_at \<Pi> \<A>) [0..<Suc (length ?\<pi>)]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
assume k_lt_length_\<pi>: "k < length ?\<pi>"
[PROOF STATE]
proof (state)
this:
k < length (\<Phi>\<inverse> \<Pi> \<A> t)

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < length (\<Phi>\<inverse> \<Pi> \<A> t)

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
have "\<A> \<Turnstile> SAT_Plan_Base.encode_problem \<Pi> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<A> \<Turnstile> \<Phi> \<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> \<Pi> t
[PROOF STEP]
unfolding encode_problem_with_operator_interference_exclusion_def
        encode_problem_def SAT_Plan_Base.encode_problem_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> \<^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 (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<A> \<Turnstile> \<Phi> \<Pi> t

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
have "length ?\<sigma> = length ?\<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (decode_state_at \<Pi> \<A>) [0..<Suc (length (\<Phi>\<inverse> \<Pi> \<A> t))]) = length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
using encode_problem_parallel_correct_vii assms(1) calculation
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_valid_problem_strips ?\<Pi>; ?\<A> \<Turnstile> \<Phi> ?\<Pi> ?t\<rbrakk> \<Longrightarrow> length (map (decode_state_at ?\<Pi> ?\<A>) [0..<Suc (length (\<Phi>\<inverse> ?\<Pi> ?\<A> ?t))]) = length (trace_parallel_plan_strips (?\<Pi>\<^sub>I) (\<Phi>\<inverse> ?\<Pi> ?\<A> ?t))
is_valid_problem_strips \<Pi>
k < length (\<Phi>\<inverse> \<Pi> \<A> t)
\<A> \<Turnstile> \<Phi> \<Pi> t

goal (1 subgoal):
 1. length (map (decode_state_at \<Pi> \<A>) [0..<Suc (length (\<Phi>\<inverse> \<Pi> \<A> t))]) = length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
unfolding decode_state_at_def decode_plan_def initial_of_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_valid_problem_strips ?\<Pi>; ?\<A> \<Turnstile> \<Phi> ?\<Pi> ?t\<rbrakk> \<Longrightarrow> length (map (\<lambda>k. let vs = ?\<Pi>\<^sub>\<V>; state_encoding_to_assignment = \<lambda>v. (v, ?\<A> (State k (index vs v))) in map_of (map state_encoding_to_assignment vs)) [0..<Suc (length (map (decode_plan' ?\<Pi> ?\<A>) [0..<?t]))]) = length (trace_parallel_plan_strips ((id \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) ?\<Pi>) (map (decode_plan' ?\<Pi> ?\<A>) [0..<?t]))
is_valid_problem_strips \<Pi>
k < length (map (decode_plan' \<Pi> \<A>) [0..<t])
\<A> \<Turnstile> \<Phi> \<Pi> t

goal (1 subgoal):
 1. length (map (\<lambda>k. let vs = \<Pi>\<^sub>\<V>; state_encoding_to_assignment = \<lambda>v. (v, \<A> (State k (index vs v))) in map_of (map state_encoding_to_assignment vs)) [0..<Suc (length (map (decode_plan' \<Pi> \<A>) [0..<t]))]) = length (trace_parallel_plan_strips ((id \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) (map (decode_plan' \<Pi> \<A>) [0..<t]))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
length (map (decode_state_at \<Pi> \<A>) [0..<Suc (length (\<Phi>\<inverse> \<Pi> \<A> t))]) = length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k < length (\<Phi>\<inverse> \<Pi> \<A> t)
\<A> \<Turnstile> \<Phi> \<Pi> t
length (map (decode_state_at \<Pi> \<A>) [0..<Suc (length (\<Phi>\<inverse> \<Pi> \<A> t))]) = length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
have "k < length ?\<tau> - 1" and "k < t"
[PROOF STATE]
proof (prove)
using this:
k < length (\<Phi>\<inverse> \<Pi> \<A> t)
\<A> \<Turnstile> \<Phi> \<Pi> t
length (map (decode_state_at \<Pi> \<A>) [0..<Suc (length (\<Phi>\<inverse> \<Pi> \<A> t))]) = length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))

goal (1 subgoal):
 1. k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1 &&& k < t
[PROOF STEP]
unfolding decode_plan_def SAT_Plan_Base.decode_plan_def
[PROOF STATE]
proof (prove)
using this:
k < length (map (decode_plan' \<Pi> \<A>) [0..<t])
\<A> \<Turnstile> \<Phi> \<Pi> t
length (map (decode_state_at \<Pi> \<A>) [0..<Suc (length (map (decode_plan' \<Pi> \<A>) [0..<t]))]) = length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (map (decode_plan' \<Pi> \<A>) [0..<t]))

goal (1 subgoal):
 1. k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (map (decode_plan' \<Pi> \<A>) [0..<t])) - 1 &&& k < t
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1
k < t

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> ?k2 < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> ?k2 < t

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
note nb = this
[PROOF STATE]
proof (state)
this:
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> ?k2 < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> ?k2 < t

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> ?k2 < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> ?k2 < t

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
have "?G \<subseteq>\<^sub>m execute_parallel_plan ?I ?\<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_parallel_plan (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)
[PROOF STEP]
using encode_problem_serializable_sound assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_valid_problem_strips ?\<Pi>; ?\<A> \<Turnstile> \<Phi>\<^sub>\<forall> ?\<Pi> ?t\<rbrakk> \<Longrightarrow> is_parallel_solution_for_problem ?\<Pi> (\<Phi>\<inverse> ?\<Pi> ?\<A> ?t)
\<lbrakk>is_valid_problem_strips ?\<Pi>; ?\<A> \<Turnstile> \<Phi>\<^sub>\<forall> ?\<Pi> ?t\<rbrakk> \<Longrightarrow> \<forall>k<length (\<Phi>\<inverse> ?\<Pi> ?\<A> ?t). are_all_operators_non_interfering ((\<Phi>\<inverse> ?\<Pi> ?\<A> ?t) ! k)
is_valid_problem_strips \<Pi>
\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_parallel_plan (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)
[PROOF STEP]
unfolding is_parallel_solution_for_problem_def decode_plan_def
        goal_of_def initial_of_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_valid_problem_strips ?\<Pi>; ?\<A> \<Turnstile> \<Phi>\<^sub>\<forall> ?\<Pi> ?t\<rbrakk> \<Longrightarrow> (id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) ?\<Pi> \<subseteq>\<^sub>m execute_parallel_plan ((id \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) ?\<Pi>) (map (decode_plan' ?\<Pi> ?\<A>) [0..<?t]) \<and> list_all (list_all (\<lambda>op. ListMem op (?\<Pi>\<^sub>\<O>))) (map (decode_plan' ?\<Pi> ?\<A>) [0..<?t])
\<lbrakk>is_valid_problem_strips ?\<Pi>; ?\<A> \<Turnstile> \<Phi>\<^sub>\<forall> ?\<Pi> ?t\<rbrakk> \<Longrightarrow> \<forall>k<length (map (decode_plan' ?\<Pi> ?\<A>) [0..<?t]). are_all_operators_non_interfering (map (decode_plan' ?\<Pi> ?\<A>) [0..<?t] ! k)
is_valid_problem_strips \<Pi>
\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t

goal (1 subgoal):
 1. (id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi> \<subseteq>\<^sub>m execute_parallel_plan ((id \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) (map (decode_plan' \<Pi> \<A>) [0..<t])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m execute_parallel_plan (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
hence "?G \<subseteq>\<^sub>m last (trace_parallel_plan_strips ?I ?\<pi>)"
[PROOF STATE]
proof (prove)
using this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m execute_parallel_plan (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m last (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
using execute_parallel_plan_reaches_goal_iff_goal_is_last_element_of_trace
[PROOF STATE]
proof (prove)
using this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m execute_parallel_plan (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)
(?G \<subseteq>\<^sub>m execute_parallel_plan ?I ?\<pi>) = (?G \<subseteq>\<^sub>m last (trace_parallel_plan_strips ?I ?\<pi>))

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m last (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m last (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m last (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m last (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m last (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
assume k_lt_length_\<pi>: "k < length ?\<pi>"
[PROOF STATE]
proof (state)
this:
k < length (\<Phi>\<inverse> \<Pi> \<A> t)

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < length (\<Phi>\<inverse> \<Pi> \<A> t)

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
have "k < length ?\<tau> - 1" and "k < t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1 &&& k < t
[PROOF STEP]
using nb calculation
[PROOF STATE]
proof (prove)
using this:
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> ?k2 < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> ?k2 < t
k < length (\<Phi>\<inverse> \<Pi> \<A> t)

goal (1 subgoal):
 1. k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1 &&& k < t
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1
k < t

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1
k < t

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
have "are_all_operators_applicable (?\<tau> ! k) (?\<pi> ! k)"
      and "are_all_operator_effects_consistent (?\<pi> ! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! k) ((\<Phi>\<inverse> \<Pi> \<A> t) ! k) &&& are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
using trace_parallel_plan_strips_operator_preconditions calculation(2)
[PROOF STATE]
proof (prove)
using this:
?k < length (trace_parallel_plan_strips ?I ?\<pi>) - 1 \<Longrightarrow> are_all_operators_applicable (trace_parallel_plan_strips ?I ?\<pi> ! ?k) (?\<pi> ! ?k) \<and> are_all_operator_effects_consistent (?\<pi> ! ?k)
k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1

goal (1 subgoal):
 1. are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! k) ((\<Phi>\<inverse> \<Pi> \<A> t) ! k) &&& are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! k) ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! k) ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
have "are_all_operators_non_interfering (?\<pi> ! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
using encode_problem_serializable_sound(2)[OF assms(1, 2)] k_lt_length_\<pi>
[PROOF STATE]
proof (prove)
using this:
\<forall>k<length (\<Phi>\<inverse> \<Pi> \<A> t). are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
k < length (\<Phi>\<inverse> \<Pi> \<A> t)

goal (1 subgoal):
 1. are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> 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. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k < length (\<Phi>\<inverse> \<Pi> \<A> t)
k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1
k < t
are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! k) ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
have "are_all_operators_applicable (?\<tau> ! k) (?\<pi> ! k)"
      and "are_all_operator_effects_consistent (?\<pi> ! k)"
      and "are_all_operators_non_interfering (?\<pi> ! k)"
[PROOF STATE]
proof (prove)
using this:
k < length (\<Phi>\<inverse> \<Pi> \<A> t)
k < length (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t)) - 1
k < t
are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! k) ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)

goal (1 subgoal):
 1. are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! k) ((\<Phi>\<inverse> \<Pi> \<A> t) ! k) &&& are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! k) &&& are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! k) ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2) ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m last (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2) ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m last (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2) ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
using execute_parallel_plan_is_execute_sequential_plan_if assms(1)
[PROOF STATE]
proof (prove)
using this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m last (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t))
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operators_applicable (trace_parallel_plan_strips (\<Pi>\<^sub>I) (\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2) ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operator_effects_consistent ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
?k2 < length (\<Phi>\<inverse> \<Pi> \<A> t) \<Longrightarrow> are_all_operators_non_interfering ((\<Phi>\<inverse> \<Pi> \<A> t) ! ?k2)
\<lbrakk>?is_valid_problem ?\<Pi>; ?G \<subseteq>\<^sub>m last (trace_parallel_plan_strips ?I ?\<pi>); \<forall>k<length ?\<pi>. are_all_operators_applicable (trace_parallel_plan_strips ?I ?\<pi> ! k) (?\<pi> ! k) \<and> are_all_operator_effects_consistent (?\<pi> ! k) \<and> are_all_operators_non_interfering (?\<pi> ! k)\<rbrakk> \<Longrightarrow> ?G \<subseteq>\<^sub>m execute_serial_plan ?I (concat ?\<pi>)
is_valid_problem_strips \<Pi>

goal (1 subgoal):
 1. \<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma encode_problem_forall_step_decoded_plan_is_serializable_ii:
  (* TODO why is the fixed type necessary? *)
  fixes \<Pi> :: "'variable strips_problem"
  shows "list_all (\<lambda>op. ListMem op (strips_problem.operators_of \<Pi>))
    (concat (\<Phi>\<inverse> \<Pi> \<A> t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
let ?\<pi> = "\<Phi>\<inverse> \<Pi> \<A> t"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
let ?\<pi>' = "concat ?\<pi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
(* TODO refactor *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
have "set ?\<pi>' = \<Union>(set `  (\<Union>k < t. { decode_plan' \<Pi> \<A> k }))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) = \<Union> (set ` (\<Union>k<t. {decode_plan' \<Pi> \<A> k}))
[PROOF STEP]
unfolding decode_plan_def decode_plan_set_is set_concat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (set ` set (map (decode_plan' \<Pi> \<A>) [0..<t])) = \<Union> (set ` (\<Union>k<t. {decode_plan' \<Pi> \<A> k}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) = \<Union> (set ` (\<Union>k<t. {decode_plan' \<Pi> \<A> k}))

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) = \<Union> (set ` (\<Union>k<t. {decode_plan' \<Pi> \<A> k}))

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
have "\<dots> = \<Union>(\<Union>k < t. { set (decode_plan' \<Pi> \<A> k) })"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (set ` (\<Union>k<t. {decode_plan' \<Pi> \<A> k})) = \<Union> (\<Union>k<t. {set (decode_plan' \<Pi> \<A> k)})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Union> (set ` (\<Union>k<t. {decode_plan' \<Pi> \<A> k})) = \<Union> (\<Union>k<t. {set (decode_plan' \<Pi> \<A> k)})

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) = \<Union> (\<Union>k<t. {set (decode_plan' \<Pi> \<A> k)})
[PROOF STEP]
have "set ?\<pi>' = (\<Union>k < t. set (decode_plan' \<Pi> \<A> k))"
[PROOF STATE]
proof (prove)
using this:
set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) = \<Union> (\<Union>k<t. {set (decode_plan' \<Pi> \<A> k)})

goal (1 subgoal):
 1. set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) = (\<Union>k<t. set (decode_plan' \<Pi> \<A> k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) = (\<Union>k<t. set (decode_plan' \<Pi> \<A> k))

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) = (\<Union>k<t. set (decode_plan' \<Pi> \<A> k))

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
note nb = this
[PROOF STATE]
proof (state)
this:
set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) = (\<Union>k<t. set (decode_plan' \<Pi> \<A> k))

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) = (\<Union>k<t. set (decode_plan' \<Pi> \<A> k))

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
fix op
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
assume "op \<in> set ?\<pi>'"
[PROOF STATE]
proof (state)
this:
op \<in> set (concat (\<Phi>\<inverse> \<Pi> \<A> t))

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
op \<in> set (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
obtain k where "k < t" and "op \<in> set (decode_plan' \<Pi> \<A> k)"
[PROOF STATE]
proof (prove)
using this:
op \<in> set (concat (\<Phi>\<inverse> \<Pi> \<A> t))

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < t; op \<in> set (decode_plan' \<Pi> \<A> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nb
[PROOF STATE]
proof (prove)
using this:
op \<in> set (concat (\<Phi>\<inverse> \<Pi> \<A> t))
set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) = (\<Union>k<t. set (decode_plan' \<Pi> \<A> k))

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < t; op \<in> set (decode_plan' \<Pi> \<A> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k < t
op \<in> set (decode_plan' \<Pi> \<A> k)

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < t
op \<in> set (decode_plan' \<Pi> \<A> k)

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
have "op \<in> set (decode_plan \<Pi> \<A> t ! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
k < t
op \<in> set (decode_plan' \<Pi> \<A> k)

goal (1 subgoal):
 1. op \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
unfolding decode_plan_def SAT_Plan_Base.decode_plan_def
[PROOF STATE]
proof (prove)
using this:
k < t
op \<in> set (decode_plan' \<Pi> \<A> k)

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

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k < t
op \<in> set (decode_plan' \<Pi> \<A> k)
op \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
[PROOF STEP]
have "op \<in> set (operators_of \<Pi>)"
[PROOF STATE]
proof (prove)
using this:
k < t
op \<in> set (decode_plan' \<Pi> \<A> k)
op \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)

goal (1 subgoal):
 1. op \<in> set (\<Pi>\<^sub>\<O>)
[PROOF STEP]
using decode_plan_step_element_then(1)
[PROOF STATE]
proof (prove)
using this:
k < t
op \<in> set (decode_plan' \<Pi> \<A> k)
op \<in> set ((\<Phi>\<inverse> \<Pi> \<A> t) ! k)
\<lbrakk>?k < ?t; ?op \<in> set ((\<Phi>\<inverse> ?\<Pi> ?\<A> ?t) ! ?k)\<rbrakk> \<Longrightarrow> ?op \<in> set (?\<Pi>\<^sub>\<O>)

goal (1 subgoal):
 1. op \<in> set (\<Pi>\<^sub>\<O>)
[PROOF STEP]
unfolding operators_of_def decode_plan_def
[PROOF STATE]
proof (prove)
using this:
k < t
op \<in> set (decode_plan' \<Pi> \<A> k)
op \<in> set (map (decode_plan' \<Pi> \<A>) [0..<t] ! k)
\<lbrakk>?k < ?t; ?op \<in> set (map (decode_plan' ?\<Pi> ?\<A>) [0..<?t] ! ?k)\<rbrakk> \<Longrightarrow> ?op \<in> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) ?\<Pi>)

goal (1 subgoal):
 1. op \<in> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
op \<in> set (\<Pi>\<^sub>\<O>)

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?op2 \<in> set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) \<Longrightarrow> ?op2 \<in> set (\<Pi>\<^sub>\<O>)

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?op2 \<in> set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) \<Longrightarrow> ?op2 \<in> set (\<Pi>\<^sub>\<O>)

goal (1 subgoal):
 1. list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
unfolding list_all_iff ListMem_iff operators_of_def
[PROOF STATE]
proof (prove)
using this:
?op2 \<in> set (concat (\<Phi>\<inverse> \<Pi> \<A> t)) \<Longrightarrow> ?op2 \<in> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>)

goal (1 subgoal):
 1. \<forall>op\<in>set (concat (\<Phi>\<inverse> \<Pi> \<A> t)). op \<in> set ((id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> \<Pi> \<A> t))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem serializable_encoding_decoded_plan_is_serializable:
  assumes "is_valid_problem_strips \<Pi>"
    and "\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t"
  shows "is_serial_solution_for_problem \<Pi> (concat (\<Phi>\<inverse> \<Pi> \<A> t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_serial_solution_for_problem \<Pi> (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
using encode_problem_forall_step_decoded_plan_is_serializable_i[OF assms]
    encode_problem_forall_step_decoded_plan_is_serializable_ii
[PROOF STATE]
proof (prove)
using this:
\<Pi>\<^sub>G \<subseteq>\<^sub>m execute_serial_plan (\<Pi>\<^sub>I) (concat (\<Phi>\<inverse> \<Pi> \<A> t))
list_all (\<lambda>op. ListMem op (?\<Pi>\<^sub>\<O>)) (concat (\<Phi>\<inverse> ?\<Pi> ?\<A> ?t))

goal (1 subgoal):
 1. is_serial_solution_for_problem \<Pi> (concat (\<Phi>\<inverse> \<Pi> \<A> t))
[PROOF STEP]
unfolding is_serial_solution_for_problem_def goal_of_def
    initial_of_def decode_plan_def
[PROOF STATE]
proof (prove)
using this:
(id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi> \<subseteq>\<^sub>m execute_serial_plan ((id \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) (concat (map (decode_plan' \<Pi> \<A>) [0..<t]))
list_all (\<lambda>op. ListMem op (?\<Pi>\<^sub>\<O>)) (concat (map (decode_plan' ?\<Pi> ?\<A>) [0..<?t]))

goal (1 subgoal):
 1. (id \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi> \<subseteq>\<^sub>m execute_serial_plan ((id \<circ> Record.iso_tuple_fst Record.tuple_iso_tuple \<circ> Record.iso_tuple_snd Record.tuple_iso_tuple \<circ> Record.iso_tuple_fst strips_problem_ext_Tuple_Iso) \<Pi>) (concat (map (decode_plan' \<Pi> \<A>) [0..<t])) \<and> list_all (\<lambda>op. ListMem op (\<Pi>\<^sub>\<O>)) (concat (map (decode_plan' \<Pi> \<A>) [0..<t]))
[PROOF STEP]
by blast


[STATEMENT]
lemma (in Congruence_Rule) Seg_Bet_add :
  assumes
    "Bet_Point (Se p11 p13) p12"
    "Bet_Point (Se p21 p23) p22"
    "Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)"
    "Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)"
  shows "Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p23) p22
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)
[PROOF STEP]
have "\<exists>l. Line_on l p11 \<and> Line_on l p13 \<and> Line_on l p12"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p23) p22
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)

goal (1 subgoal):
 1. \<exists>l. Line_on l p11 \<and> Line_on l p13 \<and> Line_on l p12
[PROOF STEP]
by (simp add:Line_Bet_exist)
[PROOF STATE]
proof (state)
this:
\<exists>l. Line_on l p11 \<and> Line_on l p13 \<and> Line_on l p12

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. Line_on l p11 \<and> Line_on l p13 \<and> Line_on l p12
[PROOF STEP]
obtain l1 :: Line where P1 : "Line_on l1 p11 \<and> Line_on l1 p13 \<and> Line_on l1 p12"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. Line_on l p11 \<and> Line_on l p13 \<and> Line_on l p12

goal (1 subgoal):
 1. (\<And>l1. Line_on l1 p11 \<and> Line_on l1 p13 \<and> Line_on l1 p12 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Line_on l1 p11 \<and> Line_on l1 p13 \<and> Line_on l1 p12

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p23) p22
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)
[PROOF STEP]
have "\<exists>l. Line_on l p21 \<and> Line_on l p23 \<and> Line_on l p22"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p23) p22
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)

goal (1 subgoal):
 1. \<exists>l. Line_on l p21 \<and> Line_on l p23 \<and> Line_on l p22
[PROOF STEP]
by (simp add:Line_Bet_exist)
[PROOF STATE]
proof (state)
this:
\<exists>l. Line_on l p21 \<and> Line_on l p23 \<and> Line_on l p22

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. Line_on l p21 \<and> Line_on l p23 \<and> Line_on l p22
[PROOF STEP]
obtain l2 :: Line where P2 : "Line_on l2 p21 \<and> Line_on l2 p23 \<and> Line_on l2 p22"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. Line_on l p21 \<and> Line_on l p23 \<and> Line_on l p22

goal (1 subgoal):
 1. (\<And>l2. Line_on l2 p21 \<and> Line_on l2 p23 \<and> Line_on l2 p22 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Line_on l2 p21 \<and> Line_on l2 p23 \<and> Line_on l2 p22

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p23) p22
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)
[PROOF STEP]
have P3 : "\<not> Seg_on_Seg (Se p11 p12) (Se p12 p13)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p23) p22
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)

goal (1 subgoal):
 1. \<not> Seg_on_Seg (Se p11 p12) (Se p12 p13)
[PROOF STEP]
by (simp add:Seg_Bet_not_on)
[PROOF STATE]
proof (state)
this:
\<not> Seg_on_Seg (Se p11 p12) (Se p12 p13)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p23) p22
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)
[PROOF STEP]
have P4 : "\<not> Seg_on_Seg (Se p21 p22) (Se p22 p23)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p23) p22
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)

goal (1 subgoal):
 1. \<not> Seg_on_Seg (Se p21 p22) (Se p22 p23)
[PROOF STEP]
by (simp add:Seg_Bet_not_on)
[PROOF STATE]
proof (state)
this:
\<not> Seg_on_Seg (Se p21 p22) (Se p22 p23)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
from assms P1 P2 P3 P4
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p23) p22
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)
Line_on l1 p11 \<and> Line_on l1 p13 \<and> Line_on l1 p12
Line_on l2 p21 \<and> Line_on l2 p23 \<and> Line_on l2 p22
\<not> Seg_on_Seg (Se p11 p12) (Se p12 p13)
\<not> Seg_on_Seg (Se p21 p22) (Se p22 p23)
[PROOF STEP]
show "Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p23) p22
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p12 p13)) add Emp) (Geos (Seg (Se p22 p23)) add Emp)
Line_on l1 p11 \<and> Line_on l1 p13 \<and> Line_on l1 p12
Line_on l2 p21 \<and> Line_on l2 p23 \<and> Line_on l2 p22
\<not> Seg_on_Seg (Se p11 p12) (Se p12 p13)
\<not> Seg_on_Seg (Se p21 p22) (Se p22 p23)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
by (blast intro:Seg_add)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed