[STATEMENT]
lemma resolve_on_eq_UNION_Bin_ord_resolve:
  "mset ` set (resolve_on A D CA) =
   {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset ` set (resolve_on A D CA) = {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
fix E :: "'a literal list"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
assume "E \<in> set (resolve_on A D CA)"
[PROOF STATE]
proof (state)
this:
E \<in> set (resolve_on A D CA)

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
E \<in> set (resolve_on A D CA)
[PROOF STEP]
have "E \<in> resolvent D A CA ` {Ls. subseq Ls CA \<and> resolvable A D CA Ls}"
[PROOF STATE]
proof (prove)
using this:
E \<in> set (resolve_on A D CA)

goal (1 subgoal):
 1. E \<in> resolvent D A CA ` {Ls. subseq Ls CA \<and> resolvable A D CA Ls}
[PROOF STEP]
unfolding resolve_on_def
[PROOF STATE]
proof (prove)
using this:
E \<in> set (map (resolvent D A CA) (filter (resolvable A D CA) (subseqs CA)))

goal (1 subgoal):
 1. E \<in> resolvent D A CA ` {Ls. subseq Ls CA \<and> resolvable A D CA Ls}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E \<in> resolvent D A CA ` {Ls. subseq Ls CA \<and> resolvable A D CA Ls}

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
E \<in> resolvent D A CA ` {Ls. subseq Ls CA \<and> resolvable A D CA Ls}
[PROOF STEP]
obtain Ls where Ls_p: "resolvent D A CA Ls = E" "subseq Ls CA \<and> resolvable A D CA Ls"
[PROOF STATE]
proof (prove)
using this:
E \<in> resolvent D A CA ` {Ls. subseq Ls CA \<and> resolvable A D CA Ls}

goal (1 subgoal):
 1. (\<And>Ls. \<lbrakk>resolvent D A CA Ls = E; subseq Ls CA \<and> resolvable A D CA Ls\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
resolvent D A CA Ls = E
subseq Ls CA \<and> resolvable A D CA Ls

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
define \<sigma> where "\<sigma> = the (mgu {insert A (atms_of (mset Ls))})"
[PROOF STATE]
proof (state)
this:
\<sigma> = the (mgu {insert A (atms_of (mset Ls))})

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<sigma> = the (mgu {insert A (atms_of (mset Ls))})
[PROOF STEP]
have \<sigma>_p:
      "mgu {insert A (atms_of (mset Ls))} = Some \<sigma>"
      "Ls \<noteq> []"
      "eligible S \<sigma> [A] (add_mset (Neg A) (mset D))"
      "strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>)"
      "\<forall>L \<in> set Ls. is_pos L"
[PROOF STATE]
proof (prove)
using this:
\<sigma> = the (mgu {insert A (atms_of (mset Ls))})

goal (1 subgoal):
 1. (mgu {insert A (atms_of (mset Ls))} = Some \<sigma> &&& Ls \<noteq> []) &&& eligible S \<sigma> [A] (add_mset (Neg A) (mset D)) &&& strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>) &&& \<forall>L\<in>set Ls. is_pos L
[PROOF STEP]
using Ls_p
[PROOF STATE]
proof (prove)
using this:
\<sigma> = the (mgu {insert A (atms_of (mset Ls))})
resolvent D A CA Ls = E
subseq Ls CA \<and> resolvable A D CA Ls

goal (1 subgoal):
 1. (mgu {insert A (atms_of (mset Ls))} = Some \<sigma> &&& Ls \<noteq> []) &&& eligible S \<sigma> [A] (add_mset (Neg A) (mset D)) &&& strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>) &&& \<forall>L\<in>set Ls. is_pos L
[PROOF STEP]
unfolding resolvable_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> = the (mgu {insert A (atms_of (mset Ls))})
resolvent D A CA Ls = E
subseq Ls CA \<and> (let \<sigma> = mgu {insert A (atms_of (mset Ls))} in \<sigma> \<noteq> None \<and> Ls \<noteq> [] \<and> maximal_wrt (A \<cdot>a the \<sigma>) (add_mset (Neg A) (mset D) \<cdot> the \<sigma>) \<and> strictly_maximal_wrt (A \<cdot>a the \<sigma>) ((mset CA - mset Ls) \<cdot> the \<sigma>) \<and> Ball (set Ls) is_pos)

goal (1 subgoal):
 1. (mgu {insert A (atms_of (mset Ls))} = Some \<sigma> &&& Ls \<noteq> []) &&& eligible S \<sigma> [A] (add_mset (Neg A) (mset D)) &&& strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>) &&& \<forall>L\<in>set Ls. is_pos L
[PROOF STEP]
unfolding Let_def eligible.simps
[PROOF STATE]
proof (prove)
using this:
\<sigma> = the (mgu {insert A (atms_of (mset Ls))})
resolvent D A CA Ls = E
subseq Ls CA \<and> mgu {insert A (atms_of (mset Ls))} \<noteq> None \<and> Ls \<noteq> [] \<and> maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) (add_mset (Neg A) (mset D) \<cdot> the (mgu {insert A (atms_of (mset Ls))})) \<and> strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))})) \<and> Ball (set Ls) is_pos

goal (1 subgoal):
 1. (mgu {insert A (atms_of (mset Ls))} = Some \<sigma> &&& Ls \<noteq> []) &&& \<exists>DA As \<sigma>'. \<sigma> = \<sigma>' \<and> [A] = As \<and> add_mset (Neg A) (mset D) = DA \<and> (S DA = negs (mset As) \<or> S DA = {#} \<and> length As = 1 \<and> maximal_wrt (As ! 0 \<cdot>a \<sigma>') (DA \<cdot> \<sigma>')) &&& strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>) &&& \<forall>L\<in>set Ls. is_pos L
[PROOF STEP]
using S_empty
[PROOF STATE]
proof (prove)
using this:
\<sigma> = the (mgu {insert A (atms_of (mset Ls))})
resolvent D A CA Ls = E
subseq Ls CA \<and> mgu {insert A (atms_of (mset Ls))} \<noteq> None \<and> Ls \<noteq> [] \<and> maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) (add_mset (Neg A) (mset D) \<cdot> the (mgu {insert A (atms_of (mset Ls))})) \<and> strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))})) \<and> Ball (set Ls) is_pos
S ?C = {#}

goal (1 subgoal):
 1. (mgu {insert A (atms_of (mset Ls))} = Some \<sigma> &&& Ls \<noteq> []) &&& \<exists>DA As \<sigma>'. \<sigma> = \<sigma>' \<and> [A] = As \<and> add_mset (Neg A) (mset D) = DA \<and> (S DA = negs (mset As) \<or> S DA = {#} \<and> length As = 1 \<and> maximal_wrt (As ! 0 \<cdot>a \<sigma>') (DA \<cdot> \<sigma>')) &&& strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>) &&& \<forall>L\<in>set Ls. is_pos L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mgu {insert A (atms_of (mset Ls))} = Some \<sigma>
Ls \<noteq> []
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>)
\<forall>L\<in>set Ls. is_pos L

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
from \<sigma>_p
[PROOF STATE]
proof (chain)
picking this:
mgu {insert A (atms_of (mset Ls))} = Some \<sigma>
Ls \<noteq> []
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>)
\<forall>L\<in>set Ls. is_pos L
[PROOF STEP]
have \<sigma>_p2: "the (mgu {insert A (atms_of (mset Ls))}) = \<sigma>"
[PROOF STATE]
proof (prove)
using this:
mgu {insert A (atms_of (mset Ls))} = Some \<sigma>
Ls \<noteq> []
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>)
\<forall>L\<in>set Ls. is_pos L

goal (1 subgoal):
 1. the (mgu {insert A (atms_of (mset Ls))}) = \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (mgu {insert A (atms_of (mset Ls))}) = \<sigma>

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have Ls_sub_CA: "mset Ls \<subseteq># mset CA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset Ls \<subseteq># mset CA
[PROOF STEP]
using subseq_mset_subseteq_mset Ls_p
[PROOF STATE]
proof (prove)
using this:
subseq ?xs ?ys \<Longrightarrow> mset ?xs \<subseteq># mset ?ys
resolvent D A CA Ls = E
subseq Ls CA \<and> resolvable A D CA Ls

goal (1 subgoal):
 1. mset Ls \<subseteq># mset CA
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset Ls \<subseteq># mset CA

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mset Ls \<subseteq># mset CA
[PROOF STEP]
have "mset (resolvent D A CA Ls) = sum_list [mset CA - mset Ls] \<cdot> \<sigma> + mset D \<cdot> \<sigma>"
[PROOF STATE]
proof (prove)
using this:
mset Ls \<subseteq># mset CA

goal (1 subgoal):
 1. mset (resolvent D A CA Ls) = sum_list [mset CA - mset Ls] \<cdot> \<sigma> + mset D \<cdot> \<sigma>
[PROOF STEP]
unfolding resolvent_def \<sigma>_p2 subst_cls_def
[PROOF STATE]
proof (prove)
using this:
mset Ls \<subseteq># mset CA

goal (1 subgoal):
 1. mset (map (\<lambda>M. M \<cdot>l \<sigma>) (remove_all CA Ls @ D)) = {#A \<cdot>l \<sigma>. A \<in># sum_list [mset CA - mset Ls]#} + {#A \<cdot>l \<sigma>. A \<in># mset D#}
[PROOF STEP]
using remove_all_mset_minus[of Ls CA]
[PROOF STATE]
proof (prove)
using this:
mset Ls \<subseteq># mset CA
mset Ls \<subseteq># mset CA \<Longrightarrow> mset (remove_all CA Ls) = mset CA - mset Ls

goal (1 subgoal):
 1. mset (map (\<lambda>M. M \<cdot>l \<sigma>) (remove_all CA Ls @ D)) = {#A \<cdot>l \<sigma>. A \<in># sum_list [mset CA - mset Ls]#} + {#A \<cdot>l \<sigma>. A \<in># mset D#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset (resolvent D A CA Ls) = sum_list [mset CA - mset Ls] \<cdot> \<sigma> + mset D \<cdot> \<sigma>

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mset (resolvent D A CA Ls) = sum_list [mset CA - mset Ls] \<cdot> \<sigma> + mset D \<cdot> \<sigma>

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "length [mset CA - mset Ls] = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [mset CA - mset Ls] = Suc 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length [mset CA - mset Ls] = Suc 0

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length [mset CA - mset Ls] = Suc 0

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "\<forall>L \<in> set Ls. is_pos L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>L\<in>set Ls. is_pos L
[PROOF STEP]
using \<sigma>_p(5) list_all_iff[of is_pos]
[PROOF STATE]
proof (prove)
using this:
\<forall>L\<in>set Ls. is_pos L
list_all is_pos ?x = Ball (set ?x) is_pos

goal (1 subgoal):
 1. \<forall>L\<in>set Ls. is_pos L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>L\<in>set Ls. is_pos L

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>L\<in>set Ls. is_pos L
[PROOF STEP]
have "{#Pos (atm_of x). x \<in># mset Ls#} = mset Ls"
[PROOF STATE]
proof (prove)
using this:
\<forall>L\<in>set Ls. is_pos L

goal (1 subgoal):
 1. {#Pos (atm_of x). x \<in># mset Ls#} = mset Ls
[PROOF STEP]
by (induction Ls) auto
[PROOF STATE]
proof (state)
this:
{#Pos (atm_of x). x \<in># mset Ls#} = mset Ls

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{#Pos (atm_of x). x \<in># mset Ls#} = mset Ls
[PROOF STEP]
have "mset CA = [mset CA - mset Ls] ! 0 + {#Pos (atm_of x). x \<in># mset Ls#}"
[PROOF STATE]
proof (prove)
using this:
{#Pos (atm_of x). x \<in># mset Ls#} = mset Ls

goal (1 subgoal):
 1. mset CA = [mset CA - mset Ls] ! 0 + {#Pos (atm_of x). x \<in># mset Ls#}
[PROOF STEP]
using Ls_sub_CA
[PROOF STATE]
proof (prove)
using this:
{#Pos (atm_of x). x \<in># mset Ls#} = mset Ls
mset Ls \<subseteq># mset CA

goal (1 subgoal):
 1. mset CA = [mset CA - mset Ls] ! 0 + {#Pos (atm_of x). x \<in># mset Ls#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset CA = [mset CA - mset Ls] ! 0 + {#Pos (atm_of x). x \<in># mset Ls#}

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mset CA = [mset CA - mset Ls] ! 0 + {#Pos (atm_of x). x \<in># mset Ls#}

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "Ls \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ls \<noteq> []
[PROOF STEP]
using \<sigma>_p
[PROOF STATE]
proof (prove)
using this:
mgu {insert A (atms_of (mset Ls))} = Some \<sigma>
Ls \<noteq> []
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>)
\<forall>L\<in>set Ls. is_pos L

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

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Ls \<noteq> []

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "Some \<sigma> = mgu {insert A (atm_of ` set Ls)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some \<sigma> = mgu {insert A (atm_of ` set Ls)}
[PROOF STEP]
using \<sigma>_p
[PROOF STATE]
proof (prove)
using this:
mgu {insert A (atms_of (mset Ls))} = Some \<sigma>
Ls \<noteq> []
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>)
\<forall>L\<in>set Ls. is_pos L

goal (1 subgoal):
 1. Some \<sigma> = mgu {insert A (atm_of ` set Ls)}
[PROOF STEP]
unfolding atms_of_def
[PROOF STATE]
proof (prove)
using this:
mgu {insert A (atm_of ` set_mset (mset Ls))} = Some \<sigma>
Ls \<noteq> []
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>)
\<forall>L\<in>set Ls. is_pos L

goal (1 subgoal):
 1. Some \<sigma> = mgu {insert A (atm_of ` set Ls)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some \<sigma> = mgu {insert A (atm_of ` set Ls)}

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Some \<sigma> = mgu {insert A (atm_of ` set Ls)}

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "eligible S \<sigma> [A] (add_mset (Neg A) (mset D))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
[PROOF STEP]
using \<sigma>_p
[PROOF STATE]
proof (prove)
using this:
mgu {insert A (atms_of (mset Ls))} = Some \<sigma>
Ls \<noteq> []
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>)
\<forall>L\<in>set Ls. is_pos L

goal (1 subgoal):
 1. eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "strictly_maximal_wrt (A \<cdot>a \<sigma>) ([mset CA - mset Ls] ! 0 \<cdot> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_maximal_wrt (A \<cdot>a \<sigma>) ([mset CA - mset Ls] ! 0 \<cdot> \<sigma>)
[PROOF STEP]
using \<sigma>_p(4)
[PROOF STATE]
proof (prove)
using this:
strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>)

goal (1 subgoal):
 1. strictly_maximal_wrt (A \<cdot>a \<sigma>) ([mset CA - mset Ls] ! 0 \<cdot> \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_maximal_wrt (A \<cdot>a \<sigma>) ([mset CA - mset Ls] ! 0 \<cdot> \<sigma>)

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
strictly_maximal_wrt (A \<cdot>a \<sigma>) ([mset CA - mset Ls] ! 0 \<cdot> \<sigma>)

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "S (mset CA) = {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S (mset CA) = {#}
[PROOF STEP]
by (simp add: S_empty)
[PROOF STATE]
proof (state)
this:
S (mset CA) = {#}

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mset (resolvent D A CA Ls) = sum_list [mset CA - mset Ls] \<cdot> \<sigma> + mset D \<cdot> \<sigma>
length [mset CA - mset Ls] = Suc 0
mset CA = [mset CA - mset Ls] ! 0 + {#Pos (atm_of x). x \<in># mset Ls#}
Ls \<noteq> []
Some \<sigma> = mgu {insert A (atm_of ` set Ls)}
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) ([mset CA - mset Ls] ! 0 \<cdot> \<sigma>)
S (mset CA) = {#}
[PROOF STEP]
have "\<exists>Cs. mset (resolvent D A CA Ls) = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
        \<and> length Cs = Suc 0 \<and> mset CA = Cs ! 0 + {#Pos (atm_of x). x \<in># mset Ls#}
        \<and> Ls \<noteq> [] \<and> Some \<sigma> = mgu {insert A (atm_of ` set Ls)}
        \<and> eligible S \<sigma> [A] (add_mset (Neg A) (mset D)) \<and> strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>)
        \<and> S (mset CA) = {#}"
[PROOF STATE]
proof (prove)
using this:
mset (resolvent D A CA Ls) = sum_list [mset CA - mset Ls] \<cdot> \<sigma> + mset D \<cdot> \<sigma>
length [mset CA - mset Ls] = Suc 0
mset CA = [mset CA - mset Ls] ! 0 + {#Pos (atm_of x). x \<in># mset Ls#}
Ls \<noteq> []
Some \<sigma> = mgu {insert A (atm_of ` set Ls)}
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) ([mset CA - mset Ls] ! 0 \<cdot> \<sigma>)
S (mset CA) = {#}

goal (1 subgoal):
 1. \<exists>Cs. mset (resolvent D A CA Ls) = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma> \<and> length Cs = Suc 0 \<and> mset CA = Cs ! 0 + {#Pos (atm_of x). x \<in># mset Ls#} \<and> Ls \<noteq> [] \<and> Some \<sigma> = mgu {insert A (atm_of ` set Ls)} \<and> eligible S \<sigma> [A] (add_mset (Neg A) (mset D)) \<and> strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>) \<and> S (mset CA) = {#}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Cs. mset (resolvent D A CA Ls) = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma> \<and> length Cs = Suc 0 \<and> mset CA = Cs ! 0 + {#Pos (atm_of x). x \<in># mset Ls#} \<and> Ls \<noteq> [] \<and> Some \<sigma> = mgu {insert A (atm_of ` set Ls)} \<and> eligible S \<sigma> [A] (add_mset (Neg A) (mset D)) \<and> strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>) \<and> S (mset CA) = {#}

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Cs. mset (resolvent D A CA Ls) = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma> \<and> length Cs = Suc 0 \<and> mset CA = Cs ! 0 + {#Pos (atm_of x). x \<in># mset Ls#} \<and> Ls \<noteq> [] \<and> Some \<sigma> = mgu {insert A (atm_of ` set Ls)} \<and> eligible S \<sigma> [A] (add_mset (Neg A) (mset D)) \<and> strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>) \<and> S (mset CA) = {#}
[PROOF STEP]
have "ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [image_mset atm_of (mset Ls)] [A]
      \<sigma> (mset (resolvent D A CA Ls))"
[PROOF STATE]
proof (prove)
using this:
\<exists>Cs. mset (resolvent D A CA Ls) = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma> \<and> length Cs = Suc 0 \<and> mset CA = Cs ! 0 + {#Pos (atm_of x). x \<in># mset Ls#} \<and> Ls \<noteq> [] \<and> Some \<sigma> = mgu {insert A (atm_of ` set Ls)} \<and> eligible S \<sigma> [A] (add_mset (Neg A) (mset D)) \<and> strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>) \<and> S (mset CA) = {#}

goal (1 subgoal):
 1. ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [image_mset atm_of (mset Ls)] [A] \<sigma> (mset (resolvent D A CA Ls))
[PROOF STEP]
unfolding ord_resolve.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>Cs. mset (resolvent D A CA Ls) = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma> \<and> length Cs = Suc 0 \<and> mset CA = Cs ! 0 + {#Pos (atm_of x). x \<in># mset Ls#} \<and> Ls \<noteq> [] \<and> Some \<sigma> = mgu {insert A (atm_of ` set Ls)} \<and> eligible S \<sigma> [A] (add_mset (Neg A) (mset D)) \<and> strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>) \<and> S (mset CA) = {#}

goal (1 subgoal):
 1. \<exists>CAs n Cs AAs As \<sigma>' Da. [mset CA] = CAs \<and> add_mset (Neg A) (mset D) = Da + negs (mset As) \<and> [image_mset atm_of (mset Ls)] = AAs \<and> [A] = As \<and> \<sigma> = \<sigma>' \<and> mset (resolvent D A CA Ls) = (\<Sum>\<^sub># (mset Cs) + Da) \<cdot> \<sigma>' \<and> length CAs = n \<and> length Cs = n \<and> length AAs = n \<and> length As = n \<and> n \<noteq> 0 \<and> (\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)) \<and> (\<forall>i<n. AAs ! i \<noteq> {#}) \<and> Some \<sigma>' = mgu (set_mset ` set (Map2.map2 add_mset As AAs)) \<and> eligible S \<sigma>' As (Da + negs (mset As)) \<and> (\<forall>i<n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>') (Cs ! i \<cdot> \<sigma>')) \<and> (\<forall>i<n. S (CAs ! i) = {#})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [image_mset atm_of (mset Ls)] [A] \<sigma> (mset (resolvent D A CA Ls))

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [image_mset atm_of (mset Ls)] [A] \<sigma> (mset (resolvent D A CA Ls))
[PROOF STEP]
have "\<exists>AA \<sigma>. ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> (mset E)"
[PROOF STATE]
proof (prove)
using this:
ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [image_mset atm_of (mset Ls)] [A] \<sigma> (mset (resolvent D A CA Ls))

goal (1 subgoal):
 1. \<exists>AA \<sigma>. ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> (mset E)
[PROOF STEP]
using Ls_p
[PROOF STATE]
proof (prove)
using this:
ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [image_mset atm_of (mset Ls)] [A] \<sigma> (mset (resolvent D A CA Ls))
resolvent D A CA Ls = E
subseq Ls CA \<and> resolvable A D CA Ls

goal (1 subgoal):
 1. \<exists>AA \<sigma>. ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> (mset E)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>AA \<sigma>. ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> (mset E)

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?E2 \<in> set (resolve_on A D CA) \<Longrightarrow> \<exists>AA \<sigma>. ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> (mset ?E2)

goal (2 subgoals):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
 2. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?E2 \<in> set (resolve_on A D CA) \<Longrightarrow> \<exists>AA \<sigma>. ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> (mset ?E2)
[PROOF STEP]
show "mset ` set (resolve_on A D CA)
    \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}"
[PROOF STATE]
proof (prove)
using this:
?E2 \<in> set (resolve_on A D CA) \<Longrightarrow> \<exists>AA \<sigma>. ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> (mset ?E2)

goal (1 subgoal):
 1. mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset ` set (resolve_on A D CA) \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
fix E AA \<sigma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
assume "ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> E"
[PROOF STATE]
proof (state)
this:
ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> E

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> E
[PROOF STEP]
obtain Cs where res': "E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>"
      "length Cs = Suc 0"
      "mset CA = Cs ! 0 + poss AA"
      "AA \<noteq> {#}"
      "Some \<sigma> = mgu {insert A (set_mset AA)}"
      "eligible S \<sigma> [A] (add_mset (Neg A) (mset D))"
      "strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>)"
      "S (Cs ! 0 + poss AA) = {#}"
[PROOF STATE]
proof (prove)
using this:
ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> E

goal (1 subgoal):
 1. (\<And>Cs. \<lbrakk>E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>; length Cs = Suc 0; mset CA = Cs ! 0 + poss AA; AA \<noteq> {#}; Some \<sigma> = mgu {insert A (set_mset AA)}; eligible S \<sigma> [A] (add_mset (Neg A) (mset D)); strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>); S (Cs ! 0 + poss AA) = {#}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ord_resolve.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>CAs n Cs AAs As \<sigma>' Da. [mset CA] = CAs \<and> add_mset (Neg A) (mset D) = Da + negs (mset As) \<and> [AA] = AAs \<and> [A] = As \<and> \<sigma> = \<sigma>' \<and> E = (\<Sum>\<^sub># (mset Cs) + Da) \<cdot> \<sigma>' \<and> length CAs = n \<and> length Cs = n \<and> length AAs = n \<and> length As = n \<and> n \<noteq> 0 \<and> (\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)) \<and> (\<forall>i<n. AAs ! i \<noteq> {#}) \<and> Some \<sigma>' = mgu (set_mset ` set (Map2.map2 add_mset As AAs)) \<and> eligible S \<sigma>' As (Da + negs (mset As)) \<and> (\<forall>i<n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>') (Cs ! i \<cdot> \<sigma>')) \<and> (\<forall>i<n. S (CAs ! i) = {#})

goal (1 subgoal):
 1. (\<And>Cs. \<lbrakk>E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>; length Cs = Suc 0; mset CA = Cs ! 0 + poss AA; AA \<noteq> {#}; Some \<sigma> = mgu {insert A (set_mset AA)}; eligible S \<sigma> [A] (add_mset (Neg A) (mset D)); strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>); S (Cs ! 0 + poss AA) = {#}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
length Cs = Suc 0
mset CA = Cs ! 0 + poss AA
AA \<noteq> {#}
Some \<sigma> = mgu {insert A (set_mset AA)}
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>)
S (Cs ! 0 + poss AA) = {#}

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
length Cs = Suc 0
mset CA = Cs ! 0 + poss AA
AA \<noteq> {#}
Some \<sigma> = mgu {insert A (set_mset AA)}
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>)
S (Cs ! 0 + poss AA) = {#}

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
define C where "C = Cs ! 0"
[PROOF STATE]
proof (state)
this:
C = Cs ! 0

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
length Cs = Suc 0
mset CA = Cs ! 0 + poss AA
AA \<noteq> {#}
Some \<sigma> = mgu {insert A (set_mset AA)}
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>)
S (Cs ! 0 + poss AA) = {#}
C = Cs ! 0
[PROOF STEP]
have res:
      "E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>"
      "mset CA = C + poss AA"
      "AA \<noteq> {#}"
      "Some \<sigma> = mgu {insert A (set_mset AA)}"
      "eligible S \<sigma> [A] (add_mset (Neg A) (mset D))"
      "strictly_maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>)"
      "S (C + poss AA) = {#}"
[PROOF STATE]
proof (prove)
using this:
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
length Cs = Suc 0
mset CA = Cs ! 0 + poss AA
AA \<noteq> {#}
Some \<sigma> = mgu {insert A (set_mset AA)}
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>)
S (Cs ! 0 + poss AA) = {#}
C = Cs ! 0

goal (1 subgoal):
 1. (E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma> &&& mset CA = C + poss AA &&& AA \<noteq> {#}) &&& (Some \<sigma> = mgu {insert A (set_mset AA)} &&& eligible S \<sigma> [A] (add_mset (Neg A) (mset D))) &&& strictly_maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>) &&& S (C + poss AA) = {#}
[PROOF STEP]
unfolding ord_resolve.simps
[PROOF STATE]
proof (prove)
using this:
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
length Cs = Suc 0
mset CA = Cs ! 0 + poss AA
AA \<noteq> {#}
Some \<sigma> = mgu {insert A (set_mset AA)}
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>)
S (Cs ! 0 + poss AA) = {#}
C = Cs ! 0

goal (1 subgoal):
 1. (E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma> &&& mset CA = C + poss AA &&& AA \<noteq> {#}) &&& (Some \<sigma> = mgu {insert A (set_mset AA)} &&& eligible S \<sigma> [A] (add_mset (Neg A) (mset D))) &&& strictly_maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>) &&& S (C + poss AA) = {#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
mset CA = C + poss AA
AA \<noteq> {#}
Some \<sigma> = mgu {insert A (set_mset AA)}
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>)
S (C + poss AA) = {#}

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
[PROOF STEP]
have
      "E = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>"
[PROOF STATE]
proof (prove)
using this:
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>

goal (1 subgoal):
 1. E = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
using this:
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>

goal (1 subgoal):
 1. E = Cs ! 0 \<cdot> \<sigma> + mset D \<cdot> \<sigma>
[PROOF STEP]
using res'(2)
[PROOF STATE]
proof (prove)
using this:
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
length Cs = Suc 0

goal (1 subgoal):
 1. E = Cs ! 0 \<cdot> \<sigma> + mset D \<cdot> \<sigma>
[PROOF STEP]
by (cases Cs) auto
[PROOF STATE]
proof (state)
this:
E = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
note res' = this res(2-7)
[PROOF STATE]
proof (state)
this:
E = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>
mset CA = C + poss AA
AA \<noteq> {#}
Some \<sigma> = mgu {insert A (set_mset AA)}
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>)
S (C + poss AA) = {#}

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA
[PROOF STEP]
using res(2)
[PROOF STATE]
proof (prove)
using this:
mset CA = C + poss AA

goal (1 subgoal):
 1. \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA
[PROOF STEP]
proof (induction CA arbitrary: AA C)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>AA C. mset [] = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) []
 2. \<And>a CA AA C. \<lbrakk>\<And>AA C. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (a # CA) = C + poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (a # CA)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
mset [] = C + poss AA

goal (2 subgoals):
 1. \<And>AA C. mset [] = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) []
 2. \<And>a CA AA C. \<lbrakk>\<And>AA C. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (a # CA) = C + poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (a # CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mset [] = C + poss AA
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mset [] = C + poss AA

goal (1 subgoal):
 1. \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) []

goal (1 subgoal):
 1. \<And>a CA AA C. \<lbrakk>\<And>AA C. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (a # CA) = C + poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (a # CA)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a CA AA C. \<lbrakk>\<And>AA C. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (a # CA) = C + poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (a # CA)
[PROOF STEP]
case (Cons L CA)
[PROOF STATE]
proof (state)
this:
mset CA = ?C + poss ?AA \<Longrightarrow> \<exists>Al. mset Al = ?AA \<and> subseq (map Pos Al) CA
mset (L # CA) = C + poss AA

goal (1 subgoal):
 1. \<And>a CA AA C. \<lbrakk>\<And>AA C. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (a # CA) = C + poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (a # CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mset CA = ?C + poss ?AA \<Longrightarrow> \<exists>Al. mset Al = ?AA \<and> subseq (map Pos Al) CA
mset (L # CA) = C + poss AA
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mset CA = ?C + poss ?AA \<Longrightarrow> \<exists>Al. mset Al = ?AA \<and> subseq (map Pos Al) CA
mset (L # CA) = C + poss AA

goal (1 subgoal):
 1. \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
proof (cases "L \<in># poss AA ")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<in># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
 2. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
L \<in># poss AA

goal (2 subgoals):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<in># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
 2. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L \<in># poss AA
[PROOF STEP]
have pos_L: "is_pos L"
[PROOF STATE]
proof (prove)
using this:
L \<in># poss AA

goal (1 subgoal):
 1. is_pos L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_pos L

goal (2 subgoals):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<in># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
 2. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
have rem: "\<And>A'. Pos A' \<in># poss AA \<Longrightarrow>
          remove1_mset (Pos A') (C + poss AA) = C + poss (remove1_mset A' AA)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A'. Pos A' \<in># poss AA \<Longrightarrow> remove1_mset (Pos A') (C + poss AA) = C + poss (remove1_mset A' AA)
[PROOF STEP]
by (induct AA) auto
[PROOF STATE]
proof (state)
this:
Pos ?A' \<in># poss AA \<Longrightarrow> remove1_mset (Pos ?A') (C + poss AA) = C + poss (remove1_mset ?A' AA)

goal (2 subgoals):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<in># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
 2. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
have "mset CA = C + (poss (AA - {#atm_of L#}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset CA = C + poss (remove1_mset (atm_of L) AA)
[PROOF STEP]
using True Cons(2)
[PROOF STATE]
proof (prove)
using this:
L \<in># poss AA
mset (L # CA) = C + poss AA

goal (1 subgoal):
 1. mset CA = C + poss (remove1_mset (atm_of L) AA)
[PROOF STEP]
by (metis add_mset_remove_trivial rem literal.collapse(1) mset.simps(2) pos_L)
[PROOF STATE]
proof (state)
this:
mset CA = C + poss (remove1_mset (atm_of L) AA)

goal (2 subgoals):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<in># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
 2. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mset CA = C + poss (remove1_mset (atm_of L) AA)
[PROOF STEP]
have "\<exists>Al. mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA"
[PROOF STATE]
proof (prove)
using this:
mset CA = C + poss (remove1_mset (atm_of L) AA)

goal (1 subgoal):
 1. \<exists>Al. mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA
[PROOF STEP]
using Cons(1)[of _ "((AA - {#atm_of L#}))"]
[PROOF STATE]
proof (prove)
using this:
mset CA = C + poss (remove1_mset (atm_of L) AA)
mset CA = ?C + poss (remove1_mset (atm_of L) AA) \<Longrightarrow> \<exists>Al. mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA

goal (1 subgoal):
 1. \<exists>Al. mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>Al. mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA

goal (2 subgoals):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<in># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
 2. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Al. mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA
[PROOF STEP]
obtain Al where
          "mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA"
[PROOF STATE]
proof (prove)
using this:
\<exists>Al. mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA

goal (1 subgoal):
 1. (\<And>Al. mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA

goal (2 subgoals):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<in># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
 2. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA
[PROOF STEP]
have
          "mset (atm_of L # Al) = AA" and
          "subseq (map Pos (atm_of L # Al)) (L # CA)"
[PROOF STATE]
proof (prove)
using this:
mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA

goal (1 subgoal):
 1. mset (atm_of L # Al) = AA &&& subseq (map Pos (atm_of L # Al)) (L # CA)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA
L \<in># poss AA

goal (1 subgoal):
 1. mset (atm_of L # Al) = AA &&& subseq (map Pos (atm_of L # Al)) (L # CA)
[PROOF STEP]
by (auto simp add: pos_L)
[PROOF STATE]
proof (state)
this:
mset (atm_of L # Al) = AA
subseq (map Pos (atm_of L # Al)) (L # CA)

goal (2 subgoals):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<in># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
 2. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mset (atm_of L # Al) = AA
subseq (map Pos (atm_of L # Al)) (L # CA)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mset (atm_of L # Al) = AA
subseq (map Pos (atm_of L # Al)) (L # CA)

goal (1 subgoal):
 1. \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)

goal (1 subgoal):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
L \<notin># poss AA

goal (1 subgoal):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L \<notin># poss AA
[PROOF STEP]
have "mset CA = remove1_mset L C + poss AA"
[PROOF STATE]
proof (prove)
using this:
L \<notin># poss AA

goal (1 subgoal):
 1. mset CA = remove1_mset L C + poss AA
[PROOF STEP]
using Cons(2)
[PROOF STATE]
proof (prove)
using this:
L \<notin># poss AA
mset (L # CA) = C + poss AA

goal (1 subgoal):
 1. mset CA = remove1_mset L C + poss AA
[PROOF STEP]
by (metis Un_iff add_mset_remove_trivial mset.simps(2) set_mset_union single_subset_iff
              subset_mset.add_diff_assoc2 union_single_eq_member)
[PROOF STATE]
proof (state)
this:
mset CA = remove1_mset L C + poss AA

goal (1 subgoal):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mset CA = remove1_mset L C + poss AA
[PROOF STEP]
have "\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA"
[PROOF STATE]
proof (prove)
using this:
mset CA = remove1_mset L C + poss AA

goal (1 subgoal):
 1. \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA
[PROOF STEP]
using Cons(1)[of "C - {#L#}" AA] Cons(2)
[PROOF STATE]
proof (prove)
using this:
mset CA = remove1_mset L C + poss AA
mset CA = remove1_mset L C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA
mset (L # CA) = C + poss AA

goal (1 subgoal):
 1. \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA

goal (1 subgoal):
 1. \<lbrakk>\<And>C AA. mset CA = C + poss AA \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA; mset (L # CA) = C + poss AA; L \<notin># poss AA\<rbrakk> \<Longrightarrow> \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA

goal (1 subgoal):
 1. \<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) (L # CA)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA
[PROOF STEP]
obtain Al where Al_p: "mset Al = AA" "subseq (map Pos Al) CA"
[PROOF STATE]
proof (prove)
using this:
\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA

goal (1 subgoal):
 1. (\<And>Al. \<lbrakk>mset Al = AA; subseq (map Pos Al) CA\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset Al = AA
subseq (map Pos Al) CA

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
define Ls :: "'a lclause" where "Ls = map Pos Al"
[PROOF STATE]
proof (state)
this:
Ls = map Pos Al

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have diff: "mset CA - mset Ls = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset CA - mset Ls = C
[PROOF STEP]
unfolding Ls_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset CA - mset (map Pos Al) = C
[PROOF STEP]
using res(2) Al_p(1)
[PROOF STATE]
proof (prove)
using this:
mset CA = C + poss AA
mset Al = AA

goal (1 subgoal):
 1. mset CA - mset (map Pos Al) = C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset CA - mset Ls = C

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have ls_subq_ca: "subseq Ls CA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseq Ls CA
[PROOF STEP]
unfolding Ls_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseq (map Pos Al) CA
[PROOF STEP]
using Al_p
[PROOF STATE]
proof (prove)
using this:
mset Al = AA
subseq (map Pos Al) CA

goal (1 subgoal):
 1. subseq (map Pos Al) CA
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
subseq Ls CA

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
subseq Ls CA

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
subseq Ls CA

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "\<exists>y. mgu {insert A (atms_of (mset Ls))} = Some y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. mgu {insert A (atms_of (mset Ls))} = Some y
[PROOF STEP]
unfolding Ls_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. mgu {insert A (atms_of (mset (map Pos Al)))} = Some y
[PROOF STEP]
using res(4) Al_p
[PROOF STATE]
proof (prove)
using this:
Some \<sigma> = mgu {insert A (set_mset AA)}
mset Al = AA
subseq (map Pos Al) CA

goal (1 subgoal):
 1. \<exists>y. mgu {insert A (atms_of (mset (map Pos Al)))} = Some y
[PROOF STEP]
by (metis atms_of_poss mset_map)
[PROOF STATE]
proof (state)
this:
\<exists>y. mgu {insert A (atms_of (mset Ls))} = Some y

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>y. mgu {insert A (atms_of (mset Ls))} = Some y

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "Ls \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ls \<noteq> []
[PROOF STEP]
using Al_p(1) Ls_def res'(3)
[PROOF STATE]
proof (prove)
using this:
mset Al = AA
Ls = map Pos Al
AA \<noteq> {#}

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

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Ls \<noteq> []

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have \<sigma>_p: "the (mgu {insert A (set Al)}) = \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (mgu {insert A (set Al)}) = \<sigma>
[PROOF STEP]
using res'(4) Al_p(1)
[PROOF STATE]
proof (prove)
using this:
Some \<sigma> = mgu {insert A (set_mset AA)}
mset Al = AA

goal (1 subgoal):
 1. the (mgu {insert A (set Al)}) = \<sigma>
[PROOF STEP]
by (metis option.sel  set_mset_mset)
[PROOF STATE]
proof (state)
this:
the (mgu {insert A (set Al)}) = \<sigma>

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
the (mgu {insert A (set Al)}) = \<sigma>
[PROOF STEP]
have "eligible S (the (mgu {insert A (atms_of (mset Ls))})) [A]
        (add_mset (Neg A) (mset D))"
[PROOF STATE]
proof (prove)
using this:
the (mgu {insert A (set Al)}) = \<sigma>

goal (1 subgoal):
 1. eligible S (the (mgu {insert A (atms_of (mset Ls))})) [A] (add_mset (Neg A) (mset D))
[PROOF STEP]
unfolding Ls_def
[PROOF STATE]
proof (prove)
using this:
the (mgu {insert A (set Al)}) = \<sigma>

goal (1 subgoal):
 1. eligible S (the (mgu {insert A (atms_of (mset (map Pos Al)))})) [A] (add_mset (Neg A) (mset D))
[PROOF STEP]
using res
[PROOF STATE]
proof (prove)
using this:
the (mgu {insert A (set Al)}) = \<sigma>
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
mset CA = C + poss AA
AA \<noteq> {#}
Some \<sigma> = mgu {insert A (set_mset AA)}
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>)
S (C + poss AA) = {#}

goal (1 subgoal):
 1. eligible S (the (mgu {insert A (atms_of (mset (map Pos Al)))})) [A] (add_mset (Neg A) (mset D))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eligible S (the (mgu {insert A (atms_of (mset Ls))})) [A] (add_mset (Neg A) (mset D))

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eligible S (the (mgu {insert A (atms_of (mset Ls))})) [A] (add_mset (Neg A) (mset D))

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))}))
        ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))}))
[PROOF STEP]
unfolding Ls_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset (map Pos Al)))})) ((mset CA - mset (map Pos Al)) \<cdot> the (mgu {insert A (atms_of (mset (map Pos Al)))}))
[PROOF STEP]
using res \<sigma>_p Al_p
[PROOF STATE]
proof (prove)
using this:
E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
mset CA = C + poss AA
AA \<noteq> {#}
Some \<sigma> = mgu {insert A (set_mset AA)}
eligible S \<sigma> [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>)
S (C + poss AA) = {#}
the (mgu {insert A (set Al)}) = \<sigma>
mset Al = AA
subseq (map Pos Al) CA

goal (1 subgoal):
 1. strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset (map Pos Al)))})) ((mset CA - mset (map Pos Al)) \<cdot> the (mgu {insert A (atms_of (mset (map Pos Al)))}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))}))

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))}))

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "\<forall>L \<in> set Ls. is_pos L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>L\<in>set Ls. is_pos L
[PROOF STEP]
by (simp add: Ls_def)
[PROOF STATE]
proof (state)
this:
\<forall>L\<in>set Ls. is_pos L

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. mgu {insert A (atms_of (mset Ls))} = Some y
Ls \<noteq> []
eligible S (the (mgu {insert A (atms_of (mset Ls))})) [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))}))
\<forall>L\<in>set Ls. is_pos L
[PROOF STEP]
have "resolvable A D CA Ls"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. mgu {insert A (atms_of (mset Ls))} = Some y
Ls \<noteq> []
eligible S (the (mgu {insert A (atms_of (mset Ls))})) [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))}))
\<forall>L\<in>set Ls. is_pos L

goal (1 subgoal):
 1. resolvable A D CA Ls
[PROOF STEP]
unfolding resolvable_def
[PROOF STATE]
proof (prove)
using this:
\<exists>y. mgu {insert A (atms_of (mset Ls))} = Some y
Ls \<noteq> []
eligible S (the (mgu {insert A (atms_of (mset Ls))})) [A] (add_mset (Neg A) (mset D))
strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))}))
\<forall>L\<in>set Ls. is_pos L

goal (1 subgoal):
 1. let \<sigma> = mgu {insert A (atms_of (mset Ls))} in \<sigma> \<noteq> None \<and> Ls \<noteq> [] \<and> maximal_wrt (A \<cdot>a the \<sigma>) (add_mset (Neg A) (mset D) \<cdot> the \<sigma>) \<and> strictly_maximal_wrt (A \<cdot>a the \<sigma>) ((mset CA - mset Ls) \<cdot> the \<sigma>) \<and> Ball (set Ls) is_pos
[PROOF STEP]
unfolding eligible.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>y. mgu {insert A (atms_of (mset Ls))} = Some y
Ls \<noteq> []
\<exists>DA As \<sigma>. the (mgu {insert A (atms_of (mset Ls))}) = \<sigma> \<and> [A] = As \<and> add_mset (Neg A) (mset D) = DA \<and> (S DA = negs (mset As) \<or> S DA = {#} \<and> length As = 1 \<and> maximal_wrt (As ! 0 \<cdot>a \<sigma>) (DA \<cdot> \<sigma>))
strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))}))
\<forall>L\<in>set Ls. is_pos L

goal (1 subgoal):
 1. let \<sigma> = mgu {insert A (atms_of (mset Ls))} in \<sigma> \<noteq> None \<and> Ls \<noteq> [] \<and> maximal_wrt (A \<cdot>a the \<sigma>) (add_mset (Neg A) (mset D) \<cdot> the \<sigma>) \<and> strictly_maximal_wrt (A \<cdot>a the \<sigma>) ((mset CA - mset Ls) \<cdot> the \<sigma>) \<and> Ball (set Ls) is_pos
[PROOF STEP]
using S_empty
[PROOF STATE]
proof (prove)
using this:
\<exists>y. mgu {insert A (atms_of (mset Ls))} = Some y
Ls \<noteq> []
\<exists>DA As \<sigma>. the (mgu {insert A (atms_of (mset Ls))}) = \<sigma> \<and> [A] = As \<and> add_mset (Neg A) (mset D) = DA \<and> (S DA = negs (mset As) \<or> S DA = {#} \<and> length As = 1 \<and> maximal_wrt (As ! 0 \<cdot>a \<sigma>) (DA \<cdot> \<sigma>))
strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))})) ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))}))
\<forall>L\<in>set Ls. is_pos L
S ?C = {#}

goal (1 subgoal):
 1. let \<sigma> = mgu {insert A (atms_of (mset Ls))} in \<sigma> \<noteq> None \<and> Ls \<noteq> [] \<and> maximal_wrt (A \<cdot>a the \<sigma>) (add_mset (Neg A) (mset D) \<cdot> the \<sigma>) \<and> strictly_maximal_wrt (A \<cdot>a the \<sigma>) ((mset CA - mset Ls) \<cdot> the \<sigma>) \<and> Ball (set Ls) is_pos
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
resolvable A D CA Ls

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
resolvable A D CA Ls

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
resolvable A D CA Ls

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have ls_sub_ca: "mset Ls \<subseteq># mset CA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset Ls \<subseteq># mset CA
[PROOF STEP]
using ls_subq_ca subseq_mset_subseteq_mset[of Ls CA]
[PROOF STATE]
proof (prove)
using this:
subseq Ls CA
subseq Ls CA \<Longrightarrow> mset Ls \<subseteq># mset CA

goal (1 subgoal):
 1. mset Ls \<subseteq># mset CA
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mset Ls \<subseteq># mset CA

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
have "{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>
[PROOF STEP]
using diff
[PROOF STATE]
proof (prove)
using this:
mset CA - mset Ls = C

goal (1 subgoal):
 1. {#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>
[PROOF STEP]
unfolding subst_cls_def
[PROOF STATE]
proof (prove)
using this:
mset CA - mset Ls = C

goal (1 subgoal):
 1. {#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = {#A \<cdot>l \<sigma>. A \<in># C#} + {#A \<cdot>l \<sigma>. A \<in># mset D#}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>
[PROOF STEP]
have "{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E"
[PROOF STATE]
proof (prove)
using this:
{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>

goal (1 subgoal):
 1. {#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E
[PROOF STEP]
using res'(1)
[PROOF STATE]
proof (prove)
using this:
{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>
E = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>

goal (1 subgoal):
 1. {#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E
[PROOF STEP]
have "{#M \<cdot>l \<sigma>. M \<in># mset (remove_all CA Ls)#} + {#M \<cdot>l \<sigma> . M \<in># mset D#} = E"
[PROOF STATE]
proof (prove)
using this:
{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E

goal (1 subgoal):
 1. {#M \<cdot>l \<sigma>. M \<in># mset (remove_all CA Ls)#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E
[PROOF STEP]
using remove_all_mset_minus[of Ls CA] ls_sub_ca
[PROOF STATE]
proof (prove)
using this:
{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E
mset Ls \<subseteq># mset CA \<Longrightarrow> mset (remove_all CA Ls) = mset CA - mset Ls
mset Ls \<subseteq># mset CA

goal (1 subgoal):
 1. {#M \<cdot>l \<sigma>. M \<in># mset (remove_all CA Ls)#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#M \<cdot>l \<sigma>. M \<in># mset (remove_all CA Ls)#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{#M \<cdot>l \<sigma>. M \<in># mset (remove_all CA Ls)#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E
[PROOF STEP]
have "mset (resolvent D A CA Ls) = E"
[PROOF STATE]
proof (prove)
using this:
{#M \<cdot>l \<sigma>. M \<in># mset (remove_all CA Ls)#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E

goal (1 subgoal):
 1. mset (resolvent D A CA Ls) = E
[PROOF STEP]
unfolding resolvable_def Let_def resolvent_def
[PROOF STATE]
proof (prove)
using this:
{#M \<cdot>l \<sigma>. M \<in># mset (remove_all CA Ls)#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E

goal (1 subgoal):
 1. mset (map (\<lambda>M. M \<cdot>l the (mgu {insert A (atms_of (mset Ls))})) (remove_all CA Ls @ D)) = E
[PROOF STEP]
using Al_p(1) Ls_def atms_of_poss res'(4)
[PROOF STATE]
proof (prove)
using this:
{#M \<cdot>l \<sigma>. M \<in># mset (remove_all CA Ls)#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E
mset Al = AA
Ls = map Pos Al
atms_of (poss ?AA) = set_mset ?AA
Some \<sigma> = mgu {insert A (set_mset AA)}

goal (1 subgoal):
 1. mset (map (\<lambda>M. M \<cdot>l the (mgu {insert A (atms_of (mset Ls))})) (remove_all CA Ls @ D)) = E
[PROOF STEP]
by (metis image_mset_union mset_append mset_map option.sel)
[PROOF STATE]
proof (state)
this:
mset (resolvent D A CA Ls) = E

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
subseq Ls CA
resolvable A D CA Ls
mset (resolvent D A CA Ls) = E
[PROOF STEP]
have "E \<in> mset ` set (resolve_on A D CA)"
[PROOF STATE]
proof (prove)
using this:
subseq Ls CA
resolvable A D CA Ls
mset (resolvent D A CA Ls) = E

goal (1 subgoal):
 1. E \<in> mset ` set (resolve_on A D CA)
[PROOF STEP]
unfolding resolve_on_def
[PROOF STATE]
proof (prove)
using this:
subseq Ls CA
resolvable A D CA Ls
mset (resolvent D A CA Ls) = E

goal (1 subgoal):
 1. E \<in> mset ` set (map (resolvent D A CA) (filter (resolvable A D CA) (subseqs CA)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E \<in> mset ` set (resolve_on A D CA)

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [?AA2] [A] ?\<sigma>2 ?E2 \<Longrightarrow> ?E2 \<in> mset ` set (resolve_on A D CA)

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [?AA2] [A] ?\<sigma>2 ?E2 \<Longrightarrow> ?E2 \<in> mset ` set (resolve_on A D CA)
[PROOF STEP]
show "{E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
    \<subseteq> mset ` set (resolve_on A D CA)"
[PROOF STATE]
proof (prove)
using this:
ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [?AA2] [A] ?\<sigma>2 ?E2 \<Longrightarrow> ?E2 \<in> mset ` set (resolve_on A D CA)

goal (1 subgoal):
 1. {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E} \<subseteq> mset ` set (resolve_on A D CA)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_lnull_sswSts: "\<not> lnull sswSts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> lnull sswSts
[PROOF STEP]
using deriv_sswSts_weighted_RP
[PROOF STATE]
proof (prove)
using this:
chain (\<leadsto>\<^sub>w) sswSts

goal (1 subgoal):
 1. \<not> lnull sswSts
[PROOF STEP]
by (cases rule: chain.cases) auto


[STATEMENT]
lemma of_complex_mult [simp]: "of_complex (x * y) = of_complex x * of_complex y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (x * y) = of_complex x * of_complex y
[PROOF STEP]
by (simp add: of_complex_def mult.commute)


[STATEMENT]
lemma nonzero_Complexs_inverse: "a \<in> \<complex> \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> inverse a \<in> \<complex>"
  for a :: "'a::complex_div_algebra"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> \<complex>; a \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> inverse a \<in> \<complex>
[PROOF STEP]
apply (auto simp add: Complexs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> 0; a = of_complex x\<rbrakk> \<Longrightarrow> inverse (of_complex x) \<in> range of_complex
[PROOF STEP]
by (metis of_complex_inverse range_eqI)


[STATEMENT]
lemma comp: "bounded_clinear f \<Longrightarrow> bounded_clinear g \<Longrightarrow> bounded_cbilinear (\<lambda>x y. f x ** g y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded_clinear f; bounded_clinear g\<rbrakk> \<Longrightarrow> bounded_cbilinear (\<lambda>x y. f x ** g y)
[PROOF STEP]
by (rule bounded_cbilinear.flip[OF bounded_cbilinear.comp1[OF bounded_cbilinear.flip[OF comp1]]])


[STATEMENT]
lemma comp_injective_below_complement:
  "injective y \<Longrightarrow> -x * y \<le> -(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective y \<Longrightarrow> - x * y \<le> - (x * y)
[PROOF STEP]
by (metis p_antitone_iff comp_associative comp_right_isotone comp_right_one schroeder_4_p)