[STATEMENT]
theorem Hintikka_model:
  assumes \<open>Hintikka H\<close>
  shows \<open>p \<in> H \<longleftrightarrow> \<lbrakk>H\<rbrakk> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<in> H) = \<lbrakk>H\<rbrakk> p
[PROOF STEP]
proof (induct p rule: wf_induct[where r=\<open>measure size_fm\<close>])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wf (measure FOL_Axiomatic_Variant.size_fm)
 2. \<And>x. \<forall>y. (y, x) \<in> measure FOL_Axiomatic_Variant.size_fm \<longrightarrow> (y \<in> H) = \<lbrakk>H\<rbrakk> y \<Longrightarrow> (x \<in> H) = \<lbrakk>H\<rbrakk> x
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. wf (measure FOL_Axiomatic_Variant.size_fm)
 2. \<And>x. \<forall>y. (y, x) \<in> measure FOL_Axiomatic_Variant.size_fm \<longrightarrow> (y \<in> H) = \<lbrakk>H\<rbrakk> y \<Longrightarrow> (x \<in> H) = \<lbrakk>H\<rbrakk> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (measure FOL_Axiomatic_Variant.size_fm)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
wf (measure FOL_Axiomatic_Variant.size_fm)

goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> measure FOL_Axiomatic_Variant.size_fm \<longrightarrow> (y \<in> H) = \<lbrakk>H\<rbrakk> y \<Longrightarrow> (x \<in> H) = \<lbrakk>H\<rbrakk> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> measure FOL_Axiomatic_Variant.size_fm \<longrightarrow> (y \<in> H) = \<lbrakk>H\<rbrakk> y \<Longrightarrow> (x \<in> H) = \<lbrakk>H\<rbrakk> x
[PROOF STEP]
case (2 x)
[PROOF STATE]
proof (state)
this:
\<forall>y. (y, x) \<in> measure FOL_Axiomatic_Variant.size_fm \<longrightarrow> (y \<in> H) = \<lbrakk>H\<rbrakk> y

goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> measure FOL_Axiomatic_Variant.size_fm \<longrightarrow> (y \<in> H) = \<lbrakk>H\<rbrakk> y \<Longrightarrow> (x \<in> H) = \<lbrakk>H\<rbrakk> x
[PROOF STEP]
show \<open>x \<in> H \<longleftrightarrow> \<lbrakk>H\<rbrakk> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> H) = \<lbrakk>H\<rbrakk> x
[PROOF STEP]
proof (cases x; safe)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<lbrakk>x = \<^bold>\<bottom>; \<^bold>\<bottom> \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> \<^bold>\<bottom>
 2. \<lbrakk>x = \<^bold>\<bottom>; \<lbrakk>H\<rbrakk> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> \<^bold>\<bottom> \<in> H
 3. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 4. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 5. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 6. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 7. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 8. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
case Falsity
[PROOF STATE]
proof (state)
this:
x = \<^bold>\<bottom>

goal (8 subgoals):
 1. \<lbrakk>x = \<^bold>\<bottom>; \<^bold>\<bottom> \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> \<^bold>\<bottom>
 2. \<lbrakk>x = \<^bold>\<bottom>; \<lbrakk>H\<rbrakk> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> \<^bold>\<bottom> \<in> H
 3. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 4. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 5. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 6. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 7. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 8. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
assume \<open>\<^bold>\<bottom> \<in> H\<close>
[PROOF STATE]
proof (state)
this:
\<^bold>\<bottom> \<in> H

goal (8 subgoals):
 1. \<lbrakk>x = \<^bold>\<bottom>; \<^bold>\<bottom> \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> \<^bold>\<bottom>
 2. \<lbrakk>x = \<^bold>\<bottom>; \<lbrakk>H\<rbrakk> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> \<^bold>\<bottom> \<in> H
 3. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 4. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 5. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 6. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 7. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 8. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<bottom> \<in> H
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<bottom> \<in> H

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms Hintikka.NoFalsity
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<bottom> \<in> H
Hintikka H
Hintikka ?H \<Longrightarrow> \<^bold>\<bottom> \<notin> ?H

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

goal (8 subgoals):
 1. \<lbrakk>x = \<^bold>\<bottom>; \<^bold>\<bottom> \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> \<^bold>\<bottom>
 2. \<lbrakk>x = \<^bold>\<bottom>; \<lbrakk>H\<rbrakk> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> \<^bold>\<bottom> \<in> H
 3. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 4. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 5. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 6. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 7. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 8. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show \<open>\<lbrakk>H\<rbrakk> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<lbrakk>H\<rbrakk> \<^bold>\<bottom>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<lbrakk>H\<rbrakk> \<^bold>\<bottom>

goal (7 subgoals):
 1. \<lbrakk>x = \<^bold>\<bottom>; \<lbrakk>H\<rbrakk> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> \<^bold>\<bottom> \<in> H
 2. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 3. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 4. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 5. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 6. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 7. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<lbrakk>x = \<^bold>\<bottom>; \<lbrakk>H\<rbrakk> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> \<^bold>\<bottom> \<in> H
 2. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 3. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 4. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 5. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 6. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 7. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
case Falsity
[PROOF STATE]
proof (state)
this:
x = \<^bold>\<bottom>

goal (7 subgoals):
 1. \<lbrakk>x = \<^bold>\<bottom>; \<lbrakk>H\<rbrakk> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> \<^bold>\<bottom> \<in> H
 2. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 3. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 4. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 5. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 6. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 7. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
assume \<open>\<lbrakk>H\<rbrakk> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>H\<rbrakk> \<^bold>\<bottom>

goal (7 subgoals):
 1. \<lbrakk>x = \<^bold>\<bottom>; \<lbrakk>H\<rbrakk> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> \<^bold>\<bottom> \<in> H
 2. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 3. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 4. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 5. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 6. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 7. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>H\<rbrakk> \<^bold>\<bottom>
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>H\<rbrakk> \<^bold>\<bottom>

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

goal (7 subgoals):
 1. \<lbrakk>x = \<^bold>\<bottom>; \<lbrakk>H\<rbrakk> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> \<^bold>\<bottom> \<in> H
 2. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 3. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 4. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 5. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 6. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 7. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show \<open>\<^bold>\<bottom> \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<^bold>\<bottom> \<in> H
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<^bold>\<bottom> \<in> H

goal (6 subgoals):
 1. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 2. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 3. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 4. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 5. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 6. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 2. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 3. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 4. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 5. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 6. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
case (Pre P ts)
[PROOF STATE]
proof (state)
this:
x = \<^bold>\<ddagger> P ts

goal (6 subgoals):
 1. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 2. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 3. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 4. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 5. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 6. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
assume \<open>\<^bold>\<ddagger>P ts \<in> H\<close>
[PROOF STATE]
proof (state)
this:
\<^bold>\<ddagger> P ts \<in> H

goal (6 subgoals):
 1. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<^bold>\<ddagger> x21 x22 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)
 2. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 3. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 4. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 5. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 6. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<ddagger> P ts \<in> H
[PROOF STEP]
show \<open>\<lbrakk>H\<rbrakk> (\<^bold>\<ddagger>P ts)\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<ddagger> P ts \<in> H

goal (1 subgoal):
 1. \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> P ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> P ts)

goal (5 subgoals):
 1. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 2. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 3. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 4. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 5. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 2. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 3. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 4. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 5. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
case (Pre P ts)
[PROOF STATE]
proof (state)
this:
x = \<^bold>\<ddagger> P ts

goal (5 subgoals):
 1. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 2. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 3. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 4. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 5. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
assume \<open>\<lbrakk>H\<rbrakk> (\<^bold>\<ddagger>P ts)\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> P ts)

goal (5 subgoals):
 1. \<And>x21 x22. \<lbrakk>x = \<^bold>\<ddagger> x21 x22; \<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> x21 x22)\<rbrakk> \<Longrightarrow> \<^bold>\<ddagger> x21 x22 \<in> H
 2. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 3. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 4. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 5. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> P ts)
[PROOF STEP]
show \<open>\<^bold>\<ddagger>P ts \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>H\<rbrakk> (\<^bold>\<ddagger> P ts)

goal (1 subgoal):
 1. \<^bold>\<ddagger> P ts \<in> H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>\<ddagger> P ts \<in> H

goal (4 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 2. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 4. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 2. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 4. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
case (Imp p q)
[PROOF STATE]
proof (state)
this:
x = p \<^bold>\<longrightarrow> q

goal (4 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 2. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 4. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
assume \<open>(p \<^bold>\<longrightarrow> q) \<in> H\<close>
[PROOF STATE]
proof (state)
this:
p \<^bold>\<longrightarrow> q \<in> H

goal (4 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 2. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 4. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<^bold>\<longrightarrow> q \<in> H
[PROOF STEP]
have \<open>p \<notin> H \<or> q \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
p \<^bold>\<longrightarrow> q \<in> H

goal (1 subgoal):
 1. p \<notin> H \<or> q \<in> H
[PROOF STEP]
using assms Hintikka.ImpP
[PROOF STATE]
proof (prove)
using this:
p \<^bold>\<longrightarrow> q \<in> H
Hintikka H
\<lbrakk>Hintikka ?H; ?p \<^bold>\<longrightarrow> ?q \<in> ?H\<rbrakk> \<Longrightarrow> ?p \<notin> ?H \<or> ?q \<in> ?H

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

goal (4 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 2. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 4. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<notin> H \<or> q \<in> H
[PROOF STEP]
have \<open>\<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q\<close>
[PROOF STATE]
proof (prove)
using this:
p \<notin> H \<or> q \<in> H

goal (1 subgoal):
 1. \<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q
[PROOF STEP]
using 2 Imp
[PROOF STATE]
proof (prove)
using this:
p \<notin> H \<or> q \<in> H
\<forall>y. (y, x) \<in> measure FOL_Axiomatic_Variant.size_fm \<longrightarrow> (y \<in> H) = \<lbrakk>H\<rbrakk> y
x = p \<^bold>\<longrightarrow> q

goal (1 subgoal):
 1. \<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q

goal (4 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; x31 \<^bold>\<longrightarrow> x32 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)
 2. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 4. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q
[PROOF STEP]
show \<open>\<lbrakk>H\<rbrakk> (p \<^bold>\<longrightarrow> q)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q

goal (1 subgoal):
 1. \<lbrakk>H\<rbrakk> (p \<^bold>\<longrightarrow> q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>H\<rbrakk> (p \<^bold>\<longrightarrow> q)

goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
case (Imp p q)
[PROOF STATE]
proof (state)
this:
x = p \<^bold>\<longrightarrow> q

goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
assume \<open>\<lbrakk>H\<rbrakk> (p \<^bold>\<longrightarrow> q)\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>H\<rbrakk> (p \<^bold>\<longrightarrow> q)

goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>H\<rbrakk> (p \<^bold>\<longrightarrow> q)
[PROOF STEP]
have \<open>\<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>H\<rbrakk> (p \<^bold>\<longrightarrow> q)

goal (1 subgoal):
 1. \<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q

goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q
[PROOF STEP]
have \<open>p \<notin> H \<or> q \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q

goal (1 subgoal):
 1. p \<notin> H \<or> q \<in> H
[PROOF STEP]
using 2 Imp
[PROOF STATE]
proof (prove)
using this:
\<not> \<lbrakk>H\<rbrakk> p \<or> \<lbrakk>H\<rbrakk> q
\<forall>y. (y, x) \<in> measure FOL_Axiomatic_Variant.size_fm \<longrightarrow> (y \<in> H) = \<lbrakk>H\<rbrakk> y
x = p \<^bold>\<longrightarrow> q

goal (1 subgoal):
 1. p \<notin> H \<or> q \<in> H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<notin> H \<or> q \<in> H

goal (3 subgoals):
 1. \<And>x31 x32. \<lbrakk>x = x31 \<^bold>\<longrightarrow> x32; \<lbrakk>H\<rbrakk> (x31 \<^bold>\<longrightarrow> x32)\<rbrakk> \<Longrightarrow> x31 \<^bold>\<longrightarrow> x32 \<in> H
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 3. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<notin> H \<or> q \<in> H
[PROOF STEP]
show \<open>(p \<^bold>\<longrightarrow> q) \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
p \<notin> H \<or> q \<in> H

goal (1 subgoal):
 1. p \<^bold>\<longrightarrow> q \<in> H
[PROOF STEP]
using assms Hintikka.ImpN
[PROOF STATE]
proof (prove)
using this:
p \<notin> H \<or> q \<in> H
Hintikka H
\<lbrakk>Hintikka ?H; ?p \<^bold>\<longrightarrow> ?q \<notin> ?H\<rbrakk> \<Longrightarrow> ?p \<in> ?H \<and> ?q \<notin> ?H

goal (1 subgoal):
 1. p \<^bold>\<longrightarrow> q \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<^bold>\<longrightarrow> q \<in> H

goal (2 subgoals):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
case (Uni p)
[PROOF STATE]
proof (state)
this:
x = \<^bold>\<forall> p

goal (2 subgoals):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
assume \<open>\<^bold>\<forall>p \<in> H\<close>
[PROOF STATE]
proof (state)
this:
\<^bold>\<forall> p \<in> H

goal (2 subgoals):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<forall> p \<in> H
[PROOF STEP]
have \<open>\<forall>t. p\<langle>t/0\<rangle> \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<forall> p \<in> H

goal (1 subgoal):
 1. \<forall>t. p\<langle>t/0\<rangle> \<in> H
[PROOF STEP]
using assms Hintikka.UniP
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<forall> p \<in> H
Hintikka H
\<lbrakk>Hintikka ?H; \<^bold>\<forall> ?p \<in> ?H\<rbrakk> \<Longrightarrow> \<forall>t. ?p\<langle>t/0\<rangle> \<in> ?H

goal (1 subgoal):
 1. \<forall>t. p\<langle>t/0\<rangle> \<in> H
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>t. p\<langle>t/0\<rangle> \<in> H

goal (2 subgoals):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t. p\<langle>t/0\<rangle> \<in> H
[PROOF STEP]
have \<open>\<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>t. p\<langle>t/0\<rangle> \<in> H

goal (1 subgoal):
 1. \<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)
[PROOF STEP]
using 2 Uni
[PROOF STATE]
proof (prove)
using this:
\<forall>t. p\<langle>t/0\<rangle> \<in> H
\<forall>y. (y, x) \<in> measure FOL_Axiomatic_Variant.size_fm \<longrightarrow> (y \<in> H) = \<lbrakk>H\<rbrakk> y
x = \<^bold>\<forall> p

goal (1 subgoal):
 1. \<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)

goal (2 subgoals):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<^bold>\<forall> x4 \<in> H\<rbrakk> \<Longrightarrow> \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)
 2. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)
[PROOF STEP]
show \<open>\<lbrakk>H\<rbrakk> (\<^bold>\<forall>p)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)

goal (1 subgoal):
 1. \<lbrakk>H\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>H\<rbrakk> (\<^bold>\<forall> p)

goal (1 subgoal):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
case (Uni p)
[PROOF STATE]
proof (state)
this:
x = \<^bold>\<forall> p

goal (1 subgoal):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
assume \<open>\<lbrakk>H\<rbrakk> (\<^bold>\<forall>p)\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>H\<rbrakk> (\<^bold>\<forall> p)

goal (1 subgoal):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>H\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
have \<open>\<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>H\<rbrakk> (\<^bold>\<forall> p)

goal (1 subgoal):
 1. \<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)

goal (1 subgoal):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)
[PROOF STEP]
have \<open>\<forall>t. p\<langle>t/0\<rangle> \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)

goal (1 subgoal):
 1. \<forall>t. p\<langle>t/0\<rangle> \<in> H
[PROOF STEP]
using 2 Uni
[PROOF STATE]
proof (prove)
using this:
\<forall>t. \<lbrakk>H\<rbrakk> (p\<langle>t/0\<rangle>)
\<forall>y. (y, x) \<in> measure FOL_Axiomatic_Variant.size_fm \<longrightarrow> (y \<in> H) = \<lbrakk>H\<rbrakk> y
x = \<^bold>\<forall> p

goal (1 subgoal):
 1. \<forall>t. p\<langle>t/0\<rangle> \<in> H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>t. p\<langle>t/0\<rangle> \<in> H

goal (1 subgoal):
 1. \<And>x4. \<lbrakk>x = \<^bold>\<forall> x4; \<lbrakk>H\<rbrakk> (\<^bold>\<forall> x4)\<rbrakk> \<Longrightarrow> \<^bold>\<forall> x4 \<in> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t. p\<langle>t/0\<rangle> \<in> H
[PROOF STEP]
show \<open>\<^bold>\<forall>p \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>t. p\<langle>t/0\<rangle> \<in> H

goal (1 subgoal):
 1. \<^bold>\<forall> p \<in> H
[PROOF STEP]
using assms Hintikka.UniN
[PROOF STATE]
proof (prove)
using this:
\<forall>t. p\<langle>t/0\<rangle> \<in> H
Hintikka H
\<lbrakk>Hintikka ?H; \<^bold>\<forall> ?p \<notin> ?H\<rbrakk> \<Longrightarrow> \<exists>n. ?p\<langle>\<^bold># n/0\<rangle> \<notin> ?H

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> H) = \<lbrakk>H\<rbrakk> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inconsistent_head:
  assumes \<open>consistent S\<close> and \<open>maximal S\<close> and \<open>p \<notin> S\<close>
  obtains S' where \<open>set S' \<subseteq> S\<close> and \<open>p # S' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> S; p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms inconsistent_fm
[PROOF STATE]
proof (prove)
using this:
consistent S
maximal S
p \<notin> S
\<lbrakk>consistent ?S; \<not> consistent ({?p} \<union> ?S); \<And>S'. \<lbrakk>set S' \<subseteq> ?S; ?p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> S; p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding consistent_def maximal_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>S'. set S' \<subseteq> S \<and> S' \<turnstile> \<^bold>\<bottom>
\<forall>p. p \<notin> S \<longrightarrow> \<not> (\<nexists>S'. set S' \<subseteq> {p} \<union> S \<and> S' \<turnstile> \<^bold>\<bottom>)
p \<notin> S
\<lbrakk>\<nexists>S'. set S' \<subseteq> ?S \<and> S' \<turnstile> \<^bold>\<bottom>; \<not> (\<nexists>S'. set S' \<subseteq> {?p} \<union> ?S \<and> S' \<turnstile> \<^bold>\<bottom>); \<And>S'. \<lbrakk>set S' \<subseteq> ?S; ?p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>set S' \<subseteq> S; p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis


[STATEMENT]
lemma inconsistent_parts [simp]:
  assumes \<open>ps \<turnstile> \<^bold>\<bottom>\<close> and \<open>set ps \<subseteq> S\<close>
  shows \<open>\<not> consistent S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> consistent S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ps \<turnstile> \<^bold>\<bottom>
set ps \<subseteq> S

goal (1 subgoal):
 1. \<not> consistent S
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
ps \<turnstile> \<^bold>\<bottom>
set ps \<subseteq> S

goal (1 subgoal):
 1. \<not> (\<nexists>S'. set S' \<subseteq> S \<and> S' \<turnstile> \<^bold>\<bottom>)
[PROOF STEP]
by blast


[STATEMENT]
lemma Hintikka_Extend:
  fixes H :: \<open>('f, 'p) fm set\<close>
  assumes \<open>consistent H\<close> and \<open>maximal H\<close> and \<open>saturated H\<close>
  shows \<open>Hintikka H\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hintikka H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<^bold>\<bottom> \<notin> H
 2. \<And>p q. p \<^bold>\<longrightarrow> q \<in> H \<Longrightarrow> p \<notin> H \<or> q \<in> H
 3. \<And>p q. p \<^bold>\<longrightarrow> q \<notin> H \<Longrightarrow> p \<in> H \<and> q \<notin> H
 4. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 5. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
show \<open>\<^bold>\<bottom> \<notin> H\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<bottom> \<notin> H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>\<bottom> \<in> H \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<^bold>\<bottom> \<in> H\<close>
[PROOF STATE]
proof (state)
this:
\<^bold>\<bottom> \<in> H

goal (1 subgoal):
 1. \<^bold>\<bottom> \<in> H \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<bottom> \<in> H

goal (1 subgoal):
 1. \<^bold>\<bottom> \<in> H \<Longrightarrow> False
[PROOF STEP]
have \<open>[\<^bold>\<bottom>] \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<bottom>] \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<bottom>] \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<^bold>\<bottom> \<in> H \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<bottom> \<in> H
[\<^bold>\<bottom>] \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
have \<open>\<not> consistent H\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<bottom> \<in> H
[\<^bold>\<bottom>] \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<not> consistent H
[PROOF STEP]
using inconsistent_parts[where ps=\<open>[\<^bold>\<bottom>]\<close>]
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<bottom> \<in> H
[\<^bold>\<bottom>] \<turnstile> \<^bold>\<bottom>
\<lbrakk>[\<^bold>\<bottom>] \<turnstile> \<^bold>\<bottom>; set [\<^bold>\<bottom>] \<subseteq> ?S\<rbrakk> \<Longrightarrow> \<not> consistent ?S

goal (1 subgoal):
 1. \<not> consistent H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> consistent H

goal (1 subgoal):
 1. \<^bold>\<bottom> \<in> H \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> consistent H
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> consistent H

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>consistent H\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> consistent H
consistent H

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<^bold>\<bottom> \<notin> H

goal (4 subgoals):
 1. \<And>p q. p \<^bold>\<longrightarrow> q \<in> H \<Longrightarrow> p \<notin> H \<or> q \<in> H
 2. \<And>p q. p \<^bold>\<longrightarrow> q \<notin> H \<Longrightarrow> p \<in> H \<and> q \<notin> H
 3. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 4. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>p q. p \<^bold>\<longrightarrow> q \<in> H \<Longrightarrow> p \<notin> H \<or> q \<in> H
 2. \<And>p q. p \<^bold>\<longrightarrow> q \<notin> H \<Longrightarrow> p \<in> H \<and> q \<notin> H
 3. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 4. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
fix p q
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>p q. p \<^bold>\<longrightarrow> q \<in> H \<Longrightarrow> p \<notin> H \<or> q \<in> H
 2. \<And>p q. p \<^bold>\<longrightarrow> q \<notin> H \<Longrightarrow> p \<in> H \<and> q \<notin> H
 3. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 4. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
assume *: \<open>(p \<^bold>\<longrightarrow> q) \<in> H\<close>
[PROOF STATE]
proof (state)
this:
p \<^bold>\<longrightarrow> q \<in> H

goal (4 subgoals):
 1. \<And>p q. p \<^bold>\<longrightarrow> q \<in> H \<Longrightarrow> p \<notin> H \<or> q \<in> H
 2. \<And>p q. p \<^bold>\<longrightarrow> q \<notin> H \<Longrightarrow> p \<in> H \<and> q \<notin> H
 3. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 4. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
show \<open>p \<notin> H \<or> q \<in> H\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<notin> H \<or> q \<in> H
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume \<open>q \<notin> H\<close>
[PROOF STATE]
proof (state)
this:
q \<notin> H

goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<notin> H
[PROOF STEP]
obtain Hq' where Hq': \<open>q # Hq' \<turnstile> \<^bold>\<bottom>\<close> \<open>set Hq' \<subseteq> H\<close>
[PROOF STATE]
proof (prove)
using this:
q \<notin> H

goal (1 subgoal):
 1. (\<And>Hq'. \<lbrakk>q # Hq' \<turnstile> \<^bold>\<bottom>; set Hq' \<subseteq> H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms inconsistent_head
[PROOF STATE]
proof (prove)
using this:
q \<notin> H
consistent H
maximal H
saturated H
\<lbrakk>consistent ?S; maximal ?S; ?p \<notin> ?S; \<And>S'. \<lbrakk>set S' \<subseteq> ?S; ?p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>Hq'. \<lbrakk>q # Hq' \<turnstile> \<^bold>\<bottom>; set Hq' \<subseteq> H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
q # Hq' \<turnstile> \<^bold>\<bottom>
set Hq' \<subseteq> H

goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume \<open>p \<in> H\<close>
[PROOF STATE]
proof (state)
this:
p \<in> H

goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> H
[PROOF STEP]
have \<open>(\<^bold>\<not> p) \<notin> H\<close>
[PROOF STATE]
proof (prove)
using this:
p \<in> H

goal (1 subgoal):
 1. \<^bold>\<not> p \<notin> H
[PROOF STEP]
using assms maximal_exactly_one
[PROOF STATE]
proof (prove)
using this:
p \<in> H
consistent H
maximal H
saturated H
\<lbrakk>consistent ?S; maximal ?S\<rbrakk> \<Longrightarrow> (?p \<in> ?S) = (\<^bold>\<not> ?p \<notin> ?S)

goal (1 subgoal):
 1. \<^bold>\<not> p \<notin> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> p \<notin> H

goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<not> p \<notin> H
[PROOF STEP]
obtain Hp' where Hp': \<open>(\<^bold>\<not> p) # Hp' \<turnstile> \<^bold>\<bottom>\<close> \<open>set Hp' \<subseteq> H\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> p \<notin> H

goal (1 subgoal):
 1. (\<And>Hp'. \<lbrakk>\<^bold>\<not> p # Hp' \<turnstile> \<^bold>\<bottom>; set Hp' \<subseteq> H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms inconsistent_head
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> p \<notin> H
consistent H
maximal H
saturated H
\<lbrakk>consistent ?S; maximal ?S; ?p \<notin> ?S; \<And>S'. \<lbrakk>set S' \<subseteq> ?S; ?p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>Hp'. \<lbrakk>\<^bold>\<not> p # Hp' \<turnstile> \<^bold>\<bottom>; set Hp' \<subseteq> H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> p # Hp' \<turnstile> \<^bold>\<bottom>
set Hp' \<subseteq> H

goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?H' = \<open>Hp' @ Hq'\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have H': \<open>set ?H' = set Hp' \<union> set Hq'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Hp' @ Hq') = set Hp' \<union> set Hq'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (Hp' @ Hq') = set Hp' \<union> set Hq'

goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (Hp' @ Hq') = set Hp' \<union> set Hq'
[PROOF STEP]
have \<open>set Hp' \<subseteq> set ?H'\<close> and \<open>set Hq' \<subseteq> set ?H'\<close>
[PROOF STATE]
proof (prove)
using this:
set (Hp' @ Hq') = set Hp' \<union> set Hq'

goal (1 subgoal):
 1. set Hp' \<subseteq> set (Hp' @ Hq') &&& set Hq' \<subseteq> set (Hp' @ Hq')
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
set Hp' \<subseteq> set (Hp' @ Hq')
set Hq' \<subseteq> set (Hp' @ Hq')

goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set Hp' \<subseteq> set (Hp' @ Hq')
set Hq' \<subseteq> set (Hp' @ Hq')
[PROOF STEP]
have \<open>(\<^bold>\<not> p) # ?H' \<turnstile> \<^bold>\<bottom>\<close> and \<open>q # ?H' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
using this:
set Hp' \<subseteq> set (Hp' @ Hq')
set Hq' \<subseteq> set (Hp' @ Hq')

goal (1 subgoal):
 1. \<^bold>\<not> p # Hp' @ Hq' \<turnstile> \<^bold>\<bottom> &&& q # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
using Hp'(1) Hq'(1) deduct imply_weaken
[PROOF STATE]
proof (prove)
using this:
set Hp' \<subseteq> set (Hp' @ Hq')
set Hq' \<subseteq> set (Hp' @ Hq')
\<^bold>\<not> p # Hp' \<turnstile> \<^bold>\<bottom>
q # Hq' \<turnstile> \<^bold>\<bottom>
?ps \<turnstile> ?p \<^bold>\<longrightarrow> ?q \<Longrightarrow> ?p # ?ps \<turnstile> ?q
?p # ?ps \<turnstile> ?q \<Longrightarrow> ?ps \<turnstile> ?p \<^bold>\<longrightarrow> ?q
\<lbrakk>?ps \<turnstile> ?q; set ?ps \<subseteq> set ?ps'\<rbrakk> \<Longrightarrow> ?ps' \<turnstile> ?q

goal (1 subgoal):
 1. \<^bold>\<not> p # Hp' @ Hq' \<turnstile> \<^bold>\<bottom> &&& q # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> p # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
q # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<not> p # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
q # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
have \<open>(p \<^bold>\<longrightarrow> q) # ?H' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> p # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
q # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. (p \<^bold>\<longrightarrow> q) # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
using Boole imply_Cons imply_head MP' cut
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> p # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
q # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
\<^bold>\<not> ?p # ?ps \<turnstile> \<^bold>\<bottom> \<Longrightarrow> ?ps \<turnstile> ?p
?ps \<turnstile> ?q \<Longrightarrow> ?p # ?ps \<turnstile> ?q
?p # ?ps \<turnstile> ?p
\<lbrakk>?ps \<turnstile> ?p \<^bold>\<longrightarrow> ?q; ?ps \<turnstile> ?p\<rbrakk> \<Longrightarrow> ?ps \<turnstile> ?q
\<lbrakk>?p # ?ps \<turnstile> ?r; ?q # ?ps \<turnstile> ?p\<rbrakk> \<Longrightarrow> ?q # ?ps \<turnstile> ?r

goal (1 subgoal):
 1. (p \<^bold>\<longrightarrow> q) # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(p \<^bold>\<longrightarrow> q) # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(p \<^bold>\<longrightarrow> q) # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>set ((p \<^bold>\<longrightarrow> q) # ?H') \<subseteq> H\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ((p \<^bold>\<longrightarrow> q) # Hp' @ Hq') \<subseteq> H
[PROOF STEP]
using \<open>q \<notin> H\<close> *(1) H' Hp'(2) Hq'(2)
[PROOF STATE]
proof (prove)
using this:
q \<notin> H
p \<^bold>\<longrightarrow> q \<in> H
set (Hp' @ Hq') = set Hp' \<union> set Hq'
set Hp' \<subseteq> H
set Hq' \<subseteq> H

goal (1 subgoal):
 1. set ((p \<^bold>\<longrightarrow> q) # Hp' @ Hq') \<subseteq> H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ((p \<^bold>\<longrightarrow> q) # Hp' @ Hq') \<subseteq> H

goal (1 subgoal):
 1. \<lbrakk>q \<notin> H; p \<in> H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(p \<^bold>\<longrightarrow> q) # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
set ((p \<^bold>\<longrightarrow> q) # Hp' @ Hq') \<subseteq> H
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(p \<^bold>\<longrightarrow> q) # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
set ((p \<^bold>\<longrightarrow> q) # Hp' @ Hq') \<subseteq> H

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(p \<^bold>\<longrightarrow> q) # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
set ((p \<^bold>\<longrightarrow> q) # Hp' @ Hq') \<subseteq> H
consistent H
maximal H
saturated H

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
(p \<^bold>\<longrightarrow> q) # Hp' @ Hq' \<turnstile> \<^bold>\<bottom>
set ((p \<^bold>\<longrightarrow> q) # Hp' @ Hq') \<subseteq> H
\<nexists>S'. set S' \<subseteq> H \<and> S' \<turnstile> \<^bold>\<bottom>
maximal H
saturated H

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<notin> H \<or> q \<in> H

goal (3 subgoals):
 1. \<And>p q. p \<^bold>\<longrightarrow> q \<notin> H \<Longrightarrow> p \<in> H \<and> q \<notin> H
 2. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 3. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p q. p \<^bold>\<longrightarrow> q \<notin> H \<Longrightarrow> p \<in> H \<and> q \<notin> H
 2. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 3. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
fix p q
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p q. p \<^bold>\<longrightarrow> q \<notin> H \<Longrightarrow> p \<in> H \<and> q \<notin> H
 2. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 3. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
assume *: \<open>(p \<^bold>\<longrightarrow> q) \<notin> H\<close>
[PROOF STATE]
proof (state)
this:
p \<^bold>\<longrightarrow> q \<notin> H

goal (3 subgoals):
 1. \<And>p q. p \<^bold>\<longrightarrow> q \<notin> H \<Longrightarrow> p \<in> H \<and> q \<notin> H
 2. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 3. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
show \<open>p \<in> H \<and> q \<notin> H\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> H \<and> q \<notin> H
[PROOF STEP]
proof (safe, rule ccontr)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<notin> H \<Longrightarrow> False
 2. q \<in> H \<Longrightarrow> False
[PROOF STEP]
assume \<open>p \<notin> H\<close>
[PROOF STATE]
proof (state)
this:
p \<notin> H

goal (2 subgoals):
 1. p \<notin> H \<Longrightarrow> False
 2. q \<in> H \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<notin> H
[PROOF STEP]
obtain H' where S': \<open>p # H' \<turnstile> \<^bold>\<bottom>\<close> \<open>set H' \<subseteq> H\<close>
[PROOF STATE]
proof (prove)
using this:
p \<notin> H

goal (1 subgoal):
 1. (\<And>H'. \<lbrakk>p # H' \<turnstile> \<^bold>\<bottom>; set H' \<subseteq> H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms inconsistent_head
[PROOF STATE]
proof (prove)
using this:
p \<notin> H
consistent H
maximal H
saturated H
\<lbrakk>consistent ?S; maximal ?S; ?p \<notin> ?S; \<And>S'. \<lbrakk>set S' \<subseteq> ?S; ?p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>H'. \<lbrakk>p # H' \<turnstile> \<^bold>\<bottom>; set H' \<subseteq> H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
p # H' \<turnstile> \<^bold>\<bottom>
set H' \<subseteq> H

goal (2 subgoals):
 1. p \<notin> H \<Longrightarrow> False
 2. q \<in> H \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p # H' \<turnstile> \<^bold>\<bottom>
set H' \<subseteq> H

goal (2 subgoals):
 1. p \<notin> H \<Longrightarrow> False
 2. q \<in> H \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<^bold>\<not> (p \<^bold>\<longrightarrow> q)) # H' \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> p

goal (2 subgoals):
 1. p \<notin> H \<Longrightarrow> False
 2. q \<in> H \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p # H' \<turnstile> \<^bold>\<bottom>
set H' \<subseteq> H
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> p
[PROOF STEP]
have \<open>(\<^bold>\<not> (p \<^bold>\<longrightarrow> q)) # H' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
using this:
p # H' \<turnstile> \<^bold>\<bottom>
set H' \<subseteq> H
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> p

goal (1 subgoal):
 1. \<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>

goal (2 subgoals):
 1. p \<notin> H \<Longrightarrow> False
 2. q \<in> H \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>

goal (2 subgoals):
 1. p \<notin> H \<Longrightarrow> False
 2. q \<in> H \<Longrightarrow> False
[PROOF STEP]
have \<open>set ((\<^bold>\<not> (p \<^bold>\<longrightarrow> q)) # H') \<subseteq> H\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H
[PROOF STEP]
using *(1) S'(2) assms maximal_exactly_one
[PROOF STATE]
proof (prove)
using this:
p \<^bold>\<longrightarrow> q \<notin> H
set H' \<subseteq> H
consistent H
maximal H
saturated H
\<lbrakk>consistent ?S; maximal ?S\<rbrakk> \<Longrightarrow> (?p \<in> ?S) = (\<^bold>\<not> ?p \<notin> ?S)

goal (1 subgoal):
 1. set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H

goal (2 subgoals):
 1. p \<notin> H \<Longrightarrow> False
 2. q \<in> H \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>
set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>
set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>
set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H
consistent H
maximal H
saturated H

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>
set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H
\<nexists>S'. set S' \<subseteq> H \<and> S' \<turnstile> \<^bold>\<bottom>
maximal H
saturated H

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

goal (1 subgoal):
 1. q \<in> H \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> H \<Longrightarrow> False
[PROOF STEP]
assume \<open>q \<in> H\<close>
[PROOF STATE]
proof (state)
this:
q \<in> H

goal (1 subgoal):
 1. q \<in> H \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> H
[PROOF STEP]
have \<open>(\<^bold>\<not> q) \<notin> H\<close>
[PROOF STATE]
proof (prove)
using this:
q \<in> H

goal (1 subgoal):
 1. \<^bold>\<not> q \<notin> H
[PROOF STEP]
using assms maximal_exactly_one
[PROOF STATE]
proof (prove)
using this:
q \<in> H
consistent H
maximal H
saturated H
\<lbrakk>consistent ?S; maximal ?S\<rbrakk> \<Longrightarrow> (?p \<in> ?S) = (\<^bold>\<not> ?p \<notin> ?S)

goal (1 subgoal):
 1. \<^bold>\<not> q \<notin> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> q \<notin> H

goal (1 subgoal):
 1. q \<in> H \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<not> q \<notin> H
[PROOF STEP]
obtain H' where H': \<open>(\<^bold>\<not> q) # H' \<turnstile> \<^bold>\<bottom>\<close> \<open>set H' \<subseteq> H\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> q \<notin> H

goal (1 subgoal):
 1. (\<And>H'. \<lbrakk>\<^bold>\<not> q # H' \<turnstile> \<^bold>\<bottom>; set H' \<subseteq> H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms inconsistent_head
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> q \<notin> H
consistent H
maximal H
saturated H
\<lbrakk>consistent ?S; maximal ?S; ?p \<notin> ?S; \<And>S'. \<lbrakk>set S' \<subseteq> ?S; ?p # S' \<turnstile> \<^bold>\<bottom>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>H'. \<lbrakk>\<^bold>\<not> q # H' \<turnstile> \<^bold>\<bottom>; set H' \<subseteq> H\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> q # H' \<turnstile> \<^bold>\<bottom>
set H' \<subseteq> H

goal (1 subgoal):
 1. q \<in> H \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> q # H' \<turnstile> \<^bold>\<bottom>
set H' \<subseteq> H

goal (1 subgoal):
 1. q \<in> H \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<^bold>\<not> (p \<^bold>\<longrightarrow> q)) # H' \<turnstile> \<^bold>\<not> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<not> q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<not> q

goal (1 subgoal):
 1. q \<in> H \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<not> q # H' \<turnstile> \<^bold>\<bottom>
set H' \<subseteq> H
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<not> q
[PROOF STEP]
have \<open>(\<^bold>\<not> (p \<^bold>\<longrightarrow> q)) # H' \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> q # H' \<turnstile> \<^bold>\<bottom>
set H' \<subseteq> H
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<not> q

goal (1 subgoal):
 1. \<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. q \<in> H \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. q \<in> H \<Longrightarrow> False
[PROOF STEP]
have \<open>set ((\<^bold>\<not> (p \<^bold>\<longrightarrow> q)) # H') \<subseteq> H\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H
[PROOF STEP]
using *(1) H'(2) assms maximal_exactly_one
[PROOF STATE]
proof (prove)
using this:
p \<^bold>\<longrightarrow> q \<notin> H
set H' \<subseteq> H
consistent H
maximal H
saturated H
\<lbrakk>consistent ?S; maximal ?S\<rbrakk> \<Longrightarrow> (?p \<in> ?S) = (\<^bold>\<not> ?p \<notin> ?S)

goal (1 subgoal):
 1. set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H

goal (1 subgoal):
 1. q \<in> H \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>
set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>
set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>
set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H
consistent H
maximal H
saturated H

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H' \<turnstile> \<^bold>\<bottom>
set (\<^bold>\<not> (p \<^bold>\<longrightarrow> q) # H') \<subseteq> H
\<nexists>S'. set S' \<subseteq> H \<and> S' \<turnstile> \<^bold>\<bottom>
maximal H
saturated H

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<in> H \<and> q \<notin> H

goal (2 subgoals):
 1. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 2. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 2. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 2. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
assume \<open>\<^bold>\<forall>p \<in> H\<close>
[PROOF STATE]
proof (state)
this:
\<^bold>\<forall> p \<in> H

goal (2 subgoals):
 1. \<And>p. \<^bold>\<forall> p \<in> H \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> H
 2. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<forall> p \<in> H
[PROOF STEP]
show \<open>\<forall>t. p\<langle>t/0\<rangle> \<in> H\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<forall> p \<in> H

goal (1 subgoal):
 1. \<forall>t. p\<langle>t/0\<rangle> \<in> H
[PROOF STEP]
using assms consistent_add_instance
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<forall> p \<in> H
consistent H
maximal H
saturated H
\<lbrakk>consistent ?S; \<^bold>\<forall> ?p \<in> ?S\<rbrakk> \<Longrightarrow> consistent ({?p\<langle>?t/0\<rangle>} \<union> ?S)

goal (1 subgoal):
 1. \<forall>t. p\<langle>t/0\<rangle> \<in> H
[PROOF STEP]
unfolding maximal_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<forall> p \<in> H
consistent H
\<forall>p. p \<notin> H \<longrightarrow> \<not> consistent ({p} \<union> H)
saturated H
\<lbrakk>consistent ?S; \<^bold>\<forall> ?p \<in> ?S\<rbrakk> \<Longrightarrow> consistent ({?p\<langle>?t/0\<rangle>} \<union> ?S)

goal (1 subgoal):
 1. \<forall>t. p\<langle>t/0\<rangle> \<in> H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>t. p\<langle>t/0\<rangle> \<in> H

goal (1 subgoal):
 1. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
assume \<open>\<^bold>\<forall>p \<notin> H\<close>
[PROOF STATE]
proof (state)
this:
\<^bold>\<forall> p \<notin> H

goal (1 subgoal):
 1. \<And>p. \<^bold>\<forall> p \<notin> H \<Longrightarrow> \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<forall> p \<notin> H
[PROOF STEP]
show \<open>\<exists>n. p\<langle>\<^bold>#n/0\<rangle> \<notin> H\<close>
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<forall> p \<notin> H

goal (1 subgoal):
 1. \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
using assms maximal_exactly_one
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<forall> p \<notin> H
consistent H
maximal H
saturated H
\<lbrakk>consistent ?S; maximal ?S\<rbrakk> \<Longrightarrow> (?p \<in> ?S) = (\<^bold>\<not> ?p \<notin> ?S)

goal (1 subgoal):
 1. \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
unfolding saturated_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<forall> p \<notin> H
consistent H
maximal H
\<forall>p. \<^bold>\<not> \<^bold>\<forall> p \<in> H \<longrightarrow> (\<exists>n. \<^bold>\<not> p\<langle>\<^bold># n/0\<rangle> \<in> H)
\<lbrakk>consistent ?S; maximal ?S\<rbrakk> \<Longrightarrow> (?p \<in> ?S) = (\<^bold>\<not> ?p \<notin> ?S)

goal (1 subgoal):
 1. \<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<exists>n. p\<langle>\<^bold># n/0\<rangle> \<notin> H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem strong_completeness:
  fixes p :: \<open>('f :: countable, 'p :: countable) fm\<close>
  assumes \<open>\<forall>(E :: _ \<Rightarrow> 'f tm) F G. Ball X \<lbrakk>E, F, G\<rbrakk> \<longrightarrow> \<lbrakk>E, F, G\<rbrakk> p\<close>
    and \<open>finite (vars X)\<close>
  shows \<open>\<exists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p
[PROOF STEP]
have *: \<open>\<nexists>ps. set ps \<subseteq> X \<and> (\<^bold>\<not> p) # ps \<turnstile> \<^bold>\<bottom>\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> \<^bold>\<not> p # ps \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
using Boole
[PROOF STATE]
proof (prove)
using this:
\<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p
\<^bold>\<not> ?p # ?ps \<turnstile> \<^bold>\<bottom> \<Longrightarrow> ?ps \<turnstile> ?p

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> \<^bold>\<not> p # ps \<turnstile> \<^bold>\<bottom>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<nexists>ps. set ps \<subseteq> X \<and> \<^bold>\<not> p # ps \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
let ?S = \<open>{\<^bold>\<not> p} \<union> X\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
let ?H = \<open>Extend ?S from_nat\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
have \<open>consistent ?S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent ({\<^bold>\<not> p} \<union> X)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<nexists>ps. set ps \<subseteq> X \<and> \<^bold>\<not> p # ps \<turnstile> \<^bold>\<bottom>

goal (1 subgoal):
 1. consistent ({\<^bold>\<not> p} \<union> X)
[PROOF STEP]
by (metis consistent_def imply_Cons inconsistent_fm)
[PROOF STATE]
proof (state)
this:
consistent ({\<^bold>\<not> p} \<union> X)

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
consistent ({\<^bold>\<not> p} \<union> X)

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
have \<open>finite (vars ?S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vars ({\<^bold>\<not> p} \<union> X))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>E F G. Ball X \<lbrakk>E, F, G\<rbrakk> \<longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
finite (vars X)

goal (1 subgoal):
 1. finite (vars ({\<^bold>\<not> p} \<union> X))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (vars ({\<^bold>\<not> p} \<union> X))

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
consistent ({\<^bold>\<not> p} \<union> X)
finite (vars ({\<^bold>\<not> p} \<union> X))
[PROOF STEP]
have \<open>consistent ?H\<close> and \<open>maximal ?H\<close>
[PROOF STATE]
proof (prove)
using this:
consistent ({\<^bold>\<not> p} \<union> X)
finite (vars ({\<^bold>\<not> p} \<union> X))

goal (1 subgoal):
 1. consistent (Extend ({\<^bold>\<not> p} \<union> X) from_nat) &&& maximal (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
[PROOF STEP]
using assms consistent_Extend maximal_Extend surj_from_nat
[PROOF STATE]
proof (prove)
using this:
consistent ({\<^bold>\<not> p} \<union> X)
finite (vars ({\<^bold>\<not> p} \<union> X))
\<forall>E F G. Ball X \<lbrakk>E, F, G\<rbrakk> \<longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
finite (vars X)
\<lbrakk>consistent ?S; finite (vars ?S)\<rbrakk> \<Longrightarrow> consistent (Extend ?S ?f)
surj ?f \<Longrightarrow> maximal (Extend ?S ?f)
surj from_nat

goal (1 subgoal):
 1. consistent (Extend ({\<^bold>\<not> p} \<union> X) from_nat) &&& maximal (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
consistent (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
maximal (Extend ({\<^bold>\<not> p} \<union> X) from_nat)

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
consistent (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
maximal (Extend ({\<^bold>\<not> p} \<union> X) from_nat)

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
consistent (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
maximal (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
[PROOF STEP]
have \<open>saturated ?H\<close>
[PROOF STATE]
proof (prove)
using this:
consistent (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
maximal (Extend ({\<^bold>\<not> p} \<union> X) from_nat)

goal (1 subgoal):
 1. saturated (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
[PROOF STEP]
using saturated_Extend
[PROOF STATE]
proof (prove)
using this:
consistent (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
maximal (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
\<lbrakk>consistent (Extend ?S ?f); surj ?f\<rbrakk> \<Longrightarrow> saturated (Extend ?S ?f)

goal (1 subgoal):
 1. saturated (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
saturated (Extend ({\<^bold>\<not> p} \<union> X) from_nat)

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
consistent (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
maximal (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
saturated (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
[PROOF STEP]
have \<open>Hintikka ?H\<close>
[PROOF STATE]
proof (prove)
using this:
consistent (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
maximal (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
saturated (Extend ({\<^bold>\<not> p} \<union> X) from_nat)

goal (1 subgoal):
 1. Hintikka (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
[PROOF STEP]
using assms Hintikka_Extend
[PROOF STATE]
proof (prove)
using this:
consistent (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
maximal (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
saturated (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
\<forall>E F G. Ball X \<lbrakk>E, F, G\<rbrakk> \<longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
finite (vars X)
\<lbrakk>consistent ?H; maximal ?H; saturated ?H\<rbrakk> \<Longrightarrow> Hintikka ?H

goal (1 subgoal):
 1. Hintikka (Extend ({\<^bold>\<not> p} \<union> X) from_nat)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Hintikka (Extend ({\<^bold>\<not> p} \<union> X) from_nat)

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
have \<open>\<lbrakk>?H\<rbrakk> p\<close> if \<open>p \<in> ?S\<close> for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> p
[PROOF STEP]
using that Extend_subset Hintikka_model \<open>Hintikka ?H\<close>
[PROOF STATE]
proof (prove)
using this:
p \<in> {\<^bold>\<not> p} \<union> X
?S \<subseteq> Extend ?S ?f
Hintikka ?H \<Longrightarrow> (?p \<in> ?H) = \<lbrakk>?H\<rbrakk> ?p
Hintikka (Extend ({\<^bold>\<not> p} \<union> X) from_nat)

goal (1 subgoal):
 1. \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?p \<in> {\<^bold>\<not> p} \<union> X \<Longrightarrow> \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> ?p

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?p \<in> {\<^bold>\<not> p} \<union> X \<Longrightarrow> \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> ?p
[PROOF STEP]
have \<open>\<lbrakk>?H\<rbrakk> (\<^bold>\<not> p)\<close> and \<open>\<forall>q \<in> X. \<lbrakk>?H\<rbrakk> q\<close>
[PROOF STATE]
proof (prove)
using this:
?p \<in> {\<^bold>\<not> p} \<union> X \<Longrightarrow> \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> ?p

goal (1 subgoal):
 1. \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> (\<^bold>\<not> p) &&& Ball X \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk>
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
\<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> (\<^bold>\<not> p)
Ball X \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk>

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> (\<^bold>\<not> p)
Ball X \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk>

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> (\<^bold>\<not> p)
Ball X \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk>
[PROOF STEP]
have \<open>\<lbrakk>?H\<rbrakk> p\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> (\<^bold>\<not> p)
Ball X \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> p
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> (\<^bold>\<not> p)
Ball X \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk>
\<forall>E F G. Ball X \<lbrakk>E, F, G\<rbrakk> \<longrightarrow> \<lbrakk>E, F, G\<rbrakk> p

goal (1 subgoal):
 1. \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> p

goal (1 subgoal):
 1. \<nexists>ps. set ps \<subseteq> X \<and> ps \<turnstile> p \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> (\<^bold>\<not> p)
Ball X \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk>
\<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> p
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> (\<^bold>\<not> p)
Ball X \<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk>
\<lbrakk>Extend ({\<^bold>\<not> p} \<union> X) from_nat\<rbrakk> p

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem completeness:
  fixes p :: \<open>('f :: countable, 'p :: countable) fm\<close>
  assumes \<open>\<forall>(E :: _ \<Rightarrow> 'f tm) F G. \<lbrakk>E, F, G\<rbrakk> p\<close>
  shows \<open>\<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> p
[PROOF STEP]
using assms strong_completeness[where X=\<open>{}\<close>]
[PROOF STATE]
proof (prove)
using this:
\<forall>E F G. \<lbrakk>E, F, G\<rbrakk> p
\<lbrakk>\<forall>E F G. Ball {} \<lbrakk>E, F, G\<rbrakk> \<longrightarrow> \<lbrakk>E, F, G\<rbrakk> ?p; finite (vars {})\<rbrakk> \<Longrightarrow> \<exists>ps. set ps \<subseteq> {} \<and> ps \<turnstile> ?p

goal (1 subgoal):
 1. \<turnstile> p
[PROOF STEP]
by simp


[STATEMENT]
theorem main: \<open>valid p \<longleftrightarrow> (\<turnstile> p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid p = (\<turnstile> p)
[PROOF STEP]
using completeness soundness
[PROOF STATE]
proof (prove)
using this:
\<forall>E F G. \<lbrakk>E, F, G\<rbrakk> ?p \<Longrightarrow> \<turnstile> ?p
\<turnstile> ?p \<Longrightarrow> \<lbrakk>?E, ?F, ?G\<rbrakk> ?p

goal (1 subgoal):
 1. valid p = (\<turnstile> p)
[PROOF STEP]
by blast


[STATEMENT]
lemma vfsequenceI[intro]:
  assumes "vsv xs" and "\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>"
  shows "vfsequence xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vsv xs
\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (simp add: vfsequence.intro vfsequence_axioms_def)


[STATEMENT]
lemma vfsequenceD[dest]:
  assumes "vfsequence xs"
  shows "\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
using assms vfsequence.vfsequence_vdomain_in_omega
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
vfsequence ?xs \<Longrightarrow> \<D>\<^sub>\<circ> ?xs \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
by simp


[STATEMENT]
lemma vfsequenceE[elim]:
  assumes "vfsequence xs" and "\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega> \<Longrightarrow> P"
  shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by auto


[STATEMENT]
lemma vfsequence_iff: "vfsequence xs \<longleftrightarrow> vsv xs \<and> \<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs = (vsv xs \<and> \<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>)
[PROOF STEP]
using vfsequence_def
[PROOF STATE]
proof (prove)
using this:
vfsequence ?xs \<equiv> vsv ?xs \<and> vfsequence_axioms ?xs

goal (1 subgoal):
 1. vfsequence xs = (vsv xs \<and> \<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>)
[PROOF STEP]
by auto


[STATEMENT]
lemma (in vfsequence) vfsequence_vdomain: "\<D>\<^sub>\<circ> xs = vcard xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> xs = vcard xs
[PROOF STEP]
unfolding vsv_vcard_vdomain[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> xs = vcard (\<D>\<^sub>\<circ> xs)
[PROOF STEP]
using vfsequence_vdomain_in_omega
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> xs = vcard (\<D>\<^sub>\<circ> xs)
[PROOF STEP]
by simp


[STATEMENT]
lemma (in vfsequence) vfsequence_vcard_in_omega[simp]: "vcard xs \<in>\<^sub>\<circ> \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard xs \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
using vfsequence_vdomain_in_omega
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> xs \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vcard xs \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
by (simp add: vfsequence_vdomain)


[STATEMENT]
lemma vfsequence_vempty[intro, simp]: "vfsequence 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence 0
[PROOF STEP]
by (simp add: vfsequenceI)


[STATEMENT]
lemma vfsequence_vsingleton[intro, simp]: "vfsequence (set {\<langle>0, a\<rangle>})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (set {\<langle>0, a\<rangle>})
[PROOF STEP]
using vone_in_omega
[PROOF STATE]
proof (prove)
using this:
1 \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vfsequence (set {\<langle>0, a\<rangle>})
[PROOF STEP]
unfolding one_V_def
[PROOF STATE]
proof (prove)
using this:
ZFC_in_HOL.succ 0 \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vfsequence (set {\<langle>0, a\<rangle>})
[PROOF STEP]
by (intro vfsequenceI) (auto simp: set_vzero_eq_ord_of_nat_vone)


[STATEMENT]
lemma (in vfsequence) vfsequence_vinsert:
  "vfsequence (vinsert \<langle>vcard xs, a\<rangle> xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (vinsert \<langle>vcard xs, a\<rangle> xs)
[PROOF STEP]
using succ_def succ_in_omega
[PROOF STATE]
proof (prove)
using this:
ZFC_in_HOL.succ ?x \<equiv> vinsert ?x ?x
?n \<in>\<^sub>\<circ> \<omega> \<Longrightarrow> ZFC_in_HOL.succ ?n \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vfsequence (vinsert \<langle>vcard xs, a\<rangle> xs)
[PROOF STEP]
by (auto simp: vfsequence_vdomain)


[STATEMENT]
lemma (in vfsequence) vfsequence_vfinite[simp]: "vfinite xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfinite xs
[PROOF STEP]
by (simp add: vfinite_vcard_omega_iff)


[STATEMENT]
lemma (in vfsequence) vfsequence_vlrestriction[intro, simp]:
  assumes "k \<in>\<^sub>\<circ> \<omega>"
  shows "vfsequence (xs \<restriction>\<^sup>l\<^sub>\<circ> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (xs \<restriction>\<^sup>l\<^sub>\<circ> k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vfsequence (xs \<restriction>\<^sup>l\<^sub>\<circ> k)
[PROOF STEP]
by (force simp: vfsequence_vdomain vdomain_vlrestriction)


[STATEMENT]
lemma vfsequence_vproduct:
  assumes "n \<in>\<^sub>\<circ> \<omega>" and "xs \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>n. A i)"
  shows "vfsequence xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n \<in>\<^sub>\<circ> \<omega>
xs \<in>\<^sub>\<circ> vproduct n A

goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by auto


[STATEMENT]
lemma vfsequence_vcpower:
  assumes "n \<in>\<^sub>\<circ> \<omega>" and "xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> n"
  shows "vfsequence xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
using assms vfsequence_vproduct
[PROOF STATE]
proof (prove)
using this:
n \<in>\<^sub>\<circ> \<omega>
xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> n
\<lbrakk>?n \<in>\<^sub>\<circ> \<omega>; ?xs \<in>\<^sub>\<circ> vproduct ?n ?A\<rbrakk> \<Longrightarrow> vfsequence ?xs

goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by auto


[STATEMENT]
lemma (in vfsequence) vfsequence_vdomain_vlrestriction[intro, simp]:
  assumes "k \<in>\<^sub>\<circ> vcard xs"
  shows "\<D>\<^sub>\<circ> (xs \<restriction>\<^sup>l\<^sub>\<circ> k) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (xs \<restriction>\<^sup>l\<^sub>\<circ> k) = k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<in>\<^sub>\<circ> vcard xs

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (xs \<restriction>\<^sup>l\<^sub>\<circ> k) = k
[PROOF STEP]
by
    (
      simp add:
        OrdmemD
        inf_absorb2
        order.strict_implies_order
        vdomain_vlrestriction
        vfsequence_vdomain
    )


[STATEMENT]
lemma (in vfsequence) vfsequence_vlrestriction_vcard[simp]:
  "xs \<restriction>\<^sup>l\<^sub>\<circ> (vcard xs) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<restriction>\<^sup>l\<^sub>\<circ> vcard xs = xs
[PROOF STEP]
by (rule vlrestriction_vdomain[unfolded vfsequence_vdomain])


[STATEMENT]
lemma vfsequence_vfinite_vcardI:
  assumes "vsv xs" and "vfinite xs" and "\<D>\<^sub>\<circ> xs = vcard xs"
  shows "vfsequence xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vsv xs
vfinite xs
\<D>\<^sub>\<circ> xs = vcard xs

goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (intro vfsequenceI) (auto simp: vfinite_vcard_omega)


[STATEMENT]
lemma (in vfsequence) vfsequence_vrangeE:
  assumes "a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xs"
  obtains n where "n \<in>\<^sub>\<circ> vcard xs" and "xs\<lparr>n\<rparr> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<in>\<^sub>\<circ> vcard xs; xs\<lparr>n\<rparr> = a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms vfsequence_vdomain
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> xs
\<D>\<^sub>\<circ> xs = vcard xs

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<in>\<^sub>\<circ> vcard xs; xs\<lparr>n\<rparr> = a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto