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

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
let ?S = "{ y. (derivable_ecl y S) }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
let ?I = "same_values (\<lambda>x. (trm_rep x ?S))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
have "fo_interpretation ?I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fo_interpretation (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S}))
[PROOF STEP]
using trm_rep_compatible_with_structure same_values_fo_int
[PROOF STATE]
proof (prove)
using this:
value_is_compatible_with_structure (\<lambda>x. trm_rep x ?S)
value_is_compatible_with_structure ?f \<Longrightarrow> fo_interpretation (same_values ?f)

goal (1 subgoal):
 1. fo_interpretation (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S}))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
fo_interpretation (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S}))

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
have "\<forall>x \<in> ?S. (cl_ecl x) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {}) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {})

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {}) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {})
[PROOF STEP]
obtain x where "x \<in> ?S" and "cl_ecl x = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {})

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> {y. derivable_ecl y S}; cl_ecl x = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> {y. derivable_ecl y S}
cl_ecl x = {}

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {}) \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<in> ?S\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> {y. derivable_ecl y S}
[PROOF STEP]
have "derivable_ecl x S"
[PROOF STATE]
proof (prove)
using this:
x \<in> {y. derivable_ecl y S}

goal (1 subgoal):
 1. derivable_ecl x S
[PROOF STEP]
by (meson CollectD)
[PROOF STATE]
proof (state)
this:
derivable_ecl x S

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {}) \<Longrightarrow> False
[PROOF STEP]
from this  \<open>cl_ecl x = {}\<close> \<open>\<not> (\<exists>x. (derivable_ecl x S) \<and> cl_ecl x = {})\<close>
[PROOF STATE]
proof (chain)
picking this:
derivable_ecl x S
cl_ecl x = {}
\<nexists>x. derivable_ecl x S \<and> cl_ecl x = {}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
derivable_ecl x S
cl_ecl x = {}
\<nexists>x. derivable_ecl x S \<and> cl_ecl 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:
\<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {}

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
have all_finite: "\<forall>x \<in> ?S. (finite (cl_ecl x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x))

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x))
[PROOF STEP]
obtain x where "x \<in> ?S" and "\<not> finite (cl_ecl x)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x))

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> {y. derivable_ecl y S}; infinite (cl_ecl x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> {y. derivable_ecl y S}
infinite (cl_ecl x)

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)) \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<in> ?S\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> {y. derivable_ecl y S}
[PROOF STEP]
have "derivable_ecl x S"
[PROOF STATE]
proof (prove)
using this:
x \<in> {y. derivable_ecl y S}

goal (1 subgoal):
 1. derivable_ecl x S
[PROOF STEP]
by (meson CollectD)
[PROOF STATE]
proof (state)
this:
derivable_ecl x S

goal (1 subgoal):
 1. \<not> (\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)) \<Longrightarrow> False
[PROOF STEP]
from this assms(2) \<open>\<not> finite (cl_ecl x)\<close>
[PROOF STATE]
proof (chain)
picking this:
derivable_ecl x S
\<forall>x\<in>S. finite (cl_ecl x)
infinite (cl_ecl x)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
derivable_ecl x S
\<forall>x\<in>S. finite (cl_ecl x)
infinite (cl_ecl x)

goal (1 subgoal):
 1. False
[PROOF STEP]
using all_derived_clauses_are_finite
[PROOF STATE]
proof (prove)
using this:
derivable_ecl x S
\<forall>x\<in>S. finite (cl_ecl x)
infinite (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. False
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
have "Ball S well_constrained"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball S well_constrained
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> well_constrained x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> well_constrained x
[PROOF STEP]
assume "x \<in> S"
[PROOF STATE]
proof (state)
this:
x \<in> S

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> well_constrained x
[PROOF STEP]
from this assms(1)
[PROOF STATE]
proof (chain)
picking this:
x \<in> S
\<forall>x. x \<in> S \<longrightarrow> trms_ecl x = {}
[PROOF STEP]
have "trms_ecl x = {}"
[PROOF STATE]
proof (prove)
using this:
x \<in> S
\<forall>x. x \<in> S \<longrightarrow> trms_ecl x = {}

goal (1 subgoal):
 1. trms_ecl x = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trms_ecl x = {}

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> well_constrained x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
trms_ecl x = {}
[PROOF STEP]
show "well_constrained x"
[PROOF STATE]
proof (prove)
using this:
trms_ecl x = {}

goal (1 subgoal):
 1. well_constrained x
[PROOF STEP]
unfolding well_constrained_def
[PROOF STATE]
proof (prove)
using this:
trms_ecl x = {}

goal (1 subgoal):
 1. \<forall>y. y \<in> trms_ecl x \<longrightarrow> dom_trm y (cl_ecl x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
well_constrained x

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

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
have "Ball ?S well_constrained"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball {y. derivable_ecl y S} well_constrained
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {y. derivable_ecl y S} \<Longrightarrow> well_constrained x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {y. derivable_ecl y S} \<Longrightarrow> well_constrained x
[PROOF STEP]
assume "x \<in> ?S"
[PROOF STATE]
proof (state)
this:
x \<in> {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<And>x. x \<in> {y. derivable_ecl y S} \<Longrightarrow> well_constrained x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> {y. derivable_ecl y S}
[PROOF STEP]
have "derivable_ecl x S"
[PROOF STATE]
proof (prove)
using this:
x \<in> {y. derivable_ecl y S}

goal (1 subgoal):
 1. derivable_ecl x S
[PROOF STEP]
by (meson CollectD)
[PROOF STATE]
proof (state)
this:
derivable_ecl x S

goal (1 subgoal):
 1. \<And>x. x \<in> {y. derivable_ecl y S} \<Longrightarrow> well_constrained x
[PROOF STEP]
from this assms(2) \<open>Ball S well_constrained\<close>
[PROOF STATE]
proof (chain)
picking this:
derivable_ecl x S
\<forall>x\<in>S. finite (cl_ecl x)
Ball S well_constrained
[PROOF STEP]
show "well_constrained x"
[PROOF STATE]
proof (prove)
using this:
derivable_ecl x S
\<forall>x\<in>S. finite (cl_ecl x)
Ball S well_constrained

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Ball {y. derivable_ecl y S} well_constrained

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
have "closed_under_renaming ?S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_under_renaming {y. derivable_ecl y S}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> closed_under_renaming {y. derivable_ecl y S} \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> closed_under_renaming {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<not> closed_under_renaming {y. derivable_ecl y S} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> closed_under_renaming {y. derivable_ecl y S}
[PROOF STEP]
obtain C D  where "C \<in> ?S" "renaming_cl C D" "D \<notin> ?S"
[PROOF STATE]
proof (prove)
using this:
\<not> closed_under_renaming {y. derivable_ecl y S}

goal (1 subgoal):
 1. (\<And>C D. \<lbrakk>C \<in> {y. derivable_ecl y S}; renaming_cl C D; D \<notin> {y. derivable_ecl y S}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding closed_under_renaming_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>C D. C \<in> {y. derivable_ecl y S} \<longrightarrow> renaming_cl C D \<longrightarrow> D \<in> {y. derivable_ecl y S})

goal (1 subgoal):
 1. (\<And>C D. \<lbrakk>C \<in> {y. derivable_ecl y S}; renaming_cl C D; D \<notin> {y. derivable_ecl y S}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
C \<in> {y. derivable_ecl y S}
renaming_cl C D
D \<notin> {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<not> closed_under_renaming {y. derivable_ecl y S} \<Longrightarrow> False
[PROOF STEP]
from \<open>C \<in> ?S\<close>
[PROOF STATE]
proof (chain)
picking this:
C \<in> {y. derivable_ecl y S}
[PROOF STEP]
have "derivable_ecl C S"
[PROOF STATE]
proof (prove)
using this:
C \<in> {y. derivable_ecl y S}

goal (1 subgoal):
 1. derivable_ecl C S
[PROOF STEP]
by (meson CollectD)
[PROOF STATE]
proof (state)
this:
derivable_ecl C S

goal (1 subgoal):
 1. \<not> closed_under_renaming {y. derivable_ecl y S} \<Longrightarrow> False
[PROOF STEP]
from \<open>derivable_ecl C S\<close> \<open>renaming_cl C D\<close>
[PROOF STATE]
proof (chain)
picking this:
derivable_ecl C S
renaming_cl C D
[PROOF STEP]
have "(derivable_ecl D S)"
[PROOF STATE]
proof (prove)
using this:
derivable_ecl C S
renaming_cl C D

goal (1 subgoal):
 1. derivable_ecl D S
[PROOF STEP]
using derivable_ecl.intros(2)
[PROOF STATE]
proof (prove)
using this:
derivable_ecl C S
renaming_cl C D
\<lbrakk>derivable_ecl ?C ?S; renaming_cl ?C ?D\<rbrakk> \<Longrightarrow> derivable_ecl ?D ?S

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

goal (1 subgoal):
 1. \<not> closed_under_renaming {y. derivable_ecl y S} \<Longrightarrow> False
[PROOF STEP]
from this and \<open>D \<notin> ?S\<close>
[PROOF STATE]
proof (chain)
picking this:
derivable_ecl D S
D \<notin> {y. derivable_ecl y S}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
derivable_ecl D S
D \<notin> {y. derivable_ecl y S}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
closed_under_renaming {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
have "inference_closed ?S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inference_closed {y. derivable_ecl y S}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> inference_closed {y. derivable_ecl y S} \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> inference_closed {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<not> inference_closed {y. derivable_ecl y S} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> inference_closed {y. derivable_ecl y S}
[PROOF STEP]
obtain D P \<theta> C' where "(derivable D P ?S \<theta> FirstOrder C')" "D \<notin> ?S"
[PROOF STATE]
proof (prove)
using this:
\<not> inference_closed {y. derivable_ecl y S}

goal (1 subgoal):
 1. (\<And>D P \<theta> C'. \<lbrakk>derivable D P {y. derivable_ecl y S} \<theta> FirstOrder C'; D \<notin> {y. derivable_ecl y S}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding inference_closed_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>P C' D \<theta>. derivable D P {y. derivable_ecl y S} \<theta> FirstOrder C' \<longrightarrow> D \<in> {y. derivable_ecl y S})

goal (1 subgoal):
 1. (\<And>D P \<theta> C'. \<lbrakk>derivable D P {y. derivable_ecl y S} \<theta> FirstOrder C'; D \<notin> {y. derivable_ecl y S}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
derivable D P {y. derivable_ecl y S} \<theta> FirstOrder C'
D \<notin> {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<not> inference_closed {y. derivable_ecl y S} \<Longrightarrow> False
[PROOF STEP]
from \<open>derivable D P ?S \<theta> FirstOrder C'\<close>
[PROOF STATE]
proof (chain)
picking this:
derivable D P {y. derivable_ecl y S} \<theta> FirstOrder C'
[PROOF STEP]
have "P \<subseteq> ?S"
[PROOF STATE]
proof (prove)
using this:
derivable D P {y. derivable_ecl y S} \<theta> FirstOrder C'

goal (1 subgoal):
 1. P \<subseteq> {y. derivable_ecl y S}
[PROOF STEP]
using derivable_premisses
[PROOF STATE]
proof (prove)
using this:
derivable D P {y. derivable_ecl y S} \<theta> FirstOrder C'
derivable ?C ?P ?S ?\<sigma> ?k ?C' \<Longrightarrow> ?P \<subseteq> ?S

goal (1 subgoal):
 1. P \<subseteq> {y. derivable_ecl y S}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P \<subseteq> {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<not> inference_closed {y. derivable_ecl y S} \<Longrightarrow> False
[PROOF STEP]
have "\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S
[PROOF STEP]
proof ((rule allI),(rule impI))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> derivable_ecl x S
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> derivable_ecl x S
[PROOF STEP]
assume "x \<in> P"
[PROOF STATE]
proof (state)
this:
x \<in> P

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> derivable_ecl x S
[PROOF STEP]
from this and \<open>P \<subseteq> ?S\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> P
P \<subseteq> {y. derivable_ecl y S}
[PROOF STEP]
have "x \<in> ?S"
[PROOF STATE]
proof (prove)
using this:
x \<in> P
P \<subseteq> {y. derivable_ecl y S}

goal (1 subgoal):
 1. x \<in> {y. derivable_ecl y S}
[PROOF STEP]
by (meson rev_subsetD)
[PROOF STATE]
proof (state)
this:
x \<in> {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> derivable_ecl x S
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> {y. derivable_ecl y S}
[PROOF STEP]
show "derivable_ecl x S"
[PROOF STATE]
proof (prove)
using this:
x \<in> {y. derivable_ecl y S}

goal (1 subgoal):
 1. derivable_ecl x S
[PROOF STEP]
by (meson CollectD)
[PROOF STATE]
proof (state)
this:
derivable_ecl x S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S

goal (1 subgoal):
 1. \<not> inference_closed {y. derivable_ecl y S} \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(derivable D P ?S \<theta> FirstOrder C')\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S
derivable D P {y. derivable_ecl y S} \<theta> FirstOrder C'
[PROOF STEP]
have "derivable_ecl D S"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S
derivable D P {y. derivable_ecl y S} \<theta> FirstOrder C'

goal (1 subgoal):
 1. derivable_ecl D S
[PROOF STEP]
using derivable_ecl.intros(3) [of P S D ?S \<theta> C']
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S
derivable D P {y. derivable_ecl y S} \<theta> FirstOrder C'
\<lbrakk>\<forall>x. x \<in> P \<longrightarrow> derivable_ecl x S; derivable D P {y. derivable_ecl y S} \<theta> FirstOrder C'\<rbrakk> \<Longrightarrow> derivable_ecl D S

goal (1 subgoal):
 1. derivable_ecl D S
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
derivable_ecl D S

goal (1 subgoal):
 1. \<not> inference_closed {y. derivable_ecl y S} \<Longrightarrow> False
[PROOF STEP]
from this and \<open>D \<notin> ?S\<close>
[PROOF STATE]
proof (chain)
picking this:
derivable_ecl D S
D \<notin> {y. derivable_ecl y S}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
derivable_ecl D S
D \<notin> {y. derivable_ecl y S}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inference_closed {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
from this all_finite
[PROOF STATE]
proof (chain)
picking this:
inference_closed {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)
[PROOF STEP]
have "clause_saturated ?S"
[PROOF STATE]
proof (prove)
using this:
inference_closed {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)

goal (1 subgoal):
 1. clause_saturated {y. derivable_ecl y S}
[PROOF STEP]
using inference_closed_sets_are_saturated
[PROOF STATE]
proof (prove)
using this:
inference_closed {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)
\<lbrakk>inference_closed ?S; \<forall>x\<in>?S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> clause_saturated ?S

goal (1 subgoal):
 1. clause_saturated {y. derivable_ecl y S}
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
clause_saturated {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
from this all_finite
[PROOF STATE]
proof (chain)
picking this:
clause_saturated {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)
[PROOF STEP]
have "inference_saturated ?S"
[PROOF STATE]
proof (prove)
using this:
clause_saturated {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)

goal (1 subgoal):
 1. inference_saturated {y. derivable_ecl y S}
[PROOF STEP]
using clause_saturated_and_inference_saturated
[PROOF STATE]
proof (prove)
using this:
clause_saturated {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)
\<lbrakk>clause_saturated ?S; \<forall>x\<in>?S. finite (cl_ecl x)\<rbrakk> \<Longrightarrow> inference_saturated ?S

goal (1 subgoal):
 1. inference_saturated {y. derivable_ecl y S}
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
inference_saturated {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
inference_saturated {y. derivable_ecl y S}
[PROOF STEP]
have "ground_inference_saturated ?S"
[PROOF STATE]
proof (prove)
using this:
inference_saturated {y. derivable_ecl y S}

goal (1 subgoal):
 1. ground_inference_saturated {y. derivable_ecl y S}
[PROOF STEP]
using lift_inference
[PROOF STATE]
proof (prove)
using this:
inference_saturated {y. derivable_ecl y S}
inference_saturated ?S \<Longrightarrow> ground_inference_saturated ?S

goal (1 subgoal):
 1. ground_inference_saturated {y. derivable_ecl y S}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
ground_inference_saturated {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
have "validate_clause_set ?I (cl_ecl ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S)

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S)
[PROOF STEP]
obtain Cl_C where clc: "Cl_C \<in> (cl_ecl ` S)" and "\<not> (validate_clause ?I Cl_C)"
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S)

goal (1 subgoal):
 1. (\<And>Cl_C. \<lbrakk>Cl_C \<in> cl_ecl ` S; \<not> validate_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) Cl_C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using validate_clause_set.simps
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S)
validate_clause_set ?I ?S = (\<forall>C. C \<in> ?S \<longrightarrow> validate_clause ?I C)

goal (1 subgoal):
 1. (\<And>Cl_C. \<lbrakk>Cl_C \<in> cl_ecl ` S; \<not> validate_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) Cl_C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Cl_C \<in> cl_ecl ` S
\<not> validate_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) Cl_C

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from clc
[PROOF STATE]
proof (chain)
picking this:
Cl_C \<in> cl_ecl ` S
[PROOF STEP]
obtain C where "C \<in> S" and "Cl_C = (cl_ecl C)"
[PROOF STATE]
proof (prove)
using this:
Cl_C \<in> cl_ecl ` S

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>C \<in> S; Cl_C = cl_ecl C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C \<in> S
Cl_C = cl_ecl C

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from \<open>C \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
C \<in> S
[PROOF STEP]
have "derivable_ecl C S"
[PROOF STATE]
proof (prove)
using this:
C \<in> S

goal (1 subgoal):
 1. derivable_ecl C S
[PROOF STEP]
using derivable_ecl.intros(1)
[PROOF STATE]
proof (prove)
using this:
C \<in> S
?C \<in> ?S \<Longrightarrow> derivable_ecl ?C ?S

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

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
derivable_ecl C S
[PROOF STEP]
have "C \<in> ?S"
[PROOF STATE]
proof (prove)
using this:
derivable_ecl C S

goal (1 subgoal):
 1. C \<in> {y. derivable_ecl y S}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C \<in> {y. derivable_ecl y S}

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not> (validate_clause ?I Cl_C)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> validate_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) Cl_C
[PROOF STEP]
obtain \<sigma>
      where "\<not> (validate_ground_clause ?I (subst_cl Cl_C \<sigma>))"
        and "ground_clause (subst_cl Cl_C \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) Cl_C

goal (1 subgoal):
 1. (\<And>\<sigma>. \<lbrakk>\<not> validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl Cl_C \<sigma>); ground_clause (subst_cl Cl_C \<sigma>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using validate_clause.simps
[PROOF STATE]
proof (prove)
using this:
\<not> validate_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) Cl_C
validate_clause ?I ?C = (\<forall>s. ground_clause (subst_cl ?C s) \<longrightarrow> validate_ground_clause ?I (subst_cl ?C s))

goal (1 subgoal):
 1. (\<And>\<sigma>. \<lbrakk>\<not> validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl Cl_C \<sigma>); ground_clause (subst_cl Cl_C \<sigma>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<not> validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl Cl_C \<sigma>)
ground_clause (subst_cl Cl_C \<sigma>)

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
let ?pair = "(C,\<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
have "fst ?pair = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (C, \<sigma>) = C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (C, \<sigma>) = C

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
have "snd ?pair = \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (C, \<sigma>) = \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd (C, \<sigma>) = \<sigma>

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from \<open>C \<in> S\<close> assms(1)
[PROOF STATE]
proof (chain)
picking this:
C \<in> S
\<forall>x. x \<in> S \<longrightarrow> trms_ecl x = {}
[PROOF STEP]
have "trms_ecl C = {}"
[PROOF STATE]
proof (prove)
using this:
C \<in> S
\<forall>x. x \<in> S \<longrightarrow> trms_ecl x = {}

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

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trms_ecl C = {}
[PROOF STEP]
have "(subst_set (trms_ecl C) \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
trms_ecl C = {}

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

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subst_set (trms_ecl C) \<sigma> = {}
[PROOF STEP]
have n: "all_trms_irreducible (subst_set (trms_ecl C) \<sigma>)
                  (\<lambda>t. trm_rep t {y. derivable_ecl y S})"
[PROOF STATE]
proof (prove)
using this:
subst_set (trms_ecl C) \<sigma> = {}

goal (1 subgoal):
 1. all_trms_irreducible (subst_set (trms_ecl C) \<sigma>) (\<lambda>t. trm_rep t {y. derivable_ecl y S})
[PROOF STEP]
unfolding all_trms_irreducible_def
[PROOF STATE]
proof (prove)
using this:
subst_set (trms_ecl C) \<sigma> = {}

goal (1 subgoal):
 1. \<forall>x y. x \<in> subst_set (trms_ecl C) \<sigma> \<longrightarrow> occurs_in y x \<longrightarrow> trm_rep y {y. derivable_ecl y S} = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
all_trms_irreducible (subst_set (trms_ecl C) \<sigma>) (\<lambda>t. trm_rep t {y. derivable_ecl y S})

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from \<open>ground_inference_saturated ?S\<close> all_finite \<open>Ball ?S well_constrained\<close>
      \<open>closed_under_renaming ?S\<close> \<open>\<forall>x \<in> ?S. (cl_ecl x) \<noteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
ground_inference_saturated {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)
Ball {y. derivable_ecl y S} well_constrained
closed_under_renaming {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {}
[PROOF STEP]
have "\<forall>C \<sigma>. fst ?pair = C \<longrightarrow>
           \<sigma> = snd ?pair \<longrightarrow>
           C \<in> {y. derivable_ecl y S} \<longrightarrow>
           ground_clause (subst_cl (cl_ecl C) \<sigma>) \<longrightarrow>
           all_trms_irreducible (subst_set (trms_ecl C) \<sigma>) (\<lambda>t. trm_rep t {y. derivable_ecl y S})
           \<longrightarrow> validate_ground_clause ?I  (subst_cl (cl_ecl C) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
ground_inference_saturated {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)
Ball {y. derivable_ecl y S} well_constrained
closed_under_renaming {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {}

goal (1 subgoal):
 1. \<forall>Ca \<sigma>'. fst (C, \<sigma>) = Ca \<longrightarrow> \<sigma>' = snd (C, \<sigma>) \<longrightarrow> Ca \<in> {y. derivable_ecl y S} \<longrightarrow> ground_clause (subst_cl (cl_ecl Ca) \<sigma>') \<longrightarrow> all_trms_irreducible (subst_set (trms_ecl Ca) \<sigma>') (\<lambda>t. trm_rep t {y. derivable_ecl y S}) \<longrightarrow> validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl (cl_ecl Ca) \<sigma>')
[PROOF STEP]
using int_clset_is_a_model [of ?S ?pair]
[PROOF STATE]
proof (prove)
using this:
ground_inference_saturated {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x)
Ball {y. derivable_ecl y S} well_constrained
closed_under_renaming {y. derivable_ecl y S}
\<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {}
\<lbrakk>ground_inference_saturated {y. derivable_ecl y S}; \<forall>x\<in>{y. derivable_ecl y S}. finite (cl_ecl x); Ball {y. derivable_ecl y S} well_constrained; \<forall>x\<in>{y. derivable_ecl y S}. cl_ecl x \<noteq> {}; closed_under_renaming {y. derivable_ecl y S}\<rbrakk> \<Longrightarrow> \<forall>Ca \<sigma>'. fst (C, \<sigma>) = Ca \<longrightarrow> \<sigma>' = snd (C, \<sigma>) \<longrightarrow> Ca \<in> {y. derivable_ecl y S} \<longrightarrow> ground_clause (subst_cl (cl_ecl Ca) \<sigma>') \<longrightarrow> all_trms_irreducible (subst_set (trms_ecl Ca) \<sigma>') (\<lambda>t. trm_rep t {y. derivable_ecl y S}) \<longrightarrow> validate_ground_clause (same_values (\<lambda>t. trm_rep t {y. derivable_ecl y S})) (subst_cl (cl_ecl Ca) \<sigma>')

goal (1 subgoal):
 1. \<forall>Ca \<sigma>'. fst (C, \<sigma>) = Ca \<longrightarrow> \<sigma>' = snd (C, \<sigma>) \<longrightarrow> Ca \<in> {y. derivable_ecl y S} \<longrightarrow> ground_clause (subst_cl (cl_ecl Ca) \<sigma>') \<longrightarrow> all_trms_irreducible (subst_set (trms_ecl Ca) \<sigma>') (\<lambda>t. trm_rep t {y. derivable_ecl y S}) \<longrightarrow> validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl (cl_ecl Ca) \<sigma>')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>Ca \<sigma>'. fst (C, \<sigma>) = Ca \<longrightarrow> \<sigma>' = snd (C, \<sigma>) \<longrightarrow> Ca \<in> {y. derivable_ecl y S} \<longrightarrow> ground_clause (subst_cl (cl_ecl Ca) \<sigma>') \<longrightarrow> all_trms_irreducible (subst_set (trms_ecl Ca) \<sigma>') (\<lambda>t. trm_rep t {y. derivable_ecl y S}) \<longrightarrow> validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl (cl_ecl Ca) \<sigma>')

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from this \<open>fst ?pair = C\<close> \<open>C \<in> ?S\<close> \<open>snd ?pair = \<sigma>\<close> \<open>Cl_C = (cl_ecl C)\<close>
        \<open>ground_clause (subst_cl Cl_C \<sigma>)\<close> n
[PROOF STATE]
proof (chain)
picking this:
\<forall>Ca \<sigma>'. fst (C, \<sigma>) = Ca \<longrightarrow> \<sigma>' = snd (C, \<sigma>) \<longrightarrow> Ca \<in> {y. derivable_ecl y S} \<longrightarrow> ground_clause (subst_cl (cl_ecl Ca) \<sigma>') \<longrightarrow> all_trms_irreducible (subst_set (trms_ecl Ca) \<sigma>') (\<lambda>t. trm_rep t {y. derivable_ecl y S}) \<longrightarrow> validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl (cl_ecl Ca) \<sigma>')
fst (C, \<sigma>) = C
C \<in> {y. derivable_ecl y S}
snd (C, \<sigma>) = \<sigma>
Cl_C = cl_ecl C
ground_clause (subst_cl Cl_C \<sigma>)
all_trms_irreducible (subst_set (trms_ecl C) \<sigma>) (\<lambda>t. trm_rep t {y. derivable_ecl y S})
[PROOF STEP]
have "validate_ground_clause ?I  (subst_cl (cl_ecl C) \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<forall>Ca \<sigma>'. fst (C, \<sigma>) = Ca \<longrightarrow> \<sigma>' = snd (C, \<sigma>) \<longrightarrow> Ca \<in> {y. derivable_ecl y S} \<longrightarrow> ground_clause (subst_cl (cl_ecl Ca) \<sigma>') \<longrightarrow> all_trms_irreducible (subst_set (trms_ecl Ca) \<sigma>') (\<lambda>t. trm_rep t {y. derivable_ecl y S}) \<longrightarrow> validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl (cl_ecl Ca) \<sigma>')
fst (C, \<sigma>) = C
C \<in> {y. derivable_ecl y S}
snd (C, \<sigma>) = \<sigma>
Cl_C = cl_ecl C
ground_clause (subst_cl Cl_C \<sigma>)
all_trms_irreducible (subst_set (trms_ecl C) \<sigma>) (\<lambda>t. trm_rep t {y. derivable_ecl y S})

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl (cl_ecl C) \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl (cl_ecl C) \<sigma>)

goal (1 subgoal):
 1. \<not> validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S) \<Longrightarrow> False
[PROOF STEP]
from this and \<open>\<not> (validate_ground_clause ?I (subst_cl Cl_C \<sigma>))\<close> \<open>Cl_C = (cl_ecl C)\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl (cl_ecl C) \<sigma>)
\<not> validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl Cl_C \<sigma>)
Cl_C = cl_ecl C
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl (cl_ecl C) \<sigma>)
\<not> validate_ground_clause (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (subst_cl Cl_C \<sigma>)
Cl_C = cl_ecl C

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:
validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S)

goal (1 subgoal):
 1. \<nexists>x. derivable_ecl x S \<and> cl_ecl x = {} \<Longrightarrow> False
[PROOF STEP]
from this and assms(3) \<open>fo_interpretation ?I\<close>
[PROOF STATE]
proof (chain)
picking this:
validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S)
\<not> satisfiable_clause_set (cl_ecl ` S)
fo_interpretation (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S}))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S)
\<not> satisfiable_clause_set (cl_ecl ` S)
fo_interpretation (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S}))

goal (1 subgoal):
 1. False
[PROOF STEP]
using satisfiable_clause_set_def
[PROOF STATE]
proof (prove)
using this:
validate_clause_set (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S})) (cl_ecl ` S)
\<not> satisfiable_clause_set (cl_ecl ` S)
fo_interpretation (same_values (\<lambda>x. trm_rep x {y. derivable_ecl y S}))
satisfiable_clause_set ?S = (\<exists>I. fo_interpretation I \<and> validate_clause_set I ?S)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Frame_deterministic[rule_format]:
"(ops, par, S, os) \<in> Frame \<Longrightarrow>
(\<forall> R opsa . (ops, par, R, opsa) \<in> Frame \<longrightarrow> R=S \<and> opsa = os)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ops, par, S, os) \<in> Frame \<Longrightarrow> \<forall>R opsa. (ops, par, R, opsa) \<in> Frame \<longrightarrow> R = S \<and> opsa = os
[PROOF STEP]
apply (erule Frame.induct, clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>oo R opsa. (oo, [], R, opsa) \<in> Frame \<Longrightarrow> R = emp \<and> opsa = oo
 2. \<And>oo par S ops R x v. \<lbrakk>(oo, par, S, ops) \<in> Frame; \<forall>R opsa. (oo, par, R, opsa) \<in> Frame \<longrightarrow> R = S \<and> opsa = ops; R = S[x\<mapsto>v]\<rbrakk> \<Longrightarrow> \<forall>Ra opsa. (v # oo, x # par, Ra, opsa) \<in> Frame \<longrightarrow> Ra = R \<and> opsa = ops
[PROOF STEP]
apply (erule Frame.cases, clarsimp, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>oo par S ops R x v. \<lbrakk>(oo, par, S, ops) \<in> Frame; \<forall>R opsa. (oo, par, R, opsa) \<in> Frame \<longrightarrow> R = S \<and> opsa = ops; R = S[x\<mapsto>v]\<rbrakk> \<Longrightarrow> \<forall>Ra opsa. (v # oo, x # par, Ra, opsa) \<in> Frame \<longrightarrow> Ra = R \<and> opsa = ops
[PROOF STEP]
apply (erule thin_rl, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>oo par S ops x v Ra opsa. \<lbrakk>\<forall>R opsa. (oo, par, R, opsa) \<in> Frame \<longrightarrow> R = S \<and> opsa = ops; (v # oo, x # par, Ra, opsa) \<in> Frame\<rbrakk> \<Longrightarrow> Ra = S[x\<mapsto>v] \<and> opsa = ops
[PROOF STEP]
apply (erule Frame.cases, clarsimp, clarsimp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma no_zero_height_derivsAux[rule_format]:
"\<forall>n . ((M,l,s,n,ll,t) : Step \<longrightarrow> (n=0 \<longrightarrow> False)) \<and> ((MM,lll,ss,m,h,v):Exec \<longrightarrow> (m=0 \<longrightarrow> False))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. ((M, l, s, n, ll, t) \<in> Step \<longrightarrow> n = 0 \<longrightarrow> False) \<and> ((MM, lll, ss, m, h, v) \<in> Exec \<longrightarrow> m = 0 \<longrightarrow> False)
[PROOF STEP]
by (rule allI, rule Step_Exec.induct, simp_all)


[STATEMENT]
lemma no_zero_height_derivsAux2: "((M,l,s,0,ll,t):Step \<longrightarrow> False) \<and> ((MM,lll,ss,0,h,v):Exec \<longrightarrow> False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((M, l, s, 0, ll, t) \<in> Step \<longrightarrow> False) \<and> ((MM, lll, ss, 0, h, v) \<in> Exec \<longrightarrow> False)
[PROOF STEP]
by (insert no_zero_height_derivsAux, fast)


[STATEMENT]
lemma no_zero_height_Step_derivs: "(M,l,s,0,ll,t):Step \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, 0, ll, t) \<in> Step \<Longrightarrow> False
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, 0, ll, t) \<in> Step \<Longrightarrow> False
[PROOF STEP]
by (insert no_zero_height_derivsAux2, fast)


[STATEMENT]
lemma no_zero_height_Step_derivs1: "(M,l,(os,S,H),0,ll,t):Step \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, (os, S, H), 0, ll, t) \<in> Step \<Longrightarrow> False
[PROOF STEP]
by (insert no_zero_height_derivsAux2, fast)


[STATEMENT]
lemma no_zero_height_Exec_derivs: "(M,l,s,0,h,v):Exec \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, 0, h, v) \<in> Exec \<Longrightarrow> False
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, 0, h, v) \<in> Exec \<Longrightarrow> False
[PROOF STEP]
by (insert no_zero_height_derivsAux2, fast)


[STATEMENT]
lemma no_zero_height_Exec_derivs1: "(M,l,(os,S,H),0,h,v):Exec \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, (os, S, H), 0, h, v) \<in> Exec \<Longrightarrow> False
[PROOF STEP]
by (insert no_zero_height_derivsAux2, fast)


[STATEMENT]
lemma ConstElim1:"\<lbrakk>(M, l, (os, S, h), n, ll,t) \<in> Step; get_ins M l = Some (const v)\<rbrakk>
               \<Longrightarrow> n = Suc 0 \<and> t = (v # os, S, h) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (const v)\<rbrakk> \<Longrightarrow> n = Suc 0 \<and> t = (v # os, S, h) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma DupElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l =  Some dup\<rbrakk>
               \<Longrightarrow> \<exists> v ops . os = v # ops \<and> n = Suc 0 \<and> t = (v # os, S, h) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some dup\<rbrakk> \<Longrightarrow> \<exists>v ops. os = v # ops \<and> n = Suc 0 \<and> t = (v # os, S, h) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma PopElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l =  Some pop\<rbrakk>
               \<Longrightarrow> \<exists> v ops . os = v # ops \<and> n = Suc 0 \<and> t = (ops, S, h) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some pop\<rbrakk> \<Longrightarrow> \<exists>v ops. os = v # ops \<and> n = Suc 0 \<and> t = (ops, S, h) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma SwapElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some swap\<rbrakk>
              \<Longrightarrow> \<exists> v w ops . os = v # w # ops \<and> n = Suc 0 \<and> t = (w # v # ops, S, h) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some swap\<rbrakk> \<Longrightarrow> \<exists>v w ops. os = v # w # ops \<and> n = Suc 0 \<and> t = (w # v # ops, S, h) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma LoadElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (load x)\<rbrakk>
                 \<Longrightarrow> \<exists> v . S\<down>x = Some v \<and> n = Suc 0 \<and> t = (v # os, S, h) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (load x)\<rbrakk> \<Longrightarrow> \<exists>v. S\<down>x = Some v \<and> n = Suc 0 \<and> t = (v # os, S, h) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma StoreElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (store x)\<rbrakk>
                  \<Longrightarrow> \<exists> v ops . os = v # ops \<and> n = Suc 0 \<and> t = (ops, S[x\<mapsto>v], h) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (store x)\<rbrakk> \<Longrightarrow> \<exists>v ops. os = v # ops \<and> n = Suc 0 \<and> t = (ops, S[x\<mapsto>v], h) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma BinopElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (binop f)\<rbrakk>
                  \<Longrightarrow> \<exists> v w ops . os = v # w # ops \<and> n = Suc 0 \<and> t = (f v w # ops, S, h) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (binop f)\<rbrakk> \<Longrightarrow> \<exists>v w ops. os = v # w # ops \<and> n = Suc 0 \<and> t = (f v w # ops, S, h) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma UnopElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (unop f)\<rbrakk>
                 \<Longrightarrow> \<exists> v ops . os = v # ops \<and> n = Suc 0 \<and> t = (f v # ops, S, h) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (unop f)\<rbrakk> \<Longrightarrow> \<exists>v ops. os = v # ops \<and> n = Suc 0 \<and> t = (f v # ops, S, h) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma NewElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (new d)\<rbrakk>
               \<Longrightarrow> \<exists> a . a = nextLoc h \<and> n = Suc 0 \<and> t = (RVal (Loc a) # os, S, h[a\<mapsto>(d, emp)]) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (new d)\<rbrakk> \<Longrightarrow> \<exists>a. a = nextLoc h \<and> n = Suc 0 \<and> t = (RVal (Loc a) # os, S, h[a\<mapsto>(d, emp)]) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma GetElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (getfield d F)\<rbrakk>
               \<Longrightarrow> \<exists> a Flds v ops. h\<down>a = Some (d, Flds) \<and> Flds\<down>F = Some v \<and>
                                   os = RVal (Loc a) # ops \<and> n = Suc 0 \<and> t = (v # ops, S, h) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (getfield d F)\<rbrakk> \<Longrightarrow> \<exists>a Flds v ops. h\<down>a = Some (d, Flds) \<and> Flds\<down>F = Some v \<and> os = RVal (Loc a) # ops \<and> n = Suc 0 \<and> t = (v # ops, S, h) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma PutElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (putfield d F)\<rbrakk>
                \<Longrightarrow> \<exists> a Flds v ops. h\<down>a = Some (d, Flds) \<and> os = v # RVal (Loc a) # ops \<and>
                                   n = Suc 0 \<and> t = (ops, S, h[a\<mapsto>(d, Flds[F\<mapsto>v])]) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (putfield d F)\<rbrakk> \<Longrightarrow> \<exists>a Flds v ops. h\<down>a = Some (d, Flds) \<and> os = v # RVal (Loc a) # ops \<and> n = Suc 0 \<and> t = (ops, S, h[a\<mapsto>(d, Flds[F\<mapsto>v])]) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma CastElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (checkcast d)\<rbrakk>
                \<Longrightarrow> \<exists> a Flds ops . h\<down>a = Some (d, Flds) \<and> os = RVal (Loc a) # ops \<and> n = Suc 0 \<and>
                                   t = (RVal (Loc a) # ops, S, h) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (checkcast d)\<rbrakk> \<Longrightarrow> \<exists>a Flds ops. h\<down>a = Some (d, Flds) \<and> os = RVal (Loc a) # ops \<and> n = Suc 0 \<and> t = (RVal (Loc a) # ops, S, h) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma GotoElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (goto pc)\<rbrakk>
                \<Longrightarrow> n = Suc 0 \<and> t = (os, S, h) \<and> ll = pc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (goto pc)\<rbrakk> \<Longrightarrow> n = Suc 0 \<and> t = (os, S, h) \<and> ll = pc
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma IfElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (iftrue pc)\<rbrakk>
              \<Longrightarrow> (\<exists> ops . os = TRUE # ops \<and> n = Suc 0 \<and> t = (ops, S, h) \<and> ll = pc) \<or>
                  (\<exists> v ops . v \<noteq> TRUE \<and> os = v # ops \<and> n = Suc 0 \<and> t = (ops, S, h) \<and> ll = l+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (iftrue pc)\<rbrakk> \<Longrightarrow> (\<exists>ops. os = TRUE # ops \<and> n = Suc 0 \<and> t = (ops, S, h) \<and> ll = pc) \<or> (\<exists>v ops. v \<noteq> TRUE \<and> os = v # ops \<and> n = Suc 0 \<and> t = (ops, S, h) \<and> ll = l + 1)
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma InvokeElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (invokeS C m)\<rbrakk>
                   \<Longrightarrow> \<exists> code l0 v ops hh u k R par.
                           mbody_is C m (par,code, l0) \<and> (os,par,R,ops):Frame \<and>
                           ((par,code,l0), l0, ([], R, h), k, hh, v) \<in> Exec \<and>
                           n = Suc k \<and> t = (v # ops, S, hh) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (invokeS C m)\<rbrakk> \<Longrightarrow> \<exists>code l0 v ops hh u k R par. mbody_is C m (par, code, l0) \<and> (os, par, R, ops) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), k, hh, v) \<in> Exec \<and> n = Suc k \<and> t = (v # ops, S, hh) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all, fastforce)


[STATEMENT]
lemma InvokeElim: "\<lbrakk>(M, l, s, n, ll, t) \<in> Step; get_ins M l = Some (invokeS C m)\<rbrakk>
                   \<Longrightarrow> \<exists> code l0 v ops hh u k R par.
                           mbody_is C m (par,code, l0) \<and> (fst s,par,R,ops):Frame \<and>
                           ((par,code,l0), l0, ([], R, snd(snd s)), k, hh, v) \<in> Exec \<and>
                           n = Suc k \<and> t = (v # ops, fst (snd s), hh) \<and> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, ll, t) \<in> Step; get_ins M l = Some (invokeS C m)\<rbrakk> \<Longrightarrow> \<exists>code l0 v ops hh u k R par. mbody_is C m (par, code, l0) \<and> (fst s, par, R, ops) \<in> Frame \<and> ((par, code, l0), l0, ([], R, snd (snd s)), k, hh, v) \<in> Exec \<and> n = Suc k \<and> t = (v # ops, fst (snd s), hh) \<and> ll = l + 1
[PROOF STEP]
by (erule eval_cases, simp_all, fastforce)


[STATEMENT]
lemma RetElim1: "\<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some (vreturn)\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, (os, S, h), n, ll, t) \<in> Step; get_ins M l = Some vreturn\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (erule eval_cases, simp_all)


[STATEMENT]
lemma ExecElim1: "\<lbrakk>(M,l,(os,S,H),k,h,v):Exec\<rbrakk>
      \<Longrightarrow> (get_ins M l = Some vreturn \<and> (\<exists> ops . os = v # ops \<and> k = Suc 0 \<and> h=H)) \<or>
          (\<exists> n m t ll. (M, l,(os,S,H), n, ll,t) \<in> Step \<and> (M, ll, t, m, h, v) \<in> Exec \<and> k = Suc (max n m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, (os, S, H), k, h, v) \<in> Exec \<Longrightarrow> get_ins M l = Some vreturn \<and> (\<exists>ops. os = v # ops \<and> k = Suc 0 \<and> h = H) \<or> (\<exists>n m t ll. (M, l, (os, S, H), n, ll, t) \<in> Step \<and> (M, ll, t, m, h, v) \<in> Exec \<and> k = Suc (max n m))
[PROOF STEP]
apply (erule eval_cases, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n ll t m. \<lbrakk>k = Suc (max n m); (M, l, (os, S, H), n, ll, t) \<in> Step; (M, ll, t, m, h, v) \<in> Exec\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<and> (\<exists>ops. os = v # ops) \<and> n = 0 \<and> m = 0 \<and> h = H \<or> (\<exists>na ma a aa b ll. (M, l, (os, S, H), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), ma, h, v) \<in> Exec \<and> max n m = max na ma)
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n ll t m. \<lbrakk>k = Suc (max n m); (M, l, (os, S, H), n, ll, t) \<in> Step; (M, ll, t, m, h, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>na ma a aa b ll. (M, l, (os, S, H), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), ma, h, v) \<in> Exec \<and> max n m = max na ma
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n ll a aa b m. \<lbrakk>k = Suc (max n m); (M, l, (os, S, H), n, ll, a, aa, b) \<in> Step; (M, ll, (a, aa, b), m, h, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>na ma a aa b ll. (M, l, (os, S, H), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), ma, h, v) \<in> Exec \<and> max n m = max na ma
[PROOF STEP]
apply (rule, rule, rule, rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n ll a aa b m. \<lbrakk>k = Suc (max n m); (M, l, (os, S, H), n, ll, a, aa, b) \<in> Step; (M, ll, (a, aa, b), m, h, v) \<in> Exec\<rbrakk> \<Longrightarrow> \<exists>ba lla. (M, l, (os, S, H), ?n6 n ll a aa b m, lla, ?a10 n ll a aa b m, ?a12 n ll a aa b m, ba) \<in> Step \<and> (M, lla, (?a10 n ll a aa b m, ?a12 n ll a aa b m, ba), ?m8 n ll a aa b m, h, v) \<in> Exec \<and> max n m = max (?n6 n ll a aa b m) (?m8 n ll a aa b m)
[PROOF STEP]
apply (rule, rule, rule)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n ll a aa b m. \<lbrakk>k = Suc (max n m); (M, l, (os, S, H), n, ll, a, aa, b) \<in> Step; (M, ll, (a, aa, b), m, h, v) \<in> Exec\<rbrakk> \<Longrightarrow> (M, l, (os, S, H), ?n6 n ll a aa b m, ?ll16 n ll a aa b m, ?a10 n ll a aa b m, ?a12 n ll a aa b m, ?b14 n ll a aa b m) \<in> Step
 2. \<And>n ll a aa b m. \<lbrakk>k = Suc (max n m); (M, l, (os, S, H), n, ll, a, aa, b) \<in> Step; (M, ll, (a, aa, b), m, h, v) \<in> Exec\<rbrakk> \<Longrightarrow> (M, ?ll16 n ll a aa b m, (?a10 n ll a aa b m, ?a12 n ll a aa b m, ?b14 n ll a aa b m), ?m8 n ll a aa b m, h, v) \<in> Exec \<and> max n m = max (?n6 n ll a aa b m) (?m8 n ll a aa b m)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n ll a aa b m. \<lbrakk>k = Suc (max n m); (M, l, (os, S, H), n, ll, a, aa, b) \<in> Step; (M, ll, (a, aa, b), m, h, v) \<in> Exec\<rbrakk> \<Longrightarrow> (M, ll, (a, aa, b), ?m8 n ll a aa b m, h, v) \<in> Exec \<and> max n m = max n (?m8 n ll a aa b m)
[PROOF STEP]
apply (rule, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n ll a aa b m. \<lbrakk>k = Suc (max n m); (M, l, (os, S, H), n, ll, a, aa, b) \<in> Step; (M, ll, (a, aa, b), m, h, v) \<in> Exec\<rbrakk> \<Longrightarrow> max n m = max n m
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma InstrElimNext:
 "\<lbrakk>(M, l, s, n, ll, t) \<in> Step;
   get_ins M l = Some I;
   I = const c \<or> I = dup \<or> I = pop \<or> I = swap \<or> I = load x \<or>
   I = store x \<or> I = binop f \<or> I = unop g \<or> I = new d \<or>
   I = getfield d F \<or> I = putfield d F \<or> I = checkcast d\<rbrakk>
  \<Longrightarrow> ll = l+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, ll, t) \<in> Step; get_ins M l = Some I; I = const c \<or> I = dup \<or> I = pop \<or> I = swap \<or> I = load x \<or> I = store x \<or> I = binop f \<or> I = unop g \<or> I = new d \<or> I = getfield d F \<or> I = putfield d F \<or> I = checkcast d\<rbrakk> \<Longrightarrow> ll = l + 1
[PROOF STEP]
apply (drule eval_cases, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>goto ll = I; I = const c \<or> I = dup \<or> I = pop \<or> I = swap \<or> I = load x \<or> I = store x \<or> I = binop f \<or> I = unop g \<or> I = new d \<or> I = getfield d F \<or> I = putfield d F \<or> I = checkcast d; n = Suc 0; t = s; get_ins M l = Some I\<rbrakk> \<Longrightarrow> ll = l + 1
 2. \<And>os sa h. \<lbrakk>iftrue ll = I; I = const c \<or> I = dup \<or> I = pop \<or> I = swap \<or> I = load x \<or> I = store x \<or> I = binop f \<or> I = unop g \<or> I = new d \<or> I = getfield d F \<or> I = putfield d F \<or> I = checkcast d; s = (TRUE # os, sa, h); n = Suc 0; t = (os, sa, h); get_ins M l = Some I\<rbrakk> \<Longrightarrow> ll = l + 1
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>os sa h. \<lbrakk>iftrue ll = I; I = const c \<or> I = dup \<or> I = pop \<or> I = swap \<or> I = load x \<or> I = store x \<or> I = binop f \<or> I = unop g \<or> I = new d \<or> I = getfield d F \<or> I = putfield d F \<or> I = checkcast d; s = (TRUE # os, sa, h); n = Suc 0; t = (os, sa, h); get_ins M l = Some I\<rbrakk> \<Longrightarrow> ll = l + 1
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done