[STATEMENT]
lemma ord_FO_\<Gamma>_infer_from_Collect_eq:
  "{\<gamma> \<in> ord_FO_\<Gamma> S. infer_from (DD \<union> {C}) \<gamma> \<and> C \<in># prems_of \<gamma>} =
   {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D \<in> DD \<union> {C}. prems_of \<gamma> = {#C, D#}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<gamma> \<in> ord_FO_\<Gamma> S. infer_from (DD \<union> {C}) \<gamma> \<and> C \<in># prems_of \<gamma>} = {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>DD \<union> {C}. prems_of \<gamma> = {#C, D#}}
[PROOF STEP]
unfolding infer_from_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<gamma> \<in> ord_FO_\<Gamma> S. set_mset (prems_of \<gamma>) \<subseteq> DD \<union> {C} \<and> C \<in># prems_of \<gamma>} = {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>DD \<union> {C}. prems_of \<gamma> = {#C, D#}}
[PROOF STEP]
apply (rule set_eq_subset[THEN iffD2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<gamma> \<in> ord_FO_\<Gamma> S. set_mset (prems_of \<gamma>) \<subseteq> DD \<union> {C} \<and> C \<in># prems_of \<gamma>} \<subseteq> {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>DD \<union> {C}. prems_of \<gamma> = {#C, D#}} \<and> {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>DD \<union> {C}. prems_of \<gamma> = {#C, D#}} \<subseteq> {\<gamma> \<in> ord_FO_\<Gamma> S. set_mset (prems_of \<gamma>) \<subseteq> DD \<union> {C} \<and> C \<in># prems_of \<gamma>}
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {\<gamma> \<in> ord_FO_\<Gamma> S. set_mset (prems_of \<gamma>) \<subseteq> DD \<union> {C} \<and> C \<in># prems_of \<gamma>} \<subseteq> {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>DD \<union> {C}. prems_of \<gamma> = {#C, D#}}
 2. {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>DD \<union> {C}. prems_of \<gamma> = {#C, D#}} \<subseteq> {\<gamma> \<in> ord_FO_\<Gamma> S. set_mset (prems_of \<gamma>) \<subseteq> DD \<union> {C} \<and> C \<in># prems_of \<gamma>}
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> ord_FO_\<Gamma> S; set_mset (prems_of x) \<subseteq> DD \<union> {C}; C \<in># prems_of x\<rbrakk> \<Longrightarrow> \<exists>D\<in>DD \<union> {C}. prems_of x = {#C, D#}
 2. {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>DD \<union> {C}. prems_of \<gamma> = {#C, D#}} \<subseteq> {\<gamma> \<in> ord_FO_\<Gamma> S. set_mset (prems_of \<gamma>) \<subseteq> DD \<union> {C} \<and> C \<in># prems_of \<gamma>}
[PROOF STEP]
apply (subst (asm) (1 2) ord_FO_\<Gamma>_side_prem, assumption, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> ord_FO_\<Gamma> S; set_mset ({#THE D. D \<in># side_prems_of x#} + {#main_prem_of x#}) \<subseteq> DD \<union> {C}; C \<in># {#THE D. D \<in># side_prems_of x#} + {#main_prem_of x#}\<rbrakk> \<Longrightarrow> \<exists>D\<in>DD \<union> {C}. prems_of x = {#C, D#}
 2. {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>DD \<union> {C}. prems_of \<gamma> = {#C, D#}} \<subseteq> {\<gamma> \<in> ord_FO_\<Gamma> S. set_mset (prems_of \<gamma>) \<subseteq> DD \<union> {C} \<and> C \<in># prems_of \<gamma>}
[PROOF STEP]
apply (subst (1) ord_FO_\<Gamma>_side_prem, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> ord_FO_\<Gamma> S; set_mset ({#THE D. D \<in># side_prems_of x#} + {#main_prem_of x#}) \<subseteq> DD \<union> {C}; C \<in># {#THE D. D \<in># side_prems_of x#} + {#main_prem_of x#}\<rbrakk> \<Longrightarrow> \<exists>D\<in>DD \<union> {C}. {#THE D. D \<in># side_prems_of x#} + {#main_prem_of x#} = {#C, D#}
 2. {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>DD \<union> {C}. prems_of \<gamma> = {#C, D#}} \<subseteq> {\<gamma> \<in> ord_FO_\<Gamma> S. set_mset (prems_of \<gamma>) \<subseteq> DD \<union> {C} \<and> C \<in># prems_of \<gamma>}
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>DD \<union> {C}. prems_of \<gamma> = {#C, D#}} \<subseteq> {\<gamma> \<in> ord_FO_\<Gamma> S. set_mset (prems_of \<gamma>) \<subseteq> DD \<union> {C} \<and> C \<in># prems_of \<gamma>}
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x D. \<lbrakk>x \<in> ord_FO_\<Gamma> S; D \<in> DD \<union> {C}; prems_of x = {#C, D#}\<rbrakk> \<Longrightarrow> set_mset (prems_of x) \<subseteq> DD \<union> {C} \<and> C \<in># prems_of x
[PROOF STEP]
apply (subst (asm) (1) ord_FO_\<Gamma>_side_prem, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x D. \<lbrakk>x \<in> ord_FO_\<Gamma> S; D \<in> DD \<union> {C}; {#THE D. D \<in># side_prems_of x#} + {#main_prem_of x#} = {#C, D#}\<rbrakk> \<Longrightarrow> set_mset (prems_of x) \<subseteq> DD \<union> {C} \<and> C \<in># prems_of x
[PROOF STEP]
apply (subst (1 2) ord_FO_\<Gamma>_side_prem, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x D. \<lbrakk>x \<in> ord_FO_\<Gamma> S; D \<in> DD \<union> {C}; {#THE D. D \<in># side_prems_of x#} + {#main_prem_of x#} = {#C, D#}\<rbrakk> \<Longrightarrow> set_mset ({#THE D. D \<in># side_prems_of x#} + {#main_prem_of x#}) \<subseteq> DD \<union> {C} \<and> C \<in># {#THE D. D \<in># side_prems_of x#} + {#main_prem_of x#}
[PROOF STEP]
by force


[STATEMENT]
lemma inferences_between_eq_UNION: "inference_system.inferences_between (ord_FO_\<Gamma> S) Q C =
  inference_system.inferences_between (ord_FO_\<Gamma> S) {C} C
  \<union> (\<Union>D \<in> Q. inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inference_system.inferences_between (ord_FO_\<Gamma> S) Q C = inference_system.inferences_between (ord_FO_\<Gamma> S) {C} C \<union> (\<Union>D\<in>Q. inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)
[PROOF STEP]
unfolding ord_FO_\<Gamma>_infer_from_Collect_eq inference_system.inferences_between_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>Q \<union> {C}. prems_of \<gamma> = {#C, D#}} = {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>{C} \<union> {C}. prems_of \<gamma> = {#C, D#}} \<union> (\<Union>D\<in>Q. {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D\<in>{D} \<union> {C}. prems_of \<gamma> = {#C, D#}})
[PROOF STEP]
by auto


[STATEMENT]
lemma concls_of_inferences_between_singleton_eq_Bin_ord_resolve_rename:
  "concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C) =
   Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C) = Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C
[PROOF STEP]
proof (intro order_antisym subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C) \<Longrightarrow> x \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C
 2. \<And>x. x \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C \<Longrightarrow> x \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)
[PROOF STEP]
fix E
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C) \<Longrightarrow> x \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C
 2. \<And>x. x \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C \<Longrightarrow> x \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)
[PROOF STEP]
assume e_in: "E \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)"
[PROOF STATE]
proof (state)
this:
E \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)

goal (2 subgoals):
 1. \<And>x. x \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C) \<Longrightarrow> x \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C
 2. \<And>x. x \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C \<Longrightarrow> x \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
E \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)
[PROOF STEP]
show "E \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D
    \<union> Bin_ord_resolve_rename D C"
[PROOF STATE]
proof (prove)
using this:
E \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)

goal (1 subgoal):
 1. E \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C
[PROOF STEP]
unfolding inference_system.inferences_between_def ord_FO_\<Gamma>_infer_from_Collect_eq
      bin_ord_FO_\<Gamma>_def infer_from_def
[PROOF STATE]
proof (prove)
using this:
E \<in> concls_of {\<gamma> \<in> {uu_. \<exists>CA DA AA A \<sigma> E. uu_ = Infer {#CA#} DA E \<and> ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E}. set_mset (prems_of \<gamma>) \<subseteq> {D} \<union> {C} \<and> C \<in># prems_of \<gamma>}

goal (1 subgoal):
 1. E \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C
[PROOF STEP]
by (fastforce simp: add_mset_eq_add_mset)
[PROOF STATE]
proof (state)
this:
E \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C

goal (1 subgoal):
 1. \<And>x. x \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C \<Longrightarrow> x \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)
[PROOF STEP]
qed (force simp: inference_system.inferences_between_def infer_from_def ord_FO_\<Gamma>_def)


[STATEMENT]
lemma concls_of_inferences_between_eq_Bin_ord_resolve_rename:
  "concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) Q C) =
   Bin_ord_resolve_rename C C \<union> (\<Union>D \<in> Q. Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) Q C) = Bin_ord_resolve_rename C C \<union> (\<Union>D\<in>Q. Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C)
[PROOF STEP]
by (subst inferences_between_eq_UNION)
    (auto simp: image_Un image_UN concls_of_inferences_between_singleton_eq_Bin_ord_resolve_rename)


[STATEMENT]
lemma resolve_rename_either_way_eq_congls_of_inferences_between:
  "mset ` set (resolve_rename C C) \<union> (\<Union>D \<in> Q. mset ` set (resolve_rename_either_way C D)) =
   concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (mset ` Q) (mset C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset ` set (resolve_rename C C) \<union> (\<Union>D\<in>Q. mset ` set (resolve_rename_either_way C D)) = concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (mset ` Q) (mset C))
[PROOF STEP]
by (simp add: resolve_rename_either_way_def image_Un resolve_rename_eq_Bin_ord_resolve_rename
      concls_of_inferences_between_eq_Bin_ord_resolve_rename UN_Un_distrib)


[STATEMENT]
lemma compute_inferences:
  assumes
    ci_in: "(C, i) \<in> set P" and
    ci_min: "\<forall>(D, j) \<in># mset (map (apfst mset) P). weight (mset C, i) \<le> weight (D, j)"
  shows
    "wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w
     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)"
    (is "_ \<leadsto>\<^sub>w wstate_of_dstate (?N, _)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w 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]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w 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]
have ms_ci_in: "(mset C, i) \<in># image_mset (apfst mset) (mset P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mset C, i) \<in># image_mset (apfst mset) (mset P)
[PROOF STEP]
using ci_in
[PROOF STATE]
proof (prove)
using this:
(C, i) \<in> set P

goal (1 subgoal):
 1. (mset C, i) \<in># image_mset (apfst mset) (mset P)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(mset C, i) \<in># image_mset (apfst mset) (mset P)

goal (1 subgoal):
 1. wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w 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]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w 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]
apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
          wrp.inference_computation[of "mset (map (apfst mset) P) - {#(mset C, i)#}" "mset C" i
            "mset (map (apfst mset) ?N)" n "mset (map (apfst mset) Q)"]])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. ({#}, remove1_mset (mset C, i) (mset (map (apfst mset) P)) + {#(mset C, i)#}, mset (map (apfst mset) Q), n) = wstate_of_dstate ([], P, Q, n)
 2. (mset (map (apfst mset) (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))))), {#(D, j) \<in># remove1_mset (mset C, i) (mset (map (apfst mset) P)). D \<noteq> mset C#}, mset (map (apfst mset) Q) + {#(mset C, i)#}, Suc n) = 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)
 3. \<forall>(D, j)\<in>#remove1_mset (mset C, i) (mset (map (apfst mset) P)). weight (mset C, i) \<le> weight (D, j)
 4. mset (map (apfst mset) (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))))) = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
apply (simp add: add_mset_remove_trivial_eq[THEN iffD2, OF ms_ci_in, symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (mset (map (apfst mset) (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))))), {#(D, j) \<in># remove1_mset (mset C, i) (mset (map (apfst mset) P)). D \<noteq> mset C#}, mset (map (apfst mset) Q) + {#(mset C, i)#}, Suc n) = 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)
 2. \<forall>(D, j)\<in>#remove1_mset (mset C, i) (mset (map (apfst mset) P)). weight (mset C, i) \<le> weight (D, j)
 3. mset (map (apfst mset) (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))))) = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
using ms_ci_in
[PROOF STATE]
proof (prove)
using this:
(mset C, i) \<in># image_mset (apfst mset) (mset P)

goal (3 subgoals):
 1. (mset (map (apfst mset) (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))))), {#(D, j) \<in># remove1_mset (mset C, i) (mset (map (apfst mset) P)). D \<noteq> mset C#}, mset (map (apfst mset) Q) + {#(mset C, i)#}, Suc n) = 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)
 2. \<forall>(D, j)\<in>#remove1_mset (mset C, i) (mset (map (apfst mset) P)). weight (mset C, i) \<le> weight (D, j)
 3. mset (map (apfst mset) (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))))) = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
apply (simp add: ci_in image_mset_remove1_mset_if)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (mset C, i) \<in> apfst mset ` set P \<Longrightarrow> {#(D, j) \<in># image_mset (apfst mset) (mset P). D \<noteq> mset C#} = image_mset (apfst mset) {#(D, j) \<in># mset P. mset D \<noteq> mset C#}
 2. \<forall>(D, j)\<in>#remove1_mset (mset C, i) (mset (map (apfst mset) P)). weight (mset C, i) \<le> weight (D, j)
 3. mset (map (apfst mset) (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))))) = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
apply (smt apfst_conv case_prodE case_prodI2 case_prod_conv filter_mset_cong
        image_mset_filter_swap mset_filter)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>(D, j)\<in>#remove1_mset (mset C, i) (mset (map (apfst mset) P)). weight (mset C, i) \<le> weight (D, j)
 2. mset (map (apfst mset) (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))))) = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
apply (metis ci_min in_diffD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (map (apfst mset) (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))))) = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
apply (simp only: list.map_comp apfst_comp_rpair_const)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (map ((\<lambda>D. (D, n)) \<circ> mset) (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q)))) = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
apply (simp only: list.map_comp[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (map (\<lambda>D. (D, n)) (map mset (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C) (map fst Q)))))) = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
apply (subst mset_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#(D, n). D \<in># mset (map mset (remdups_gen mset (resolve_rename C C @ concat (map (resolve_rename_either_way C) (map fst Q)))))#} = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
apply (unfold mset_map_remdups_gen mset_remdups_gen_ident)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#(D, n). D \<in># mset_set (set (map mset (resolve_rename C C @ concat (map (resolve_rename_either_way C) (map fst Q)))))#} = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
apply (subst image_mset_mset_set)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. inj_on (\<lambda>D. (D, n)) (set (map mset (resolve_rename C C @ concat (map (resolve_rename_either_way C) (map fst Q)))))
 2. mset_set ((\<lambda>D. (D, n)) ` set (map mset (resolve_rename C C @ concat (map (resolve_rename_either_way C) (map fst Q))))) = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
apply (simp add: inj_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_set ((\<lambda>D. (D, n)) ` set (map mset (resolve_rename C C @ concat (map (resolve_rename_either_way C) (map fst Q))))) = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
[PROOF STEP]
apply (subst mset_set_eq_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite ((\<lambda>D. (D, n)) ` set (map mset (resolve_rename C C @ concat (map (resolve_rename_either_way C) (map fst Q)))))
 2. finite ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
 3. (\<lambda>D. (D, n)) ` set (map mset (resolve_rename C C @ concat (map (resolve_rename_either_way C) (map fst Q)))) = (\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C)))
 2. (\<lambda>D. (D, n)) ` set (map mset (resolve_rename C C @ concat (map (resolve_rename_either_way C) (map fst Q)))) = (\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C))
[PROOF STEP]
apply (simp add: finite_ord_FO_resolution_inferences_between)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>D. (D, n)) ` set (map mset (resolve_rename C C @ concat (map (resolve_rename_either_way C) (map fst Q)))) = (\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C))
[PROOF STEP]
apply (rule arg_cong[of _ _ "\<lambda>N. (\<lambda>D. (D, n)) ` N"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map mset (resolve_rename C C @ concat (map (resolve_rename_either_way C) (map fst Q)))) = concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C))
[PROOF STEP]
apply (simp only: map_concat list.map_comp image_comp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))) = concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C))
[PROOF STEP]
using resolve_rename_either_way_eq_congls_of_inferences_between[of C "fst ` set Q", symmetric]
[PROOF STATE]
proof (prove)
using this:
concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (mset ` fst ` set Q) (mset C)) = mset ` set (resolve_rename C C) \<union> (\<Union>D\<in>fst ` set Q. mset ` set (resolve_rename_either_way C D))

goal (1 subgoal):
 1. set (map mset (resolve_rename C C @ concat (map (resolve_rename_either_way C \<circ> fst) Q))) = concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst (mset (map (apfst mset) Q)))) (mset C))
[PROOF STEP]
by (simp add: image_comp comp_def image_UN)
[PROOF STATE]
proof (state)
this:
wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w 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)

goal:
No subgoals!
[PROOF STEP]
qed