[STATEMENT]
lemma removeRedundant:
assumes (*<*)a:(*>*) "r1 = (p#ps,c) \<and> r1 \<in> upRules"
and     (*<*)b:(*>*) "r2 = (ps,c) \<and> r2 \<in> upRules"
and     (*<*)c:(*>*) "R1 \<subseteq> upRules \<and> R = Ax \<union> R1"
and     (*<*)d:(*>*) "(T,n) \<in> derivable (R \<union> {r1} \<union> {r2})*"
shows   "\<exists> m\<le>n. (T,m) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r1 = (p # ps, c) \<and> r1 \<in> upRules
r2 = (ps, c) \<and> r2 \<in> upRules
R1 \<subseteq> upRules \<and> R = Ax \<union> R1
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (prove)
using this:
r1 = (p # ps, c) \<and> r1 \<in> upRules
r2 = (ps, c) \<and> r2 \<in> upRules
R1 \<subseteq> upRules \<and> R = Ax \<union> R1
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
proof (induct n (*<*)arbitrary: T (*>*)rule:nat_less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n T. \<lbrakk>\<forall>m<n. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (\<forall>x. (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>ma\<le>m. (x, ma) \<in> derivable R \<union> {r2}*)); r1 = (p # ps, c) \<and> r1 \<in> upRules; r2 = (ps, c) \<and> r2 \<in> upRules; R1 \<subseteq> upRules \<and> R = Ax \<union> R1; (T, n) \<in> derivable R \<union> {r1} \<union> {r2}*\<rbrakk> \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n T. \<lbrakk>\<forall>m<n. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (\<forall>x. (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>ma\<le>m. (x, ma) \<in> derivable R \<union> {r2}*)); r1 = (p # ps, c) \<and> r1 \<in> upRules; r2 = (ps, c) \<and> r2 \<in> upRules; R1 \<subseteq> upRules \<and> R = Ax \<union> R1; (T, n) \<in> derivable R \<union> {r1} \<union> {r2}*\<rbrakk> \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
case (1 n T)
[PROOF STATE]
proof (state)
this:
\<forall>m<n. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (\<forall>x. (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>ma\<le>m. (x, ma) \<in> derivable R \<union> {r2}*))
r1 = (p # ps, c) \<and> r1 \<in> upRules
r2 = (ps, c) \<and> r2 \<in> upRules
R1 \<subseteq> upRules \<and> R = Ax \<union> R1
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. \<And>n T. \<lbrakk>\<forall>m<n. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (\<forall>x. (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>ma\<le>m. (x, ma) \<in> derivable R \<union> {r2}*)); r1 = (p # ps, c) \<and> r1 \<in> upRules; r2 = (ps, c) \<and> r2 \<in> upRules; R1 \<subseteq> upRules \<and> R = Ax \<union> R1; (T, n) \<in> derivable R \<union> {r1} \<union> {r2}*\<rbrakk> \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m<n. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (\<forall>x. (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>ma\<le>m. (x, ma) \<in> derivable R \<union> {r2}*))
r1 = (p # ps, c) \<and> r1 \<in> upRules
r2 = (ps, c) \<and> r2 \<in> upRules
R1 \<subseteq> upRules \<and> R = Ax \<union> R1
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*
[PROOF STEP]
have IH: " \<forall>m<n. \<forall> x. (r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow>
                         r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow>
                         R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow>
                         (x, m) \<in> derivable (R \<union> {r1} \<union> {r2})* \<longrightarrow>
                         (\<exists> m'\<le>m. (x, m') \<in> derivable (R \<union> {r2})*))" and
             prm: "(T,n) \<in> derivable (R \<union> {r1} \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (\<forall>x. (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>ma\<le>m. (x, ma) \<in> derivable R \<union> {r2}*))
r1 = (p # ps, c) \<and> r1 \<in> upRules
r2 = (ps, c) \<and> r2 \<in> upRules
R1 \<subseteq> upRules \<and> R = Ax \<union> R1
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. \<forall>m<n. \<forall>x. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>m'\<le>m. (x, m') \<in> derivable R \<union> {r2}*) &&& (T, n) \<in> derivable R \<union> {r1} \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m<n. \<forall>x. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>m'\<le>m. (x, m') \<in> derivable R \<union> {r2}*)
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. \<And>n T. \<lbrakk>\<forall>m<n. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (\<forall>x. (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>ma\<le>m. (x, ma) \<in> derivable R \<union> {r2}*)); r1 = (p # ps, c) \<and> r1 \<in> upRules; r2 = (ps, c) \<and> r2 \<in> upRules; R1 \<subseteq> upRules \<and> R = Ax \<union> R1; (T, n) \<in> derivable R \<union> {r1} \<union> {r2}*\<rbrakk> \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
proof (cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
with prm
[PROOF STATE]
proof (chain)
picking this:
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*
n = 0
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (chain)
picking this:
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*
n = 0
[PROOF STEP]
have "(T,0) \<in> derivable (R \<union> {r1} \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*
n = 0

goal (1 subgoal):
 1. (T, 0) \<in> derivable R \<union> {r1} \<union> {r2}*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(T, 0) \<in> derivable R \<union> {r1} \<union> {r2}*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(T, 0) \<in> derivable R \<union> {r1} \<union> {r2}*
[PROOF STEP]
have "([],T) \<in> (R \<union> {r1} \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
(T, 0) \<in> derivable R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. ([], T) \<in> R \<union> {r1} \<union> {r2}*
[PROOF STEP]
by (cases) auto
[PROOF STATE]
proof (state)
this:
([], T) \<in> R \<union> {r1} \<union> {r2}*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([], T) \<in> R \<union> {r1} \<union> {r2}*
[PROOF STEP]
obtain S r where ext: "extendRule S r = ([],T)" and
        "r \<in> (R \<union> {r1} \<union> {r2})"
[PROOF STATE]
proof (prove)
using this:
([], T) \<in> R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. (\<And>S r. \<lbrakk>extendRule S r = ([], T); r \<in> R \<union> {r1} \<union> {r2}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule extRules.cases) auto
[PROOF STATE]
proof (state)
this:
extendRule S r = ([], T)
r \<in> R \<union> {r1} \<union> {r2}

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = ([], T)
r \<in> R \<union> {r1} \<union> {r2}
[PROOF STEP]
have "r \<in> R \<or> r = r1 \<or> r = r2"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = ([], T)
r \<in> R \<union> {r1} \<union> {r2}

goal (1 subgoal):
 1. r \<in> R \<or> r = r1 \<or> r = r2
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
extendRule S r = ([], T)
r \<in> R \<union> {r1} \<union> {r2}
R1 \<subseteq> upRules \<and> R = Ax \<union> R1

goal (1 subgoal):
 1. r \<in> R \<or> r = r1 \<or> r = r2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> R \<or> r = r1 \<or> r = r2

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
txt\<open>\noindent It cannot be the case that $r=r_{1}$ or $r=r_{2}$, since those are \SC rules, whereas anything with an empty set of premisses
must be an axiom.  Since $\mathcal{R}$ contains the set of axioms, so will $\mathcal{R} \cup r_{2}$:\<close>
[PROOF STATE]
proof (state)
this:
r \<in> R \<or> r = r1 \<or> r = r2

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (state)
this:
r \<in> R \<or> r = r1 \<or> r = r2

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<in> R \<or> r = r1 \<or> r = r2

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
from ext
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = ([], T)
[PROOF STEP]
obtain d where "r = ([],d)"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = ([], T)

goal (1 subgoal):
 1. (\<And>d. r = ([], d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases r) (auto simp add:extendRule_def)
[PROOF STATE]
proof (state)
this:
r = ([], d)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r \<in> R \<or> r = r1 \<or> r = r2
r = ([], d)
[PROOF STEP]
have "r \<in> R \<or> r = r2"
[PROOF STATE]
proof (prove)
using this:
r \<in> R \<or> r = r1 \<or> r = r2
r = ([], d)

goal (1 subgoal):
 1. r \<in> R \<or> r = r2
[PROOF STEP]
using c a ext
[PROOF STATE]
proof (prove)
using this:
r \<in> R \<or> r = r1 \<or> r = r2
r = ([], d)
R1 \<subseteq> upRules \<and> R = Ax \<union> R1
r1 = (p # ps, c) \<and> r1 \<in> upRules
extendRule S r = ([], T)

goal (1 subgoal):
 1. r \<in> R \<or> r = r2
[PROOF STEP]
by (auto simp add:extendRule_def)
[PROOF STATE]
proof (state)
this:
r \<in> R \<or> r = r2

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (state)
this:
r \<in> R \<or> r = r2

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> R \<or> r = r2
[PROOF STEP]
have "r \<in> (R \<union> {r2})"
[PROOF STATE]
proof (prove)
using this:
r \<in> R \<or> r = r2

goal (1 subgoal):
 1. r \<in> R \<union> {r2}
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
r \<in> R \<or> r = r2
R1 \<subseteq> upRules \<and> R = Ax \<union> R1

goal (1 subgoal):
 1. r \<in> R \<union> {r2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2}

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2}

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> R \<union> {r2}
[PROOF STEP]
have "([],T) \<in> (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
r \<in> R \<union> {r2}

goal (1 subgoal):
 1. ([], T) \<in> R \<union> {r2}*
[PROOF STEP]
using \<open>extendRule S r = ([],T)\<close>
          and extRules.I[where r=r and R="R \<union> {r2}" and seq=S]
[PROOF STATE]
proof (prove)
using this:
r \<in> R \<union> {r2}
extendRule S r = ([], T)
r \<in> R \<union> {r2} \<Longrightarrow> extendRule S r \<in> R \<union> {r2}*

goal (1 subgoal):
 1. ([], T) \<in> R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([], T) \<in> R \<union> {r2}*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (state)
this:
([], T) \<in> R \<union> {r2}*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([], T) \<in> R \<union> {r2}*
[PROOF STEP]
have "(T,0) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
([], T) \<in> R \<union> {r2}*

goal (1 subgoal):
 1. (T, 0) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(T, 0) \<in> derivable R \<union> {r2}*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(T, 0) \<in> derivable R \<union> {r2}*
[PROOF STEP]
show "\<exists> m\<le>n. (T,m) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
(T, 0) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
using \<open>n=0\<close>
[PROOF STATE]
proof (prove)
using this:
(T, 0) \<in> derivable R \<union> {r2}*
n = 0

goal (1 subgoal):
 1. \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
case (Suc n')
[PROOF STATE]
proof (state)
this:
n = Suc n'

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (state)
this:
n = Suc n'

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
with prm
[PROOF STATE]
proof (chain)
picking this:
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*
n = Suc n'
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (chain)
picking this:
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*
n = Suc n'
[PROOF STEP]
have "(T,n'+1) \<in> derivable (R \<union> {r1} \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
(T, n) \<in> derivable R \<union> {r1} \<union> {r2}*
n = Suc n'

goal (1 subgoal):
 1. (T, n' + 1) \<in> derivable R \<union> {r1} \<union> {r2}*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(T, n' + 1) \<in> derivable R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(T, n' + 1) \<in> derivable R \<union> {r1} \<union> {r2}*
[PROOF STEP]
obtain Ps where e: "Ps \<noteq> []"
         and   f: "(Ps,T) \<in> (R \<union> {r1} \<union> {r2})*"
         and   g: "\<forall> P \<in> set Ps. \<exists> m\<le>n'. (P,m) \<in> derivable (R \<union> {r1} \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
(T, n' + 1) \<in> derivable R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. (\<And>Ps. \<lbrakk>Ps \<noteq> []; (Ps, T) \<in> R \<union> {r1} \<union> {r2}*; \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r1} \<union> {r2}*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
using this:
(T, n' + 1) \<in> derivable R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. (\<And>Ps. \<lbrakk>Ps \<noteq> []; (Ps, T) \<in> R \<union> {r1} \<union> {r2}*; \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r1} \<union> {r2}*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using characteriseLast[where C=T and m=n' and R="(R \<union> {r1} \<union> {r2})*"]
[PROOF STATE]
proof (prove)
using this:
(T, n' + 1) \<in> derivable R \<union> {r1} \<union> {r2}*
(T, n' + 1) \<in> derivable R \<union> {r1} \<union> {r2}* \<Longrightarrow> \<exists>Ps. Ps \<noteq> [] \<and> (Ps, T) \<in> R \<union> {r1} \<union> {r2}* \<and> (\<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R \<union> {r1} \<union> {r2}*)

goal (1 subgoal):
 1. (\<And>Ps. \<lbrakk>Ps \<noteq> []; (Ps, T) \<in> R \<union> {r1} \<union> {r2}*; \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r1} \<union> {r2}*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (prove)
using this:
(T, n' + 1) \<in> derivable R \<union> {r1} \<union> {r2}*
(T, n' + 1) \<in> derivable R \<union> {r1} \<union> {r2}* \<Longrightarrow> \<exists>Ps. Ps \<noteq> [] \<and> (Ps, T) \<in> R \<union> {r1} \<union> {r2}* \<and> (\<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R \<union> {r1} \<union> {r2}*)

goal (1 subgoal):
 1. (\<And>Ps. \<lbrakk>Ps \<noteq> []; (Ps, T) \<in> R \<union> {r1} \<union> {r2}*; \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r1} \<union> {r2}*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ps \<noteq> []
(Ps, T) \<in> R \<union> {r1} \<union> {r2}*
\<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
have g': "\<forall> P \<in> set Ps. \<exists> m\<le>n'. (P,m) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
assume "P \<in> set Ps"
[PROOF STATE]
proof (state)
this:
P \<in> set Ps

goal (1 subgoal):
 1. \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
with g
[PROOF STATE]
proof (chain)
picking this:
\<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r1} \<union> {r2}*
P \<in> set Ps
[PROOF STEP]
obtain m where "(P,m) \<in> derivable (R \<union> {r1} \<union> {r2})*" and "m\<le>n'"
[PROOF STATE]
proof (prove)
using this:
\<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r1} \<union> {r2}*
P \<in> set Ps

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>(P, m) \<in> derivable R \<union> {r1} \<union> {r2}*; m \<le> n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(P, m) \<in> derivable R \<union> {r1} \<union> {r2}*
m \<le> n'

goal (1 subgoal):
 1. \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
with IH
[PROOF STATE]
proof (chain)
picking this:
\<forall>m<n. \<forall>x. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>m'\<le>m. (x, m') \<in> derivable R \<union> {r2}*)
(P, m) \<in> derivable R \<union> {r1} \<union> {r2}*
m \<le> n'
[PROOF STEP]
have "\<exists> m'\<le>m. (P,m') \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. \<forall>x. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>m'\<le>m. (x, m') \<in> derivable R \<union> {r2}*)
(P, m) \<in> derivable R \<union> {r1} \<union> {r2}*
m \<le> n'

goal (1 subgoal):
 1. \<exists>m'\<le>m. (P, m') \<in> derivable R \<union> {r2}*
[PROOF STEP]
using a b c and \<open>n = Suc n'\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. \<forall>x. r1 = (p # ps, c) \<and> r1 \<in> upRules \<longrightarrow> r2 = (ps, c) \<and> r2 \<in> upRules \<longrightarrow> R1 \<subseteq> upRules \<and> R = Ax \<union> R1 \<longrightarrow> (x, m) \<in> derivable R \<union> {r1} \<union> {r2}* \<longrightarrow> (\<exists>m'\<le>m. (x, m') \<in> derivable R \<union> {r2}*)
(P, m) \<in> derivable R \<union> {r1} \<union> {r2}*
m \<le> n'
r1 = (p # ps, c) \<and> r1 \<in> upRules
r2 = (ps, c) \<and> r2 \<in> upRules
R1 \<subseteq> upRules \<and> R = Ax \<union> R1
n = Suc n'

goal (1 subgoal):
 1. \<exists>m'\<le>m. (P, m') \<in> derivable R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m'\<le>m. (P, m') \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m'\<le>m. (P, m') \<in> derivable R \<union> {r2}*
[PROOF STEP]
have "\<exists> m\<le>n'. (P,m) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
\<exists>m'\<le>m. (P, m') \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
using \<open>m\<le>n'\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>m'\<le>m. (P, m') \<in> derivable R \<union> {r2}*
m \<le> n'

goal (1 subgoal):
 1. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m'. \<lbrakk>m \<le> n'; m' \<le> m; (P, m') \<in> derivable insert r2 R*\<rbrakk> \<Longrightarrow> \<exists>m\<le>n'. (P, m) \<in> derivable insert r2 R*
[PROOF STEP]
by (rule_tac x=m' in exI) auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?P2 \<in> set Ps \<Longrightarrow> \<exists>m\<le>n'. (?P2, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?P2 \<in> set Ps \<Longrightarrow> \<exists>m\<le>n'. (?P2, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?P2 \<in> set Ps \<Longrightarrow> \<exists>m\<le>n'. (?P2, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (state)
this:
\<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
(Ps, T) \<in> R \<union> {r1} \<union> {r2}*
[PROOF STEP]
obtain S r where ext: "extendRule S r = (Ps,T)"
        and "r \<in> (R \<union> {r1} \<union> {r2})"
[PROOF STATE]
proof (prove)
using this:
(Ps, T) \<in> R \<union> {r1} \<union> {r2}*

goal (1 subgoal):
 1. (\<And>S r. \<lbrakk>extendRule S r = (Ps, T); r \<in> R \<union> {r1} \<union> {r2}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule extRules.cases) auto
[PROOF STATE]
proof (state)
this:
extendRule S r = (Ps, T)
r \<in> R \<union> {r1} \<union> {r2}

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = (Ps, T)
r \<in> R \<union> {r1} \<union> {r2}
[PROOF STEP]
have "r \<in> (R \<union> {r2}) \<or> r = r1"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = (Ps, T)
r \<in> R \<union> {r1} \<union> {r2}

goal (1 subgoal):
 1. r \<in> R \<union> {r2} \<or> r = r1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2} \<or> r = r1

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
txt\<open>\noindent Either $r$ is in the new rule set or $r$ is the redundant rule.  In the former case, there is nothing to do:\<close>
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2} \<or> r = r1

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2} \<or> r = r1

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2} \<or> r = r1

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2} \<or> r = r1

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2} \<or> r = r1

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
assume "r \<in> (R \<union> {r2})"
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2}

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> R \<union> {r2}
[PROOF STEP]
have "(Ps,T) \<in> (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
r \<in> R \<union> {r2}

goal (1 subgoal):
 1. (Ps, T) \<in> R \<union> {r2}*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
using this:
r \<in> R \<union> {r2}

goal (1 subgoal):
 1. (Ps, T) \<in> R \<union> {r2}*
[PROOF STEP]
using ext and extRules.I[where r=r and R="R \<union> {r2}" and seq=S]
[PROOF STATE]
proof (prove)
using this:
r \<in> R \<union> {r2}
extendRule S r = (Ps, T)
r \<in> R \<union> {r2} \<Longrightarrow> extendRule S r \<in> R \<union> {r2}*

goal (1 subgoal):
 1. (Ps, T) \<in> R \<union> {r2}*
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (prove)
using this:
r \<in> R \<union> {r2}
extendRule S r = (Ps, T)
r \<in> R \<union> {r2} \<Longrightarrow> extendRule S r \<in> R \<union> {r2}*

goal (1 subgoal):
 1. (Ps, T) \<in> R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Ps, T) \<in> R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
with g'
[PROOF STATE]
proof (chain)
picking this:
\<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
(Ps, T) \<in> R \<union> {r2}*
[PROOF STEP]
have "(T,n) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
\<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
(Ps, T) \<in> R \<union> {r2}*

goal (1 subgoal):
 1. (T, n) \<in> derivable R \<union> {r2}*
[PROOF STEP]
using \<open>n = Suc n'\<close> (*<*)and e and
       derivable.step[where r="(Ps,T)" and R="(R \<union> {r2})*" and m=n']
[PROOF STATE]
proof (prove)
using this:
\<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
(Ps, T) \<in> R \<union> {r2}*
n = Suc n'
Ps \<noteq> []
\<lbrakk>(Ps, T) \<in> R \<union> {r2}*; fst (Ps, T) \<noteq> []; \<forall>p\<in>set (fst (Ps, T)). \<exists>n\<le>n'. (p, n) \<in> derivable R \<union> {r2}*\<rbrakk> \<Longrightarrow> (snd (Ps, T), n' + 1) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. (T, n) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (prove)
using this:
\<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
(Ps, T) \<in> R \<union> {r2}*
n = Suc n'
Ps \<noteq> []
\<lbrakk>(Ps, T) \<in> R \<union> {r2}*; fst (Ps, T) \<noteq> []; \<forall>p\<in>set (fst (Ps, T)). \<exists>n\<le>n'. (p, n) \<in> derivable R \<union> {r2}*\<rbrakk> \<Longrightarrow> (snd (Ps, T), n' + 1) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. (T, n) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(T, n) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (state)
this:
(T, n) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2} \<Longrightarrow> (T, n) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2} \<Longrightarrow> (T, n) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2} \<Longrightarrow> (T, n) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2} \<Longrightarrow> (T, n) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
txt\<open>\noindent In the latter case, the last inference was redundant.  Therefore the premisses, which are derivable at a lower height than the conclusion,
contain the premisses of $r_{2}$ (these premisses are \texttt{extend S ps}).  This completes the proof:\<close>
[PROOF STATE]
proof (state)
this:
r \<in> R \<union> {r2} \<Longrightarrow> (T, n) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
assume "r = r1"
[PROOF STATE]
proof (state)
this:
r = r1

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
with ext
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = (Ps, T)
r = r1
[PROOF STEP]
have "map (extend S) (p # ps) = Ps"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = (Ps, T)
r = r1

goal (1 subgoal):
 1. map (extend S) (p # ps) = Ps
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
extendRule S r = (Ps, T)
r = r1
r1 = (p # ps, c) \<and> r1 \<in> upRules

goal (1 subgoal):
 1. map (extend S) (p # ps) = Ps
[PROOF STEP]
by (auto(*<*) simp add:extendRule_def(*>*))
[PROOF STATE]
proof (state)
this:
map (extend S) (p # ps) = Ps

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (extend S) (p # ps) = Ps
[PROOF STEP]
have "\<forall> P \<in> set (map (extend S) (p#ps)).
                   \<exists> m\<le>n'. (P,m) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
map (extend S) (p # ps) = Ps

goal (1 subgoal):
 1. \<forall>P\<in>set (map (extend S) (p # ps)). \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
using g'
[PROOF STATE]
proof (prove)
using this:
map (extend S) (p # ps) = Ps
\<forall>P\<in>set Ps. \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<forall>P\<in>set (map (extend S) (p # ps)). \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>P\<in>set (map (extend S) (p # ps)). \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>P\<in>set (map (extend S) (p # ps)). \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
have h: "\<forall> P \<in> set (map (extend S) ps).
                      \<exists> m\<le>n'. (P,m) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
\<forall>P\<in>set (map (extend S) (p # ps)). \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<forall>P\<in>set (map (extend S) ps). \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>P\<in>set (map (extend S) ps). \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (state)
this:
\<forall>P\<in>set (map (extend S) ps). \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
have "extendRule S r2 = (map (extend S) ps, T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extendRule S r2 = (map (extend S) ps, T)
[PROOF STEP]
using b and a and ext and \<open>r = r1\<close>
[PROOF STATE]
proof (prove)
using this:
r2 = (ps, c) \<and> r2 \<in> upRules
r1 = (p # ps, c) \<and> r1 \<in> upRules
extendRule S r = (Ps, T)
r = r1

goal (1 subgoal):
 1. extendRule S r2 = (map (extend S) ps, T)
[PROOF STEP]
by (auto simp add:extendRule_def)
[PROOF STATE]
proof (state)
this:
extendRule S r2 = (map (extend S) ps, T)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extendRule S r2 = (map (extend S) ps, T)
[PROOF STEP]
have i: "(map (extend S) ps,T) \<in> (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
extendRule S r2 = (map (extend S) ps, T)

goal (1 subgoal):
 1. (map (extend S) ps, T) \<in> R \<union> {r2}*
[PROOF STEP]
using extRules.I(*<*)[where r=r2 and R="(R \<union> {r2})" and seq=S]
[PROOF STATE]
proof (prove)
using this:
extendRule S r2 = (map (extend S) ps, T)
r2 \<in> R \<union> {r2} \<Longrightarrow> extendRule S r2 \<in> R \<union> {r2}*

goal (1 subgoal):
 1. (map (extend S) ps, T) \<in> R \<union> {r2}*
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (prove)
using this:
extendRule S r2 = (map (extend S) ps, T)
r2 \<in> R \<union> {r2} \<Longrightarrow> extendRule S r2 \<in> R \<union> {r2}*

goal (1 subgoal):
 1. (map (extend S) ps, T) \<in> R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(map (extend S) ps, T) \<in> R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
have "ps = [] \<or> ps \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps = [] \<or> ps \<noteq> []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ps = [] \<or> ps \<noteq> []

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ps = [] \<or> ps \<noteq> []

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ps = [] \<or> ps \<noteq> []

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
assume "ps = []"
[PROOF STATE]
proof (state)
this:
ps = []

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
(map (extend S) ps, T) \<in> R \<union> {r2}*
ps = []
[PROOF STEP]
have "([],T) \<in> (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
(map (extend S) ps, T) \<in> R \<union> {r2}*
ps = []

goal (1 subgoal):
 1. ([], T) \<in> R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([], T) \<in> R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([], T) \<in> R \<union> {r2}*
[PROOF STEP]
have "(T,0) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
([], T) \<in> R \<union> {r2}*

goal (1 subgoal):
 1. (T, 0) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(T, 0) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(T, 0) \<in> derivable R \<union> {r2}*
[PROOF STEP]
have "\<exists> m\<le>n. (T,m) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
(T, 0) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ps = [] \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ps = [] \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ps = [] \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
assume "ps \<noteq> []"
[PROOF STATE]
proof (state)
this:
ps \<noteq> []

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ps \<noteq> []
[PROOF STEP]
have "map (extend S) ps \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
ps \<noteq> []

goal (1 subgoal):
 1. map (extend S) ps \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (extend S) ps \<noteq> []

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
with i and h
[PROOF STATE]
proof (chain)
picking this:
(map (extend S) ps, T) \<in> R \<union> {r2}*
\<forall>P\<in>set (map (extend S) ps). \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
map (extend S) ps \<noteq> []
[PROOF STEP]
have "(T,n'+1) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
(map (extend S) ps, T) \<in> R \<union> {r2}*
\<forall>P\<in>set (map (extend S) ps). \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
map (extend S) ps \<noteq> []

goal (1 subgoal):
 1. (T, n' + 1) \<in> derivable R \<union> {r2}*
[PROOF STEP]
using derivable.step[where r="(map (extend S) ps,T)" and R="(R \<union> {r2})*" and m=n']
[PROOF STATE]
proof (prove)
using this:
(map (extend S) ps, T) \<in> R \<union> {r2}*
\<forall>P\<in>set (map (extend S) ps). \<exists>m\<le>n'. (P, m) \<in> derivable R \<union> {r2}*
map (extend S) ps \<noteq> []
\<lbrakk>(map (extend S) ps, T) \<in> R \<union> {r2}*; fst (map (extend S) ps, T) \<noteq> []; \<forall>p\<in>set (fst (map (extend S) ps, T)). \<exists>n\<le>n'. (p, n) \<in> derivable R \<union> {r2}*\<rbrakk> \<Longrightarrow> (snd (map (extend S) ps, T), n' + 1) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. (T, n' + 1) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(T, n' + 1) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
with \<open>n = Suc n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n = Suc n'
(T, n' + 1) \<in> derivable R \<union> {r2}*
[PROOF STEP]
have "\<exists> m\<le>n. (T,m) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
n = Suc n'
(T, n' + 1) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ps \<noteq> [] \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ps = [] \<or> ps \<noteq> []
ps = [] \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
ps \<noteq> [] \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
have "\<exists> m\<le>n. (T,m) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
ps = [] \<or> ps \<noteq> []
ps = [] \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
ps \<noteq> [] \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
r = r1 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r \<in> R \<union> {r2} \<or> r = r1
r \<in> R \<union> {r2} \<Longrightarrow> (T, n) \<in> derivable R \<union> {r2}*
r = r1 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
show "\<exists> m\<le>n. (T,m) \<in> derivable (R \<union> {r2})*"
[PROOF STATE]
proof (prove)
using this:
r \<in> R \<union> {r2} \<or> r = r1
r \<in> R \<union> {r2} \<Longrightarrow> (T, n) \<in> derivable R \<union> {r2}*
r = r1 \<Longrightarrow> \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal (1 subgoal):
 1. \<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. (T, m) \<in> derivable R \<union> {r2}*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_on_rsuml [simp]: "inj_on rsuml A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on rsuml A
[PROOF STEP]
by(auto simp add: inj_on_def elim: rsuml.elims)


[STATEMENT]
lemma analz_Un_partition:
  "analz S \<subseteq> synth (analz ((S \<inter> payload) \<union> (S \<inter> valid) \<union> (S \<inter> range LtK) \<union> Tags)) \<Longrightarrow>
  H \<subseteq> payload \<union> valid \<union> range LtK \<Longrightarrow>
  analz (H \<union> S) \<subseteq>
    synth (analz (((H \<union> S) \<inter> payload) \<union> ((H \<union> S) \<inter> valid) \<union> ((H \<union> S) \<inter> range LtK) \<union> Tags))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)); H \<subseteq> payload \<union> valid \<union> range LtK\<rbrakk> \<Longrightarrow> analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)); H \<subseteq> payload \<union> valid \<union> range LtK\<rbrakk> \<Longrightarrow> analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
assume "H \<subseteq> payload \<union> valid \<union> range LtK"
[PROOF STATE]
proof (state)
this:
H \<subseteq> payload \<union> valid \<union> range LtK

goal (1 subgoal):
 1. \<lbrakk>analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)); H \<subseteq> payload \<union> valid \<union> range LtK\<rbrakk> \<Longrightarrow> analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
H \<subseteq> payload \<union> valid \<union> range LtK
[PROOF STEP]
have HH:"H = (H \<inter> payload) \<union> (H \<inter> valid) \<union> (H \<inter> range LtK)"
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> payload \<union> valid \<union> range LtK

goal (1 subgoal):
 1. H = H \<inter> payload \<union> H \<inter> valid \<union> H \<inter> range LtK
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H = H \<inter> payload \<union> H \<inter> valid \<union> H \<inter> range LtK

goal (1 subgoal):
 1. \<lbrakk>analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)); H \<subseteq> payload \<union> valid \<union> range LtK\<rbrakk> \<Longrightarrow> analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
assume HA:
    "analz S \<subseteq> synth (analz ((S \<inter> payload) \<union> (S \<inter> valid) \<union> (S \<inter> range LtK) \<union> Tags))"
[PROOF STATE]
proof (state)
this:
analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags))

goal (1 subgoal):
 1. \<lbrakk>analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)); H \<subseteq> payload \<union> valid \<union> range LtK\<rbrakk> \<Longrightarrow> analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags))
[PROOF STEP]
have
   "analz (H \<union> S) \<subseteq>
    synth (analz (H \<union> ((S \<inter> payload) \<union> (S \<inter> valid) \<union> (S \<inter> range LtK) \<union> Tags)))"
[PROOF STATE]
proof (prove)
using this:
analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags))

goal (1 subgoal):
 1. analz (H \<union> S) \<subseteq> synth (analz (H \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)))
[PROOF STEP]
by (rule analz_synth_subset_Un2)
[PROOF STATE]
proof (state)
this:
analz (H \<union> S) \<subseteq> synth (analz (H \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)))

goal (1 subgoal):
 1. \<lbrakk>analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)); H \<subseteq> payload \<union> valid \<union> range LtK\<rbrakk> \<Longrightarrow> analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
analz (H \<union> S) \<subseteq> synth (analz (H \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)))

goal (1 subgoal):
 1. \<lbrakk>analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)); H \<subseteq> payload \<union> valid \<union> range LtK\<rbrakk> \<Longrightarrow> analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
with HH
[PROOF STATE]
proof (chain)
picking this:
H = H \<inter> payload \<union> H \<inter> valid \<union> H \<inter> range LtK
analz (H \<union> S) \<subseteq> synth (analz (H \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)))
[PROOF STEP]
have
    "... \<subseteq> synth (analz (((H \<inter> payload) \<union> (H \<inter> valid) \<union> (H \<inter> range LtK)) \<union>
                         ((S \<inter> payload) \<union> (S \<inter> valid) \<union> (S \<inter> range LtK) \<union> Tags)))"
[PROOF STATE]
proof (prove)
using this:
H = H \<inter> payload \<union> H \<inter> valid \<union> H \<inter> range LtK
analz (H \<union> S) \<subseteq> synth (analz (H \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)))

goal (1 subgoal):
 1. synth (analz (H \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags))) \<subseteq> synth (analz (H \<inter> payload \<union> H \<inter> valid \<union> H \<inter> range LtK \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
synth (analz (H \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags))) \<subseteq> synth (analz (H \<inter> payload \<union> H \<inter> valid \<union> H \<inter> range LtK \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)))

goal (1 subgoal):
 1. \<lbrakk>analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)); H \<subseteq> payload \<union> valid \<union> range LtK\<rbrakk> \<Longrightarrow> analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
synth (analz (H \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags))) \<subseteq> synth (analz (H \<inter> payload \<union> H \<inter> valid \<union> H \<inter> range LtK \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)))

goal (1 subgoal):
 1. \<lbrakk>analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)); H \<subseteq> payload \<union> valid \<union> range LtK\<rbrakk> \<Longrightarrow> analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
have "... = synth (analz (((H \<union> S) \<inter> payload) \<union> ((H \<union> S) \<inter> valid) \<union>
                                 ((H \<union> S) \<inter> range LtK) \<union> Tags))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. synth (analz (H \<inter> payload \<union> H \<inter> valid \<union> H \<inter> range LtK \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags))) = synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
by (simp add: Un_left_commute sup.commute Int_Un_distrib2)
[PROOF STATE]
proof (state)
this:
synth (analz (H \<inter> payload \<union> H \<inter> valid \<union> H \<inter> range LtK \<union> (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags))) = synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))

goal (1 subgoal):
 1. \<lbrakk>analz S \<subseteq> synth (analz (S \<inter> payload \<union> S \<inter> valid \<union> S \<inter> range LtK \<union> Tags)); H \<subseteq> payload \<union> valid \<union> range LtK\<rbrakk> \<Longrightarrow> analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))

goal (1 subgoal):
 1. analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
analz (H \<union> S) \<subseteq> synth (analz ((H \<union> S) \<inter> payload \<union> (H \<union> S) \<inter> valid \<union> (H \<union> S) \<inter> range LtK \<union> Tags))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntcf_const_ntcf_vcomp[cat_cs_simps]:
  assumes "category \<alpha> \<JJ>"
    and "category \<alpha> \<CC>"
    and "g : b \<mapsto>\<^bsub>\<CC>\<^esub> c"
    and "f : a \<mapsto>\<^bsub>\<CC>\<^esub> b"
  shows "ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)
[PROOF STEP]
interpret \<JJ>: category \<alpha> \<JJ>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> \<JJ>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)
[PROOF STEP]
interpret \<CC>: category \<alpha> \<CC>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> \<CC>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)
[PROOF STEP]
from assms(3,4)
[PROOF STATE]
proof (chain)
picking this:
g : b \<mapsto>\<^bsub>\<CC>\<^esub> c
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[PROOF STEP]
have gf: "g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f : a \<mapsto>\<^bsub>\<CC>\<^esub> c"
[PROOF STATE]
proof (prove)
using this:
g : b \<mapsto>\<^bsub>\<CC>\<^esub> c
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f : a \<mapsto>\<^bsub>\<CC>\<^esub> c
[PROOF STEP]
by (simp add: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f : a \<mapsto>\<^bsub>\<CC>\<^esub> c

goal (1 subgoal):
 1. ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)
[PROOF STEP]
note \<JJ>\<CC>g = ntcf_const_is_ntcf[OF assms(1,2,3)]
    and \<JJ>\<CC>f = ntcf_const_is_ntcf[OF assms(1,2,4)]
[PROOF STATE]
proof (state)
this:
ntcf_const \<JJ> \<CC> g : dghm_const \<JJ> \<CC> b (\<CC>\<lparr>CId\<rparr>\<lparr>b\<rparr>) \<mapsto>\<^sub>C\<^sub>F dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>) : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
ntcf_const \<JJ> \<CC> f : dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>) \<mapsto>\<^sub>C\<^sub>F dghm_const \<JJ> \<CC> b (\<CC>\<lparr>CId\<rparr>\<lparr>b\<rparr>) : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)
[PROOF STEP]
proof(rule ntcf_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f) : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr> = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
from ntcf_const_is_ntcf[OF assms(1,2,3)] ntcf_const_is_ntcf[OF assms(1,2,4)]
[PROOF STATE]
proof (chain)
picking this:
ntcf_const \<JJ> \<CC> g : dghm_const \<JJ> \<CC> b (\<CC>\<lparr>CId\<rparr>\<lparr>b\<rparr>) \<mapsto>\<^sub>C\<^sub>F dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>) : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
ntcf_const \<JJ> \<CC> f : dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>) \<mapsto>\<^sub>C\<^sub>F dghm_const \<JJ> \<CC> b (\<CC>\<lparr>CId\<rparr>\<lparr>b\<rparr>) : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show
      "ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f :
        cf_const \<JJ> \<CC> a \<mapsto>\<^sub>C\<^sub>F cf_const \<JJ> \<CC> c : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
using this:
ntcf_const \<JJ> \<CC> g : dghm_const \<JJ> \<CC> b (\<CC>\<lparr>CId\<rparr>\<lparr>b\<rparr>) \<mapsto>\<^sub>C\<^sub>F dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>) : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
ntcf_const \<JJ> \<CC> f : dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>) \<mapsto>\<^sub>C\<^sub>F dghm_const \<JJ> \<CC> b (\<CC>\<lparr>CId\<rparr>\<lparr>b\<rparr>) : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f : dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>) \<mapsto>\<^sub>C\<^sub>F dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>) : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule ntcf_vcomp_is_ntcf)
[PROOF STATE]
proof (state)
this:
ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f : dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>) \<mapsto>\<^sub>C\<^sub>F dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>) : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (6 subgoals):
 1. ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f) : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. (ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr> = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>NTMap\<rparr>
 3. dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>) = ?\<FF>'
 4. dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>) = ?\<GG>'
 5. \<JJ> = ?\<AA>'
 6. \<CC> = ?\<BB>'
[PROOF STEP]
show
      "ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f) :
        cf_const \<JJ> \<CC> a \<mapsto>\<^sub>C\<^sub>F cf_const \<JJ> \<CC> c : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f) : dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>) \<mapsto>\<^sub>C\<^sub>F dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>) : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule ntcf_const_is_ntcf[OF assms(1,2) gf])
[PROOF STATE]
proof (state)
this:
ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f) : dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>) \<mapsto>\<^sub>C\<^sub>F dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>) : \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (5 subgoals):
 1. (ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr> = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>NTMap\<rparr>
 2. dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>) = dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>)
 3. dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>) = dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>)
 4. \<JJ> = \<JJ>
 5. \<CC> = \<CC>
[PROOF STEP]
show "(ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr> =
      ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr> = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>NTMap\<rparr>
[PROOF STEP]
unfolding ntcf_const_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr> = vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)
[PROOF STEP]
proof(rule vsv_eqI, unfold ntcf_vcomp_NTMap_vdomain[OF \<JJ>\<CC>f])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr>)
 2. vsv (vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f))
 3. \<JJ>\<lparr>Obj\<rparr> = \<D>\<^sub>\<circ> (vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f))
 4. \<And>a. a \<in>\<^sub>\<circ> \<JJ>\<lparr>Obj\<rparr> \<Longrightarrow> (ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr>)
 2. vsv (vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f))
 3. \<JJ>\<lparr>Obj\<rparr> = \<D>\<^sub>\<circ> (vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f))
 4. \<And>a. a \<in>\<^sub>\<circ> \<JJ>\<lparr>Obj\<rparr> \<Longrightarrow> (ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>a\<rparr>
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<JJ>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<JJ>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv ((ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr>)
 2. vsv (vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f))
 3. \<JJ>\<lparr>Obj\<rparr> = \<D>\<^sub>\<circ> (vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f))
 4. \<And>a. a \<in>\<^sub>\<circ> \<JJ>\<lparr>Obj\<rparr> \<Longrightarrow> (ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<JJ>\<lparr>Obj\<rparr>
[PROOF STEP]
show
        "(ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> =
          vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<JJ>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>a\<rparr>
[PROOF STEP]
unfolding ntcf_vcomp_NTMap_app[OF \<JJ>\<CC>g \<JJ>\<CC>f prems]
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<JJ>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. ntcf_const \<JJ> \<CC> g\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> ntcf_const \<JJ> \<CC> f\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>a\<rparr>
[PROOF STEP]
by (simp add: ntcf_const_components)
[PROOF STATE]
proof (state)
this:
(ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv ((ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr>)
 2. vsv (vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f))
 3. \<JJ>\<lparr>Obj\<rparr> = \<D>\<^sub>\<circ> (vconst_on (\<JJ>\<lparr>Obj\<rparr>) (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f))
[PROOF STEP]
qed (simp_all add: ntsmcf_vcomp_components)
[PROOF STATE]
proof (state)
this:
(ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f)\<lparr>NTMap\<rparr> = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)\<lparr>NTMap\<rparr>

goal (4 subgoals):
 1. dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>) = dghm_const \<JJ> \<CC> a (\<CC>\<lparr>CId\<rparr>\<lparr>a\<rparr>)
 2. dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>) = dghm_const \<JJ> \<CC> c (\<CC>\<lparr>CId\<rparr>\<lparr>c\<rparr>)
 3. \<JJ> = \<JJ>
 4. \<CC> = \<CC>
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
ntcf_const \<JJ> \<CC> g \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<JJ> \<CC> f = ntcf_const \<JJ> \<CC> (g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_iso_arr_is_iso_ntcf:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<MM> : \<GG> \<mapsto>\<^sub>C\<^sub>F \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<MM> = ntcf_id \<GG>"
    and "\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<NN> = ntcf_id \<FF>"
  shows "\<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
interpret \<NN>: is_ntcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
interpret \<MM>: is_ntcf \<alpha> \<AA> \<BB> \<GG> \<FF> \<MM>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> : \<GG> \<mapsto>\<^sub>C\<^sub>F \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
proof(rule is_iso_ntcfI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (2 subgoals):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
proof(rule is_iso_arrI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
 2. is_inverse \<BB> ?g (\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
show "is_inverse \<BB> (\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>) (\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inverse \<BB> (\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>) (\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
proof(rule is_inverseI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?a
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?a\<rparr>
 4. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
have
          "\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (simp add: ntcf_vcomp_NTMap_app[OF assms(2,1) prems])
[PROOF STATE]
proof (state)
this:
\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (4 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?a
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?a\<rparr>
 4. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (4 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?a
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?a\<rparr>
 4. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
have "\<dots> = ntcf_id \<FF>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_id \<FF>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
unfolding assms(4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_id \<FF>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_id \<FF>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_id \<FF>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (4 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?a
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?a\<rparr>
 4. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_id \<FF>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (4 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?a
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?a\<rparr>
 4. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
from prems \<NN>.NTDom.ntcf_id_NTMap_app_vdomain
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> ntcf_id \<FF>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>\<rparr>
[PROOF STEP]
have
          "\<dots> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> ntcf_id \<FF>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>\<rparr>

goal (1 subgoal):
 1. ntcf_id \<FF>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
unfolding ntcf_id_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<FF>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ObjMap\<rparr>)\<lparr>?a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>\<rparr>

goal (1 subgoal):
 1. (\<FF>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ObjMap\<rparr>)\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ntcf_id \<FF>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>

goal (4 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?a
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?a\<rparr>
 4. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
show "\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>

goal (1 subgoal):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>

goal (3 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
have
          "\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (simp add: ntcf_vcomp_NTMap_app[OF assms(1,2) prems])
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
have "\<dots> = ntcf_id \<GG>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_id \<GG>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
unfolding assms(3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_id \<GG>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_id \<GG>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_id \<GG>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_id \<GG>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
from prems \<NN>.NTCod.ntcf_id_NTMap_app_vdomain
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> ntcf_id \<GG>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>\<rparr>
[PROOF STEP]
have
          "\<dots> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> ntcf_id \<GG>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>\<rparr>

goal (1 subgoal):
 1. ntcf_id \<GG>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
unfolding ntcf_id_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<GG>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr> \<circ>\<^sub>\<circ> \<GG>\<lparr>ObjMap\<rparr>)\<lparr>?a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>\<rparr>

goal (1 subgoal):
 1. (\<GG>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr> \<circ>\<^sub>\<circ> \<GG>\<lparr>ObjMap\<rparr>)\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ntcf_id \<GG>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>

goal (3 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : ?b \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> ?b
 3. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>?b\<rparr>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
show "\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>

goal (2 subgoals):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
 2. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
qed (auto simp: prems cat_cs_intros)
[PROOF STATE]
proof (state)
this:
is_inverse \<BB> (\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>) (\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
qed (auto simp: prems cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
qed (auto simp: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma WeakI2: "[| Gamma : deductions(A); Perms <= A; Weaks <= A |] ==> (Gamma @ Delta) : deductions(A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma \<in> deductions A; Perms \<subseteq> A; Weaks \<subseteq> A\<rbrakk> \<Longrightarrow> Gamma @ Delta \<in> deductions A
[PROOF STEP]
apply (auto intro: PermI [of \<open>Delta @ Gamma\<close>] WeakI1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma equivp_qr_rel: "equivp qr_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivp qr_rel
[PROOF STEP]
by (intro equivpI sympI reflpI transpI)
     (auto simp: qr_rel_def cong_sym intro: cong_trans)


[STATEMENT]
lemma WHILE_bounded:
    "m \<bind> WHILE cond step
    = filter_nb cond (Sup {bounded_WHILE n cond step m | n. True})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<bind> WHILE cond step = filter_nb cond (Sup {bounded_WHILE n cond step m |n. True})
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. m \<bind> WHILE cond step \<le> filter_nb cond (Sup {bounded_WHILE n cond step m |n. True})
 2. filter_nb cond (Sup {bounded_WHILE n cond step m |n. True}) \<le> m \<bind> WHILE cond step
[PROOF STEP]
apply (rule WHILE_bounded_aux2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_nb cond (Sup {bounded_WHILE n cond step m |n. True}) \<le> m \<bind> WHILE cond step
[PROOF STEP]
apply (simp add: filter_nb_cont)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup {filter_nb cond ma |ma. \<exists>n. ma = bounded_WHILE n cond step m} \<le> m \<bind> WHILE cond step
[PROOF STEP]
apply (rule Sup_least)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {filter_nb cond ma |ma. \<exists>n. ma = bounded_WHILE n cond step m} \<Longrightarrow> x \<le> m \<bind> WHILE cond step
[PROOF STEP]
apply (auto simp: WHILE_bounded_aux1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done