[STATEMENT]
theorem hintikka_model:
  assumes hin: \<open>hintikka H\<close>
  shows \<open>(p \<in> H \<longrightarrow> closed 0 p \<longrightarrow>
    eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) p) \<and>
  (Neg p \<in> H \<longrightarrow> closed 0 p \<longrightarrow>
    eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg p))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<in> H \<longrightarrow> closed 0 p \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) p) \<and> (Neg p \<in> H \<longrightarrow> closed 0 p \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg p))
[PROOF STEP]
proof (induct p rule: wf_induct [where r=\<open>measure size_form\<close>])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wf (measure FOL_Fitting.size_form)
 2. \<And>x. \<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y)) \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
show \<open>wf (measure size_form)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (measure FOL_Fitting.size_form)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wf (measure FOL_Fitting.size_form)

goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y)) \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y)) \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
let ?eval = \<open>eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y)) \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y)) \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
assume wf: \<open>\<forall>y. (y, x) \<in> measure size_form \<longrightarrow>
                  (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> ?eval y) \<and>
              (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> ?eval (Neg y))\<close>
[PROOF STATE]
proof (state)
this:
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))

goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y)) \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
show \<open>(x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> ?eval x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> ?eval (Neg x))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
proof (cases x)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. x = FF \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. x = TT \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x31 x32. x = Pred x31 x32 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 6. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 7. \<And>x7. x = Neg x7 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 8. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 9. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
case FF
[PROOF STATE]
proof (state)
this:
x = FF

goal (9 subgoals):
 1. x = FF \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. x = TT \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x31 x32. x = Pred x31 x32 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 6. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 7. \<And>x7. x = Neg x7 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 8. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 9. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
proof (intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>x \<in> H\<close>
[PROOF STATE]
proof (state)
this:
x \<in> H

goal (2 subgoals):
 1. \<lbrakk>x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> H
[PROOF STEP]
show \<open>?eval x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
using FF hin
[PROOF STATE]
proof (prove)
using this:
x \<in> H
x = FF
hintikka H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
by (simp add: hintikka_def)
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x

goal (1 subgoal):
 1. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>Neg x \<in> H\<close>
[PROOF STATE]
proof (state)
this:
Neg x \<in> H

goal (1 subgoal):
 1. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg x \<in> H
[PROOF STEP]
show \<open>?eval (Neg x)\<close>
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
using FF
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
x = FF

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))

goal (8 subgoals):
 1. x = TT \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x31 x32. x = Pred x31 x32 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 6. \<And>x7. x = Neg x7 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 7. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 8. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. x = TT \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x31 x32. x = Pred x31 x32 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 6. \<And>x7. x = Neg x7 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 7. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 8. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
case TT
[PROOF STATE]
proof (state)
this:
x = TT

goal (8 subgoals):
 1. x = TT \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x31 x32. x = Pred x31 x32 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 6. \<And>x7. x = Neg x7 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 7. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 8. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
proof (intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>x \<in> H\<close>
[PROOF STATE]
proof (state)
this:
x \<in> H

goal (2 subgoals):
 1. \<lbrakk>x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> H
[PROOF STEP]
show \<open>?eval x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
using TT
[PROOF STATE]
proof (prove)
using this:
x \<in> H
x = TT

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x

goal (1 subgoal):
 1. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>Neg x \<in> H\<close>
[PROOF STATE]
proof (state)
this:
Neg x \<in> H

goal (1 subgoal):
 1. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg x \<in> H
[PROOF STEP]
show \<open>?eval (Neg x)\<close>
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
using TT hin
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
x = TT
hintikka H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
by (simp add: hintikka_def)
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))

goal (7 subgoals):
 1. \<And>x31 x32. x = Pred x31 x32 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x7. x = Neg x7 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 6. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 7. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x31 x32. x = Pred x31 x32 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x7. x = Neg x7 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 6. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 7. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
case (Pred p ts)
[PROOF STATE]
proof (state)
this:
x = Pred p ts

goal (7 subgoals):
 1. \<And>x31 x32. x = Pred x31 x32 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x7. x = Neg x7 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 6. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 7. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
proof (intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
x \<in> H
closed 0 x

goal (2 subgoals):
 1. \<lbrakk>x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> H
closed 0 x
[PROOF STEP]
show \<open>?eval x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
using Pred
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x
x = Pred p ts

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x

goal (1 subgoal):
 1. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>Neg x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg x \<in> H
closed 0 x
[PROOF STEP]
have \<open>Neg (Pred p ts) \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. Neg (Pred p ts) \<in> H
[PROOF STEP]
using Pred
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x
x = Pred p ts

goal (1 subgoal):
 1. Neg (Pred p ts) \<in> H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Neg (Pred p ts) \<in> H

goal (1 subgoal):
 1. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Pred p ts) \<in> H
[PROOF STEP]
have \<open>Pred p ts \<notin> H\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Pred p ts) \<in> H

goal (1 subgoal):
 1. Pred p ts \<notin> H
[PROOF STEP]
using hin
[PROOF STATE]
proof (prove)
using this:
Neg (Pred p ts) \<in> H
hintikka H

goal (1 subgoal):
 1. Pred p ts \<notin> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
Neg (Pred p ts) \<in> H
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. Pred p ts \<notin> H
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
Pred p ts \<notin> H

goal (1 subgoal):
 1. \<lbrakk>Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Pred p ts \<notin> H
[PROOF STEP]
show \<open>?eval (Neg x)\<close>
[PROOF STATE]
proof (prove)
using this:
Pred p ts \<notin> H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
using Pred \<open>closed 0 x\<close>
[PROOF STATE]
proof (prove)
using this:
Pred p ts \<notin> H
x = Pred p ts
closed 0 x

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))

goal (6 subgoals):
 1. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x7. x = Neg x7 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 6. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x7. x = Neg x7 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 6. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
case (Neg Z)
[PROOF STATE]
proof (state)
this:
x = Neg Z

goal (6 subgoals):
 1. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x7. x = Neg x7 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 6. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = Neg Z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = Neg Z

goal (1 subgoal):
 1. (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
proof (intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x = Neg Z; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Neg Z; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
x \<in> H
closed 0 x

goal (2 subgoals):
 1. \<lbrakk>x = Neg Z; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Neg Z; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> H
closed 0 x
[PROOF STEP]
show \<open>?eval x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
using Neg wf
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x
x = Neg Z
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x

goal (1 subgoal):
 1. \<lbrakk>x = Neg Z; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x = Neg Z; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>Neg x \<in> H\<close>
[PROOF STATE]
proof (state)
this:
Neg x \<in> H

goal (1 subgoal):
 1. \<lbrakk>x = Neg Z; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg x \<in> H
[PROOF STEP]
have \<open>Z \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H

goal (1 subgoal):
 1. Z \<in> H
[PROOF STEP]
using Neg hin
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
x = Neg Z
hintikka H

goal (1 subgoal):
 1. Z \<in> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
x = Neg Z
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. Z \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Z \<in> H

goal (1 subgoal):
 1. \<lbrakk>x = Neg Z; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Z \<in> H

goal (1 subgoal):
 1. \<lbrakk>x = Neg Z; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
closed 0 x

goal (1 subgoal):
 1. \<lbrakk>x = Neg Z; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closed 0 x
[PROOF STEP]
have \<open>closed 0 Z\<close>
[PROOF STATE]
proof (prove)
using this:
closed 0 x

goal (1 subgoal):
 1. closed 0 Z
[PROOF STEP]
using Neg
[PROOF STATE]
proof (prove)
using this:
closed 0 x
x = Neg Z

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

goal (1 subgoal):
 1. \<lbrakk>x = Neg Z; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Z \<in> H
closed 0 Z
[PROOF STEP]
have \<open>?eval Z\<close>
[PROOF STATE]
proof (prove)
using this:
Z \<in> H
closed 0 Z

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) Z
[PROOF STEP]
using Neg wf
[PROOF STATE]
proof (prove)
using this:
Z \<in> H
closed 0 Z
x = Neg Z
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) Z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) Z

goal (1 subgoal):
 1. \<lbrakk>x = Neg Z; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) Z
[PROOF STEP]
show \<open>?eval (Neg x)\<close>
[PROOF STATE]
proof (prove)
using this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) Z

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
using Neg
[PROOF STATE]
proof (prove)
using this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) Z
x = Neg Z

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))

goal (5 subgoals):
 1. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
case (And A B)
[PROOF STATE]
proof (state)
this:
x = And A B

goal (5 subgoals):
 1. \<And>x41 x42. x = And x41 x42 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 5. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = And A B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = And A B

goal (1 subgoal):
 1. (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
proof (intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x = And A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = And A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
x \<in> H
closed 0 x

goal (2 subgoals):
 1. \<lbrakk>x = And A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = And A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> H
closed 0 x
[PROOF STEP]
have \<open>And A B \<in> H\<close> and \<open>closed 0 (And A B)\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x

goal (1 subgoal):
 1. And A B \<in> H &&& closed 0 (And A B)
[PROOF STEP]
using And
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x
x = And A B

goal (1 subgoal):
 1. And A B \<in> H &&& closed 0 (And A B)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
And A B \<in> H
closed 0 (And A B)

goal (2 subgoals):
 1. \<lbrakk>x = And A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = And A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
And A B \<in> H
closed 0 (And A B)
[PROOF STEP]
have \<open>A \<in> H \<and> B \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
And A B \<in> H
closed 0 (And A B)

goal (1 subgoal):
 1. A \<in> H \<and> B \<in> H
[PROOF STEP]
using And hin
[PROOF STATE]
proof (prove)
using this:
And A B \<in> H
closed 0 (And A B)
x = And A B
hintikka H

goal (1 subgoal):
 1. A \<in> H \<and> B \<in> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
And A B \<in> H
closed 0 (And A B)
x = And A B
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. A \<in> H \<and> B \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<in> H \<and> B \<in> H

goal (2 subgoals):
 1. \<lbrakk>x = And A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = And A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> H \<and> B \<in> H
[PROOF STEP]
show \<open>?eval x\<close>
[PROOF STATE]
proof (prove)
using this:
A \<in> H \<and> B \<in> H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
using And wf \<open>closed 0 (And A B)\<close>
[PROOF STATE]
proof (prove)
using this:
A \<in> H \<and> B \<in> H
x = And A B
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))
closed 0 (And A B)

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x

goal (1 subgoal):
 1. \<lbrakk>x = And A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x = And A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>Neg x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. \<lbrakk>x = And A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg x \<in> H
closed 0 x
[PROOF STEP]
have \<open>Neg (And A B) \<in> H\<close> and \<open>closed 0 (And A B)\<close>
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. Neg (And A B) \<in> H &&& closed 0 (And A B)
[PROOF STEP]
using And
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x
x = And A B

goal (1 subgoal):
 1. Neg (And A B) \<in> H &&& closed 0 (And A B)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
Neg (And A B) \<in> H
closed 0 (And A B)

goal (1 subgoal):
 1. \<lbrakk>x = And A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (And A B) \<in> H
closed 0 (And A B)
[PROOF STEP]
have \<open>Neg A \<in> H \<or> Neg B \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (And A B) \<in> H
closed 0 (And A B)

goal (1 subgoal):
 1. Neg A \<in> H \<or> Neg B \<in> H
[PROOF STEP]
using hin
[PROOF STATE]
proof (prove)
using this:
Neg (And A B) \<in> H
closed 0 (And A B)
hintikka H

goal (1 subgoal):
 1. Neg A \<in> H \<or> Neg B \<in> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
Neg (And A B) \<in> H
closed 0 (And A B)
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. Neg A \<in> H \<or> Neg B \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg A \<in> H \<or> Neg B \<in> H

goal (1 subgoal):
 1. \<lbrakk>x = And A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg A \<in> H \<or> Neg B \<in> H
[PROOF STEP]
show \<open>?eval (Neg x)\<close>
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> H \<or> Neg B \<in> H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
using And wf \<open>closed 0 (And A B)\<close>
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> H \<or> Neg B \<in> H
x = And A B
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))
closed 0 (And A B)

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))

goal (4 subgoals):
 1. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
case (Or A B)
[PROOF STATE]
proof (state)
this:
x = Or A B

goal (4 subgoals):
 1. \<And>x51 x52. x = Or x51 x52 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 4. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = Or A B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = Or A B

goal (1 subgoal):
 1. (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
proof (intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x = Or A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Or A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
x \<in> H
closed 0 x

goal (2 subgoals):
 1. \<lbrakk>x = Or A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Or A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> H
closed 0 x
[PROOF STEP]
have \<open>Or A B \<in> H\<close> and \<open>closed 0 (Or A B)\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x

goal (1 subgoal):
 1. Or A B \<in> H &&& closed 0 (Or A B)
[PROOF STEP]
using Or
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x
x = Or A B

goal (1 subgoal):
 1. Or A B \<in> H &&& closed 0 (Or A B)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
Or A B \<in> H
closed 0 (Or A B)

goal (2 subgoals):
 1. \<lbrakk>x = Or A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Or A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Or A B \<in> H
closed 0 (Or A B)
[PROOF STEP]
have \<open>A \<in> H \<or> B \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
Or A B \<in> H
closed 0 (Or A B)

goal (1 subgoal):
 1. A \<in> H \<or> B \<in> H
[PROOF STEP]
using hin
[PROOF STATE]
proof (prove)
using this:
Or A B \<in> H
closed 0 (Or A B)
hintikka H

goal (1 subgoal):
 1. A \<in> H \<or> B \<in> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
Or A B \<in> H
closed 0 (Or A B)
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. A \<in> H \<or> B \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<in> H \<or> B \<in> H

goal (2 subgoals):
 1. \<lbrakk>x = Or A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Or A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> H \<or> B \<in> H
[PROOF STEP]
show \<open>?eval x\<close>
[PROOF STATE]
proof (prove)
using this:
A \<in> H \<or> B \<in> H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
using Or wf \<open>closed 0 (Or A B)\<close>
[PROOF STATE]
proof (prove)
using this:
A \<in> H \<or> B \<in> H
x = Or A B
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))
closed 0 (Or A B)

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x

goal (1 subgoal):
 1. \<lbrakk>x = Or A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x = Or A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>Neg x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. \<lbrakk>x = Or A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg x \<in> H
closed 0 x
[PROOF STEP]
have \<open>Neg (Or A B) \<in> H\<close> and \<open>closed 0 (Or A B)\<close>
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. Neg (Or A B) \<in> H &&& closed 0 (Or A B)
[PROOF STEP]
using Or
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x
x = Or A B

goal (1 subgoal):
 1. Neg (Or A B) \<in> H &&& closed 0 (Or A B)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
Neg (Or A B) \<in> H
closed 0 (Or A B)

goal (1 subgoal):
 1. \<lbrakk>x = Or A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Or A B) \<in> H
closed 0 (Or A B)
[PROOF STEP]
have \<open>Neg A \<in> H \<and> Neg B \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Or A B) \<in> H
closed 0 (Or A B)

goal (1 subgoal):
 1. Neg A \<in> H \<and> Neg B \<in> H
[PROOF STEP]
using hin
[PROOF STATE]
proof (prove)
using this:
Neg (Or A B) \<in> H
closed 0 (Or A B)
hintikka H

goal (1 subgoal):
 1. Neg A \<in> H \<and> Neg B \<in> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
Neg (Or A B) \<in> H
closed 0 (Or A B)
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. Neg A \<in> H \<and> Neg B \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg A \<in> H \<and> Neg B \<in> H

goal (1 subgoal):
 1. \<lbrakk>x = Or A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg A \<in> H \<and> Neg B \<in> H
[PROOF STEP]
show \<open>?eval (Neg x)\<close>
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> H \<and> Neg B \<in> H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
using Or wf \<open>closed 0 (Or A B)\<close>
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> H \<and> Neg B \<in> H
x = Or A B
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))
closed 0 (Or A B)

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))

goal (3 subgoals):
 1. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
case (Impl A B)
[PROOF STATE]
proof (state)
this:
x = Impl A B

goal (3 subgoals):
 1. \<And>x61 x62. x = Impl x61 x62 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 3. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = Impl A B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = Impl A B

goal (1 subgoal):
 1. (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
proof (intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x = Impl A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Impl A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
x \<in> H
closed 0 x

goal (2 subgoals):
 1. \<lbrakk>x = Impl A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Impl A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> H
closed 0 x
[PROOF STEP]
have \<open>Impl A B \<in> H\<close> and \<open>closed 0 (Impl A B)\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x

goal (1 subgoal):
 1. Impl A B \<in> H &&& closed 0 (Impl A B)
[PROOF STEP]
using Impl
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x
x = Impl A B

goal (1 subgoal):
 1. Impl A B \<in> H &&& closed 0 (Impl A B)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
Impl A B \<in> H
closed 0 (Impl A B)

goal (2 subgoals):
 1. \<lbrakk>x = Impl A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Impl A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Impl A B \<in> H
closed 0 (Impl A B)
[PROOF STEP]
have \<open>Neg A \<in> H \<or> B \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
Impl A B \<in> H
closed 0 (Impl A B)

goal (1 subgoal):
 1. Neg A \<in> H \<or> B \<in> H
[PROOF STEP]
using hin
[PROOF STATE]
proof (prove)
using this:
Impl A B \<in> H
closed 0 (Impl A B)
hintikka H

goal (1 subgoal):
 1. Neg A \<in> H \<or> B \<in> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
Impl A B \<in> H
closed 0 (Impl A B)
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. Neg A \<in> H \<or> B \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg A \<in> H \<or> B \<in> H

goal (2 subgoals):
 1. \<lbrakk>x = Impl A B; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Impl A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg A \<in> H \<or> B \<in> H
[PROOF STEP]
show \<open>?eval x\<close>
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> H \<or> B \<in> H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
using Impl wf \<open>closed 0 (Impl A B)\<close>
[PROOF STATE]
proof (prove)
using this:
Neg A \<in> H \<or> B \<in> H
x = Impl A B
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))
closed 0 (Impl A B)

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x

goal (1 subgoal):
 1. \<lbrakk>x = Impl A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x = Impl A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>Neg x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. \<lbrakk>x = Impl A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg x \<in> H
closed 0 x
[PROOF STEP]
have \<open>Neg (Impl A B) \<in> H\<close> and \<open>closed 0 (Impl A B)\<close>
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. Neg (Impl A B) \<in> H &&& closed 0 (Impl A B)
[PROOF STEP]
using Impl
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x
x = Impl A B

goal (1 subgoal):
 1. Neg (Impl A B) \<in> H &&& closed 0 (Impl A B)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
Neg (Impl A B) \<in> H
closed 0 (Impl A B)

goal (1 subgoal):
 1. \<lbrakk>x = Impl A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Impl A B) \<in> H
closed 0 (Impl A B)
[PROOF STEP]
have \<open>A \<in> H \<and> Neg B \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Impl A B) \<in> H
closed 0 (Impl A B)

goal (1 subgoal):
 1. A \<in> H \<and> Neg B \<in> H
[PROOF STEP]
using hin
[PROOF STATE]
proof (prove)
using this:
Neg (Impl A B) \<in> H
closed 0 (Impl A B)
hintikka H

goal (1 subgoal):
 1. A \<in> H \<and> Neg B \<in> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
Neg (Impl A B) \<in> H
closed 0 (Impl A B)
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. A \<in> H \<and> Neg B \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<in> H \<and> Neg B \<in> H

goal (1 subgoal):
 1. \<lbrakk>x = Impl A B; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> H \<and> Neg B \<in> H
[PROOF STEP]
show \<open>?eval (Neg x)\<close>
[PROOF STATE]
proof (prove)
using this:
A \<in> H \<and> Neg B \<in> H

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
using Impl wf \<open>closed 0 (Impl A B)\<close>
[PROOF STATE]
proof (prove)
using this:
A \<in> H \<and> Neg B \<in> H
x = Impl A B
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))
closed 0 (Impl A B)

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))

goal (2 subgoals):
 1. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
case (Forall P)
[PROOF STATE]
proof (state)
this:
x = Forall P

goal (2 subgoals):
 1. \<And>x8. x = Forall x8 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
 2. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = Forall P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = Forall P

goal (1 subgoal):
 1. (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
proof (intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x = Forall P; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
x \<in> H
closed 0 x

goal (2 subgoals):
 1. \<lbrakk>x = Forall P; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
have \<open>\<forall>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
proof (rule allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
from \<open>x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> H
closed 0 x
[PROOF STEP]
have \<open>Forall P \<in> H\<close> and \<open>closed 0 (Forall P)\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x

goal (1 subgoal):
 1. Forall P \<in> H &&& closed 0 (Forall P)
[PROOF STEP]
using Forall
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x
x = Forall P

goal (1 subgoal):
 1. Forall P \<in> H &&& closed 0 (Forall P)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
Forall P \<in> H
closed 0 (Forall P)

goal (1 subgoal):
 1. \<And>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Forall P \<in> H
closed 0 (Forall P)
[PROOF STEP]
have *: \<open>\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
Forall P \<in> H
closed 0 (Forall P)

goal (1 subgoal):
 1. \<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H
[PROOF STEP]
using hin
[PROOF STATE]
proof (prove)
using this:
Forall P \<in> H
closed 0 (Forall P)
hintikka H

goal (1 subgoal):
 1. \<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
Forall P \<in> H
closed 0 (Forall P)
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. \<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H

goal (1 subgoal):
 1. \<And>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
from \<open>closed 0 (Forall P)\<close>
[PROOF STATE]
proof (chain)
picking this:
closed 0 (Forall P)
[PROOF STEP]
have \<open>closed (Suc 0) P\<close>
[PROOF STATE]
proof (prove)
using this:
closed 0 (Forall P)

goal (1 subgoal):
 1. closed (Suc 0) P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closed (Suc 0) P

goal (1 subgoal):
 1. \<And>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
have \<open>(P[term_of_hterm z/0], Forall P) \<in> measure size_form \<longrightarrow>
              (P[term_of_hterm z/0] \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow>
              ?eval (P[term_of_hterm z/0]))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P[term_of_hterm z/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[term_of_hterm z/0] \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[term_of_hterm z/0])
[PROOF STEP]
using Forall wf
[PROOF STATE]
proof (prove)
using this:
x = Forall P
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))

goal (1 subgoal):
 1. (P[term_of_hterm z/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[term_of_hterm z/0] \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[term_of_hterm z/0])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(P[term_of_hterm z/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[term_of_hterm z/0] \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[term_of_hterm z/0])

goal (1 subgoal):
 1. \<And>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(P[term_of_hterm z/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[term_of_hterm z/0] \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[term_of_hterm z/0])
[PROOF STEP]
show \<open>eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P\<close>
[PROOF STATE]
proof (prove)
using this:
(P[term_of_hterm z/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[term_of_hterm z/0] \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[term_of_hterm z/0])

goal (1 subgoal):
 1. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
using * \<open>Forall P \<in> H\<close> \<open>closed (Suc 0) P\<close>
[PROOF STATE]
proof (prove)
using this:
(P[term_of_hterm z/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[term_of_hterm z/0] \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[term_of_hterm z/0])
\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H
Forall P \<in> H
closed (Suc 0) P

goal (1 subgoal):
 1. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P

goal (2 subgoals):
 1. \<lbrakk>x = Forall P; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
show \<open>?eval x\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
using Forall
[PROOF STATE]
proof (prove)
using this:
\<forall>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
x = Forall P

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x

goal (1 subgoal):
 1. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>Neg x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg x \<in> H
closed 0 x
[PROOF STEP]
have \<open>Neg (Forall P) \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. Neg (Forall P) \<in> H
[PROOF STEP]
using Forall
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x
x = Forall P

goal (1 subgoal):
 1. Neg (Forall P) \<in> H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Neg (Forall P) \<in> H

goal (1 subgoal):
 1. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Forall P) \<in> H
[PROOF STEP]
have \<open>\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) \<in> H

goal (1 subgoal):
 1. \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H
[PROOF STEP]
using Forall hin
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) \<in> H
x = Forall P
hintikka H

goal (1 subgoal):
 1. \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) \<in> H
x = Forall P
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. \<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H

goal (1 subgoal):
 1. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H
[PROOF STEP]
obtain t where *: \<open>closedt 0 t \<and> Neg (P[t/0]) \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H

goal (1 subgoal):
 1. (\<And>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
closedt 0 t \<and> Neg (P[t/0]) \<in> H

goal (1 subgoal):
 1. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closedt 0 t \<and> Neg (P[t/0]) \<in> H
[PROOF STEP]
have \<open>closed 0 (P[t/0])\<close>
[PROOF STATE]
proof (prove)
using this:
closedt 0 t \<and> Neg (P[t/0]) \<in> H

goal (1 subgoal):
 1. closed 0 (P[t/0])
[PROOF STEP]
using Forall \<open>closed 0 x\<close>
[PROOF STATE]
proof (prove)
using this:
closedt 0 t \<and> Neg (P[t/0]) \<in> H
x = Forall P
closed 0 x

goal (1 subgoal):
 1. closed 0 (P[t/0])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closed 0 (P[t/0])

goal (1 subgoal):
 1. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
have \<open>(subst P t 0, Forall P) \<in> measure size_form \<longrightarrow>
              (Neg (subst P t 0) \<in> H \<longrightarrow> closed 0 (subst P t 0) \<longrightarrow>
              ?eval (Neg (subst P t 0)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P[t/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[t/0]) \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[t/0]))
[PROOF STEP]
using Forall wf
[PROOF STATE]
proof (prove)
using this:
x = Forall P
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))

goal (1 subgoal):
 1. (P[t/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[t/0]) \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[t/0]))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(P[t/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[t/0]) \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[t/0]))

goal (1 subgoal):
 1. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(P[t/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[t/0]) \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[t/0]))
[PROOF STEP]
have \<open>?eval (Neg (P[t/0]))\<close>
[PROOF STATE]
proof (prove)
using this:
(P[t/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[t/0]) \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[t/0]))

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[t/0]))
[PROOF STEP]
using Forall * \<open>closed 0 (P[t/0])\<close>
[PROOF STATE]
proof (prove)
using this:
(P[t/0], Forall P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[t/0]) \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[t/0]))
x = Forall P
closedt 0 t \<and> Neg (P[t/0]) \<in> H
closed 0 (P[t/0])

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[t/0]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[t/0]))

goal (1 subgoal):
 1. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[t/0]))
[PROOF STEP]
have \<open>\<exists>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P\<close>
[PROOF STATE]
proof (prove)
using this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[t/0]))

goal (1 subgoal):
 1. \<exists>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P

goal (1 subgoal):
 1. \<lbrakk>x = Forall P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
show \<open>?eval (Neg x)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
using Forall
[PROOF STATE]
proof (prove)
using this:
\<exists>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
x = Forall P

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))

goal (1 subgoal):
 1. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
case (Exists P)
[PROOF STATE]
proof (state)
this:
x = Exists P

goal (1 subgoal):
 1. \<And>x9. x = Exists x9 \<Longrightarrow> (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = Exists P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = Exists P

goal (1 subgoal):
 1. (x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))
[PROOF STEP]
proof (intro conjI impI allI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x = Exists P; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
x \<in> H
closed 0 x

goal (2 subgoals):
 1. \<lbrakk>x = Exists P; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> H
closed 0 x
[PROOF STEP]
have \<open>\<exists>t. closedt 0 t \<and> (P[t/0]) \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x

goal (1 subgoal):
 1. \<exists>t. closedt 0 t \<and> P[t/0] \<in> H
[PROOF STEP]
using Exists hin
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x
x = Exists P
hintikka H

goal (1 subgoal):
 1. \<exists>t. closedt 0 t \<and> P[t/0] \<in> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
x \<in> H
closed 0 x
x = Exists P
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. \<exists>t. closedt 0 t \<and> P[t/0] \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>t. closedt 0 t \<and> P[t/0] \<in> H

goal (2 subgoals):
 1. \<lbrakk>x = Exists P; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. closedt 0 t \<and> P[t/0] \<in> H
[PROOF STEP]
obtain t where *: \<open>closedt 0 t \<and> (P[t/0]) \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>t. closedt 0 t \<and> P[t/0] \<in> H

goal (1 subgoal):
 1. (\<And>t. closedt 0 t \<and> P[t/0] \<in> H \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
closedt 0 t \<and> P[t/0] \<in> H

goal (2 subgoals):
 1. \<lbrakk>x = Exists P; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closedt 0 t \<and> P[t/0] \<in> H
[PROOF STEP]
have \<open>closed 0 (P[t/0])\<close>
[PROOF STATE]
proof (prove)
using this:
closedt 0 t \<and> P[t/0] \<in> H

goal (1 subgoal):
 1. closed 0 (P[t/0])
[PROOF STEP]
using Exists \<open>closed 0 x\<close>
[PROOF STATE]
proof (prove)
using this:
closedt 0 t \<and> P[t/0] \<in> H
x = Exists P
closed 0 x

goal (1 subgoal):
 1. closed 0 (P[t/0])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closed 0 (P[t/0])

goal (2 subgoals):
 1. \<lbrakk>x = Exists P; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
have \<open>(subst P t 0, Exists P) \<in> measure size_form \<longrightarrow>
              ((subst P t 0) \<in> H \<longrightarrow> closed 0 (subst P t 0) \<longrightarrow>
              ?eval (subst P t 0))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P[t/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[t/0] \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[t/0])
[PROOF STEP]
using Exists wf
[PROOF STATE]
proof (prove)
using this:
x = Exists P
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))

goal (1 subgoal):
 1. (P[t/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[t/0] \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[t/0])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(P[t/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[t/0] \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[t/0])

goal (2 subgoals):
 1. \<lbrakk>x = Exists P; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(P[t/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[t/0] \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[t/0])
[PROOF STEP]
have \<open>?eval (P[t/0])\<close>
[PROOF STATE]
proof (prove)
using this:
(P[t/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[t/0] \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[t/0])

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[t/0])
[PROOF STEP]
using Exists * \<open>closed 0 (P[t/0])\<close>
[PROOF STATE]
proof (prove)
using this:
(P[t/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> P[t/0] \<in> H \<longrightarrow> closed 0 (P[t/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[t/0])
x = Exists P
closedt 0 t \<and> P[t/0] \<in> H
closed 0 (P[t/0])

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[t/0])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[t/0])

goal (2 subgoals):
 1. \<lbrakk>x = Exists P; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[t/0])
[PROOF STEP]
have \<open>\<exists>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P\<close>
[PROOF STATE]
proof (prove)
using this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (P[t/0])

goal (1 subgoal):
 1. \<exists>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P

goal (2 subgoals):
 1. \<lbrakk>x = Exists P; x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
 2. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
show \<open>?eval x\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
using Exists
[PROOF STATE]
proof (prove)
using this:
\<exists>z. eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
x = Exists P

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x

goal (1 subgoal):
 1. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
assume \<open>Neg x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (state)
this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
have \<open>\<forall>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
proof (rule allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
from \<open>Neg x \<in> H\<close> and \<open>closed 0 x\<close>
[PROOF STATE]
proof (chain)
picking this:
Neg x \<in> H
closed 0 x
[PROOF STEP]
have \<open>Neg (Exists P) \<in> H\<close> and \<open>closed 0 (Neg (Exists P))\<close>
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x

goal (1 subgoal):
 1. Neg (Exists P) \<in> H &&& closed 0 (Neg (Exists P))
[PROOF STEP]
using Exists
[PROOF STATE]
proof (prove)
using this:
Neg x \<in> H
closed 0 x
x = Exists P

goal (1 subgoal):
 1. Neg (Exists P) \<in> H &&& closed 0 (Neg (Exists P))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
Neg (Exists P) \<in> H
closed 0 (Neg (Exists P))

goal (1 subgoal):
 1. \<And>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg (Exists P) \<in> H
closed 0 (Neg (Exists P))
[PROOF STEP]
have *: \<open>\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Exists P) \<in> H
closed 0 (Neg (Exists P))

goal (1 subgoal):
 1. \<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H
[PROOF STEP]
using hin
[PROOF STATE]
proof (prove)
using this:
Neg (Exists P) \<in> H
closed 0 (Neg (Exists P))
hintikka H

goal (1 subgoal):
 1. \<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H
[PROOF STEP]
unfolding hintikka_def
[PROOF STATE]
proof (prove)
using this:
Neg (Exists P) \<in> H
closed 0 (Neg (Exists P))
(\<forall>p ts. \<not> (Pred p ts \<in> H \<and> Neg (Pred p ts) \<in> H)) \<and> FF \<notin> H \<and> Neg TT \<notin> H \<and> (\<forall>Z. Neg (Neg Z) \<in> H \<longrightarrow> Z \<in> H) \<and> (\<forall>A B. And A B \<in> H \<longrightarrow> A \<in> H \<and> B \<in> H) \<and> (\<forall>A B. Neg (Or A B) \<in> H \<longrightarrow> Neg A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>A B. Or A B \<in> H \<longrightarrow> A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (And A B) \<in> H \<longrightarrow> Neg A \<in> H \<or> Neg B \<in> H) \<and> (\<forall>A B. Impl A B \<in> H \<longrightarrow> Neg A \<in> H \<or> B \<in> H) \<and> (\<forall>A B. Neg (Impl A B) \<in> H \<longrightarrow> A \<in> H \<and> Neg B \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Forall P \<in> H \<longrightarrow> P[t/0] \<in> H) \<and> (\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H) \<and> (\<forall>P. Exists P \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> P[t/0] \<in> H)) \<and> (\<forall>P. Neg (Forall P) \<in> H \<longrightarrow> (\<exists>t. closedt 0 t \<and> Neg (P[t/0]) \<in> H))

goal (1 subgoal):
 1. \<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H

goal (1 subgoal):
 1. \<And>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
from \<open>closed 0 (Neg (Exists P))\<close>
[PROOF STATE]
proof (chain)
picking this:
closed 0 (Neg (Exists P))
[PROOF STEP]
have \<open>closed (Suc 0) P\<close>
[PROOF STATE]
proof (prove)
using this:
closed 0 (Neg (Exists P))

goal (1 subgoal):
 1. closed (Suc 0) P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closed (Suc 0) P

goal (1 subgoal):
 1. \<And>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
have \<open>(P[term_of_hterm z/0], Exists P) \<in> measure size_form \<longrightarrow>
              (Neg (P[term_of_hterm z/0]) \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow>
              ?eval (Neg (P[term_of_hterm z/0])))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P[term_of_hterm z/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[term_of_hterm z/0]) \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[term_of_hterm z/0]))
[PROOF STEP]
using Exists wf
[PROOF STATE]
proof (prove)
using this:
x = Exists P
\<forall>y. (y, x) \<in> measure FOL_Fitting.size_form \<longrightarrow> (y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) y) \<and> (Neg y \<in> H \<longrightarrow> closed 0 y \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg y))

goal (1 subgoal):
 1. (P[term_of_hterm z/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[term_of_hterm z/0]) \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[term_of_hterm z/0]))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(P[term_of_hterm z/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[term_of_hterm z/0]) \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[term_of_hterm z/0]))

goal (1 subgoal):
 1. \<And>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(P[term_of_hterm z/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[term_of_hterm z/0]) \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[term_of_hterm z/0]))
[PROOF STEP]
show \<open>\<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P\<close>
[PROOF STATE]
proof (prove)
using this:
(P[term_of_hterm z/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[term_of_hterm z/0]) \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[term_of_hterm z/0]))

goal (1 subgoal):
 1. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
using * \<open>Neg (Exists P) \<in> H\<close> \<open>closed (Suc 0) P\<close>
[PROOF STATE]
proof (prove)
using this:
(P[term_of_hterm z/0], Exists P) \<in> measure FOL_Fitting.size_form \<longrightarrow> Neg (P[term_of_hterm z/0]) \<in> H \<longrightarrow> closed 0 (P[term_of_hterm z/0]) \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg (P[term_of_hterm z/0]))
\<forall>P t. closedt 0 t \<longrightarrow> Neg (Exists P) \<in> H \<longrightarrow> Neg (P[t/0]) \<in> H
Neg (Exists P) \<in> H
closed (Suc 0) P

goal (1 subgoal):
 1. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P

goal (1 subgoal):
 1. \<lbrakk>x = Exists P; Neg x \<in> H; closed 0 x\<rbrakk> \<Longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
[PROOF STEP]
show \<open>?eval (Neg x)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
using Exists
[PROOF STATE]
proof (prove)
using this:
\<forall>z. \<not> eval (e\<langle>0:z\<rangle>) HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) P
x = Exists P

goal (1 subgoal):
 1. eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) x) \<and> (Neg x \<in> H \<longrightarrow> closed 0 x \<longrightarrow> eval e HApp (\<lambda>a ts. Pred a (terms_of_hterms ts) \<in> H) (Neg x))

goal:
No subgoals!
[PROOF STEP]
qed