[STATEMENT]
lemma nonfinal_deterministic_RP_step:
  assumes
    nonfinal: "\<not> is_final_dstate St" and
    step: "St' = deterministic_RP_step St"
  shows "wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
obtain N P Q :: "'a dclause list" and n :: nat where
    st: "St = (N, P, Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N P Q n. St = (N, P, Q, n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases St) blast
[PROOF STATE]
proof (state)
this:
St = (N, P, Q, n)

goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[unfolded st deterministic_RP_step.simps, simplified]
[PROOF STATE]
proof (state)
this:
St' = (if \<exists>Ci\<in>set P \<union> set Q. fst Ci = [] then ([], [], remdups_clss P @ Q, n + length (remdups_clss P)) else case N of [] \<Rightarrow> case P of [] \<Rightarrow> (N, P, Q, n) | P0 # P' \<Rightarrow> let (C, i) = select_min_weight_clause P0 P'; N = map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))); P = filter (\<lambda>(D, j). mset D \<noteq> mset C) P; Q = (C, i) # Q; n = Suc n in (N, P, Q, n) | (C, i) # N \<Rightarrow> let C = reduce (map fst (P @ Q)) [] C in if C = [] then ([], [], [([], i)], Suc n) else if is_tautology C \<or> subsume (map fst (P @ Q)) C then (N, P, Q, n) else let P = reduce_all C P; (back_to_P, Q) = reduce_all2 C Q; P = back_to_P @ P; Q = filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q; P = filter (Not \<circ> strictly_subsume [C] \<circ> fst) P; P = (C, i) # P in (N, P, Q, n))

goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
proof (cases "\<exists>Ci \<in> set P \<union> set Q. fst Ci = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>Ci\<in>set P \<union> set Q. fst Ci = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = []) \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
case nil_in: True
[PROOF STATE]
proof (state)
this:
\<exists>Ci\<in>set P \<union> set Q. fst Ci = []

goal (2 subgoals):
 1. \<exists>Ci\<in>set P \<union> set Q. fst Ci = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = []) \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[simplified nil_in, simplified]
[PROOF STATE]
proof (state)
this:
St' = ([], [], remdups_clss P @ Q, n + length (remdups_clss P))

goal (2 subgoals):
 1. \<exists>Ci\<in>set P \<union> set Q. fst Ci = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = []) \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have nil_in': "[] \<in> fst ` set (P @ Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<in> fst ` set (P @ Q)
[PROOF STEP]
using nil_in
[PROOF STATE]
proof (prove)
using this:
\<exists>Ci\<in>set P \<union> set Q. fst Ci = []

goal (1 subgoal):
 1. [] \<in> fst ` set (P @ Q)
[PROOF STEP]
by (force simp: image_def)
[PROOF STATE]
proof (state)
this:
[] \<in> fst ` set (P @ Q)

goal (2 subgoals):
 1. \<exists>Ci\<in>set P \<union> set Q. fst Ci = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = []) \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have star: "[] \<in> fst ` set (P @ Q) \<Longrightarrow>
      wstate_of_dstate (N, P, Q, n)
      \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<in> fst ` set (P @ Q) \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
proof (induct "length (remdups_clss P)" arbitrary: N P Q n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P N Q n. \<lbrakk>0 = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
 2. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = length (remdups_clss P)
[] \<in> fst ` set (P @ Q)

goal (2 subgoals):
 1. \<And>P N Q n. \<lbrakk>0 = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
 2. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
note len_p = this(1) and nil_in' = this(2)
[PROOF STATE]
proof (state)
this:
0 = length (remdups_clss P)
[] \<in> fst ` set (P @ Q)

goal (2 subgoals):
 1. \<And>P N Q n. \<lbrakk>0 = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
 2. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
have p_nil: "P = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P = []
[PROOF STEP]
using len_p remdups_clss_Nil_iff
[PROOF STATE]
proof (prove)
using this:
0 = length (remdups_clss P)
(remdups_clss ?Cs = []) = (?Cs = [])

goal (1 subgoal):
 1. P = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P = []

goal (2 subgoals):
 1. \<And>P N Q n. \<lbrakk>0 = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
 2. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
have "wstate_of_dstate (N, [], Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, [], Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], Q, n)
[PROOF STEP]
by (rule empty_N_if_Nil_in_P_or_Q[OF nil_in'[unfolded p_nil]])
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, [], Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], Q, n)

goal (2 subgoals):
 1. \<And>P N Q n. \<lbrakk>0 = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
 2. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate (N, [], Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], Q, n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, [], Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], Q, n)

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
unfolding p_nil
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, [], Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], Q, n)

goal (1 subgoal):
 1. wstate_of_dstate (N, [], Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss [] @ Q, n + length (remdups_clss []))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k = length (remdups_clss ?P); [] \<in> fst ` set (?P @ ?Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (?N, ?P, ?Q, ?n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss ?P @ ?Q, ?n + length (remdups_clss ?P))
Suc k = length (remdups_clss P)
[] \<in> fst ` set (P @ Q)

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
note ih = this(1) and suc_k = this(2) and nil_in' = this(3)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k = length (remdups_clss ?P); [] \<in> fst ` set (?P @ ?Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (?N, ?P, ?Q, ?n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss ?P @ ?Q, ?n + length (remdups_clss ?P))
Suc k = length (remdups_clss P)
[] \<in> fst ` set (P @ Q)

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
have "P \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<noteq> []
[PROOF STEP]
using suc_k remdups_clss_Nil_iff
[PROOF STATE]
proof (prove)
using this:
Suc k = length (remdups_clss P)
(remdups_clss ?Cs = []) = (?Cs = [])

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

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
hence p_cons: "P = hd P # tl P"
[PROOF STATE]
proof (prove)
using this:
P \<noteq> []

goal (1 subgoal):
 1. P = hd P # tl P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P = hd P # tl P

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
obtain C :: "'a lclause" and i :: nat where
        ci: "(C, i) = select_min_weight_clause (hd P) (tl P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C i. (C, i) = select_min_weight_clause (hd P) (tl P) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.exhaust)
[PROOF STATE]
proof (state)
this:
(C, i) = select_min_weight_clause (hd P) (tl P)

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
have ci_in: "(C, i) \<in> set P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, i) \<in> set P
[PROOF STEP]
unfolding ci
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select_min_weight_clause (hd P) (tl P) \<in> set P
[PROOF STEP]
using p_cons select_min_weight_clause_in[of "hd P" "tl P"]
[PROOF STATE]
proof (prove)
using this:
P = hd P # tl P
select_min_weight_clause (hd P) (tl P) \<in> set (hd P # tl P)

goal (1 subgoal):
 1. select_min_weight_clause (hd P) (tl P) \<in> set P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(C, i) \<in> set P

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
have ci_min: "\<forall>(D, j) \<in># mset (map (apfst mset) P). weight (mset C, i) \<le> weight (D, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(D, j)\<in>#mset (map (apfst mset) P). weight (mset C, i) \<le> weight (D, j)
[PROOF STEP]
by (subst p_cons) (simp add: select_min_weight_clause_min_weight[OF ci, simplified])
[PROOF STATE]
proof (state)
this:
\<forall>(D, j)\<in>#mset (map (apfst mset) P). weight (mset C, i) \<le> weight (D, j)

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
let ?P' = "filter (\<lambda>(D, j). mset D \<noteq> mset C) P"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
have ms_p'_ci_q_eq: "mset (remdups_clss ?P' @ (C, i) # Q) = mset (remdups_clss P @ Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P) @ (C, i) # Q) = mset (remdups_clss P @ Q)
[PROOF STEP]
apply (subst (2) p_cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P) @ (C, i) # Q) = mset (remdups_clss (hd P # tl P) @ Q)
[PROOF STEP]
apply (subst remdups_clss.simps(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P) @ (C, i) # Q) = mset ((let Ci' = select_min_weight_clause (hd P) (tl P) in Ci' # remdups_clss (filter (\<lambda>(D, uu_). mset D \<noteq> mset (fst Ci')) (hd P # tl P))) @ Q)
[PROOF STEP]
by (auto simp: Let_def case_prod_beta p_cons[symmetric] ci[symmetric])
[PROOF STATE]
proof (state)
this:
mset (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P) @ (C, i) # Q) = mset (remdups_clss P @ Q)

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mset (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P) @ (C, i) # Q) = mset (remdups_clss P @ Q)
[PROOF STEP]
have len_p: "length (remdups_clss P) = length (remdups_clss ?P') + 1"
[PROOF STATE]
proof (prove)
using this:
mset (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P) @ (C, i) # Q) = mset (remdups_clss P @ Q)

goal (1 subgoal):
 1. length (remdups_clss P) = length (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P)) + 1
[PROOF STEP]
by (smt Suc_eq_plus1_left add.assoc add_right_cancel length_Cons length_append
            mset_eq_length)
[PROOF STATE]
proof (state)
this:
length (remdups_clss P) = length (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P)) + 1

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
have "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]
by (rule empty_N_if_Nil_in_P_or_Q[OF nil_in'])
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
obtain N' :: "'a dclause list" where
        "\<dots> \<leadsto>\<^sub>w wstate_of_dstate (N', ?P', (C, i) # Q, Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N'. wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', filter (\<lambda>(D, j). mset D \<noteq> mset C) P, (C, i) # Q, Suc n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (atomize_elim, rule exI, rule compute_inferences[OF ci_in], use ci_min in fastforce)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', filter (\<lambda>(D, j). mset D \<noteq> mset C) P, (C, i) # Q, Suc n)

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', filter (\<lambda>(D, j). mset D \<noteq> mset C) P, (C, i) # Q, Suc n)

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
have "\<dots> \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N', filter (\<lambda>(D, j). mset D \<noteq> mset C) P, (C, i) # Q, Suc n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
            ih[of ?P' "(C, i) # Q" N' "Suc n"], OF refl])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. wstate_of_dstate ([], [], remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P) @ (C, i) # Q, Suc n + length (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P))) = wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
 2. k = length (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P))
 3. [] \<in> fst ` set (filter (\<lambda>(D, j). mset D \<noteq> mset C) P @ (C, i) # Q)
[PROOF STEP]
using ms_p'_ci_q_eq suc_k nil_in' ci_in
[PROOF STATE]
proof (prove)
using this:
mset (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P) @ (C, i) # Q) = mset (remdups_clss P @ Q)
Suc k = length (remdups_clss P)
[] \<in> fst ` set (P @ Q)
(C, i) \<in> set P

goal (3 subgoals):
 1. wstate_of_dstate ([], [], remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P) @ (C, i) # Q, Suc n + length (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P))) = wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
 2. k = length (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P))
 3. [] \<in> fst ` set (filter (\<lambda>(D, j). mset D \<noteq> mset C) P @ (C, i) # Q)
[PROOF STEP]
apply (simp_all add: len_p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>add_mset (C, i) (mset (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P))) = mset (remdups_clss P); k = length (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P)); [] \<in> fst ` (set P \<union> set Q); (C, i) \<in> set P\<rbrakk> \<Longrightarrow> add_mset (mset C, i) (image_mset (apfst mset) (mset (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P)))) = image_mset (apfst mset) (mset (remdups_clss P))
 2. \<lbrakk>add_mset (C, i) (mset (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P))) = mset (remdups_clss P); k = length (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P)); [] \<in> fst ` (set P \<union> set Q); (C, i) \<in> set P\<rbrakk> \<Longrightarrow> [] = C \<or> [] \<in> fst ` ({x \<in> set P. case x of (D, j) \<Rightarrow> mset D \<noteq> mset C} \<union> set Q)
[PROOF STEP]
apply (metis (no_types) apfst_conv image_mset_add_mset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>add_mset (C, i) (mset (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P))) = mset (remdups_clss P); k = length (remdups_clss (filter (\<lambda>(D, j). mset D \<noteq> mset C) P)); [] \<in> fst ` (set P \<union> set Q); (C, i) \<in> set P\<rbrakk> \<Longrightarrow> [] = C \<or> [] \<in> fst ` ({x \<in> set P. case x of (D, j) \<Rightarrow> mset D \<noteq> mset C} \<union> set Q)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N', filter (\<lambda>(D, j). mset D \<noteq> mset C) P, (C, i) # Q, Suc n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))

goal (1 subgoal):
 1. \<And>x P N Q n. \<lbrakk>\<And>P N Q n. \<lbrakk>x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P)); Suc x = length (remdups_clss P); [] \<in> fst ` set (P @ Q)\<rbrakk> \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[] \<in> fst ` set (P @ Q) \<Longrightarrow> wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))

goal (2 subgoals):
 1. \<exists>Ci\<in>set P \<union> set Q. fst Ci = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = []) \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
unfolding st step
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
using star[OF nil_in'] nonfinal[unfolded st is_final_dstate.simps]
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
\<not> (N = [] \<and> P = [])

goal (1 subgoal):
 1. wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
[PROOF STEP]
by cases simp_all
[PROOF STATE]
proof (state)
this:
wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'

goal (1 subgoal):
 1. \<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = []) \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = []) \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
case nil_ni: False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = [])

goal (1 subgoal):
 1. \<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = []) \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[simplified nil_ni, simplified]
[PROOF STATE]
proof (state)
this:
St' = (case N of [] \<Rightarrow> case P of [] \<Rightarrow> (N, P, Q, n) | P0 # P' \<Rightarrow> let (C, i) = select_min_weight_clause P0 P'; N = map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))); P = filter (\<lambda>(D, j). mset D \<noteq> mset C) P; Q = (C, i) # Q; n = Suc n in (N, P, Q, n) | (C, i) # N \<Rightarrow> let C = reduce (map fst (P @ Q)) [] C in if C = [] then ([], [], [([], i)], Suc n) else if is_tautology C \<or> subsume (map fst (P @ Q)) C then (N, P, Q, n) else let P = reduce_all C P; (back_to_P, Q) = reduce_all2 C Q; P = back_to_P @ P; Q = filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q; P = filter (Not \<circ> strictly_subsume [C] \<circ> fst) P; P = (C, i) # P in (N, P, Q, n))

goal (1 subgoal):
 1. \<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = []) \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
proof (cases N)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. N = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
case n_nil: Nil
[PROOF STATE]
proof (state)
this:
N = []

goal (2 subgoals):
 1. N = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[unfolded n_nil, simplified]
[PROOF STATE]
proof (state)
this:
St' = (case P of [] \<Rightarrow> ([], P, Q, n) | P0 # P' \<Rightarrow> let (C, i) = select_min_weight_clause P0 P'; N = map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))); P = filter (\<lambda>(D, j). mset D \<noteq> mset C) P; Q = (C, i) # Q; n = Suc n in (N, P, Q, n))

goal (2 subgoals):
 1. N = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
proof (cases P)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<And>a list. P = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
P = []

goal (2 subgoals):
 1. P = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<And>a list. P = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P = []
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
P = []

goal (1 subgoal):
 1. False
[PROOF STEP]
using n_nil nonfinal[unfolded st]
[PROOF STATE]
proof (prove)
using this:
P = []
N = []
\<not> is_final_dstate (N, P, Q, n)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: is_final_dstate.simps)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. P = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<And>a list. P = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
False
St' = (case P of [] \<Rightarrow> ([], P, Q, n) | P0 # P' \<Rightarrow> let (C, i) = select_min_weight_clause P0 P'; N = map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))); P = filter (\<lambda>(D, j). mset D \<noteq> mset C) P; Q = (C, i) # Q; n = Suc n in (N, P, Q, n))

goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'

goal (1 subgoal):
 1. \<And>a list. P = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. P = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
case p_cons: (Cons P0 P')
[PROOF STATE]
proof (state)
this:
P = P0 # P'

goal (1 subgoal):
 1. \<And>a list. P = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[unfolded p_cons list.case, folded p_cons]
[PROOF STATE]
proof (state)
this:
St' = (let (C, i) = select_min_weight_clause P0 P'; N = map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))); P = filter (\<lambda>(D, j). mset D \<noteq> mset C) P; Q = (C, i) # Q; n = Suc n in (N, P, Q, n))

goal (1 subgoal):
 1. \<And>a list. P = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
obtain C :: "'a lclause" and i :: nat where
          ci: "(C, i) = select_min_weight_clause P0 P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C i. (C, i) = select_min_weight_clause P0 P' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.exhaust)
[PROOF STATE]
proof (state)
this:
(C, i) = select_min_weight_clause P0 P'

goal (1 subgoal):
 1. \<And>a list. P = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[unfolded select, simplified]
[PROOF STATE]
proof (state)
this:
St' = (case select_min_weight_clause P0 P' of (C, i) \<Rightarrow> (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))), filter (\<lambda>(D, j). mset D \<noteq> mset C) P, (C, i) # Q, Suc n))

goal (1 subgoal):
 1. \<And>a list. P = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have ci_in: "(C, i) \<in> set P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, i) \<in> set P
[PROOF STEP]
by (rule select_min_weight_clause_in[of P0 P', folded ci p_cons])
[PROOF STATE]
proof (state)
this:
(C, i) \<in> set P

goal (1 subgoal):
 1. \<And>a list. P = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
unfolding st n_nil step p_cons[symmetric] ci[symmetric] prod.case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))), filter (\<lambda>(D, j). mset D \<noteq> mset C) P, (C, i) # Q, Suc n)
[PROOF STEP]
by (rule tranclp.r_into_trancl, rule compute_inferences[OF ci_in])
            (simp add: select_min_weight_clause_min_weight[OF ci, simplified] p_cons)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
case n_cons: (Cons Ci N')
[PROOF STATE]
proof (state)
this:
N = Ci # N'

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[unfolded n_cons, simplified]
[PROOF STATE]
proof (state)
this:
St' = (case Ci of (C, i) \<Rightarrow> let C = reduce (map fst P @ map fst Q) [] C in if C = [] then ([], [], [([], i)], Suc n) else if is_tautology C \<or> subsume (map fst (P @ Q)) C then (N', P, Q, n) else let P = reduce_all C P; (back_to_P, Q) = reduce_all2 C Q; P = back_to_P @ P; Q = filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q; P = filter (Not \<circ> strictly_subsume [C] \<circ> fst) P; P = (C, i) # P in (N', P, Q, n))

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
obtain C :: "'a lclause" and i :: nat where
        ci: "Ci = (C, i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C i. Ci = (C, i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases Ci) simp
[PROOF STATE]
proof (state)
this:
Ci = (C, i)

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[unfolded ci, simplified]
[PROOF STATE]
proof (state)
this:
St' = (let C = reduce (map fst P @ map fst Q) [] C in if C = [] then ([], [], [([], i)], Suc n) else if is_tautology C \<or> subsume (map fst (P @ Q)) C then (N', P, Q, n) else let P = reduce_all C P; (back_to_P, Q) = reduce_all2 C Q; P = back_to_P @ P; Q = filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q; P = filter (Not \<circ> strictly_subsume [C] \<circ> fst) P; P = (C, i) # P in (N', P, Q, n))

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
define C' :: "'a lclause" where
        "C' = reduce (map fst P @ map fst Q) [] C"
[PROOF STATE]
proof (state)
this:
C' = reduce (map fst P @ map fst Q) [] C

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[unfolded ci C'_def[symmetric], simplified]
[PROOF STATE]
proof (state)
this:
St' = (if C' = [] then ([], [], [([], i)], Suc n) else if is_tautology C' \<or> subsume (map fst (P @ Q)) C' then (N', P, Q, n) else let P = reduce_all C' P; (back_to_P, Q) = reduce_all2 C' Q; P = back_to_P @ P; Q = filter (Not \<circ> strictly_subsume [C'] \<circ> fst) Q; P = filter (Not \<circ> strictly_subsume [C'] \<circ> fst) P; P = (C', i) # P in (N', P, Q, n))

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have "wstate_of_dstate ((E @ C, i) # N', P, Q, n)
           \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E C, i) # N', P, Q, n)" for E
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((E @ C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E C, i) # N', P, Q, n)
[PROOF STEP]
unfolding C'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((E @ C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E C, i) # N', P, Q, n)
[PROOF STEP]
proof (induct C arbitrary: E)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>E. wstate_of_dstate ((E @ [], i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E [], i) # N', P, Q, n)
 2. \<And>a C E. (\<And>E. wstate_of_dstate ((E @ C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E C, i) # N', P, Q, n)) \<Longrightarrow> wstate_of_dstate ((E @ a # C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E (a # C), i) # N', P, Q, n)
[PROOF STEP]
case (Cons L C)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((?E @ C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((?E @ reduce (map fst P @ map fst Q) ?E C, i) # N', P, Q, n)

goal (2 subgoals):
 1. \<And>E. wstate_of_dstate ((E @ [], i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E [], i) # N', P, Q, n)
 2. \<And>a C E. (\<And>E. wstate_of_dstate ((E @ C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E C, i) # N', P, Q, n)) \<Longrightarrow> wstate_of_dstate ((E @ a # C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E (a # C), i) # N', P, Q, n)
[PROOF STEP]
note ih = this(1)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((?E @ C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((?E @ reduce (map fst P @ map fst Q) ?E C, i) # N', P, Q, n)

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

goal (2 subgoals):
 1. is_reducible_lit (map fst P @ map fst Q) (E @ C) L \<Longrightarrow> wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E (L # C), i) # N', P, Q, n)
 2. \<not> is_reducible_lit (map fst P @ map fst Q) (E @ C) L \<Longrightarrow> wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E (L # C), i) # N', P, Q, n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_reducible_lit (map fst P @ map fst Q) (E @ C) L
[PROOF STEP]
have red_lc:
            "reduce (map fst P @ map fst Q) E (L # C) = reduce (map fst P @ map fst Q) E C"
[PROOF STATE]
proof (prove)
using this:
is_reducible_lit (map fst P @ map fst Q) (E @ C) L

goal (1 subgoal):
 1. reduce (map fst P @ map fst Q) E (L # C) = reduce (map fst P @ map fst Q) E C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
reduce (map fst P @ map fst Q) E (L # C) = reduce (map fst P @ map fst Q) E C

goal (2 subgoals):
 1. is_reducible_lit (map fst P @ map fst Q) (E @ C) L \<Longrightarrow> wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E (L # C), i) # N', P, Q, n)
 2. \<not> is_reducible_lit (map fst P @ map fst Q) (E @ C) L \<Longrightarrow> wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E (L # C), i) # N', P, Q, n)
[PROOF STEP]
obtain D D' :: "'a literal list" and L' :: "'a literal" and \<sigma> :: 's where
            "D \<in> set (map fst P @ map fst Q)" and
            "D' = remove1 L' D" and
            "L' \<in> set D" and
            "- L = L' \<cdot>l \<sigma>" and
            "mset D' \<cdot> \<sigma> \<subseteq># mset (E @ C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>D D' L' \<sigma>. \<lbrakk>D \<in> set (map fst P @ map fst Q); D' = remove1 L' D; L' \<in> set D; - L = L' \<cdot>l \<sigma>; mset D' \<cdot> \<sigma> \<subseteq># mset (E @ C)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using l_red
[PROOF STATE]
proof (prove)
using this:
is_reducible_lit (map fst P @ map fst Q) (E @ C) L

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

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

goal (2 subgoals):
 1. is_reducible_lit (map fst P @ map fst Q) (E @ C) L \<Longrightarrow> wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E (L # C), i) # N', P, Q, n)
 2. \<not> is_reducible_lit (map fst P @ map fst Q) (E @ C) L \<Longrightarrow> wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E (L # C), i) # N', P, Q, n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
D \<in> set (map fst P @ map fst Q)
D' = remove1 L' D
L' \<in> set D
- L = L' \<cdot>l \<sigma>
mset D' \<cdot> \<sigma> \<subseteq># mset (E @ C)
[PROOF STEP]
have \<sigma>:
            "mset D' + {#L'#} \<in> set (map (mset \<circ> fst) (P @ Q))"
            "- L = L' \<cdot>l \<sigma> \<and> mset D' \<cdot> \<sigma> \<subseteq># mset (E @ C)"
[PROOF STATE]
proof (prove)
using this:
D \<in> set (map fst P @ map fst Q)
D' = remove1 L' D
L' \<in> set D
- L = L' \<cdot>l \<sigma>
mset D' \<cdot> \<sigma> \<subseteq># mset (E @ C)

goal (1 subgoal):
 1. mset D' + {#L'#} \<in> set (map (mset \<circ> fst) (P @ Q)) &&& - L = L' \<cdot>l \<sigma> \<and> mset D' \<cdot> \<sigma> \<subseteq># mset (E @ C)
[PROOF STEP]
unfolding is_reducible_lit_def
[PROOF STATE]
proof (prove)
using this:
D \<in> set (map fst P @ map fst Q)
D' = remove1 L' D
L' \<in> set D
- L = L' \<cdot>l \<sigma>
mset D' \<cdot> \<sigma> \<subseteq># mset (E @ C)

goal (1 subgoal):
 1. mset D' + {#L'#} \<in> set (map (mset \<circ> fst) (P @ Q)) &&& - L = L' \<cdot>l \<sigma> \<and> mset D' \<cdot> \<sigma> \<subseteq># mset (E @ C)
[PROOF STEP]
by (auto simp: comp_def)
[PROOF STATE]
proof (state)
this:
mset D' + {#L'#} \<in> set (map (mset \<circ> fst) (P @ Q))
- L = L' \<cdot>l \<sigma> \<and> mset D' \<cdot> \<sigma> \<subseteq># mset (E @ C)

goal (2 subgoals):
 1. is_reducible_lit (map fst P @ map fst Q) (E @ C) L \<Longrightarrow> wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E (L # C), i) # N', P, Q, n)
 2. \<not> is_reducible_lit (map fst P @ map fst Q) (E @ C) L \<Longrightarrow> wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E (L # C), i) # N', P, Q, n)
[PROOF STEP]
have "wstate_of_dstate ((E @ L # C, i) # N', P, Q, n)
              \<leadsto>\<^sub>w wstate_of_dstate ((E @ C, i) # N', P, Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate ((E @ C, i) # N', P, Q, n)
[PROOF STEP]
by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
                  wrp.forward_reduction[of "mset D'" L' "mset (map (apfst mset) P)"
                    "mset (map (apfst mset) Q)" L \<sigma> "mset (E @ C)" "mset (map (apfst mset) N')"
                    i n]])
              (use \<sigma> in \<open>auto simp: comp_def\<close>)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate ((E @ C, i) # N', P, Q, n)

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

goal (1 subgoal):
 1. wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E (L # C), i) # N', P, Q, n)
[PROOF STEP]
unfolding red_lc
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate ((E @ L # C, i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate ((E @ C, i) # N', P, Q, n)

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>E. wstate_of_dstate ((E @ [], i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E [], i) # N', P, Q, n)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((?E @ C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((?E @ reduce (map fst P @ map fst Q) ?E C, i) # N', P, Q, n)

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate ((?E @ C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((?E @ reduce (map fst P @ map fst Q) ?E C, i) # N', P, Q, n)
[PROOF STEP]
have red_C:
        "wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P, Q, n)"
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate ((?E @ C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((?E @ reduce (map fst P @ map fst Q) ?E C, i) # N', P, Q, n)

goal (1 subgoal):
 1. wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P, Q, n)
[PROOF STEP]
unfolding C'_def
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate ((?E @ C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((?E @ reduce (map fst P @ map fst Q) ?E C, i) # N', P, Q, n)

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

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have proc_C: "wstate_of_dstate ((C', i) # N', P', Q', n')
          \<leadsto>\<^sub>w wstate_of_dstate (N', (C', i) # P', Q', n')" for P' Q' n'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((C', i) # N', P', Q', n') \<leadsto>\<^sub>w wstate_of_dstate (N', (C', i) # P', Q', n')
[PROOF STEP]
by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
              wrp.clause_processing[of "mset (map (apfst mset) N')" "mset C'" i
                "mset (map (apfst mset) P')" "mset (map (apfst mset) Q')" n']],
            simp+)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', ?P', ?Q', ?n') \<leadsto>\<^sub>w wstate_of_dstate (N', (C', i) # ?P', ?Q', ?n')

goal (1 subgoal):
 1. \<And>a list. N = a # list \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
proof (cases "C' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
C' = []

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note c'_nil = this
[PROOF STATE]
proof (state)
this:
C' = []

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[simplified c'_nil, simplified]
[PROOF STATE]
proof (state)
this:
St' = ([], [], [([], i)], Suc n)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have
          filter_p: "filter (Not \<circ> strictly_subsume [[]] \<circ> fst) P = []" and
          filter_q: "filter (Not \<circ> strictly_subsume [[]] \<circ> fst) Q = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (Not \<circ> strictly_subsume [[]] \<circ> fst) P = [] &&& filter (Not \<circ> strictly_subsume [[]] \<circ> fst) Q = []
[PROOF STEP]
using nil_ni
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = [])

goal (1 subgoal):
 1. filter (Not \<circ> strictly_subsume [[]] \<circ> fst) P = [] &&& filter (Not \<circ> strictly_subsume [[]] \<circ> fst) Q = []
[PROOF STEP]
unfolding strictly_subsume_def filter_empty_conv find_None_iff
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>Ci\<in>set P \<union> set Q. fst Ci = [])

goal (1 subgoal):
 1. \<forall>x\<in>set P. \<not> (Not \<circ> (\<lambda>C. \<exists>D\<in>set [[]]. strictly_subsumes (mset D) (mset C)) \<circ> fst) x &&& \<forall>x\<in>set Q. \<not> (Not \<circ> (\<lambda>C. \<exists>D\<in>set [[]]. strictly_subsumes (mset D) (mset C)) \<circ> fst) x
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
filter (Not \<circ> strictly_subsume [[]] \<circ> fst) P = []
filter (Not \<circ> strictly_subsume [[]] \<circ> fst) Q = []

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note red_C[unfolded c'_nil]
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', P, Q, n)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', P, Q, n)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have "wstate_of_dstate (([], i) # N', P, Q, n)
            \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', [], Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (([], i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', [], Q, n)
[PROOF STEP]
by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
                remove_strictly_subsumed_clauses_in_P[of "[]" _ "[]", unfolded append_Nil],
                OF refl])
            (auto simp: filter_p)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (([], i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', [], Q, n)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (([], i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', [], Q, n)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have "\<dots> \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', [], [], n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (([], i) # N', [], Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', [], [], n)
[PROOF STEP]
by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
                remove_strictly_subsumed_clauses_in_Q[of "[]" _ _ "[]", unfolded append_Nil],
                OF refl])
            (auto simp: filter_q)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (([], i) # N', [], Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', [], [], n)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (([], i) # N', [], Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', [], [], n)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note proc_C[unfolded c'_nil, THEN tranclp.r_into_trancl[of "(\<leadsto>\<^sub>w)"]]
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (([], i) # N', ?P'1, ?Q'1, ?n'1) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (N', ([], i) # ?P'1, ?Q'1, ?n'1)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (([], i) # N', ?P'1, ?Q'1, ?n'1) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (N', ([], i) # ?P'1, ?Q'1, ?n'1)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have "wstate_of_dstate (N', [([], i)], [], n)
            \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [([], i)], [], n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate (N', [([], i)], [], n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [([], i)], [], n)
[PROOF STEP]
by (rule empty_N_if_Nil_in_P_or_Q) simp
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N', [([], i)], [], n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [([], i)], [], n)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate (N', [([], i)], [], n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [([], i)], [], n)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have "\<dots> \<leadsto>\<^sub>w wstate_of_dstate ([], [], [([], i)], Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ([], [([], i)], [], n) \<leadsto>\<^sub>w wstate_of_dstate ([], [], [([], i)], Suc n)
[PROOF STEP]
by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
                wrp.inference_computation[of "{#}" "{#}" i "{#}" n "{#}"]])
            (auto simp: ord_FO_resolution_inferences_between_empty_empty)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ([], [([], i)], [], n) \<leadsto>\<^sub>w wstate_of_dstate ([], [], [([], i)], Suc n)

goal (2 subgoals):
 1. C' = [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate ([], [], [([], i)], Suc n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate ([], [], [([], i)], Suc n)

goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
unfolding step st n_cons ci
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate ([], [], [([], i)], Suc n)

goal (1 subgoal):
 1. wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate ([], [], [([], i)], Suc n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'

goal (1 subgoal):
 1. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
case c'_nnil: False
[PROOF STATE]
proof (state)
this:
C' \<noteq> []

goal (1 subgoal):
 1. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[simplified c'_nnil, simplified]
[PROOF STATE]
proof (state)
this:
St' = (if is_tautology C' \<or> subsume (map fst P @ map fst Q) C' then (N', P, Q, n) else let P = reduce_all C' P; (back_to_P, Q) = reduce_all2 C' Q; P = back_to_P @ P; Q = filter (Not \<circ> strictly_subsume [C'] \<circ> fst) Q; P = filter (Not \<circ> strictly_subsume [C'] \<circ> fst) P; P = (C', i) # P in (N', P, Q, n))

goal (1 subgoal):
 1. C' \<noteq> [] \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
proof (cases "is_tautology C' \<or> subsume (map fst P @ map fst Q) C'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_tautology C' \<or> subsume (map fst P @ map fst Q) C' \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
case taut_or_subs: True
[PROOF STATE]
proof (state)
this:
is_tautology C' \<or> subsume (map fst P @ map fst Q) C'

goal (2 subgoals):
 1. is_tautology C' \<or> subsume (map fst P @ map fst Q) C' \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[simplified taut_or_subs, simplified]
[PROOF STATE]
proof (state)
this:
St' = (N', P, Q, n)

goal (2 subgoals):
 1. is_tautology C' \<or> subsume (map fst P @ map fst Q) C' \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have "wstate_of_dstate ((C', i) # 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 ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
[PROOF STEP]
proof (cases "is_tautology C'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_tautology C' \<Longrightarrow> wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
 2. \<not> is_tautology C' \<Longrightarrow> wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_tautology C'

goal (2 subgoals):
 1. is_tautology C' \<Longrightarrow> wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
 2. \<not> is_tautology C' \<Longrightarrow> wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_tautology C'
[PROOF STEP]
obtain A :: 'a where
              neg_a: "Neg A \<in> set C'" and pos_a: "Pos A \<in> set C'"
[PROOF STATE]
proof (prove)
using this:
is_tautology C'

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>Neg A \<in> set C'; Pos A \<in> set C'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_tautology_def
[PROOF STATE]
proof (prove)
using this:
\<exists>A\<in>set (map atm_of C'). Pos A \<in> set C' \<and> Neg A \<in> set C'

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>Neg A \<in> set C'; Pos A \<in> set C'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg A \<in> set C'
Pos A \<in> set C'

goal (2 subgoals):
 1. is_tautology C' \<Longrightarrow> wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
 2. \<not> is_tautology C' \<Longrightarrow> wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((C', i) # 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.tautology_deletion[of A "mset C'" "mset (map (apfst mset) N')" i
                      "mset (map (apfst mset) P)" "mset (map (apfst mset) Q)" n]])
                (use neg_a pos_a in simp_all)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)

goal (1 subgoal):
 1. \<not> is_tautology C' \<Longrightarrow> wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_tautology C' \<Longrightarrow> wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_tautology C'

goal (1 subgoal):
 1. \<not> is_tautology C' \<Longrightarrow> wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> is_tautology C'
[PROOF STEP]
have "subsume (map fst P @ map fst Q) C'"
[PROOF STATE]
proof (prove)
using this:
\<not> is_tautology C'

goal (1 subgoal):
 1. subsume (map fst P @ map fst Q) C'
[PROOF STEP]
using taut_or_subs
[PROOF STATE]
proof (prove)
using this:
\<not> is_tautology C'
is_tautology C' \<or> subsume (map fst P @ map fst Q) C'

goal (1 subgoal):
 1. subsume (map fst P @ map fst Q) C'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
subsume (map fst P @ map fst Q) C'

goal (1 subgoal):
 1. \<not> is_tautology C' \<Longrightarrow> wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subsume (map fst P @ map fst Q) C'
[PROOF STEP]
obtain D :: "'a lclause" where
              d_in: "D \<in> set (map fst P @ map fst Q)" and
              subs: "subsumes (mset D) (mset C')"
[PROOF STATE]
proof (prove)
using this:
subsume (map fst P @ map fst Q) C'

goal (1 subgoal):
 1. (\<And>D. \<lbrakk>D \<in> set (map fst P @ map fst Q); subsumes (mset D) (mset C')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding subsume_def
[PROOF STATE]
proof (prove)
using this:
\<exists>D\<in>set (map fst P @ map fst Q). subsumes (mset D) (mset C')

goal (1 subgoal):
 1. (\<And>D. \<lbrakk>D \<in> set (map fst P @ map fst Q); subsumes (mset D) (mset C')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
D \<in> set (map fst P @ map fst Q)
subsumes (mset D) (mset C')

goal (1 subgoal):
 1. \<not> is_tautology C' \<Longrightarrow> wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((C', i) # 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 D" "mset (map (apfst mset) P)"
                      "mset (map (apfst mset) Q)" "mset C'" "mset (map (apfst mset) N')" i n]],
                  use d_in subs in \<open>auto simp: subsume_def\<close>)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)

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

goal (2 subgoals):
 1. is_tautology C' \<or> subsume (map fst P @ map fst Q) C' \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
 2. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)

goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
unfolding step st n_cons ci
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)

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

goal (1 subgoal):
 1. wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (N', P, Q, n)
[PROOF STEP]
by (rule rtranclp_into_tranclp1[rotated])
[PROOF STATE]
proof (state)
this:
wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
case not_taut_or_subs: False
[PROOF STATE]
proof (state)
this:
\<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C')

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[simplified not_taut_or_subs, simplified]
[PROOF STATE]
proof (state)
this:
St' = (case reduce_all2 C' Q of (back_to_P, Q) \<Rightarrow> (N', (C', i) # filter (Not \<circ> strictly_subsume [C'] \<circ> fst) back_to_P @ filter (Not \<circ> strictly_subsume [C'] \<circ> fst) (reduce_all C' P), filter (Not \<circ> strictly_subsume [C'] \<circ> fst) Q, n))

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
define P' :: "('a literal list \<times> nat) list" where
            "P' = reduce_all C' P"
[PROOF STATE]
proof (state)
this:
P' = reduce_all C' P

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
obtain back_to_P Q' :: "'a dclause list" where
            red_Q: "(back_to_P, Q') = reduce_all2 C' Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>back_to_P Q'. (back_to_P, Q') = reduce_all2 C' Q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.exhaust)
[PROOF STATE]
proof (state)
this:
(back_to_P, Q') = reduce_all2 C' Q

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[unfolded red_Q[symmetric], simplified]
[PROOF STATE]
proof (state)
this:
St' = (N', (C', i) # filter (Not \<circ> strictly_subsume [C'] \<circ> fst) back_to_P @ filter (Not \<circ> strictly_subsume [C'] \<circ> fst) (reduce_all C' P), filter (Not \<circ> strictly_subsume [C'] \<circ> fst) Q', n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
define Q'' :: "('a literal list \<times> nat) list" where
            "Q'' = filter (Not \<circ> strictly_subsume [C'] \<circ> fst) Q'"
[PROOF STATE]
proof (state)
this:
Q'' = filter (Not \<circ> strictly_subsume [C'] \<circ> fst) Q'

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
define P'' :: "('a literal list \<times> nat) list" where
            "P'' = filter (Not \<circ> strictly_subsume [C'] \<circ> fst) (back_to_P @ P')"
[PROOF STATE]
proof (state)
this:
P'' = filter (Not \<circ> strictly_subsume [C'] \<circ> fst) (back_to_P @ P')

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note step = step[unfolded P'_def[symmetric] Q''_def[symmetric] P''_def[symmetric],
              simplified]
[PROOF STATE]
proof (state)
this:
St' = (N', (C', i) # filter (Not \<circ> strictly_subsume [C'] \<circ> fst) back_to_P @ filter (Not \<circ> strictly_subsume [C'] \<circ> fst) P', Q'', n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note red_C
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P, Q, n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P, Q, n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have "wstate_of_dstate ((C', i) # N', P, Q, n)
              \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P', Q, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P', Q, n)
[PROOF STEP]
unfolding P'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', reduce_all C' P, Q, n)
[PROOF STEP]
by (rule reduce_clauses_in_P[of _ _ "[]", unfolded append_Nil]) simp+
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P', Q, n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P', Q, n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have "\<dots> \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q', n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((C', i) # N', P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q', n)
[PROOF STEP]
unfolding P'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((C', i) # N', reduce_all C' P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ reduce_all C' P, Q', n)
[PROOF STEP]
by (rule reduce_clauses_in_Q[of C' _ _ "[]" Q, folded red_Q,
                  unfolded append_Nil prod.sel])
              (auto intro: reduce_idem simp: reduce_all_def)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q', n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q', n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have "\<dots> \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q'', n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((C', i) # N', back_to_P @ P', Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q'', n)
[PROOF STEP]
unfolding Q''_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((C', i) # N', back_to_P @ P', Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ P', filter (Not \<circ> strictly_subsume [C'] \<circ> fst) Q', n)
[PROOF STEP]
by (rule remove_strictly_subsumed_clauses_in_Q[of _ _ _ "[]", unfolded append_Nil])
              simp
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', back_to_P @ P', Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q'', n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', back_to_P @ P', Q', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q'', n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
have "\<dots> \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P'', Q'', n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((C', i) # N', back_to_P @ P', Q'', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P'', Q'', n)
[PROOF STEP]
unfolding P''_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ((C', i) # N', back_to_P @ P', Q'', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', filter (Not \<circ> strictly_subsume [C'] \<circ> fst) (back_to_P @ P'), Q'', n)
[PROOF STEP]
by (rule remove_strictly_subsumed_clauses_in_P[of _ _ "[]", unfolded append_Nil]) auto
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', back_to_P @ P', Q'', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P'', Q'', n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', back_to_P @ P', Q'', n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P'', Q'', n)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
note proc_C[THEN tranclp.r_into_trancl[of "(\<leadsto>\<^sub>w)"]]
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ((C', i) # N', ?P'1, ?Q'1, ?n'1) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (N', (C', i) # ?P'1, ?Q'1, ?n'1)

goal (1 subgoal):
 1. \<not> (is_tautology C' \<or> subsume (map fst P @ map fst Q) C') \<Longrightarrow> wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (N', (C', i) # P'', Q'', n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (N', (C', i) # P'', Q'', n)

goal (1 subgoal):
 1. wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'
[PROOF STEP]
unfolding step st n_cons ci P''_def
[PROOF STATE]
proof (prove)
using this:
wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (N', (C', i) # filter (Not \<circ> strictly_subsume [C'] \<circ> fst) (back_to_P @ P'), Q'', n)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma final_deterministic_RP_step: "is_final_dstate St \<Longrightarrow> deterministic_RP_step St = St"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_final_dstate St \<Longrightarrow> deterministic_RP_step St = St
[PROOF STEP]
by (cases St) (auto simp: deterministic_RP_step.simps is_final_dstate.simps)