[STATEMENT]
lemma reduce_clauses_in_P:
  assumes
    c_in: "C \<in> fst ` set N" and
    p_irred: "\<forall>(E, k) \<in> set P. is_irreducible [C] E"
  shows "wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ reduce_all C P', Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ reduce_all C P', Q, n)
[PROOF STEP]
unfolding reduce_all_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
using p_irred
[PROOF STATE]
proof (prove)
using this:
\<forall>(E, k)\<in>set P. is_irreducible [C] E

goal (1 subgoal):
 1. wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
proof (induct "length P'" arbitrary: P P')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>l = length ?P'; \<forall>(E, k)\<in>set ?P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, ?P @ ?P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, ?P @ map (apfst (reduce [C] [])) ?P', Q, n)
Suc l = length P'
\<forall>(E, k)\<in>set P. is_irreducible [C] E

goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
note ih = this(1) and suc_l = this(2) and p_irred = this(3)
[PROOF STATE]
proof (state)
this:
\<lbrakk>l = length ?P'; \<forall>(E, k)\<in>set ?P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, ?P @ ?P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, ?P @ map (apfst (reduce [C] [])) ?P', Q, n)
Suc l = length P'
\<forall>(E, k)\<in>set P. is_irreducible [C] E

goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
have p'_nnil: "P' \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P' \<noteq> []
[PROOF STEP]
using suc_l
[PROOF STATE]
proof (prove)
using this:
Suc l = length P'

goal (1 subgoal):
 1. P' \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P' \<noteq> []

goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
define j :: nat where
    "j = Max (snd ` set P')"
[PROOF STATE]
proof (state)
this:
j = Max (snd ` set P')

goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
obtain Dj :: "'a dclause" where
    dj_in: "Dj \<in> set P'" and
    snd_dj: "snd Dj = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Dj. \<lbrakk>Dj \<in> set P'; snd Dj = j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Max_in[of "snd ` set P'", unfolded image_def, simplified]
[PROOF STATE]
proof (prove)
using this:
\<exists>x. \<exists>xa\<in>set P'. x = snd xa \<Longrightarrow> \<exists>x\<in>set P'. Max {y. \<exists>x\<in>set P'. y = snd x} = snd x

goal (1 subgoal):
 1. (\<And>Dj. \<lbrakk>Dj \<in> set P'; snd Dj = j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis image_def j_def length_Suc_conv list.set_intros(1) suc_l)
[PROOF STATE]
proof (state)
this:
Dj \<in> set P'
snd Dj = j

goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
have "\<forall>k \<in> snd ` set P'. k \<le> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>snd ` set P'. k \<le> j
[PROOF STEP]
unfolding j_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>snd ` set P'. k \<le> Max (snd ` set P')
[PROOF STEP]
using p'_nnil
[PROOF STATE]
proof (prove)
using this:
P' \<noteq> []

goal (1 subgoal):
 1. \<forall>k\<in>snd ` set P'. k \<le> Max (snd ` set P')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>k\<in>snd ` set P'. k \<le> j

goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>k\<in>snd ` set P'. k \<le> j
[PROOF STEP]
have j_max: "\<forall>(E, k) \<in> set P'. j \<ge> k"
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>snd ` set P'. k \<le> j

goal (1 subgoal):
 1. \<forall>(E, k)\<in>set P'. k \<le> j
[PROOF STEP]
unfolding image_def
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<in>{y. \<exists>x\<in>set P'. y = snd x}. k \<le> j

goal (1 subgoal):
 1. \<forall>(E, k)\<in>set P'. k \<le> j
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>(E, k)\<in>set P'. k \<le> j

goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
obtain P1' P2' :: "'a dclause list"  where
    p': "P' = P1' @ Dj # P2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P1' P2'. P' = P1' @ Dj # P2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using split_list[OF dj_in]
[PROOF STATE]
proof (prove)
using this:
\<exists>ys zs. P' = ys @ Dj # zs

goal (1 subgoal):
 1. (\<And>P1' P2'. P' = P1' @ Dj # P2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P' = P1' @ Dj # P2'

goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
have "wstate_of_dstate (N, P @ P1' @ Dj # P2', Q, n)
     \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P @ P1' @ Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)
[PROOF STEP]
unfolding append_assoc[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, (P @ P1') @ Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (P @ P1') @ apfst (reduce [C] []) Dj # P2', Q, n)
[PROOF STEP]
apply (subst (1 2) surjective_pairing[of Dj, unfolded snd_dj])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, (P @ P1') @ (fst Dj, j) # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (P @ P1') @ apfst (reduce [C] []) (fst Dj, j) # P2', Q, n)
[PROOF STEP]
apply (simp only: apfst_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, (P @ P1') @ (fst Dj, j) # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (P @ P1') @ (reduce [C] [] (fst Dj), j) # P2', Q, n)
[PROOF STEP]
apply (rule reduce_clause_in_P[of _ _ _ _ _ "[]", unfolded append_Nil, OF c_in])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(E, k)\<in>set ((P @ P1') @ P2'). j < k \<longrightarrow> is_irreducible [C] E
[PROOF STEP]
using p_irred j_max[unfolded p']
[PROOF STATE]
proof (prove)
using this:
\<forall>(E, k)\<in>set P. is_irreducible [C] E
\<forall>(E, k)\<in>set (P1' @ Dj # P2'). k \<le> j

goal (1 subgoal):
 1. \<forall>(E, k)\<in>set ((P @ P1') @ P2'). j < k \<longrightarrow> is_irreducible [C] E
[PROOF STEP]
by (force simp: case_prod_beta)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P @ P1' @ Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)

goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P @ P1' @ Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)

goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
have "wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)
     \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)
[PROOF STEP]
apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
          ih[of "P1' @ P2'" "apfst (reduce [C] []) Dj # P"]])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. wstate_of_dstate (N, (apfst (reduce [C] []) Dj # P) @ P1' @ P2', Q, n) = wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)
 2. wstate_of_dstate (N, (apfst (reduce [C] []) Dj # P) @ map (apfst (reduce [C] [])) (P1' @ P2'), Q, n) = wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)
 3. l = length (P1' @ P2')
 4. \<forall>(E, k)\<in>set (apfst (reduce [C] []) Dj # P). is_irreducible [C] E
[PROOF STEP]
using suc_l reduce_idem p_irred
[PROOF STATE]
proof (prove)
using this:
Suc l = length P'
reduce ?Ds ?C (reduce ?Ds ?C ?E) = reduce ?Ds ?C ?E
\<forall>(E, k)\<in>set P. is_irreducible [C] E

goal (4 subgoals):
 1. wstate_of_dstate (N, (apfst (reduce [C] []) Dj # P) @ P1' @ P2', Q, n) = wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)
 2. wstate_of_dstate (N, (apfst (reduce [C] []) Dj # P) @ map (apfst (reduce [C] [])) (P1' @ P2'), Q, n) = wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)
 3. l = length (P1' @ P2')
 4. \<forall>(E, k)\<in>set (apfst (reduce [C] []) Dj # P). is_irreducible [C] E
[PROOF STEP]
unfolding p'
[PROOF STATE]
proof (prove)
using this:
Suc l = length (P1' @ Dj # P2')
reduce ?Ds ?C (reduce ?Ds ?C ?E) = reduce ?Ds ?C ?E
\<forall>(E, k)\<in>set P. is_irreducible [C] E

goal (4 subgoals):
 1. wstate_of_dstate (N, (apfst (reduce [C] []) Dj # P) @ P1' @ P2', Q, n) = wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)
 2. wstate_of_dstate (N, (apfst (reduce [C] []) Dj # P) @ map (apfst (reduce [C] [])) (P1' @ P2'), Q, n) = wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)
 3. l = length (P1' @ P2')
 4. \<forall>(E, k)\<in>set (apfst (reduce [C] []) Dj # P). is_irreducible [C] E
[PROOF STEP]
by (auto simp: case_prod_beta)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)

goal (2 subgoals):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
 2. \<And>x P' P. \<lbrakk>\<And>P' P. \<lbrakk>x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n); Suc x = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate (N, P @ P1' @ Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)
wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P @ P1' @ Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)
wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)

goal (1 subgoal):
 1. wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
unfolding p'
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P @ P1' @ Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)
wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)

goal (1 subgoal):
 1. wstate_of_dstate (N, P @ P1' @ Dj # P2', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)

goal (1 subgoal):
 1. \<And>P' P. \<lbrakk>0 = length P'; \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) P', Q, n)
[PROOF STEP]
qed simp


[STATEMENT]
lemma reduce_clauses_in_Q:
  assumes
    c_in: "C \<in> fst ` set N" and
    p_irred: "\<forall>(E, k) \<in> set P. is_irreducible [C] E"
  shows "wstate_of_dstate (N, P, Q @ Q', n)
    \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C Q') @ P, Q @ snd (reduce_all2 C Q'), n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C Q') @ P, Q @ snd (reduce_all2 C Q'), n)
[PROOF STEP]
using p_irred
[PROOF STATE]
proof (prove)
using this:
\<forall>(E, k)\<in>set P. is_irreducible [C] E

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C Q') @ P, Q @ snd (reduce_all2 C Q'), n)
[PROOF STEP]
proof (induct Q' arbitrary: P Q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q. \<forall>(E, k)\<in>set P. is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, P, Q @ [], n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C []) @ P, Q @ snd (reduce_all2 C []), n)
 2. \<And>a Q' P Q. \<lbrakk>\<And>P Q. \<forall>(E, k)\<in>set P. is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, P, Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C Q') @ P, Q @ snd (reduce_all2 C Q'), n); \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ a # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (a # Q')) @ P, Q @ snd (reduce_all2 C (a # Q')), n)
[PROOF STEP]
case (Cons Dj Q')
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set ?P. case a of (E, k) \<Rightarrow> is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, ?P, ?Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C Q') @ ?P, ?Q @ snd (reduce_all2 C Q'), n)
\<forall>a\<in>set P. case a of (E, k) \<Rightarrow> is_irreducible [C] E

goal (2 subgoals):
 1. \<And>P Q. \<forall>(E, k)\<in>set P. is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, P, Q @ [], n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C []) @ P, Q @ snd (reduce_all2 C []), n)
 2. \<And>a Q' P Q. \<lbrakk>\<And>P Q. \<forall>(E, k)\<in>set P. is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, P, Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C Q') @ P, Q @ snd (reduce_all2 C Q'), n); \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ a # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (a # Q')) @ P, Q @ snd (reduce_all2 C (a # Q')), n)
[PROOF STEP]
note ih = this(1) and p_irred = this(2)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set ?P. case a of (E, k) \<Rightarrow> is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, ?P, ?Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C Q') @ ?P, ?Q @ snd (reduce_all2 C Q'), n)
\<forall>a\<in>set P. case a of (E, k) \<Rightarrow> is_irreducible [C] E

goal (2 subgoals):
 1. \<And>P Q. \<forall>(E, k)\<in>set P. is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, P, Q @ [], n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C []) @ P, Q @ snd (reduce_all2 C []), n)
 2. \<And>a Q' P Q. \<lbrakk>\<And>P Q. \<forall>(E, k)\<in>set P. is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, P, Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C Q') @ P, Q @ snd (reduce_all2 C Q'), n); \<forall>(E, k)\<in>set P. is_irreducible [C] E\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ a # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (a # Q')) @ P, Q @ snd (reduce_all2 C (a # Q')), n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
[PROOF STEP]
proof (cases "is_irreducible [C] (fst Dj)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_irreducible [C] (fst Dj) \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
 2. reduce [C] [] (fst Dj) \<noteq> fst Dj \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_irreducible [C] (fst Dj)

goal (2 subgoals):
 1. is_irreducible [C] (fst Dj) \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
 2. reduce [C] [] (fst Dj) \<noteq> fst Dj \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_irreducible [C] (fst Dj)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_irreducible [C] (fst Dj)

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
[PROOF STEP]
using ih[of _ "Q @ [Dj]"] p_irred
[PROOF STATE]
proof (prove)
using this:
is_irreducible [C] (fst Dj)
\<forall>a\<in>set ?P. case a of (E, k) \<Rightarrow> is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, ?P, (Q @ [Dj]) @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C Q') @ ?P, (Q @ [Dj]) @ snd (reduce_all2 C Q'), n)
\<forall>a\<in>set P. case a of (E, k) \<Rightarrow> is_irreducible [C] E

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
[PROOF STEP]
by (simp add: case_prod_beta)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)

goal (1 subgoal):
 1. reduce [C] [] (fst Dj) \<noteq> fst Dj \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. reduce [C] [] (fst Dj) \<noteq> fst Dj \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
[PROOF STEP]
case d_red: False
[PROOF STATE]
proof (state)
this:
reduce [C] [] (fst Dj) \<noteq> fst Dj

goal (1 subgoal):
 1. reduce [C] [] (fst Dj) \<noteq> fst Dj \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
[PROOF STEP]
have "wstate_of_dstate (N, P, Q @ Dj # Q', n)
      \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (reduce [C] [] (fst Dj), snd Dj) # P, Q @ Q', n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (reduce [C] [] (fst Dj), snd Dj) # P, Q @ Q', n)
[PROOF STEP]
using p_irred reduce_clause_in_Q[of _ _ P "snd Dj" "[]" _ Q Q' n, OF c_in _ d_red]
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set P. case a of (E, k) \<Rightarrow> is_irreducible [C] E
\<forall>(E, k)\<in>set P. snd Dj < k \<longrightarrow> is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, P, Q @ ([] @ fst Dj, snd Dj) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, ([] @ reduce [C] [] (fst Dj), snd Dj) # P, Q @ Q', n)

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (reduce [C] [] (fst Dj), snd Dj) # P, Q @ Q', n)
[PROOF STEP]
by (cases Dj) force
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (reduce [C] [] (fst Dj), snd Dj) # P, Q @ Q', n)

goal (1 subgoal):
 1. reduce [C] [] (fst Dj) \<noteq> fst Dj \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (reduce [C] [] (fst Dj), snd Dj) # P, Q @ Q', n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (reduce [C] [] (fst Dj), snd Dj) # P, Q @ Q', n)

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
[PROOF STEP]
using ih[of "(reduce [C] [] (fst Dj), snd Dj) # P" Q] d_red p_irred reduce_idem
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (reduce [C] [] (fst Dj), snd Dj) # P, Q @ Q', n)
\<forall>a\<in>set ((reduce [C] [] (fst Dj), snd Dj) # P). case a of (E, k) \<Rightarrow> is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, (reduce [C] [] (fst Dj), snd Dj) # P, Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C Q') @ (reduce [C] [] (fst Dj), snd Dj) # P, Q @ snd (reduce_all2 C Q'), n)
reduce [C] [] (fst Dj) \<noteq> fst Dj
\<forall>a\<in>set P. case a of (E, k) \<Rightarrow> is_irreducible [C] E
reduce ?Ds ?C (reduce ?Ds ?C ?E) = reduce ?Ds ?C ?E

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)
[PROOF STEP]
by (force simp: case_prod_beta)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C (Dj # Q')) @ P, Q @ snd (reduce_all2 C (Dj # Q')), n)

goal (1 subgoal):
 1. \<And>P Q. \<forall>(E, k)\<in>set P. is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, P, Q @ [], n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C []) @ P, Q @ snd (reduce_all2 C []), n)
[PROOF STEP]
qed simp


[STATEMENT]
lemma eligible_iff:
  "eligible S \<sigma> As DA \<longleftrightarrow> As = [] \<or> length As = 1 \<and> maximal_wrt (hd As \<cdot>a \<sigma>) (DA \<cdot> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eligible S \<sigma> As DA = (As = [] \<or> length As = 1 \<and> maximal_wrt (hd As \<cdot>a \<sigma>) (DA \<cdot> \<sigma>))
[PROOF STEP]
unfolding eligible.simps S_empty
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>DAa Asa \<sigma>'. \<sigma> = \<sigma>' \<and> As = Asa \<and> DA = DAa \<and> ({#} = negs (mset Asa) \<or> {#} = {#} \<and> length Asa = 1 \<and> maximal_wrt (Asa ! 0 \<cdot>a \<sigma>') (DAa \<cdot> \<sigma>'))) = (As = [] \<or> length As = 1 \<and> maximal_wrt (hd As \<cdot>a \<sigma>) (DA \<cdot> \<sigma>))
[PROOF STEP]
by (fastforce dest: hd_conv_nth)


[STATEMENT]
lemma ord_resolve_one_side_prem:
  "ord_resolve S CAs DA AAs As \<sigma> E \<Longrightarrow> length CAs = 1 \<and> length AAs = 1 \<and> length As = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_resolve S CAs DA AAs As \<sigma> E \<Longrightarrow> length CAs = 1 \<and> length AAs = 1 \<and> length As = 1
[PROOF STEP]
by (force elim!: ord_resolve.cases simp: eligible_iff)


[STATEMENT]
lemma ord_resolve_rename_one_side_prem:
  "ord_resolve_rename S CAs DA AAs As \<sigma> E \<Longrightarrow> length CAs = 1 \<and> length AAs = 1 \<and> length As = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_resolve_rename S CAs DA AAs As \<sigma> E \<Longrightarrow> length CAs = 1 \<and> length AAs = 1 \<and> length As = 1
[PROOF STEP]
by (force elim!: ord_resolve_rename.cases dest: ord_resolve_one_side_prem)


[STATEMENT]
lemma set_resolve_eq_UNION_set_resolve_on:
  "set (resolve C D) =
   (\<Union>L \<in> set D.
      (case L of
         Pos _ \<Rightarrow> {}
       | Neg A \<Rightarrow> if maximal_wrt A (mset D) then set (resolve_on A (remove1 L D) C) else {}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (resolve C D) = (\<Union>L\<in>set D. case L of Pos x \<Rightarrow> {} | Neg A \<Rightarrow> if maximal_wrt A (mset D) then set (resolve_on A (remove1 L D) C) else {})
[PROOF STEP]
unfolding resolve_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (concat (map (\<lambda>L. case L of Pos A \<Rightarrow> [] | Neg A \<Rightarrow> if maximal_wrt A (mset D) then resolve_on A (remove1 L D) C else []) D)) = (\<Union>L\<in>set D. case L of Pos x \<Rightarrow> {} | Neg A \<Rightarrow> if maximal_wrt A (mset D) then set (resolve_on A (remove1 L D) C) else {})
[PROOF STEP]
by (fastforce split: literal.splits if_splits)


[STATEMENT]
lemma resolve_eq_Bin_ord_resolve: "mset ` set (resolve C D) = Bin_ord_resolve (mset C) (mset D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset ` set (resolve C D) = Bin_ord_resolve (mset C) (mset D)
[PROOF STEP]
unfolding set_resolve_eq_UNION_set_resolve_on
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset ` (\<Union>L\<in>set D. case L of Pos x \<Rightarrow> {} | Neg A \<Rightarrow> if maximal_wrt A (mset D) then set (resolve_on A (remove1 L D) C) else {}) = Bin_ord_resolve (mset C) (mset D)
[PROOF STEP]
apply (unfold image_UN literal.case_distrib if_distrib)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>set D. case x of Pos x \<Rightarrow> mset ` {} | Neg xa \<Rightarrow> if maximal_wrt xa (mset D) then mset ` set (resolve_on xa (remove1 x D) C) else mset ` {}) = Bin_ord_resolve (mset C) (mset D)
[PROOF STEP]
apply (subst resolve_on_eq_UNION_Bin_ord_resolve)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>set D. case x of Pos x \<Rightarrow> mset ` {} | Neg xa \<Rightarrow> if maximal_wrt xa (mset D) then {E. \<exists>AA \<sigma>. ord_resolve S [mset C] ({#Neg xa#} + mset (remove1 x D)) [AA] [xa] \<sigma> E} else mset ` {}) = Bin_ord_resolve (mset C) (mset D)
[PROOF STEP]
apply (rule order_antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<Union>x\<in>set D. case x of Pos x \<Rightarrow> mset ` {} | Neg xa \<Rightarrow> if maximal_wrt xa (mset D) then {E. \<exists>AA \<sigma>. ord_resolve S [mset C] ({#Neg xa#} + mset (remove1 x D)) [AA] [xa] \<sigma> E} else mset ` {}) \<subseteq> Bin_ord_resolve (mset C) (mset D)
 2. Bin_ord_resolve (mset C) (mset D) \<subseteq> (\<Union>x\<in>set D. case x of Pos x \<Rightarrow> mset ` {} | Neg xa \<Rightarrow> if maximal_wrt xa (mset D) then {E. \<exists>AA \<sigma>. ord_resolve S [mset C] ({#Neg xa#} + mset (remove1 x D)) [AA] [xa] \<sigma> E} else mset ` {})
[PROOF STEP]
apply (force split: literal.splits if_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bin_ord_resolve (mset C) (mset D) \<subseteq> (\<Union>x\<in>set D. case x of Pos x \<Rightarrow> mset ` {} | Neg xa \<Rightarrow> if maximal_wrt xa (mset D) then {E. \<exists>AA \<sigma>. ord_resolve S [mset C] ({#Neg xa#} + mset (remove1 x D)) [AA] [xa] \<sigma> E} else mset ` {})
[PROOF STEP]
apply (clarsimp split: literal.splits if_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> \<exists>xa\<in>set D. (\<forall>x1. xa \<noteq> Pos x1) \<and> (\<forall>x2. (maximal_wrt x2 (mset D) \<longrightarrow> xa = Neg x2 \<longrightarrow> (\<exists>AA \<sigma>. ord_resolve S [mset C] (add_mset (Neg x2) (remove1_mset (Neg x2) (mset D))) [AA] [x2] \<sigma> x)) \<and> (\<not> maximal_wrt x2 (mset D) \<longrightarrow> xa \<noteq> Neg x2))
[PROOF STEP]
apply (rule_tac x = "Neg A" in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> (\<forall>x1. Neg A \<noteq> Pos x1) \<and> (\<forall>x2. (maximal_wrt x2 (mset D) \<longrightarrow> Neg A = Neg x2 \<longrightarrow> (\<exists>AA \<sigma>. ord_resolve S [mset C] (add_mset (Neg x2) (remove1_mset (Neg x2) (mset D))) [AA] [x2] \<sigma> x)) \<and> (\<not> maximal_wrt x2 (mset D) \<longrightarrow> Neg A \<noteq> Neg x2))
 2. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> \<forall>x1. Neg A \<noteq> Pos x1
 2. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> \<forall>x2. (maximal_wrt x2 (mset D) \<longrightarrow> Neg A = Neg x2 \<longrightarrow> (\<exists>AA \<sigma>. ord_resolve S [mset C] (add_mset (Neg x2) (remove1_mset (Neg x2) (mset D))) [AA] [x2] \<sigma> x)) \<and> (\<not> maximal_wrt x2 (mset D) \<longrightarrow> Neg A \<noteq> Neg x2)
 3. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> \<forall>x2. (maximal_wrt x2 (mset D) \<longrightarrow> Neg A = Neg x2 \<longrightarrow> (\<exists>AA \<sigma>. ord_resolve S [mset C] (add_mset (Neg x2) (remove1_mset (Neg x2) (mset D))) [AA] [x2] \<sigma> x)) \<and> (\<not> maximal_wrt x2 (mset D) \<longrightarrow> Neg A \<noteq> Neg x2)
 2. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x AA A \<sigma> x2. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> (maximal_wrt x2 (mset D) \<longrightarrow> Neg A = Neg x2 \<longrightarrow> (\<exists>AA \<sigma>. ord_resolve S [mset C] (add_mset (Neg x2) (remove1_mset (Neg x2) (mset D))) [AA] [x2] \<sigma> x)) \<and> (\<not> maximal_wrt x2 (mset D) \<longrightarrow> Neg A \<noteq> Neg x2)
 2. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x AA A \<sigma> x2. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> maximal_wrt x2 (mset D) \<longrightarrow> Neg A = Neg x2 \<longrightarrow> (\<exists>AA \<sigma>. ord_resolve S [mset C] (add_mset (Neg x2) (remove1_mset (Neg x2) (mset D))) [AA] [x2] \<sigma> x)
 2. \<And>x AA A \<sigma> x2. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> \<not> maximal_wrt x2 (mset D) \<longrightarrow> Neg A \<noteq> Neg x2
 3. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x AA A \<sigma> x2. \<lbrakk>ord_resolve S [mset C] (mset D) [AA] [x2] \<sigma> x; maximal_wrt x2 (mset D)\<rbrakk> \<Longrightarrow> \<exists>AA \<sigma>. ord_resolve S [mset C] (add_mset (Neg x2) (remove1_mset (Neg x2) (mset D))) [AA] [x2] \<sigma> x
 2. \<And>x AA A \<sigma> x2. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> \<not> maximal_wrt x2 (mset D) \<longrightarrow> Neg A \<noteq> Neg x2
 3. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply (rule_tac x = AA in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x AA A \<sigma> x2. \<lbrakk>ord_resolve S [mset C] (mset D) [AA] [x2] \<sigma> x; maximal_wrt x2 (mset D)\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. ord_resolve S [mset C] (add_mset (Neg x2) (remove1_mset (Neg x2) (mset D))) [AA] [x2] \<sigma> x
 2. \<And>x AA A \<sigma> x2. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> \<not> maximal_wrt x2 (mset D) \<longrightarrow> Neg A \<noteq> Neg x2
 3. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply (rule_tac x = \<sigma> in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x AA A \<sigma> x2. \<lbrakk>ord_resolve S [mset C] (mset D) [AA] [x2] \<sigma> x; maximal_wrt x2 (mset D)\<rbrakk> \<Longrightarrow> ord_resolve S [mset C] (add_mset (Neg x2) (remove1_mset (Neg x2) (mset D))) [AA] [x2] \<sigma> x
 2. \<And>x AA A \<sigma> x2. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> \<not> maximal_wrt x2 (mset D) \<longrightarrow> Neg A \<noteq> Neg x2
 3. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply (frule ord_resolve.simps[THEN iffD1])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x AA A \<sigma> x2. \<lbrakk>ord_resolve S [mset C] (mset D) [AA] [x2] \<sigma> x; maximal_wrt x2 (mset D); \<exists>CAs n Cs AAs As \<sigma>' Da. [mset C] = CAs \<and> mset D = Da + negs (mset As) \<and> [AA] = AAs \<and> [x2] = As \<and> \<sigma> = \<sigma>' \<and> x = (\<Sum>\<^sub># (mset Cs) + Da) \<cdot> \<sigma>' \<and> length CAs = n \<and> length Cs = n \<and> length AAs = n \<and> length As = n \<and> n \<noteq> 0 \<and> (\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)) \<and> (\<forall>i<n. AAs ! i \<noteq> {#}) \<and> Some \<sigma>' = mgu (set_mset ` set (Map2.map2 add_mset As AAs)) \<and> eligible S \<sigma>' As (Da + negs (mset As)) \<and> (\<forall>i<n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>') (Cs ! i \<cdot> \<sigma>')) \<and> (\<forall>i<n. S (CAs ! i) = {#})\<rbrakk> \<Longrightarrow> ord_resolve S [mset C] (add_mset (Neg x2) (remove1_mset (Neg x2) (mset D))) [AA] [x2] \<sigma> x
 2. \<And>x AA A \<sigma> x2. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> \<not> maximal_wrt x2 (mset D) \<longrightarrow> Neg A \<noteq> Neg x2
 3. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x AA A \<sigma> x2. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> \<not> maximal_wrt x2 (mset D) \<longrightarrow> Neg A \<noteq> Neg x2
 2. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply (drule ord_resolve.simps[THEN iffD1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x AA A \<sigma> x2. \<exists>CAs n Cs AAs As \<sigma>' Da. [mset C] = CAs \<and> mset D = Da + negs (mset As) \<and> [AA] = AAs \<and> [A] = As \<and> \<sigma> = \<sigma>' \<and> x = (\<Sum>\<^sub># (mset Cs) + Da) \<cdot> \<sigma>' \<and> length CAs = n \<and> length Cs = n \<and> length AAs = n \<and> length As = n \<and> n \<noteq> 0 \<and> (\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)) \<and> (\<forall>i<n. AAs ! i \<noteq> {#}) \<and> Some \<sigma>' = mgu (set_mset ` set (Map2.map2 add_mset As AAs)) \<and> eligible S \<sigma>' As (Da + negs (mset As)) \<and> (\<forall>i<n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>') (Cs ! i \<cdot> \<sigma>')) \<and> (\<forall>i<n. S (CAs ! i) = {#}) \<Longrightarrow> \<not> maximal_wrt x2 (mset D) \<longrightarrow> Neg A \<noteq> Neg x2
 2. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply (clarsimp simp: eligible_iff simp del: subst_cls_add_mset subst_cls_union)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>AA \<sigma> x2 Cs Da. \<lbrakk>mset D = add_mset (Neg x2) Da; length Cs = Suc 0; mset C = Cs ! 0 + poss AA; AA \<noteq> {#}; Some \<sigma> = mgu {insert x2 (set_mset AA)}; maximal_wrt (x2 \<cdot>a \<sigma>) (add_mset (Neg x2) Da \<cdot> \<sigma>); strictly_maximal_wrt (x2 \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>); S (Cs ! 0 + poss AA) = {#}; \<not> maximal_wrt x2 (add_mset (Neg x2) Da)\<rbrakk> \<Longrightarrow> False
 2. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply (drule maximal_wrt_subst)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>AA \<sigma> x2 Cs Da. \<lbrakk>mset D = add_mset (Neg x2) Da; length Cs = Suc 0; mset C = Cs ! 0 + poss AA; AA \<noteq> {#}; Some \<sigma> = mgu {insert x2 (set_mset AA)}; strictly_maximal_wrt (x2 \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>); S (Cs ! 0 + poss AA) = {#}; \<not> maximal_wrt x2 (add_mset (Neg x2) Da); maximal_wrt x2 (add_mset (Neg x2) Da)\<rbrakk> \<Longrightarrow> False
 2. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply sat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x AA A \<sigma>. ord_resolve S [mset C] (mset D) [AA] [A] \<sigma> x \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
apply (drule ord_resolve.simps[THEN iffD1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x AA A \<sigma>. \<exists>CAs n Cs AAs As \<sigma>' Da. [mset C] = CAs \<and> mset D = Da + negs (mset As) \<and> [AA] = AAs \<and> [A] = As \<and> \<sigma> = \<sigma>' \<and> x = (\<Sum>\<^sub># (mset Cs) + Da) \<cdot> \<sigma>' \<and> length CAs = n \<and> length Cs = n \<and> length AAs = n \<and> length As = n \<and> n \<noteq> 0 \<and> (\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)) \<and> (\<forall>i<n. AAs ! i \<noteq> {#}) \<and> Some \<sigma>' = mgu (set_mset ` set (Map2.map2 add_mset As AAs)) \<and> eligible S \<sigma>' As (Da + negs (mset As)) \<and> (\<forall>i<n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>') (Cs ! i \<cdot> \<sigma>')) \<and> (\<forall>i<n. S (CAs ! i) = {#}) \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
using set_mset_mset
[PROOF STATE]
proof (prove)
using this:
set_mset (mset ?xs) = set ?xs

goal (1 subgoal):
 1. \<And>x AA A \<sigma>. \<exists>CAs n Cs AAs As \<sigma>' Da. [mset C] = CAs \<and> mset D = Da + negs (mset As) \<and> [AA] = AAs \<and> [A] = As \<and> \<sigma> = \<sigma>' \<and> x = (\<Sum>\<^sub># (mset Cs) + Da) \<cdot> \<sigma>' \<and> length CAs = n \<and> length Cs = n \<and> length AAs = n \<and> length As = n \<and> n \<noteq> 0 \<and> (\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)) \<and> (\<forall>i<n. AAs ! i \<noteq> {#}) \<and> Some \<sigma>' = mgu (set_mset ` set (Map2.map2 add_mset As AAs)) \<and> eligible S \<sigma>' As (Da + negs (mset As)) \<and> (\<forall>i<n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>') (Cs ! i \<cdot> \<sigma>')) \<and> (\<forall>i<n. S (CAs ! i) = {#}) \<Longrightarrow> Neg A \<in> set D
[PROOF STEP]
by fastforce


[STATEMENT]
lemma poss_in_map_clauseD:
  "poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = {#f A. A \<in># AA0#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = image_mset f AA0
[PROOF STEP]
proof (induct AA arbitrary: C)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C. poss {#} \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> {#} = image_mset f AA0
 2. \<And>x AA C. \<lbrakk>\<And>C. poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = image_mset f AA0; poss (add_mset x AA) \<subseteq># map_clause f C\<rbrakk> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset x AA = image_mset f AA0
[PROOF STEP]
case (add A AA)
[PROOF STATE]
proof (state)
this:
poss AA \<subseteq># map_clause f ?C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># ?C \<and> AA = image_mset f AA0
poss (add_mset A AA) \<subseteq># map_clause f C

goal (2 subgoals):
 1. \<And>C. poss {#} \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> {#} = image_mset f AA0
 2. \<And>x AA C. \<lbrakk>\<And>C. poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = image_mset f AA0; poss (add_mset x AA) \<subseteq># map_clause f C\<rbrakk> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset x AA = image_mset f AA0
[PROOF STEP]
note ih = this(1) and aaa_sub = this(2)
[PROOF STATE]
proof (state)
this:
poss AA \<subseteq># map_clause f ?C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># ?C \<and> AA = image_mset f AA0
poss (add_mset A AA) \<subseteq># map_clause f C

goal (2 subgoals):
 1. \<And>C. poss {#} \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> {#} = image_mset f AA0
 2. \<And>x AA C. \<lbrakk>\<And>C. poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = image_mset f AA0; poss (add_mset x AA) \<subseteq># map_clause f C\<rbrakk> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset x AA = image_mset f AA0
[PROOF STEP]
have "Pos A \<in># map_clause f C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pos A \<in># map_clause f C
[PROOF STEP]
using aaa_sub
[PROOF STATE]
proof (prove)
using this:
poss (add_mset A AA) \<subseteq># map_clause f C

goal (1 subgoal):
 1. Pos A \<in># map_clause f C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Pos A \<in># map_clause f C

goal (2 subgoals):
 1. \<And>C. poss {#} \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> {#} = image_mset f AA0
 2. \<And>x AA C. \<lbrakk>\<And>C. poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = image_mset f AA0; poss (add_mset x AA) \<subseteq># map_clause f C\<rbrakk> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset x AA = image_mset f AA0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Pos A \<in># map_clause f C
[PROOF STEP]
obtain A0 where
    pa0_in: "Pos A0 \<in># C" and
    a: "A = f A0"
[PROOF STATE]
proof (prove)
using this:
Pos A \<in># map_clause f C

goal (1 subgoal):
 1. (\<And>A0. \<lbrakk>Pos A0 \<in># C; A = f A0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarify (metis literal.distinct(1) literal.exhaust literal.inject(1) literal.simps(9,10))
[PROOF STATE]
proof (state)
this:
Pos A0 \<in># C
A = f A0

goal (2 subgoals):
 1. \<And>C. poss {#} \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> {#} = image_mset f AA0
 2. \<And>x AA C. \<lbrakk>\<And>C. poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = image_mset f AA0; poss (add_mset x AA) \<subseteq># map_clause f C\<rbrakk> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset x AA = image_mset f AA0
[PROOF STEP]
have "poss AA \<subseteq># map_clause f (C - {#Pos A0#})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poss AA \<subseteq># map_clause f (remove1_mset (Pos A0) C)
[PROOF STEP]
using pa0_in aaa_sub[unfolded a]
[PROOF STATE]
proof (prove)
using this:
Pos A0 \<in># C
poss (add_mset (f A0) AA) \<subseteq># map_clause f C

goal (1 subgoal):
 1. poss AA \<subseteq># map_clause f (remove1_mset (Pos A0) C)
[PROOF STEP]
by (simp add: image_mset_remove1_mset_if insert_subset_eq_iff)
[PROOF STATE]
proof (state)
this:
poss AA \<subseteq># map_clause f (remove1_mset (Pos A0) C)

goal (2 subgoals):
 1. \<And>C. poss {#} \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> {#} = image_mset f AA0
 2. \<And>x AA C. \<lbrakk>\<And>C. poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = image_mset f AA0; poss (add_mset x AA) \<subseteq># map_clause f C\<rbrakk> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset x AA = image_mset f AA0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poss AA \<subseteq># map_clause f (remove1_mset (Pos A0) C)
[PROOF STEP]
obtain AA0 where
    paa0_sub: "poss AA0 \<subseteq># C - {#Pos A0#}" and
    aa: "AA = image_mset f AA0"
[PROOF STATE]
proof (prove)
using this:
poss AA \<subseteq># map_clause f (remove1_mset (Pos A0) C)

goal (1 subgoal):
 1. (\<And>AA0. \<lbrakk>poss AA0 \<subseteq># remove1_mset (Pos A0) C; AA = image_mset f AA0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
poss AA \<subseteq># map_clause f (remove1_mset (Pos A0) C)
poss AA \<subseteq># map_clause f ?C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># ?C \<and> AA = image_mset f AA0

goal (1 subgoal):
 1. (\<And>AA0. \<lbrakk>poss AA0 \<subseteq># remove1_mset (Pos A0) C; AA = image_mset f AA0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
poss AA0 \<subseteq># remove1_mset (Pos A0) C
AA = image_mset f AA0

goal (2 subgoals):
 1. \<And>C. poss {#} \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> {#} = image_mset f AA0
 2. \<And>x AA C. \<lbrakk>\<And>C. poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = image_mset f AA0; poss (add_mset x AA) \<subseteq># map_clause f C\<rbrakk> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset x AA = image_mset f AA0
[PROOF STEP]
have "poss (add_mset A0 AA0) \<subseteq># C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poss (add_mset A0 AA0) \<subseteq># C
[PROOF STEP]
using pa0_in paa0_sub
[PROOF STATE]
proof (prove)
using this:
Pos A0 \<in># C
poss AA0 \<subseteq># remove1_mset (Pos A0) C

goal (1 subgoal):
 1. poss (add_mset A0 AA0) \<subseteq># C
[PROOF STEP]
by (simp add: insert_subset_eq_iff)
[PROOF STATE]
proof (state)
this:
poss (add_mset A0 AA0) \<subseteq># C

goal (2 subgoals):
 1. \<And>C. poss {#} \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> {#} = image_mset f AA0
 2. \<And>x AA C. \<lbrakk>\<And>C. poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = image_mset f AA0; poss (add_mset x AA) \<subseteq># map_clause f C\<rbrakk> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset x AA = image_mset f AA0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
poss (add_mset A0 AA0) \<subseteq># C

goal (2 subgoals):
 1. \<And>C. poss {#} \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> {#} = image_mset f AA0
 2. \<And>x AA C. \<lbrakk>\<And>C. poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = image_mset f AA0; poss (add_mset x AA) \<subseteq># map_clause f C\<rbrakk> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset x AA = image_mset f AA0
[PROOF STEP]
have "add_mset A AA = image_mset f (add_mset A0 AA0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_mset A AA = image_mset f (add_mset A0 AA0)
[PROOF STEP]
unfolding a aa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_mset (f A0) (image_mset f AA0) = image_mset f (add_mset A0 AA0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
add_mset A AA = image_mset f (add_mset A0 AA0)

goal (2 subgoals):
 1. \<And>C. poss {#} \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> {#} = image_mset f AA0
 2. \<And>x AA C. \<lbrakk>\<And>C. poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = image_mset f AA0; poss (add_mset x AA) \<subseteq># map_clause f C\<rbrakk> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset x AA = image_mset f AA0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
poss (add_mset A0 AA0) \<subseteq># C
add_mset A AA = image_mset f (add_mset A0 AA0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
poss (add_mset A0 AA0) \<subseteq># C
add_mset A AA = image_mset f (add_mset A0 AA0)

goal (1 subgoal):
 1. \<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset A AA = image_mset f AA0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>AA0. poss AA0 \<subseteq># C \<and> add_mset A AA = image_mset f AA0

goal (1 subgoal):
 1. \<And>C. poss {#} \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> {#} = image_mset f AA0
[PROOF STEP]
qed simp


[STATEMENT]
lemma poss_subset_filterD:
  "poss AA \<subseteq># {#L \<cdot>l \<rho>. L \<in># mset C#} \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># mset C \<and> AA = AA0 \<cdot>am \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poss AA \<subseteq># {#L \<cdot>l \<rho>. L \<in># mset C#} \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># mset C \<and> AA = AA0 \<cdot>am \<rho>
[PROOF STEP]
unfolding subst_atm_mset_def subst_lit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poss AA \<subseteq># map_clause (\<lambda>A. A \<cdot>a \<rho>) (mset C) \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># mset C \<and> AA = {#A \<cdot>a \<rho>. A \<in># AA0#}
[PROOF STEP]
by (rule poss_in_map_clauseD)


[STATEMENT]
lemma neg_in_map_literalD: "Neg A \<in> map_literal f ` D \<Longrightarrow> \<exists>A0. Neg A0 \<in> D \<and> A = f A0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Neg A \<in> map_literal f ` D \<Longrightarrow> \<exists>A0. Neg A0 \<in> D \<and> A = f A0
[PROOF STEP]
unfolding image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Neg A \<in> {y. \<exists>x\<in>D. y = map_literal f x} \<Longrightarrow> \<exists>A0. Neg A0 \<in> D \<and> A = f A0
[PROOF STEP]
by (clarify, case_tac x, auto)


[STATEMENT]
lemma neg_in_filterD: "Neg A \<in># {#L \<cdot>l \<rho>'. L \<in># mset D#} \<Longrightarrow> \<exists>A0. Neg A0 \<in># mset D \<and> A = A0 \<cdot>a \<rho>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Neg A \<in># {#L \<cdot>l \<rho>'. L \<in># mset D#} \<Longrightarrow> \<exists>A0. Neg A0 \<in># mset D \<and> A = A0 \<cdot>a \<rho>'
[PROOF STEP]
unfolding subst_lit_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Neg A \<in># map_clause (\<lambda>A. A \<cdot>a \<rho>') (mset D) \<Longrightarrow> \<exists>A0. Neg A0 \<in># mset D \<and> A = A0 \<cdot>a \<rho>'
[PROOF STEP]
by (rule neg_in_map_literalD) simp


[STATEMENT]
lemma resolve_rename_eq_Bin_ord_resolve_rename:
  "mset ` set (resolve_rename C D) = Bin_ord_resolve_rename (mset C) (mset D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset ` set (resolve_rename C D) = Bin_ord_resolve_rename (mset C) (mset D)
[PROOF STEP]
proof (intro order_antisym subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> mset ` set (resolve_rename C D) \<Longrightarrow> x \<in> Bin_ord_resolve_rename (mset C) (mset D)
 2. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
let ?\<rho>s = "renamings_apart [mset D, mset C]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> mset ` set (resolve_rename C D) \<Longrightarrow> x \<in> Bin_ord_resolve_rename (mset C) (mset D)
 2. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
define \<rho>' :: 's where
    "\<rho>' = hd ?\<rho>s"
[PROOF STATE]
proof (state)
this:
\<rho>' = hd (renamings_apart [mset D, mset C])

goal (2 subgoals):
 1. \<And>x. x \<in> mset ` set (resolve_rename C D) \<Longrightarrow> x \<in> Bin_ord_resolve_rename (mset C) (mset D)
 2. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
define \<rho> :: 's where
    "\<rho> = last ?\<rho>s"
[PROOF STATE]
proof (state)
this:
\<rho> = last (renamings_apart [mset D, mset C])

goal (2 subgoals):
 1. \<And>x. x \<in> mset ` set (resolve_rename C D) \<Longrightarrow> x \<in> Bin_ord_resolve_rename (mset C) (mset D)
 2. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
have tl_\<rho>s: "tl ?\<rho>s = [\<rho>]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (renamings_apart [mset D, mset C]) = [\<rho>]
[PROOF STEP]
unfolding \<rho>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (renamings_apart [mset D, mset C]) = [last (renamings_apart [mset D, mset C])]
[PROOF STEP]
using renamings_apart_length Nitpick.size_list_simp(2) Suc_length_conv last.simps
[PROOF STATE]
proof (prove)
using this:
length (renamings_apart ?Cs) = length ?Cs
length ?xs = (if ?xs = [] then 0 else Suc (length (tl ?xs)))
(Suc ?n = length ?xs) = (\<exists>y ys. ?xs = y # ys \<and> length ys = ?n)
last (?x # ?xs) = (if ?xs = [] then ?x else last ?xs)

goal (1 subgoal):
 1. tl (renamings_apart [mset D, mset C]) = [last (renamings_apart [mset D, mset C])]
[PROOF STEP]
by (smt length_greater_0_conv list.sel(3))
[PROOF STATE]
proof (state)
this:
tl (renamings_apart [mset D, mset C]) = [\<rho>]

goal (2 subgoals):
 1. \<And>x. x \<in> mset ` set (resolve_rename C D) \<Longrightarrow> x \<in> Bin_ord_resolve_rename (mset C) (mset D)
 2. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
tl (renamings_apart [mset D, mset C]) = [\<rho>]

goal (2 subgoals):
 1. \<And>x. x \<in> mset ` set (resolve_rename C D) \<Longrightarrow> x \<in> Bin_ord_resolve_rename (mset C) (mset D)
 2. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
fix E
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> mset ` set (resolve_rename C D) \<Longrightarrow> x \<in> Bin_ord_resolve_rename (mset C) (mset D)
 2. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
assume e_in: "E \<in> mset ` set (resolve_rename C D)"
[PROOF STATE]
proof (state)
this:
E \<in> mset ` set (resolve_rename C D)

goal (2 subgoals):
 1. \<And>x. x \<in> mset ` set (resolve_rename C D) \<Longrightarrow> x \<in> Bin_ord_resolve_rename (mset C) (mset D)
 2. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
from e_in
[PROOF STATE]
proof (chain)
picking this:
E \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
obtain AA :: "'a multiset" and A :: 'a and \<sigma> :: 's where
      aa_sub: "poss AA \<subseteq># mset C \<cdot> \<rho>" and
      a_in: "Neg A \<in># mset D \<cdot> \<rho>'" and
      res_e: "ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E"
[PROOF STATE]
proof (prove)
using this:
E \<in> mset ` set (resolve_rename C D)

goal (1 subgoal):
 1. (\<And>AA A \<sigma>. \<lbrakk>poss AA \<subseteq># mset C \<cdot> \<rho>; Neg A \<in># mset D \<cdot> \<rho>'; ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<rho>'_def \<rho>_def
[PROOF STATE]
proof (prove)
using this:
E \<in> mset ` set (resolve_rename C D)

goal (1 subgoal):
 1. (\<And>AA A \<sigma>. \<lbrakk>poss AA \<subseteq># mset C \<cdot> last (renamings_apart [mset D, mset C]); Neg A \<in># mset D \<cdot> hd (renamings_apart [mset D, mset C]); ord_resolve S [mset C \<cdot> last (renamings_apart [mset D, mset C])] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<in> mset ` set (resolve_rename C D) \<Longrightarrow> \<exists>AA A \<sigma>. poss AA \<subseteq># mset C \<cdot> last (renamings_apart [mset D, mset C]) \<and> Neg A \<in># mset D \<cdot> hd (renamings_apart [mset D, mset C]) \<and> ord_resolve S [mset C \<cdot> last (renamings_apart [mset D, mset C])] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E
[PROOF STEP]
using e_in
[PROOF STATE]
proof (prove)
using this:
E \<in> mset ` set (resolve_rename C D)

goal (1 subgoal):
 1. E \<in> mset ` set (resolve_rename C D) \<Longrightarrow> \<exists>AA A \<sigma>. poss AA \<subseteq># mset C \<cdot> last (renamings_apart [mset D, mset C]) \<and> Neg A \<in># mset D \<cdot> hd (renamings_apart [mset D, mset C]) \<and> ord_resolve S [mset C \<cdot> last (renamings_apart [mset D, mset C])] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E
[PROOF STEP]
unfolding resolve_rename_def Let_def resolve_eq_Bin_ord_resolve
[PROOF STATE]
proof (prove)
using this:
E \<in> Bin_ord_resolve (mset (map (\<lambda>L. L \<cdot>l last (renamings_apart [mset D, mset C])) C)) (mset (map (\<lambda>L. L \<cdot>l hd (renamings_apart [mset D, mset C])) D))

goal (1 subgoal):
 1. E \<in> Bin_ord_resolve (mset (map (\<lambda>L. L \<cdot>l last (renamings_apart [mset D, mset C])) C)) (mset (map (\<lambda>L. L \<cdot>l hd (renamings_apart [mset D, mset C])) D)) \<Longrightarrow> \<exists>AA A \<sigma>. poss AA \<subseteq># mset C \<cdot> last (renamings_apart [mset D, mset C]) \<and> Neg A \<in># mset D \<cdot> hd (renamings_apart [mset D, mset C]) \<and> ord_resolve S [mset C \<cdot> last (renamings_apart [mset D, mset C])] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA A \<sigma>. ord_resolve S [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E \<Longrightarrow> \<exists>AA. poss AA \<subseteq># mset C \<cdot> last (renamings_apart [mset D, mset C]) \<and> (\<exists>A. (\<exists>M. M \<in> set D \<and> Neg A = M \<cdot>l hd (renamings_apart [mset D, mset C])) \<and> (\<exists>\<sigma>. ord_resolve S [mset C \<cdot> last (renamings_apart [mset D, mset C])] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E))
[PROOF STEP]
apply (frule ord_resolve_one_side_prem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA A \<sigma>. \<lbrakk>ord_resolve S [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E; length [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] = 1 \<and> length [AA] = 1 \<and> length [A] = 1\<rbrakk> \<Longrightarrow> \<exists>AA. poss AA \<subseteq># mset C \<cdot> last (renamings_apart [mset D, mset C]) \<and> (\<exists>A. (\<exists>M. M \<in> set D \<and> Neg A = M \<cdot>l hd (renamings_apart [mset D, mset C])) \<and> (\<exists>\<sigma>. ord_resolve S [mset C \<cdot> last (renamings_apart [mset D, mset C])] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E))
[PROOF STEP]
apply (frule ord_resolve.simps[THEN iffD1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA A \<sigma>. \<lbrakk>ord_resolve S [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E; length [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] = 1 \<and> length [AA] = 1 \<and> length [A] = 1; \<exists>CAs n Cs AAs As \<sigma>' Da. [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] = CAs \<and> {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} = Da + negs (mset As) \<and> [AA] = AAs \<and> [A] = As \<and> \<sigma> = \<sigma>' \<and> E = (\<Sum>\<^sub># (mset Cs) + Da) \<cdot> \<sigma>' \<and> length CAs = n \<and> length Cs = n \<and> length AAs = n \<and> length As = n \<and> n \<noteq> 0 \<and> (\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)) \<and> (\<forall>i<n. AAs ! i \<noteq> {#}) \<and> Some \<sigma>' = mgu (set_mset ` set (Map2.map2 add_mset As AAs)) \<and> eligible S \<sigma>' As (Da + negs (mset As)) \<and> (\<forall>i<n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>') (Cs ! i \<cdot> \<sigma>')) \<and> (\<forall>i<n. S (CAs ! i) = {#})\<rbrakk> \<Longrightarrow> \<exists>AA. poss AA \<subseteq># mset C \<cdot> last (renamings_apart [mset D, mset C]) \<and> (\<exists>A. (\<exists>M. M \<in> set D \<and> Neg A = M \<cdot>l hd (renamings_apart [mset D, mset C])) \<and> (\<exists>\<sigma>. ord_resolve S [mset C \<cdot> last (renamings_apart [mset D, mset C])] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E))
[PROOF STEP]
apply (rule_tac x = AA in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA A \<sigma>. \<lbrakk>ord_resolve S [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E; length [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] = 1 \<and> length [AA] = 1 \<and> length [A] = 1; \<exists>CAs n Cs AAs As \<sigma>' Da. [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] = CAs \<and> {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} = Da + negs (mset As) \<and> [AA] = AAs \<and> [A] = As \<and> \<sigma> = \<sigma>' \<and> E = (\<Sum>\<^sub># (mset Cs) + Da) \<cdot> \<sigma>' \<and> length CAs = n \<and> length Cs = n \<and> length AAs = n \<and> length As = n \<and> n \<noteq> 0 \<and> (\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)) \<and> (\<forall>i<n. AAs ! i \<noteq> {#}) \<and> Some \<sigma>' = mgu (set_mset ` set (Map2.map2 add_mset As AAs)) \<and> eligible S \<sigma>' As (Da + negs (mset As)) \<and> (\<forall>i<n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>') (Cs ! i \<cdot> \<sigma>')) \<and> (\<forall>i<n. S (CAs ! i) = {#})\<rbrakk> \<Longrightarrow> poss AA \<subseteq># mset C \<cdot> last (renamings_apart [mset D, mset C]) \<and> (\<exists>A. (\<exists>M. M \<in> set D \<and> Neg A = M \<cdot>l hd (renamings_apart [mset D, mset C])) \<and> (\<exists>\<sigma>. ord_resolve S [mset C \<cdot> last (renamings_apart [mset D, mset C])] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E))
[PROOF STEP]
apply (clarsimp simp: subst_cls_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA A \<sigma> Cs Da. \<lbrakk>ord_resolve S [Cs ! 0 + poss AA] (add_mset (Neg A) Da) [AA] [A] \<sigma> ({#A \<cdot>l \<sigma>. A \<in># sum_list Cs#} + {#A \<cdot>l \<sigma>. A \<in># Da#}); {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} = add_mset (Neg A) Da; E = {#A \<cdot>l \<sigma>. A \<in># sum_list Cs#} + {#A \<cdot>l \<sigma>. A \<in># Da#}; length Cs = Suc 0; {#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#} = Cs ! 0 + poss AA; AA \<noteq> {#}; Some \<sigma> = mgu {insert A (set_mset AA)}; eligible S \<sigma> [A] (add_mset (Neg A) Da); strictly_maximal_wrt (A \<cdot>a \<sigma>) {#x \<cdot>l \<sigma>. x \<in># Cs ! 0#}; S (Cs ! 0 + poss AA) = {#}\<rbrakk> \<Longrightarrow> \<exists>Aa. (\<exists>M. M \<in> set D \<and> Neg Aa = M \<cdot>l hd (renamings_apart [mset D, mset C])) \<and> (\<exists>\<sigma>'. ord_resolve S [Cs ! 0 + poss AA] (add_mset (Neg A) Da) [AA] [Aa] \<sigma>' ({#A \<cdot>l \<sigma>. A \<in># sum_list Cs#} + {#A \<cdot>l \<sigma>. A \<in># Da#}))
[PROOF STEP]
apply (rule_tac x = A in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA A \<sigma> Cs Da. \<lbrakk>ord_resolve S [Cs ! 0 + poss AA] (add_mset (Neg A) Da) [AA] [A] \<sigma> ({#A \<cdot>l \<sigma>. A \<in># sum_list Cs#} + {#A \<cdot>l \<sigma>. A \<in># Da#}); {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} = add_mset (Neg A) Da; E = {#A \<cdot>l \<sigma>. A \<in># sum_list Cs#} + {#A \<cdot>l \<sigma>. A \<in># Da#}; length Cs = Suc 0; {#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#} = Cs ! 0 + poss AA; AA \<noteq> {#}; Some \<sigma> = mgu {insert A (set_mset AA)}; eligible S \<sigma> [A] (add_mset (Neg A) Da); strictly_maximal_wrt (A \<cdot>a \<sigma>) {#x \<cdot>l \<sigma>. x \<in># Cs ! 0#}; S (Cs ! 0 + poss AA) = {#}\<rbrakk> \<Longrightarrow> (\<exists>M. M \<in> set D \<and> Neg A = M \<cdot>l hd (renamings_apart [mset D, mset C])) \<and> (\<exists>\<sigma>'. ord_resolve S [Cs ! 0 + poss AA] (add_mset (Neg A) Da) [AA] [A] \<sigma>' ({#A \<cdot>l \<sigma>. A \<in># sum_list Cs#} + {#A \<cdot>l \<sigma>. A \<in># Da#}))
[PROOF STEP]
by (metis (full_types) Melem_subst_cls set_mset_mset subst_cls_def union_single_eq_member)
[PROOF STATE]
proof (state)
this:
poss AA \<subseteq># mset C \<cdot> \<rho>
Neg A \<in># mset D \<cdot> \<rho>'
ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E

goal (2 subgoals):
 1. \<And>x. x \<in> mset ` set (resolve_rename C D) \<Longrightarrow> x \<in> Bin_ord_resolve_rename (mset C) (mset D)
 2. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
obtain AA0 :: "'a multiset" where
      aa0_sub: "poss AA0 \<subseteq># mset C" and
      aa: "AA = AA0 \<cdot>am \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>AA0. \<lbrakk>poss AA0 \<subseteq># mset C; AA = AA0 \<cdot>am \<rho>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using aa_sub
[PROOF STATE]
proof (prove)
using this:
poss AA \<subseteq># mset C \<cdot> \<rho>

goal (1 subgoal):
 1. (\<And>AA0. \<lbrakk>poss AA0 \<subseteq># mset C; AA = AA0 \<cdot>am \<rho>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poss AA \<subseteq># mset C \<cdot> \<rho> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># mset C \<and> AA = AA0 \<cdot>am \<rho>
[PROOF STEP]
apply (rule ord_resolve.cases[OF res_e])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>CAs n Cs AAs As \<sigma>' Da. \<lbrakk>poss AA \<subseteq># mset C \<cdot> \<rho>; [mset C \<cdot> \<rho>] = CAs; {#L \<cdot>l \<rho>'. L \<in># mset D#} = Da + negs (mset As); [AA] = AAs; [A] = As; \<sigma> = \<sigma>'; E = (\<Sum>\<^sub># (mset Cs) + Da) \<cdot> \<sigma>'; length CAs = n; length Cs = n; length AAs = n; length As = n; n \<noteq> 0; \<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i); \<forall>i<n. AAs ! i \<noteq> {#}; Some \<sigma>' = mgu (set_mset ` set (Map2.map2 add_mset As AAs)); eligible S \<sigma>' As (Da + negs (mset As)); \<forall>i<n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>') (Cs ! i \<cdot> \<sigma>'); \<forall>i<n. S (CAs ! i) = {#}\<rbrakk> \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># mset C \<and> AA = AA0 \<cdot>am \<rho>
[PROOF STEP]
by (rule poss_subset_filterD[OF aa_sub[unfolded subst_cls_def]])
[PROOF STATE]
proof (state)
this:
poss AA0 \<subseteq># mset C
AA = AA0 \<cdot>am \<rho>

goal (2 subgoals):
 1. \<And>x. x \<in> mset ` set (resolve_rename C D) \<Longrightarrow> x \<in> Bin_ord_resolve_rename (mset C) (mset D)
 2. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
obtain A0 :: 'a where
      a0_in: "Neg A0 \<in> set D" and
      a: "A = A0 \<cdot>a \<rho>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A0. \<lbrakk>Neg A0 \<in> set D; A = A0 \<cdot>a \<rho>'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A0. Neg A0 \<in> set D \<and> A = A0 \<cdot>a \<rho>'
[PROOF STEP]
apply (rule ord_resolve.cases[OF res_e])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>CAs n Cs AAs As \<sigma>' Da. \<lbrakk>[mset C \<cdot> \<rho>] = CAs; {#L \<cdot>l \<rho>'. L \<in># mset D#} = Da + negs (mset As); [AA] = AAs; [A] = As; \<sigma> = \<sigma>'; E = (\<Sum>\<^sub># (mset Cs) + Da) \<cdot> \<sigma>'; length CAs = n; length Cs = n; length AAs = n; length As = n; n \<noteq> 0; \<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i); \<forall>i<n. AAs ! i \<noteq> {#}; Some \<sigma>' = mgu (set_mset ` set (Map2.map2 add_mset As AAs)); eligible S \<sigma>' As (Da + negs (mset As)); \<forall>i<n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>') (Cs ! i \<cdot> \<sigma>'); \<forall>i<n. S (CAs ! i) = {#}\<rbrakk> \<Longrightarrow> \<exists>A0. Neg A0 \<in> set D \<and> A = A0 \<cdot>a \<rho>'
[PROOF STEP]
using neg_in_filterD[OF a_in[unfolded subst_cls_def]]
[PROOF STATE]
proof (prove)
using this:
\<exists>A0. Neg A0 \<in># mset D \<and> A = A0 \<cdot>a \<rho>'

goal (1 subgoal):
 1. \<And>CAs n Cs AAs As \<sigma>' Da. \<lbrakk>[mset C \<cdot> \<rho>] = CAs; {#L \<cdot>l \<rho>'. L \<in># mset D#} = Da + negs (mset As); [AA] = AAs; [A] = As; \<sigma> = \<sigma>'; E = (\<Sum>\<^sub># (mset Cs) + Da) \<cdot> \<sigma>'; length CAs = n; length Cs = n; length AAs = n; length As = n; n \<noteq> 0; \<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i); \<forall>i<n. AAs ! i \<noteq> {#}; Some \<sigma>' = mgu (set_mset ` set (Map2.map2 add_mset As AAs)); eligible S \<sigma>' As (Da + negs (mset As)); \<forall>i<n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>') (Cs ! i \<cdot> \<sigma>'); \<forall>i<n. S (CAs ! i) = {#}\<rbrakk> \<Longrightarrow> \<exists>A0. Neg A0 \<in> set D \<and> A = A0 \<cdot>a \<rho>'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Neg A0 \<in> set D
A = A0 \<cdot>a \<rho>'

goal (2 subgoals):
 1. \<And>x. x \<in> mset ` set (resolve_rename C D) \<Longrightarrow> x \<in> Bin_ord_resolve_rename (mset C) (mset D)
 2. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
show "E \<in> Bin_ord_resolve_rename (mset C) (mset D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<in> Bin_ord_resolve_rename (mset C) (mset D)
[PROOF STEP]
unfolding ord_resolve_rename.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<in> {E. \<exists>AA A \<sigma> CAs n AAs As DA \<rho> \<rho>s \<sigma>' Ea. [mset C] = CAs \<and> mset D = DA \<and> [AA] = AAs \<and> [A] = As \<and> \<sigma> = \<sigma>' \<and> E = Ea \<and> length CAs = n \<and> length AAs = n \<and> length As = n \<and> (\<forall>i<n. poss (AAs ! i) \<subseteq># CAs ! i) \<and> negs (mset As) \<subseteq># DA \<and> \<rho> = hd (renamings_apart (DA # CAs)) \<and> \<rho>s = tl (renamings_apart (DA # CAs)) \<and> ord_resolve S (CAs \<cdot>\<cdot>cl \<rho>s) (DA \<cdot> \<rho>) (AAs \<cdot>\<cdot>aml \<rho>s) (As \<cdot>al \<rho>) \<sigma>' Ea}
[PROOF STEP]
using res_e
[PROOF STATE]
proof (prove)
using this:
ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E

goal (1 subgoal):
 1. E \<in> {E. \<exists>AA A \<sigma> CAs n AAs As DA \<rho> \<rho>s \<sigma>' Ea. [mset C] = CAs \<and> mset D = DA \<and> [AA] = AAs \<and> [A] = As \<and> \<sigma> = \<sigma>' \<and> E = Ea \<and> length CAs = n \<and> length AAs = n \<and> length As = n \<and> (\<forall>i<n. poss (AAs ! i) \<subseteq># CAs ! i) \<and> negs (mset As) \<subseteq># DA \<and> \<rho> = hd (renamings_apart (DA # CAs)) \<and> \<rho>s = tl (renamings_apart (DA # CAs)) \<and> ord_resolve S (CAs \<cdot>\<cdot>cl \<rho>s) (DA \<cdot> \<rho>) (AAs \<cdot>\<cdot>aml \<rho>s) (As \<cdot>al \<rho>) \<sigma>' Ea}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E \<Longrightarrow> \<exists>AA. poss AA \<subseteq># mset C \<and> (\<exists>A. Neg A \<in> set D \<and> (\<exists>\<sigma>. ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E))
[PROOF STEP]
apply (rule_tac x = AA0 in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E \<Longrightarrow> poss AA0 \<subseteq># mset C \<and> (\<exists>A. Neg A \<in> set D \<and> (\<exists>\<sigma>. ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA0] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E))
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E \<Longrightarrow> poss AA0 \<subseteq># mset C
 2. ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E \<Longrightarrow> \<exists>A. Neg A \<in> set D \<and> (\<exists>\<sigma>. ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA0] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E)
[PROOF STEP]
apply (rule aa0_sub)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E \<Longrightarrow> \<exists>A. Neg A \<in> set D \<and> (\<exists>\<sigma>. ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA0] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E)
[PROOF STEP]
apply (rule_tac x = A0 in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E \<Longrightarrow> Neg A0 \<in> set D \<and> (\<exists>\<sigma>. ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA0] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A0 \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E)
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E \<Longrightarrow> Neg A0 \<in> set D
 2. ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E \<Longrightarrow> \<exists>\<sigma>. ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA0] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A0 \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E
[PROOF STEP]
apply (rule a0_in)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E \<Longrightarrow> \<exists>\<sigma>. ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA0] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A0 \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E
[PROOF STEP]
apply (rule_tac x = \<sigma> in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E \<Longrightarrow> ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA0] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A0 \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E
[PROOF STEP]
unfolding aa a \<rho>'_def[symmetric] \<rho>_def[symmetric] tl_\<rho>s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA0 \<cdot>am \<rho>] [A0 \<cdot>a \<rho>'] \<sigma> E \<Longrightarrow> ord_resolve S ([mset C] \<cdot>\<cdot>cl [\<rho>]) (mset D \<cdot> \<rho>') ([AA0] \<cdot>\<cdot>aml [\<rho>]) [A0 \<cdot>a \<rho>'] \<sigma> E
[PROOF STEP]
by (simp add: subst_cls_def)
[PROOF STATE]
proof (state)
this:
E \<in> Bin_ord_resolve_rename (mset C) (mset D)

goal (1 subgoal):
 1. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?E2 \<in> mset ` set (resolve_rename C D) \<Longrightarrow> ?E2 \<in> Bin_ord_resolve_rename (mset C) (mset D)

goal (1 subgoal):
 1. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?E2 \<in> mset ` set (resolve_rename C D) \<Longrightarrow> ?E2 \<in> Bin_ord_resolve_rename (mset C) (mset D)

goal (1 subgoal):
 1. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
fix E
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
assume e_in: "E \<in> Bin_ord_resolve_rename (mset C) (mset D)"
[PROOF STATE]
proof (state)
this:
E \<in> Bin_ord_resolve_rename (mset C) (mset D)

goal (1 subgoal):
 1. \<And>x. x \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> x \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
show "E \<in> mset ` set (resolve_rename C D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
using e_in
[PROOF STATE]
proof (prove)
using this:
E \<in> Bin_ord_resolve_rename (mset C) (mset D)

goal (1 subgoal):
 1. E \<in> mset ` set (resolve_rename C D)
[PROOF STEP]
unfolding resolve_rename_def Let_def resolve_eq_Bin_ord_resolve ord_resolve_rename.simps
[PROOF STATE]
proof (prove)
using this:
E \<in> {E. \<exists>AA A \<sigma> CAs n AAs As DA \<rho> \<rho>s \<sigma>' Ea. [mset C] = CAs \<and> mset D = DA \<and> [AA] = AAs \<and> [A] = As \<and> \<sigma> = \<sigma>' \<and> E = Ea \<and> length CAs = n \<and> length AAs = n \<and> length As = n \<and> (\<forall>i<n. poss (AAs ! i) \<subseteq># CAs ! i) \<and> negs (mset As) \<subseteq># DA \<and> \<rho> = hd (renamings_apart (DA # CAs)) \<and> \<rho>s = tl (renamings_apart (DA # CAs)) \<and> ord_resolve S (CAs \<cdot>\<cdot>cl \<rho>s) (DA \<cdot> \<rho>) (AAs \<cdot>\<cdot>aml \<rho>s) (As \<cdot>al \<rho>) \<sigma>' Ea}

goal (1 subgoal):
 1. E \<in> Bin_ord_resolve (mset (map (\<lambda>L. L \<cdot>l last (renamings_apart [mset D, mset C])) C)) (mset (map (\<lambda>L. L \<cdot>l hd (renamings_apart [mset D, mset C])) D))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA A \<sigma>. \<lbrakk>poss AA \<subseteq># mset C; Neg A \<in> set D; ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E\<rbrakk> \<Longrightarrow> \<exists>AA A \<sigma>. ord_resolve S [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA] [A] \<sigma> E
[PROOF STEP]
apply (rule_tac x = "AA \<cdot>am \<rho>" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA A \<sigma>. \<lbrakk>poss AA \<subseteq># mset C; Neg A \<in> set D; ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E\<rbrakk> \<Longrightarrow> \<exists>A \<sigma>. ord_resolve S [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA \<cdot>am \<rho>] [A] \<sigma> E
[PROOF STEP]
apply (rule_tac x = "A \<cdot>a \<rho>'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA A \<sigma>. \<lbrakk>poss AA \<subseteq># mset C; Neg A \<in> set D; ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E\<rbrakk> \<Longrightarrow> \<exists>\<sigma>. ord_resolve S [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA \<cdot>am \<rho>] [A \<cdot>a \<rho>'] \<sigma> E
[PROOF STEP]
apply (rule_tac x = \<sigma> in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA A \<sigma>. \<lbrakk>poss AA \<subseteq># mset C; Neg A \<in> set D; ord_resolve S ([mset C] \<cdot>\<cdot>cl tl (renamings_apart [mset D, mset C])) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA] \<cdot>\<cdot>aml tl (renamings_apart [mset D, mset C])) [A \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E\<rbrakk> \<Longrightarrow> ord_resolve S [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA \<cdot>am \<rho>] [A \<cdot>a \<rho>'] \<sigma> E
[PROOF STEP]
unfolding tl_\<rho>s \<rho>'_def \<rho>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA A \<sigma>. \<lbrakk>poss AA \<subseteq># mset C; Neg A \<in> set D; ord_resolve S ([mset C] \<cdot>\<cdot>cl [last (renamings_apart [mset D, mset C])]) (mset D \<cdot> hd (renamings_apart [mset D, mset C])) ([AA] \<cdot>\<cdot>aml [last (renamings_apart [mset D, mset C])]) [A \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E\<rbrakk> \<Longrightarrow> ord_resolve S [{#L \<cdot>l last (renamings_apart [mset D, mset C]). L \<in># mset C#}] {#L \<cdot>l hd (renamings_apart [mset D, mset C]). L \<in># mset D#} [AA \<cdot>am last (renamings_apart [mset D, mset C])] [A \<cdot>a hd (renamings_apart [mset D, mset C])] \<sigma> E
[PROOF STEP]
by (simp add: subst_cls_def subst_cls_lists_def)
[PROOF STATE]
proof (state)
this:
E \<in> mset ` set (resolve_rename C D)

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?E2 \<in> Bin_ord_resolve_rename (mset C) (mset D) \<Longrightarrow> ?E2 \<in> mset ` set (resolve_rename C D)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bin_ord_FO_\<Gamma>_def:
  "ord_FO_\<Gamma> S = {Infer {#CA#} DA E | CA DA AA A \<sigma> E. ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_FO_\<Gamma> S = {uu_. \<exists>CA DA AA A \<sigma> E. uu_ = Infer {#CA#} DA E \<and> ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E}
[PROOF STEP]
unfolding ord_FO_\<Gamma>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>CAs DA AAs As \<sigma> E. uu_ = Infer (mset CAs) DA E \<and> ord_resolve_rename S CAs DA AAs As \<sigma> E} = {uu_. \<exists>CA DA AA A \<sigma> E. uu_ = Infer {#CA#} DA E \<and> ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E}
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {uu_. \<exists>CAs DA AAs As \<sigma> E. uu_ = Infer (mset CAs) DA E \<and> ord_resolve_rename S CAs DA AAs As \<sigma> E} \<subseteq> {uu_. \<exists>CA DA AA A \<sigma> E. uu_ = Infer {#CA#} DA E \<and> ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E}
 2. {uu_. \<exists>CA DA AA A \<sigma> E. uu_ = Infer {#CA#} DA E \<and> ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E} \<subseteq> {uu_. \<exists>CAs DA AAs As \<sigma> E. uu_ = Infer (mset CAs) DA E \<and> ord_resolve_rename S CAs DA AAs As \<sigma> E}
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x CAs DA AAs As \<sigma> E. ord_resolve_rename S CAs DA AAs As \<sigma> E \<Longrightarrow> \<exists>CA DAa AA A \<sigma> Ea. Infer (mset CAs) DA E = Infer {#CA#} DAa Ea \<and> ord_resolve_rename S [CA] DAa [AA] [A] \<sigma> Ea
 2. {uu_. \<exists>CA DA AA A \<sigma> E. uu_ = Infer {#CA#} DA E \<and> ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E} \<subseteq> {uu_. \<exists>CAs DA AAs As \<sigma> E. uu_ = Infer (mset CAs) DA E \<and> ord_resolve_rename S CAs DA AAs As \<sigma> E}
[PROOF STEP]
apply (frule ord_resolve_rename_one_side_prem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x CAs DA AAs As \<sigma> E. \<lbrakk>ord_resolve_rename S CAs DA AAs As \<sigma> E; length CAs = 1 \<and> length AAs = 1 \<and> length As = 1\<rbrakk> \<Longrightarrow> \<exists>CA DAa AA A \<sigma> Ea. Infer (mset CAs) DA E = Infer {#CA#} DAa Ea \<and> ord_resolve_rename S [CA] DAa [AA] [A] \<sigma> Ea
 2. {uu_. \<exists>CA DA AA A \<sigma> E. uu_ = Infer {#CA#} DA E \<and> ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E} \<subseteq> {uu_. \<exists>CAs DA AAs As \<sigma> E. uu_ = Infer (mset CAs) DA E \<and> ord_resolve_rename S CAs DA AAs As \<sigma> E}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>CAs DA AAs As \<sigma> E. \<lbrakk>ord_resolve_rename S CAs DA AAs As \<sigma> E; length CAs = Suc 0 \<and> length AAs = Suc 0 \<and> length As = Suc 0\<rbrakk> \<Longrightarrow> \<exists>CA. CAs = [CA] \<and> (\<exists>AA A \<sigma>. ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E)
 2. {uu_. \<exists>CA DA AA A \<sigma> E. uu_ = Infer {#CA#} DA E \<and> ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E} \<subseteq> {uu_. \<exists>CAs DA AAs As \<sigma> E. uu_ = Infer (mset CAs) DA E \<and> ord_resolve_rename S CAs DA AAs As \<sigma> E}
[PROOF STEP]
apply (metis Suc_length_conv length_0_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>CA DA AA A \<sigma> E. uu_ = Infer {#CA#} DA E \<and> ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E} \<subseteq> {uu_. \<exists>CAs DA AAs As \<sigma> E. uu_ = Infer (mset CAs) DA E \<and> ord_resolve_rename S CAs DA AAs As \<sigma> E}
[PROOF STEP]
by blast


[STATEMENT]
lemma ord_FO_\<Gamma>_side_prem: "\<gamma> \<in> ord_FO_\<Gamma> S \<Longrightarrow> side_prems_of \<gamma> = {#THE D. D \<in># side_prems_of \<gamma>#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> \<in> ord_FO_\<Gamma> S \<Longrightarrow> side_prems_of \<gamma> = {#THE D. D \<in># side_prems_of \<gamma>#}
[PROOF STEP]
unfolding bin_ord_FO_\<Gamma>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> \<in> {uu_. \<exists>CA DA AA A \<sigma> E. uu_ = Infer {#CA#} DA E \<and> ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E} \<Longrightarrow> side_prems_of \<gamma> = {#THE D. D \<in># side_prems_of \<gamma>#}
[PROOF STEP]
by clarsimp