[STATEMENT]
lemma EVAL'_I: 
  "(\<And>I. finite (adom I) \<Longrightarrow> eval Qinf I = {} \<Longrightarrow> eval_on (fv Q) Qfin I = eval Q I) \<Longrightarrow>
   (\<And>I. finite (adom I) \<Longrightarrow> eval Qinf I \<noteq> {} \<Longrightarrow> infinite (eval Q I)) \<Longrightarrow> EVAL' Q Qfin Qinf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>I. \<lbrakk>finite (adom I); eval Qinf I = {}\<rbrakk> \<Longrightarrow> eval_on (fv Q) Qfin I = eval Q I; \<And>I. \<lbrakk>finite (adom I); eval Qinf I \<noteq> {}\<rbrakk> \<Longrightarrow> infinite (eval Q I)\<rbrakk> \<Longrightarrow> EVAL' Q Qfin Qinf
[PROOF STEP]
unfolding EVAL'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>I. \<lbrakk>finite (adom I); eval Qinf I = {}\<rbrakk> \<Longrightarrow> eval_on (fv Q) Qfin I = eval Q I; \<And>I. \<lbrakk>finite (adom I); eval Qinf I \<noteq> {}\<rbrakk> \<Longrightarrow> infinite (eval Q I)\<rbrakk> \<Longrightarrow> \<forall>I. finite (adom I) \<longrightarrow> (if eval Qinf I = {} then eval_on (fv Q) Qfin I = eval Q I else infinite (eval Q I))
[PROOF STEP]
by auto