[STATEMENT]
lemma cnf_of_encode_interfering_operator_exclusion_is:
  "cnf (encode_interfering_operator_exclusion \<Pi> t) = \<Union>(\<Union>(op\<^sub>1, op\<^sub>2)
      \<in> { (op\<^sub>1, op\<^sub>2) \<in> set (operators_of \<Pi>) \<times> set (operators_of \<Pi>).
        index (strips_problem.operators_of \<Pi>) op\<^sub>1 \<noteq> index (strips_problem.operators_of \<Pi>) op\<^sub>2
          \<and> are_operators_interfering op\<^sub>1 op\<^sub>2 }.
    {{{ (Operator k (index (strips_problem.operators_of \<Pi>) op\<^sub>1))\<inverse>
      , (Operator k (index (strips_problem.operators_of \<Pi>) op\<^sub>2))\<inverse> }} | k. k \<in> {0..<t}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})
[PROOF STEP]
let ?ops = "strips_problem.operators_of \<Pi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})
[PROOF STEP]
let ?interfering = "filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2
    \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product ?ops ?ops)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})
[PROOF STEP]
let ?fs = "[encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2.
    (op\<^sub>1, op\<^sub>2) \<leftarrow> ?interfering, k \<leftarrow> [0..<t]]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})
[PROOF STEP]
have "cnf (encode_interfering_operator_exclusion \<Pi> t) = cnf (foldr (\<^bold>\<and>) ?fs (\<^bold>\<not>\<bottom>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf (encode_interfering_operator_exclusion \<Pi> t) = cnf (foldr (\<^bold>\<and>) (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) (\<^bold>\<not> \<bottom>))
[PROOF STEP]
unfolding encode_interfering_operator_exclusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf (let ops = \<Pi>\<^sub>\<O>; interfering = filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ops op\<^sub>1 \<noteq> index ops op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product ops ops) in foldr (\<^bold>\<and>) (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) interfering)) (\<^bold>\<not> \<bottom>)) = cnf (foldr (\<^bold>\<and>) (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) (\<^bold>\<not> \<bottom>))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
cnf (encode_interfering_operator_exclusion \<Pi> t) = cnf (foldr (\<^bold>\<and>) (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) (\<^bold>\<not> \<bottom>))

goal (1 subgoal):
 1. cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnf (encode_interfering_operator_exclusion \<Pi> t) = cnf (foldr (\<^bold>\<and>) (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) (\<^bold>\<not> \<bottom>))

goal (1 subgoal):
 1. cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})
[PROOF STEP]
have "\<dots> = \<Union>(cnf ` set ?fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf (foldr (\<^bold>\<and>) (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) (\<^bold>\<not> \<bottom>)) = \<Union> (cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))))
[PROOF STEP]
unfolding cnf_foldr_and[of ?fs]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>)))))) = \<Union> (cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
cnf (foldr (\<^bold>\<and>) (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) (\<^bold>\<not> \<bottom>)) = \<Union> (cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))))

goal (1 subgoal):
 1. cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cnf (encode_interfering_operator_exclusion \<Pi> t) = \<Union> (cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cnf (encode_interfering_operator_exclusion \<Pi> t) = \<Union> (cnf ` set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))))

goal (1 subgoal):
 1. cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})
[PROOF STEP]
unfolding cnf_of_encode_interfering_operator_exclusion_is_iii[of \<Pi> t]
[PROOF STATE]
proof (prove)
using this:
cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})

goal (1 subgoal):
 1. cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cnf (encode_interfering_operator_exclusion \<Pi> t) = \<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..<t}})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cnf_of_encode_interfering_operator_exclusion_contains_clause_if:
  (* TODO why do we need to fix the problem type? *)
  fixes \<Pi> :: "'variable strips_problem"
  assumes "k < t"
    and "op\<^sub>1 \<in> set (strips_problem.operators_of \<Pi>)" and "op\<^sub>2 \<in> set (strips_problem.operators_of \<Pi>)"
    and "index (strips_problem.operators_of \<Pi>) op\<^sub>1 \<noteq> index (strips_problem.operators_of \<Pi>) op\<^sub>2"
    and "are_operators_interfering op\<^sub>1 op\<^sub>2"
  shows "{ (Operator k (index (strips_problem.operators_of \<Pi>) op\<^sub>1))\<inverse>
      , (Operator k (index (strips_problem.operators_of \<Pi>) op\<^sub>2))\<inverse>}
    \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
let ?ops = "strips_problem.operators_of \<Pi>"
    and ?\<Phi>\<^sub>X = "encode_interfering_operator_exclusion \<Pi> t"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
let ?Ops = "{ (op\<^sub>1, op\<^sub>2) \<in> set (operators_of \<Pi>) \<times> set (operators_of \<Pi>).
        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..<t}}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
let ?A = "(\<Union>(op\<^sub>1, op\<^sub>2) \<in> ?Ops. ?f (op\<^sub>1, op\<^sub>2))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
let ?B = "\<Union>?A"
    and ?C = "{ (Operator k (index ?ops op\<^sub>1))\<inverse>, (Operator k (index ?ops op\<^sub>2))\<inverse> }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
have "(op\<^sub>1, op\<^sub>2) \<in> ?Ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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}
[PROOF STEP]
using assms(2, 3, 4, 5)
[PROOF STATE]
proof (prove)
using this:
op\<^sub>1 \<in> set (\<Pi>\<^sub>\<O>)
op\<^sub>2 \<in> 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

goal (1 subgoal):
 1. (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}
[PROOF STEP]
unfolding operators_of_def
[PROOF STATE]
proof (prove)
using this:
op\<^sub>1 \<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>)
op\<^sub>2 \<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>)
index ((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>) op\<^sub>1 \<noteq> index ((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>) op\<^sub>2
are_operators_interfering op\<^sub>1 op\<^sub>2

goal (1 subgoal):
 1. (op\<^sub>1, op\<^sub>2) \<in> {(op\<^sub>1, op\<^sub>2). (op\<^sub>1, op\<^sub>2) \<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>) \<times> 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>) \<and> index ((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>) op\<^sub>1 \<noteq> index ((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>) op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(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}

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

goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
have "{ ?C } \<in> ?f (op\<^sub>1, op\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} \<in> (case (op\<^sub>1, op\<^sub>2) 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..<t}})
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
k < t

goal (1 subgoal):
 1. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} \<in> (case (op\<^sub>1, op\<^sub>2) 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..<t}})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} \<in> (case (op\<^sub>1, op\<^sub>2) 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..<t}})

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

goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
have "{ ?C } \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} \<in> (\<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}})
[PROOF STEP]
using UN_iff[of ?C _ ?Ops] calculation(1, 2)
[PROOF STATE]
proof (prove)
using this:
({(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> \<Union> (?B ` {(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})) = (\<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}. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> ?B x)
(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>}} \<in> (case (op\<^sub>1, op\<^sub>2) 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..<t}})

goal (1 subgoal):
 1. {{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} \<in> (\<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} \<in> (\<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}})

goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
(* TODO slow *)
[PROOF STATE]
proof (state)
this:
{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} \<in> (\<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}})

goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(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>}} \<in> (case (op\<^sub>1, op\<^sub>2) 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..<t}})
{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} \<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}})
[PROOF STEP]
have "\<exists>X \<in> ?A. ?C \<in> X"
[PROOF STATE]
proof (prove)
using this:
(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>}} \<in> (case (op\<^sub>1, op\<^sub>2) 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..<t}})
{{(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>}} \<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}})

goal (1 subgoal):
 1. \<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}}. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}}. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> X

goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}}. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> X

goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
(* TODO slow *)
[PROOF STATE]
proof (state)
this:
\<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}}. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> X

goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}}. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> X

goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
unfolding cnf_of_encode_interfering_operator_exclusion_is
[PROOF STATE]
proof (prove)
using this:
\<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}}. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> X

goal (1 subgoal):
 1. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> \<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..<t}})
[PROOF STEP]
using Union_iff[of ?C ?A]
[PROOF STATE]
proof (prove)
using this:
\<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}}. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> X
({(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}})) = (\<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}. case (op\<^sub>1, op\<^sub>2) 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..<t}}. {(Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))\<inverse>, (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2))\<inverse>} \<in> X)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_cnf_encode_interfering_operator_exclusion:
  (* TODO why is this necessary? *)
  fixes \<Pi> :: "'variable strips_problem"
  shows "is_cnf (encode_interfering_operator_exclusion \<Pi> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
let ?ops = "strips_problem.operators_of \<Pi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
let ?interfering = "filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ?ops op\<^sub>1 \<noteq> index ?ops op\<^sub>2
    \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product ?ops ?ops)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
let ?fs = "[encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2.
    (op\<^sub>1, op\<^sub>2) \<leftarrow> ?interfering, k \<leftarrow> [0..<t]]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
let ?Fs = "(\<Union>(op\<^sub>1, op\<^sub>2)
        \<in> { (op\<^sub>1, op\<^sub>2) \<in> set (operators_of \<Pi>) \<times> set (operators_of \<Pi>). are_operators_interfering op\<^sub>1 op\<^sub>2 }.
      (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
assume "f \<in> set ?fs"
[PROOF STATE]
proof (state)
this:
f \<in> set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>)))))

goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>)))))
[PROOF STEP]
have "f \<in> ?Fs"
[PROOF STATE]
proof (prove)
using this:
f \<in> set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>)))))

goal (1 subgoal):
 1. f \<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> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
unfolding cnf_of_encode_interfering_operator_exclusion_is_ii
[PROOF STATE]
proof (prove)
using this:
f \<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}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})

goal (1 subgoal):
 1. f \<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> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<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> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})

goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<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> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})
[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 "are_operators_interfering op\<^sub>1 op\<^sub>2"
      and "f \<in> (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}"
[PROOF STATE]
proof (prove)
using this:
f \<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> are_operators_interfering op\<^sub>1 op\<^sub>2}. (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t})

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>); are_operators_interfering op\<^sub>1 op\<^sub>2; f \<in> (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>)
are_operators_interfering op\<^sub>1 op\<^sub>2
f \<in> (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}

goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[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>)
are_operators_interfering op\<^sub>1 op\<^sub>2
f \<in> (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}
[PROOF STEP]
obtain k where "f = encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
(op\<^sub>1, op\<^sub>2) \<in> set (\<Pi>\<^sub>\<O>) \<times> set (\<Pi>\<^sub>\<O>)
are_operators_interfering op\<^sub>1 op\<^sub>2
f \<in> (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) ` {0..<t}

goal (1 subgoal):
 1. (\<And>k. f = encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f = encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2

goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f = encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2
[PROOF STEP]
have "f = \<^bold>\<not>(Atom (Operator k (index ?ops op\<^sub>1))) \<^bold>\<or> \<^bold>\<not>(Atom (Operator k (index ?ops op\<^sub>2)))"
[PROOF STATE]
proof (prove)
using this:
f = encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2

goal (1 subgoal):
 1. f = \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2)))
[PROOF STEP]
unfolding encode_interfering_operator_pair_exclusion_def
[PROOF STATE]
proof (prove)
using this:
f = (let ops = \<Pi>\<^sub>\<O> in \<^bold>\<not> (Atom (Operator k (index ops op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index ops op\<^sub>2))))

goal (1 subgoal):
 1. f = \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
f = \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2)))

goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
hence "is_cnf f"
[PROOF STATE]
proof (prove)
using this:
f = \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>1))) \<^bold>\<or> \<^bold>\<not> (Atom (Operator k (index (\<Pi>\<^sub>\<O>) op\<^sub>2)))

goal (1 subgoal):
 1. is_cnf f
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
is_cnf f

goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?f2 \<in> set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) \<Longrightarrow> is_cnf ?f2

goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?f2 \<in> set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) \<Longrightarrow> is_cnf ?f2

goal (1 subgoal):
 1. is_cnf (encode_interfering_operator_exclusion \<Pi> t)
[PROOF STEP]
unfolding encode_interfering_operator_exclusion_def
[PROOF STATE]
proof (prove)
using this:
?f2 \<in> set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) \<Longrightarrow> is_cnf ?f2

goal (1 subgoal):
 1. is_cnf (let ops = \<Pi>\<^sub>\<O>; interfering = filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ops op\<^sub>1 \<noteq> index ops op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product ops ops) in foldr (\<^bold>\<and>) (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) interfering)) (\<^bold>\<not> \<bottom>))
[PROOF STEP]
using is_cnf_foldr_and_if[of ?fs]
[PROOF STATE]
proof (prove)
using this:
?f2 \<in> set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) \<Longrightarrow> is_cnf ?f2
\<forall>f\<in>set (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))). is_cnf f \<Longrightarrow> is_cnf (foldr (\<^bold>\<and>) (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) (filter (\<lambda>(op\<^sub>1, op\<^sub>2). 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) (List.product (\<Pi>\<^sub>\<O>) (\<Pi>\<^sub>\<O>))))) (\<^bold>\<not> \<bottom>))

goal (1 subgoal):
 1. is_cnf (let ops = \<Pi>\<^sub>\<O>; interfering = filter (\<lambda>(op\<^sub>1, op\<^sub>2). index ops op\<^sub>1 \<noteq> index ops op\<^sub>2 \<and> are_operators_interfering op\<^sub>1 op\<^sub>2) (List.product ops ops) in foldr (\<^bold>\<and>) (concat (map (\<lambda>(op\<^sub>1, op\<^sub>2). map (\<lambda>k. encode_interfering_operator_pair_exclusion \<Pi> k op\<^sub>1 op\<^sub>2) [0..<t]) interfering)) (\<^bold>\<not> \<bottom>))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
is_cnf (encode_interfering_operator_exclusion \<Pi> t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_cnf_encode_problem_with_operator_interference_exclusion:
  assumes "is_valid_problem_strips \<Pi>"
  shows "is_cnf (\<Phi>\<^sub>\<forall> \<Pi> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cnf (\<Phi>\<^sub>\<forall> \<Pi> t)
[PROOF STEP]
using is_cnf_encode_problem is_cnf_encode_interfering_operator_exclusion assms
[PROOF STATE]
proof (prove)
using this:
is_valid_problem_strips ?\<Pi> \<Longrightarrow> is_cnf (\<Phi> ?\<Pi> ?t)
is_cnf (encode_interfering_operator_exclusion ?\<Pi> ?t)
is_valid_problem_strips \<Pi>

goal (1 subgoal):
 1. is_cnf (\<Phi>\<^sub>\<forall> \<Pi> t)
[PROOF STEP]
unfolding encode_problem_with_operator_interference_exclusion_def SAT_Plan_Base.encode_problem_def
    is_cnf.simps(1)
[PROOF STATE]
proof (prove)
using this:
is_valid_problem_strips ?\<Pi> \<Longrightarrow> is_cnf (\<Phi>\<^sub>I ?\<Pi>) \<and> is_cnf (encode_operators ?\<Pi> ?t) \<and> is_cnf (encode_all_frame_axioms ?\<Pi> ?t) \<and> is_cnf ((\<Phi>\<^sub>G ?\<Pi>) ?t)
is_cnf (encode_interfering_operator_exclusion ?\<Pi> ?t)
is_valid_problem_strips \<Pi>

goal (1 subgoal):
 1. is_cnf (\<Phi>\<^sub>I \<Pi>) \<and> is_cnf (encode_operators \<Pi> t) \<and> is_cnf (encode_all_frame_axioms \<Pi> t) \<and> is_cnf (encode_interfering_operator_exclusion \<Pi> t) \<and> is_cnf ((\<Phi>\<^sub>G \<Pi>) t)
[PROOF STEP]
by blast


[STATEMENT]
lemma cnf_of_encode_problem_with_operator_interference_exclusion_structure:
  shows "cnf (\<Phi>\<^sub>I \<Pi>) \<subseteq> cnf (\<Phi>\<^sub>\<forall> \<Pi> t)"
    and "cnf ((\<Phi>\<^sub>G \<Pi>) t) \<subseteq> cnf (\<Phi>\<^sub>\<forall> \<Pi> t)"
    and "cnf (encode_operators \<Pi> t) \<subseteq> cnf (\<Phi>\<^sub>\<forall> \<Pi> t)"
    and "cnf (encode_all_frame_axioms \<Pi> t) \<subseteq> cnf (\<Phi>\<^sub>\<forall> \<Pi> t)"
    and "cnf (encode_interfering_operator_exclusion \<Pi> t) \<subseteq> cnf (\<Phi>\<^sub>\<forall> \<Pi> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cnf (\<Phi>\<^sub>I \<Pi>) \<subseteq> cnf (\<Phi>\<^sub>\<forall> \<Pi> t) &&& cnf ((\<Phi>\<^sub>G \<Pi>) t) \<subseteq> cnf (\<Phi>\<^sub>\<forall> \<Pi> t)) &&& cnf (encode_operators \<Pi> t) \<subseteq> cnf (\<Phi>\<^sub>\<forall> \<Pi> t) &&& cnf (encode_all_frame_axioms \<Pi> t) \<subseteq> cnf (\<Phi>\<^sub>\<forall> \<Pi> t) &&& cnf (encode_interfering_operator_exclusion \<Pi> t) \<subseteq> cnf (\<Phi>\<^sub>\<forall> \<Pi> t)
[PROOF STEP]
unfolding encode_problem_with_operator_interference_exclusion_def encode_problem_def SAT_Plan_Base.encode_problem_def
    encode_initial_state_def
    encode_goal_state_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cnf (let I = \<Pi>\<^sub>I; vs = \<Pi>\<^sub>\<V> in \<^bold>\<And>map (\<lambda>v. encode_state_variable 0 (index vs v) (I v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. I v \<noteq> None) vs)) \<subseteq> cnf ((let I = \<Pi>\<^sub>I; vs = \<Pi>\<^sub>\<V> in \<^bold>\<And>map (\<lambda>v. encode_state_variable 0 (index vs v) (I v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. I v \<noteq> None) vs)) \<^bold>\<and> (encode_operators \<Pi> t \<^bold>\<and> (encode_all_frame_axioms \<Pi> t \<^bold>\<and> (encode_interfering_operator_exclusion \<Pi> t \<^bold>\<and> (let vs = \<Pi>\<^sub>\<V>; G = \<Pi>\<^sub>G in \<^bold>\<And>map (\<lambda>v. encode_state_variable t (index vs v) (G v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. G v \<noteq> None) vs)))))) &&& cnf (let vs = \<Pi>\<^sub>\<V>; G = \<Pi>\<^sub>G in \<^bold>\<And>map (\<lambda>v. encode_state_variable t (index vs v) (G v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. G v \<noteq> None) vs)) \<subseteq> cnf ((let I = \<Pi>\<^sub>I; vs = \<Pi>\<^sub>\<V> in \<^bold>\<And>map (\<lambda>v. encode_state_variable 0 (index vs v) (I v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. I v \<noteq> None) vs)) \<^bold>\<and> (encode_operators \<Pi> t \<^bold>\<and> (encode_all_frame_axioms \<Pi> t \<^bold>\<and> (encode_interfering_operator_exclusion \<Pi> t \<^bold>\<and> (let vs = \<Pi>\<^sub>\<V>; G = \<Pi>\<^sub>G in \<^bold>\<And>map (\<lambda>v. encode_state_variable t (index vs v) (G v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. G v \<noteq> None) vs))))))) &&& cnf (encode_operators \<Pi> t) \<subseteq> cnf ((let I = \<Pi>\<^sub>I; vs = \<Pi>\<^sub>\<V> in \<^bold>\<And>map (\<lambda>v. encode_state_variable 0 (index vs v) (I v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. I v \<noteq> None) vs)) \<^bold>\<and> (encode_operators \<Pi> t \<^bold>\<and> (encode_all_frame_axioms \<Pi> t \<^bold>\<and> (encode_interfering_operator_exclusion \<Pi> t \<^bold>\<and> (let vs = \<Pi>\<^sub>\<V>; G = \<Pi>\<^sub>G in \<^bold>\<And>map (\<lambda>v. encode_state_variable t (index vs v) (G v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. G v \<noteq> None) vs)))))) &&& cnf (encode_all_frame_axioms \<Pi> t) \<subseteq> cnf ((let I = \<Pi>\<^sub>I; vs = \<Pi>\<^sub>\<V> in \<^bold>\<And>map (\<lambda>v. encode_state_variable 0 (index vs v) (I v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. I v \<noteq> None) vs)) \<^bold>\<and> (encode_operators \<Pi> t \<^bold>\<and> (encode_all_frame_axioms \<Pi> t \<^bold>\<and> (encode_interfering_operator_exclusion \<Pi> t \<^bold>\<and> (let vs = \<Pi>\<^sub>\<V>; G = \<Pi>\<^sub>G in \<^bold>\<And>map (\<lambda>v. encode_state_variable t (index vs v) (G v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. G v \<noteq> None) vs)))))) &&& cnf (encode_interfering_operator_exclusion \<Pi> t) \<subseteq> cnf ((let I = \<Pi>\<^sub>I; vs = \<Pi>\<^sub>\<V> in \<^bold>\<And>map (\<lambda>v. encode_state_variable 0 (index vs v) (I v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. I v \<noteq> None) vs)) \<^bold>\<and> (encode_operators \<Pi> t \<^bold>\<and> (encode_all_frame_axioms \<Pi> t \<^bold>\<and> (encode_interfering_operator_exclusion \<Pi> t \<^bold>\<and> (let vs = \<Pi>\<^sub>\<V>; G = \<Pi>\<^sub>G in \<^bold>\<And>map (\<lambda>v. encode_state_variable t (index vs v) (G v) \<^bold>\<or> \<bottom>) (filter (\<lambda>v. G v \<noteq> None) vs))))))
[PROOF STEP]
by auto+


[STATEMENT]
lemma encode_problem_with_operator_interference_exclusion_has_model_then_also_partial_encodings:
  assumes "\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t"
  shows "\<A> \<Turnstile> SAT_Plan_Base.encode_initial_state \<Pi>"
    and "\<A> \<Turnstile> SAT_Plan_Base.encode_operators \<Pi> t"
    and "\<A> \<Turnstile> SAT_Plan_Base.encode_all_frame_axioms \<Pi> t"
    and "\<A> \<Turnstile> encode_interfering_operator_exclusion \<Pi> t"
    and "\<A> \<Turnstile> SAT_Plan_Base.encode_goal_state \<Pi> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<A> \<Turnstile> \<Phi>\<^sub>I \<Pi> &&& \<A> \<Turnstile> encode_operators \<Pi> t) &&& \<A> \<Turnstile> encode_all_frame_axioms \<Pi> t &&& \<A> \<Turnstile> encode_interfering_operator_exclusion \<Pi> t &&& \<A> \<Turnstile> (\<Phi>\<^sub>G \<Pi>) t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<A> \<Turnstile> \<Phi>\<^sub>\<forall> \<Pi> t

goal (1 subgoal):
 1. (\<A> \<Turnstile> \<Phi>\<^sub>I \<Pi> &&& \<A> \<Turnstile> encode_operators \<Pi> t) &&& \<A> \<Turnstile> encode_all_frame_axioms \<Pi> t &&& \<A> \<Turnstile> encode_interfering_operator_exclusion \<Pi> t &&& \<A> \<Turnstile> (\<Phi>\<^sub>G \<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> &&& \<A> \<Turnstile> encode_operators \<Pi> t) &&& \<A> \<Turnstile> encode_all_frame_axioms \<Pi> t &&& \<A> \<Turnstile> encode_interfering_operator_exclusion \<Pi> t &&& \<A> \<Turnstile> (\<Phi>\<^sub>G \<Pi>) t
[PROOF STEP]
by simp+