[STATEMENT]
lemma replacement_monotonic :
  shows "\<And> t  s. ((subst v \<sigma>), (subst u \<sigma>)) \<in> trm_ord
          \<Longrightarrow> subterm t p u \<Longrightarrow> replace_subterm t p v s
          \<Longrightarrow> ((subst s \<sigma>), (subst t \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t p u; replace_subterm t p v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
proof (induction p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t [] u; replace_subterm t [] v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
 2. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t p u; replace_subterm t p v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord; (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t (a # p) u; replace_subterm t (a # p) v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
subterm t [] u
replace_subterm t [] v s

goal (2 subgoals):
 1. \<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t [] u; replace_subterm t [] v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
 2. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t p u; replace_subterm t p v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord; (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t (a # p) u; replace_subterm t (a # p) v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from \<open>subterm t Nil u\<close>
[PROOF STATE]
proof (chain)
picking this:
subterm t [] u
[PROOF STEP]
have "t = u"
[PROOF STATE]
proof (prove)
using this:
subterm t [] u

goal (1 subgoal):
 1. t = u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = u

goal (2 subgoals):
 1. \<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t [] u; replace_subterm t [] v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
 2. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t p u; replace_subterm t p v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord; (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t (a # p) u; replace_subterm t (a # p) v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from \<open>replace_subterm t Nil v s\<close>
[PROOF STATE]
proof (chain)
picking this:
replace_subterm t [] v s
[PROOF STEP]
have "s = v"
[PROOF STATE]
proof (prove)
using this:
replace_subterm t [] v s

goal (1 subgoal):
 1. s = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = v

goal (2 subgoals):
 1. \<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t [] u; replace_subterm t [] v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
 2. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t p u; replace_subterm t p v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord; (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t (a # p) u; replace_subterm t (a # p) v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from \<open>t = u\<close> and \<open>s = v\<close> and \<open>((subst v \<sigma>), (subst u \<sigma>)) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
t = u
s = v
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
t = u
s = v
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t p u; replace_subterm t p v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord; (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t (a # p) u; replace_subterm t (a # p) v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t p u; replace_subterm t p v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord; (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t (a # p) u; replace_subterm t (a # p) v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
case (Cons i q)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm ?t q u; replace_subterm ?t q v ?s\<rbrakk> \<Longrightarrow> (?s \<lhd> \<sigma>, ?t \<lhd> \<sigma>) \<in> trm_ord
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
subterm t (i # q) u
replace_subterm t (i # q) v s

goal (1 subgoal):
 1. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t p u; replace_subterm t p v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord; (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t (a # p) u; replace_subterm t (a # p) v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from \<open>subterm t (i # q) u\<close>
[PROOF STATE]
proof (chain)
picking this:
subterm t (i # q) u
[PROOF STEP]
obtain t1 t2 where
        "t = (Comb t1 t2)"
[PROOF STATE]
proof (prove)
using this:
subterm t (i # q) u

goal (1 subgoal):
 1. (\<And>t1 t2. t = t1 \<cdot> t2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subterm.elims(2)
[PROOF STATE]
proof (prove)
using this:
subterm t (i # q) u
\<lbrakk>subterm ?x ?xa ?xb; \<And>T S. \<lbrakk>?x = T; ?xa = []; ?xb = S; T = S\<rbrakk> \<Longrightarrow> ?P; \<And>x y next S. \<lbrakk>?x = x \<cdot> y; ?xa = indices.Left # next; ?xb = S; subterm x next S\<rbrakk> \<Longrightarrow> ?P; \<And>x y next S. \<lbrakk>?x = x \<cdot> y; ?xa = indices.Right # next; ?xb = S; subterm y next S\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>t1 t2. t = t1 \<cdot> t2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t = t1 \<cdot> t2

goal (1 subgoal):
 1. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t p u; replace_subterm t p v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord; (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t (a # p) u; replace_subterm t (a # p) v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
have "i = Left \<or> i = Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = indices.Left \<or> i = indices.Right
[PROOF STEP]
using indices.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = indices.Left \<Longrightarrow> ?P; ?y = indices.Right \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. i = indices.Left \<or> i = indices.Right
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i = indices.Left \<or> i = indices.Right

goal (1 subgoal):
 1. \<And>a p t s. \<lbrakk>\<And>t s. \<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t p u; replace_subterm t p v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord; (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm t (a # p) u; replace_subterm t (a # p) v s\<rbrakk> \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = indices.Left \<or> i = indices.Right
[PROOF STEP]
show "((subst s \<sigma>), (subst t \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
i = indices.Left \<or> i = indices.Right

goal (1 subgoal):
 1. (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
 2. i = indices.Right \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
assume "i = Left"
[PROOF STATE]
proof (state)
this:
i = indices.Left

goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
 2. i = indices.Right \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from this and \<open>t = Comb t1 t2\<close> and \<open>subterm t (i # q) u\<close>
[PROOF STATE]
proof (chain)
picking this:
i = indices.Left
t = t1 \<cdot> t2
subterm t (i # q) u
[PROOF STEP]
have "subterm t1 q u"
[PROOF STATE]
proof (prove)
using this:
i = indices.Left
t = t1 \<cdot> t2
subterm t (i # q) u

goal (1 subgoal):
 1. subterm t1 q u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterm t1 q u

goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
 2. i = indices.Right \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from \<open>i = Left\<close> and \<open>t = Comb t1 t2\<close> and \<open>replace_subterm t (i # q) v s\<close>
[PROOF STATE]
proof (chain)
picking this:
i = indices.Left
t = t1 \<cdot> t2
replace_subterm t (i # q) v s
[PROOF STEP]
obtain t1' where "replace_subterm t1 q v t1'" and "s = Comb t1' t2"
[PROOF STATE]
proof (prove)
using this:
i = indices.Left
t = t1 \<cdot> t2
replace_subterm t (i # q) v s

goal (1 subgoal):
 1. (\<And>t1'. \<lbrakk>replace_subterm t1 q v t1'; s = t1' \<cdot> t2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
replace_subterm t1 q v t1'
s = t1' \<cdot> t2

goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
 2. i = indices.Right \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from  \<open>((subst v \<sigma>), (subst u \<sigma>)) \<in> trm_ord\<close>
        and \<open>subterm t1 q u\<close> and \<open>replace_subterm t1 q v t1'\<close>
[PROOF STATE]
proof (chain)
picking this:
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
subterm t1 q u
replace_subterm t1 q v t1'
[PROOF STEP]
have
        "((subst t1' \<sigma>), (subst t1 \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
subterm t1 q u
replace_subterm t1 q v t1'

goal (1 subgoal):
 1. (t1' \<lhd> \<sigma>, t1 \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using Cons.IH Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
subterm t1 q u
replace_subterm t1 q v t1'
\<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm ?t q u; replace_subterm ?t q v ?s\<rbrakk> \<Longrightarrow> (?s \<lhd> \<sigma>, ?t \<lhd> \<sigma>) \<in> trm_ord
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (t1' \<lhd> \<sigma>, t1 \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(t1' \<lhd> \<sigma>, t1 \<lhd> \<sigma>) \<in> trm_ord

goal (2 subgoals):
 1. i = indices.Left \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
 2. i = indices.Right \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from this  and \<open>t = (Comb t1 t2)\<close> and \<open>s = (Comb t1' t2)\<close>
[PROOF STATE]
proof (chain)
picking this:
(t1' \<lhd> \<sigma>, t1 \<lhd> \<sigma>) \<in> trm_ord
t = t1 \<cdot> t2
s = t1' \<cdot> t2
[PROOF STEP]
show "((subst s \<sigma>), (subst t \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t1' \<lhd> \<sigma>, t1 \<lhd> \<sigma>) \<in> trm_ord
t = t1 \<cdot> t2
s = t1' \<cdot> t2

goal (1 subgoal):
 1. (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by (simp add: trm_ord_reduction_left)
[PROOF STATE]
proof (state)
this:
(s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
assume "i = Right"
[PROOF STATE]
proof (state)
this:
i = indices.Right

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from this and \<open>t = Comb t1 t2\<close> and \<open>subterm t (i # q) u\<close>
[PROOF STATE]
proof (chain)
picking this:
i = indices.Right
t = t1 \<cdot> t2
subterm t (i # q) u
[PROOF STEP]
have "subterm t2 q u"
[PROOF STATE]
proof (prove)
using this:
i = indices.Right
t = t1 \<cdot> t2
subterm t (i # q) u

goal (1 subgoal):
 1. subterm t2 q u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterm t2 q u

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from \<open>i = Right\<close> and \<open>t = Comb t1 t2\<close> and \<open>replace_subterm t (i # q) v s\<close>
[PROOF STATE]
proof (chain)
picking this:
i = indices.Right
t = t1 \<cdot> t2
replace_subterm t (i # q) v s
[PROOF STEP]
obtain t2' where "replace_subterm t2 q v t2'" and "s = Comb t1 t2'"
[PROOF STATE]
proof (prove)
using this:
i = indices.Right
t = t1 \<cdot> t2
replace_subterm t (i # q) v s

goal (1 subgoal):
 1. (\<And>t2'. \<lbrakk>replace_subterm t2 q v t2'; s = t1 \<cdot> t2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
replace_subterm t2 q v t2'
s = t1 \<cdot> t2'

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from  \<open>((subst v \<sigma>), (subst u \<sigma>)) \<in> trm_ord\<close>
        and \<open>subterm t2 q u\<close> and \<open>replace_subterm t2 q v t2'\<close>
[PROOF STATE]
proof (chain)
picking this:
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
subterm t2 q u
replace_subterm t2 q v t2'
[PROOF STEP]
have
        "((subst t2' \<sigma>), (subst t2 \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
subterm t2 q u
replace_subterm t2 q v t2'

goal (1 subgoal):
 1. (t2' \<lhd> \<sigma>, t2 \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using Cons.IH Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
subterm t2 q u
replace_subterm t2 q v t2'
\<lbrakk>(v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord; subterm ?t q u; replace_subterm ?t q v ?s\<rbrakk> \<Longrightarrow> (?s \<lhd> \<sigma>, ?t \<lhd> \<sigma>) \<in> trm_ord
subterm t (i # q) u

goal (1 subgoal):
 1. (t2' \<lhd> \<sigma>, t2 \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(t2' \<lhd> \<sigma>, t2 \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. i = indices.Right \<Longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
from this and \<open>t = (Comb t1 t2)\<close> and \<open>s = (Comb t1 t2')\<close>
[PROOF STATE]
proof (chain)
picking this:
(t2' \<lhd> \<sigma>, t2 \<lhd> \<sigma>) \<in> trm_ord
t = t1 \<cdot> t2
s = t1 \<cdot> t2'
[PROOF STEP]
show "((subst s \<sigma>), (subst t \<sigma>)) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t2' \<lhd> \<sigma>, t2 \<lhd> \<sigma>) \<in> trm_ord
t = t1 \<cdot> t2
s = t1 \<cdot> t2'

goal (1 subgoal):
 1. (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by (simp add: trm_ord_reduction_right)
[PROOF STATE]
proof (state)
this:
(s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_lit_subst:
  shows "(mset_lit (subst_lit L \<sigma>)) =
    {# (subst x \<sigma>). x \<in># (mset_lit L) #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
have "positive_literal L \<or> negative_literal L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive_literal L \<or> negative_literal L
[PROOF STEP]
using negative_literal.simps(2) positive_literal.elims(3)
[PROOF STATE]
proof (prove)
using this:
negative_literal (Neg ?x) = True
\<lbrakk>\<not> positive_literal ?x; \<And>x. ?x = Neg x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. positive_literal L \<or> negative_literal L
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
positive_literal L \<or> negative_literal L

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive_literal L \<or> negative_literal L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
positive_literal L \<or> negative_literal L

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. positive_literal L \<Longrightarrow> mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
 2. negative_literal L \<Longrightarrow> mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
assume "positive_literal L"
[PROOF STATE]
proof (state)
this:
positive_literal L

goal (2 subgoals):
 1. positive_literal L \<Longrightarrow> mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
 2. negative_literal L \<Longrightarrow> mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive_literal L
[PROOF STEP]
obtain t s where "L = Pos (Eq t s)"
[PROOF STATE]
proof (prove)
using this:
positive_literal L

goal (1 subgoal):
 1. (\<And>t s. L = Pos (Eq t s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis equation.exhaust positive_literal.elims(2))
[PROOF STATE]
proof (state)
this:
L = Pos (Eq t s)

goal (2 subgoals):
 1. positive_literal L \<Longrightarrow> mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
 2. negative_literal L \<Longrightarrow> mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s)

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}

goal (1 subgoal):
 1. negative_literal L \<Longrightarrow> mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. negative_literal L \<Longrightarrow> mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
assume "negative_literal L"
[PROOF STATE]
proof (state)
this:
negative_literal L

goal (1 subgoal):
 1. negative_literal L \<Longrightarrow> mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
negative_literal L
[PROOF STEP]
obtain t s where "L = Neg (Eq t s)"
[PROOF STATE]
proof (prove)
using this:
negative_literal L

goal (1 subgoal):
 1. (\<And>t s. L = Neg (Eq t s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis equation.exhaust negative_literal.elims(2))
[PROOF STATE]
proof (state)
this:
L = Neg (Eq t s)

goal (1 subgoal):
 1. negative_literal L \<Longrightarrow> mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq t s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq t s)

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L \<sigma>) = {#x \<lhd> \<sigma>. x \<in># mset_lit L#}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lit_ord_irrefl:
  shows "(L,L) \<notin> lit_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (L, L) \<notin> lit_ord
[PROOF STEP]
by (simp add: lit_ord_wf)


[STATEMENT]
lemma lit_ord_subst:
  assumes "(L,M) \<in> lit_ord"
  shows "((subst_lit L \<sigma>), (subst_lit M \<sigma>)) \<in> lit_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
let ?f = "\<lambda>x. (subst x \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
have i: "\<And> t s. ((t,s) \<in> trm_ord \<Longrightarrow> ((?f t), (?f s)) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t s. (t, s) \<in> trm_ord \<Longrightarrow> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_subst
[PROOF STATE]
proof (prove)
using this:
\<forall>s x y. (x, y) \<in> trm_ord \<longrightarrow> (x \<lhd> s, y \<lhd> s) \<in> trm_ord

goal (1 subgoal):
 1. \<And>t s. (t, s) \<in> trm_ord \<Longrightarrow> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(?t, ?s) \<in> trm_ord \<Longrightarrow> (?t \<lhd> \<sigma>, ?s \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
(L, M) \<in> lit_ord
[PROOF STEP]
have ii: "( (mset_lit L),(mset_lit M)) \<in> (mult trm_ord)"
[PROOF STATE]
proof (prove)
using this:
(L, M) \<in> lit_ord

goal (1 subgoal):
 1. (mset_lit L, mset_lit M) \<in> mult trm_ord
[PROOF STEP]
unfolding lit_ord_def
[PROOF STATE]
proof (prove)
using this:
(L, M) \<in> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

goal (1 subgoal):
 1. (mset_lit L, mset_lit M) \<in> mult trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mset_lit L, mset_lit M) \<in> mult trm_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
let ?L = "{# (?f x). x \<in># (mset_lit L) #}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
let ?M = "{# (?f x). x \<in># (mset_lit M) #}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
from i and ii
[PROOF STATE]
proof (chain)
picking this:
(?t, ?s) \<in> trm_ord \<Longrightarrow> (?t \<lhd> \<sigma>, ?s \<lhd> \<sigma>) \<in> trm_ord
(mset_lit L, mset_lit M) \<in> mult trm_ord
[PROOF STEP]
have iii: "( ?L,?M ) \<in> (mult trm_ord)"
[PROOF STATE]
proof (prove)
using this:
(?t, ?s) \<in> trm_ord \<Longrightarrow> (?t \<lhd> \<sigma>, ?s \<lhd> \<sigma>) \<in> trm_ord
(mset_lit L, mset_lit M) \<in> mult trm_ord

goal (1 subgoal):
 1. ({#x \<lhd> \<sigma>. x \<in># mset_lit L#}, {#x \<lhd> \<sigma>. x \<in># mset_lit M#}) \<in> mult trm_ord
[PROOF STEP]
using monotonic_fun_mult
[PROOF STATE]
proof (prove)
using this:
(?t, ?s) \<in> trm_ord \<Longrightarrow> (?t \<lhd> \<sigma>, ?s \<lhd> \<sigma>) \<in> trm_ord
(mset_lit L, mset_lit M) \<in> mult trm_ord
\<lbrakk>\<And>t s. (t, s) \<in> ?r \<Longrightarrow> (?f t, ?f s) \<in> ?r; (?E1.0, ?E2.0) \<in> mult ?r\<rbrakk> \<Longrightarrow> (image_mset ?f ?E1.0, image_mset ?f ?E2.0) \<in> mult ?r

goal (1 subgoal):
 1. ({#x \<lhd> \<sigma>. x \<in># mset_lit L#}, {#x \<lhd> \<sigma>. x \<in># mset_lit M#}) \<in> mult trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
({#x \<lhd> \<sigma>. x \<in># mset_lit L#}, {#x \<lhd> \<sigma>. x \<in># mset_lit M#}) \<in> mult trm_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
have l: "?L = (mset_lit (subst_lit L \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#x \<lhd> \<sigma>. x \<in># mset_lit L#} = mset_lit (subst_lit L \<sigma>)
[PROOF STEP]
using mset_lit_subst
[PROOF STATE]
proof (prove)
using this:
mset_lit (subst_lit ?L ?\<sigma>) = {#x \<lhd> ?\<sigma>. x \<in># mset_lit ?L#}

goal (1 subgoal):
 1. {#x \<lhd> \<sigma>. x \<in># mset_lit L#} = mset_lit (subst_lit L \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#x \<lhd> \<sigma>. x \<in># mset_lit L#} = mset_lit (subst_lit L \<sigma>)

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
have m: "?M = (mset_lit (subst_lit M \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#x \<lhd> \<sigma>. x \<in># mset_lit M#} = mset_lit (subst_lit M \<sigma>)
[PROOF STEP]
using mset_lit_subst
[PROOF STATE]
proof (prove)
using this:
mset_lit (subst_lit ?L ?\<sigma>) = {#x \<lhd> ?\<sigma>. x \<in># mset_lit ?L#}

goal (1 subgoal):
 1. {#x \<lhd> \<sigma>. x \<in># mset_lit M#} = mset_lit (subst_lit M \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#x \<lhd> \<sigma>. x \<in># mset_lit M#} = mset_lit (subst_lit M \<sigma>)

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
from l m iii
[PROOF STATE]
proof (chain)
picking this:
{#x \<lhd> \<sigma>. x \<in># mset_lit L#} = mset_lit (subst_lit L \<sigma>)
{#x \<lhd> \<sigma>. x \<in># mset_lit M#} = mset_lit (subst_lit M \<sigma>)
({#x \<lhd> \<sigma>. x \<in># mset_lit L#}, {#x \<lhd> \<sigma>. x \<in># mset_lit M#}) \<in> mult trm_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{#x \<lhd> \<sigma>. x \<in># mset_lit L#} = mset_lit (subst_lit L \<sigma>)
{#x \<lhd> \<sigma>. x \<in># mset_lit M#} = mset_lit (subst_lit M \<sigma>)
({#x \<lhd> \<sigma>. x \<in># mset_lit L#}, {#x \<lhd> \<sigma>. x \<in># mset_lit M#}) \<in> mult trm_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord
[PROOF STEP]
unfolding lit_ord_def
[PROOF STATE]
proof (prove)
using this:
{#x \<lhd> \<sigma>. x \<in># mset_lit L#} = mset_lit (subst_lit L \<sigma>)
{#x \<lhd> \<sigma>. x \<in># mset_lit M#} = mset_lit (subst_lit M \<sigma>)
({#x \<lhd> \<sigma>. x \<in># mset_lit L#}, {#x \<lhd> \<sigma>. x \<in># mset_lit M#}) \<in> mult trm_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(subst_lit L \<sigma>, subst_lit M \<sigma>) \<in> lit_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma args_are_strictly_lower:
   assumes "is_compound t"
   shows "(lhs t,t) \<in> trm_ord \<and> (rhs t,t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lhs t, t) \<in> trm_ord \<and> (rhs t, t) \<in> trm_ord
[PROOF STEP]
by (metis assms is_compound.elims(2) lhs.simps(1) rhs.simps(1) trm_ord_subterm)


[STATEMENT]
lemma mset_subst:
  assumes "C' = subst_cl D \<theta>"
  assumes "\<sigma> \<doteq> \<theta> \<lozenge> \<eta>"
  assumes "finite D"
  shows "mset_cl (C',\<eta>) = mset_cl (D,\<sigma>) \<or> (mset_cl (C',\<eta>),mset_cl (D,\<sigma>)) \<in> (mult (mult trm_ord))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
let ?f = "\<lambda>x. (subst_lit x \<theta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
let ?g = "\<lambda>x. (mset_lit (subst_lit x \<eta>))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
let ?h = "\<lambda>x. (mset_lit (subst_lit x \<sigma>))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
have i: "\<forall>x \<in> D. ( (?g (?f x)) = (?h x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>D. mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = mset_lit (subst_lit x \<sigma>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> D \<Longrightarrow> mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = mset_lit (subst_lit x \<sigma>)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> D \<Longrightarrow> mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = mset_lit (subst_lit x \<sigma>)
[PROOF STEP]
have "(subst_lit (subst_lit x \<theta>) \<eta>) = (subst_lit x (\<theta> \<lozenge> \<eta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_lit (subst_lit x \<theta>) \<eta> = subst_lit x (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
using composition_of_substs_lit
[PROOF STATE]
proof (prove)
using this:
subst_lit (subst_lit ?l ?\<sigma>) ?\<eta> = subst_lit ?l (?\<sigma> \<lozenge> ?\<eta>)

goal (1 subgoal):
 1. subst_lit (subst_lit x \<theta>) \<eta> = subst_lit x (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_lit (subst_lit x \<theta>) \<eta> = subst_lit x (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. \<And>x. x \<in> D \<Longrightarrow> mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = mset_lit (subst_lit x \<sigma>)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "(subst_lit x  \<sigma>) = (subst_lit x (\<theta> \<lozenge> \<eta>))"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. subst_lit x \<sigma> = subst_lit x (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
using subst_eq_lit
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
?\<sigma> \<doteq> ?\<eta> \<Longrightarrow> subst_lit ?l ?\<sigma> = subst_lit ?l ?\<eta>

goal (1 subgoal):
 1. subst_lit x \<sigma> = subst_lit x (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_lit x \<sigma> = subst_lit x (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. \<And>x. x \<in> D \<Longrightarrow> mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = mset_lit (subst_lit x \<sigma>)
[PROOF STEP]
from this \<open>(subst_lit (subst_lit x \<theta>) \<eta>) = (subst_lit x (\<theta> \<lozenge> \<eta>))\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit x \<sigma> = subst_lit x (\<theta> \<lozenge> \<eta>)
subst_lit (subst_lit x \<theta>) \<eta> = subst_lit x (\<theta> \<lozenge> \<eta>)
[PROOF STEP]
show "(?g (?f x)) = (?h x)"
[PROOF STATE]
proof (prove)
using this:
subst_lit x \<sigma> = subst_lit x (\<theta> \<lozenge> \<eta>)
subst_lit (subst_lit x \<theta>) \<eta> = subst_lit x (\<theta> \<lozenge> \<eta>)

goal (1 subgoal):
 1. mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = mset_lit (subst_lit x \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = mset_lit (subst_lit x \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>D. mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = mset_lit (subst_lit x \<sigma>)

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
finite D
[PROOF STEP]
have "mset_set (?f ` D) \<subseteq>#  {# (?f x). x \<in># mset_set (D) #}"
[PROOF STATE]
proof (prove)
using this:
finite D

goal (1 subgoal):
 1. mset_set ((\<lambda>x. subst_lit x \<theta>) ` D) \<subseteq># {#subst_lit x \<theta>. x \<in># mset_set D#}
[PROOF STEP]
using mset_set_mset_image
[PROOF STATE]
proof (prove)
using this:
finite D
\<lbrakk>card ?E = ?N; finite ?E\<rbrakk> \<Longrightarrow> mset_set (?g ` ?E) \<subseteq># image_mset ?g (mset_set ?E)

goal (1 subgoal):
 1. mset_set ((\<lambda>x. subst_lit x \<theta>) ` D) \<subseteq># {#subst_lit x \<theta>. x \<in># mset_set D#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_set ((\<lambda>x. subst_lit x \<theta>) ` D) \<subseteq># {#subst_lit x \<theta>. x \<in># mset_set D#}

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_set ((\<lambda>x. subst_lit x \<theta>) ` D) \<subseteq># {#subst_lit x \<theta>. x \<in># mset_set D#}
[PROOF STEP]
have ii: "{# (?g x). x \<in># mset_set (?f ` D) #} \<subseteq>#  {# (?g x). x \<in># {# (?f x). x \<in># mset_set (D) #} #}"
[PROOF STATE]
proof (prove)
using this:
mset_set ((\<lambda>x. subst_lit x \<theta>) ` D) \<subseteq># {#subst_lit x \<theta>. x \<in># mset_set D#}

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit x \<eta>). x \<in># {#subst_lit x \<theta>. x \<in># mset_set D#}#}
[PROOF STEP]
using image_mset_subseteq_mono
[PROOF STATE]
proof (prove)
using this:
mset_set ((\<lambda>x. subst_lit x \<theta>) ` D) \<subseteq># {#subst_lit x \<theta>. x \<in># mset_set D#}
?A \<subseteq># ?B \<Longrightarrow> image_mset ?f ?A \<subseteq># image_mset ?f ?B

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit x \<eta>). x \<in># {#subst_lit x \<theta>. x \<in># mset_set D#}#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit x \<eta>). x \<in># {#subst_lit x \<theta>. x \<in># mset_set D#}#}

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
have "{# (?g x). x \<in># {# (?f x). x \<in># mset_set (D) #} #} = {# (?g (?f x)). x \<in># mset_set D #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<eta>). x \<in># {#subst_lit x \<theta>. x \<in># mset_set D#}#} = {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#}
[PROOF STEP]
using mset_image_comp [of ?g ?f ]
[PROOF STATE]
proof (prove)
using this:
{#mset_lit (subst_lit x \<eta>). x \<in># {#subst_lit x \<theta>. x \<in># ?E#}#} = {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># ?E#}

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<eta>). x \<in># {#subst_lit x \<theta>. x \<in># mset_set D#}#} = {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<eta>). x \<in># {#subst_lit x \<theta>. x \<in># mset_set D#}#} = {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#}

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
from this and ii
[PROOF STATE]
proof (chain)
picking this:
{#mset_lit (subst_lit x \<eta>). x \<in># {#subst_lit x \<theta>. x \<in># mset_set D#}#} = {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#}
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit x \<eta>). x \<in># {#subst_lit x \<theta>. x \<in># mset_set D#}#}
[PROOF STEP]
have
    iii: "{# (?g x). x \<in># mset_set (?f ` D) #} \<subseteq># {# (?g (?f x)). x \<in># mset_set D #}"
[PROOF STATE]
proof (prove)
using this:
{#mset_lit (subst_lit x \<eta>). x \<in># {#subst_lit x \<theta>. x \<in># mset_set D#}#} = {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#}
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit x \<eta>). x \<in># {#subst_lit x \<theta>. x \<in># mset_set D#}#}

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#}

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>D. mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = mset_lit (subst_lit x \<sigma>)
[PROOF STEP]
have "{# (?g (?f x)). x \<in># (mset_set D) #} = {# (?h x). x \<in># (mset_set D)  #} "
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>D. mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = mset_lit (subst_lit x \<sigma>)

goal (1 subgoal):
 1. {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set D#}
[PROOF STEP]
using equal_image_mset [of D "\<lambda>x. (?g (?f x))"]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>D. mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = mset_lit (subst_lit x \<sigma>)
\<forall>x\<in>D. mset_lit (subst_lit (subst_lit x \<theta>) \<eta>) = ?g x \<Longrightarrow> {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#} = image_mset ?g (mset_set D)

goal (1 subgoal):
 1. {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set D#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set D#}

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
from this and iii
[PROOF STATE]
proof (chain)
picking this:
{#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set D#}
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#}
[PROOF STEP]
have "{# (?g x). x \<in># mset_set (?f ` D) #} \<subseteq># {# (?h x). x \<in># mset_set D #}"
[PROOF STATE]
proof (prove)
using this:
{#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#} = {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set D#}
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit (subst_lit x \<theta>) \<eta>). x \<in># mset_set D#}

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set D#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set D#}

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set D#}
[PROOF STEP]
have iv: "{# (?g x). x \<in># mset_set (?f ` D) #} \<subseteq># mset_cl (D,\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set D#}

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># mset_cl (D, \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># mset_cl (D, \<sigma>)

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
C' = subst_cl D \<theta>
[PROOF STEP]
have "((\<lambda>x. subst_lit x \<theta>) ` D) = C'"
[PROOF STATE]
proof (prove)
using this:
C' = subst_cl D \<theta>

goal (1 subgoal):
 1. (\<lambda>x. subst_lit x \<theta>) ` D = C'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. subst_lit x \<theta>) ` D = C'

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
from this and iv
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. subst_lit x \<theta>) ` D = C'
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># mset_cl (D, \<sigma>)
[PROOF STEP]
have "{#mset_lit (subst_lit x \<eta>). x \<in># mset_set C' #} \<subseteq># mset_cl (D, \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. subst_lit x \<theta>) ` D = C'
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set ((\<lambda>x. subst_lit x \<theta>) ` D)#} \<subseteq># mset_cl (D, \<sigma>)

goal (1 subgoal):
 1. {#mset_lit (subst_lit x \<eta>). x \<in># mset_set C'#} \<subseteq># mset_cl (D, \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set C'#} \<subseteq># mset_cl (D, \<sigma>)

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set C'#} \<subseteq># mset_cl (D, \<sigma>)
[PROOF STEP]
have "mset_cl (C', \<eta>) \<subseteq># mset_cl (D, \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
{#mset_lit (subst_lit x \<eta>). x \<in># mset_set C'#} \<subseteq># mset_cl (D, \<sigma>)

goal (1 subgoal):
 1. mset_cl (C', \<eta>) \<subseteq># mset_cl (D, \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_cl (C', \<eta>) \<subseteq># mset_cl (D, \<sigma>)

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_cl (C', \<eta>) \<subseteq># mset_cl (D, \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mset_cl (C', \<eta>) \<subseteq># mset_cl (D, \<sigma>)

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
using multiset_order_inclusion_eq mult_trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
mset_cl (C', \<eta>) \<subseteq># mset_cl (D, \<sigma>)
\<lbrakk>?E \<subseteq># ?F; trans ?r\<rbrakk> \<Longrightarrow> ?E = ?F \<or> (?E, ?F) \<in> mult ?r
trans (mult trm_ord)

goal (1 subgoal):
 1. mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_cl (C', \<eta>) = mset_cl (D, \<sigma>) \<or> (mset_cl (C', \<eta>), mset_cl (D, \<sigma>)) \<in> mult (mult trm_ord)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_lit_exists:
  shows "finite C \<Longrightarrow> C \<noteq> {} \<longrightarrow> ground_clause C \<longrightarrow> (\<exists>L. (L \<in> C \<and> (maximal_literal L C)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite C \<Longrightarrow> C \<noteq> {} \<longrightarrow> ground_clause C \<longrightarrow> (\<exists>L. L \<in> C \<and> maximal_literal L C)
[PROOF STEP]
proof (induction rule: finite.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {} \<noteq> {} \<longrightarrow> ground_clause {} \<longrightarrow> (\<exists>L. L \<in> {} \<and> maximal_literal L {})
 2. \<And>A a. \<lbrakk>finite A; A \<noteq> {} \<longrightarrow> ground_clause A \<longrightarrow> (\<exists>L. L \<in> A \<and> maximal_literal L A)\<rbrakk> \<Longrightarrow> insert a A \<noteq> {} \<longrightarrow> ground_clause (insert a A) \<longrightarrow> (\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A))
[PROOF STEP]
case emptyI
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. {} \<noteq> {} \<longrightarrow> ground_clause {} \<longrightarrow> (\<exists>L. L \<in> {} \<and> maximal_literal L {})
 2. \<And>A a. \<lbrakk>finite A; A \<noteq> {} \<longrightarrow> ground_clause A \<longrightarrow> (\<exists>L. L \<in> A \<and> maximal_literal L A)\<rbrakk> \<Longrightarrow> insert a A \<noteq> {} \<longrightarrow> ground_clause (insert a A) \<longrightarrow> (\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<noteq> {} \<longrightarrow> ground_clause {} \<longrightarrow> (\<exists>L. L \<in> {} \<and> maximal_literal L {})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{} \<noteq> {} \<longrightarrow> ground_clause {} \<longrightarrow> (\<exists>L. L \<in> {} \<and> maximal_literal L {})

goal (1 subgoal):
 1. \<And>A a. \<lbrakk>finite A; A \<noteq> {} \<longrightarrow> ground_clause A \<longrightarrow> (\<exists>L. L \<in> A \<and> maximal_literal L A)\<rbrakk> \<Longrightarrow> insert a A \<noteq> {} \<longrightarrow> ground_clause (insert a A) \<longrightarrow> (\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A a. \<lbrakk>finite A; A \<noteq> {} \<longrightarrow> ground_clause A \<longrightarrow> (\<exists>L. L \<in> A \<and> maximal_literal L A)\<rbrakk> \<Longrightarrow> insert a A \<noteq> {} \<longrightarrow> ground_clause (insert a A) \<longrightarrow> (\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A))
[PROOF STEP]
fix A :: "'a clause" and a:: "'a literal"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A a. \<lbrakk>finite A; A \<noteq> {} \<longrightarrow> ground_clause A \<longrightarrow> (\<exists>L. L \<in> A \<and> maximal_literal L A)\<rbrakk> \<Longrightarrow> insert a A \<noteq> {} \<longrightarrow> ground_clause (insert a A) \<longrightarrow> (\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A))
[PROOF STEP]
assume "finite A"
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. \<And>A a. \<lbrakk>finite A; A \<noteq> {} \<longrightarrow> ground_clause A \<longrightarrow> (\<exists>L. L \<in> A \<and> maximal_literal L A)\<rbrakk> \<Longrightarrow> insert a A \<noteq> {} \<longrightarrow> ground_clause (insert a A) \<longrightarrow> (\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A))
[PROOF STEP]
assume hyp_ind: "A \<noteq> {} \<longrightarrow> ground_clause A \<longrightarrow> (\<exists>L. (L \<in> A \<and> (maximal_literal L A)))"
[PROOF STATE]
proof (state)
this:
A \<noteq> {} \<longrightarrow> ground_clause A \<longrightarrow> (\<exists>L. L \<in> A \<and> maximal_literal L A)

goal (1 subgoal):
 1. \<And>A a. \<lbrakk>finite A; A \<noteq> {} \<longrightarrow> ground_clause A \<longrightarrow> (\<exists>L. L \<in> A \<and> maximal_literal L A)\<rbrakk> \<Longrightarrow> insert a A \<noteq> {} \<longrightarrow> ground_clause (insert a A) \<longrightarrow> (\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A))
[PROOF STEP]
show "(insert a A) \<noteq> {} \<longrightarrow> ground_clause (insert a A)
          \<longrightarrow> (\<exists>L. (L \<in> (insert a A) \<and> (maximal_literal L (insert a A))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert a A \<noteq> {} \<longrightarrow> ground_clause (insert a A) \<longrightarrow> (\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A))
[PROOF STEP]
proof ((rule impI)+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>insert a A \<noteq> {}; ground_clause (insert a A)\<rbrakk> \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
assume "insert a A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
insert a A \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>insert a A \<noteq> {}; ground_clause (insert a A)\<rbrakk> \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
assume "ground_clause (insert a A)"
[PROOF STATE]
proof (state)
this:
ground_clause (insert a A)

goal (1 subgoal):
 1. \<lbrakk>insert a A \<noteq> {}; ground_clause (insert a A)\<rbrakk> \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
show "(\<exists>L. (L \<in> (insert a A) \<and> (maximal_literal L (insert a A))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
 2. \<not> ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
assume "A = {}"
[PROOF STATE]
proof (state)
this:
A = {}

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
 2. \<not> ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = {}
[PROOF STEP]
have "a \<in> (insert a A) \<and> (maximal_literal a (insert a A))"
[PROOF STATE]
proof (prove)
using this:
A = {}

goal (1 subgoal):
 1. a \<in> insert a A \<and> maximal_literal a (insert a A)
[PROOF STEP]
unfolding maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
A = {}

goal (1 subgoal):
 1. a \<in> insert a A \<and> (\<forall>x. x \<in> insert a A \<longrightarrow> (a, x) \<notin> lit_ord)
[PROOF STEP]
using lit_ord_irrefl
[PROOF STATE]
proof (prove)
using this:
A = {}
(?L, ?L) \<notin> lit_ord

goal (1 subgoal):
 1. a \<in> insert a A \<and> (\<forall>x. x \<in> insert a A \<longrightarrow> (a, x) \<notin> lit_ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> insert a A \<and> maximal_literal a (insert a A)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
 2. \<not> ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> insert a A \<and> maximal_literal a (insert a A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<in> insert a A \<and> maximal_literal a (insert a A)

goal (1 subgoal):
 1. \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
assume "A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
have "insert a A = {a} \<union> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert a A = {a} \<union> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert a A = {a} \<union> A

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert a A = {a} \<union> A
[PROOF STEP]
have "vars_of_cl (insert a A) = vars_of_cl A \<union> vars_of_lit a"
[PROOF STATE]
proof (prove)
using this:
insert a A = {a} \<union> A

goal (1 subgoal):
 1. vars_of_cl (insert a A) = vars_of_cl A \<union> vars_of_lit a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_cl (insert a A) = vars_of_cl A \<union> vars_of_lit a

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
from this and \<open>ground_clause (insert a A)\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_cl (insert a A) = vars_of_cl A \<union> vars_of_lit a
ground_clause (insert a A)
[PROOF STEP]
have
        "vars_of_lit a = {}" and "ground_clause A"
[PROOF STATE]
proof (prove)
using this:
vars_of_cl (insert a A) = vars_of_cl A \<union> vars_of_lit a
ground_clause (insert a A)

goal (1 subgoal):
 1. vars_of_lit a = {} &&& ground_clause A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_lit a = {}
ground_clause A

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
from \<open>ground_clause A\<close> and \<open>A \<noteq> {}\<close> and hyp_ind
[PROOF STATE]
proof (chain)
picking this:
ground_clause A
A \<noteq> {}
A \<noteq> {} \<longrightarrow> ground_clause A \<longrightarrow> (\<exists>L. L \<in> A \<and> maximal_literal L A)
[PROOF STEP]
obtain b where
        "b \<in> A" and "maximal_literal b A"
[PROOF STATE]
proof (prove)
using this:
ground_clause A
A \<noteq> {}
A \<noteq> {} \<longrightarrow> ground_clause A \<longrightarrow> (\<exists>L. L \<in> A \<and> maximal_literal L A)

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>b \<in> A; maximal_literal b A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> A
maximal_literal b A

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
 2. \<not> ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
assume "maximal_literal a A"
[PROOF STATE]
proof (state)
this:
maximal_literal a A

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
 2. \<not> ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
maximal_literal a A
[PROOF STEP]
have "maximal_literal a (insert a A)"
[PROOF STATE]
proof (prove)
using this:
maximal_literal a A

goal (1 subgoal):
 1. maximal_literal a (insert a A)
[PROOF STEP]
using lit_ord_wf maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
maximal_literal a A
wf lit_ord
maximal_literal ?L ?C = (\<forall>x. x \<in> ?C \<longrightarrow> (?L, x) \<notin> lit_ord)

goal (1 subgoal):
 1. maximal_literal a (insert a A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
maximal_literal a (insert a A)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
 2. \<not> ?P \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
maximal_literal a (insert a A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
maximal_literal a (insert a A)

goal (1 subgoal):
 1. \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)

goal (1 subgoal):
 1. \<not> maximal_literal a A \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> maximal_literal a A \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
assume "\<not>maximal_literal a A"
[PROOF STATE]
proof (state)
this:
\<not> maximal_literal a A

goal (1 subgoal):
 1. \<not> maximal_literal a A \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> maximal_literal a A
[PROOF STEP]
obtain a' where "a' \<in> A" and "(a,a') \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
\<not> maximal_literal a A

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>a' \<in> A; (a, a') \<in> lit_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x. x \<in> A \<longrightarrow> (a, x) \<notin> lit_ord)

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>a' \<in> A; (a, a') \<in> lit_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a' \<in> A
(a, a') \<in> lit_ord

goal (1 subgoal):
 1. \<not> maximal_literal a A \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
from \<open>a' \<in> A\<close> and \<open>maximal_literal b A\<close>
[PROOF STATE]
proof (chain)
picking this:
a' \<in> A
maximal_literal b A
[PROOF STEP]
have "(b,a') \<notin> lit_ord"
[PROOF STATE]
proof (prove)
using this:
a' \<in> A
maximal_literal b A

goal (1 subgoal):
 1. (b, a') \<notin> lit_ord
[PROOF STEP]
unfolding maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
a' \<in> A
\<forall>x. x \<in> A \<longrightarrow> (b, x) \<notin> lit_ord

goal (1 subgoal):
 1. (b, a') \<notin> lit_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(b, a') \<notin> lit_ord

goal (1 subgoal):
 1. \<not> maximal_literal a A \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
from this and \<open>(a,a') \<in> lit_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(b, a') \<notin> lit_ord
(a, a') \<in> lit_ord
[PROOF STEP]
have "(b,a) \<notin> lit_ord"
[PROOF STATE]
proof (prove)
using this:
(b, a') \<notin> lit_ord
(a, a') \<in> lit_ord

goal (1 subgoal):
 1. (b, a) \<notin> lit_ord
[PROOF STEP]
unfolding lit_ord_def
[PROOF STATE]
proof (prove)
using this:
(b, a') \<notin> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
(a, a') \<in> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}

goal (1 subgoal):
 1. (b, a) \<notin> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
[PROOF STEP]
using mult_def trancl_trans
[PROOF STATE]
proof (prove)
using this:
(b, a') \<notin> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
(a, a') \<in> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
mult ?r = (mult1 ?r)\<^sup>+
\<lbrakk>(?x, ?y) \<in> ?r\<^sup>+; (?y, ?z) \<in> ?r\<^sup>+\<rbrakk> \<Longrightarrow> (?x, ?z) \<in> ?r\<^sup>+

goal (1 subgoal):
 1. (b, a) \<notin> {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(b, a) \<notin> lit_ord

goal (1 subgoal):
 1. \<not> maximal_literal a A \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
from this and \<open>maximal_literal b A\<close>
[PROOF STATE]
proof (chain)
picking this:
(b, a) \<notin> lit_ord
maximal_literal b A
[PROOF STEP]
have "maximal_literal b (insert a A)"
[PROOF STATE]
proof (prove)
using this:
(b, a) \<notin> lit_ord
maximal_literal b A

goal (1 subgoal):
 1. maximal_literal b (insert a A)
[PROOF STEP]
unfolding maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
(b, a) \<notin> lit_ord
\<forall>x. x \<in> A \<longrightarrow> (b, x) \<notin> lit_ord

goal (1 subgoal):
 1. \<forall>x. x \<in> insert a A \<longrightarrow> (b, x) \<notin> lit_ord
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
maximal_literal b (insert a A)

goal (1 subgoal):
 1. \<not> maximal_literal a A \<Longrightarrow> \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
from this and \<open>b \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
maximal_literal b (insert a A)
b \<in> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
maximal_literal b (insert a A)
b \<in> A

goal (1 subgoal):
 1. \<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insert a A \<noteq> {} \<longrightarrow> ground_clause (insert a A) \<longrightarrow> (\<exists>L. L \<in> insert a A \<and> maximal_literal L (insert a A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eligible_lit_exists:
  assumes "finite (cl_ecl C)"
  assumes "(cl_ecl C) \<noteq> {}"
  assumes "(ground_clause (subst_cl (cl_ecl C) \<sigma>))"
  shows "\<exists>L. ((eligible_literal L C \<sigma>) \<and> (L \<in> (cl_ecl C)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
 2. \<not> ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
assume "sel (cl_ecl C) = {}"
[PROOF STATE]
proof (state)
this:
sel (cl_ecl C) = {}

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
 2. \<not> ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
let ?C = "(subst_cl (cl_ecl C) \<sigma>)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
 2. \<not> ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
have "finite ?C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (subst_cl (cl_ecl C) \<sigma>)
[PROOF STEP]
by (simp add: assms(1))
[PROOF STATE]
proof (state)
this:
finite (subst_cl (cl_ecl C) \<sigma>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
 2. \<not> ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
have "?C \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_cl (cl_ecl C) \<sigma> \<noteq> {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subst_cl (cl_ecl C) \<sigma> \<noteq> {}
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
cl_ecl C \<noteq> {}
[PROOF STEP]
obtain L where "L \<in> (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
cl_ecl C \<noteq> {}

goal (1 subgoal):
 1. (\<And>L. L \<in> cl_ecl C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<in> cl_ecl C

goal (1 subgoal):
 1. subst_cl (cl_ecl C) \<sigma> \<noteq> {}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
L \<in> cl_ecl C
[PROOF STEP]
have "(subst_lit L \<sigma>) \<in> ?C"
[PROOF STATE]
proof (prove)
using this:
L \<in> cl_ecl C

goal (1 subgoal):
 1. subst_lit L \<sigma> \<in> subst_cl (cl_ecl C) \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_lit L \<sigma> \<in> subst_cl (cl_ecl C) \<sigma>

goal (1 subgoal):
 1. subst_cl (cl_ecl C) \<sigma> \<noteq> {}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subst_lit L \<sigma> \<in> subst_cl (cl_ecl C) \<sigma>
[PROOF STEP]
show "?C \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
subst_lit L \<sigma> \<in> subst_cl (cl_ecl C) \<sigma>

goal (1 subgoal):
 1. subst_cl (cl_ecl C) \<sigma> \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_cl (cl_ecl C) \<sigma> \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
subst_cl (cl_ecl C) \<sigma> \<noteq> {}

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
 2. \<not> ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
from \<open>finite ?C\<close> \<open>?C \<noteq> {}\<close> assms(3)
[PROOF STATE]
proof (chain)
picking this:
finite (subst_cl (cl_ecl C) \<sigma>)
subst_cl (cl_ecl C) \<sigma> \<noteq> {}
ground_clause (subst_cl (cl_ecl C) \<sigma>)
[PROOF STEP]
obtain L where "L \<in> ?C" "maximal_literal L ?C"
[PROOF STATE]
proof (prove)
using this:
finite (subst_cl (cl_ecl C) \<sigma>)
subst_cl (cl_ecl C) \<sigma> \<noteq> {}
ground_clause (subst_cl (cl_ecl C) \<sigma>)

goal (1 subgoal):
 1. (\<And>L. \<lbrakk>L \<in> subst_cl (cl_ecl C) \<sigma>; maximal_literal L (subst_cl (cl_ecl C) \<sigma>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using max_lit_exists
[PROOF STATE]
proof (prove)
using this:
finite (subst_cl (cl_ecl C) \<sigma>)
subst_cl (cl_ecl C) \<sigma> \<noteq> {}
ground_clause (subst_cl (cl_ecl C) \<sigma>)
finite ?C \<Longrightarrow> ?C \<noteq> {} \<longrightarrow> ground_clause ?C \<longrightarrow> (\<exists>L. L \<in> ?C \<and> maximal_literal L ?C)

goal (1 subgoal):
 1. (\<And>L. \<lbrakk>L \<in> subst_cl (cl_ecl C) \<sigma>; maximal_literal L (subst_cl (cl_ecl C) \<sigma>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
L \<in> subst_cl (cl_ecl C) \<sigma>
maximal_literal L (subst_cl (cl_ecl C) \<sigma>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
 2. \<not> ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
from \<open>L \<in> ?C\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<in> subst_cl (cl_ecl C) \<sigma>
[PROOF STEP]
obtain L' where "L' \<in> (cl_ecl C)" and "L = (subst_lit L' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L \<in> subst_cl (cl_ecl C) \<sigma>

goal (1 subgoal):
 1. (\<And>L'. \<lbrakk>L' \<in> cl_ecl C; L = subst_lit L' \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L' \<in> cl_ecl C
L = subst_lit L' \<sigma>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
 2. \<not> ?P \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
from \<open>L' \<in> (cl_ecl C)\<close> \<open>L = (subst_lit L' \<sigma>)\<close> \<open>maximal_literal L ?C\<close> \<open>sel (cl_ecl C) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
L' \<in> cl_ecl C
L = subst_lit L' \<sigma>
maximal_literal L (subst_cl (cl_ecl C) \<sigma>)
sel (cl_ecl C) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L' \<in> cl_ecl C
L = subst_lit L' \<sigma>
maximal_literal L (subst_cl (cl_ecl C) \<sigma>)
sel (cl_ecl C) = {}

goal (1 subgoal):
 1. \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
unfolding eligible_literal_def
[PROOF STATE]
proof (prove)
using this:
L' \<in> cl_ecl C
L = subst_lit L' \<sigma>
maximal_literal L (subst_cl (cl_ecl C) \<sigma>)
sel (cl_ecl C) = {}

goal (1 subgoal):
 1. \<exists>L. (L \<in> sel (cl_ecl C) \<or> sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)) \<and> L \<in> cl_ecl C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C

goal (1 subgoal):
 1. sel (cl_ecl C) \<noteq> {} \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sel (cl_ecl C) \<noteq> {} \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
assume "sel (cl_ecl C) \<noteq> {}"
[PROOF STATE]
proof (state)
this:
sel (cl_ecl C) \<noteq> {}

goal (1 subgoal):
 1. sel (cl_ecl C) \<noteq> {} \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sel (cl_ecl C) \<noteq> {}
[PROOF STEP]
obtain L where "L \<in> sel (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
sel (cl_ecl C) \<noteq> {}

goal (1 subgoal):
 1. (\<And>L. L \<in> sel (cl_ecl C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<in> sel (cl_ecl C)

goal (1 subgoal):
 1. sel (cl_ecl C) \<noteq> {} \<Longrightarrow> \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
L \<in> sel (cl_ecl C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L \<in> sel (cl_ecl C)

goal (1 subgoal):
 1. \<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C
[PROOF STEP]
unfolding eligible_literal_def
[PROOF STATE]
proof (prove)
using this:
L \<in> sel (cl_ecl C)

goal (1 subgoal):
 1. \<exists>L. (L \<in> sel (cl_ecl C) \<or> sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)) \<and> L \<in> cl_ecl C
[PROOF STEP]
using sel_neg
[PROOF STATE]
proof (prove)
using this:
L \<in> sel (cl_ecl C)
\<forall>x. sel (cl_ecl x) \<subseteq> cl_ecl x \<and> (\<forall>y\<in>sel (cl_ecl x). negative_literal y)

goal (1 subgoal):
 1. \<exists>L. (L \<in> sel (cl_ecl C) \<or> sel (cl_ecl C) = {} \<and> maximal_literal (subst_lit L \<sigma>) (subst_cl (cl_ecl C) \<sigma>)) \<and> L \<in> cl_ecl C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>L. eligible_literal L C \<sigma> \<and> L \<in> cl_ecl C

goal:
No subgoals!
[PROOF STEP]
qed