[STATEMENT]
theorem close_closed: \<open>subset_closed (close C)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subset_closed (close C)
[PROOF STEP]
unfolding close_def subset_closed_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S'\<in>{S. Bex C ((\<subseteq>) S)}. \<forall>S\<subseteq>S'. S \<in> {S. Bex C ((\<subseteq>) S)}
[PROOF STEP]
by blast


[STATEMENT]
theorem mk_alt_consistency_closed:
  assumes \<open>subset_closed C\<close>
  shows \<open>subset_closed (mk_alt_consistency C)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subset_closed (mk_alt_consistency C)
[PROOF STEP]
unfolding subset_closed_def mk_alt_consistency_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S'\<in>{S. \<exists>f. psubst f ` S \<in> C}. \<forall>S\<subseteq>S'. S \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
proof (intro ballI allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>S' \<in> {S. \<exists>f. psubst f ` S \<in> C}; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
fix S S' :: \<open>('a, 'b) form set\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>S' \<in> {S. \<exists>f. psubst f ` S \<in> C}; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
assume \<open>S \<subseteq> S'\<close> and \<open>S' \<in> {S. \<exists>f. psubst f ` S \<in> C}\<close>
[PROOF STATE]
proof (state)
this:
S \<subseteq> S'
S' \<in> {S. \<exists>f. psubst f ` S \<in> C}

goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>S' \<in> {S. \<exists>f. psubst f ` S \<in> C}; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> S'
S' \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
obtain f where *: \<open>psubst f ` S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> S'
S' \<in> {S. \<exists>f. psubst f ` S \<in> C}

goal (1 subgoal):
 1. (\<And>f. psubst f ` S' \<in> C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
psubst f ` S' \<in> C

goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>S' \<in> {S. \<exists>f. psubst f ` S \<in> C}; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
psubst f ` S' \<in> C

goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>S' \<in> {S. \<exists>f. psubst f ` S \<in> C}; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
have \<open>psubst f ` S \<subseteq> psubst f ` S'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst f ` S \<subseteq> psubst f ` S'
[PROOF STEP]
using \<open>S \<subseteq> S'\<close>
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> S'

goal (1 subgoal):
 1. psubst f ` S \<subseteq> psubst f ` S'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
psubst f ` S \<subseteq> psubst f ` S'

goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>S' \<in> {S. \<exists>f. psubst f ` S \<in> C}; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
psubst f ` S \<subseteq> psubst f ` S'

goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>S' \<in> {S. \<exists>f. psubst f ` S \<in> C}; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
have \<open>\<forall>S' \<in> C. \<forall>S \<subseteq> S'. S \<in> C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
using \<open>subset_closed C\<close>
[PROOF STATE]
proof (prove)
using this:
subset_closed C

goal (1 subgoal):
 1. \<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
unfolding subset_closed_def
[PROOF STATE]
proof (prove)
using this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C

goal (1 subgoal):
 1. \<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C

goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>S' \<in> {S. \<exists>f. psubst f ` S \<in> C}; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
psubst f ` S' \<in> C
psubst f ` S \<subseteq> psubst f ` S'
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C
[PROOF STEP]
have \<open>psubst f ` S \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
psubst f ` S' \<in> C
psubst f ` S \<subseteq> psubst f ` S'
\<forall>S'\<in>C. \<forall>S\<subseteq>S'. S \<in> C

goal (1 subgoal):
 1. psubst f ` S \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
psubst f ` S \<in> C

goal (1 subgoal):
 1. \<And>S' S. \<lbrakk>S' \<in> {S. \<exists>f. psubst f ` S \<in> C}; S \<subseteq> S'\<rbrakk> \<Longrightarrow> S \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
psubst f ` S \<in> C
[PROOF STEP]
show \<open>S \<in> {S. \<exists>f. psubst f ` S \<in> C}\<close>
[PROOF STATE]
proof (prove)
using this:
psubst f ` S \<in> C

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

goal:
No subgoals!
[PROOF STEP]
qed