[STATEMENT]
lemma all_derived_clauses_are_wellconstrained:
  shows "derivable_ecl C S \<Longrightarrow> \<forall>x \<in> S. (well_constrained x) \<Longrightarrow> well_constrained C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>derivable_ecl C S; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
proof (induction rule: derivable_ecl.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
fix C :: "'a eclause"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
assume "C \<in> S"
[PROOF STATE]
proof (state)
this:
C \<in> S

goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
assume "\<forall>x \<in> S. (well_constrained x)"
[PROOF STATE]
proof (state)
this:
Ball S well_constrained

goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
from this \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
Ball S well_constrained
C \<in> S
[PROOF STEP]
show "well_constrained C"
[PROOF STATE]
proof (prove)
using this:
Ball S well_constrained
C \<in> S

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

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
fix C S
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
fix D :: "'a eclause"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
assume "derivable_ecl C S"
[PROOF STATE]
proof (state)
this:
derivable_ecl C S

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
assume "\<forall>x \<in> S. (well_constrained x)"
[PROOF STATE]
proof (state)
this:
Ball S well_constrained

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
assume hyp_ind: "\<forall>x \<in> S. (well_constrained x) \<Longrightarrow> well_constrained C"
    "(renaming_cl C D)"
[PROOF STATE]
proof (state)
this:
Ball S well_constrained \<Longrightarrow> well_constrained C
renaming_cl C D

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
from \<open>\<forall>x \<in> S. (well_constrained x)\<close> and hyp_ind
[PROOF STATE]
proof (chain)
picking this:
Ball S well_constrained
Ball S well_constrained \<Longrightarrow> well_constrained C
renaming_cl C D
[PROOF STEP]
have "well_constrained C"
[PROOF STATE]
proof (prove)
using this:
Ball S well_constrained
Ball S well_constrained \<Longrightarrow> well_constrained C
renaming_cl C D

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

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
from \<open>(renaming_cl C D)\<close>
[PROOF STATE]
proof (chain)
picking this:
renaming_cl C D
[PROOF STEP]
obtain \<eta> where "D = (subst_ecl C \<eta>)"
[PROOF STATE]
proof (prove)
using this:
renaming_cl C D

goal (1 subgoal):
 1. (\<And>\<eta>. D = subst_ecl C \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding renaming_cl_def
[PROOF STATE]
proof (prove)
using this:
\<exists>\<eta>. renaming \<eta> (vars_of_cl (cl_ecl C)) \<and> D = subst_ecl C \<eta>

goal (1 subgoal):
 1. (\<And>\<eta>. D = subst_ecl C \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D = subst_ecl C \<eta>

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; Ball S well_constrained \<Longrightarrow> well_constrained C; renaming_cl C D; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained D
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
from this and \<open>well_constrained C\<close>
[PROOF STATE]
proof (chain)
picking this:
D = subst_ecl C \<eta>
well_constrained C
[PROOF STEP]
show "well_constrained D"
[PROOF STATE]
proof (prove)
using this:
D = subst_ecl C \<eta>
well_constrained C

goal (1 subgoal):
 1. well_constrained D
[PROOF STEP]
using substs_preserve_well_constrainedness
[PROOF STATE]
proof (prove)
using this:
D = subst_ecl C \<eta>
well_constrained C
well_constrained ?C \<Longrightarrow> well_constrained (subst_ecl ?C ?\<sigma>)

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

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
fix P S C S' \<sigma> C'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
assume "\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x)"
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x)

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
assume "derivable C P S' \<sigma> FirstOrder C'"
[PROOF STATE]
proof (state)
this:
derivable C P S' \<sigma> FirstOrder C'

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
assume "Ball S well_constrained"
[PROOF STATE]
proof (state)
this:
Ball S well_constrained

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> (Ball S well_constrained \<longrightarrow> well_constrained x); derivable C P S' \<sigma> FirstOrder C'; Ball S well_constrained\<rbrakk> \<Longrightarrow> well_constrained C
[PROOF STEP]
from \<open>derivable C P S' \<sigma> FirstOrder C'\<close>
[PROOF STATE]
proof (chain)
picking this:
derivable C P S' \<sigma> FirstOrder C'
[PROOF STEP]
show "well_constrained C"
[PROOF STATE]
proof (prove)
using this:
derivable C P S' \<sigma> FirstOrder C'

goal (1 subgoal):
 1. well_constrained C
[PROOF STEP]
using derivable_clauses_are_well_constrained
[PROOF STATE]
proof (prove)
using this:
derivable C P S' \<sigma> FirstOrder C'
derivable ?C ?P ?S ?\<sigma> ?k ?C' \<Longrightarrow> well_constrained ?C

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma SOUNDNESS:
  shows "derivable_ecl C S \<Longrightarrow> \<forall>x \<in> S. (finite (cl_ecl x))
    \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
proof (induction rule: derivable_ecl.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
fix C :: "'a eclause"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
assume "C \<in> S"
[PROOF STATE]
proof (state)
this:
C \<in> S

goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
assume "\<forall>x \<in> S. (finite (cl_ecl x))"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. finite (cl_ecl x)

goal (3 subgoals):
 1. \<And>C S. \<lbrakk>C \<in> S; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
 2. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 3. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
from \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
C \<in> S
[PROOF STEP]
show "set_entails_clause (cl_ecl ` S) (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
C \<in> S

goal (1 subgoal):
 1. set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
unfolding set_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
C \<in> S

goal (1 subgoal):
 1. \<forall>I. fo_interpretation I \<longrightarrow> validate_clause_set I (cl_ecl ` S) \<longrightarrow> validate_clause I (cl_ecl C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_entails_clause (cl_ecl ` S) (cl_ecl C)

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
fix C S
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
fix D :: "'a eclause"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
assume "derivable_ecl C S"
[PROOF STATE]
proof (state)
this:
derivable_ecl C S

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
assume "\<forall>x \<in> S. (finite (cl_ecl x))"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. finite (cl_ecl x)

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
assume hyp_ind: "\<forall>x \<in> S. (finite (cl_ecl x)) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
assume  "(renaming_cl C D)"
[PROOF STATE]
proof (state)
this:
renaming_cl C D

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
from \<open>(renaming_cl C D)\<close>
[PROOF STATE]
proof (chain)
picking this:
renaming_cl C D
[PROOF STEP]
obtain \<eta> where "D = (subst_ecl C \<eta>)"
[PROOF STATE]
proof (prove)
using this:
renaming_cl C D

goal (1 subgoal):
 1. (\<And>\<eta>. D = subst_ecl C \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding renaming_cl_def
[PROOF STATE]
proof (prove)
using this:
\<exists>\<eta>. renaming \<eta> (vars_of_cl (cl_ecl C)) \<and> D = subst_ecl C \<eta>

goal (1 subgoal):
 1. (\<And>\<eta>. D = subst_ecl C \<eta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D = subst_ecl C \<eta>

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
obtain C_Cl T where "C = (Ecl C_Cl T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C_Cl T. C = Ecl C_Cl T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using "eclause.exhaust"
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = Ecl x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>C_Cl T. C = Ecl C_Cl T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = Ecl C_Cl T

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
from this and \<open>D = (subst_ecl C \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
C = Ecl C_Cl T
D = subst_ecl C \<eta>
[PROOF STEP]
have "(cl_ecl D) = (subst_cl (cl_ecl C) \<eta>)"
[PROOF STATE]
proof (prove)
using this:
C = Ecl C_Cl T
D = subst_ecl C \<eta>

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

goal (2 subgoals):
 1. \<And>C S D. \<lbrakk>derivable_ecl C S; \<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C); renaming_cl C D; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl D)
 2. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
show "set_entails_clause (cl_ecl ` S) (cl_ecl D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_entails_clause (cl_ecl ` S) (cl_ecl D)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>?thesis"
[PROOF STATE]
proof (state)
this:
\<not> set_entails_clause (cl_ecl ` S) (cl_ecl D)

goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> set_entails_clause (cl_ecl ` S) (cl_ecl D)
[PROOF STEP]
obtain I where "fo_interpretation I" and i: "validate_clause_set I (cl_ecl `S)"
      "\<not>validate_clause I (cl_ecl D)"
[PROOF STATE]
proof (prove)
using this:
\<not> set_entails_clause (cl_ecl ` S) (cl_ecl D)

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>fo_interpretation I; validate_clause_set I (cl_ecl ` S); \<not> validate_clause I (cl_ecl D)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding set_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>I. fo_interpretation I \<longrightarrow> validate_clause_set I (cl_ecl ` S) \<longrightarrow> validate_clause I (cl_ecl D))

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>fo_interpretation I; validate_clause_set I (cl_ecl ` S); \<not> validate_clause I (cl_ecl D)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fo_interpretation I
validate_clause_set I (cl_ecl ` S)
\<not> validate_clause I (cl_ecl D)

goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not>validate_clause I (cl_ecl D)\<close> and \<open>(cl_ecl D) = (subst_cl (cl_ecl C) \<eta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> validate_clause I (cl_ecl D)
cl_ecl D = subst_cl (cl_ecl C) \<eta>
[PROOF STEP]
have "\<not>validate_clause I (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause I (cl_ecl D)
cl_ecl D = subst_cl (cl_ecl C) \<eta>

goal (1 subgoal):
 1. \<not> validate_clause I (cl_ecl C)
[PROOF STEP]
using instances_are_entailed
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause I (cl_ecl D)
cl_ecl D = subst_cl (cl_ecl C) \<eta>
validate_clause ?I ?C \<Longrightarrow> validate_clause ?I (subst_cl ?C ?\<sigma>)

goal (1 subgoal):
 1. \<not> validate_clause I (cl_ecl C)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<not> validate_clause I (cl_ecl C)

goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>fo_interpretation I\<close> i
[PROOF STATE]
proof (chain)
picking this:
\<not> validate_clause I (cl_ecl C)
fo_interpretation I
validate_clause_set I (cl_ecl ` S)
\<not> validate_clause I (cl_ecl D)
[PROOF STEP]
have "\<not>set_entails_clause (cl_ecl ` S) (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause I (cl_ecl C)
fo_interpretation I
validate_clause_set I (cl_ecl ` S)
\<not> validate_clause I (cl_ecl D)

goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
unfolding set_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause I (cl_ecl C)
fo_interpretation I
validate_clause_set I (cl_ecl ` S)
\<not> validate_clause I (cl_ecl D)

goal (1 subgoal):
 1. \<not> (\<forall>I. fo_interpretation I \<longrightarrow> validate_clause_set I (cl_ecl ` S) \<longrightarrow> validate_clause I (cl_ecl C))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> set_entails_clause (cl_ecl ` S) (cl_ecl C)

goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl D) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<forall>x \<in> S. (finite (cl_ecl x))\<close> hyp_ind
[PROOF STATE]
proof (chain)
picking this:
\<not> set_entails_clause (cl_ecl ` S) (cl_ecl C)
\<forall>x\<in>S. finite (cl_ecl x)
\<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> set_entails_clause (cl_ecl ` S) (cl_ecl C)
\<forall>x\<in>S. finite (cl_ecl x)
\<forall>x\<in>S. finite (cl_ecl x) \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)

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:
set_entails_clause (cl_ecl ` S) (cl_ecl D)

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
fix P S C S' \<sigma> C'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
assume h: "\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x))"
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x))

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
assume "derivable C P S' \<sigma> FirstOrder C'"
[PROOF STATE]
proof (state)
this:
derivable C P S' \<sigma> FirstOrder C'

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
assume "\<forall>x\<in>S. finite (cl_ecl x)"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. finite (cl_ecl x)

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
from h and \<open>\<forall>x\<in>S. finite (cl_ecl x)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x))
\<forall>x\<in>S. finite (cl_ecl x)
[PROOF STEP]
have i: "\<forall>x \<in> P.  set_entails_clause (cl_ecl ` S) (cl_ecl x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x))
\<forall>x\<in>S. finite (cl_ecl x)

goal (1 subgoal):
 1. \<forall>x\<in>P. set_entails_clause (cl_ecl ` S) (cl_ecl x)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>P. set_entails_clause (cl_ecl ` S) (cl_ecl x)

goal (1 subgoal):
 1. \<And>P S C S' \<sigma> C'. \<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x)); derivable C P S' \<sigma> FirstOrder C'; \<forall>x\<in>S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
show "set_entails_clause (cl_ecl ` S) (cl_ecl C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>?thesis"
[PROOF STATE]
proof (state)
this:
\<not> set_entails_clause (cl_ecl ` S) (cl_ecl C)

goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
obtain I where "fo_interpretation I" and ii: "validate_clause_set I (cl_ecl `S)"
      "\<not>validate_clause I (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
\<not> set_entails_clause (cl_ecl ` S) (cl_ecl C)

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>fo_interpretation I; validate_clause_set I (cl_ecl ` S); \<not> validate_clause I (cl_ecl C)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding set_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>I. fo_interpretation I \<longrightarrow> validate_clause_set I (cl_ecl ` S) \<longrightarrow> validate_clause I (cl_ecl C))

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>fo_interpretation I; validate_clause_set I (cl_ecl ` S); \<not> validate_clause I (cl_ecl C)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fo_interpretation I
validate_clause_set I (cl_ecl ` S)
\<not> validate_clause I (cl_ecl C)

goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
from h \<open>\<forall>x\<in>S. finite (cl_ecl x)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x))
\<forall>x\<in>S. finite (cl_ecl x)
[PROOF STEP]
have "(\<forall>x\<in>P. finite (cl_ecl x))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x))
\<forall>x\<in>S. finite (cl_ecl x)

goal (1 subgoal):
 1. \<forall>x\<in>P. finite (cl_ecl x)
[PROOF STEP]
using all_derived_clauses_are_finite
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S \<and> ((\<forall>x\<in>S. finite (cl_ecl x)) \<longrightarrow> set_entails_clause (cl_ecl ` S) (cl_ecl x))
\<forall>x\<in>S. finite (cl_ecl x)
\<lbrakk>derivable_ecl ?C ?S; \<forall>x\<in>?S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> finite (cl_ecl ?C)

goal (1 subgoal):
 1. \<forall>x\<in>P. finite (cl_ecl x)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>P. finite (cl_ecl x)

goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
from \<open>fo_interpretation I\<close>  i and ii
[PROOF STATE]
proof (chain)
picking this:
fo_interpretation I
\<forall>x\<in>P. set_entails_clause (cl_ecl ` S) (cl_ecl x)
validate_clause_set I (cl_ecl ` S)
\<not> validate_clause I (cl_ecl C)
[PROOF STEP]
have "\<forall>x \<in> P.  (validate_clause I (cl_ecl x))"
[PROOF STATE]
proof (prove)
using this:
fo_interpretation I
\<forall>x\<in>P. set_entails_clause (cl_ecl ` S) (cl_ecl x)
validate_clause_set I (cl_ecl ` S)
\<not> validate_clause I (cl_ecl C)

goal (1 subgoal):
 1. \<forall>x\<in>P. validate_clause I (cl_ecl x)
[PROOF STEP]
unfolding set_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
fo_interpretation I
\<forall>x\<in>P. \<forall>I. fo_interpretation I \<longrightarrow> validate_clause_set I (cl_ecl ` S) \<longrightarrow> validate_clause I (cl_ecl x)
validate_clause_set I (cl_ecl ` S)
\<not> validate_clause I (cl_ecl C)

goal (1 subgoal):
 1. \<forall>x\<in>P. validate_clause I (cl_ecl x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>P. validate_clause I (cl_ecl x)

goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>P. validate_clause I (cl_ecl x)
[PROOF STEP]
have "validate_clause_set I (cl_ecl ` P)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>P. validate_clause I (cl_ecl x)

goal (1 subgoal):
 1. validate_clause_set I (cl_ecl ` P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
validate_clause_set I (cl_ecl ` P)

goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(\<forall>x\<in>P. finite (cl_ecl x))\<close> \<open>fo_interpretation I\<close> \<open>derivable C P S' \<sigma> FirstOrder C'\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_clause_set I (cl_ecl ` P)
\<forall>x\<in>P. finite (cl_ecl x)
fo_interpretation I
derivable C P S' \<sigma> FirstOrder C'
[PROOF STEP]
have "validate_clause I (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
validate_clause_set I (cl_ecl ` P)
\<forall>x\<in>P. finite (cl_ecl x)
fo_interpretation I
derivable C P S' \<sigma> FirstOrder C'

goal (1 subgoal):
 1. validate_clause I (cl_ecl C)
[PROOF STEP]
using derivable_clauses_are_entailed [of C P S' \<sigma> FirstOrder C' I]
[PROOF STATE]
proof (prove)
using this:
validate_clause_set I (cl_ecl ` P)
\<forall>x\<in>P. finite (cl_ecl x)
fo_interpretation I
derivable C P S' \<sigma> FirstOrder C'
\<lbrakk>derivable C P S' \<sigma> FirstOrder C'; validate_clause_set I (cl_ecl ` P); fo_interpretation I; \<forall>x\<in>P. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> validate_clause I (cl_ecl C)

goal (1 subgoal):
 1. validate_clause I (cl_ecl C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
validate_clause I (cl_ecl C)

goal (1 subgoal):
 1. \<not> set_entails_clause (cl_ecl ` S) (cl_ecl C) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not>validate_clause I (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_clause I (cl_ecl C)
\<not> validate_clause I (cl_ecl C)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_clause I (cl_ecl C)
\<not> validate_clause I (cl_ecl C)

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:
set_entails_clause (cl_ecl ` S) (cl_ecl C)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma REFUTABLE_SETS_ARE_UNSAT:
  assumes "\<forall>x \<in> S. (finite (cl_ecl x))"
  assumes "derivable_ecl C S"
  assumes "(cl_ecl C = {})"
  shows "\<not> (satisfiable_clause_set (cl_ecl ` S))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> satisfiable_clause_set (cl_ecl ` S)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. satisfiable_clause_set (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
assume "(satisfiable_clause_set (cl_ecl ` S))"
[PROOF STATE]
proof (state)
this:
satisfiable_clause_set (cl_ecl ` S)

goal (1 subgoal):
 1. satisfiable_clause_set (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
satisfiable_clause_set (cl_ecl ` S)
[PROOF STEP]
obtain I where "fo_interpretation I" and model: "validate_clause_set I (cl_ecl ` S)"
[PROOF STATE]
proof (prove)
using this:
satisfiable_clause_set (cl_ecl ` S)

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>fo_interpretation I; validate_clause_set I (cl_ecl ` S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding satisfiable_clause_set_def [of "cl_ecl ` S"]
[PROOF STATE]
proof (prove)
using this:
\<exists>I. fo_interpretation I \<and> validate_clause_set I (cl_ecl ` S)

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>fo_interpretation I; validate_clause_set I (cl_ecl ` S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fo_interpretation I
validate_clause_set I (cl_ecl ` S)

goal (1 subgoal):
 1. satisfiable_clause_set (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from assms(1) assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S. finite (cl_ecl x)
derivable_ecl C S
[PROOF STEP]
have "set_entails_clause (cl_ecl ` S) (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. finite (cl_ecl x)
derivable_ecl C S

goal (1 subgoal):
 1. set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
using SOUNDNESS
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. finite (cl_ecl x)
derivable_ecl C S
\<lbrakk>derivable_ecl ?C ?S; \<forall>x\<in>?S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> set_entails_clause (cl_ecl ` ?S) (cl_ecl ?C)

goal (1 subgoal):
 1. set_entails_clause (cl_ecl ` S) (cl_ecl C)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
set_entails_clause (cl_ecl ` S) (cl_ecl C)

goal (1 subgoal):
 1. satisfiable_clause_set (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from this \<open>fo_interpretation I\<close> and model
[PROOF STATE]
proof (chain)
picking this:
set_entails_clause (cl_ecl ` S) (cl_ecl C)
fo_interpretation I
validate_clause_set I (cl_ecl ` S)
[PROOF STEP]
have "validate_clause I (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
set_entails_clause (cl_ecl ` S) (cl_ecl C)
fo_interpretation I
validate_clause_set I (cl_ecl ` S)

goal (1 subgoal):
 1. validate_clause I (cl_ecl C)
[PROOF STEP]
unfolding set_entails_clause_def
[PROOF STATE]
proof (prove)
using this:
\<forall>I. fo_interpretation I \<longrightarrow> validate_clause_set I (cl_ecl ` S) \<longrightarrow> validate_clause I (cl_ecl C)
fo_interpretation I
validate_clause_set I (cl_ecl ` S)

goal (1 subgoal):
 1. validate_clause I (cl_ecl C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
validate_clause I (cl_ecl C)

goal (1 subgoal):
 1. satisfiable_clause_set (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from this and assms(3)
[PROOF STATE]
proof (chain)
picking this:
validate_clause I (cl_ecl C)
cl_ecl C = {}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_clause I (cl_ecl C)
cl_ecl C = {}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subterms_inclusion_refl:
 shows "subterms_inclusion E E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subterms_inclusion E E
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> subterms_inclusion E E \<Longrightarrow> False
[PROOF STEP]
assume "\<not>subterms_inclusion E E"
[PROOF STATE]
proof (state)
this:
\<not> subterms_inclusion E E

goal (1 subgoal):
 1. \<not> subterms_inclusion E E \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> subterms_inclusion E E
[PROOF STEP]
obtain x1 where "x1 \<in> E" and "\<not> occurs_in x1 x1"
[PROOF STATE]
proof (prove)
using this:
\<not> subterms_inclusion E E

goal (1 subgoal):
 1. (\<And>x1. \<lbrakk>x1 \<in> E; \<not> occurs_in x1 x1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding subterms_inclusion_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x1\<in>E. Bex E (occurs_in x1))

goal (1 subgoal):
 1. (\<And>x1. \<lbrakk>x1 \<in> E; \<not> occurs_in x1 x1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x1 \<in> E
\<not> occurs_in x1 x1

goal (1 subgoal):
 1. \<not> subterms_inclusion E E \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not> occurs_in x1 x1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> occurs_in x1 x1
[PROOF STEP]
have "\<not> (\<exists>p. subterm x1 p x1)"
[PROOF STATE]
proof (prove)
using this:
\<not> occurs_in x1 x1

goal (1 subgoal):
 1. \<nexists>p. subterm x1 p x1
[PROOF STEP]
unfolding occurs_in_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>p. subterm x1 p x1

goal (1 subgoal):
 1. \<nexists>p. subterm x1 p x1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>p. subterm x1 p x1

goal (1 subgoal):
 1. \<not> subterms_inclusion E E \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<nexists>p. subterm x1 p x1
[PROOF STEP]
have "\<not>subterm x1 Nil x1"
[PROOF STATE]
proof (prove)
using this:
\<nexists>p. subterm x1 p x1

goal (1 subgoal):
 1. \<not> subterm x1 [] x1
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<not> subterm x1 [] x1

goal (1 subgoal):
 1. \<not> subterms_inclusion E E \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> subterm x1 [] x1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> subterm x1 [] x1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subterms_inclusion_subset:
  assumes "subterms_inclusion E1 E2"
  assumes "E2 \<subseteq> E2'"
  shows "subterms_inclusion E1 E2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subterms_inclusion E1 E2'
[PROOF STEP]
by (meson assms(1) assms(2) basic_superposition.subterms_inclusion_def basic_superposition_axioms
      subsetD)


[STATEMENT]
lemma set_inclusion_preserve_normalization:
  assumes "all_trms_irreducible E f"
  assumes "E' \<subseteq> E"
  shows "all_trms_irreducible E' f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_trms_irreducible E' f
[PROOF STEP]
by (meson all_trms_irreducible_def assms(1) assms(2) subsetD)


[STATEMENT]
lemma subterms_inclusion_preserves_normalization:
  assumes "all_trms_irreducible E f"
  assumes "subterms_inclusion E' E"
  shows "all_trms_irreducible E' f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_trms_irreducible E' f
[PROOF STEP]
by (meson all_trms_irreducible_def assms(1) assms(2) occur_in_subterm subterms_inclusion_def)


[STATEMENT]
lemma self_redundant_clause:
  assumes "C \<in> S"
  assumes "C' = (cl_ecl C)"
  assumes "ground_clause (subst_cl (cl_ecl C) \<sigma>)"
  shows "redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
obtain Cl_C and T where "C = Ecl Cl_C T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Cl_C T. C = Ecl Cl_C T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eclause.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = Ecl x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>Cl_C T. C = Ecl Cl_C T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = Ecl Cl_C T

goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
C = Ecl Cl_C T
[PROOF STEP]
have "cl_ecl C = Cl_C" and "trms_ecl C = T"
[PROOF STATE]
proof (prove)
using this:
C = Ecl Cl_C T

goal (1 subgoal):
 1. cl_ecl C = Cl_C &&& trms_ecl C = T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cl_ecl C = Cl_C
trms_ecl C = T

goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
let ?Cl_C = "subst_cl Cl_C \<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
let ?T  = "subst_set T \<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
let ?C = "subst_ecl C \<sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
from \<open>C = Ecl Cl_C T\<close>
[PROOF STATE]
proof (chain)
picking this:
C = Ecl Cl_C T
[PROOF STEP]
have "?C = (Ecl ?Cl_C ?T)"
[PROOF STATE]
proof (prove)
using this:
C = Ecl Cl_C T

goal (1 subgoal):
 1. subst_ecl C \<sigma> = Ecl (subst_cl Cl_C \<sigma>) (subst_set T \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_ecl C \<sigma> = Ecl (subst_cl Cl_C \<sigma>) (subst_set T \<sigma>)

goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subst_ecl C \<sigma> = Ecl (subst_cl Cl_C \<sigma>) (subst_set T \<sigma>)
[PROOF STEP]
have "cl_ecl ?C = ?Cl_C" and "trms_ecl ?C = ?T"
[PROOF STATE]
proof (prove)
using this:
subst_ecl C \<sigma> = Ecl (subst_cl Cl_C \<sigma>) (subst_set T \<sigma>)

goal (1 subgoal):
 1. cl_ecl (subst_ecl C \<sigma>) = subst_cl Cl_C \<sigma> &&& trms_ecl (subst_ecl C \<sigma>) = subst_set T \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cl_ecl (subst_ecl C \<sigma>) = subst_cl Cl_C \<sigma>
trms_ecl (subst_ecl C \<sigma>) = subst_set T \<sigma>

goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
let ?S = "{ (C,\<sigma>) }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
from assms(1) assms(3)
[PROOF STATE]
proof (chain)
picking this:
C \<in> S
ground_clause (subst_cl (cl_ecl C) \<sigma>)
[PROOF STEP]
have i: "?S \<subseteq> (instances S)"
[PROOF STATE]
proof (prove)
using this:
C \<in> S
ground_clause (subst_cl (cl_ecl C) \<sigma>)

goal (1 subgoal):
 1. {(C, \<sigma>)} \<subseteq> instances S
[PROOF STEP]
unfolding instances_def
[PROOF STATE]
proof (prove)
using this:
C \<in> S
ground_clause (subst_cl (cl_ecl C) \<sigma>)

goal (1 subgoal):
 1. {(C, \<sigma>)} \<subseteq> {x. \<exists>C \<sigma>. C \<in> S \<and> ground_clause (subst_cl (cl_ecl C) \<sigma>) \<and> x = (C, \<sigma>)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(C, \<sigma>)} \<subseteq> instances S

goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
from \<open>cl_ecl C = Cl_C\<close>
[PROOF STATE]
proof (chain)
picking this:
cl_ecl C = Cl_C
[PROOF STEP]
have "clset_instances ?S = { ?Cl_C }"
[PROOF STATE]
proof (prove)
using this:
cl_ecl C = Cl_C

goal (1 subgoal):
 1. clset_instances {(C, \<sigma>)} = {subst_cl Cl_C \<sigma>}
[PROOF STEP]
unfolding clset_instances_def
[PROOF STATE]
proof (prove)
using this:
cl_ecl C = Cl_C

goal (1 subgoal):
 1. {Ca. \<exists>x. x \<in> {(C, \<sigma>)} \<and> Ca = subst_cl (cl_ecl (fst x)) (snd x)} = {subst_cl Cl_C \<sigma>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
clset_instances {(C, \<sigma>)} = {subst_cl Cl_C \<sigma>}

goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
from this and \<open>cl_ecl ?C = ?Cl_C\<close>
[PROOF STATE]
proof (chain)
picking this:
clset_instances {(C, \<sigma>)} = {subst_cl Cl_C \<sigma>}
cl_ecl (subst_ecl C \<sigma>) = subst_cl Cl_C \<sigma>
[PROOF STEP]
have ii: "set_entails_clause (clset_instances ?S) (cl_ecl ?C)"
[PROOF STATE]
proof (prove)
using this:
clset_instances {(C, \<sigma>)} = {subst_cl Cl_C \<sigma>}
cl_ecl (subst_ecl C \<sigma>) = subst_cl Cl_C \<sigma>

goal (1 subgoal):
 1. set_entails_clause (clset_instances {(C, \<sigma>)}) (cl_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
using set_entails_clause_member
[PROOF STATE]
proof (prove)
using this:
clset_instances {(C, \<sigma>)} = {subst_cl Cl_C \<sigma>}
cl_ecl (subst_ecl C \<sigma>) = subst_cl Cl_C \<sigma>
?C \<in> ?S \<Longrightarrow> set_entails_clause ?S ?C

goal (1 subgoal):
 1. set_entails_clause (clset_instances {(C, \<sigma>)}) (cl_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
set_entails_clause (clset_instances {(C, \<sigma>)}) (cl_ecl (subst_ecl C \<sigma>))

goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
have iii: "(\<forall>x \<in> ?S. ( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl ?C)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{(C, \<sigma>)}. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
assume "x \<in> ?S"
[PROOF STATE]
proof (state)
this:
x \<in> {(C, \<sigma>)}

goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> {(C, \<sigma>)}
[PROOF STEP]
have "x = (C,\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
x \<in> {(C, \<sigma>)}

goal (1 subgoal):
 1. x = (C, \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (C, \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
from this \<open>C = Ecl Cl_C T\<close>
[PROOF STATE]
proof (chain)
picking this:
x = (C, \<sigma>)
C = Ecl Cl_C T
[PROOF STEP]
have "subst_set (trms_ecl (fst x)) (snd x) = ?T"
[PROOF STATE]
proof (prove)
using this:
x = (C, \<sigma>)
C = Ecl Cl_C T

goal (1 subgoal):
 1. subst_set (trms_ecl (fst x)) (snd x) = subst_set T \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_set (trms_ecl (fst x)) (snd x) = subst_set T \<sigma>

goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
from this and \<open>trms_ecl ?C = ?T\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_set (trms_ecl (fst x)) (snd x) = subst_set T \<sigma>
trms_ecl (subst_ecl C \<sigma>) = subst_set T \<sigma>
[PROOF STEP]
have "subst_set (trms_ecl (fst x)) (snd x) = (trms_ecl ?C)"
[PROOF STATE]
proof (prove)
using this:
subst_set (trms_ecl (fst x)) (snd x) = subst_set T \<sigma>
trms_ecl (subst_ecl C \<sigma>) = subst_set T \<sigma>

goal (1 subgoal):
 1. subst_set (trms_ecl (fst x)) (snd x) = trms_ecl (subst_ecl C \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_set (trms_ecl (fst x)) (snd x) = trms_ecl (subst_ecl C \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subst_set (trms_ecl (fst x)) (snd x) = trms_ecl (subst_ecl C \<sigma>)
[PROOF STEP]
show "( subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x))
              (trms_ecl ?C))"
[PROOF STATE]
proof (prove)
using this:
subst_set (trms_ecl (fst x)) (snd x) = trms_ecl (subst_ecl C \<sigma>)

goal (1 subgoal):
 1. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
using subterms_inclusion_refl
[PROOF STATE]
proof (prove)
using this:
subst_set (trms_ecl (fst x)) (snd x) = trms_ecl (subst_ecl C \<sigma>)
subterms_inclusion ?E ?E

goal (1 subgoal):
 1. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{(C, \<sigma>)}. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))

goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
have iv: "(\<forall>x \<in> ?S. ( ((mset_ecl ((fst x),(snd x))),(mset_cl (C',\<sigma>))) \<in> (mult (mult trm_ord))
              \<or> (mset_ecl ((fst x),(snd x))) = mset_cl (C',\<sigma>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{(C, \<sigma>)}. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
assume "x \<in> ?S"
[PROOF STATE]
proof (state)
this:
x \<in> {(C, \<sigma>)}

goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> {(C, \<sigma>)}
[PROOF STEP]
have "x = (C,\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
x \<in> {(C, \<sigma>)}

goal (1 subgoal):
 1. x = (C, \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (C, \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
from this \<open>C = Ecl Cl_C T\<close>
[PROOF STATE]
proof (chain)
picking this:
x = (C, \<sigma>)
C = Ecl Cl_C T
[PROOF STEP]
have "(mset_ecl ((fst x),(snd x))) = (mset_ecl (C,\<sigma>))"
[PROOF STATE]
proof (prove)
using this:
x = (C, \<sigma>)
C = Ecl Cl_C T

goal (1 subgoal):
 1. mset_ecl (fst x, snd x) = mset_ecl (C, \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_ecl (fst x, snd x) = mset_ecl (C, \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
from this \<open>C' = (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
mset_ecl (fst x, snd x) = mset_ecl (C, \<sigma>)
C' = cl_ecl C
[PROOF STEP]
have "(mset_ecl ((fst x),(snd x))) = mset_cl (C',\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
mset_ecl (fst x, snd x) = mset_ecl (C, \<sigma>)
C' = cl_ecl C

goal (1 subgoal):
 1. mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> {(C, \<sigma>)} \<Longrightarrow> (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
show "( ((mset_ecl ((fst x),(snd x))),(mset_cl (C',\<sigma>))) \<in> (mult (mult trm_ord))
              \<or> (mset_ecl ((fst x),(snd x))) = mset_cl (C',\<sigma>))"
[PROOF STATE]
proof (prove)
using this:
mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{(C, \<sigma>)}. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)

goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
from i ii iii iv
[PROOF STATE]
proof (chain)
picking this:
{(C, \<sigma>)} \<subseteq> instances S
set_entails_clause (clset_instances {(C, \<sigma>)}) (cl_ecl (subst_ecl C \<sigma>))
\<forall>x\<in>{(C, \<sigma>)}. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
\<forall>x\<in>{(C, \<sigma>)}. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{(C, \<sigma>)} \<subseteq> instances S
set_entails_clause (clset_instances {(C, \<sigma>)}) (cl_ecl (subst_ecl C \<sigma>))
\<forall>x\<in>{(C, \<sigma>)}. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
\<forall>x\<in>{(C, \<sigma>)}. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)

goal (1 subgoal):
 1. redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'
[PROOF STEP]
unfolding redundant_clause_def
[PROOF STATE]
proof (prove)
using this:
{(C, \<sigma>)} \<subseteq> instances S
set_entails_clause (clset_instances {(C, \<sigma>)}) (cl_ecl (subst_ecl C \<sigma>))
\<forall>x\<in>{(C, \<sigma>)}. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))
\<forall>x\<in>{(C, \<sigma>)}. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>)

goal (1 subgoal):
 1. \<exists>S'\<subseteq>instances S. set_entails_clause (clset_instances S') (cl_ecl (subst_ecl C \<sigma>)) \<and> (\<forall>x\<in>S'. subterms_inclusion (subst_set (trms_ecl (fst x)) (snd x)) (trms_ecl (subst_ecl C \<sigma>))) \<and> (\<forall>x\<in>S'. (mset_ecl (fst x, snd x), mset_cl (C', \<sigma>)) \<in> mult (mult trm_ord) \<or> mset_ecl (fst x, snd x) = mset_cl (C', \<sigma>))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
redundant_clause (subst_ecl C \<sigma>) S \<sigma> C'

goal:
No subgoals!
[PROOF STEP]
qed