[STATEMENT]
lemma is_reducible_lit_remove1_Cons_iff:
  assumes "L \<in> set C'"
  shows "is_reducible_lit Ds (C @ remove1 L (M # C')) L \<longleftrightarrow>
    is_reducible_lit Ds (M # C @ remove1 L C') L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_reducible_lit Ds (C @ remove1 L (M # C')) L = is_reducible_lit Ds (M # C @ remove1 L C') L
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
L \<in> set C'

goal (1 subgoal):
 1. is_reducible_lit Ds (C @ remove1 L (M # C')) L = is_reducible_lit Ds (M # C @ remove1 L C') L
[PROOF STEP]
by (subst is_reducible_lit_mset_iff, auto)


[STATEMENT]
lemma reduce_mset_eq: "mset C = mset C' \<Longrightarrow> reduce Ds C E = reduce Ds C' E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset C = mset C' \<Longrightarrow> reduce Ds C E = reduce Ds C' E
[PROOF STEP]
proof (induct E arbitrary: C C')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C C'. mset C = mset C' \<Longrightarrow> reduce Ds C [] = reduce Ds C' []
 2. \<And>a E C C'. \<lbrakk>\<And>C C'. mset C = mset C' \<Longrightarrow> reduce Ds C E = reduce Ds C' E; mset C = mset C'\<rbrakk> \<Longrightarrow> reduce Ds C (a # E) = reduce Ds C' (a # E)
[PROOF STEP]
case (Cons L E)
[PROOF STATE]
proof (state)
this:
mset ?C = mset ?C' \<Longrightarrow> reduce Ds ?C E = reduce Ds ?C' E
mset C = mset C'

goal (2 subgoals):
 1. \<And>C C'. mset C = mset C' \<Longrightarrow> reduce Ds C [] = reduce Ds C' []
 2. \<And>a E C C'. \<lbrakk>\<And>C C'. mset C = mset C' \<Longrightarrow> reduce Ds C E = reduce Ds C' E; mset C = mset C'\<rbrakk> \<Longrightarrow> reduce Ds C (a # E) = reduce Ds C' (a # E)
[PROOF STEP]
note ih = this(1) and mset_eq = this(2)
[PROOF STATE]
proof (state)
this:
mset ?C = mset ?C' \<Longrightarrow> reduce Ds ?C E = reduce Ds ?C' E
mset C = mset C'

goal (2 subgoals):
 1. \<And>C C'. mset C = mset C' \<Longrightarrow> reduce Ds C [] = reduce Ds C' []
 2. \<And>a E C C'. \<lbrakk>\<And>C C'. mset C = mset C' \<Longrightarrow> reduce Ds C E = reduce Ds C' E; mset C = mset C'\<rbrakk> \<Longrightarrow> reduce Ds C (a # E) = reduce Ds C' (a # E)
[PROOF STEP]
have
    mset_lc_eq: "mset (L # C) = mset (L # C')" and
    mset_ce_eq: "mset (C @ E) = mset (C' @ E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (L # C) = mset (L # C') &&& mset (C @ E) = mset (C' @ E)
[PROOF STEP]
using mset_eq
[PROOF STATE]
proof (prove)
using this:
mset C = mset C'

goal (1 subgoal):
 1. mset (L # C) = mset (L # C') &&& mset (C @ E) = mset (C' @ E)
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
mset (L # C) = mset (L # C')
mset (C @ E) = mset (C' @ E)

goal (2 subgoals):
 1. \<And>C C'. mset C = mset C' \<Longrightarrow> reduce Ds C [] = reduce Ds C' []
 2. \<And>a E C C'. \<lbrakk>\<And>C C'. mset C = mset C' \<Longrightarrow> reduce Ds C E = reduce Ds C' E; mset C = mset C'\<rbrakk> \<Longrightarrow> reduce Ds C (a # E) = reduce Ds C' (a # E)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduce Ds C (L # E) = reduce Ds C' (L # E)
[PROOF STEP]
using ih[OF mset_eq] ih[OF mset_lc_eq]
[PROOF STATE]
proof (prove)
using this:
reduce Ds C E = reduce Ds C' E
reduce Ds (L # C) E = reduce Ds (L # C') E

goal (1 subgoal):
 1. reduce Ds C (L # E) = reduce Ds C' (L # E)
[PROOF STEP]
by (simp add: is_reducible_lit_mset_iff[OF mset_ce_eq])
[PROOF STATE]
proof (state)
this:
reduce Ds C (L # E) = reduce Ds C' (L # E)

goal (1 subgoal):
 1. \<And>C C'. mset C = mset C' \<Longrightarrow> reduce Ds C [] = reduce Ds C' []
[PROOF STEP]
qed simp


[STATEMENT]
lemma reduce_rotate[simp]: "reduce Ds (C @ [L]) E = reduce Ds (L # C) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduce Ds (C @ [L]) E = reduce Ds (L # C) E
[PROOF STEP]
by (rule reduce_mset_eq) simp


[STATEMENT]
lemma mset_reduce_subset: "mset (reduce Ds C E) \<subseteq># mset E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (reduce Ds C E) \<subseteq># mset E
[PROOF STEP]
by (induct E arbitrary: C) (auto intro: subset_mset_imp_subset_add_mset)


[STATEMENT]
lemma reduce_idem: "reduce Ds C (reduce Ds C E) = reduce Ds C E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduce Ds C (reduce Ds C E) = reduce Ds C E
[PROOF STEP]
by (induct E arbitrary: C)
    (auto intro!: mset_reduce_subset
      dest!: is_reducible_lit_mono_cls[of "C @ reduce Ds (L # C) E" "C @ E" Ds L for L E C,
        rotated])


[STATEMENT]
lemma is_reducible_lit_imp_is_reducible:
  "L \<in> set C' \<Longrightarrow> is_reducible_lit Ds (C @ remove1 L C') L \<Longrightarrow> reduce Ds C C' \<noteq> C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>L \<in> set C'; is_reducible_lit Ds (C @ remove1 L C') L\<rbrakk> \<Longrightarrow> reduce Ds C C' \<noteq> C'
[PROOF STEP]
proof (induct C' arbitrary: C)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>L \<in> set []; is_reducible_lit Ds (C @ remove1 L []) L\<rbrakk> \<Longrightarrow> reduce Ds C [] \<noteq> []
 2. \<And>a C' C. \<lbrakk>\<And>C. \<lbrakk>L \<in> set C'; is_reducible_lit Ds (C @ remove1 L C') L\<rbrakk> \<Longrightarrow> reduce Ds C C' \<noteq> C'; L \<in> set (a # C'); is_reducible_lit Ds (C @ remove1 L (a # C')) L\<rbrakk> \<Longrightarrow> reduce Ds C (a # C') \<noteq> a # C'
[PROOF STEP]
case (Cons M C')
[PROOF STATE]
proof (state)
this:
\<lbrakk>L \<in> set C'; is_reducible_lit Ds (?C @ remove1 L C') L\<rbrakk> \<Longrightarrow> reduce Ds ?C C' \<noteq> C'
L \<in> set (M # C')
is_reducible_lit Ds (C @ remove1 L (M # C')) L

goal (2 subgoals):
 1. \<And>C. \<lbrakk>L \<in> set []; is_reducible_lit Ds (C @ remove1 L []) L\<rbrakk> \<Longrightarrow> reduce Ds C [] \<noteq> []
 2. \<And>a C' C. \<lbrakk>\<And>C. \<lbrakk>L \<in> set C'; is_reducible_lit Ds (C @ remove1 L C') L\<rbrakk> \<Longrightarrow> reduce Ds C C' \<noteq> C'; L \<in> set (a # C'); is_reducible_lit Ds (C @ remove1 L (a # C')) L\<rbrakk> \<Longrightarrow> reduce Ds C (a # C') \<noteq> a # C'
[PROOF STEP]
note ih = this(1) and l_in = this(2) and l_red = this(3)
[PROOF STATE]
proof (state)
this:
\<lbrakk>L \<in> set C'; is_reducible_lit Ds (?C @ remove1 L C') L\<rbrakk> \<Longrightarrow> reduce Ds ?C C' \<noteq> C'
L \<in> set (M # C')
is_reducible_lit Ds (C @ remove1 L (M # C')) L

goal (2 subgoals):
 1. \<And>C. \<lbrakk>L \<in> set []; is_reducible_lit Ds (C @ remove1 L []) L\<rbrakk> \<Longrightarrow> reduce Ds C [] \<noteq> []
 2. \<And>a C' C. \<lbrakk>\<And>C. \<lbrakk>L \<in> set C'; is_reducible_lit Ds (C @ remove1 L C') L\<rbrakk> \<Longrightarrow> reduce Ds C C' \<noteq> C'; L \<in> set (a # C'); is_reducible_lit Ds (C @ remove1 L (a # C')) L\<rbrakk> \<Longrightarrow> reduce Ds C (a # C') \<noteq> a # C'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduce Ds C (M # C') \<noteq> M # C'
[PROOF STEP]
proof (cases "is_reducible_lit Ds (C @ C') M")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_reducible_lit Ds (C @ C') M \<Longrightarrow> reduce Ds C (M # C') \<noteq> M # C'
 2. \<not> is_reducible_lit Ds (C @ C') M \<Longrightarrow> reduce Ds C (M # C') \<noteq> M # C'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_reducible_lit Ds (C @ C') M

goal (2 subgoals):
 1. is_reducible_lit Ds (C @ C') M \<Longrightarrow> reduce Ds C (M # C') \<noteq> M # C'
 2. \<not> is_reducible_lit Ds (C @ C') M \<Longrightarrow> reduce Ds C (M # C') \<noteq> M # C'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_reducible_lit Ds (C @ C') M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_reducible_lit Ds (C @ C') M

goal (1 subgoal):
 1. reduce Ds C (M # C') \<noteq> M # C'
[PROOF STEP]
by simp (metis mset.simps(2) mset_reduce_subset multi_self_add_other_not_self
          subset_mset.eq_iff subset_mset_imp_subset_add_mset)
[PROOF STATE]
proof (state)
this:
reduce Ds C (M # C') \<noteq> M # C'

goal (1 subgoal):
 1. \<not> is_reducible_lit Ds (C @ C') M \<Longrightarrow> reduce Ds C (M # C') \<noteq> M # C'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_reducible_lit Ds (C @ C') M \<Longrightarrow> reduce Ds C (M # C') \<noteq> M # C'
[PROOF STEP]
case m_irred: False
[PROOF STATE]
proof (state)
this:
\<not> is_reducible_lit Ds (C @ C') M

goal (1 subgoal):
 1. \<not> is_reducible_lit Ds (C @ C') M \<Longrightarrow> reduce Ds C (M # C') \<noteq> M # C'
[PROOF STEP]
have
      "L \<in> set C'" and
      "is_reducible_lit Ds (M # C @ remove1 L C') L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<in> set C' &&& is_reducible_lit Ds (M # C @ remove1 L C') L
[PROOF STEP]
using l_in l_red m_irred is_reducible_lit_remove1_Cons_iff
[PROOF STATE]
proof (prove)
using this:
L \<in> set (M # C')
is_reducible_lit Ds (C @ remove1 L (M # C')) L
\<not> is_reducible_lit Ds (C @ C') M
?L \<in> set ?C' \<Longrightarrow> is_reducible_lit ?Ds (?C @ remove1 ?L (?M # ?C')) ?L = is_reducible_lit ?Ds (?M # ?C @ remove1 ?L ?C') ?L

goal (1 subgoal):
 1. L \<in> set C' &&& is_reducible_lit Ds (M # C @ remove1 L C') L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<in> set C'
is_reducible_lit Ds (M # C @ remove1 L C') L

goal (1 subgoal):
 1. \<not> is_reducible_lit Ds (C @ C') M \<Longrightarrow> reduce Ds C (M # C') \<noteq> M # C'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L \<in> set C'
is_reducible_lit Ds (M # C @ remove1 L C') L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L \<in> set C'
is_reducible_lit Ds (M # C @ remove1 L C') L

goal (1 subgoal):
 1. reduce Ds C (M # C') \<noteq> M # C'
[PROOF STEP]
by (simp add: ih[of "M # C"] m_irred)
[PROOF STATE]
proof (state)
this:
reduce Ds C (M # C') \<noteq> M # C'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
reduce Ds C (M # C') \<noteq> M # C'

goal (1 subgoal):
 1. \<And>C. \<lbrakk>L \<in> set []; is_reducible_lit Ds (C @ remove1 L []) L\<rbrakk> \<Longrightarrow> reduce Ds C [] \<noteq> []
[PROOF STEP]
qed simp


[STATEMENT]
lemma is_reducible_imp_is_reducible_lit:
  "reduce Ds C C' \<noteq> C' \<Longrightarrow> \<exists>L \<in> set C'. is_reducible_lit Ds (C @ remove1 L C') L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduce Ds C C' \<noteq> C' \<Longrightarrow> \<exists>L\<in>set C'. is_reducible_lit Ds (C @ remove1 L C') L
[PROOF STEP]
proof (induct C' arbitrary: C)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C. reduce Ds C [] \<noteq> [] \<Longrightarrow> \<exists>L\<in>set []. is_reducible_lit Ds (C @ remove1 L []) L
 2. \<And>a C' C. \<lbrakk>\<And>C. reduce Ds C C' \<noteq> C' \<Longrightarrow> \<exists>L\<in>set C'. is_reducible_lit Ds (C @ remove1 L C') L; reduce Ds C (a # C') \<noteq> a # C'\<rbrakk> \<Longrightarrow> \<exists>L\<in>set (a # C'). is_reducible_lit Ds (C @ remove1 L (a # C')) L
[PROOF STEP]
case (Cons M C')
[PROOF STATE]
proof (state)
this:
reduce Ds ?C C' \<noteq> C' \<Longrightarrow> \<exists>L\<in>set C'. is_reducible_lit Ds (?C @ remove1 L C') L
reduce Ds C (M # C') \<noteq> M # C'

goal (2 subgoals):
 1. \<And>C. reduce Ds C [] \<noteq> [] \<Longrightarrow> \<exists>L\<in>set []. is_reducible_lit Ds (C @ remove1 L []) L
 2. \<And>a C' C. \<lbrakk>\<And>C. reduce Ds C C' \<noteq> C' \<Longrightarrow> \<exists>L\<in>set C'. is_reducible_lit Ds (C @ remove1 L C') L; reduce Ds C (a # C') \<noteq> a # C'\<rbrakk> \<Longrightarrow> \<exists>L\<in>set (a # C'). is_reducible_lit Ds (C @ remove1 L (a # C')) L
[PROOF STEP]
note ih = this(1) and mc'_red = this(2)
[PROOF STATE]
proof (state)
this:
reduce Ds ?C C' \<noteq> C' \<Longrightarrow> \<exists>L\<in>set C'. is_reducible_lit Ds (?C @ remove1 L C') L
reduce Ds C (M # C') \<noteq> M # C'

goal (2 subgoals):
 1. \<And>C. reduce Ds C [] \<noteq> [] \<Longrightarrow> \<exists>L\<in>set []. is_reducible_lit Ds (C @ remove1 L []) L
 2. \<And>a C' C. \<lbrakk>\<And>C. reduce Ds C C' \<noteq> C' \<Longrightarrow> \<exists>L\<in>set C'. is_reducible_lit Ds (C @ remove1 L C') L; reduce Ds C (a # C') \<noteq> a # C'\<rbrakk> \<Longrightarrow> \<exists>L\<in>set (a # C'). is_reducible_lit Ds (C @ remove1 L (a # C')) L
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>L\<in>set (M # C'). is_reducible_lit Ds (C @ remove1 L (M # C')) L
[PROOF STEP]
proof (cases "is_reducible_lit Ds (C @ C') M")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_reducible_lit Ds (C @ C') M \<Longrightarrow> \<exists>L\<in>set (M # C'). is_reducible_lit Ds (C @ remove1 L (M # C')) L
 2. \<not> is_reducible_lit Ds (C @ C') M \<Longrightarrow> \<exists>L\<in>set (M # C'). is_reducible_lit Ds (C @ remove1 L (M # C')) L
[PROOF STEP]
case m_irred: False
[PROOF STATE]
proof (state)
this:
\<not> is_reducible_lit Ds (C @ C') M

goal (2 subgoals):
 1. is_reducible_lit Ds (C @ C') M \<Longrightarrow> \<exists>L\<in>set (M # C'). is_reducible_lit Ds (C @ remove1 L (M # C')) L
 2. \<not> is_reducible_lit Ds (C @ C') M \<Longrightarrow> \<exists>L\<in>set (M # C'). is_reducible_lit Ds (C @ remove1 L (M # C')) L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>L\<in>set (M # C'). is_reducible_lit Ds (C @ remove1 L (M # C')) L
[PROOF STEP]
using ih[of "M # C"] mc'_red[simplified, simplified m_irred, simplified] m_irred
        is_reducible_lit_remove1_Cons_iff
[PROOF STATE]
proof (prove)
using this:
reduce Ds (M # C) C' \<noteq> C' \<Longrightarrow> \<exists>L\<in>set C'. is_reducible_lit Ds ((M # C) @ remove1 L C') L
reduce Ds (M # C) C' \<noteq> C'
\<not> is_reducible_lit Ds (C @ C') M
?L \<in> set ?C' \<Longrightarrow> is_reducible_lit ?Ds (?C @ remove1 ?L (?M # ?C')) ?L = is_reducible_lit ?Ds (?M # ?C @ remove1 ?L ?C') ?L

goal (1 subgoal):
 1. \<exists>L\<in>set (M # C'). is_reducible_lit Ds (C @ remove1 L (M # C')) L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>L\<in>set (M # C'). is_reducible_lit Ds (C @ remove1 L (M # C')) L

goal (1 subgoal):
 1. is_reducible_lit Ds (C @ C') M \<Longrightarrow> \<exists>L\<in>set (M # C'). is_reducible_lit Ds (C @ remove1 L (M # C')) L
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<exists>L\<in>set (M # C'). is_reducible_lit Ds (C @ remove1 L (M # C')) L

goal (1 subgoal):
 1. \<And>C. reduce Ds C [] \<noteq> [] \<Longrightarrow> \<exists>L\<in>set []. is_reducible_lit Ds (C @ remove1 L []) L
[PROOF STEP]
qed simp


[STATEMENT]
lemma is_irreducible_iff_nexists_is_reducible_lit:
  "reduce Ds C C' = C' \<longleftrightarrow> \<not> (\<exists>L \<in> set C'. is_reducible_lit Ds (C @ remove1 L C') L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (reduce Ds C C' = C') = (\<not> (\<exists>L\<in>set C'. is_reducible_lit Ds (C @ remove1 L C') L))
[PROOF STEP]
using is_reducible_imp_is_reducible_lit is_reducible_lit_imp_is_reducible
[PROOF STATE]
proof (prove)
using this:
reduce ?Ds ?C ?C' \<noteq> ?C' \<Longrightarrow> \<exists>L\<in>set ?C'. is_reducible_lit ?Ds (?C @ remove1 L ?C') L
\<lbrakk>?L \<in> set ?C'; is_reducible_lit ?Ds (?C @ remove1 ?L ?C') ?L\<rbrakk> \<Longrightarrow> reduce ?Ds ?C ?C' \<noteq> ?C'

goal (1 subgoal):
 1. (reduce Ds C C' = C') = (\<not> (\<exists>L\<in>set C'. is_reducible_lit Ds (C @ remove1 L C') L))
[PROOF STEP]
by blast


[STATEMENT]
lemma is_irreducible_mset_iff: "mset E = mset E' \<Longrightarrow> reduce Ds C E = E \<longleftrightarrow> reduce Ds C E' = E'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset E = mset E' \<Longrightarrow> (reduce Ds C E = E) = (reduce Ds C E' = E')
[PROOF STEP]
unfolding is_irreducible_iff_nexists_is_reducible_lit
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset E = mset E' \<Longrightarrow> (\<not> (\<exists>L\<in>set E. is_reducible_lit Ds (C @ remove1 L E) L)) = (\<not> (\<exists>L\<in>set E'. is_reducible_lit Ds (C @ remove1 L E') L))
[PROOF STEP]
by (metis (full_types) is_reducible_lit_mset_iff mset_remove1 set_mset_mset union_code)


[STATEMENT]
lemma select_min_weight_clause_min_weight:
  assumes "Ci = select_min_weight_clause P0 P"
  shows "weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Ci = select_min_weight_clause P0 P

goal (1 subgoal):
 1. weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P))
[PROOF STEP]
proof (induct P arbitrary: P0 Ci)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P0 Ci. Ci = select_min_weight_clause P0 [] \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set [P0])
 2. \<And>a P P0 Ci. \<lbrakk>\<And>P0 Ci. Ci = select_min_weight_clause P0 P \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P)); Ci = select_min_weight_clause P0 (a # P)\<rbrakk> \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # a # P))
[PROOF STEP]
case (Cons P1 P)
[PROOF STATE]
proof (state)
this:
?Ci = select_min_weight_clause ?P0.0 P \<Longrightarrow> weight (apfst mset ?Ci) = Min ((weight \<circ> apfst mset) ` set (?P0.0 # P))
Ci = select_min_weight_clause P0 (P1 # P)

goal (2 subgoals):
 1. \<And>P0 Ci. Ci = select_min_weight_clause P0 [] \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set [P0])
 2. \<And>a P P0 Ci. \<lbrakk>\<And>P0 Ci. Ci = select_min_weight_clause P0 P \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P)); Ci = select_min_weight_clause P0 (a # P)\<rbrakk> \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # a # P))
[PROOF STEP]
note ih = this(1) and ci = this(2)
[PROOF STATE]
proof (state)
this:
?Ci = select_min_weight_clause ?P0.0 P \<Longrightarrow> weight (apfst mset ?Ci) = Min ((weight \<circ> apfst mset) ` set (?P0.0 # P))
Ci = select_min_weight_clause P0 (P1 # P)

goal (2 subgoals):
 1. \<And>P0 Ci. Ci = select_min_weight_clause P0 [] \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set [P0])
 2. \<And>a P P0 Ci. \<lbrakk>\<And>P0 Ci. Ci = select_min_weight_clause P0 P \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P)); Ci = select_min_weight_clause P0 (a # P)\<rbrakk> \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # a # P))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
[PROOF STEP]
proof (cases "weight (apfst mset P1) < weight (apfst mset P0)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. weight (apfst mset P1) < weight (apfst mset P0) \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
 2. \<not> weight (apfst mset P1) < weight (apfst mset P0) \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
weight (apfst mset P1) < weight (apfst mset P0)

goal (2 subgoals):
 1. weight (apfst mset P1) < weight (apfst mset P0) \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
 2. \<not> weight (apfst mset P1) < weight (apfst mset P0) \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
weight (apfst mset P1) < weight (apfst mset P0)
[PROOF STEP]
have min: "Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) =
      Min ((weight \<circ> apfst mset) ` set (P1 # P))"
[PROOF STATE]
proof (prove)
using this:
weight (apfst mset P1) < weight (apfst mset P0)

goal (1 subgoal):
 1. Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) = Min ((weight \<circ> apfst mset) ` set (P1 # P))
[PROOF STEP]
by (simp add: min_def)
[PROOF STATE]
proof (state)
this:
Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) = Min ((weight \<circ> apfst mset) ` set (P1 # P))

goal (2 subgoals):
 1. weight (apfst mset P1) < weight (apfst mset P0) \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
 2. \<not> weight (apfst mset P1) < weight (apfst mset P0) \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
[PROOF STEP]
unfolding min
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P1 # P))
[PROOF STEP]
by (rule ih[of Ci P1]) (simp add: ih[of Ci P1] ci True)
[PROOF STATE]
proof (state)
this:
weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))

goal (1 subgoal):
 1. \<not> weight (apfst mset P1) < weight (apfst mset P0) \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> weight (apfst mset P1) < weight (apfst mset P0) \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> weight (apfst mset P1) < weight (apfst mset P0)

goal (1 subgoal):
 1. \<not> weight (apfst mset P1) < weight (apfst mset P0) \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
[PROOF STEP]
have "Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) =
      Min ((weight \<circ> apfst mset) ` set (P1 # P0 # P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) = Min ((weight \<circ> apfst mset) ` set (P1 # P0 # P))
[PROOF STEP]
by (rule arg_cong[of _ _ Min]) auto
[PROOF STATE]
proof (state)
this:
Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) = Min ((weight \<circ> apfst mset) ` set (P1 # P0 # P))

goal (1 subgoal):
 1. \<not> weight (apfst mset P1) < weight (apfst mset P0) \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) = Min ((weight \<circ> apfst mset) ` set (P1 # P0 # P))
[PROOF STEP]
have min: "Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) =
      Min ((weight \<circ> apfst mset) ` set (P0 # P))"
[PROOF STATE]
proof (prove)
using this:
Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) = Min ((weight \<circ> apfst mset) ` set (P1 # P0 # P))

goal (1 subgoal):
 1. Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) = Min ((weight \<circ> apfst mset) ` set (P0 # P))
[PROOF STEP]
by (simp add: min_def) (use False eq_iff in fastforce)
[PROOF STATE]
proof (state)
this:
Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) = Min ((weight \<circ> apfst mset) ` set (P0 # P))

goal (1 subgoal):
 1. \<not> weight (apfst mset P1) < weight (apfst mset P0) \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))
[PROOF STEP]
unfolding min
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P))
[PROOF STEP]
by (rule ih[of Ci P0]) (simp add: ih[of Ci P1] ci False)
[PROOF STATE]
proof (state)
this:
weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P))

goal (1 subgoal):
 1. \<And>P0 Ci. Ci = select_min_weight_clause P0 [] \<Longrightarrow> weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set [P0])
[PROOF STEP]
qed simp


[STATEMENT]
lemma remdups_clss_Nil_iff: "remdups_clss Cs = [] \<longleftrightarrow> Cs = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (remdups_clss Cs = []) = (Cs = [])
[PROOF STEP]
by (cases Cs, simp, hypsubst, subst remdups_clss.simps(2), simp add: Let_def)


[STATEMENT]
lemma empty_N_if_Nil_in_P_or_Q:
  assumes nil_in: "[] \<in> fst ` set (P @ Q)"
  shows "wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)
[PROOF STEP]
proof (induct N)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)
 2. \<And>a N. wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n) \<Longrightarrow> wstate_of_dstate (a # N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)
[PROOF STEP]
case ih: (Cons N0 N)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)

goal (2 subgoals):
 1. wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)
 2. \<And>a N. wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n) \<Longrightarrow> wstate_of_dstate (a # N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)
[PROOF STEP]
have "wstate_of_dstate (N0 # N, P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P, Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N0 # N, P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P, Q, n)
[PROOF STEP]
by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
          wrp.forward_subsumption[of "{#}" "mset (map (apfst mset) P)" "mset (map (apfst mset) Q)"
            "mset (fst N0)" "mset (map (apfst mset) N)" "snd N0" n]])
      (use nil_in in \<open>force simp: image_def apfst_fst_snd\<close>)+
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N0 # N, P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P, Q, n)

goal (2 subgoals):
 1. wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)
 2. \<And>a N. wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n) \<Longrightarrow> wstate_of_dstate (a # N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate (N0 # N, P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P, Q, n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N0 # N, P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P, Q, n)

goal (1 subgoal):
 1. wstate_of_dstate (N0 # N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N0 # N, P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P, Q, n)
wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)

goal (1 subgoal):
 1. wstate_of_dstate (N0 # N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)
[PROOF STEP]
by (rule converse_rtranclp_into_rtranclp)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N0 # N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)

goal (1 subgoal):
 1. wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)
[PROOF STEP]
qed simp


[STATEMENT]
lemma remove_strictly_subsumed_clauses_in_P:
  assumes
    c_in: "C \<in> fst ` set N" and
    p_nsubs: "\<forall>D \<in> fst ` set P. \<not> strictly_subsume [C] D"
  shows "wstate_of_dstate (N, P @ P', Q, n)
    \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) 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 @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
using p_nsubs
[PROOF STATE]
proof (prove)
using this:
\<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D

goal (1 subgoal):
 1. wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
proof (induct "length P'" arbitrary: P P' rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' P. \<lbrakk>\<And>P'a P. \<lbrakk>length P'a < length P'; \<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P'a, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P'a, Q, n); \<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?P' < length P'; \<forall>D\<in>fst ` set ?P. \<not> strictly_subsume [C] D\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, ?P @ ?P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, ?P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) ?P', Q, n)
\<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D

goal (1 subgoal):
 1. \<And>P' P. \<lbrakk>\<And>P'a P. \<lbrakk>length P'a < length P'; \<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P'a, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P'a, Q, n); \<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
note ih = this(1) and p_nsubs = this(2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?P' < length P'; \<forall>D\<in>fst ` set ?P. \<not> strictly_subsume [C] D\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, ?P @ ?P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, ?P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) ?P', Q, n)
\<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D

goal (1 subgoal):
 1. \<And>P' P. \<lbrakk>\<And>P'a P. \<lbrakk>length P'a < length P'; \<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P'a, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P'a, Q, n); \<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
show ?case
[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 @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
proof (cases "length P'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length P' = 0 \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<And>nat. length P' = Suc nat \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
case Suc
[PROOF STATE]
proof (state)
this:
length P' = Suc nat_

goal (2 subgoals):
 1. length P' = 0 \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<And>nat. length P' = Suc nat \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
let ?Dj = "hd P'"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length P' = 0 \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<And>nat. length P' = Suc nat \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
let ?P'' = "tl P'"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length P' = 0 \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<And>nat. length P' = Suc nat \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
have p': "P' = hd P' # tl P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P' = hd P' # tl P'
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
length P' = Suc nat_

goal (1 subgoal):
 1. P' = hd P' # tl P'
[PROOF STEP]
by (metis length_Suc_conv list.distinct(1) list.exhaust_sel)
[PROOF STATE]
proof (state)
this:
P' = hd P' # tl P'

goal (2 subgoals):
 1. length P' = 0 \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<And>nat. length P' = Suc nat \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
show ?thesis
[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 @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
proof (cases "strictly_subsume [C] (fst ?Dj)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
case subs: True
[PROOF STATE]
proof (state)
this:
strictly_subsume [C] (fst (hd P'))

goal (2 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
have p_filtered: "{#(E, k) \<in># image_mset (apfst mset) (mset P). E \<noteq> mset (fst ?Dj)#} =
        image_mset (apfst mset) (mset P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#(E, k) \<in># image_mset (apfst mset) (mset P). E \<noteq> mset (fst (hd P'))#} = image_mset (apfst mset) (mset P)
[PROOF STEP]
by (rule filter_mset_cong[OF refl, of _ _ "\<lambda>_. True", simplified],
            use subs p_nsubs in \<open>auto simp: strictly_subsume_def\<close>)
[PROOF STATE]
proof (state)
this:
{#(E, k) \<in># image_mset (apfst mset) (mset P). E \<noteq> mset (fst (hd P'))#} = image_mset (apfst mset) (mset P)

goal (2 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
have "{#(E, k) \<in># image_mset (apfst mset) (mset P'). E \<noteq> mset (fst ?Dj)#} =
        {#(E, k) \<in># image_mset (apfst mset) (mset ?P''). E \<noteq> mset (fst ?Dj)#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#(E, k) \<in># image_mset (apfst mset) (mset P'). E \<noteq> mset (fst (hd P'))#} = {#(E, k) \<in># image_mset (apfst mset) (mset (tl P')). E \<noteq> mset (fst (hd P'))#}
[PROOF STEP]
by (subst (2) p') (simp add: case_prod_beta)
[PROOF STATE]
proof (state)
this:
{#(E, k) \<in># image_mset (apfst mset) (mset P'). E \<noteq> mset (fst (hd P'))#} = {#(E, k) \<in># image_mset (apfst mset) (mset (tl P')). E \<noteq> mset (fst (hd P'))#}

goal (2 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{#(E, k) \<in># image_mset (apfst mset) (mset P'). E \<noteq> mset (fst (hd P'))#} = {#(E, k) \<in># image_mset (apfst mset) (mset (tl P')). E \<noteq> mset (fst (hd P'))#}

goal (2 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
have "\<dots> =
        image_mset (apfst mset) (mset (filter (\<lambda>(E, l). mset E \<noteq> mset (fst ?Dj)) ?P''))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#(E, k) \<in># image_mset (apfst mset) (mset (tl P')). E \<noteq> mset (fst (hd P'))#} = image_mset (apfst mset) (mset (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')))
[PROOF STEP]
by (auto simp: image_mset_filter_swap[symmetric] case_prod_beta)
[PROOF STATE]
proof (state)
this:
{#(E, k) \<in># image_mset (apfst mset) (mset (tl P')). E \<noteq> mset (fst (hd P'))#} = image_mset (apfst mset) (mset (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')))

goal (2 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{#(E, k) \<in># image_mset (apfst mset) (mset P'). E \<noteq> mset (fst (hd P'))#} = image_mset (apfst mset) (mset (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')))
[PROOF STEP]
have p'_filtered:
        "{#(E, k) \<in># image_mset (apfst mset) (mset P'). E \<noteq> mset (fst ?Dj)#} =
        image_mset (apfst mset) (mset (filter (\<lambda>(E, l). mset E \<noteq> mset (fst ?Dj)) ?P''))"
[PROOF STATE]
proof (prove)
using this:
{#(E, k) \<in># image_mset (apfst mset) (mset P'). E \<noteq> mset (fst (hd P'))#} = image_mset (apfst mset) (mset (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')))

goal (1 subgoal):
 1. {#(E, k) \<in># image_mset (apfst mset) (mset P'). E \<noteq> mset (fst (hd P'))#} = image_mset (apfst mset) (mset (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
{#(E, k) \<in># image_mset (apfst mset) (mset P'). E \<noteq> mset (fst (hd P'))#} = image_mset (apfst mset) (mset (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')))

goal (2 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
have "wstate_of_dstate (N, P @ P', Q, n)
        \<leadsto>\<^sub>w wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst ?Dj)) ?P'', Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P'), Q, n)
[PROOF STEP]
by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
              wrp.backward_subsumption_P[of "mset C" "mset (map (apfst mset) N)" "mset (fst ?Dj)"
                "mset (map (apfst mset) (P @ P'))" "mset (map (apfst mset) Q)" n]],
          use c_in subs in \<open>auto simp add: p_filtered p'_filtered arg_cong[OF p', of set]
            strictly_subsume_def\<close>)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P'), Q, n)

goal (2 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P'), Q, n)

goal (2 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
have "\<dots>
        \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P'), Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
              ih[of "filter (\<lambda>(E, l). mset E \<noteq> mset (fst ?Dj)) ?P''" P]])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P'), Q, n) = wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P'), Q, n)
 2. wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')), Q, n) = wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 3. length (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')) < length P'
 4. \<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. image_mset (apfst mset) {#x \<in># mset (tl P'). (case x of (E, l) \<Rightarrow> mset E \<noteq> mset (fst (hd P'))) \<and> \<not> strictly_subsume [C] (fst x)#} = image_mset (apfst mset) {#x \<in># mset P'. \<not> strictly_subsume [C] (fst x)#}
 2. length (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')) < length P'
 3. \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)
[PROOF STEP]
apply (subst (3) p')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. image_mset (apfst mset) {#x \<in># mset (tl P'). (case x of (E, l) \<Rightarrow> mset E \<noteq> mset (fst (hd P'))) \<and> \<not> strictly_subsume [C] (fst x)#} = image_mset (apfst mset) {#x \<in># mset (hd P' # tl P'). \<not> strictly_subsume [C] (fst x)#}
 2. length (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')) < length P'
 3. \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)
[PROOF STEP]
using subs
[PROOF STATE]
proof (prove)
using this:
strictly_subsume [C] (fst (hd P'))

goal (3 subgoals):
 1. image_mset (apfst mset) {#x \<in># mset (tl P'). (case x of (E, l) \<Rightarrow> mset E \<noteq> mset (fst (hd P'))) \<and> \<not> strictly_subsume [C] (fst x)#} = image_mset (apfst mset) {#x \<in># mset (hd P' # tl P'). \<not> strictly_subsume [C] (fst x)#}
 2. length (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')) < length P'
 3. \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)
[PROOF STEP]
apply (simp add: case_prod_beta)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> image_mset (apfst mset) {#x \<in># mset (tl P'). mset (fst x) \<noteq> mset (fst (hd P')) \<and> \<not> strictly_subsume [C] (fst x)#} = image_mset (apfst mset) {#x \<in># mset (tl P'). \<not> strictly_subsume [C] (fst x)#}
 2. length (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')) < length P'
 3. \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)
[PROOF STEP]
apply (rule arg_cong[of _ _ "\<lambda>x. image_mset (apfst mset) x"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> {#x \<in># mset (tl P'). mset (fst x) \<noteq> mset (fst (hd P')) \<and> \<not> strictly_subsume [C] (fst x)#} = {#x \<in># mset (tl P'). \<not> strictly_subsume [C] (fst x)#}
 2. length (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')) < length P'
 3. \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)
[PROOF STEP]
apply (metis (no_types, opaque_lifting) strictly_subsume_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')) < length P'
 2. \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)
[PROOF STEP]
apply (subst (3) p')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')) < length (hd P' # tl P')
 2. \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)
[PROOF STEP]
apply (subst list.size)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P')) < length (tl P') + Suc 0
 2. \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)
[PROOF STEP]
apply (metis (no_types, lifting) less_Suc0 less_add_same_cancel1 linorder_neqE_nat
            not_add_less1 sum_length_filter_compl trans_less_add1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)
[PROOF STEP]
using p_nsubs
[PROOF STATE]
proof (prove)
using this:
\<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D

goal (1 subgoal):
 1. \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P'), Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)

goal (2 subgoals):
 1. strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 2. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P'), Q, n)
wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P'), Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P'), Q, n)
wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst (hd P'))) (tl P'), Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)

goal (1 subgoal):
 1. wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
by (rule converse_rtranclp_into_rtranclp)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)

goal (1 subgoal):
 1. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
case nsubs: False
[PROOF STATE]
proof (state)
this:
\<not> strictly_subsume [C] (fst (hd P'))

goal (1 subgoal):
 1. \<not> strictly_subsume [C] (fst (hd P')) \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
show ?thesis
[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 @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
              ih[of ?P'' "P @ [?Dj]"]])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. wstate_of_dstate (N, (P @ [hd P']) @ tl P', Q, n) = wstate_of_dstate (N, P @ P', Q, n)
 2. wstate_of_dstate (N, (P @ [hd P']) @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) (tl P'), Q, n) = wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 3. length (tl P') < length P'
 4. \<forall>D\<in>fst ` set (P @ [hd P']). \<not> strictly_subsume [C] D
[PROOF STEP]
using nsubs p_nsubs
[PROOF STATE]
proof (prove)
using this:
\<not> strictly_subsume [C] (fst (hd P'))
\<forall>D\<in>fst ` set P. \<not> strictly_subsume [C] D

goal (4 subgoals):
 1. wstate_of_dstate (N, (P @ [hd P']) @ tl P', Q, n) = wstate_of_dstate (N, P @ P', Q, n)
 2. wstate_of_dstate (N, (P @ [hd P']) @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) (tl P'), Q, n) = wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
 3. length (tl P') < length P'
 4. \<forall>D\<in>fst ` set (P @ [hd P']). \<not> strictly_subsume [C] D
[PROOF STEP]
apply (simp_all add: arg_cong[OF p', of mset] arg_cong[OF p', of "filter f" for f])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> strictly_subsume [C] (fst (hd P')); \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)\<rbrakk> \<Longrightarrow> length P' - Suc 0 < length P'
[PROOF STEP]
apply (subst (1 2) p')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> strictly_subsume [C] (fst (hd P')); \<forall>D\<in>set P. \<not> strictly_subsume [C] (fst D)\<rbrakk> \<Longrightarrow> length (hd P' # tl P') - Suc 0 < length (hd P' # tl P')
[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 @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)

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

goal (1 subgoal):
 1. length P' = 0 \<Longrightarrow> wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma remove_strictly_subsumed_clauses_in_Q:
  assumes c_in: "C \<in> fst ` set N"
  shows "wstate_of_dstate (N, P, Q @ Q', n)
    \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) 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, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q', n)
[PROOF STEP]
proof (induct Q' arbitrary: Q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Q. wstate_of_dstate (N, P, Q @ [], n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [], n)
 2. \<And>a Q' Q. (\<And>Q. wstate_of_dstate (N, P, Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q', n)) \<Longrightarrow> wstate_of_dstate (N, P, Q @ a # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) (a # Q'), n)
[PROOF STEP]
case ih: (Cons Dj Q')
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, ?Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, ?Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q', n)

goal (2 subgoals):
 1. \<And>Q. wstate_of_dstate (N, P, Q @ [], n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [], n)
 2. \<And>a Q' Q. (\<And>Q. wstate_of_dstate (N, P, Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q', n)) \<Longrightarrow> wstate_of_dstate (N, P, Q @ a # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) (a # Q'), n)
[PROOF STEP]
have "wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>*
    wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ 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, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)
[PROOF STEP]
proof (cases "strictly_subsume [C] (fst Dj)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. strictly_subsume [C] (fst Dj) \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)
 2. \<not> strictly_subsume [C] (fst Dj) \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)
[PROOF STEP]
case subs: True
[PROOF STATE]
proof (state)
this:
strictly_subsume [C] (fst Dj)

goal (2 subgoals):
 1. strictly_subsume [C] (fst Dj) \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)
 2. \<not> strictly_subsume [C] (fst Dj) \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)
[PROOF STEP]
have "wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w wstate_of_dstate (N, P, Q @ Q', n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w wstate_of_dstate (N, P, Q @ Q', n)
[PROOF STEP]
by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
            wrp.backward_subsumption_Q[of "mset C" "mset (map (apfst mset) N)" "mset (fst Dj)"
              "mset (map (apfst mset) P)" "mset (map (apfst mset) (Q @ Q'))" "snd Dj" n]])
        (use c_in subs in \<open>auto simp: apfst_fst_snd strictly_subsume_def\<close>)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w wstate_of_dstate (N, P, Q @ Q', n)

goal (2 subgoals):
 1. strictly_subsume [C] (fst Dj) \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)
 2. \<not> strictly_subsume [C] (fst Dj) \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w wstate_of_dstate (N, 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 wstate_of_dstate (N, 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, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)

goal (1 subgoal):
 1. \<not> strictly_subsume [C] (fst Dj) \<Longrightarrow> wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)

goal (2 subgoals):
 1. \<And>Q. wstate_of_dstate (N, P, Q @ [], n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [], n)
 2. \<And>a Q' Q. (\<And>Q. wstate_of_dstate (N, P, Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q', n)) \<Longrightarrow> wstate_of_dstate (N, P, Q @ a # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) (a # 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, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) (Dj # Q'), n)
[PROOF STEP]
using ih[of "Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj]"]
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)
wstate_of_dstate (N, P, (Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj]) @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, (Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj]) @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q', n)

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

goal (1 subgoal):
 1. \<And>Q. wstate_of_dstate (N, P, Q @ [], n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [], n)
[PROOF STEP]
qed simp


[STATEMENT]
lemma reduce_clause_in_P:
  assumes
    c_in: "C \<in> fst ` set N" and
    p_irred: "\<forall>(E, k) \<in> set (P @ P'). k > j \<longrightarrow> is_irreducible [C] E"
  shows "wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n)
    \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D D', j) # P', Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D D', j) # P', Q, n)
[PROOF STEP]
proof (induct D' arbitrary: D)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>D. wstate_of_dstate (N, P @ (D @ [], j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D [], j) # P', Q, n)
 2. \<And>a D' D. (\<And>D. wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D D', j) # P', Q, n)) \<Longrightarrow> wstate_of_dstate (N, P @ (D @ a # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (a # D'), j) # P', Q, n)
[PROOF STEP]
case ih: (Cons L D')
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P @ (?D @ D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (?D @ reduce [C] ?D D', j) # P', Q, n)

goal (2 subgoals):
 1. \<And>D. wstate_of_dstate (N, P @ (D @ [], j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D [], j) # P', Q, n)
 2. \<And>a D' D. (\<And>D. wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D D', j) # P', Q, n)) \<Longrightarrow> wstate_of_dstate (N, P @ (D @ a # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (a # D'), j) # P', Q, n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
[PROOF STEP]
proof (cases "is_reducible_lit [C] (D @ D') L")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
 2. \<not> is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
[PROOF STEP]
case l_red: True
[PROOF STATE]
proof (state)
this:
is_reducible_lit [C] (D @ D') L

goal (2 subgoals):
 1. is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
 2. \<not> is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_reducible_lit [C] (D @ D') L
[PROOF STEP]
obtain L' :: "'a literal" and \<sigma> :: 's where
      l'_in: "L' \<in> set C" and
      not_l: "- L = L' \<cdot>l \<sigma>" and
      subs: "mset (remove1 L' C) \<cdot> \<sigma> \<subseteq># mset (D @ D')"
[PROOF STATE]
proof (prove)
using this:
is_reducible_lit [C] (D @ D') L

goal (1 subgoal):
 1. (\<And>L' \<sigma>. \<lbrakk>L' \<in> set C; - L = L' \<cdot>l \<sigma>; mset (remove1 L' C) \<cdot> \<sigma> \<subseteq># mset (D @ D')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_reducible_lit_def
[PROOF STATE]
proof (prove)
using this:
\<exists>D\<in>set [C]. \<exists>L'\<in>set D. \<exists>\<sigma>. - L = L' \<cdot>l \<sigma> \<and> mset (remove1 L' D) \<cdot> \<sigma> \<subseteq># mset (D @ D')

goal (1 subgoal):
 1. (\<And>L' \<sigma>. \<lbrakk>L' \<in> set C; - L = L' \<cdot>l \<sigma>; mset (remove1 L' C) \<cdot> \<sigma> \<subseteq># mset (D @ D')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
L' \<in> set C
- L = L' \<cdot>l \<sigma>
mset (remove1 L' C) \<cdot> \<sigma> \<subseteq># mset (D @ D')

goal (2 subgoals):
 1. is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
 2. \<not> is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
[PROOF STEP]
have ldd'_red: "is_reducible [C] (L # D @ D')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduce [C] [] (L # D @ D') \<noteq> L # D @ D'
[PROOF STEP]
apply (rule is_reducible_lit_imp_is_reducible)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ?L \<in> set (L # D @ D')
 2. is_reducible_lit [C] ([] @ remove1 ?L (L # D @ D')) ?L
[PROOF STEP]
using l_red
[PROOF STATE]
proof (prove)
using this:
is_reducible_lit [C] (D @ D') L

goal (2 subgoals):
 1. ?L \<in> set (L # D @ D')
 2. is_reducible_lit [C] ([] @ remove1 ?L (L # D @ D')) ?L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reduce [C] [] (L # D @ D') \<noteq> L # D @ D'

goal (2 subgoals):
 1. is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
 2. \<not> is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
[PROOF STEP]
have lt_imp_neq: "\<forall>(E, k) \<in> set (P @ P'). j < k \<longrightarrow> mset E \<noteq> mset (L # D @ D')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(E, k)\<in>set (P @ P'). j < k \<longrightarrow> mset E \<noteq> mset (L # D @ D')
[PROOF STEP]
using p_irred ldd'_red is_irreducible_mset_iff
[PROOF STATE]
proof (prove)
using this:
\<forall>(E, k)\<in>set (P @ P'). j < k \<longrightarrow> is_irreducible [C] E
reduce [C] [] (L # D @ D') \<noteq> L # D @ D'
mset ?E = mset ?E' \<Longrightarrow> (reduce ?Ds ?C ?E = ?E) = (reduce ?Ds ?C ?E' = ?E')

goal (1 subgoal):
 1. \<forall>(E, k)\<in>set (P @ P'). j < k \<longrightarrow> mset E \<noteq> mset (L # D @ D')
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>(E, k)\<in>set (P @ P'). j < k \<longrightarrow> mset E \<noteq> mset (L # D @ D')

goal (2 subgoals):
 1. is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
 2. \<not> is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
[PROOF STEP]
have "wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n)
      \<leadsto>\<^sub>w wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n)
[PROOF STEP]
apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
            wrp.backward_reduction_P[of "mset C - {#L'#}" L' "mset (map (apfst mset) N)" L \<sigma>
              "mset (D @ D')" "mset (map (apfst mset) (P @ P'))" j "mset (map (apfst mset) Q)" n]])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. (mset (map (apfst mset) N), mset (map (apfst mset) (P @ P')) + {#(mset (D @ D') + {#L#}, j)#}, mset (map (apfst mset) Q), n) = wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n)
 2. (mset (map (apfst mset) N), mset (map (apfst mset) (P @ P')) + {#(mset (D @ D'), j)#}, mset (map (apfst mset) Q), n) = wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n)
 3. remove1_mset L' (mset C) + {#L'#} \<in># image_mset fst (mset (map (apfst mset) N))
 4. - L = L' \<cdot>l \<sigma>
 5. remove1_mset L' (mset C) \<cdot> \<sigma> \<subseteq># mset (D @ D')
 6. \<forall>ja. (mset (D @ D') + {#L#}, ja) \<in># mset (map (apfst mset) (P @ P')) \<longrightarrow> ja \<le> j
[PROOF STEP]
using l'_in not_l subs c_in lt_imp_neq
[PROOF STATE]
proof (prove)
using this:
L' \<in> set C
- L = L' \<cdot>l \<sigma>
mset (remove1 L' C) \<cdot> \<sigma> \<subseteq># mset (D @ D')
C \<in> fst ` set N
\<forall>(E, k)\<in>set (P @ P'). j < k \<longrightarrow> mset E \<noteq> mset (L # D @ D')

goal (6 subgoals):
 1. (mset (map (apfst mset) N), mset (map (apfst mset) (P @ P')) + {#(mset (D @ D') + {#L#}, j)#}, mset (map (apfst mset) Q), n) = wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n)
 2. (mset (map (apfst mset) N), mset (map (apfst mset) (P @ P')) + {#(mset (D @ D'), j)#}, mset (map (apfst mset) Q), n) = wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n)
 3. remove1_mset L' (mset C) + {#L'#} \<in># image_mset fst (mset (map (apfst mset) N))
 4. - L = L' \<cdot>l \<sigma>
 5. remove1_mset L' (mset C) \<cdot> \<sigma> \<subseteq># mset (D @ D')
 6. \<forall>ja. (mset (D @ D') + {#L#}, ja) \<in># mset (map (apfst mset) (P @ P')) \<longrightarrow> ja \<le> j
[PROOF STEP]
by (simp_all add: case_prod_beta) force+
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n)

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

goal (1 subgoal):
 1. wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
[PROOF STEP]
using ih[of D] l_red
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n)
wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D D', j) # P', Q, n)
is_reducible_lit [C] (D @ D') L

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

goal (1 subgoal):
 1. \<not> is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_reducible_lit [C] (D @ D') L \<Longrightarrow> wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_reducible_lit [C] (D @ D') L

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

goal (1 subgoal):
 1. wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D (L # D'), j) # P', Q, n)
[PROOF STEP]
using ih[of "D @ [L]"]
[PROOF STATE]
proof (prove)
using this:
\<not> is_reducible_lit [C] (D @ D') L
wstate_of_dstate (N, P @ ((D @ [L]) @ D', j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ ((D @ [L]) @ reduce [C] (D @ [L]) D', j) # P', Q, n)

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

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

goal (1 subgoal):
 1. \<And>D. wstate_of_dstate (N, P @ (D @ [], j) # P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D [], j) # P', Q, n)
[PROOF STEP]
qed simp


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

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n)
[PROOF STEP]
proof (induct D' arbitrary: D)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>D. reduce [C] D [] \<noteq> [] \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ [], j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D [], j) # P, Q @ Q', n)
 2. \<And>a D' D. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (a # D') \<noteq> a # D'\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ a # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (a # D'), j) # P, Q @ Q', n)
[PROOF STEP]
case (Cons L D')
[PROOF STATE]
proof (state)
this:
reduce [C] ?D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (?D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (?D @ reduce [C] ?D D', j) # P, Q @ Q', n)
reduce [C] D (L # D') \<noteq> L # D'

goal (2 subgoals):
 1. \<And>D. reduce [C] D [] \<noteq> [] \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ [], j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D [], j) # P, Q @ Q', n)
 2. \<And>a D' D. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (a # D') \<noteq> a # D'\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ a # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (a # D'), j) # P, Q @ Q', n)
[PROOF STEP]
note ih = this(1) and ld'_red = this(2)
[PROOF STATE]
proof (state)
this:
reduce [C] ?D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (?D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (?D @ reduce [C] ?D D', j) # P, Q @ Q', n)
reduce [C] D (L # D') \<noteq> L # D'

goal (2 subgoals):
 1. \<And>D. reduce [C] D [] \<noteq> [] \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ [], j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D [], j) # P, Q @ Q', n)
 2. \<And>a D' D. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (a # D') \<noteq> a # D'\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ a # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (a # D'), j) # P, Q @ Q', n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
reduce [C] ?D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (?D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (?D @ reduce [C] ?D D', j) # P, Q @ Q', n)
reduce [C] D (L # D') \<noteq> L # D'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
reduce [C] ?D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (?D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (?D @ reduce [C] ?D D', j) # P, Q @ Q', n)
reduce [C] D (L # D') \<noteq> L # D'

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
[PROOF STEP]
proof (cases "is_reducible_lit [C] (D @ D') L")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
 2. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; \<not> is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
[PROOF STEP]
case l_red: True
[PROOF STATE]
proof (state)
this:
is_reducible_lit [C] (D @ D') L

goal (2 subgoals):
 1. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
 2. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; \<not> is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_reducible_lit [C] (D @ D') L
[PROOF STEP]
obtain L' :: "'a literal" and \<sigma> :: 's where
      l'_in: "L' \<in> set C" and
      not_l: "- L = L' \<cdot>l \<sigma>" and
      subs: "mset (remove1 L' C) \<cdot> \<sigma> \<subseteq># mset (D @ D')"
[PROOF STATE]
proof (prove)
using this:
is_reducible_lit [C] (D @ D') L

goal (1 subgoal):
 1. (\<And>L' \<sigma>. \<lbrakk>L' \<in> set C; - L = L' \<cdot>l \<sigma>; mset (remove1 L' C) \<cdot> \<sigma> \<subseteq># mset (D @ D')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_reducible_lit_def
[PROOF STATE]
proof (prove)
using this:
\<exists>D\<in>set [C]. \<exists>L'\<in>set D. \<exists>\<sigma>. - L = L' \<cdot>l \<sigma> \<and> mset (remove1 L' D) \<cdot> \<sigma> \<subseteq># mset (D @ D')

goal (1 subgoal):
 1. (\<And>L' \<sigma>. \<lbrakk>L' \<in> set C; - L = L' \<cdot>l \<sigma>; mset (remove1 L' C) \<cdot> \<sigma> \<subseteq># mset (D @ D')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
L' \<in> set C
- L = L' \<cdot>l \<sigma>
mset (remove1 L' C) \<cdot> \<sigma> \<subseteq># mset (D @ D')

goal (2 subgoals):
 1. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
 2. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; \<not> is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
[PROOF STEP]
have "wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n)
      \<leadsto>\<^sub>w wstate_of_dstate (N, (D @ D', j) # P, Q @ Q', n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w wstate_of_dstate (N, (D @ D', j) # P, Q @ Q', n)
[PROOF STEP]
by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
            wrp.backward_reduction_Q[of "mset C - {#L'#}" L' "mset (map (apfst mset) N)" L \<sigma>
              "mset (D @ D')" "mset (map (apfst mset) P)" "mset (map (apfst mset) (Q @ Q'))" j n]],
          use l'_in not_l subs c_in in auto)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w wstate_of_dstate (N, (D @ D', j) # P, Q @ Q', n)

goal (2 subgoals):
 1. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
 2. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; \<not> is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w wstate_of_dstate (N, (D @ D', j) # P, Q @ Q', n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w wstate_of_dstate (N, (D @ D', j) # P, Q @ Q', n)

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
[PROOF STEP]
using l_red p_irred reduce_clause_in_P[OF c_in, of "[]" P j D D' "Q @ Q'" n]
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w wstate_of_dstate (N, (D @ D', j) # P, Q @ Q', n)
is_reducible_lit [C] (D @ D') L
\<forall>(E, k)\<in>set P. j < k \<longrightarrow> is_irreducible [C] E
\<forall>(E, k)\<in>set ([] @ P). j < k \<longrightarrow> is_irreducible [C] E \<Longrightarrow> wstate_of_dstate (N, [] @ (D @ D', j) # P, Q @ Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, [] @ (D @ reduce [C] D D', j) # P, Q @ Q', n)

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

goal (1 subgoal):
 1. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; \<not> is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; \<not> is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
[PROOF STEP]
case l_nred: False
[PROOF STATE]
proof (state)
this:
\<not> is_reducible_lit [C] (D @ D') L

goal (1 subgoal):
 1. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; \<not> is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> is_reducible_lit [C] (D @ D') L
[PROOF STEP]
have d'_red: "reduce [C] (D @ [L]) D' \<noteq> D'"
[PROOF STATE]
proof (prove)
using this:
\<not> is_reducible_lit [C] (D @ D') L

goal (1 subgoal):
 1. reduce [C] (D @ [L]) D' \<noteq> D'
[PROOF STEP]
using ld'_red
[PROOF STATE]
proof (prove)
using this:
\<not> is_reducible_lit [C] (D @ D') L
reduce [C] D (L # D') \<noteq> L # D'

goal (1 subgoal):
 1. reduce [C] (D @ [L]) D' \<noteq> D'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
reduce [C] (D @ [L]) D' \<noteq> D'

goal (1 subgoal):
 1. \<lbrakk>\<And>D. reduce [C] D D' \<noteq> D' \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n); reduce [C] D (L # D') \<noteq> L # D'; \<not> is_reducible_lit [C] (D @ D') L\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D (L # D'), j) # P, Q @ Q', n)
[PROOF STEP]
using ih[OF d'_red] l_nred
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P, Q @ ((D @ [L]) @ D', j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, ((D @ [L]) @ reduce [C] (D @ [L]) D', j) # P, Q @ Q', n)
\<not> is_reducible_lit [C] (D @ D') L

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

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

goal (1 subgoal):
 1. \<And>D. reduce [C] D [] \<noteq> [] \<Longrightarrow> wstate_of_dstate (N, P, Q @ (D @ [], j) # Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D [], j) # P, Q @ Q', n)
[PROOF STEP]
qed simp