[STATEMENT]
lemma inv_notame:
 "\<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); inv g; notame7 g\<rbrakk>
  \<Longrightarrow> notame7 g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; notame7 g\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(simp add:notame_def notame7_def tame11b_def is_tame13a_def tame10ub_def del:disj_not1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; \<not> countVertices g \<le> 15 \<or> (\<exists>v\<in>\<V> g. \<not> degree g v \<le> (if except g v = 0 then 7 else 6)) \<or> \<not> squanderLowerBound g < squanderTarget\<rbrakk> \<Longrightarrow> \<not> countVertices g' \<le> 15 \<or> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply(frule inv_mgp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; \<not> countVertices g \<le> 15 \<or> (\<exists>v\<in>\<V> g. \<not> degree g v \<le> (if except g v = 0 then 7 else 6)) \<or> \<not> squanderLowerBound g < squanderTarget; minGraphProps g\<rbrakk> \<Longrightarrow> \<not> countVertices g' \<le> 15 \<or> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply(frule (1) next_plane0_vertices_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; \<not> countVertices g \<le> 15 \<or> (\<exists>v\<in>\<V> g. \<not> degree g v \<le> (if except g v = 0 then 7 else 6)) \<or> \<not> squanderLowerBound g < squanderTarget; minGraphProps g; \<V> g \<subseteq> \<V> g'\<rbrakk> \<Longrightarrow> \<not> countVertices g' \<le> 15 \<or> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; \<not> countVertices g \<le> 15\<rbrakk> \<Longrightarrow> \<not> countVertices g' \<le> 15 \<or> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
 2. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; (\<exists>v\<in>\<V> g. \<not> degree g v \<le> (if except g v = 0 then 7 else 6)) \<or> \<not> squanderLowerBound g < squanderTarget\<rbrakk> \<Longrightarrow> \<not> countVertices g' \<le> 15 \<or> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply(simp add:vertices_graph)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; (\<exists>v\<in>\<V> g. \<not> degree g v \<le> (if except g v = 0 then 7 else 6)) \<or> \<not> squanderLowerBound g < squanderTarget\<rbrakk> \<Longrightarrow> \<not> countVertices g' \<le> 15 \<or> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply(rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; (\<exists>v\<in>\<V> g. \<not> degree g v \<le> (if except g v = 0 then 7 else 6)) \<or> \<not> squanderLowerBound g < squanderTarget\<rbrakk> \<Longrightarrow> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; \<exists>v\<in>\<V> g. \<not> degree g v \<le> (if except g v = 0 then 7 else 6)\<rbrakk> \<Longrightarrow> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
 2. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; \<not> squanderLowerBound g < squanderTarget\<rbrakk> \<Longrightarrow> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; v \<in> \<V> g; \<not> degree g v \<le> (if except g v = 0 then 7 else 6); \<not> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)); squanderLowerBound g' < squanderTarget\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; \<not> squanderLowerBound g < squanderTarget\<rbrakk> \<Longrightarrow> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply(frule (2) next_plane0_incr_degree)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; v \<in> \<V> g; \<not> degree g v \<le> (if except g v = 0 then 7 else 6); \<not> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)); squanderLowerBound g' < squanderTarget; degree g v \<le> degree g' v\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; \<not> squanderLowerBound g < squanderTarget\<rbrakk> \<Longrightarrow> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply(frule (2) next_plane0_incr_except)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; v \<in> \<V> g; \<not> degree g v \<le> (if except g v = 0 then 7 else 6); \<not> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)); squanderLowerBound g' < squanderTarget; degree g v \<le> degree g' v; except g v \<le> except g' v\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; \<not> squanderLowerBound g < squanderTarget\<rbrakk> \<Longrightarrow> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply (force split:if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; \<not> squanderLowerBound g < squanderTarget\<rbrakk> \<Longrightarrow> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply(frule (1) next_plane0_incr_squander_lb)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; minGraphProps g; \<V> g \<subseteq> \<V> g'; \<not> squanderLowerBound g < squanderTarget; squanderLowerBound g \<le> squanderLowerBound g'\<rbrakk> \<Longrightarrow> (\<exists>v\<in>\<V> g'. (except g' v = 0 \<longrightarrow> \<not> degree g' v \<le> 7) \<and> (0 < except g' v \<longrightarrow> \<not> degree g' v \<le> 6)) \<or> \<not> squanderLowerBound g' < squanderTarget
[PROOF STEP]
apply(arith)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma inv_inv_notame:
 "invariant(\<lambda>g. inv g \<and> notame7 g) next_plane\<^bsub>p\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant (\<lambda>g. Invariants.inv g \<and> notame7 g) next_plane\<^bsub>p\<^esub>
[PROOF STEP]
apply(simp add:invariant_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>g g'. g' \<in> set (next_plane\<^bsub>p\<^esub> g) \<longrightarrow> Invariants.inv g \<and> notame7 g \<longrightarrow> Invariants.inv g' \<and> notame7 g'
[PROOF STEP]
apply(blast intro: inv_notame mgp_next_plane0_if_next_plane[OF inv_mgp]
       invariantE[OF inv_inv_next_plane])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma untame_notame:
 "untame (\<lambda>g. inv g \<and> notame7 g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. untame (\<lambda>g. Invariants.inv g \<and> notame7 g)
[PROOF STEP]
proof(clarsimp simp add: notame_def notame7_def untame_def tame11b_def is_tame13a_def tame10ub_def
                         linorder_not_le linorder_not_less)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g. \<lbrakk>final g; Invariants.inv g; 15 < countVertices g \<or> (\<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)) \<or> squanderTarget \<le> squanderLowerBound g; tame g\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g. \<lbrakk>final g; Invariants.inv g; 15 < countVertices g \<or> (\<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)) \<or> squanderTarget \<le> squanderLowerBound g; tame g\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "final g" "inv g" "tame g"
    and cases: "15 < countVertices g \<or>
                (\<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and>
                            (0 < except g v \<longrightarrow> 6 < degree g v))
                \<or> squanderTarget \<le> squanderLowerBound g"
                (is "?A \<or> ?B \<or> ?C" is "_ \<or> (\<exists>v\<in>\<V> g. ?B' v) \<or> _")
[PROOF STATE]
proof (state)
this:
final g
Invariants.inv g
tame g
15 < countVertices g \<or> (\<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)) \<or> squanderTarget \<le> squanderLowerBound g

goal (1 subgoal):
 1. \<And>g. \<lbrakk>final g; Invariants.inv g; 15 < countVertices g \<or> (\<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)) \<or> squanderTarget \<le> squanderLowerBound g; tame g\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from cases
[PROOF STATE]
proof (chain)
picking this:
15 < countVertices g \<or> (\<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)) \<or> squanderTarget \<le> squanderLowerBound g
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
15 < countVertices g \<or> (\<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)) \<or> squanderTarget \<le> squanderLowerBound g

goal (1 subgoal):
 1. False
[PROOF STEP]
proof(elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 15 < countVertices g \<Longrightarrow> False
 2. \<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v) \<Longrightarrow> False
 3. squanderTarget \<le> squanderLowerBound g \<Longrightarrow> False
[PROOF STEP]
assume ?B
[PROOF STATE]
proof (state)
this:
\<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)

goal (3 subgoals):
 1. 15 < countVertices g \<Longrightarrow> False
 2. \<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v) \<Longrightarrow> False
 3. squanderTarget \<le> squanderLowerBound g \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)
[PROOF STEP]
obtain v where v: "v \<in>\<V> g" "?B' v"
[PROOF STATE]
proof (prove)
using this:
\<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> \<V> g; (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> \<V> g
(except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)

goal (3 subgoals):
 1. 15 < countVertices g \<Longrightarrow> False
 2. \<exists>v\<in>\<V> g. (except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v) \<Longrightarrow> False
 3. squanderTarget \<le> squanderLowerBound g \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
assume "except g v = 0"
[PROOF STATE]
proof (state)
this:
except g v = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
except g v = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>tame g\<close> v
[PROOF STATE]
proof (prove)
using this:
except g v = 0
tame g
v \<in> \<V> g
(except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)

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

goal (1 subgoal):
 1. except g v \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. except g v \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume "except g v \<noteq> 0"
[PROOF STATE]
proof (state)
this:
except g v \<noteq> 0

goal (1 subgoal):
 1. except g v \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
except g v \<noteq> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>tame g\<close> v
[PROOF STATE]
proof (prove)
using this:
except g v \<noteq> 0
tame g
v \<in> \<V> g
(except g v = 0 \<longrightarrow> 7 < degree g v) \<and> (0 < except g v \<longrightarrow> 6 < degree g v)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(auto simp: except_def filter_empty_conv tame_def tame11b_def
          minGraphProps_facesAt_eq[OF inv_mgp[OF \<open>inv g\<close>]] split:if_split_asm)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. 15 < countVertices g \<Longrightarrow> False
 2. squanderTarget \<le> squanderLowerBound g \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 15 < countVertices g \<Longrightarrow> False
 2. squanderTarget \<le> squanderLowerBound g \<Longrightarrow> False
[PROOF STEP]
assume ?A
[PROOF STATE]
proof (state)
this:
15 < countVertices g

goal (2 subgoals):
 1. 15 < countVertices g \<Longrightarrow> False
 2. squanderTarget \<le> squanderLowerBound g \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
15 < countVertices g

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>tame g\<close>
[PROOF STATE]
proof (prove)
using this:
15 < countVertices g
tame g

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

goal (1 subgoal):
 1. squanderTarget \<le> squanderLowerBound g \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. squanderTarget \<le> squanderLowerBound g \<Longrightarrow> False
[PROOF STEP]
assume ?C
[PROOF STATE]
proof (state)
this:
squanderTarget \<le> squanderLowerBound g

goal (1 subgoal):
 1. squanderTarget \<le> squanderLowerBound g \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
squanderTarget \<le> squanderLowerBound g

goal (1 subgoal):
 1. False
[PROOF STEP]
using total_weight_lowerbound[OF \<open>inv g\<close> \<open>final g\<close> \<open>tame g\<close>]
      \<open>tame g\<close>
[PROOF STATE]
proof (prove)
using this:
squanderTarget \<le> squanderLowerBound g
\<lbrakk>admissible ?w g; ListSum (faces g) ?w < squanderTarget\<rbrakk> \<Longrightarrow> squanderLowerBound g \<le> ListSum (faces g) ?w
tame g

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma polysizes_tame:
 "\<lbrakk> g' \<in> set (generatePolygon n v f g); inv g; f \<in> set(nonFinals g);
   v \<in> \<V> f; 3 \<le> n; n < 4+p; n \<notin> set(polysizes p g) \<rbrakk>
 \<Longrightarrow> notame7 g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (generatePolygon n v f g); Invariants.inv g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g)\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(frule (4) in_next_plane0I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (generatePolygon n v f g); Invariants.inv g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g)\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(frule (4) genPoly_incr_facesquander_lb)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (generatePolygon n v f g); Invariants.inv g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(frule (1) next_plane0_incr_ExcessNotAt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (generatePolygon n v f g); Invariants.inv g; f \<in> set (nonFinals g); v \<in> \<V> f; 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); faceSquanderLowerBound g + \<d> n \<le> faceSquanderLowerBound g'; ExcessNotAt g None \<le> ExcessNotAt g' None\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(simp add: notame_def notame7_def is_tame13a_def faceSquanderLowerBound_def
           polysizes_def squanderLowerBound_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma genPolyTame_notame:
 "\<lbrakk> g' \<in> set (generatePolygon n v f g); g' \<notin> set (generatePolygonTame n v f g);
    inv g; 3 \<le> n \<rbrakk>
  \<Longrightarrow> notame7 g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (generatePolygon n v f g); g' \<notin> set (generatePolygonTame n v f g); Invariants.inv g; 3 \<le> n\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
by(fastforce simp:generatePolygon_def generatePolygonTame_def enum_enumerator
                 notame_def notame7_def)


[STATEMENT]
lemma excess_notame:
 "\<lbrakk> inv g; g' \<in> set (next_plane\<^bsub>p\<^esub> g); g' \<notin> set (next_tame0 p g) \<rbrakk>
       \<Longrightarrow> notame7 g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Invariants.inv g; g' \<in> set (next_plane\<^bsub>p\<^esub> g); g' \<notin> set (next_tame0\<^bsub>p\<^esub> g)\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(frule (1) mgp_next_plane0_if_next_plane[OF inv_mgp])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Invariants.inv g; g' \<in> set (next_plane\<^bsub>p\<^esub> g); g' \<notin> set (next_tame0\<^bsub>p\<^esub> g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g)\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(auto simp add:next_tame0_def next_plane_def split:if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> x; x < 4 + p\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(rename_tac n)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(case_tac "n \<in> set(polysizes p g)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<in> set (polysizes p g)\<rbrakk> \<Longrightarrow> notame7 g'
 2. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g)\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(drule bspec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<in> set (polysizes p g)\<rbrakk> \<Longrightarrow> ?x20 n \<in> set (polysizes p g)
 2. \<And>n. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<in> set (polysizes p g); g' \<notin> set (generatePolygonTame (?x20 n) (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g)\<rbrakk> \<Longrightarrow> notame7 g'
 3. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g)\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<in> set (polysizes p g); g' \<notin> set (generatePolygonTame n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g)\<rbrakk> \<Longrightarrow> notame7 g'
 2. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g)\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(simp add:genPolyTame_notame)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g)\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(subgoal_tac "minimalFace (nonFinals g) \<in> set(nonFinals g)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); minimalFace (nonFinals g) \<in> set (nonFinals g)\<rbrakk> \<Longrightarrow> notame7 g'
 2. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g)\<rbrakk> \<Longrightarrow> minimalFace (nonFinals g) \<in> set (nonFinals g)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g)\<rbrakk> \<Longrightarrow> minimalFace (nonFinals g) \<in> set (nonFinals g)
 2. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); minimalFace (nonFinals g) \<in> set (nonFinals g)\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(simp add:minimalFace_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); minimalFace (nonFinals g) \<in> set (nonFinals g)\<rbrakk> \<Longrightarrow> notame7 g'
[PROOF STEP]
apply(subgoal_tac "minimalVertex g (minimalFace (nonFinals g)) \<in> \<V>(minimalFace (nonFinals g))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); minimalFace (nonFinals g) \<in> set (nonFinals g); minimalVertex g (minimalFace (nonFinals g)) \<in> \<V> (minimalFace (nonFinals g))\<rbrakk> \<Longrightarrow> notame7 g'
 2. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); minimalFace (nonFinals g) \<in> set (nonFinals g)\<rbrakk> \<Longrightarrow> minimalVertex g (minimalFace (nonFinals g)) \<in> \<V> (minimalFace (nonFinals g))
[PROOF STEP]
apply(blast intro:polysizes_tame)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimalVertex g (minimalFace (nonFinals g))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); minimalFace (nonFinals g) \<in> set (nonFinals g)\<rbrakk> \<Longrightarrow> minimalVertex g (minimalFace (nonFinals g)) \<in> \<V> (minimalFace (nonFinals g))
[PROOF STEP]
apply(simp add:minimalVertex_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimal (height g) (vertices (minimalFace (nonFinals g)))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimal (height g) (vertices (minimalFace (nonFinals g)))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); minimalFace (nonFinals g) \<in> set (nonFinals g)\<rbrakk> \<Longrightarrow> minimal (height g) (vertices (minimalFace (nonFinals g))) \<in> \<V> (minimalFace (nonFinals g))
[PROOF STEP]
apply(rule minimal_in_set)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimal (height g) (vertices (minimalFace (nonFinals g)))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimal (height g) (vertices (minimalFace (nonFinals g)))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); minimalFace (nonFinals g) \<in> set (nonFinals g)\<rbrakk> \<Longrightarrow> vertices (minimalFace (nonFinals g)) \<noteq> []
[PROOF STEP]
apply(erule mgp_vertices_nonempty[OF inv_mgp])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>set (polysizes p g). g' \<notin> set (generatePolygonTame x (minimal (height g) (vertices (minimalFace (nonFinals g)))) (minimalFace (nonFinals g)) g); g' \<in> set (next_plane0\<^bsub>p\<^esub> g); nonFinals g \<noteq> []; g' \<in> set (generatePolygon n (minimal (height g) (vertices (minimalFace (nonFinals g)))) (minimalFace (nonFinals g)) g); 3 \<le> n; n < 4 + p; n \<notin> set (polysizes p g); minimalFace (nonFinals g) \<in> set (nonFinals g)\<rbrakk> \<Longrightarrow> minimalFace (nonFinals g) \<in> \<F> g
[PROOF STEP]
apply(simp add:nonFinals_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma next_tame0_comp: "\<lbrakk> Seed\<^bsub>p\<^esub> [next_plane p]\<rightarrow>* g; final g; tame g \<rbrakk>
 \<Longrightarrow> Seed\<^bsub>p\<^esub> [next_tame0 p]\<rightarrow>* g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> Seed\<^bsub>p\<^esub> [next_tame0\<^bsub>p\<^esub>]\<rightarrow>* g
[PROOF STEP]
apply(rule filterout_untame_succs[OF inv_inv_next_plane inv_inv_notame
  untame_notame])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ga g'. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g; Invariants.inv ga; g' \<in> set (next_plane\<^bsub>?p1\<^esub> ga); g' \<notin> set (next_tame0\<^bsub>p\<^esub> ga)\<rbrakk> \<Longrightarrow> notame7 g'
 2. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> Seed\<^bsub>p\<^esub> [next_plane\<^bsub>?p1\<^esub>]\<rightarrow>* g
 3. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> Invariants.inv Seed\<^bsub>p\<^esub>
 4. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> final g
 5. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> tame g
[PROOF STEP]
apply(blast intro:excess_notame)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g
 2. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> Invariants.inv Seed\<^bsub>p\<^esub>
 3. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> final g
 4. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> tame g
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> Invariants.inv Seed\<^bsub>p\<^esub>
 2. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> final g
 3. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> tame g
[PROOF STEP]
apply(rule inv_Seed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> final g
 2. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> tame g
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Seed\<^bsub>p\<^esub> [next_plane\<^bsub>p\<^esub>]\<rightarrow>* g; final g; tame g\<rbrakk> \<Longrightarrow> tame g
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma inv_inv_next_tame0: "invariant inv (next_tame0 p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant Invariants.inv next_tame0\<^bsub>p\<^esub>
[PROOF STEP]
by(rule inv_subset[OF inv_inv_next_plane next_tame0_subset_plane])


[STATEMENT]
lemma inv_inv_next_tame: "invariant inv next_tame\<^bsub>p\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant Invariants.inv next_tame\<^bsub>p\<^esub>
[PROOF STEP]
apply(simp add:next_tame_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant Invariants.inv (filter (\<lambda>g. final g \<longrightarrow> is_tame g) \<circ> next_tame0\<^bsub>p\<^esub>)
[PROOF STEP]
apply(rule inv_subset[OF inv_inv_next_tame0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g. Invariants.inv g \<Longrightarrow> set ((filter (\<lambda>g. final g \<longrightarrow> is_tame g) \<circ> next_tame0\<^bsub>p\<^esub>) g) \<subseteq> set (next_tame0\<^bsub>?p1\<^esub> g)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mgp_TameEnum: "g \<in> TameEnum\<^bsub>p\<^esub> \<Longrightarrow> minGraphProps g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> TameEnum\<^bsub>p\<^esub> \<Longrightarrow> minGraphProps g
[PROOF STEP]
by (unfold TameEnumP_def)
   (blast intro: RTranCl_inv[OF inv_inv_next_tame] inv_Seed inv_mgp)


[STATEMENT]
lemma (in is_cat_rKe) is_cat_rKe_axioms'[cat_Kan_cs_intros]:
  assumes "\<alpha>' = \<alpha>"
    and "\<GG>' = \<GG>"
    and "\<KK>' = \<KK>"
    and "\<TT>' = \<TT>"
    and "\<BB>' = \<BB>"
    and "\<AA>' = \<AA>"
    and "\<CC>' = \<CC>"
  shows "\<epsilon> : \<GG>' \<circ>\<^sub>C\<^sub>F \<KK>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>'\<^esub> \<TT>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<AA>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG>' \<circ>\<^sub>C\<^sub>F \<KK>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>'\<^esub> \<TT>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<AA>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
by (rule is_cat_rKe_axioms)


[STATEMENT]
lemma (in is_cat_lKe) is_cat_lKe_axioms'[cat_Kan_cs_intros]:
  assumes "\<alpha>' = \<alpha>"
    and "\<FF>' = \<FF>"
    and "\<KK>' = \<KK>"
    and "\<TT>' = \<TT>"
    and "\<BB>' = \<BB>"
    and "\<AA>' = \<AA>"
    and "\<CC>' = \<CC>"
  shows "\<eta> : \<TT>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF>' \<circ>\<^sub>C\<^sub>F \<KK>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<AA>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : \<TT>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF>' \<circ>\<^sub>C\<^sub>F \<KK>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<AA>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
by (rule is_cat_lKe_axioms)


[STATEMENT]
lemma (in is_cat_rKe) is_cat_lKe_op:
  "op_ntcf \<epsilon> :
    op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<GG> \<circ>\<^sub>C\<^sub>F op_cf \<KK> :
    op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<epsilon> : op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<GG> \<circ>\<^sub>C\<^sub>F op_cf \<KK> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \<AA>
[PROOF STEP]
by (intro is_cat_lKeI, unfold cat_op_simps; (intro cat_rKe_ua_fo)?)
    (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)+


[STATEMENT]
lemma (in is_cat_rKe) is_cat_lKe_op'[cat_op_intros]:
  assumes "\<TT>' = op_cf \<TT>"
    and "\<GG>' = op_cf \<GG>"
    and "\<KK>' = op_cf \<KK>"
    and "\<BB>' = op_cat \<BB>"
    and "\<AA>' = op_cat \<AA>"
    and "\<CC>' = op_cat \<CC>"
  shows "op_ntcf \<epsilon> : \<TT>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<GG>' \<circ>\<^sub>C\<^sub>F \<KK>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<AA>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<epsilon> : \<TT>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<GG>' \<circ>\<^sub>C\<^sub>F \<KK>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<AA>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<epsilon> : op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<GG> \<circ>\<^sub>C\<^sub>F op_cf \<KK> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \<AA>
[PROOF STEP]
by (rule is_cat_lKe_op)


[STATEMENT]
lemma (in is_cat_lKe) is_cat_rKe_op:
  "op_ntcf \<eta> :
    op_cf \<FF> \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<TT> :
    op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<eta> : op_cf \<FF> \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<TT> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \<AA>
[PROOF STEP]
by (intro is_cat_rKeI, unfold cat_op_simps; (intro cat_lKe_ua_fo)?)
    (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)+


[STATEMENT]
lemma (in is_cat_lKe) is_cat_lKe_op'[cat_op_intros]:
  assumes "\<TT>' = op_cf \<TT>"
    and "\<FF>' = op_cf \<FF>"
    and "\<KK>' = op_cf \<KK>"
    and "\<BB>' = op_cat \<BB>"
    and "\<AA>' = op_cat \<AA>"
    and "\<CC>' = op_cat \<CC>"
  shows "op_ntcf \<eta> : \<FF>' \<circ>\<^sub>C\<^sub>F \<KK>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<AA>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<eta> : \<FF>' \<circ>\<^sub>C\<^sub>F \<KK>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<AA>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<eta> : op_cf \<FF> \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<TT> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \<AA>
[PROOF STEP]
by (rule is_cat_rKe_op)


[STATEMENT]
lemma (in is_cat_rKe) cat_rKe_exp_cat_cf_cat_FUNCT_is_arr:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "exp_cat_cf \<alpha> \<AA> \<KK> : cat_FUNCT \<alpha> \<CC> \<AA> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>i\<^sub>n\<^sub>y\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> \<BB> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp_cat_cf \<alpha> \<AA> \<KK> : cat_FUNCT \<alpha> \<CC> \<AA> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>i\<^sub>n\<^sub>y\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> \<BB> \<AA>
[PROOF STEP]
by
    (
      rule exp_cat_cf_is_tiny_functor[
        OF assms Ran.HomCod.category_axioms AG.is_functor_axioms
        ]
    )


[STATEMENT]
lemma (in is_cat_lKe) cat_lKe_exp_cat_cf_cat_FUNCT_is_arr:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "exp_cat_cf \<alpha> \<AA> \<KK> : cat_FUNCT \<alpha> \<CC> \<AA> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>i\<^sub>n\<^sub>y\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> \<BB> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp_cat_cf \<alpha> \<AA> \<KK> : cat_FUNCT \<alpha> \<CC> \<AA> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>i\<^sub>n\<^sub>y\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> \<BB> \<AA>
[PROOF STEP]
by
    (
      rule exp_cat_cf_is_tiny_functor[
        OF assms Lan.HomCod.category_axioms AG.is_functor_axioms
        ]
    )


[STATEMENT]
lemma is_cat_rKeI':
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "\<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "\<And>\<GG>' \<epsilon>'.
      \<lbrakk> \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<rbrakk> \<Longrightarrow>
        \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>)"
  shows "\<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
interpret \<KK>: is_functor \<alpha> \<BB> \<CC> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
interpret \<GG>: is_functor \<alpha> \<CC> \<AA> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
interpret \<epsilon>: is_ntcf \<alpha> \<BB> \<AA> \<open>\<GG> \<circ>\<^sub>C\<^sub>F \<KK>\<close> \<TT> \<epsilon>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
let ?\<AA>\<KK> = \<open>exp_cat_cf \<alpha> \<AA> \<KK>\<close>
    and ?\<TT> = \<open>cf_map \<TT>\<close>
    and ?\<GG> = \<open>cf_map \<GG>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
proof(intro is_cat_rKeI is_functor.universal_arrow_foI assms)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. exp_cat_cf \<alpha> \<AA> \<KK> : ?\<AA>1 \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>1\<^esub> ?\<BB>1
 2. cf_map \<GG> \<in>\<^sub>\<circ> ?\<AA>1\<lparr>Obj\<rparr>
 3. ntcf_arrow \<epsilon> : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>cf_map \<GG>\<rparr> \<mapsto>\<^bsub>?\<BB>1\<^esub> cf_map \<TT>
 4. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> ?\<AA>1\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>?\<BB>1\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>?\<AA>1\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
define \<beta> where "\<beta> = \<alpha> + \<omega>"
[PROOF STATE]
proof (state)
this:
\<beta> = \<alpha> + \<omega>

goal (4 subgoals):
 1. exp_cat_cf \<alpha> \<AA> \<KK> : ?\<AA>1 \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>1\<^esub> ?\<BB>1
 2. cf_map \<GG> \<in>\<^sub>\<circ> ?\<AA>1\<lparr>Obj\<rparr>
 3. ntcf_arrow \<epsilon> : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>cf_map \<GG>\<rparr> \<mapsto>\<^bsub>?\<BB>1\<^esub> cf_map \<TT>
 4. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> ?\<AA>1\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>?\<BB>1\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>?\<AA>1\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
have "\<Z> \<beta>" and \<alpha>\<beta>: "\<alpha> \<in>\<^sub>\<circ> \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> \<beta> &&& \<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
by (simp_all add: \<beta>_def \<KK>.\<Z>_Limit_\<alpha>\<omega> \<KK>.\<Z>_\<omega>_\<alpha>\<omega> \<Z>_def \<KK>.\<Z>_\<alpha>_\<alpha>\<omega>)
[PROOF STATE]
proof (state)
this:
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (4 subgoals):
 1. exp_cat_cf \<alpha> \<AA> \<KK> : ?\<AA>1 \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>1\<^esub> ?\<BB>1
 2. cf_map \<GG> \<in>\<^sub>\<circ> ?\<AA>1\<lparr>Obj\<rparr>
 3. ntcf_arrow \<epsilon> : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>cf_map \<GG>\<rparr> \<mapsto>\<^bsub>?\<BB>1\<^esub> cf_map \<TT>
 4. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> ?\<AA>1\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>?\<BB>1\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>?\<AA>1\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
interpret \<beta>: \<Z> \<beta>
[PROOF STATE]
proof (prove)
using this:
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. \<Z> \<beta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. exp_cat_cf \<alpha> \<AA> \<KK> : ?\<AA>1 \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>1\<^esub> ?\<BB>1
 2. cf_map \<GG> \<in>\<^sub>\<circ> ?\<AA>1\<lparr>Obj\<rparr>
 3. ntcf_arrow \<epsilon> : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>cf_map \<GG>\<rparr> \<mapsto>\<^bsub>?\<BB>1\<^esub> cf_map \<TT>
 4. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> ?\<AA>1\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>?\<BB>1\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>?\<AA>1\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
show "?\<AA>\<KK> : cat_FUNCT \<alpha> \<CC> \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> \<BB> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp_cat_cf \<alpha> \<AA> \<KK> : cat_FUNCT \<alpha> \<CC> \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> \<BB> \<AA>
[PROOF STEP]
by
        (
          cs_concl cs_shallow cs_intro:
            cat_small_cs_intros
            exp_cat_cf_is_tiny_functor[
              OF \<beta>.\<Z>_axioms \<alpha>\<beta> \<GG>.HomCod.category_axioms assms(1)
              ]
        )
[PROOF STATE]
proof (state)
this:
exp_cat_cf \<alpha> \<AA> \<KK> : cat_FUNCT \<alpha> \<CC> \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> \<BB> \<AA>

goal (3 subgoals):
 1. cf_map \<GG> \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>
 2. ntcf_arrow \<epsilon> : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>cf_map \<GG>\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>
 3. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
from \<alpha>\<beta> assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<in>\<^sub>\<circ> \<beta>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show "cf_map \<GG> \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in>\<^sub>\<circ> \<beta>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. cf_map \<GG> \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding cat_FUNCT_components
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in>\<^sub>\<circ> \<beta>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. cf_map \<GG> \<in>\<^sub>\<circ> cf_maps \<alpha> \<CC> \<AA>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_FUNCT_cs_intros)
[PROOF STATE]
proof (state)
this:
cf_map \<GG> \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>

goal (2 subgoals):
 1. ntcf_arrow \<epsilon> : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>cf_map \<GG>\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>
 2. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
from assms(1-3)
[PROOF STATE]
proof (chain)
picking this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show "ntcf_arrow \<epsilon> :
      ?\<AA>\<KK>\<lparr>ObjMap\<rparr>\<lparr>?\<GG>\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> ?\<TT>"
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. ntcf_arrow \<epsilon> : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>cf_map \<GG>\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_Kan_cs_simps cat_FUNCT_cs_simps cat_FUNCT_components(1)
            cs_intro: cat_FUNCT_cs_intros
        )
[PROOF STATE]
proof (state)
this:
ntcf_arrow \<epsilon> : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>cf_map \<GG>\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>

goal (1 subgoal):
 1. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
fix \<FF>' \<epsilon>'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
assume prems:
      "\<FF>' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>"
      "\<epsilon>' : ?\<AA>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<FF>'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> ?\<TT>"
[PROOF STATE]
proof (state)
this:
\<FF>' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>
\<epsilon>' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>\<FF>'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>

goal (1 subgoal):
 1. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
from prems(1)
[PROOF STATE]
proof (chain)
picking this:
\<FF>' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
have "\<FF>' \<in>\<^sub>\<circ> cf_maps \<alpha> \<CC> \<AA>"
[PROOF STATE]
proof (prove)
using this:
\<FF>' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<FF>' \<in>\<^sub>\<circ> cf_maps \<alpha> \<CC> \<AA>
[PROOF STEP]
unfolding cat_FUNCT_components(1)
[PROOF STATE]
proof (prove)
using this:
\<FF>' \<in>\<^sub>\<circ> cf_maps \<alpha> \<CC> \<AA>

goal (1 subgoal):
 1. \<FF>' \<in>\<^sub>\<circ> cf_maps \<alpha> \<CC> \<AA>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<FF>' \<in>\<^sub>\<circ> cf_maps \<alpha> \<CC> \<AA>

goal (1 subgoal):
 1. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<FF>' \<in>\<^sub>\<circ> cf_maps \<alpha> \<CC> \<AA>
[PROOF STEP]
obtain \<FF> where \<FF>'_def: "\<FF>' = cf_map \<FF>" and \<FF>: "\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
\<FF>' \<in>\<^sub>\<circ> cf_maps \<alpha> \<CC> \<AA>

goal (1 subgoal):
 1. (\<And>\<FF>. \<lbrakk>\<FF>' = cf_map \<FF>; \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<FF>' = cf_map \<FF>
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
note \<epsilon>' = cat_FUNCT_is_arrD[OF prems(2)]
[PROOF STATE]
proof (state)
this:
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' : cf_of_cf_map \<BB> \<AA> (exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>\<FF>'\<rparr>) \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<BB> \<AA> (cf_map \<TT>) : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon>' = ntcf_arrow (ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>')
exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>\<FF>'\<rparr> = cf_map (cf_of_cf_map \<BB> \<AA> (exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>\<FF>'\<rparr>))
cf_map \<TT> = cf_map (cf_of_cf_map \<BB> \<AA> (cf_map \<TT>))

goal (1 subgoal):
 1. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
from \<epsilon>'(1) \<FF>
[PROOF STATE]
proof (chain)
picking this:
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' : cf_of_cf_map \<BB> \<AA> (exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>\<FF>'\<rparr>) \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<BB> \<AA> (cf_map \<TT>) : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have \<epsilon>'_is_ntcf:
      "ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' : \<FF> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' : cf_of_cf_map \<BB> \<AA> (exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>\<FF>'\<rparr>) \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<BB> \<AA> (cf_map \<TT>) : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by
        (
          cs_prems
            cs_simp: \<FF>'_def cat_Kan_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
[PROOF STATE]
proof (state)
this:
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
from assms(4)[OF \<FF> \<epsilon>'_is_ntcf]
[PROOF STATE]
proof (chain)
picking this:
\<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
obtain \<sigma>
      where \<sigma>: "\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
        and \<epsilon>'_def': "ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>)"
        and unique_\<sigma>: "\<And>\<sigma>'.
          \<lbrakk>
            \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>;
            ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>)
          \<rbrakk> \<Longrightarrow> \<sigma>' = \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal (1 subgoal):
 1. (\<And>\<sigma>. \<lbrakk>\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>); \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
\<lbrakk>?\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (?\<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> ?\<sigma>' = \<sigma>

goal (1 subgoal):
 1. \<And>r' u'. \<lbrakk>r' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>; u' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>r'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>\<rbrakk> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> u' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) r'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
show "\<exists>!f'.
      f' : \<FF>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> ?\<GG> \<and>
      \<epsilon>' = umap_fo ?\<AA>\<KK> ?\<TT> ?\<GG> (ntcf_arrow \<epsilon>) \<FF>'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!f'. f' : \<FF>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) \<FF>'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
proof(intro ex1I conjI; (elim conjE)?, unfold \<FF>'_def)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?a1 : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>
 2. \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>?a1\<rparr>
 3. \<And>f'. \<lbrakk>f' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>\<rbrakk> \<Longrightarrow> f' = ?a1
[PROOF STEP]
from \<sigma>
[PROOF STATE]
proof (chain)
picking this:
\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show "ntcf_arrow \<sigma> : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> ?\<GG>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. ntcf_arrow \<sigma> : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_FUNCT_cs_intros)
[PROOF STATE]
proof (state)
this:
ntcf_arrow \<sigma> : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>

goal (2 subgoals):
 1. \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>ntcf_arrow \<sigma>\<rparr>
 2. \<And>f'. \<lbrakk>f' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>\<rbrakk> \<Longrightarrow> f' = ntcf_arrow \<sigma>
[PROOF STEP]
from \<alpha>\<beta> assms(1-3) \<sigma> \<epsilon>'(1)
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<in>\<^sub>\<circ> \<beta>
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' : cf_of_cf_map \<BB> \<AA> (exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>\<FF>'\<rparr>) \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<BB> \<AA> (cf_map \<TT>) : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show
        "\<epsilon>' = umap_fo ?\<AA>\<KK> ?\<TT> ?\<GG> (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>ntcf_arrow \<sigma>\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in>\<^sub>\<circ> \<beta>
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' : cf_of_cf_map \<BB> \<AA> (exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>\<FF>'\<rparr>) \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<BB> \<AA> (cf_map \<TT>) : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>ntcf_arrow \<sigma>\<rparr>
[PROOF STEP]
by (subst \<epsilon>')
          (
            cs_concl
              cs_simp:
                \<epsilon>'_def'[symmetric]
                cat_cs_simps
                cat_FUNCT_cs_simps
                cat_Kan_cs_simps
              cs_intro:
                cat_small_cs_intros
                cat_cs_intros
                cat_Kan_cs_intros
                cat_FUNCT_cs_intros
          )
[PROOF STATE]
proof (state)
this:
\<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>ntcf_arrow \<sigma>\<rparr>

goal (1 subgoal):
 1. \<And>f'. \<lbrakk>f' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>\<rbrakk> \<Longrightarrow> f' = ntcf_arrow \<sigma>
[PROOF STEP]
fix \<sigma>'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f'. \<lbrakk>f' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>\<rbrakk> \<Longrightarrow> f' = ntcf_arrow \<sigma>
[PROOF STEP]
assume prems:
        "\<sigma>' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> ?\<GG>"
        "\<epsilon>' = umap_fo ?\<AA>\<KK> ?\<TT> ?\<GG> (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>\<sigma>'\<rparr>"
[PROOF STATE]
proof (state)
this:
\<sigma>' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>
\<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>\<sigma>'\<rparr>

goal (1 subgoal):
 1. \<And>f'. \<lbrakk>f' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>\<rbrakk> \<Longrightarrow> f' = ntcf_arrow \<sigma>
[PROOF STEP]
note \<sigma>' = cat_FUNCT_is_arrD[OF prems(1)]
[PROOF STATE]
proof (state)
this:
ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' : cf_of_cf_map \<CC> \<AA> (cf_map \<FF>) \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<CC> \<AA> (cf_map \<GG>) : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<sigma>' = ntcf_arrow (ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>')
cf_map \<FF> = cf_map (cf_of_cf_map \<CC> \<AA> (cf_map \<FF>))
cf_map \<GG> = cf_map (cf_of_cf_map \<CC> \<AA> (cf_map \<GG>))

goal (1 subgoal):
 1. \<And>f'. \<lbrakk>f' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>\<rbrakk> \<Longrightarrow> f' = ntcf_arrow \<sigma>
[PROOF STEP]
from \<sigma>'(1) \<FF>
[PROOF STATE]
proof (chain)
picking this:
ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' : cf_of_cf_map \<CC> \<AA> (cf_map \<FF>) \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<CC> \<AA> (cf_map \<GG>) : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have "ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' : cf_of_cf_map \<CC> \<AA> (cf_map \<FF>) \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<CC> \<AA> (cf_map \<GG>) : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by
          (
            cs_prems cs_shallow
              cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros
          )
[PROOF STATE]
proof (state)
this:
ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<And>f'. \<lbrakk>f' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>\<rbrakk> \<Longrightarrow> f' = ntcf_arrow \<sigma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<And>f'. \<lbrakk>f' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>\<rbrakk> \<Longrightarrow> f' = ntcf_arrow \<sigma>
[PROOF STEP]
from prems(2) prems(1) \<alpha>\<beta> assms(1-3) this \<epsilon>'(1)
[PROOF STATE]
proof (chain)
picking this:
\<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>\<sigma>'\<rparr>
\<sigma>' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>
\<alpha> \<in>\<^sub>\<circ> \<beta>
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' : cf_of_cf_map \<BB> \<AA> (exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>\<FF>'\<rparr>) \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<BB> \<AA> (cf_map \<TT>) : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have
        "ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' =
          \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>)"
[PROOF STATE]
proof (prove)
using this:
\<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>\<sigma>'\<rparr>
\<sigma>' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>
\<alpha> \<in>\<^sub>\<circ> \<beta>
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' : cf_of_cf_map \<BB> \<AA> (exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>\<FF>'\<rparr>) \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<BB> \<AA> (cf_map \<TT>) : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
by (subst (asm) \<epsilon>'(2))
          (
            cs_prems
              cs_simp: cat_Kan_cs_simps cat_FUNCT_cs_simps cat_cs_simps
              cs_intro:
                cat_Kan_cs_intros
                cat_small_cs_intros
                cat_cs_intros
                cat_FUNCT_cs_intros
          )
[PROOF STATE]
proof (state)
this:
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal (1 subgoal):
 1. \<And>f'. \<lbrakk>f' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>\<rbrakk> \<Longrightarrow> f' = ntcf_arrow \<sigma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
have \<sigma>_def: "\<sigma> = ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>'"
[PROOF STATE]
proof (prove)
using this:
ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
ntcf_of_ntcf_arrow \<BB> \<AA> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal (1 subgoal):
 1. \<sigma> = ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>'
[PROOF STEP]
by (rule unique_\<sigma>[symmetric])
[PROOF STATE]
proof (state)
this:
\<sigma> = ntcf_of_ntcf_arrow \<CC> \<AA> \<sigma>'

goal (1 subgoal):
 1. \<And>f'. \<lbrakk>f' : cf_map \<FF> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<FF>)\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>\<rbrakk> \<Longrightarrow> f' = ntcf_arrow \<sigma>
[PROOF STEP]
show "\<sigma>' = ntcf_arrow \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>' = ntcf_arrow \<sigma>
[PROOF STEP]
by (subst \<sigma>'(2), use nothing in \<open>subst \<sigma>_def\<close>)
          (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<sigma>' = ntcf_arrow \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!f'. f' : \<FF>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) \<FF>'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>

goal:
No subgoals!
[PROOF STEP]
qed