[STATEMENT]
lemma HC_consistent:  "pcp {\<Gamma>| \<Gamma>. \<not>(\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcp {\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)}
[PROOF STEP]
unfolding pcp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S\<in>{\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)}. \<bottom> \<notin> S \<and> (\<forall>k. Atom k \<in> S \<longrightarrow> \<^bold>\<not> (Atom k) \<in> S \<longrightarrow> False) \<and> (\<forall>F G. F \<^bold>\<and> G \<in> S \<longrightarrow> F \<triangleright> G \<triangleright> S \<in> {\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)}) \<and> (\<forall>F G. F \<^bold>\<or> G \<in> S \<longrightarrow> F \<triangleright> S \<in> {\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)} \<or> G \<triangleright> S \<in> {\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)}) \<and> (\<forall>F G. F \<^bold>\<rightarrow> G \<in> S \<longrightarrow> \<^bold>\<not> F \<triangleright> S \<in> {\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)} \<or> G \<triangleright> S \<in> {\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)}) \<and> (\<forall>F. \<^bold>\<not> (\<^bold>\<not> F) \<in> S \<longrightarrow> F \<triangleright> S \<in> {\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)}) \<and> (\<forall>F G. \<^bold>\<not> (F \<^bold>\<and> G) \<in> S \<longrightarrow> \<^bold>\<not> F \<triangleright> S \<in> {\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)} \<or> \<^bold>\<not> G \<triangleright> S \<in> {\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)}) \<and> (\<forall>F G. \<^bold>\<not> (F \<^bold>\<or> G) \<in> S \<longrightarrow> \<^bold>\<not> F \<triangleright> \<^bold>\<not> G \<triangleright> S \<in> {\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)}) \<and> (\<forall>F G. \<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> S \<longrightarrow> F \<triangleright> \<^bold>\<not> G \<triangleright> S \<in> {\<Gamma> |\<Gamma>. \<not> (\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>)})
[PROOF STEP]
apply(intro ballI conjI; unfold mem_Collect_eq; elim exE conjE; erule contrapos_np; clarsimp)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>S. \<bottom> \<in> S \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 2. \<And>S k. \<lbrakk>Atom k \<in> S; \<^bold>\<not> (Atom k) \<in> S\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 3. \<And>S F G. \<lbrakk>F \<^bold>\<and> G \<in> S; F \<triangleright> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 4. \<And>S F G. \<lbrakk>F \<^bold>\<or> G \<in> S; F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 5. \<And>S F G. \<lbrakk>F \<^bold>\<rightarrow> G \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 6. \<And>S F. \<lbrakk>\<^bold>\<not> (\<^bold>\<not> F) \<in> S; F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 7. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<and> G) \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 8. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<or> G) \<in> S; \<^bold>\<not> F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 9. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> S; F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> \<in> S_ \<Longrightarrow> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (simp add: HC.Ax)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>S k. \<lbrakk>Atom k \<in> S; \<^bold>\<not> (Atom k) \<in> S\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 2. \<And>S F G. \<lbrakk>F \<^bold>\<and> G \<in> S; F \<triangleright> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 3. \<And>S F G. \<lbrakk>F \<^bold>\<or> G \<in> S; F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 4. \<And>S F G. \<lbrakk>F \<^bold>\<rightarrow> G \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 5. \<And>S F. \<lbrakk>\<^bold>\<not> (\<^bold>\<not> F) \<in> S; F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 6. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<and> G) \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 7. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<or> G) \<in> S; \<^bold>\<not> F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 8. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> S; F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Atom k_ \<in> S_; \<^bold>\<not> (Atom k_) \<in> S_\<rbrakk> \<Longrightarrow> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (meson Ax HC_intros(12) HC_mono MP Un_upper1 sup_ge2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>S F G. \<lbrakk>F \<^bold>\<and> G \<in> S; F \<triangleright> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 2. \<And>S F G. \<lbrakk>F \<^bold>\<or> G \<in> S; F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 3. \<And>S F G. \<lbrakk>F \<^bold>\<rightarrow> G \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 4. \<And>S F. \<lbrakk>\<^bold>\<not> (\<^bold>\<not> F) \<in> S; F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 5. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<and> G) \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 6. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<or> G) \<in> S; \<^bold>\<not> F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 7. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> S; F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F_ \<^bold>\<and> G_ \<in> S_; F_ \<triangleright> G_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
using sim_conj
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?F \<triangleright> ?G \<triangleright> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?H; ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?F; ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?G\<rbrakk> \<Longrightarrow> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?H

goal (1 subgoal):
 1. \<lbrakk>F_ \<^bold>\<and> G_ \<in> S_; F_ \<triangleright> G_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (metis (no_types, lifting) Ax HC_intros(8) HC_intros(9) HC_mono MP sup_ge1 sup_ge2)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>S F G. \<lbrakk>F \<^bold>\<or> G \<in> S; F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 2. \<And>S F G. \<lbrakk>F \<^bold>\<rightarrow> G \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 3. \<And>S F. \<lbrakk>\<^bold>\<not> (\<^bold>\<not> F) \<in> S; F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 4. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<and> G) \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 5. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<or> G) \<in> S; \<^bold>\<not> F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 6. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> S; F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F_ \<^bold>\<or> G_ \<in> S_; F_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
using sim_disj
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?F \<triangleright> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?H; ?G \<triangleright> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?H; ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?F \<^bold>\<or> ?G\<rbrakk> \<Longrightarrow> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?H

goal (1 subgoal):
 1. \<lbrakk>F_ \<^bold>\<or> G_ \<in> S_; F_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
using Ax
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?F \<triangleright> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?H; ?G \<triangleright> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?H; ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?F \<^bold>\<or> ?G\<rbrakk> \<Longrightarrow> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?H
?F \<in> ?\<Gamma> \<Longrightarrow> ?\<Gamma> \<turnstile>\<^sub>H ?F

goal (1 subgoal):
 1. \<lbrakk>F_ \<^bold>\<or> G_ \<in> S_; F_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>S F G. \<lbrakk>F \<^bold>\<rightarrow> G \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 2. \<And>S F. \<lbrakk>\<^bold>\<not> (\<^bold>\<not> F) \<in> S; F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 3. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<and> G) \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 4. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<or> G) \<in> S; \<^bold>\<not> F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 5. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> S; F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F_ \<^bold>\<rightarrow> G_ \<in> S_; \<^bold>\<not> F_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>; G_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (erule (1) sim_disj) (simp add: Ax imp_sim)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>S F. \<lbrakk>\<^bold>\<not> (\<^bold>\<not> F) \<in> S; F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 2. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<and> G) \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 3. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<or> G) \<in> S; \<^bold>\<not> F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 4. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> S; F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<^bold>\<not> (\<^bold>\<not> F_) \<in> S_; F_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (metis Ax HC_contrapos_nn MP Un_iff Un_insert_left dt inpcp someax)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<and> G) \<in> S; \<^bold>\<not> F \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>; \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 2. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<or> G) \<in> S; \<^bold>\<not> F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 3. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> S; F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<^bold>\<not> (F_ \<^bold>\<and> G_) \<in> S_; \<^bold>\<not> F_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>; \<^bold>\<not> G_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by(erule (1) sim_disj) (simp add: Ax nand_sim)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<or> G) \<in> S; \<^bold>\<not> F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
 2. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> S; F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<^bold>\<not> (F_ \<^bold>\<or> G_) \<in> S_; \<^bold>\<not> F_ \<triangleright> \<^bold>\<not> G_ \<triangleright> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S_ \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by(erule  sim_conj) (meson Ax Un_iff nor_sim)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S F G. \<lbrakk>\<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> S; F \<triangleright> \<^bold>\<not> G \<triangleright> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> S \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
subgoal for \<Gamma> F G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> \<Gamma>; F \<triangleright> \<^bold>\<not> G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
apply(erule sim_conj)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> \<Gamma> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F
 2. \<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> \<Gamma> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> \<Gamma> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F
[PROOF STEP]
by (meson Ax HC_Compl_Consistency.not_imp HC_contrapos_np Un_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> \<Gamma> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<not> (F \<^bold>\<rightarrow> G) \<in> \<Gamma> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G
[PROOF STEP]
by (metis Ax HC_contrapos_nn HC_intros(3) HC_mono sup_ge1 sup_ge2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma isTrue_neg_excl:
"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow>
 isTrue \<phi> \<Longrightarrow> isTrue (neg \<phi>) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; isTrue \<phi>; isTrue (neg \<phi>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using isTrue_imp not_isTrue_fls
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<psi> \<in> fmla; Fvars ?\<phi> = {}; Fvars ?\<psi> = {}; isTrue ?\<phi>; isTrue (imp ?\<phi> ?\<psi>)\<rbrakk> \<Longrightarrow> isTrue ?\<psi>
\<not> isTrue fls

goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; isTrue \<phi>; isTrue (neg \<phi>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding neg_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<psi> \<in> fmla; Fvars ?\<phi> = {}; Fvars ?\<psi> = {}; isTrue ?\<phi>; isTrue (imp ?\<phi> ?\<psi>)\<rbrakk> \<Longrightarrow> isTrue ?\<psi>
\<not> isTrue fls

goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; isTrue \<phi>; isTrue (imp \<phi> fls)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by auto


[STATEMENT]
lemma isTrue_neg_neg:
assumes "\<phi> \<in> fmla" "Fvars \<phi> = {}"
and "isTrue (neg (neg \<phi>))"
shows "isTrue \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isTrue \<phi>
[PROOF STEP]
using assms isTrue_neg isTrue_neg_excl
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
Fvars \<phi> = {}
isTrue (neg (neg \<phi>))
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}\<rbrakk> \<Longrightarrow> isTrue ?\<phi> \<or> isTrue (neg ?\<phi>)
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}; isTrue ?\<phi>; isTrue (neg ?\<phi>)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. isTrue \<phi>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma consistent: consistent
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> prv fls
[PROOF STEP]
using not_isTrue_fls sound_isTrue
[PROOF STATE]
proof (prove)
using this:
\<not> isTrue fls
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}; prv ?\<phi>\<rbrakk> \<Longrightarrow> isTrue ?\<phi>

goal (1 subgoal):
 1. \<not> prv fls
[PROOF STEP]
by blast


[STATEMENT]
lemma prv_neg_excl:
"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv \<phi> \<Longrightarrow> prv (neg \<phi>) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; prv \<phi>; prv (neg \<phi>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using isTrue_neg_excl[of \<phi>] sound_isTrue
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; isTrue \<phi>; isTrue (neg \<phi>)\<rbrakk> \<Longrightarrow> False
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}; prv ?\<phi>\<rbrakk> \<Longrightarrow> isTrue ?\<phi>

goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; prv \<phi>; prv (neg \<phi>)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by auto


[STATEMENT]
lemma prv_imp_implies_isTrue:
assumes [simp]: "\<phi> \<in> fmla" "\<chi> \<in> fmla" "Fvars \<phi> = {}" "Fvars \<chi> = {}"
and p: "prv (imp \<phi> \<chi>)" and i: "isTrue \<phi>"
shows "isTrue \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isTrue \<chi>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isTrue \<chi>
[PROOF STEP]
have "isTrue (imp \<phi> \<chi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isTrue (imp \<phi> \<chi>)
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi> \<chi>)

goal (1 subgoal):
 1. isTrue (imp \<phi> \<chi>)
[PROOF STEP]
by (intro sound_isTrue) auto
[PROOF STATE]
proof (state)
this:
isTrue (imp \<phi> \<chi>)

goal (1 subgoal):
 1. isTrue \<chi>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
isTrue (imp \<phi> \<chi>)

goal (1 subgoal):
 1. isTrue \<chi>
[PROOF STEP]
using assms isTrue_imp
[PROOF STATE]
proof (prove)
using this:
isTrue (imp \<phi> \<chi>)
\<phi> \<in> fmla
\<chi> \<in> fmla
Fvars \<phi> = {}
Fvars \<chi> = {}
prv (imp \<phi> \<chi>)
isTrue \<phi>
\<lbrakk>?\<phi> \<in> fmla; ?\<psi> \<in> fmla; Fvars ?\<phi> = {}; Fvars ?\<psi> = {}; isTrue ?\<phi>; isTrue (imp ?\<phi> ?\<psi>)\<rbrakk> \<Longrightarrow> isTrue ?\<psi>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<omega>consistent: \<omega>consistent
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>consistent
[PROOF STEP]
unfolding \<omega>consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. prv (neg (subst \<phi> n x))) \<longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
proof (safe del: notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
fix \<phi> x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
assume 0[simp,intro]: "\<phi> \<in> fmla"  "x \<in> var" and 1: "Fvars \<phi> = {x}"
  and 00: "\<forall>n\<in>num. prv (neg (subst \<phi> n x))"
[PROOF STATE]
proof (state)
this:
\<phi> \<in> fmla
x \<in> var
Fvars \<phi> = {x}
\<forall>n\<in>num. prv (neg (subst \<phi> n x))

goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
hence "\<forall>n\<in>num. isTrue (neg (subst \<phi> n x))"
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
x \<in> var
Fvars \<phi> = {x}
\<forall>n\<in>num. prv (neg (subst \<phi> n x))

goal (1 subgoal):
 1. \<forall>n\<in>num. isTrue (neg (subst \<phi> n x))
[PROOF STEP]
using 00 1
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
x \<in> var
Fvars \<phi> = {x}
\<forall>n\<in>num. prv (neg (subst \<phi> n x))
\<forall>n\<in>num. prv (neg (subst \<phi> n x))
Fvars \<phi> = {x}

goal (1 subgoal):
 1. \<forall>n\<in>num. isTrue (neg (subst \<phi> n x))
[PROOF STEP]
by (auto intro!: sound_isTrue)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>num. isTrue (neg (subst \<phi> n x))

goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
hence "isTrue (all x (neg \<phi>))"
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>num. isTrue (neg (subst \<phi> n x))

goal (1 subgoal):
 1. isTrue (all x (neg \<phi>))
[PROOF STEP]
by (simp add: "1" isTrue_all)
[PROOF STATE]
proof (state)
this:
isTrue (all x (neg \<phi>))

goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
isTrue (all x (neg \<phi>))

goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
isTrue (all x (neg \<phi>))

goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
have "prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))
[PROOF STEP]
using prv_all_neg_imp_neg_exi
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> var; ?\<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (all ?x (neg ?\<phi>)) (neg (exi ?x ?\<phi>)))

goal (1 subgoal):
 1. prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))

goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
hence "isTrue (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))"
[PROOF STATE]
proof (prove)
using this:
prv (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))

goal (1 subgoal):
 1. isTrue (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))
[PROOF STEP]
by (simp add: "1" sound_isTrue)
[PROOF STATE]
proof (state)
this:
isTrue (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))

goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
isTrue (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))

goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
isTrue (all x (neg \<phi>))
isTrue (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))
[PROOF STEP]
have "isTrue (neg (exi x \<phi>))"
[PROOF STATE]
proof (prove)
using this:
isTrue (all x (neg \<phi>))
isTrue (imp (all x (neg \<phi>)) (neg (exi x \<phi>)))

goal (1 subgoal):
 1. isTrue (neg (exi x \<phi>))
[PROOF STEP]
by (metis 0 1 Diff_insert_absorb Fvars_all Fvars_exi Fvars_neg all
      exi insert_absorb insert_not_empty isTrue_imp neg)
[PROOF STATE]
proof (state)
this:
isTrue (neg (exi x \<phi>))

goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
hence "\<not> isTrue (neg (neg (exi x \<phi>)))"
[PROOF STATE]
proof (prove)
using this:
isTrue (neg (exi x \<phi>))

goal (1 subgoal):
 1. \<not> isTrue (neg (neg (exi x \<phi>)))
[PROOF STEP]
using 1 isTrue_neg_excl
[PROOF STATE]
proof (prove)
using this:
isTrue (neg (exi x \<phi>))
Fvars \<phi> = {x}
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}; isTrue ?\<phi>; isTrue (neg ?\<phi>)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> isTrue (neg (neg (exi x \<phi>)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<not> isTrue (neg (neg (exi x \<phi>)))

goal (1 subgoal):
 1. \<And>\<phi> x. \<lbrakk>\<phi> \<in> fmla; x \<in> var; Fvars \<phi> = {x}; \<forall>n\<in>num. prv (neg (subst \<phi> n x))\<rbrakk> \<Longrightarrow> \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
thus "\<not> prv (neg (neg (exi x \<phi>)))"
[PROOF STATE]
proof (prove)
using this:
\<not> isTrue (neg (neg (exi x \<phi>)))

goal (1 subgoal):
 1. \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
using "1" sound_isTrue
[PROOF STATE]
proof (prove)
using this:
\<not> isTrue (neg (neg (exi x \<phi>)))
Fvars \<phi> = {x}
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}; prv ?\<phi>\<rbrakk> \<Longrightarrow> isTrue ?\<phi>

goal (1 subgoal):
 1. \<not> prv (neg (neg (exi x \<phi>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> prv (neg (neg (exi x \<phi>)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<omega>consistentStd1: \<omega>consistentStd1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>consistentStd1
[PROOF STEP]
using \<omega>consistent \<omega>consistent_impliesStd1
[PROOF STATE]
proof (prove)
using this:
\<omega>consistent
\<omega>consistent \<Longrightarrow> \<omega>consistentStd1

goal (1 subgoal):
 1. \<omega>consistentStd1
[PROOF STEP]
by blast


[STATEMENT]
lemma \<omega>consistentStd2: \<omega>consistentStd2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>consistentStd2
[PROOF STEP]
using \<omega>consistent \<omega>consistent_impliesStd2
[PROOF STATE]
proof (prove)
using this:
\<omega>consistent
\<omega>consistent \<Longrightarrow> \<omega>consistentStd2

goal (1 subgoal):
 1. \<omega>consistentStd2
[PROOF STEP]
by blast


[STATEMENT]
lemma (in Yoneda) F_into_set:
  "Functor F : AA \<longrightarrow> Set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Functor F : AA \<longrightarrow> Set
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Functor F : AA \<longrightarrow> Set
[PROOF STEP]
from F_axioms
[PROOF STATE]
proof (chain)
picking this:
F \<^bsub>\<a>\<^esub> \<in> Ar \<rightarrow> Ar\<^bsub>BB\<^esub>
F \<^bsub>\<o>\<^esub> \<in> Ob \<rightarrow> Ob\<^bsub>BB\<^esub>
preserves_dom F
preserves_cod F
preserves_id F
preserves_comp F
[PROOF STEP]
have "Functor F : AA \<longrightarrow> BB"
[PROOF STATE]
proof (prove)
using this:
F \<^bsub>\<a>\<^esub> \<in> Ar \<rightarrow> Ar\<^bsub>BB\<^esub>
F \<^bsub>\<o>\<^esub> \<in> Ob \<rightarrow> Ob\<^bsub>BB\<^esub>
preserves_dom F
preserves_cod F
preserves_id F
preserves_comp F

goal (1 subgoal):
 1. Functor F : AA \<longrightarrow> BB
[PROOF STEP]
by intro_locales
[PROOF STATE]
proof (state)
this:
Functor F : AA \<longrightarrow> BB

goal (1 subgoal):
 1. Functor F : AA \<longrightarrow> Set
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Functor F : AA \<longrightarrow> BB

goal (1 subgoal):
 1. Functor F : AA \<longrightarrow> Set
[PROOF STEP]
by (simp only: BB_Set)
[PROOF STATE]
proof (state)
this:
Functor F : AA \<longrightarrow> Set

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Yoneda) F_comp_func:
  assumes 1: "A \<in> Ob" and 2: "B \<in> Ob" and 3: "C \<in> Ob"
  and 4: "g \<in> Hom A B" and 5: "f \<in> Hom B C"
  shows "set_func (F\<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F\<^bsub>\<o>\<^esub> A) (set_func (F\<^bsub>\<a>\<^esub> f)) (set_func (F\<^bsub>\<a>\<^esub> g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))
[PROOF STEP]
from 4 and 5
[PROOF STATE]
proof (chain)
picking this:
g \<in> Hom A B
f \<in> Hom B C
[PROOF STEP]
have 7: "Cod g = Dom f"
    and 8: "g \<in> Ar"
    and 9: "f \<in> Ar"
    and 10: "Dom g = A"
[PROOF STATE]
proof (prove)
using this:
g \<in> Hom A B
f \<in> Hom B C

goal (1 subgoal):
 1. (Cod g = Dom f &&& g \<in> Ar) &&& f \<in> Ar &&& Dom g = A
[PROOF STEP]
by (simp_all add: hom_def)
[PROOF STATE]
proof (state)
this:
Cod g = Dom f
g \<in> Ar
f \<in> Ar
Dom g = A

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))
[PROOF STEP]
from F_preserves_dom and 8 and 10
[PROOF STATE]
proof (chain)
picking this:
preserves_dom F
g \<in> Ar
Dom g = A
[PROOF STEP]
have 11: "set_dom (F\<^bsub>\<a>\<^esub> g) = F\<^bsub>\<o>\<^esub> A"
[PROOF STATE]
proof (prove)
using this:
preserves_dom F
g \<in> Ar
Dom g = A

goal (1 subgoal):
 1. set_dom (F \<^bsub>\<a>\<^esub> g) = F \<^bsub>\<o>\<^esub> A
[PROOF STEP]
by (simp add: preserves_dom_def BB_Set Set_def) auto
[PROOF STATE]
proof (state)
this:
set_dom (F \<^bsub>\<a>\<^esub> g) = F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))
[PROOF STEP]
from F_preserves_comp and 7 and 8 and 9
[PROOF STATE]
proof (chain)
picking this:
preserves_comp F
Cod g = Dom f
g \<in> Ar
f \<in> Ar
[PROOF STEP]
have "F\<^bsub>\<a>\<^esub> (f \<bullet> g) = (F\<^bsub>\<a>\<^esub> f) \<bullet>\<^bsub>BB\<^esub> (F\<^bsub>\<a>\<^esub> g)"
[PROOF STATE]
proof (prove)
using this:
preserves_comp F
Cod g = Dom f
g \<in> Ar
f \<in> Ar

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> (f \<bullet> g) = F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>BB\<^esub> F \<^bsub>\<a>\<^esub> g
[PROOF STEP]
by (simp add: preserves_comp_def)
[PROOF STATE]
proof (state)
this:
F \<^bsub>\<a>\<^esub> (f \<bullet> g) = F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>BB\<^esub> F \<^bsub>\<a>\<^esub> g

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))
[PROOF STEP]
hence "set_func (F\<^bsub>\<a>\<^esub> (f \<bullet> g))  = set_func ((F\<^bsub>\<a>\<^esub> f) \<odot> (F\<^bsub>\<a>\<^esub> g))"
[PROOF STATE]
proof (prove)
using this:
F \<^bsub>\<a>\<^esub> (f \<bullet> g) = F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>BB\<^esub> F \<^bsub>\<a>\<^esub> g

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = set_func (F \<^bsub>\<a>\<^esub> f \<odot> F \<^bsub>\<a>\<^esub> g)
[PROOF STEP]
by (simp add: BB_Set Set_def)
[PROOF STATE]
proof (state)
this:
set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = set_func (F \<^bsub>\<a>\<^esub> f \<odot> F \<^bsub>\<a>\<^esub> g)

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = set_func (F \<^bsub>\<a>\<^esub> f \<odot> F \<^bsub>\<a>\<^esub> g)

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))
[PROOF STEP]
have "\<dots> = compose (F\<^bsub>\<o>\<^esub> A) (set_func (F\<^bsub>\<a>\<^esub> f)) (set_func (F\<^bsub>\<a>\<^esub> g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> f \<odot> F \<^bsub>\<a>\<^esub> g) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))
[PROOF STEP]
by (simp add: set_comp_def 11)
[PROOF STATE]
proof (state)
this:
set_func (F \<^bsub>\<a>\<^esub> f \<odot> F \<^bsub>\<a>\<^esub> g) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) = compose (F \<^bsub>\<o>\<^esub> A) (set_func (F \<^bsub>\<a>\<^esub> f)) (set_func (F \<^bsub>\<a>\<^esub> g))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Yoneda) sandwich_funcset:
  assumes A: "A \<in> Ob"
  and "a \<in> F\<^bsub>\<o>\<^esub> A"
  shows  "\<sigma>(A,a) : Ob \<rightarrow> ar Set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
proof (rule funcsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,a) x \<in> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,a) x \<in> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
assume B: "B \<in> Ob"
[PROOF STATE]
proof (state)
this:
B \<in> Ob

goal (1 subgoal):
 1. \<And>x. x \<in> Ob \<Longrightarrow> \<sigma>(A,a) x \<in> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
thus "\<sigma>(A,a) B \<in> ar Set"
[PROOF STATE]
proof (prove)
using this:
B \<in> Ob

goal (1 subgoal):
 1. \<sigma>(A,a) B \<in> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
proof (simp add: Set_def sandwich_def set_cat_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B \<in> Ob \<Longrightarrow> set_arrow U \<lparr>set_dom = Hom A B, set_func = \<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) a, set_cod = F \<^bsub>\<o>\<^esub> B\<rparr>
[PROOF STEP]
show "set_arrow U \<lparr>
      set_dom = Hom A B,
      set_func = \<lambda>f\<in>Hom A B. set_func (F\<^bsub>\<a>\<^esub> f) a,
      set_cod = F\<^bsub>\<o>\<^esub> B\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_arrow U \<lparr>set_dom = Hom A B, set_func = \<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) a, set_cod = F \<^bsub>\<o>\<^esub> B\<rparr>
[PROOF STEP]
proof (simp add: set_arrow_def, intro conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Hom A B \<subseteq> U
 2. F \<^bsub>\<o>\<^esub> B \<subseteq> U
 3. (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) a) \<in> Hom A B \<rightarrow> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
show "Hom A B \<subseteq> U" and "F\<^bsub>\<o>\<^esub> B \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hom A B \<subseteq> U &&& F \<^bsub>\<o>\<^esub> B \<subseteq> U
[PROOF STEP]
by (simp_all add: U_def)
[PROOF STATE]
proof (state)
this:
Hom A B \<subseteq> U
F \<^bsub>\<o>\<^esub> B \<subseteq> U

goal (1 subgoal):
 1. (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) a) \<in> Hom A B \<rightarrow> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
show "(\<lambda>f\<in>Hom A B. set_func (F\<^bsub>\<a>\<^esub> f) a) \<in> Hom A B \<rightarrow> F\<^bsub>\<o>\<^esub> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) a) \<in> Hom A B \<rightarrow> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
proof (rule funcsetI, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> set_func (F \<^bsub>\<a>\<^esub> x) a \<in> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> set_func (F \<^bsub>\<a>\<^esub> x) a \<in> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
assume f: "f \<in> Hom A B"
[PROOF STATE]
proof (state)
this:
f \<in> Hom A B

goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> set_func (F \<^bsub>\<a>\<^esub> x) a \<in> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
with A B
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
B \<in> Ob
f \<in> Hom A B
[PROOF STEP]
have "F\<^bsub>\<a>\<^esub> f \<in> Hom\<^bsub>BB\<^esub> (F\<^bsub>\<o>\<^esub> A) (F\<^bsub>\<o>\<^esub> B)"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
B \<in> Ob
f \<in> Hom A B

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<in> Hom\<^bsub>BB\<^esub> F \<^bsub>\<o>\<^esub> A F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
by (rule functors_preserve_homsets)
[PROOF STATE]
proof (state)
this:
F \<^bsub>\<a>\<^esub> f \<in> Hom\<^bsub>BB\<^esub> F \<^bsub>\<o>\<^esub> A F \<^bsub>\<o>\<^esub> B

goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> set_func (F \<^bsub>\<a>\<^esub> x) a \<in> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
hence "F\<^bsub>\<a>\<^esub> f \<in> ar Set"
          and "set_dom (F\<^bsub>\<a>\<^esub> f) = (F\<^bsub>\<o>\<^esub> A)"
          and "set_cod (F\<^bsub>\<a>\<^esub> f) = (F\<^bsub>\<o>\<^esub> B)"
[PROOF STATE]
proof (prove)
using this:
F \<^bsub>\<a>\<^esub> f \<in> Hom\<^bsub>BB\<^esub> F \<^bsub>\<o>\<^esub> A F \<^bsub>\<o>\<^esub> B

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<in> Ar\<^bsub>Set\<^esub> &&& set_dom (F \<^bsub>\<a>\<^esub> f) = F \<^bsub>\<o>\<^esub> A &&& set_cod (F \<^bsub>\<a>\<^esub> f) = F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
by (simp_all add: hom_def BB_Set Set_def)
[PROOF STATE]
proof (state)
this:
F \<^bsub>\<a>\<^esub> f \<in> Ar\<^bsub>Set\<^esub>
set_dom (F \<^bsub>\<a>\<^esub> f) = F \<^bsub>\<o>\<^esub> A
set_cod (F \<^bsub>\<a>\<^esub> f) = F \<^bsub>\<o>\<^esub> B

goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> set_func (F \<^bsub>\<a>\<^esub> x) a \<in> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
hence "set_func (F\<^bsub>\<a>\<^esub> f) : (F\<^bsub>\<o>\<^esub> A) \<rightarrow> (F\<^bsub>\<o>\<^esub> B)"
[PROOF STATE]
proof (prove)
using this:
F \<^bsub>\<a>\<^esub> f \<in> Ar\<^bsub>Set\<^esub>
set_dom (F \<^bsub>\<a>\<^esub> f) = F \<^bsub>\<o>\<^esub> A
set_cod (F \<^bsub>\<a>\<^esub> f) = F \<^bsub>\<o>\<^esub> B

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> f) \<in> F \<^bsub>\<o>\<^esub> A \<rightarrow> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
by (simp add: Set_def set_cat_def set_arrow_def)
[PROOF STATE]
proof (state)
this:
set_func (F \<^bsub>\<a>\<^esub> f) \<in> F \<^bsub>\<o>\<^esub> A \<rightarrow> F \<^bsub>\<o>\<^esub> B

goal (1 subgoal):
 1. \<And>x. x \<in> Hom A B \<Longrightarrow> set_func (F \<^bsub>\<a>\<^esub> x) a \<in> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
thus "set_func (F\<^bsub>\<a>\<^esub> f) a \<in> F\<^bsub>\<o>\<^esub> B"
[PROOF STATE]
proof (prove)
using this:
set_func (F \<^bsub>\<a>\<^esub> f) \<in> F \<^bsub>\<o>\<^esub> A \<rightarrow> F \<^bsub>\<o>\<^esub> B

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> f) a \<in> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
using \<open>a \<in> F\<^bsub>\<o>\<^esub> A\<close>
[PROOF STATE]
proof (prove)
using this:
set_func (F \<^bsub>\<a>\<^esub> f) \<in> F \<^bsub>\<o>\<^esub> A \<rightarrow> F \<^bsub>\<o>\<^esub> B
a \<in> F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> f) a \<in> F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
by (rule funcset_mem)
[PROOF STATE]
proof (state)
this:
set_func (F \<^bsub>\<a>\<^esub> f) a \<in> F \<^bsub>\<o>\<^esub> B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) a) \<in> Hom A B \<rightarrow> F \<^bsub>\<o>\<^esub> B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_arrow U \<lparr>set_dom = Hom A B, set_func = \<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) a, set_cod = F \<^bsub>\<o>\<^esub> B\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<sigma>(A,a) B \<in> Ar\<^bsub>Set\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Yoneda) sandwich_type:
  assumes A: "A \<in> Ob" and B: "B \<in> Ob"
  and "a \<in> F\<^bsub>\<o>\<^esub> A"
  shows "\<sigma>(A,a) B \<in> hom Set (Hom A B) (F\<^bsub>\<o>\<^esub> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>(A,a) B \<in> Hom\<^bsub>Set\<^esub> (Hom A B) F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma>(A,a) B \<in> Hom\<^bsub>Set\<^esub> (Hom A B) F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
have "\<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
using A and \<open>a \<in> F\<^bsub>\<o>\<^esub> A\<close>
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
a \<in> F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. \<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
by (rule sandwich_funcset)
[PROOF STATE]
proof (state)
this:
\<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>

goal (1 subgoal):
 1. \<sigma>(A,a) B \<in> Hom\<^bsub>Set\<^esub> (Hom A B) F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
hence "\<sigma>(A,a) B \<in> ar Set"
[PROOF STATE]
proof (prove)
using this:
\<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>

goal (1 subgoal):
 1. \<sigma>(A,a) B \<in> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
\<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
B \<in> Ob

goal (1 subgoal):
 1. \<sigma>(A,a) B \<in> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
by (rule funcset_mem)
[PROOF STATE]
proof (state)
this:
\<sigma>(A,a) B \<in> Ar\<^bsub>Set\<^esub>

goal (1 subgoal):
 1. \<sigma>(A,a) B \<in> Hom\<^bsub>Set\<^esub> (Hom A B) F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<sigma>(A,a) B \<in> Ar\<^bsub>Set\<^esub>

goal (1 subgoal):
 1. \<sigma>(A,a) B \<in> Hom\<^bsub>Set\<^esub> (Hom A B) F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
\<sigma>(A,a) B \<in> Ar\<^bsub>Set\<^esub>
B \<in> Ob

goal (1 subgoal):
 1. \<sigma>(A,a) B \<in> Hom\<^bsub>Set\<^esub> (Hom A B) F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
by (simp add: sandwich_def hom_def Set_def)
[PROOF STATE]
proof (state)
this:
\<sigma>(A,a) B \<in> Hom\<^bsub>Set\<^esub> (Hom A B) F \<^bsub>\<o>\<^esub> B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Yoneda) sandwich_commutes:
  assumes AOb: "A \<in> Ob" and BOb: "B \<in> Ob" and COb: "C \<in> Ob"
  and aFa: "a \<in> F\<^bsub>\<o>\<^esub> A"
  and fBC: "f \<in> Hom B C"
  shows "(F\<^bsub>\<a>\<^esub> f) \<odot> (\<sigma>(A,a) B) = (\<sigma>(A,a) C) \<odot> (Hom(A,_)\<^bsub>\<a>\<^esub> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
from fBC
[PROOF STATE]
proof (chain)
picking this:
f \<in> Hom B C
[PROOF STEP]
have 1: "f \<in> Ar" and 2: "Dom f = B" and 3: "Cod f = C"
[PROOF STATE]
proof (prove)
using this:
f \<in> Hom B C

goal (1 subgoal):
 1. f \<in> Ar &&& Dom f = B &&& Cod f = C
[PROOF STEP]
by (simp_all add: hom_def)
[PROOF STATE]
proof (state)
this:
f \<in> Ar
Dom f = B
Cod f = C

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
from BOb
[PROOF STATE]
proof (chain)
picking this:
B \<in> Ob
[PROOF STEP]
have "set_dom ((F\<^bsub>\<a>\<^esub> f) \<odot> (\<sigma>(A,a) B)) = Hom A B"
[PROOF STATE]
proof (prove)
using this:
B \<in> Ob

goal (1 subgoal):
 1. set_dom (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = Hom A B
[PROOF STEP]
by (simp add: set_comp_def sandwich_def)
[PROOF STATE]
proof (state)
this:
set_dom (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = Hom A B

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_dom (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = Hom A B

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
have "\<dots> = set_dom ((\<sigma>(A,a) C) \<odot> (Hom(A,_)\<^bsub>\<a>\<^esub> f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hom A B = set_dom (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
[PROOF STEP]
by (simp add: set_comp_def homf_def 1 2)
[PROOF STATE]
proof (state)
this:
Hom A B = set_dom (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set_dom (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_dom (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
[PROOF STEP]
have set_dom_eq:
    "set_dom ((F\<^bsub>\<a>\<^esub> f) \<odot> (\<sigma>(A,a) B))
    = set_dom ((\<sigma>(A,a) C) \<odot> (Hom(A,_)\<^bsub>\<a>\<^esub> f))"
[PROOF STATE]
proof (prove)
using this:
set_dom (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_dom (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)

goal (1 subgoal):
 1. set_dom (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_dom (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set_dom (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_dom (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
from BOb COb fBC
[PROOF STATE]
proof (chain)
picking this:
B \<in> Ob
C \<in> Ob
f \<in> Hom B C
[PROOF STEP]
have "(F\<^bsub>\<a>\<^esub> f) \<in> Hom\<^bsub>BB\<^esub> (F\<^bsub>\<o>\<^esub> B) (F\<^bsub>\<o>\<^esub> C)"
[PROOF STATE]
proof (prove)
using this:
B \<in> Ob
C \<in> Ob
f \<in> Hom B C

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<in> Hom\<^bsub>BB\<^esub> F \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> C
[PROOF STEP]
by (rule functors_preserve_homsets)
[PROOF STATE]
proof (state)
this:
F \<^bsub>\<a>\<^esub> f \<in> Hom\<^bsub>BB\<^esub> F \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> C

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
hence "set_cod ((F\<^bsub>\<a>\<^esub> f) \<odot> (\<sigma>(A,a) B)) = F\<^bsub>\<o>\<^esub> C"
[PROOF STATE]
proof (prove)
using this:
F \<^bsub>\<a>\<^esub> f \<in> Hom\<^bsub>BB\<^esub> F \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> C

goal (1 subgoal):
 1. set_cod (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = F \<^bsub>\<o>\<^esub> C
[PROOF STEP]
by (simp add: set_comp_def BB_Set Set_def set_cat_def hom_def)
[PROOF STATE]
proof (state)
this:
set_cod (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = F \<^bsub>\<o>\<^esub> C

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_cod (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = F \<^bsub>\<o>\<^esub> C

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
from COb
[PROOF STATE]
proof (chain)
picking this:
C \<in> Ob
[PROOF STEP]
have "\<dots> = set_cod ((\<sigma>(A,a) C) \<odot> (Hom(A,_)\<^bsub>\<a>\<^esub> f))"
[PROOF STATE]
proof (prove)
using this:
C \<in> Ob

goal (1 subgoal):
 1. F \<^bsub>\<o>\<^esub> C = set_cod (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
[PROOF STEP]
by (simp add: set_comp_def sandwich_def)
[PROOF STATE]
proof (state)
this:
F \<^bsub>\<o>\<^esub> C = set_cod (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set_cod (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_cod (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
[PROOF STEP]
have set_cod_eq:
    "set_cod ((F\<^bsub>\<a>\<^esub> f) \<odot> (\<sigma>(A,a) B))
    = set_cod ((\<sigma>(A,a) C) \<odot> (Hom(A,_)\<^bsub>\<a>\<^esub> f))"
[PROOF STATE]
proof (prove)
using this:
set_cod (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_cod (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)

goal (1 subgoal):
 1. set_cod (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_cod (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set_cod (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_cod (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
from AOb and BOb and COb and fBC and aFa
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
B \<in> Ob
C \<in> Ob
f \<in> Hom B C
a \<in> F \<^bsub>\<o>\<^esub> A
[PROOF STEP]
have set_func_lhs:
    "set_func ((F\<^bsub>\<a>\<^esub> f) \<odot> (\<sigma>(A,a) B)) =
    (\<lambda>g\<in>Hom A B. set_func (F\<^bsub>\<a>\<^esub> (f \<bullet> g)) a)"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
B \<in> Ob
C \<in> Ob
f \<in> Hom B C
a \<in> F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)
[PROOF STEP]
apply (simp add:  set_comp_def sandwich_def compose_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> Ob; B \<in> Ob; C \<in> Ob; f \<in> Hom B C; a \<in> F \<^bsub>\<o>\<^esub> A\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) (if x \<in> Hom A B then set_func (F \<^bsub>\<a>\<^esub> x) a else undefined)) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)
[PROOF STEP]
apply (rule extensionalityI, rule restrict_extensional, rule restrict_extensional)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>A \<in> Ob; B \<in> Ob; C \<in> Ob; f \<in> Hom B C; a \<in> F \<^bsub>\<o>\<^esub> A; x \<in> Hom A B\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) (if x \<in> Hom A B then set_func (F \<^bsub>\<a>\<^esub> x) a else undefined)) x = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a) x
[PROOF STEP]
by (simp add: F_comp_func compose_def)
[PROOF STATE]
proof (state)
this:
set_func (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
have "(\<bullet>) : Hom B C \<rightarrow> Hom A B \<rightarrow> Hom A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<bullet>) \<in> Hom B C \<rightarrow> Hom A B \<rightarrow> Hom A C
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<bullet>) \<in> Hom B C \<rightarrow> Hom A B \<rightarrow> Hom A C

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
from this and fBC
[PROOF STATE]
proof (chain)
picking this:
(\<bullet>) \<in> Hom B C \<rightarrow> Hom A B \<rightarrow> Hom A C
f \<in> Hom B C
[PROOF STEP]
have opfType: "(\<bullet>) f : Hom A B \<rightarrow> Hom A C"
[PROOF STATE]
proof (prove)
using this:
(\<bullet>) \<in> Hom B C \<rightarrow> Hom A B \<rightarrow> Hom A C
f \<in> Hom B C

goal (1 subgoal):
 1. (\<bullet>) f \<in> Hom A B \<rightarrow> Hom A C
[PROOF STEP]
by (rule funcset_mem)
[PROOF STATE]
proof (state)
this:
(\<bullet>) f \<in> Hom A B \<rightarrow> Hom A C

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
from 1 and 2
[PROOF STATE]
proof (chain)
picking this:
f \<in> Ar
Dom f = B
[PROOF STEP]
have "set_func ((\<sigma>(A,a) C) \<odot> (Hom(A,_)\<^bsub>\<a>\<^esub> f)) =
    (\<lambda>g\<in>Hom A B. set_func (\<sigma>(A,a) C) (f \<bullet> g))"
[PROOF STATE]
proof (prove)
using this:
f \<in> Ar
Dom f = B

goal (1 subgoal):
 1. set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) = (\<lambda>g\<in>Hom A B. set_func (\<sigma>(A,a) C) (f \<bullet> g))
[PROOF STEP]
apply (simp add: set_comp_def homf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> Ar; Dom f = B\<rbrakk> \<Longrightarrow> compose (Hom A B) (set_func (\<sigma>(A,a) C)) (restrict ((\<bullet>) f) (Hom A B)) = (\<lambda>g\<in>Hom A B. set_func (\<sigma>(A,a) C) (f \<bullet> g))
[PROOF STEP]
apply (simp add: compose_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> Ar; Dom f = B\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>Hom A B. set_func (\<sigma>(A,a) C) (if x \<in> Hom A B then f \<bullet> x else undefined)) = (\<lambda>g\<in>Hom A B. set_func (\<sigma>(A,a) C) (f \<bullet> g))
[PROOF STEP]
apply (rule extensionalityI, rule restrict_extensional, rule restrict_extensional)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f \<in> Ar; Dom f = B; x \<in> Hom A B\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>Hom A B. set_func (\<sigma>(A,a) C) (if x \<in> Hom A B then f \<bullet> x else undefined)) x = (\<lambda>g\<in>Hom A B. set_func (\<sigma>(A,a) C) (f \<bullet> g)) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) = (\<lambda>g\<in>Hom A B. set_func (\<sigma>(A,a) C) (f \<bullet> g))

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) = (\<lambda>g\<in>Hom A B. set_func (\<sigma>(A,a) C) (f \<bullet> g))

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
from COb and opfType
[PROOF STATE]
proof (chain)
picking this:
C \<in> Ob
(\<bullet>) f \<in> Hom A B \<rightarrow> Hom A C
[PROOF STEP]
have " \<dots> = (\<lambda>g\<in>Hom A B. set_func (F\<^bsub>\<a>\<^esub> (f \<bullet> g)) a)"
[PROOF STATE]
proof (prove)
using this:
C \<in> Ob
(\<bullet>) f \<in> Hom A B \<rightarrow> Hom A C

goal (1 subgoal):
 1. (\<lambda>g\<in>Hom A B. set_func (\<sigma>(A,a) C) (f \<bullet> g)) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)
[PROOF STEP]
apply (simp add: sandwich_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<in> Ob; (\<bullet>) f \<in> Hom A B \<rightarrow> Hom A C\<rbrakk> \<Longrightarrow> (\<lambda>g\<in>Hom A B. if f \<bullet> g \<in> Hom A C then set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a else undefined) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)
[PROOF STEP]
apply (rule extensionalityI, rule restrict_extensional, rule restrict_extensional)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>C \<in> Ob; (\<bullet>) f \<in> Hom A B \<rightarrow> Hom A C; x \<in> Hom A B\<rbrakk> \<Longrightarrow> (\<lambda>g\<in>Hom A B. if f \<bullet> g \<in> Hom A C then set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a else undefined) x = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a) x
[PROOF STEP]
by (simp add:Pi_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>g\<in>Hom A B. set_func (\<sigma>(A,a) C) (f \<bullet> g)) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)
[PROOF STEP]
have set_func_rhs:
    "set_func ((\<sigma>(A,a) C) \<odot> (Hom(A,_)\<^bsub>\<a>\<^esub> f)) =
    (\<lambda>g\<in>Hom A B. set_func (F\<^bsub>\<a>\<^esub> (f \<bullet> g)) a)"
[PROOF STATE]
proof (prove)
using this:
set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)

goal (1 subgoal):
 1. set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
from set_func_lhs and set_func_rhs
[PROOF STATE]
proof (chain)
picking this:
set_func (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)
set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)
[PROOF STEP]
have
    "set_func ((F\<^bsub>\<a>\<^esub> f) \<odot> (\<sigma>(A,a) B))
    = set_func ((\<sigma>(A,a) C) \<odot> (Hom(A,_)\<^bsub>\<a>\<^esub> f))"
[PROOF STATE]
proof (prove)
using this:
set_func (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)
set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f) = (\<lambda>g\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> (f \<bullet> g)) a)

goal (1 subgoal):
 1. set_func (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_func (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
with set_dom_eq and set_cod_eq
[PROOF STATE]
proof (chain)
picking this:
set_dom (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_dom (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
set_cod (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_cod (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
set_func (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set_dom (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_dom (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
set_cod (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_cod (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)
set_func (F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B) = set_func (\<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f)

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F \<^bsub>\<a>\<^esub> f \<odot> \<sigma>(A,a) B = \<sigma>(A,a) C \<odot> Hom(A,_) \<^bsub>\<a>\<^esub> f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Yoneda) sandwich_natural:
  assumes "A \<in> Ob"
  and "a \<in> F\<^bsub>\<o>\<^esub> A"
  shows "\<sigma>(A,a) : Hom(A,_) \<Rightarrow> F in Func(AA,Set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>(A,a) : Hom(A,_) \<Rightarrow> F in Func (AA , Set )
[PROOF STEP]
proof (intro natural_transformation.intro natural_transformation_axioms.intro two_cats.intro)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. category AA
 2. category Set
 3. Functor Hom(A,_) : AA \<longrightarrow> Set
 4. Functor F : AA \<longrightarrow> Set
 5. \<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
 6. \<sigma>(A,a) \<in> extensional (Ob)
 7. \<forall>Aa\<in>Ob. \<sigma>(A,a) Aa \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> Aa F \<^bsub>\<o>\<^esub> Aa
 8. \<forall>Aa\<in>Ob. \<forall>B\<in>Ob. \<forall>f\<in>Hom Aa B. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>Set\<^esub> \<sigma>(A,a) Aa = \<sigma>(A,a) B \<bullet>\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
show "category AA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category AA
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
category AA

goal (7 subgoals):
 1. category Set
 2. Functor Hom(A,_) : AA \<longrightarrow> Set
 3. Functor F : AA \<longrightarrow> Set
 4. \<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
 5. \<sigma>(A,a) \<in> extensional (Ob)
 6. \<forall>Aa\<in>Ob. \<sigma>(A,a) Aa \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> Aa F \<^bsub>\<o>\<^esub> Aa
 7. \<forall>Aa\<in>Ob. \<forall>B\<in>Ob. \<forall>f\<in>Hom Aa B. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>Set\<^esub> \<sigma>(A,a) Aa = \<sigma>(A,a) B \<bullet>\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
show "category Set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category Set
[PROOF STEP]
by (simp only: Set_def)(rule set_cat_cat)
[PROOF STATE]
proof (state)
this:
category Set

goal (6 subgoals):
 1. Functor Hom(A,_) : AA \<longrightarrow> Set
 2. Functor F : AA \<longrightarrow> Set
 3. \<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
 4. \<sigma>(A,a) \<in> extensional (Ob)
 5. \<forall>Aa\<in>Ob. \<sigma>(A,a) Aa \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> Aa F \<^bsub>\<o>\<^esub> Aa
 6. \<forall>Aa\<in>Ob. \<forall>B\<in>Ob. \<forall>f\<in>Hom Aa B. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>Set\<^esub> \<sigma>(A,a) Aa = \<sigma>(A,a) B \<bullet>\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
show "Functor Hom(A,_) : AA \<longrightarrow> Set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Functor Hom(A,_) : AA \<longrightarrow> Set
[PROOF STEP]
by (rule homf_into_set)
[PROOF STATE]
proof (state)
this:
Functor Hom(A,_) : AA \<longrightarrow> Set

goal (5 subgoals):
 1. Functor F : AA \<longrightarrow> Set
 2. \<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
 3. \<sigma>(A,a) \<in> extensional (Ob)
 4. \<forall>Aa\<in>Ob. \<sigma>(A,a) Aa \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> Aa F \<^bsub>\<o>\<^esub> Aa
 5. \<forall>Aa\<in>Ob. \<forall>B\<in>Ob. \<forall>f\<in>Hom Aa B. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>Set\<^esub> \<sigma>(A,a) Aa = \<sigma>(A,a) B \<bullet>\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
show "Functor F : AA \<longrightarrow> Set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Functor F : AA \<longrightarrow> Set
[PROOF STEP]
by (rule F_into_set)
[PROOF STATE]
proof (state)
this:
Functor F : AA \<longrightarrow> Set

goal (4 subgoals):
 1. \<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
 2. \<sigma>(A,a) \<in> extensional (Ob)
 3. \<forall>Aa\<in>Ob. \<sigma>(A,a) Aa \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> Aa F \<^bsub>\<o>\<^esub> Aa
 4. \<forall>Aa\<in>Ob. \<forall>B\<in>Ob. \<forall>f\<in>Hom Aa B. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>Set\<^esub> \<sigma>(A,a) Aa = \<sigma>(A,a) B \<bullet>\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
show "\<forall>B\<in>Ob. \<sigma>(A,a) B \<in> hom Set (Hom(A,_)\<^bsub>\<o>\<^esub> B) (F\<^bsub>\<o>\<^esub> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>B\<in>Ob. \<sigma>(A,a) B \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
a \<in> F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. \<forall>B\<in>Ob. \<sigma>(A,a) B \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> B
[PROOF STEP]
by (auto simp add: homf_def intro: sandwich_type)
[PROOF STATE]
proof (state)
this:
\<forall>B\<in>Ob. \<sigma>(A,a) B \<in> Hom\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<o>\<^esub> B F \<^bsub>\<o>\<^esub> B

goal (3 subgoals):
 1. \<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
 2. \<sigma>(A,a) \<in> extensional (Ob)
 3. \<forall>Aa\<in>Ob. \<forall>B\<in>Ob. \<forall>f\<in>Hom Aa B. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>Set\<^esub> \<sigma>(A,a) Aa = \<sigma>(A,a) B \<bullet>\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
show "\<sigma>(A,a) : Ob \<rightarrow> ar Set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
a \<in> F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. \<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>
[PROOF STEP]
by (rule sandwich_funcset)
[PROOF STATE]
proof (state)
this:
\<sigma>(A,a) \<in> Ob \<rightarrow> Ar\<^bsub>Set\<^esub>

goal (2 subgoals):
 1. \<sigma>(A,a) \<in> extensional (Ob)
 2. \<forall>Aa\<in>Ob. \<forall>B\<in>Ob. \<forall>f\<in>Hom Aa B. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>Set\<^esub> \<sigma>(A,a) Aa = \<sigma>(A,a) B \<bullet>\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
show "\<sigma>(A,a) \<in> extensional (Ob)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>(A,a) \<in> extensional (Ob)
[PROOF STEP]
unfolding sandwich_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>B\<in>Ob. \<lparr>set_dom = Hom A B, set_func = \<lambda>f\<in>Hom A B. set_func (F \<^bsub>\<a>\<^esub> f) a, set_cod = F \<^bsub>\<o>\<^esub> B\<rparr>) \<in> extensional (Ob)
[PROOF STEP]
by (rule restrict_extensional)
[PROOF STATE]
proof (state)
this:
\<sigma>(A,a) \<in> extensional (Ob)

goal (1 subgoal):
 1. \<forall>Aa\<in>Ob. \<forall>B\<in>Ob. \<forall>f\<in>Hom Aa B. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>Set\<^esub> \<sigma>(A,a) Aa = \<sigma>(A,a) B \<bullet>\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
show "\<forall>B\<in>Ob. \<forall>C\<in>Ob. \<forall>f\<in>Hom B C.
    comp Set (F \<^bsub>\<a>\<^esub> f) (\<sigma>(A,a) B) = comp Set (\<sigma>(A,a) C) (Hom(A,_)\<^bsub>\<a>\<^esub> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>B\<in>Ob. \<forall>C\<in>Ob. \<forall>f\<in>Hom B C. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>Set\<^esub> \<sigma>(A,a) B = \<sigma>(A,a) C \<bullet>\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
a \<in> F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. \<forall>B\<in>Ob. \<forall>C\<in>Ob. \<forall>f\<in>Hom B C. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>Set\<^esub> \<sigma>(A,a) B = \<sigma>(A,a) C \<bullet>\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f
[PROOF STEP]
by (auto simp add: Set_def intro: sandwich_commutes)
[PROOF STATE]
proof (state)
this:
\<forall>B\<in>Ob. \<forall>C\<in>Ob. \<forall>f\<in>Hom B C. F \<^bsub>\<a>\<^esub> f \<bullet>\<^bsub>Set\<^esub> \<sigma>(A,a) B = \<sigma>(A,a) C \<bullet>\<^bsub>Set\<^esub> Hom(A,_) \<^bsub>\<a>\<^esub> f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Yoneda) unsandwich_left_inverse:
  assumes 1: "A \<in> Ob"
  and 2: "a \<in> F\<^bsub>\<o>\<^esub> A"
  shows "\<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = a
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
[PROOF STEP]
have "Id A \<in> Hom A A"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob

goal (1 subgoal):
 1. Id A \<in> Hom A A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Id A \<in> Hom A A

goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = a
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
Id A \<in> Hom A A
[PROOF STEP]
have 3: "\<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = set_func (F\<^bsub>\<a>\<^esub> (Id A)) a"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob
Id A \<in> Hom A A

goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = set_func (F \<^bsub>\<a>\<^esub> (Id A)) a
[PROOF STEP]
by (simp add: sandwich_def homf_def unsandwich_def)
[PROOF STATE]
proof (state)
this:
\<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = set_func (F \<^bsub>\<a>\<^esub> (Id A)) a

goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = a
[PROOF STEP]
from F_preserves_id and 1
[PROOF STATE]
proof (chain)
picking this:
preserves_id F
A \<in> Ob
[PROOF STEP]
have 4: "F\<^bsub>\<a>\<^esub> (Id A) = id Set (F\<^bsub>\<o>\<^esub> A)"
[PROOF STATE]
proof (prove)
using this:
preserves_id F
A \<in> Ob

goal (1 subgoal):
 1. F \<^bsub>\<a>\<^esub> (Id A) = Id\<^bsub>Set\<^esub> F \<^bsub>\<o>\<^esub> A
[PROOF STEP]
by (simp add: preserves_id_def BB_Set)
[PROOF STATE]
proof (state)
this:
F \<^bsub>\<a>\<^esub> (Id A) = Id\<^bsub>Set\<^esub> F \<^bsub>\<o>\<^esub> A

goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = a
[PROOF STEP]
from F_preserves_objects and 1
[PROOF STATE]
proof (chain)
picking this:
F \<^bsub>\<o>\<^esub> \<in> Ob \<rightarrow> Ob\<^bsub>BB\<^esub>
A \<in> Ob
[PROOF STEP]
have "F\<^bsub>\<o>\<^esub> A \<in> Ob\<^bsub>BB\<^esub>"
[PROOF STATE]
proof (prove)
using this:
F \<^bsub>\<o>\<^esub> \<in> Ob \<rightarrow> Ob\<^bsub>BB\<^esub>
A \<in> Ob

goal (1 subgoal):
 1. F \<^bsub>\<o>\<^esub> A \<in> Ob\<^bsub>BB\<^esub>
[PROOF STEP]
by (rule funcset_mem)
[PROOF STATE]
proof (state)
this:
F \<^bsub>\<o>\<^esub> A \<in> Ob\<^bsub>BB\<^esub>

goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = a
[PROOF STEP]
hence "F\<^bsub>\<o>\<^esub> A \<subseteq> U"
[PROOF STATE]
proof (prove)
using this:
F \<^bsub>\<o>\<^esub> A \<in> Ob\<^bsub>BB\<^esub>

goal (1 subgoal):
 1. F \<^bsub>\<o>\<^esub> A \<subseteq> U
[PROOF STEP]
by (simp add: BB_Set Set_def set_cat_def)
[PROOF STATE]
proof (state)
this:
F \<^bsub>\<o>\<^esub> A \<subseteq> U

goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = a
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
a \<in> F \<^bsub>\<o>\<^esub> A
F \<^bsub>\<o>\<^esub> A \<subseteq> U
[PROOF STEP]
have 5: "set_func (id Set (F\<^bsub>\<o>\<^esub> A)) a = a"
[PROOF STATE]
proof (prove)
using this:
a \<in> F \<^bsub>\<o>\<^esub> A
F \<^bsub>\<o>\<^esub> A \<subseteq> U

goal (1 subgoal):
 1. set_func (Id\<^bsub>Set\<^esub> F \<^bsub>\<o>\<^esub> A) a = a
[PROOF STEP]
by (simp add: Set_def  set_id_def)
[PROOF STATE]
proof (state)
this:
set_func (Id\<^bsub>Set\<^esub> F \<^bsub>\<o>\<^esub> A) a = a

goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = a
[PROOF STEP]
by (simp add: 3 4 5)
[PROOF STATE]
proof (state)
this:
\<sigma>\<^sup>\<leftarrow>(A,\<sigma>(A,a)) = a

goal:
No subgoals!
[PROOF STEP]
qed