[STATEMENT]
lemma candidate_values_renaming:
    assumes "(candidate_values z CC C' C s L L' \<sigma> t' s' t S)"
    assumes "finite C'"
    assumes "finite (cl_ecl (D:: 'a eclause))"
    assumes "closed_under_renaming S"
    assumes "Ball S well_constrained"
    shows "\<exists> CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis.
     (candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S)
     \<and> (vars_of_cl (cl_ecl D)) \<inter> vars_of_cl (cl_ecl CC_bis) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
finite C'
[PROOF STEP]
have "finite (vars_of_cl C')"
[PROOF STATE]
proof (prove)
using this:
finite C'

goal (1 subgoal):
 1. finite (vars_of_cl C')
[PROOF STEP]
using set_of_variables_is_finite_cl
[PROOF STATE]
proof (prove)
using this:
finite C'
finite ?C \<Longrightarrow> finite (vars_of_cl ?C)

goal (1 subgoal):
 1. finite (vars_of_cl C')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (vars_of_cl C')

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
finite (cl_ecl D)
[PROOF STEP]
have "finite (vars_of_cl (cl_ecl D))"
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl D)

goal (1 subgoal):
 1. finite (vars_of_cl (cl_ecl D))
[PROOF STEP]
using set_of_variables_is_finite_cl
[PROOF STATE]
proof (prove)
using this:
finite (cl_ecl D)
finite ?C \<Longrightarrow> finite (vars_of_cl ?C)

goal (1 subgoal):
 1. finite (vars_of_cl (cl_ecl D))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (vars_of_cl (cl_ecl D))

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from infinite_vars
[PROOF STATE]
proof (chain)
picking this:
infinite vars
[PROOF STEP]
have "\<not> (finite vars)"
[PROOF STATE]
proof (prove)
using this:
infinite vars

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

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from \<open>finite (vars_of_cl C')\<close> \<open>finite (vars_of_cl (cl_ecl D))\<close>
    and \<open>\<not> (finite vars)\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (vars_of_cl C')
finite (vars_of_cl (cl_ecl D))
infinite vars
[PROOF STEP]
obtain \<eta> where "renaming \<eta> (vars_of_cl C')"
      and "((subst_codomain \<eta> (vars_of_cl C')) \<inter> (vars_of_cl (cl_ecl D))) = {}"
[PROOF STATE]
proof (prove)
using this:
finite (vars_of_cl C')
finite (vars_of_cl (cl_ecl D))
infinite vars

goal (1 subgoal):
 1. (\<And>\<eta>. \<lbrakk>renaming \<eta> (vars_of_cl C'); subst_codomain \<eta> (vars_of_cl C') \<inter> vars_of_cl (cl_ecl D) = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using renaming_exists [of vars ]
[PROOF STATE]
proof (prove)
using this:
finite (vars_of_cl C')
finite (vars_of_cl (cl_ecl D))
infinite vars
\<lbrakk>infinite vars; finite ?V\<rbrakk> \<Longrightarrow> \<forall>V'. finite V' \<longrightarrow> (\<exists>\<eta>. renaming \<eta> ?V \<and> subst_codomain \<eta> ?V \<inter> V' = {})

goal (1 subgoal):
 1. (\<And>\<eta>. \<lbrakk>renaming \<eta> (vars_of_cl C'); subst_codomain \<eta> (vars_of_cl C') \<inter> vars_of_cl (cl_ecl D) = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
renaming \<eta> (vars_of_cl C')
subst_codomain \<eta> (vars_of_cl C') \<inter> vars_of_cl (cl_ecl D) = {}

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this \<open>finite (vars_of_cl C')\<close>
[PROOF STATE]
proof (chain)
picking this:
renaming \<eta> (vars_of_cl C')
subst_codomain \<eta> (vars_of_cl C') \<inter> vars_of_cl (cl_ecl D) = {}
finite (vars_of_cl C')
[PROOF STEP]
obtain \<eta>'
    where i: "(\<forall> x \<in> (vars_of_cl C'). (subst (subst (Var x) \<eta> ) \<eta>')
                                      = (Var x))"
[PROOF STATE]
proof (prove)
using this:
renaming \<eta> (vars_of_cl C')
subst_codomain \<eta> (vars_of_cl C') \<inter> vars_of_cl (cl_ecl D) = {}
finite (vars_of_cl C')

goal (1 subgoal):
 1. (\<And>\<eta>'. \<forall>x\<in>vars_of_cl C'. Var x \<lhd> \<eta> \<lhd> \<eta>' = Var x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using renamings_admit_inverse
[PROOF STATE]
proof (prove)
using this:
renaming \<eta> (vars_of_cl C')
subst_codomain \<eta> (vars_of_cl C') \<inter> vars_of_cl (cl_ecl D) = {}
finite (vars_of_cl C')
\<lbrakk>finite ?V; renaming ?\<sigma> ?V\<rbrakk> \<Longrightarrow> \<exists>\<theta>. (\<forall>x\<in>?V. Var x \<lhd> ?\<sigma> \<lhd> \<theta> = Var x) \<and> (\<forall>x. x \<notin> subst_codomain ?\<sigma> ?V \<longrightarrow> Var x \<lhd> \<theta> = Var x) \<and> (\<forall>x. is_a_variable (Var x \<lhd> \<theta>))

goal (1 subgoal):
 1. (\<And>\<eta>'. \<forall>x\<in>vars_of_cl C'. Var x \<lhd> \<eta> \<lhd> \<eta>' = Var x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>vars_of_cl C'. Var x \<lhd> \<eta> \<lhd> \<eta>' = Var x

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
obtain CC_bis where "CC_bis = (subst_ecl CC \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>CC_bis. CC_bis = subst_ecl CC \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
CC_bis = subst_ecl CC \<eta>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
obtain C'_bis where "C'_bis = (subst_cl C' \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C'_bis. C'_bis = subst_cl C' \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C'_bis = subst_cl C' \<eta>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "C' = (cl_ecl CC)"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. C' = cl_ecl CC
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. C' = cl_ecl CC
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
C' = cl_ecl CC

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
C' = cl_ecl CC
[PROOF STEP]
obtain T where "CC = (Ecl C' T)"
[PROOF STATE]
proof (prove)
using this:
C' = cl_ecl CC

goal (1 subgoal):
 1. (\<And>T. CC = Ecl C' T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis cl_ecl.simps trms_ecl.elims)
[PROOF STATE]
proof (state)
this:
CC = Ecl C' T

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this and \<open>CC_bis = (subst_ecl CC \<eta>)\<close>
    and \<open>C'_bis = (subst_cl C' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
CC = Ecl C' T
CC_bis = subst_ecl CC \<eta>
C'_bis = subst_cl C' \<eta>
[PROOF STEP]
have "C'_bis = (cl_ecl CC_bis)"
[PROOF STATE]
proof (prove)
using this:
CC = Ecl C' T
CC_bis = subst_ecl CC \<eta>
C'_bis = subst_cl C' \<eta>

goal (1 subgoal):
 1. C'_bis = cl_ecl CC_bis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C'_bis = cl_ecl CC_bis

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "CC \<in> S"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. CC \<in> S
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. CC \<in> S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
CC \<in> S

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "(s,t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. (s, t) \<in> trm_ord
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

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

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "((s,t) \<in> trm_ord \<longrightarrow> (z = trm_rep s S))"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. (s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. (s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "(maximal_literal L C)"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. maximal_literal L C
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. maximal_literal L C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
maximal_literal L C

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "(ground_clause C)"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. ground_clause C
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. ground_clause C
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
ground_clause C

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "L' \<in> C'"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. L' \<in> C'
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. L' \<in> C'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
L' \<in> C'

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "L = (subst_lit L' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. L = subst_lit L' \<sigma>
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. L = subst_lit L' \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
L = subst_lit L' \<sigma>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "(smaller_lits_are_false t C S)"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. smaller_lits_are_false t C S
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. smaller_lits_are_false t C S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
smaller_lits_are_false t C S

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "C = (subst_cl C' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. C = subst_cl C' \<sigma>
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. C = subst_cl C' \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
C = subst_cl C' \<sigma>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "(orient_lit_inst L' t' s' pos \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. orient_lit_inst L' t' s' pos \<sigma>
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. orient_lit_inst L' t' s' pos \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
orient_lit_inst L' t' s' pos \<sigma>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "(trms_irreducible CC \<sigma> S t)"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. trms_irreducible CC \<sigma> S t
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. trms_irreducible CC \<sigma> S t
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trms_irreducible CC \<sigma> S t

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "t = subst t' \<sigma>"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. t = t' \<lhd> \<sigma>
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. t = t' \<lhd> \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
t = t' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "s = subst s' \<sigma>"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. s = s' \<lhd> \<sigma>
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. s = s' \<lhd> \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = s' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from \<open>CC \<in> S\<close> and assms(4) and \<open>renaming \<eta> (vars_of_cl C')\<close> and \<open>C' = (cl_ecl CC)\<close>
    \<open>CC_bis = (subst_ecl CC \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
CC \<in> S
closed_under_renaming S
renaming \<eta> (vars_of_cl C')
C' = cl_ecl CC
CC_bis = subst_ecl CC \<eta>
[PROOF STEP]
have "CC_bis \<in> S"
[PROOF STATE]
proof (prove)
using this:
CC \<in> S
closed_under_renaming S
renaming \<eta> (vars_of_cl C')
C' = cl_ecl CC
CC_bis = subst_ecl CC \<eta>

goal (1 subgoal):
 1. CC_bis \<in> S
[PROOF STEP]
unfolding closed_under_renaming_def renaming_cl_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S
\<forall>C D. C \<in> S \<longrightarrow> (\<exists>\<eta>. renaming \<eta> (vars_of_cl (cl_ecl C)) \<and> D = subst_ecl C \<eta>) \<longrightarrow> D \<in> S
renaming \<eta> (vars_of_cl C')
C' = cl_ecl CC
CC_bis = subst_ecl CC \<eta>

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

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
have "(sel C' = {})"
[PROOF STATE]
proof (prove)
using this:
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. sel C' = {}
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. sel C' = {}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
sel C' = {}

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this and \<open>renaming \<eta> (vars_of_cl C')\<close> \<open>C' = (cl_ecl CC)\<close>
    \<open>C'_bis = (subst_cl C' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
sel C' = {}
renaming \<eta> (vars_of_cl C')
C' = cl_ecl CC
C'_bis = subst_cl C' \<eta>
[PROOF STEP]
have "sel C'_bis = {}"
[PROOF STATE]
proof (prove)
using this:
sel C' = {}
renaming \<eta> (vars_of_cl C')
C' = cl_ecl CC
C'_bis = subst_cl C' \<eta>

goal (1 subgoal):
 1. sel C'_bis = {}
[PROOF STEP]
using sel_renaming
[PROOF STATE]
proof (prove)
using this:
sel C' = {}
renaming \<eta> (vars_of_cl C')
C' = cl_ecl CC
C'_bis = subst_cl C' \<eta>
\<forall>\<eta> C. renaming \<eta> (vars_of_cl C) \<longrightarrow> sel C = {} \<longrightarrow> sel (subst_cl C \<eta>) = {}

goal (1 subgoal):
 1. sel C'_bis = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sel C'_bis = {}

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
obtain L'_bis where "L'_bis = (subst_lit L' \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>L'_bis. L'_bis = subst_lit L' \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L'_bis = subst_lit L' \<eta>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this and \<open>L' \<in> C'\<close> \<open>C'_bis = (subst_cl C' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
L'_bis = subst_lit L' \<eta>
L' \<in> C'
C'_bis = subst_cl C' \<eta>
[PROOF STEP]
have "L'_bis \<in> C'_bis"
[PROOF STATE]
proof (prove)
using this:
L'_bis = subst_lit L' \<eta>
L' \<in> C'
C'_bis = subst_cl C' \<eta>

goal (1 subgoal):
 1. L'_bis \<in> C'_bis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L'_bis \<in> C'_bis

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
let ?\<theta> = "(comp (comp \<eta> \<eta>') \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
let ?\<theta>' = "(comp \<eta>' \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
have "coincide_on \<sigma> ?\<theta> (vars_of_cl C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C') \<Longrightarrow> False
[PROOF STEP]
assume "\<not>coincide_on \<sigma> ?\<theta> (vars_of_cl C')"
[PROOF STATE]
proof (state)
this:
\<not> coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')

goal (1 subgoal):
 1. \<not> coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C') \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')
[PROOF STEP]
obtain x where "(subst (Var x) \<sigma>) \<noteq> (subst (Var x) ?\<theta>)"
      and "x \<in> vars_of_cl C'"
[PROOF STATE]
proof (prove)
using this:
\<not> coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>; x \<in> vars_of_cl C'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x\<in>vars_of_cl C'. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>; x \<in> vars_of_cl C'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
x \<in> vars_of_cl C'

goal (1 subgoal):
 1. \<not> coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C') \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<in> vars_of_cl C'\<close> i
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of_cl C'
\<forall>x\<in>vars_of_cl C'. Var x \<lhd> \<eta> \<lhd> \<eta>' = Var x
[PROOF STEP]
have "(subst (subst (Var x) \<eta> ) \<eta>') = (Var x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of_cl C'
\<forall>x\<in>vars_of_cl C'. Var x \<lhd> \<eta> \<lhd> \<eta>' = Var x

goal (1 subgoal):
 1. Var x \<lhd> \<eta> \<lhd> \<eta>' = Var x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Var x \<lhd> \<eta> \<lhd> \<eta>' = Var x

goal (1 subgoal):
 1. \<not> coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C') \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst (Var x) \<sigma>) \<noteq> (subst (Var x) ?\<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
Var x \<lhd> \<eta> \<lhd> \<eta>' = Var x
Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Var x \<lhd> \<eta> \<lhd> \<eta>' = Var x
Var x \<lhd> \<sigma> \<noteq> Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from \<open>L' \<in> C'\<close>
[PROOF STATE]
proof (chain)
picking this:
L' \<in> C'
[PROOF STEP]
have "vars_of_lit L' \<subseteq> vars_of_cl C'"
[PROOF STATE]
proof (prove)
using this:
L' \<in> C'

goal (1 subgoal):
 1. vars_of_lit L' \<subseteq> vars_of_cl C'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_lit L' \<subseteq> vars_of_cl C'

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this and \<open>coincide_on \<sigma> ?\<theta> (vars_of_cl C')\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit L' \<subseteq> vars_of_cl C'
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')
[PROOF STEP]
have "coincide_on \<sigma> ?\<theta> (vars_of_lit L')"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L' \<subseteq> vars_of_cl C'
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')

goal (1 subgoal):
 1. coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit L')
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L' \<subseteq> vars_of_cl C'
\<forall>x\<in>vars_of_cl C'. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of_lit L'. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit L')

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this and \<open>L = (subst_lit L' \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit L')
L = subst_lit L' \<sigma>
[PROOF STEP]
have "L = (subst_lit L' ?\<theta>)"
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit L')
L = subst_lit L' \<sigma>

goal (1 subgoal):
 1. L = subst_lit L' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
using coincide_on_lit
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit L')
L = subst_lit L' \<sigma>
coincide_on ?\<sigma> ?\<eta> (vars_of_lit ?l) \<Longrightarrow> subst_lit ?l ?\<sigma> = subst_lit ?l ?\<eta>

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

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
have "subst_lit L' ?\<theta>
    = subst_lit (subst_lit L' \<eta>) ?\<theta>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_lit L' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) = subst_lit (subst_lit L' \<eta>) (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
by (simp add: coincide_on_def coincide_on_lit composition_of_substs_lit)
[PROOF STATE]
proof (state)
this:
subst_lit L' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) = subst_lit (subst_lit L' \<eta>) (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this and \<open>L = (subst_lit L' ?\<theta>)\<close> and
    \<open>L'_bis = (subst_lit L' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_lit L' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) = subst_lit (subst_lit L' \<eta>) (\<eta>' \<lozenge> \<sigma>)
L = subst_lit L' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
L'_bis = subst_lit L' \<eta>
[PROOF STEP]
have "L = (subst_lit L'_bis ?\<theta>')"
[PROOF STATE]
proof (prove)
using this:
subst_lit L' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) = subst_lit (subst_lit L' \<eta>) (\<eta>' \<lozenge> \<sigma>)
L = subst_lit L' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
L'_bis = subst_lit L' \<eta>

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

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from \<open>coincide_on \<sigma> ?\<theta> (vars_of_cl C')\<close> and \<open>C = (subst_cl C' \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')
C = subst_cl C' \<sigma>
[PROOF STEP]
have "C  = subst_cl C' ?\<theta>"
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')
C = subst_cl C' \<sigma>

goal (1 subgoal):
 1. C = subst_cl C' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
using coincide_on_cl
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')
C = subst_cl C' \<sigma>
coincide_on ?\<sigma> ?\<eta> (vars_of_cl ?C) \<Longrightarrow> subst_cl ?C ?\<sigma> = subst_cl ?C ?\<eta>

goal (1 subgoal):
 1. C = subst_cl C' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C = subst_cl C' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
have "subst_cl C' ?\<theta>
    = subst_cl (subst_cl C' \<eta>) ?\<theta>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_cl C' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) = subst_cl (subst_cl C' \<eta>) (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
by (metis composition_of_substs_cl)
[PROOF STATE]
proof (state)
this:
subst_cl C' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) = subst_cl (subst_cl C' \<eta>) (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this and \<open>C  = subst_cl C' ?\<theta>\<close> and \<open>C'_bis = (subst_cl C' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_cl C' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) = subst_cl (subst_cl C' \<eta>) (\<eta>' \<lozenge> \<sigma>)
C = subst_cl C' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
C'_bis = subst_cl C' \<eta>
[PROOF STEP]
have "C = subst_cl C'_bis ?\<theta>'"
[PROOF STATE]
proof (prove)
using this:
subst_cl C' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) = subst_cl (subst_cl C' \<eta>) (\<eta>' \<lozenge> \<sigma>)
C = subst_cl C' (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
C'_bis = subst_cl C' \<eta>

goal (1 subgoal):
 1. C = subst_cl C'_bis (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = subst_cl C'_bis (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from \<open>(finite C')\<close> and \<open>C'_bis = (subst_cl C' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
finite C'
C'_bis = subst_cl C' \<eta>
[PROOF STEP]
have "finite C'_bis"
[PROOF STATE]
proof (prove)
using this:
finite C'
C'_bis = subst_cl C' \<eta>

goal (1 subgoal):
 1. finite C'_bis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite C'_bis

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
have "t \<notin> (subst_set (trms_ecl CC_bis) ?\<theta>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<notin> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
assume "t \<in> (subst_set (trms_ecl CC_bis) ?\<theta>')"
[PROOF STATE]
proof (state)
this:
t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
obtain u where "u \<in> (trms_ecl CC_bis)"
      and "t = (subst u ?\<theta>')"
[PROOF STATE]
proof (prove)
using this:
t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u \<in> trms_ecl CC_bis; t = u \<lhd> \<eta>' \<lozenge> \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> trms_ecl CC_bis
t = u \<lhd> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>u \<in> (trms_ecl CC_bis)\<close> and \<open>CC_bis = (subst_ecl CC \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<in> trms_ecl CC_bis
CC_bis = subst_ecl CC \<eta>
[PROOF STEP]
obtain v where "v \<in> trms_ecl CC" and "u = (subst v \<eta>)"
[PROOF STATE]
proof (prove)
using this:
u \<in> trms_ecl CC_bis
CC_bis = subst_ecl CC \<eta>

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> trms_ecl CC; u = v \<lhd> \<eta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>CC = Ecl C' T\<close>
[PROOF STATE]
proof (prove)
using this:
u \<in> trms_ecl CC_bis
CC_bis = subst_ecl CC \<eta>
CC = Ecl C' T

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> trms_ecl CC; u = v \<lhd> \<eta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> trms_ecl CC
u = v \<lhd> \<eta>

goal (1 subgoal):
 1. t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>u = (subst v \<eta>)\<close> \<open>t = (subst u ?\<theta>')\<close>
[PROOF STATE]
proof (chain)
picking this:
u = v \<lhd> \<eta>
t = u \<lhd> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
have "subst v ?\<theta> = t"
[PROOF STATE]
proof (prove)
using this:
u = v \<lhd> \<eta>
t = u \<lhd> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = t

goal (1 subgoal):
 1. t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>v \<in> trms_ecl CC\<close> \<open>CC \<in> S\<close> assms(5)
[PROOF STATE]
proof (chain)
picking this:
v \<in> trms_ecl CC
CC \<in> S
Ball S well_constrained
[PROOF STEP]
have "dom_trm v (cl_ecl CC)"
[PROOF STATE]
proof (prove)
using this:
v \<in> trms_ecl CC
CC \<in> S
Ball S well_constrained

goal (1 subgoal):
 1. dom_trm v (cl_ecl CC)
[PROOF STEP]
unfolding Ball_def well_constrained_def
[PROOF STATE]
proof (prove)
using this:
v \<in> trms_ecl CC
CC \<in> S
\<forall>x. x \<in> S \<longrightarrow> (\<forall>y. y \<in> trms_ecl x \<longrightarrow> dom_trm y (cl_ecl x))

goal (1 subgoal):
 1. dom_trm v (cl_ecl CC)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
dom_trm v (cl_ecl CC)

goal (1 subgoal):
 1. t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
dom_trm v (cl_ecl CC)
[PROOF STEP]
have "vars_of v \<subseteq> vars_of_cl (cl_ecl CC)"
[PROOF STATE]
proof (prove)
using this:
dom_trm v (cl_ecl CC)

goal (1 subgoal):
 1. vars_of v \<subseteq> vars_of_cl (cl_ecl CC)
[PROOF STEP]
using dom_trm_vars
[PROOF STATE]
proof (prove)
using this:
dom_trm v (cl_ecl CC)
dom_trm ?t ?C \<Longrightarrow> vars_of ?t \<subseteq> vars_of_cl ?C

goal (1 subgoal):
 1. vars_of v \<subseteq> vars_of_cl (cl_ecl CC)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of v \<subseteq> vars_of_cl (cl_ecl CC)

goal (1 subgoal):
 1. t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>C' = (cl_ecl CC)\<close> \<open>coincide_on \<sigma> ?\<theta> (vars_of_cl C')\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of v \<subseteq> vars_of_cl (cl_ecl CC)
C' = cl_ecl CC
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')
[PROOF STEP]
have "coincide_on \<sigma> ?\<theta> (vars_of v)"
[PROOF STATE]
proof (prove)
using this:
vars_of v \<subseteq> vars_of_cl (cl_ecl CC)
C' = cl_ecl CC
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')

goal (1 subgoal):
 1. coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of v)
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of v \<subseteq> vars_of_cl (cl_ecl CC)
C' = cl_ecl CC
\<forall>x\<in>vars_of_cl C'. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of v. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of v)

goal (1 subgoal):
 1. t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>subst v ?\<theta> = t\<close>
[PROOF STATE]
proof (chain)
picking this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of v)
v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = t
[PROOF STEP]
have "(subst v \<sigma>) = t"
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of v)
v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = t

goal (1 subgoal):
 1. v \<lhd> \<sigma> = t
[PROOF STEP]
using coincide_on_term
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of v)
v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = t
coincide_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?t \<lhd> ?\<eta>

goal (1 subgoal):
 1. v \<lhd> \<sigma> = t
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
v \<lhd> \<sigma> = t

goal (1 subgoal):
 1. t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>v \<in> trms_ecl CC\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<lhd> \<sigma> = t
v \<in> trms_ecl CC
[PROOF STEP]
have
      "(t \<in> (subst_set (trms_ecl CC) \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
v \<lhd> \<sigma> = t
v \<in> trms_ecl CC

goal (1 subgoal):
 1. t \<in> subst_set (trms_ecl CC) \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> subst_set (trms_ecl CC) \<sigma>

goal (1 subgoal):
 1. t \<in> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
t \<in> subst_set (trms_ecl CC) \<sigma>
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
t \<in> subst_set (trms_ecl CC) \<sigma>
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
t \<in> subst_set (trms_ecl CC) \<sigma>
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. False
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<notin> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
have "(trms_irreducible CC_bis ?\<theta>' S t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t \<Longrightarrow> False
[PROOF STEP]
assume "\<not>(trms_irreducible CC_bis ?\<theta>' S t)"
[PROOF STATE]
proof (state)
this:
\<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t

goal (1 subgoal):
 1. \<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t
[PROOF STEP]
obtain x x' where "x' \<in> trms_ecl CC_bis"
            "occurs_in x (subst x' ?\<theta>')"
            "(x,t) \<in> trm_ord" "(trm_rep x S) \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
\<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t

goal (1 subgoal):
 1. (\<And>x' x. \<lbrakk>x' \<in> trms_ecl CC_bis; occurs_in x (x' \<lhd> \<eta>' \<lozenge> \<sigma>); (x, t) \<in> trm_ord; trm_rep x S \<noteq> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using trms_irreducible_def
[PROOF STATE]
proof (prove)
using this:
\<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t
trms_irreducible ?CC ?\<sigma> ?S ?t = (\<forall>x. (\<exists>x'\<in>trms_ecl ?CC. occurs_in x (x' \<lhd> ?\<sigma>)) \<longrightarrow> (x, ?t) \<in> trm_ord \<longrightarrow> trm_rep x ?S = x)

goal (1 subgoal):
 1. (\<And>x' x. \<lbrakk>x' \<in> trms_ecl CC_bis; occurs_in x (x' \<lhd> \<eta>' \<lozenge> \<sigma>); (x, t) \<in> trm_ord; trm_rep x S \<noteq> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x' \<in> trms_ecl CC_bis
occurs_in x (x' \<lhd> \<eta>' \<lozenge> \<sigma>)
(x, t) \<in> trm_ord
trm_rep x S \<noteq> x

goal (1 subgoal):
 1. \<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t \<Longrightarrow> False
[PROOF STEP]
from \<open>x' \<in> (trms_ecl CC_bis)\<close> and \<open>CC_bis = (subst_ecl CC \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
x' \<in> trms_ecl CC_bis
CC_bis = subst_ecl CC \<eta>
[PROOF STEP]
obtain v where "v \<in> trms_ecl CC" and "x' = (subst v \<eta>)"
[PROOF STATE]
proof (prove)
using this:
x' \<in> trms_ecl CC_bis
CC_bis = subst_ecl CC \<eta>

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> trms_ecl CC; x' = v \<lhd> \<eta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>CC = Ecl C' T\<close>
[PROOF STATE]
proof (prove)
using this:
x' \<in> trms_ecl CC_bis
CC_bis = subst_ecl CC \<eta>
CC = Ecl C' T

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> trms_ecl CC; x' = v \<lhd> \<eta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> trms_ecl CC
x' = v \<lhd> \<eta>

goal (1 subgoal):
 1. \<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t \<Longrightarrow> False
[PROOF STEP]
from \<open>occurs_in x (subst x' ?\<theta>')\<close> \<open>x' = subst v \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
occurs_in x (x' \<lhd> \<eta>' \<lozenge> \<sigma>)
x' = v \<lhd> \<eta>
[PROOF STEP]
have "occurs_in x (subst v ?\<theta>)"
[PROOF STATE]
proof (prove)
using this:
occurs_in x (x' \<lhd> \<eta>' \<lozenge> \<sigma>)
x' = v \<lhd> \<eta>

goal (1 subgoal):
 1. occurs_in x (v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
occurs_in x (v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. \<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t \<Longrightarrow> False
[PROOF STEP]
from \<open>v \<in> trms_ecl CC\<close> \<open>CC \<in> S\<close> assms(5)
[PROOF STATE]
proof (chain)
picking this:
v \<in> trms_ecl CC
CC \<in> S
Ball S well_constrained
[PROOF STEP]
have "dom_trm v (cl_ecl CC)"
[PROOF STATE]
proof (prove)
using this:
v \<in> trms_ecl CC
CC \<in> S
Ball S well_constrained

goal (1 subgoal):
 1. dom_trm v (cl_ecl CC)
[PROOF STEP]
unfolding Ball_def well_constrained_def
[PROOF STATE]
proof (prove)
using this:
v \<in> trms_ecl CC
CC \<in> S
\<forall>x. x \<in> S \<longrightarrow> (\<forall>y. y \<in> trms_ecl x \<longrightarrow> dom_trm y (cl_ecl x))

goal (1 subgoal):
 1. dom_trm v (cl_ecl CC)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom_trm v (cl_ecl CC)

goal (1 subgoal):
 1. \<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
dom_trm v (cl_ecl CC)
[PROOF STEP]
have "vars_of v \<subseteq> vars_of_cl (cl_ecl CC)"
[PROOF STATE]
proof (prove)
using this:
dom_trm v (cl_ecl CC)

goal (1 subgoal):
 1. vars_of v \<subseteq> vars_of_cl (cl_ecl CC)
[PROOF STEP]
using dom_trm_vars
[PROOF STATE]
proof (prove)
using this:
dom_trm v (cl_ecl CC)
dom_trm ?t ?C \<Longrightarrow> vars_of ?t \<subseteq> vars_of_cl ?C

goal (1 subgoal):
 1. vars_of v \<subseteq> vars_of_cl (cl_ecl CC)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of v \<subseteq> vars_of_cl (cl_ecl CC)

goal (1 subgoal):
 1. \<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t \<Longrightarrow> False
[PROOF STEP]
from this and \<open>C' = (cl_ecl CC)\<close> \<open>coincide_on \<sigma> ?\<theta> (vars_of_cl C')\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of v \<subseteq> vars_of_cl (cl_ecl CC)
C' = cl_ecl CC
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')
[PROOF STEP]
have "coincide_on \<sigma> ?\<theta> (vars_of v)"
[PROOF STATE]
proof (prove)
using this:
vars_of v \<subseteq> vars_of_cl (cl_ecl CC)
C' = cl_ecl CC
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')

goal (1 subgoal):
 1. coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of v)
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of v \<subseteq> vars_of_cl (cl_ecl CC)
C' = cl_ecl CC
\<forall>x\<in>vars_of_cl C'. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of v. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of v)

goal (1 subgoal):
 1. \<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of v)
[PROOF STEP]
have "(subst v \<sigma>) = (subst v ?\<theta>)"
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of v)

goal (1 subgoal):
 1. v \<lhd> \<sigma> = v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
using coincide_on_term
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of v)
coincide_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?t \<lhd> ?\<eta>

goal (1 subgoal):
 1. v \<lhd> \<sigma> = v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
v \<lhd> \<sigma> = v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. \<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t \<Longrightarrow> False
[PROOF STEP]
from this and \<open>occurs_in x (subst v ?\<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<lhd> \<sigma> = v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
occurs_in x (v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
have "occurs_in x (subst v \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
v \<lhd> \<sigma> = v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
occurs_in x (v \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. occurs_in x (v \<lhd> \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
occurs_in x (v \<lhd> \<sigma>)

goal (1 subgoal):
 1. \<not> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t \<Longrightarrow> False
[PROOF STEP]
from this and \<open>v \<in> trms_ecl CC\<close> and \<open>(x,t) \<in> trm_ord\<close>
      \<open>(trm_rep x S) \<noteq> x\<close> and \<open>(trms_irreducible CC \<sigma> S t)\<close>
[PROOF STATE]
proof (chain)
picking this:
occurs_in x (v \<lhd> \<sigma>)
v \<in> trms_ecl CC
(x, t) \<in> trm_ord
trm_rep x S \<noteq> x
trms_irreducible CC \<sigma> S t
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
occurs_in x (v \<lhd> \<sigma>)
v \<in> trms_ecl CC
(x, t) \<in> trm_ord
trm_rep x S \<noteq> x
trms_irreducible CC \<sigma> S t

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding trms_irreducible_def
[PROOF STATE]
proof (prove)
using this:
occurs_in x (v \<lhd> \<sigma>)
v \<in> trms_ecl CC
(x, t) \<in> trm_ord
trm_rep x S \<noteq> x
\<forall>x. (\<exists>x'\<in>trms_ecl CC. occurs_in x (x' \<lhd> \<sigma>)) \<longrightarrow> (x, t) \<in> trm_ord \<longrightarrow> trm_rep x S = x

goal (1 subgoal):
 1. False
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
obtain t'_bis where "t'_bis = (subst t' \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t'_bis. t'_bis = t' \<lhd> \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t'_bis = t' \<lhd> \<eta>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
obtain s'_bis where "s'_bis = (subst s' \<eta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s'_bis. s'_bis = s' \<lhd> \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s'_bis = s' \<lhd> \<eta>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from \<open>(orient_lit_inst L' t' s' pos \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L' t' s' pos \<sigma>
[PROOF STEP]
have "vars_of t' \<subseteq> vars_of_lit L'"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L' t' s' pos \<sigma>

goal (1 subgoal):
 1. vars_of t' \<subseteq> vars_of_lit L'
[PROOF STEP]
using orient_lit_inst_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L' t' s' pos \<sigma>
orient_lit_inst ?L ?t ?s ?p ?\<sigma> \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of t' \<subseteq> vars_of_lit L'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t' \<subseteq> vars_of_lit L'

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this \<open>coincide_on \<sigma> ?\<theta> (vars_of_lit L')\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of t' \<subseteq> vars_of_lit L'
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit L')
[PROOF STEP]
have "coincide_on \<sigma> ?\<theta> (vars_of t')"
[PROOF STATE]
proof (prove)
using this:
vars_of t' \<subseteq> vars_of_lit L'
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit L')

goal (1 subgoal):
 1. coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of t')
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of t' \<subseteq> vars_of_lit L'
\<forall>x\<in>vars_of_lit L'. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of t'. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of t')

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of t')
[PROOF STEP]
have "subst t' ?\<theta> = subst t' \<sigma>"
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of t')

goal (1 subgoal):
 1. t' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = t' \<lhd> \<sigma>
[PROOF STEP]
using coincide_on_term
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of t')
coincide_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?t \<lhd> ?\<eta>

goal (1 subgoal):
 1. t' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = t' \<lhd> \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
t' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = t' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this \<open>t'_bis = (subst t' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
t' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = t' \<lhd> \<sigma>
t'_bis = t' \<lhd> \<eta>
[PROOF STEP]
have "subst t'_bis ?\<theta>' = subst t' \<sigma>"
[PROOF STATE]
proof (prove)
using this:
t' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = t' \<lhd> \<sigma>
t'_bis = t' \<lhd> \<eta>

goal (1 subgoal):
 1. t'_bis \<lhd> \<eta>' \<lozenge> \<sigma> = t' \<lhd> \<sigma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t'_bis \<lhd> \<eta>' \<lozenge> \<sigma> = t' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from \<open>(orient_lit_inst L' t' s' pos \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L' t' s' pos \<sigma>
[PROOF STEP]
have "vars_of s' \<subseteq> vars_of_lit L'"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L' t' s' pos \<sigma>

goal (1 subgoal):
 1. vars_of s' \<subseteq> vars_of_lit L'
[PROOF STEP]
using orient_lit_inst_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L' t' s' pos \<sigma>
orient_lit_inst ?L ?t ?s ?p ?\<sigma> \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of s' \<subseteq> vars_of_lit L'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of s' \<subseteq> vars_of_lit L'

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this \<open>coincide_on \<sigma> ?\<theta> (vars_of_lit L')\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of s' \<subseteq> vars_of_lit L'
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit L')
[PROOF STEP]
have "coincide_on \<sigma> ?\<theta> (vars_of s')"
[PROOF STATE]
proof (prove)
using this:
vars_of s' \<subseteq> vars_of_lit L'
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit L')

goal (1 subgoal):
 1. coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of s')
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of s' \<subseteq> vars_of_lit L'
\<forall>x\<in>vars_of_lit L'. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of s'. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of s')

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of s')
[PROOF STEP]
have "subst s' ?\<theta> = subst s' \<sigma>"
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of s')

goal (1 subgoal):
 1. s' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = s' \<lhd> \<sigma>
[PROOF STEP]
using coincide_on_term
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of s')
coincide_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?t \<lhd> ?\<eta>

goal (1 subgoal):
 1. s' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = s' \<lhd> \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = s' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this \<open>s'_bis = (subst s' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
s' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = s' \<lhd> \<sigma>
s'_bis = s' \<lhd> \<eta>
[PROOF STEP]
have "subst s'_bis ?\<theta>' = subst s' \<sigma>"
[PROOF STATE]
proof (prove)
using this:
s' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = s' \<lhd> \<sigma>
s'_bis = s' \<lhd> \<eta>

goal (1 subgoal):
 1. s'_bis \<lhd> \<eta>' \<lozenge> \<sigma> = s' \<lhd> \<sigma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s'_bis \<lhd> \<eta>' \<lozenge> \<sigma> = s' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
have "(orient_lit_inst L'_bis t'_bis s'_bis pos ?\<theta>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
from \<open>(orient_lit_inst L' t' s' pos \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L' t' s' pos \<sigma>
[PROOF STEP]
have "((subst t' \<sigma>),(subst s' \<sigma>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L' t' s' pos \<sigma>

goal (1 subgoal):
 1. (t' \<lhd> \<sigma>, s' \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
using orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L' t' s' pos \<sigma>
orient_lit_inst ?L ?u ?v ?s ?\<sigma> = ((?L = Pos (Eq ?u ?v) \<or> ?L = Pos (Eq ?v ?u)) \<and> (?u \<lhd> ?\<sigma>, ?v \<lhd> ?\<sigma>) \<notin> trm_ord \<and> ?s = pos \<or> (?L = Neg (Eq ?u ?v) \<or> ?L = Neg (Eq ?v ?u)) \<and> (?u \<lhd> ?\<sigma>, ?v \<lhd> ?\<sigma>) \<notin> trm_ord \<and> ?s = neg)

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

goal (1 subgoal):
 1. orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
from \<open>(orient_lit_inst L' t' s' pos \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L' t' s' pos \<sigma>
[PROOF STEP]
have "L' = (Pos (Eq t' s')) \<or> L' = (Pos (Eq s' t'))"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L' t' s' pos \<sigma>

goal (1 subgoal):
 1. L' = Pos (Eq t' s') \<or> L' = Pos (Eq s' t')
[PROOF STEP]
by (simp add: orient_lit_inst_def)
[PROOF STATE]
proof (state)
this:
L' = Pos (Eq t' s') \<or> L' = Pos (Eq s' t')

goal (1 subgoal):
 1. orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
from this
      \<open>L'_bis = (subst_lit L' \<eta>)\<close>
      \<open>t'_bis = (subst t' \<eta>)\<close>
      \<open>s'_bis = (subst s' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
L' = Pos (Eq t' s') \<or> L' = Pos (Eq s' t')
L'_bis = subst_lit L' \<eta>
t'_bis = t' \<lhd> \<eta>
s'_bis = s' \<lhd> \<eta>
[PROOF STEP]
have "L'_bis = (Pos (Eq t'_bis s'_bis)) \<or> L'_bis = (Pos (Eq s'_bis t'_bis))"
[PROOF STATE]
proof (prove)
using this:
L' = Pos (Eq t' s') \<or> L' = Pos (Eq s' t')
L'_bis = subst_lit L' \<eta>
t'_bis = t' \<lhd> \<eta>
s'_bis = s' \<lhd> \<eta>

goal (1 subgoal):
 1. L'_bis = Pos (Eq t'_bis s'_bis) \<or> L'_bis = Pos (Eq s'_bis t'_bis)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L'_bis = Pos (Eq t'_bis s'_bis) \<or> L'_bis = Pos (Eq s'_bis t'_bis)

goal (1 subgoal):
 1. orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
from \<open>subst s'_bis ?\<theta>' = subst s' \<sigma>\<close>
      and \<open>subst t'_bis ?\<theta>' = subst t' \<sigma>\<close>
      and \<open>((subst t' \<sigma>),(subst s' \<sigma>)) \<notin> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
s'_bis \<lhd> \<eta>' \<lozenge> \<sigma> = s' \<lhd> \<sigma>
t'_bis \<lhd> \<eta>' \<lozenge> \<sigma> = t' \<lhd> \<sigma>
(t' \<lhd> \<sigma>, s' \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
have "((subst t'_bis ?\<theta>'),(subst s'_bis ?\<theta>')) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
s'_bis \<lhd> \<eta>' \<lozenge> \<sigma> = s' \<lhd> \<sigma>
t'_bis \<lhd> \<eta>' \<lozenge> \<sigma> = t' \<lhd> \<sigma>
(t' \<lhd> \<sigma>, s' \<lhd> \<sigma>) \<notin> trm_ord

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

goal (1 subgoal):
 1. orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
from this and \<open>L'_bis = (Pos (Eq t'_bis s'_bis)) \<or> L'_bis = (Pos (Eq s'_bis t'_bis))\<close>
[PROOF STATE]
proof (chain)
picking this:
(t'_bis \<lhd> \<eta>' \<lozenge> \<sigma>, s'_bis \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord
L'_bis = Pos (Eq t'_bis s'_bis) \<or> L'_bis = Pos (Eq s'_bis t'_bis)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(t'_bis \<lhd> \<eta>' \<lozenge> \<sigma>, s'_bis \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord
L'_bis = Pos (Eq t'_bis s'_bis) \<or> L'_bis = Pos (Eq s'_bis t'_bis)

goal (1 subgoal):
 1. orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
(t'_bis \<lhd> \<eta>' \<lozenge> \<sigma>, s'_bis \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord
L'_bis = Pos (Eq t'_bis s'_bis) \<or> L'_bis = Pos (Eq s'_bis t'_bis)

goal (1 subgoal):
 1. (L'_bis = Pos (Eq t'_bis s'_bis) \<or> L'_bis = Pos (Eq s'_bis t'_bis)) \<and> (t'_bis \<lhd> \<eta>' \<lozenge> \<sigma>, s'_bis \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord \<and> pos = pos \<or> (L'_bis = Neg (Eq t'_bis s'_bis) \<or> L'_bis = Neg (Eq s'_bis t'_bis)) \<and> (t'_bis \<lhd> \<eta>' \<lozenge> \<sigma>, s'_bis \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord \<and> pos = neg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
have "(maximal_literal_is_unique t s C'_bis L'_bis S ?\<theta>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>(maximal_literal_is_unique t s C'_bis L'_bis S ?\<theta>')"
[PROOF STATE]
proof (state)
this:
\<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
obtain s'' where "(eq_occurs_in_cl t s'' (C'_bis- { L'_bis }) ?\<theta>')"
                "(s'',t) \<in> trm_ord"
                "(s,t) \<in> trm_ord"
                "(trm_rep s S) = (trm_rep s'' S)"
[PROOF STATE]
proof (prove)
using this:
\<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. (\<And>s''. \<lbrakk>eq_occurs_in_cl t s'' (C'_bis - {L'_bis}) (\<eta>' \<lozenge> \<sigma>); (s'', t) \<in> trm_ord; (s, t) \<in> trm_ord; trm_rep s S = trm_rep s'' S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding  maximal_literal_is_unique_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>s''. eq_occurs_in_cl t s'' (C'_bis - {L'_bis}) (\<eta>' \<lozenge> \<sigma>) \<longrightarrow> (s'', t) \<in> trm_ord \<longrightarrow> (s, t) \<in> trm_ord \<longrightarrow> trm_rep s S \<noteq> trm_rep s'' S)

goal (1 subgoal):
 1. (\<And>s''. \<lbrakk>eq_occurs_in_cl t s'' (C'_bis - {L'_bis}) (\<eta>' \<lozenge> \<sigma>); (s'', t) \<in> trm_ord; (s, t) \<in> trm_ord; trm_rep s S = trm_rep s'' S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
eq_occurs_in_cl t s'' (C'_bis - {L'_bis}) (\<eta>' \<lozenge> \<sigma>)
(s'', t) \<in> trm_ord
(s, t) \<in> trm_ord
trm_rep s S = trm_rep s'' S

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>(eq_occurs_in_cl t s'' (C'_bis- { L'_bis }) ?\<theta>')\<close>
[PROOF STATE]
proof (chain)
picking this:
eq_occurs_in_cl t s'' (C'_bis - {L'_bis}) (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
obtain M u v where
      "M \<in> C'_bis - { L'_bis }" "orient_lit_inst M u v pos ?\<theta>'"
      "t = (subst u ?\<theta>')" "s'' = (subst v ?\<theta>')"
[PROOF STATE]
proof (prove)
using this:
eq_occurs_in_cl t s'' (C'_bis - {L'_bis}) (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. (\<And>M u v. \<lbrakk>M \<in> C'_bis - {L'_bis}; orient_lit_inst M u v pos (\<eta>' \<lozenge> \<sigma>); t = u \<lhd> \<eta>' \<lozenge> \<sigma>; s'' = v \<lhd> \<eta>' \<lozenge> \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding eq_occurs_in_cl_def
[PROOF STATE]
proof (prove)
using this:
\<exists>L t' s'. L \<in> C'_bis - {L'_bis} \<and> orient_lit_inst L t' s' pos (\<eta>' \<lozenge> \<sigma>) \<and> t = t' \<lhd> \<eta>' \<lozenge> \<sigma> \<and> s'' = s' \<lhd> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. (\<And>M u v. \<lbrakk>M \<in> C'_bis - {L'_bis}; orient_lit_inst M u v pos (\<eta>' \<lozenge> \<sigma>); t = u \<lhd> \<eta>' \<lozenge> \<sigma>; s'' = v \<lhd> \<eta>' \<lozenge> \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
M \<in> C'_bis - {L'_bis}
orient_lit_inst M u v pos (\<eta>' \<lozenge> \<sigma>)
t = u \<lhd> \<eta>' \<lozenge> \<sigma>
s'' = v \<lhd> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>M \<in> C'_bis - { L'_bis }\<close>
      and \<open>C'_bis = (subst_cl C' \<eta>)\<close> and \<open>L'_bis = (subst_lit L' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
M \<in> C'_bis - {L'_bis}
C'_bis = subst_cl C' \<eta>
L'_bis = subst_lit L' \<eta>
[PROOF STEP]
obtain M' where "M' \<in> C'- { L' }" and "subst_lit M' \<eta> =  M"
[PROOF STATE]
proof (prove)
using this:
M \<in> C'_bis - {L'_bis}
C'_bis = subst_cl C' \<eta>
L'_bis = subst_lit L' \<eta>

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

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit_inst M u v pos ?\<theta>'\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst M u v pos (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
obtain e where "M = (Pos e)"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst M u v pos (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. (\<And>e. M = Pos e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
(M = Pos (Eq u v) \<or> M = Pos (Eq v u)) \<and> (u \<lhd> \<eta>' \<lozenge> \<sigma>, v \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord \<and> pos = pos \<or> (M = Neg (Eq u v) \<or> M = Neg (Eq v u)) \<and> (u \<lhd> \<eta>' \<lozenge> \<sigma>, v \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord \<and> pos = neg

goal (1 subgoal):
 1. (\<And>e. M = Pos e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M = Pos e

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and  \<open>orient_lit_inst M u v pos ?\<theta>'\<close>
[PROOF STATE]
proof (chain)
picking this:
M = Pos e
orient_lit_inst M u v pos (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
have "e = (Eq u v) \<or> e = (Eq v u)"
[PROOF STATE]
proof (prove)
using this:
M = Pos e
orient_lit_inst M u v pos (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. e = Eq u v \<or> e = Eq v u
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
M = Pos e
(M = Pos (Eq u v) \<or> M = Pos (Eq v u)) \<and> (u \<lhd> \<eta>' \<lozenge> \<sigma>, v \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord \<and> pos = pos \<or> (M = Neg (Eq u v) \<or> M = Neg (Eq v u)) \<and> (u \<lhd> \<eta>' \<lozenge> \<sigma>, v \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord \<and> pos = neg

goal (1 subgoal):
 1. e = Eq u v \<or> e = Eq v u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e = Eq u v \<or> e = Eq v u

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit_inst M u v pos ?\<theta>'\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst M u v pos (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
have
      "( (subst u ?\<theta>'),(subst v ?\<theta>')) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst M u v pos (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. (u \<lhd> \<eta>' \<lozenge> \<sigma>, v \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
(M = Pos (Eq u v) \<or> M = Pos (Eq v u)) \<and> (u \<lhd> \<eta>' \<lozenge> \<sigma>, v \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord \<and> pos = pos \<or> (M = Neg (Eq u v) \<or> M = Neg (Eq v u)) \<and> (u \<lhd> \<eta>' \<lozenge> \<sigma>, v \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord \<and> pos = neg

goal (1 subgoal):
 1. (u \<lhd> \<eta>' \<lozenge> \<sigma>, v \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u \<lhd> \<eta>' \<lozenge> \<sigma>, v \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>M = (Pos e)\<close> and \<open>subst_lit M' \<eta> =  M\<close>
[PROOF STATE]
proof (chain)
picking this:
M = Pos e
subst_lit M' \<eta> = M
[PROOF STEP]
obtain e' where "(subst_equation e' \<eta>)  = e" and "M' = (Pos e')"
[PROOF STATE]
proof (prove)
using this:
M = Pos e
subst_lit M' \<eta> = M

goal (1 subgoal):
 1. (\<And>e'. \<lbrakk>subst_equation e' \<eta> = e; M' = Pos e'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types, opaque_lifting) subst_lit.simps(1) subst_lit.simps(2) atom.simps(1)
          literal.distinct(1) positive_literal.elims(1))
[PROOF STATE]
proof (state)
this:
subst_equation e' \<eta> = e
M' = Pos e'

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>e = (Eq u v) \<or> e = (Eq v u)\<close> and \<open>(subst_equation e' \<eta>)  = e\<close>
[PROOF STATE]
proof (chain)
picking this:
e = Eq u v \<or> e = Eq v u
subst_equation e' \<eta> = e
[PROOF STEP]
obtain u' v' where "e' = (Eq u' v') \<or> (e' = (Eq v' u'))" and "(subst u' \<eta>) = u" and
        "(subst v' \<eta>) = v"
[PROOF STATE]
proof (prove)
using this:
e = Eq u v \<or> e = Eq v u
subst_equation e' \<eta> = e

goal (1 subgoal):
 1. (\<And>u' v'. \<lbrakk>e' = Eq u' v' \<or> e' = Eq v' u'; u' \<lhd> \<eta> = u; v' \<lhd> \<eta> = v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis subst_equation.simps equation.inject subterms_of_eq.cases)
[PROOF STATE]
proof (state)
this:
e' = Eq u' v' \<or> e' = Eq v' u'
u' \<lhd> \<eta> = u
v' \<lhd> \<eta> = v

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>( (subst u ?\<theta>'),(subst v ?\<theta>')) \<notin> trm_ord\<close>
      \<open>(subst u' \<eta>) = u\<close>
      \<open>(subst v' \<eta>) = v\<close>
[PROOF STATE]
proof (chain)
picking this:
(u \<lhd> \<eta>' \<lozenge> \<sigma>, v \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord
u' \<lhd> \<eta> = u
v' \<lhd> \<eta> = v
[PROOF STEP]
have "( (subst u' ?\<theta>),(subst v' ?\<theta>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<eta>' \<lozenge> \<sigma>, v \<lhd> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord
u' \<lhd> \<eta> = u
v' \<lhd> \<eta> = v

goal (1 subgoal):
 1. (u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>, v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>, v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>M' = (Pos e')\<close> and \<open>e' = (Eq u' v') \<or> (e' = (Eq v' u'))\<close>
[PROOF STATE]
proof (chain)
picking this:
(u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>, v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord
M' = Pos e'
e' = Eq u' v' \<or> e' = Eq v' u'
[PROOF STEP]
have "orient_lit_inst M' u' v' pos ?\<theta>"
[PROOF STATE]
proof (prove)
using this:
(u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>, v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord
M' = Pos e'
e' = Eq u' v' \<or> e' = Eq v' u'

goal (1 subgoal):
 1. orient_lit_inst M' u' v' pos (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
(u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>, v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord
M' = Pos e'
e' = Eq u' v' \<or> e' = Eq v' u'

goal (1 subgoal):
 1. (M' = Pos (Eq u' v') \<or> M' = Pos (Eq v' u')) \<and> (u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>, v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord \<and> pos = pos \<or> (M' = Neg (Eq u' v') \<or> M' = Neg (Eq v' u')) \<and> (u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>, v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<notin> trm_ord \<and> pos = neg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit_inst M' u' v' pos (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>M' \<in> C' - { L' }\<close>
[PROOF STATE]
proof (chain)
picking this:
M' \<in> C' - {L'}
[PROOF STEP]
have "vars_of_lit M' \<subseteq> vars_of_cl C'"
[PROOF STATE]
proof (prove)
using this:
M' \<in> C' - {L'}

goal (1 subgoal):
 1. vars_of_lit M' \<subseteq> vars_of_cl C'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_lit M' \<subseteq> vars_of_cl C'

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>coincide_on \<sigma> ?\<theta> (vars_of_cl C')\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit M' \<subseteq> vars_of_cl C'
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')
[PROOF STEP]
have "coincide_on \<sigma> ?\<theta> (vars_of_lit M')"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit M' \<subseteq> vars_of_cl C'
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_cl C')

goal (1 subgoal):
 1. coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit M')
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of_lit M' \<subseteq> vars_of_cl C'
\<forall>x\<in>vars_of_cl C'. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of_lit M'. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit M')

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit M')
[PROOF STEP]
have "coincide_on ?\<theta> \<sigma> (vars_of_lit M')"
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit M')

goal (1 subgoal):
 1. coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of_lit M')
[PROOF STEP]
using coincide_sym
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) (vars_of_lit M')
coincide_on ?\<sigma> ?\<eta> ?V \<Longrightarrow> coincide_on ?\<eta> ?\<sigma> ?V

goal (1 subgoal):
 1. coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of_lit M')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of_lit M')

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>orient_lit_inst M' u' v' pos ?\<theta>\<close>
[PROOF STATE]
proof (chain)
picking this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of_lit M')
orient_lit_inst M' u' v' pos (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
have "orient_lit_inst M' u' v' pos \<sigma>"
[PROOF STATE]
proof (prove)
using this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of_lit M')
orient_lit_inst M' u' v' pos (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. orient_lit_inst M' u' v' pos \<sigma>
[PROOF STEP]
using orient_lit_inst_coincide
[PROOF STATE]
proof (prove)
using this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of_lit M')
orient_lit_inst M' u' v' pos (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
\<lbrakk>orient_lit_inst ?L1.0 ?t ?s ?polarity ?\<sigma>; coincide_on ?\<sigma> ?\<eta> (vars_of_lit ?L1.0)\<rbrakk> \<Longrightarrow> orient_lit_inst ?L1.0 ?t ?s ?polarity ?\<eta>

goal (1 subgoal):
 1. orient_lit_inst M' u' v' pos \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit_inst M' u' v' pos \<sigma>

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>orient_lit_inst M' u' v' pos ?\<theta>\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst M' u' v' pos (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
have "vars_of u' \<subseteq> vars_of_lit M'" and
       "vars_of v' \<subseteq> vars_of_lit M'"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst M' u' v' pos (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. vars_of u' \<subseteq> vars_of_lit M' &&& vars_of v' \<subseteq> vars_of_lit M'
[PROOF STEP]
using orient_lit_inst_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst M' u' v' pos (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>)
orient_lit_inst ?L ?t ?s ?p ?\<sigma> \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of u' \<subseteq> vars_of_lit M' &&& vars_of v' \<subseteq> vars_of_lit M'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of u' \<subseteq> vars_of_lit M'
vars_of v' \<subseteq> vars_of_lit M'

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>vars_of u' \<subseteq> vars_of_lit M'\<close> and \<open>coincide_on ?\<theta> \<sigma> (vars_of_lit M')\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of u' \<subseteq> vars_of_lit M'
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of_lit M')
[PROOF STEP]
have "coincide_on ?\<theta> \<sigma> (vars_of u')"
[PROOF STATE]
proof (prove)
using this:
vars_of u' \<subseteq> vars_of_lit M'
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of_lit M')

goal (1 subgoal):
 1. coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of u')
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of u' \<subseteq> vars_of_lit M'
\<forall>x\<in>vars_of_lit M'. Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = Var x \<lhd> \<sigma>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of u'. Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = Var x \<lhd> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of u')

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of u')
[PROOF STEP]
have "subst u' ?\<theta> = subst u' \<sigma>"
[PROOF STATE]
proof (prove)
using this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of u')

goal (1 subgoal):
 1. u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = u' \<lhd> \<sigma>
[PROOF STEP]
using coincide_on_term
[PROOF STATE]
proof (prove)
using this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of u')
coincide_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?t \<lhd> ?\<eta>

goal (1 subgoal):
 1. u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = u' \<lhd> \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = u' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst u' \<eta>) = u\<close>
[PROOF STATE]
proof (chain)
picking this:
u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = u' \<lhd> \<sigma>
u' \<lhd> \<eta> = u
[PROOF STEP]
have "subst u ?\<theta>' = subst u' \<sigma>"
[PROOF STATE]
proof (prove)
using this:
u' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = u' \<lhd> \<sigma>
u' \<lhd> \<eta> = u

goal (1 subgoal):
 1. u \<lhd> \<eta>' \<lozenge> \<sigma> = u' \<lhd> \<sigma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u \<lhd> \<eta>' \<lozenge> \<sigma> = u' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>vars_of v' \<subseteq> vars_of_lit M'\<close> and \<open>coincide_on ?\<theta> \<sigma> (vars_of_lit M')\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of v' \<subseteq> vars_of_lit M'
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of_lit M')
[PROOF STEP]
have "coincide_on ?\<theta> \<sigma> (vars_of v')"
[PROOF STATE]
proof (prove)
using this:
vars_of v' \<subseteq> vars_of_lit M'
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of_lit M')

goal (1 subgoal):
 1. coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of v')
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of v' \<subseteq> vars_of_lit M'
\<forall>x\<in>vars_of_lit M'. Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = Var x \<lhd> \<sigma>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of v'. Var x \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = Var x \<lhd> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of v')

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of v')
[PROOF STEP]
have "subst v' ?\<theta> = subst v' \<sigma>"
[PROOF STATE]
proof (prove)
using this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of v')

goal (1 subgoal):
 1. v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = v' \<lhd> \<sigma>
[PROOF STEP]
using coincide_on_term
[PROOF STATE]
proof (prove)
using this:
coincide_on (\<eta> \<lozenge> \<eta>' \<lozenge> \<sigma>) \<sigma> (vars_of v')
coincide_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?t \<lhd> ?\<eta>

goal (1 subgoal):
 1. v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = v' \<lhd> \<sigma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = v' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst v' \<eta>) = v\<close>
[PROOF STATE]
proof (chain)
picking this:
v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = v' \<lhd> \<sigma>
v' \<lhd> \<eta> = v
[PROOF STEP]
have "subst v ?\<theta>' = subst v' \<sigma>"
[PROOF STATE]
proof (prove)
using this:
v' \<lhd> \<eta> \<lozenge> \<eta>' \<lozenge> \<sigma> = v' \<lhd> \<sigma>
v' \<lhd> \<eta> = v

goal (1 subgoal):
 1. v \<lhd> \<eta>' \<lozenge> \<sigma> = v' \<lhd> \<sigma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<lhd> \<eta>' \<lozenge> \<sigma> = v' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>subst v ?\<theta>' = subst v' \<sigma>\<close> \<open>s'' = (subst v ?\<theta>')\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<lhd> \<eta>' \<lozenge> \<sigma> = v' \<lhd> \<sigma>
s'' = v \<lhd> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
have "s'' = (subst v' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
v \<lhd> \<eta>' \<lozenge> \<sigma> = v' \<lhd> \<sigma>
s'' = v \<lhd> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. s'' = v' \<lhd> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s'' = v' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>subst u ?\<theta>' = subst u' \<sigma>\<close> \<open>t = (subst u ?\<theta>')\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<lhd> \<eta>' \<lozenge> \<sigma> = u' \<lhd> \<sigma>
t = u \<lhd> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
have "t = (subst u' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
u \<lhd> \<eta>' \<lozenge> \<sigma> = u' \<lhd> \<sigma>
t = u \<lhd> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. t = u' \<lhd> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = u' \<lhd> \<sigma>

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>s'' = (subst v' \<sigma>)\<close> \<open>t = (subst u' \<sigma>)\<close>
      \<open>orient_lit_inst M' u' v' pos \<sigma>\<close> \<open>M' \<in> C' - { L'}\<close>
[PROOF STATE]
proof (chain)
picking this:
s'' = v' \<lhd> \<sigma>
t = u' \<lhd> \<sigma>
orient_lit_inst M' u' v' pos \<sigma>
M' \<in> C' - {L'}
[PROOF STEP]
have "eq_occurs_in_cl t s'' (C'- { L' }) \<sigma>"
[PROOF STATE]
proof (prove)
using this:
s'' = v' \<lhd> \<sigma>
t = u' \<lhd> \<sigma>
orient_lit_inst M' u' v' pos \<sigma>
M' \<in> C' - {L'}

goal (1 subgoal):
 1. eq_occurs_in_cl t s'' (C' - {L'}) \<sigma>
[PROOF STEP]
unfolding eq_occurs_in_cl_def
[PROOF STATE]
proof (prove)
using this:
s'' = v' \<lhd> \<sigma>
t = u' \<lhd> \<sigma>
orient_lit_inst M' u' v' pos \<sigma>
M' \<in> C' - {L'}

goal (1 subgoal):
 1. \<exists>L t' s'. L \<in> C' - {L'} \<and> orient_lit_inst L t' s' pos \<sigma> \<and> t = t' \<lhd> \<sigma> \<and> s'' = s' \<lhd> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eq_occurs_in_cl t s'' (C' - {L'}) \<sigma>

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(s'',t) \<in> trm_ord\<close> and \<open>(s,t) \<in> trm_ord\<close> and \<open>(trm_rep s S) = (trm_rep s'' S)\<close>
[PROOF STATE]
proof (chain)
picking this:
eq_occurs_in_cl t s'' (C' - {L'}) \<sigma>
(s'', t) \<in> trm_ord
(s, t) \<in> trm_ord
trm_rep s S = trm_rep s'' S
[PROOF STEP]
have "\<not>(maximal_literal_is_unique t s C' L' S \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
eq_occurs_in_cl t s'' (C' - {L'}) \<sigma>
(s'', t) \<in> trm_ord
(s, t) \<in> trm_ord
trm_rep s S = trm_rep s'' S

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C' L' S \<sigma>
[PROOF STEP]
unfolding maximal_literal_is_unique_def
[PROOF STATE]
proof (prove)
using this:
eq_occurs_in_cl t s'' (C' - {L'}) \<sigma>
(s'', t) \<in> trm_ord
(s, t) \<in> trm_ord
trm_rep s S = trm_rep s'' S

goal (1 subgoal):
 1. \<not> (\<forall>s''. eq_occurs_in_cl t s'' (C' - {L'}) \<sigma> \<longrightarrow> (s'', t) \<in> trm_ord \<longrightarrow> (s, t) \<in> trm_ord \<longrightarrow> trm_rep s S \<noteq> trm_rep s'' S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<not> maximal_literal_is_unique t s C' L' S \<sigma>
candidate_values z CC C' C s L L' \<sigma> t' s' t S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> maximal_literal_is_unique t s C' L' S \<sigma>
candidate_values z CC C' C s L L' \<sigma> t' s' t S

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
\<not> maximal_literal_is_unique t s C' L' S \<sigma>
CC \<in> S \<and> t \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S t \<and> C' = cl_ecl CC \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> t = t' \<lhd> \<sigma> \<and> s = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C' L' S \<sigma>

goal (1 subgoal):
 1. False
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from \<open>t'_bis = (subst t' \<eta>)\<close>
    and \<open>t = subst t' \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
t'_bis = t' \<lhd> \<eta>
t = t' \<lhd> \<sigma>
[PROOF STEP]
have "t = subst t'_bis (comp \<eta>' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
t'_bis = t' \<lhd> \<eta>
t = t' \<lhd> \<sigma>

goal (1 subgoal):
 1. t = t'_bis \<lhd> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
using \<open>subst t'_bis (comp \<eta>' \<sigma>) = subst t' \<sigma>\<close>
[PROOF STATE]
proof (prove)
using this:
t'_bis = t' \<lhd> \<eta>
t = t' \<lhd> \<sigma>
t'_bis \<lhd> \<eta>' \<lozenge> \<sigma> = t' \<lhd> \<sigma>

goal (1 subgoal):
 1. t = t'_bis \<lhd> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = t'_bis \<lhd> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from \<open>s'_bis = (subst s' \<eta>)\<close>
    and \<open>s = subst s' \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
s'_bis = s' \<lhd> \<eta>
s = s' \<lhd> \<sigma>
[PROOF STEP]
have "s = subst s'_bis (comp \<eta>' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
s'_bis = s' \<lhd> \<eta>
s = s' \<lhd> \<sigma>

goal (1 subgoal):
 1. s = s'_bis \<lhd> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
using \<open>subst s'_bis (comp \<eta>' \<sigma>) = subst s' \<sigma>\<close>
[PROOF STATE]
proof (prove)
using this:
s'_bis = s' \<lhd> \<eta>
s = s' \<lhd> \<sigma>
s'_bis \<lhd> \<eta>' \<lozenge> \<sigma> = s' \<lhd> \<sigma>

goal (1 subgoal):
 1. s = s'_bis \<lhd> \<eta>' \<lozenge> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = s'_bis \<lhd> \<eta>' \<lozenge> \<sigma>

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from \<open>CC_bis \<in> S\<close> \<open>t \<notin> subst_set (trms_ecl CC_bis) (comp \<eta>' \<sigma>)\<close>
    \<open>trms_irreducible CC_bis (comp \<eta>' \<sigma>) S t\<close>
    \<open>C'_bis = cl_ecl CC_bis\<close> \<open>(s, t) \<in> trm_ord\<close> \<open>((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S)\<close>
    \<open>orient_lit_inst L'_bis t'_bis s'_bis pos (comp \<eta>' \<sigma>)\<close>
    \<open>sel C'_bis = {}\<close> \<open>L'_bis \<in> C'_bis\<close> \<open>maximal_literal L C\<close>
    \<open>L = subst_lit L'_bis (comp \<eta>' \<sigma>)\<close>
    \<open>C = subst_cl C'_bis (comp \<eta>' \<sigma>)\<close>
    \<open>ground_clause C\<close> \<open>t = subst t'_bis (comp \<eta>' \<sigma>)\<close>
    \<open>s = subst s'_bis (comp \<eta>' \<sigma>)\<close>
    \<open>finite C'_bis\<close> \<open>smaller_lits_are_false t C S\<close>
    \<open>maximal_literal_is_unique t s C'_bis L'_bis S (comp \<eta>' \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
CC_bis \<in> S
t \<notin> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>)
trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t
C'_bis = cl_ecl CC_bis
(s, t) \<in> trm_ord
(s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S
orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)
sel C'_bis = {}
L'_bis \<in> C'_bis
maximal_literal L C
L = subst_lit L'_bis (\<eta>' \<lozenge> \<sigma>)
C = subst_cl C'_bis (\<eta>' \<lozenge> \<sigma>)
ground_clause C
t = t'_bis \<lhd> \<eta>' \<lozenge> \<sigma>
s = s'_bis \<lhd> \<eta>' \<lozenge> \<sigma>
finite C'_bis
smaller_lits_are_false t C S
maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
have "(candidate_values z CC_bis C'_bis C s L L'_bis ?\<theta>' t'_bis s'_bis t S)"
[PROOF STATE]
proof (prove)
using this:
CC_bis \<in> S
t \<notin> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>)
trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t
C'_bis = cl_ecl CC_bis
(s, t) \<in> trm_ord
(s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S
orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)
sel C'_bis = {}
L'_bis \<in> C'_bis
maximal_literal L C
L = subst_lit L'_bis (\<eta>' \<lozenge> \<sigma>)
C = subst_cl C'_bis (\<eta>' \<lozenge> \<sigma>)
ground_clause C
t = t'_bis \<lhd> \<eta>' \<lozenge> \<sigma>
s = s'_bis \<lhd> \<eta>' \<lozenge> \<sigma>
finite C'_bis
smaller_lits_are_false t C S
maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. candidate_values z CC_bis C'_bis C s L L'_bis (\<eta>' \<lozenge> \<sigma>) t'_bis s'_bis t S
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
CC_bis \<in> S
t \<notin> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>)
trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t
C'_bis = cl_ecl CC_bis
(s, t) \<in> trm_ord
(s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S
orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>)
sel C'_bis = {}
L'_bis \<in> C'_bis
maximal_literal L C
L = subst_lit L'_bis (\<eta>' \<lozenge> \<sigma>)
C = subst_cl C'_bis (\<eta>' \<lozenge> \<sigma>)
ground_clause C
t = t'_bis \<lhd> \<eta>' \<lozenge> \<sigma>
s = s'_bis \<lhd> \<eta>' \<lozenge> \<sigma>
finite C'_bis
smaller_lits_are_false t C S
maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>)

goal (1 subgoal):
 1. CC_bis \<in> S \<and> t \<notin> subst_set (trms_ecl CC_bis) (\<eta>' \<lozenge> \<sigma>) \<and> trms_irreducible CC_bis (\<eta>' \<lozenge> \<sigma>) S t \<and> C'_bis = cl_ecl CC_bis \<and> (s, t) \<in> trm_ord \<and> ((s, t) \<in> trm_ord \<longrightarrow> z = trm_rep s S) \<and> orient_lit_inst L'_bis t'_bis s'_bis pos (\<eta>' \<lozenge> \<sigma>) \<and> sel C'_bis = {} \<and> L'_bis \<in> C'_bis \<and> maximal_literal L C \<and> L = subst_lit L'_bis (\<eta>' \<lozenge> \<sigma>) \<and> C = subst_cl C'_bis (\<eta>' \<lozenge> \<sigma>) \<and> ground_clause C \<and> t = t'_bis \<lhd> \<eta>' \<lozenge> \<sigma> \<and> s = s'_bis \<lhd> \<eta>' \<lozenge> \<sigma> \<and> finite C'_bis \<and> smaller_lits_are_false t C S \<and> maximal_literal_is_unique t s C'_bis L'_bis S (\<eta>' \<lozenge> \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
candidate_values z CC_bis C'_bis C s L L'_bis (\<eta>' \<lozenge> \<sigma>) t'_bis s'_bis t S

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
have "vars_of_cl (cl_ecl D) \<inter> (vars_of_cl (cl_ecl CC_bis)) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "vars_of_cl (cl_ecl D) \<inter> (vars_of_cl (cl_ecl CC_bis)) \<noteq> {}"
[PROOF STATE]
proof (state)
this:
vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {}

goal (1 subgoal):
 1. vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from this and \<open>C'_bis = (cl_ecl CC_bis)\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {}
C'_bis = cl_ecl CC_bis
[PROOF STEP]
obtain x where "x \<in> vars_of_cl C'_bis" and "x \<in> vars_of_cl (cl_ecl D)"
[PROOF STATE]
proof (prove)
using this:
vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {}
C'_bis = cl_ecl CC_bis

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> vars_of_cl C'_bis; x \<in> vars_of_cl (cl_ecl D)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vars_of_cl C'_bis
x \<in> vars_of_cl (cl_ecl D)

goal (1 subgoal):
 1. vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<in> vars_of_cl C'_bis\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of_cl C'_bis
[PROOF STEP]
obtain N where "N \<in> C'_bis" and "x \<in> vars_of_lit N"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of_cl C'_bis

goal (1 subgoal):
 1. (\<And>N. \<lbrakk>N \<in> C'_bis; x \<in> vars_of_lit N\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
N \<in> C'_bis
x \<in> vars_of_lit N

goal (1 subgoal):
 1. vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from \<open>N \<in> C'_bis\<close> and \<open>C'_bis = (subst_cl C' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
N \<in> C'_bis
C'_bis = subst_cl C' \<eta>
[PROOF STEP]
obtain N' where
        "N' \<in> C'" and "N = subst_lit N' \<eta>"
[PROOF STATE]
proof (prove)
using this:
N \<in> C'_bis
C'_bis = subst_cl C' \<eta>

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

goal (1 subgoal):
 1. vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<in> vars_of_lit N\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of_lit N
[PROOF STEP]
obtain e where "N = (Pos e) \<or> (N = (Neg e))"
        and "x \<in> vars_of_eq e"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of_lit N

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>N = Pos e \<or> N = Neg e; x \<in> vars_of_eq e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis negative_literal.elims(2) negative_literal.elims(3) vars_of_lit.simps(1)
            vars_of_lit.simps(2))
[PROOF STATE]
proof (state)
this:
N = Pos e \<or> N = Neg e
x \<in> vars_of_eq e

goal (1 subgoal):
 1. vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from \<open>N = (Pos e) \<or> (N = (Neg e))\<close> and \<open>N = subst_lit N' \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
N = Pos e \<or> N = Neg e
N = subst_lit N' \<eta>
[PROOF STEP]
obtain e' where
        "N' = (Pos e') \<or> (N' = (Neg e'))" and "e = subst_equation e' \<eta>"
[PROOF STATE]
proof (prove)
using this:
N = Pos e \<or> N = Neg e
N = subst_lit N' \<eta>

goal (1 subgoal):
 1. (\<And>e'. \<lbrakk>N' = Pos e' \<or> N' = Neg e'; e = subst_equation e' \<eta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis subst_lit.elims atom.simps(1) atom.simps(2))
[PROOF STATE]
proof (state)
this:
N' = Pos e' \<or> N' = Neg e'
e = subst_equation e' \<eta>

goal (1 subgoal):
 1. vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<in> vars_of_eq e\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of_eq e
[PROOF STEP]
obtain u v where "e = (Eq u v)" and "x \<in> vars_of u \<union> vars_of v"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of_eq e

goal (1 subgoal):
 1. (\<And>u v. \<lbrakk>e = Eq u v; x \<in> vars_of u \<union> vars_of v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis equation.exhaust vars_of_eq.simps)
[PROOF STATE]
proof (state)
this:
e = Eq u v
x \<in> vars_of u \<union> vars_of v

goal (1 subgoal):
 1. vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from \<open>e = (Eq u v)\<close> and \<open>e = subst_equation e' \<eta>\<close>
[PROOF STATE]
proof (chain)
picking this:
e = Eq u v
e = subst_equation e' \<eta>
[PROOF STEP]
obtain u' v' where "e' = (Eq u' v')"
        "u = (subst u' \<eta>)" and "v = (subst v' \<eta>)"
[PROOF STATE]
proof (prove)
using this:
e = Eq u v
e = subst_equation e' \<eta>

goal (1 subgoal):
 1. (\<And>u' v'. \<lbrakk>e' = Eq u' v'; u = u' \<lhd> \<eta>; v = v' \<lhd> \<eta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis subst_equation.simps equation.exhaust equation.inject)
[PROOF STATE]
proof (state)
this:
e' = Eq u' v'
u = u' \<lhd> \<eta>
v = v' \<lhd> \<eta>

goal (1 subgoal):
 1. vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<in> vars_of u \<union> vars_of v\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of u \<union> vars_of v
[PROOF STEP]
have "x \<in> vars_of u \<or> x \<in> vars_of v"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of u \<union> vars_of v

goal (1 subgoal):
 1. x \<in> vars_of u \<or> x \<in> vars_of v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vars_of u \<or> x \<in> vars_of v

goal (1 subgoal):
 1. vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of u \<or> x \<in> vars_of v
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of u \<or> x \<in> vars_of v

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> vars_of u \<Longrightarrow> False
 2. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
assume "x \<in> vars_of u"
[PROOF STATE]
proof (state)
this:
x \<in> vars_of u

goal (2 subgoals):
 1. x \<in> vars_of u \<Longrightarrow> False
 2. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>u = (subst u' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of u
u = u' \<lhd> \<eta>
[PROOF STEP]
obtain y where "y \<in> vars_of u'" and "x \<in> vars_of (subst (Var y) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of u
u = u' \<lhd> \<eta>

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> vars_of u'; x \<in> vars_of (Var y \<lhd> \<eta>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vars_of_instances [of u' \<eta>]
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of u
u = u' \<lhd> \<eta>
vars_of (u' \<lhd> \<eta>) = \<Union> {V. \<exists>x. x \<in> vars_of u' \<and> V = vars_of (Var x \<lhd> \<eta>)}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> vars_of u'; x \<in> vars_of (Var y \<lhd> \<eta>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> vars_of u'
x \<in> vars_of (Var y \<lhd> \<eta>)

goal (2 subgoals):
 1. x \<in> vars_of u \<Longrightarrow> False
 2. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from \<open>y \<in> vars_of u'\<close> and \<open>e' = (Eq u' v')\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> vars_of u'
e' = Eq u' v'
[PROOF STEP]
have "y \<in> vars_of_eq e'"
[PROOF STATE]
proof (prove)
using this:
y \<in> vars_of u'
e' = Eq u' v'

goal (1 subgoal):
 1. y \<in> vars_of_eq e'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> vars_of_eq e'

goal (2 subgoals):
 1. x \<in> vars_of u \<Longrightarrow> False
 2. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>N' = (Pos e') \<or> (N' = (Neg e'))\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> vars_of_eq e'
N' = Pos e' \<or> N' = Neg e'
[PROOF STEP]
have "y \<in> vars_of_lit N'"
[PROOF STATE]
proof (prove)
using this:
y \<in> vars_of_eq e'
N' = Pos e' \<or> N' = Neg e'

goal (1 subgoal):
 1. y \<in> vars_of_lit N'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> vars_of_lit N'

goal (2 subgoals):
 1. x \<in> vars_of u \<Longrightarrow> False
 2. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>N' \<in> C'\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> vars_of_lit N'
N' \<in> C'
[PROOF STEP]
have "y \<in> vars_of_cl C'"
[PROOF STATE]
proof (prove)
using this:
y \<in> vars_of_lit N'
N' \<in> C'

goal (1 subgoal):
 1. y \<in> vars_of_cl C'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> vars_of_cl C'

goal (2 subgoals):
 1. x \<in> vars_of u \<Longrightarrow> False
 2. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>renaming \<eta> (vars_of_cl C')\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> vars_of_cl C'
renaming \<eta> (vars_of_cl C')
[PROOF STEP]
have "is_a_variable (subst (Var y) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
y \<in> vars_of_cl C'
renaming \<eta> (vars_of_cl C')

goal (1 subgoal):
 1. is_a_variable (Var y \<lhd> \<eta>)
[PROOF STEP]
unfolding renaming_def
[PROOF STATE]
proof (prove)
using this:
y \<in> vars_of_cl C'
\<forall>x\<in>vars_of_cl C'. is_a_variable (Var x \<lhd> \<eta>) \<and> (\<forall>x y. x \<in> vars_of_cl C' \<longrightarrow> y \<in> vars_of_cl C' \<longrightarrow> x \<noteq> y \<longrightarrow> Var x \<lhd> \<eta> \<noteq> Var y \<lhd> \<eta>)

goal (1 subgoal):
 1. is_a_variable (Var y \<lhd> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_a_variable (Var y \<lhd> \<eta>)

goal (2 subgoals):
 1. x \<in> vars_of u \<Longrightarrow> False
 2. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>x \<in> vars_of (subst (Var y) \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
is_a_variable (Var y \<lhd> \<eta>)
x \<in> vars_of (Var y \<lhd> \<eta>)
[PROOF STEP]
have
          "Var x = (subst (Var y) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
is_a_variable (Var y \<lhd> \<eta>)
x \<in> vars_of (Var y \<lhd> \<eta>)

goal (1 subgoal):
 1. Var x = Var y \<lhd> \<eta>
[PROOF STEP]
by (metis is_a_variable.elims(2) singletonD vars_of.simps(1))
[PROOF STATE]
proof (state)
this:
Var x = Var y \<lhd> \<eta>

goal (2 subgoals):
 1. x \<in> vars_of u \<Longrightarrow> False
 2. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>y \<in> vars_of_cl C'\<close>
[PROOF STATE]
proof (chain)
picking this:
Var x = Var y \<lhd> \<eta>
y \<in> vars_of_cl C'
[PROOF STEP]
have "x \<in> (subst_codomain \<eta> (vars_of_cl C'))"
[PROOF STATE]
proof (prove)
using this:
Var x = Var y \<lhd> \<eta>
y \<in> vars_of_cl C'

goal (1 subgoal):
 1. x \<in> subst_codomain \<eta> (vars_of_cl C')
[PROOF STEP]
unfolding subst_codomain_def
[PROOF STATE]
proof (prove)
using this:
Var x = Var y \<lhd> \<eta>
y \<in> vars_of_cl C'

goal (1 subgoal):
 1. x \<in> {x. \<exists>y. Var y \<lhd> \<eta> = Var x \<and> y \<in> vars_of_cl C'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> subst_codomain \<eta> (vars_of_cl C')

goal (2 subgoals):
 1. x \<in> vars_of u \<Longrightarrow> False
 2. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>x \<in> vars_of_cl (cl_ecl D)\<close>
          and \<open>((subst_codomain \<eta> (vars_of_cl C')) \<inter> (vars_of_cl (cl_ecl D))) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> subst_codomain \<eta> (vars_of_cl C')
x \<in> vars_of_cl (cl_ecl D)
subst_codomain \<eta> (vars_of_cl C') \<inter> vars_of_cl (cl_ecl D) = {}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x \<in> subst_codomain \<eta> (vars_of_cl C')
x \<in> vars_of_cl (cl_ecl D)
subst_codomain \<eta> (vars_of_cl C') \<inter> vars_of_cl (cl_ecl D) = {}

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

goal (1 subgoal):
 1. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
assume "x \<in> vars_of v"
[PROOF STATE]
proof (state)
this:
x \<in> vars_of v

goal (1 subgoal):
 1. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>v = (subst v' \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars_of v
v = v' \<lhd> \<eta>
[PROOF STEP]
obtain y where "y \<in> vars_of v'" and "x \<in> vars_of (subst (Var y) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of v
v = v' \<lhd> \<eta>

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> vars_of v'; x \<in> vars_of (Var y \<lhd> \<eta>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vars_of_instances [of v' \<eta>]
[PROOF STATE]
proof (prove)
using this:
x \<in> vars_of v
v = v' \<lhd> \<eta>
vars_of (v' \<lhd> \<eta>) = \<Union> {V. \<exists>x. x \<in> vars_of v' \<and> V = vars_of (Var x \<lhd> \<eta>)}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> vars_of v'; x \<in> vars_of (Var y \<lhd> \<eta>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> vars_of v'
x \<in> vars_of (Var y \<lhd> \<eta>)

goal (1 subgoal):
 1. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from \<open>y \<in> vars_of v'\<close> and \<open>e' = (Eq u' v')\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> vars_of v'
e' = Eq u' v'
[PROOF STEP]
have "y \<in> vars_of_eq e'"
[PROOF STATE]
proof (prove)
using this:
y \<in> vars_of v'
e' = Eq u' v'

goal (1 subgoal):
 1. y \<in> vars_of_eq e'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> vars_of_eq e'

goal (1 subgoal):
 1. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>N' = (Pos e') \<or> (N' = (Neg e'))\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> vars_of_eq e'
N' = Pos e' \<or> N' = Neg e'
[PROOF STEP]
have "y \<in> vars_of_lit N'"
[PROOF STATE]
proof (prove)
using this:
y \<in> vars_of_eq e'
N' = Pos e' \<or> N' = Neg e'

goal (1 subgoal):
 1. y \<in> vars_of_lit N'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> vars_of_lit N'

goal (1 subgoal):
 1. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>N' \<in> C'\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> vars_of_lit N'
N' \<in> C'
[PROOF STEP]
have "y \<in> vars_of_cl C'"
[PROOF STATE]
proof (prove)
using this:
y \<in> vars_of_lit N'
N' \<in> C'

goal (1 subgoal):
 1. y \<in> vars_of_cl C'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> vars_of_cl C'

goal (1 subgoal):
 1. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>renaming \<eta> (vars_of_cl C')\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> vars_of_cl C'
renaming \<eta> (vars_of_cl C')
[PROOF STEP]
have "is_a_variable (subst (Var y) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
y \<in> vars_of_cl C'
renaming \<eta> (vars_of_cl C')

goal (1 subgoal):
 1. is_a_variable (Var y \<lhd> \<eta>)
[PROOF STEP]
unfolding renaming_def
[PROOF STATE]
proof (prove)
using this:
y \<in> vars_of_cl C'
\<forall>x\<in>vars_of_cl C'. is_a_variable (Var x \<lhd> \<eta>) \<and> (\<forall>x y. x \<in> vars_of_cl C' \<longrightarrow> y \<in> vars_of_cl C' \<longrightarrow> x \<noteq> y \<longrightarrow> Var x \<lhd> \<eta> \<noteq> Var y \<lhd> \<eta>)

goal (1 subgoal):
 1. is_a_variable (Var y \<lhd> \<eta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_a_variable (Var y \<lhd> \<eta>)

goal (1 subgoal):
 1. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>x \<in> vars_of (subst (Var y) \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
is_a_variable (Var y \<lhd> \<eta>)
x \<in> vars_of (Var y \<lhd> \<eta>)
[PROOF STEP]
have
          "Var x = (subst (Var y) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
is_a_variable (Var y \<lhd> \<eta>)
x \<in> vars_of (Var y \<lhd> \<eta>)

goal (1 subgoal):
 1. Var x = Var y \<lhd> \<eta>
[PROOF STEP]
by (metis is_a_variable.elims(2) singletonD vars_of.simps(1))
[PROOF STATE]
proof (state)
this:
Var x = Var y \<lhd> \<eta>

goal (1 subgoal):
 1. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>y \<in> vars_of_cl C'\<close>
[PROOF STATE]
proof (chain)
picking this:
Var x = Var y \<lhd> \<eta>
y \<in> vars_of_cl C'
[PROOF STEP]
have "x \<in> (subst_codomain \<eta> (vars_of_cl C'))"
[PROOF STATE]
proof (prove)
using this:
Var x = Var y \<lhd> \<eta>
y \<in> vars_of_cl C'

goal (1 subgoal):
 1. x \<in> subst_codomain \<eta> (vars_of_cl C')
[PROOF STEP]
unfolding subst_codomain_def
[PROOF STATE]
proof (prove)
using this:
Var x = Var y \<lhd> \<eta>
y \<in> vars_of_cl C'

goal (1 subgoal):
 1. x \<in> {x. \<exists>y. Var y \<lhd> \<eta> = Var x \<and> y \<in> vars_of_cl C'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> subst_codomain \<eta> (vars_of_cl C')

goal (1 subgoal):
 1. x \<in> vars_of v \<Longrightarrow> False
[PROOF STEP]
from this and \<open>x \<in> vars_of_cl (cl_ecl D)\<close>
          and \<open>((subst_codomain \<eta> (vars_of_cl C')) \<inter> (vars_of_cl (cl_ecl D))) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> subst_codomain \<eta> (vars_of_cl C')
x \<in> vars_of_cl (cl_ecl D)
subst_codomain \<eta> (vars_of_cl C') \<inter> vars_of_cl (cl_ecl D) = {}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x \<in> subst_codomain \<eta> (vars_of_cl C')
x \<in> vars_of_cl (cl_ecl D)
subst_codomain \<eta> (vars_of_cl C') \<inter> vars_of_cl (cl_ecl D) = {}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
from this and \<open>(candidate_values z CC_bis C'_bis C s L L'_bis ?\<theta>' t'_bis s'_bis t S)\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
candidate_values z CC_bis C'_bis C s L L'_bis (\<eta>' \<lozenge> \<sigma>) t'_bis s'_bis t S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
candidate_values z CC_bis C'_bis C s L L'_bis (\<eta>' \<lozenge> \<sigma>) t'_bis s'_bis t S

goal (1 subgoal):
 1. \<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>CC_bis C'_bis L'_bis \<sigma>_bis t'_bis s'_bis t_bis. candidate_values z CC_bis C'_bis C s L L'_bis \<sigma>_bis t'_bis s'_bis t S \<and> vars_of_cl (cl_ecl D) \<inter> vars_of_cl (cl_ecl CC_bis) = {}

goal:
No subgoals!
[PROOF STEP]
qed