[STATEMENT]
theorem no_interleaving:
  assumes "insert_ops ops"
    and "insert_seq start xs" and "insert_ops xs"
    and "insert_seq start ys" and "insert_ops ys"
    and "set xs \<subseteq> set ops" and "set ys \<subseteq> set ops"
    and "distinct (map fst xs @ map fst ys)"
    and "start = None \<or> (\<exists>r. start = Some r \<and> r \<in> set (interp_ins ops))"
  shows "(\<forall>x \<in> set (map fst xs). \<forall>y \<in> set (map fst ys). list_order ops x y) \<or>
         (\<forall>x \<in> set (map fst xs). \<forall>y \<in> set (map fst ys). list_order ops y x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
proof(cases "fst (hd xs) < fst (hd ys)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
 2. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
fst (hd xs) < fst (hd ys)

goal (2 subgoals):
 1. fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
 2. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst (hd xs) < fst (hd ys)

goal (2 subgoals):
 1. fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
 2. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
have "\<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
using assms(9)
[PROOF STATE]
proof (prove)
using this:
start = None \<or> (\<exists>r. start = Some r \<and> r \<in> set (interp_ins ops))

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)

goal (2 subgoals):
 1. fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
 2. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)
[PROOF STEP]
have "\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x"
[PROOF STATE]
proof (prove)
using this:
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x
[PROOF STEP]
using assms no_interleaving_ordered
[PROOF STATE]
proof (prove)
using this:
fst (hd xs) < fst (hd ys)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)
insert_ops ops
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set ops
set ys \<subseteq> set ops
distinct (map fst xs @ map fst ys)
start = None \<or> (\<exists>r. start = Some r \<and> r \<in> set (interp_ins ops))
\<lbrakk>insert_ops ?ops; insert_seq ?start ?xs; insert_ops ?xs; insert_seq ?start ?ys; insert_ops ?ys; set ?xs \<subseteq> set ?ops; set ?ys \<subseteq> set ?ops; distinct (map fst ?xs @ map fst ?ys); fst (hd ?xs) < fst (hd ?ys); \<And>r. ?start = Some r \<Longrightarrow> r \<in> set (interp_ins ?ops)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst ?xs). \<forall>y\<in>set (map fst ?ys). list_order ?ops y x) \<and> (\<forall>r. ?start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst ?xs). list_order ?ops r x) \<and> (\<forall>y\<in>set (map fst ?ys). list_order ?ops r y))

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x

goal (2 subgoals):
 1. fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
 2. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)

goal (1 subgoal):
 1. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> fst (hd xs) < fst (hd ys)

goal (1 subgoal):
 1. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
hence "fst (hd ys) < fst (hd xs)"
[PROOF STATE]
proof (prove)
using this:
\<not> fst (hd xs) < fst (hd ys)

goal (1 subgoal):
 1. fst (hd ys) < fst (hd xs)
[PROOF STEP]
using assms(2) assms(4) assms(8) insert_seq_nonempty distinct_fst_append
[PROOF STATE]
proof (prove)
using this:
\<not> fst (hd xs) < fst (hd ys)
insert_seq start xs
insert_seq start ys
distinct (map fst xs @ map fst ys)
insert_seq ?start ?xs \<Longrightarrow> ?xs \<noteq> []
\<lbrakk>?x \<in> set (map fst ?xs); distinct (map fst (?xs @ ?ys))\<rbrakk> \<Longrightarrow> ?x \<notin> set (map fst ?ys)

goal (1 subgoal):
 1. fst (hd ys) < fst (hd xs)
[PROOF STEP]
by (metis (no_types, lifting) hd_in_set hd_map list.map_disc_iff map_append neqE)
[PROOF STATE]
proof (state)
this:
fst (hd ys) < fst (hd xs)

goal (1 subgoal):
 1. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst (hd ys) < fst (hd xs)

goal (1 subgoal):
 1. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
have "distinct (map fst ys @ map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst ys @ map fst xs)
[PROOF STEP]
using assms(8) distinct_append_swap
[PROOF STATE]
proof (prove)
using this:
distinct (map fst xs @ map fst ys)
distinct (?xs @ ?ys) \<Longrightarrow> distinct (?ys @ ?xs)

goal (1 subgoal):
 1. distinct (map fst ys @ map fst xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (map fst ys @ map fst xs)

goal (1 subgoal):
 1. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (map fst ys @ map fst xs)

goal (1 subgoal):
 1. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
have "\<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
using assms(9)
[PROOF STATE]
proof (prove)
using this:
start = None \<or> (\<exists>r. start = Some r \<and> r \<in> set (interp_ins ops))

goal (1 subgoal):
 1. \<And>r. start = Some r \<Longrightarrow> r \<in> set (interp_ins ops)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst (hd ys) < fst (hd xs)
distinct (map fst ys @ map fst xs)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)
[PROOF STEP]
have "\<forall>x\<in>set (map fst ys). \<forall>y\<in>set (map fst xs). list_order ops y x"
[PROOF STATE]
proof (prove)
using this:
fst (hd ys) < fst (hd xs)
distinct (map fst ys @ map fst xs)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst ys). \<forall>y\<in>set (map fst xs). list_order ops y x
[PROOF STEP]
using assms no_interleaving_ordered
[PROOF STATE]
proof (prove)
using this:
fst (hd ys) < fst (hd xs)
distinct (map fst ys @ map fst xs)
start = Some ?r \<Longrightarrow> ?r \<in> set (interp_ins ops)
insert_ops ops
insert_seq start xs
insert_ops xs
insert_seq start ys
insert_ops ys
set xs \<subseteq> set ops
set ys \<subseteq> set ops
distinct (map fst xs @ map fst ys)
start = None \<or> (\<exists>r. start = Some r \<and> r \<in> set (interp_ins ops))
\<lbrakk>insert_ops ?ops; insert_seq ?start ?xs; insert_ops ?xs; insert_seq ?start ?ys; insert_ops ?ys; set ?xs \<subseteq> set ?ops; set ?ys \<subseteq> set ?ops; distinct (map fst ?xs @ map fst ?ys); fst (hd ?xs) < fst (hd ?ys); \<And>r. ?start = Some r \<Longrightarrow> r \<in> set (interp_ins ?ops)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (map fst ?xs). \<forall>y\<in>set (map fst ?ys). list_order ?ops y x) \<and> (\<forall>r. ?start = Some r \<longrightarrow> (\<forall>x\<in>set (map fst ?xs). list_order ?ops r x) \<and> (\<forall>y\<in>set (map fst ?ys). list_order ?ops r y))

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst ys). \<forall>y\<in>set (map fst xs). list_order ops y x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (map fst ys). \<forall>y\<in>set (map fst xs). list_order ops y x

goal (1 subgoal):
 1. \<not> fst (hd xs) < fst (hd ys) \<Longrightarrow> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set (map fst ys). \<forall>y\<in>set (map fst xs). list_order ops y x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (map fst ys). \<forall>y\<in>set (map fst xs). list_order ops y x

goal (1 subgoal):
 1. (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops x y) \<or> (\<forall>x\<in>set (map fst xs). \<forall>y\<in>set (map fst ys). list_order ops y x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem missing_start_no_insertion:
  assumes "insert_ops ops"
    and "insert_seq (Some start) xs" and "insert_ops xs"
    and "insert_seq (Some start) ys" and "insert_ops ys"
    and "set xs \<subseteq> set ops" and "set ys \<subseteq> set ops"
    and "start \<notin> set (interp_ins ops)"
  shows "\<forall>x \<in> set (map fst xs) \<union> set (map fst ys). x \<notin> set (interp_ins ops)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs) \<union> set (map fst ys). x \<notin> set (interp_ins ops)
[PROOF STEP]
using assms insert_seq_no_start
[PROOF STATE]
proof (prove)
using this:
insert_ops ops
insert_seq (Some start) xs
insert_ops xs
insert_seq (Some start) ys
insert_ops ys
set xs \<subseteq> set ops
set ys \<subseteq> set ops
start \<notin> set (interp_ins ops)
\<lbrakk>insert_ops ?ops; insert_seq (Some ?ref) ?xs; insert_ops ?xs; set ?xs \<subseteq> set ?ops; ?ref \<notin> set (interp_ins ?ops)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map fst ?xs). i \<notin> set (interp_ins ?ops)

goal (1 subgoal):
 1. \<forall>x\<in>set (map fst xs) \<union> set (map fst ys). x \<notin> set (interp_ins ops)
[PROOF STEP]
by (metis UnE)


[STATEMENT]
lemma (in subsemicategory) subsemicategory_axioms'[smc_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<BB>' = \<BB>"
  shows "\<BB>' \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>'\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB>' \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>'\<^esub> \<CC>
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule subsemicategory_axioms)


[STATEMENT]
lemma (in subsemicategory) subsemicategory_axioms''[smc_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<CC>' = \<CC>"
  shows "\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>'\<^esub> \<CC>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>'\<^esub> \<CC>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule subsemicategory_axioms)


[STATEMENT]
lemma subsemicategoryI':
  assumes "semicategory \<alpha> \<BB>"
    and "semicategory \<alpha> \<CC>"
    and "\<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
    and "\<And>a b f. f : a \<mapsto>\<^bsub>\<BB>\<^esub> b \<Longrightarrow> f : a \<mapsto>\<^bsub>\<CC>\<^esub> b"
    and "\<And>b c g a f. \<lbrakk> g : b \<mapsto>\<^bsub>\<BB>\<^esub> c; f : a \<mapsto>\<^bsub>\<BB>\<^esub> b \<rbrakk> \<Longrightarrow>
      g \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f"
  shows "\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<BB>: semicategory \<alpha> \<BB>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semicategory \<alpha> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<CC>: semicategory \<alpha> \<CC>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semicategory \<alpha> \<CC>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by
      (
        intro subsemicategoryI subdigraphI,
        unfold slicing_simps;
        (intro \<BB>.smc_digraph \<CC>.smc_digraph assms)?
      )
[PROOF STATE]
proof (state)
this:
\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in subsemicategory) subsmc_subsemicategory_op_smc:
  "op_smc \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_smc \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<CC>
[PROOF STEP]
proof(rule subsemicategoryI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. semicategory \<alpha> (op_smc \<BB>)
 2. semicategory \<alpha> (op_smc \<CC>)
 3. smc_dg (op_smc \<BB>) \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<CC>)
 4. \<And>b c g a f. \<lbrakk>g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c; f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b\<rbrakk> \<Longrightarrow> g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f
[PROOF STEP]
fix g b c f a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. semicategory \<alpha> (op_smc \<BB>)
 2. semicategory \<alpha> (op_smc \<CC>)
 3. smc_dg (op_smc \<BB>) \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<CC>)
 4. \<And>b c g a f. \<lbrakk>g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c; f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b\<rbrakk> \<Longrightarrow> g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f
[PROOF STEP]
assume prems: "g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c" "f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b"
[PROOF STATE]
proof (state)
this:
g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c
f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b

goal (4 subgoals):
 1. semicategory \<alpha> (op_smc \<BB>)
 2. semicategory \<alpha> (op_smc \<CC>)
 3. smc_dg (op_smc \<BB>) \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<CC>)
 4. \<And>b c g a f. \<lbrakk>g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c; f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b\<rbrakk> \<Longrightarrow> g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c
f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b
[PROOF STEP]
have "g : c \<mapsto>\<^bsub>\<BB>\<^esub> b" and "f : b \<mapsto>\<^bsub>\<BB>\<^esub> a"
[PROOF STATE]
proof (prove)
using this:
g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c
f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b

goal (1 subgoal):
 1. g : c \<mapsto>\<^bsub>\<BB>\<^esub> b &&& f : b \<mapsto>\<^bsub>\<BB>\<^esub> a
[PROOF STEP]
by (simp_all add: smc_op_simps)
[PROOF STATE]
proof (state)
this:
g : c \<mapsto>\<^bsub>\<BB>\<^esub> b
f : b \<mapsto>\<^bsub>\<BB>\<^esub> a

goal (4 subgoals):
 1. semicategory \<alpha> (op_smc \<BB>)
 2. semicategory \<alpha> (op_smc \<CC>)
 3. smc_dg (op_smc \<BB>) \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<CC>)
 4. \<And>b c g a f. \<lbrakk>g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c; f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b\<rbrakk> \<Longrightarrow> g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f
[PROOF STEP]
with subsemicategory_axioms
[PROOF STATE]
proof (chain)
picking this:
\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
g : c \<mapsto>\<^bsub>\<BB>\<^esub> b
f : b \<mapsto>\<^bsub>\<BB>\<^esub> a
[PROOF STEP]
have g: "g : c \<mapsto>\<^bsub>\<CC>\<^esub> b" and f: "f : b \<mapsto>\<^bsub>\<CC>\<^esub> a"
[PROOF STATE]
proof (prove)
using this:
\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
g : c \<mapsto>\<^bsub>\<BB>\<^esub> b
f : b \<mapsto>\<^bsub>\<BB>\<^esub> a

goal (1 subgoal):
 1. g : c \<mapsto>\<^bsub>\<CC>\<^esub> b &&& f : b \<mapsto>\<^bsub>\<CC>\<^esub> a
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: smc_sub_fw_cs_intros)+
[PROOF STATE]
proof (state)
this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> b
f : b \<mapsto>\<^bsub>\<CC>\<^esub> a

goal (4 subgoals):
 1. semicategory \<alpha> (op_smc \<BB>)
 2. semicategory \<alpha> (op_smc \<CC>)
 3. smc_dg (op_smc \<BB>) \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<CC>)
 4. \<And>b c g a f. \<lbrakk>g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c; f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b\<rbrakk> \<Longrightarrow> g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f
[PROOF STEP]
from dg.op_smc_Comp[OF this(2,1)]
[PROOF STATE]
proof (chain)
picking this:
g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f = f \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> g
[PROOF STEP]
have "g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f = f \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> g"
[PROOF STATE]
proof (prove)
using this:
g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f = f \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> g

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f = f \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> g
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f = f \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> g

goal (4 subgoals):
 1. semicategory \<alpha> (op_smc \<BB>)
 2. semicategory \<alpha> (op_smc \<CC>)
 3. smc_dg (op_smc \<BB>) \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<CC>)
 4. \<And>b c g a f. \<lbrakk>g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c; f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b\<rbrakk> \<Longrightarrow> g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c
f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b
g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f = f \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> g
[PROOF STEP]
show "g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f"
[PROOF STATE]
proof (prove)
using this:
g : b \<mapsto>\<^bsub>op_smc \<BB>\<^esub> c
f : a \<mapsto>\<^bsub>op_smc \<BB>\<^esub> b
g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f = f \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> g

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f
[PROOF STEP]
by (simp add: smc_op_simps subsmc_Comp)
[PROOF STATE]
proof (state)
this:
g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>op_smc \<CC>\<^esub> f

goal (3 subgoals):
 1. semicategory \<alpha> (op_smc \<BB>)
 2. semicategory \<alpha> (op_smc \<CC>)
 3. smc_dg (op_smc \<BB>) \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<CC>)
[PROOF STEP]
qed
  (
    auto
      simp:
        smc_op_simps slicing_commute[symmetric] subsmc_subdigraph_op_dg_op_dg
      intro: smc_op_intros
  )


[STATEMENT]
lemma (in subsemicategory) subsmc_Comp_simp:
  assumes "g : b \<mapsto>\<^bsub>\<BB>\<^esub> c" and "f : a \<mapsto>\<^bsub>\<BB>\<^esub> b"
  shows "g \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f
[PROOF STEP]
using assms subsmc_Comp
[PROOF STATE]
proof (prove)
using this:
g : b \<mapsto>\<^bsub>\<BB>\<^esub> c
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b
\<lbrakk>?g : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?c; ?f : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b\<rbrakk> \<Longrightarrow> ?g \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> ?f = ?g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> ?f

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> f = g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f
[PROOF STEP]
by auto


[STATEMENT]
lemma (in subsemicategory) subsmc_is_idem_arrD:
  assumes "f : \<mapsto>\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<BB>\<^esub> b"
  shows "f : \<mapsto>\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<CC>\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f : \<mapsto>\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<CC>\<^esub> b
[PROOF STEP]
using assms subsemicategory_axioms
[PROOF STATE]
proof (prove)
using this:
f : \<mapsto>\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<BB>\<^esub> b
\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. f : \<mapsto>\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<CC>\<^esub> b
[PROOF STEP]
by (intro is_idem_arrI; elim is_idem_arrE)
    (
      cs_concl cs_shallow
        cs_simp: smc_sub_bw_cs_simps[symmetric] cs_intro: smc_sub_fw_cs_intros
    )


[STATEMENT]
lemma subsmc_refl:
  assumes "semicategory \<alpha> \<AA>"
  shows "\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret semicategory \<alpha> \<AA>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semicategory \<alpha> \<AA>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (auto intro: smc_cs_intros slicing_intros subdg_refl subsemicategoryI)
[PROOF STATE]
proof (state)
this:
\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subsmc_trans[trans]:
  assumes "\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>" and "\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<AA>\<BB>: subsemicategory \<alpha> \<AA> \<BB>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<BB>\<CC>: subsemicategory \<alpha> \<BB> \<CC>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof(rule subsemicategoryI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. semicategory \<alpha> \<AA>
 2. semicategory \<alpha> \<CC>
 3. smc_dg \<AA> \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>
 4. \<And>b c g a f. \<lbrakk>g : b \<mapsto>\<^bsub>\<AA>\<^esub> c; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b\<rbrakk> \<Longrightarrow> g \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> f = g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f
[PROOF STEP]
from \<AA>\<BB>.subsmc_subdigraph \<BB>\<CC>.subsmc_subdigraph
[PROOF STATE]
proof (chain)
picking this:
smc_dg \<AA> \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<BB>
smc_dg \<BB> \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>
[PROOF STEP]
show "smc_dg \<AA> \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>"
[PROOF STATE]
proof (prove)
using this:
smc_dg \<AA> \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<BB>
smc_dg \<BB> \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>

goal (1 subgoal):
 1. smc_dg \<AA> \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>
[PROOF STEP]
by (meson subdg_trans)
[PROOF STATE]
proof (state)
this:
smc_dg \<AA> \<subseteq>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>

goal (3 subgoals):
 1. semicategory \<alpha> \<AA>
 2. semicategory \<alpha> \<CC>
 3. \<And>b c g a f. \<lbrakk>g : b \<mapsto>\<^bsub>\<AA>\<^esub> c; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b\<rbrakk> \<Longrightarrow> g \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> f = g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f
[PROOF STEP]
show "g \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> f = g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f"
      if "g : b \<mapsto>\<^bsub>\<AA>\<^esub> c" and "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b" for g b c f a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> f = g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f
[PROOF STEP]
by
        (
          metis
            that
            \<AA>\<BB>.subsmc_is_arr_vsubset
            \<AA>\<BB>.subsmc_Comp_simp
            \<BB>\<CC>.subsmc_Comp_simp
        )
[PROOF STATE]
proof (state)
this:
\<lbrakk>?g : ?b \<mapsto>\<^bsub>\<AA>\<^esub> ?c; ?f : ?a \<mapsto>\<^bsub>\<AA>\<^esub> ?b\<rbrakk> \<Longrightarrow> ?g \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> ?f = ?g \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> ?f

goal (2 subgoals):
 1. semicategory \<alpha> \<AA>
 2. semicategory \<alpha> \<CC>
[PROOF STEP]
qed (auto intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subsmc_antisym:
  assumes "\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>" and "\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "\<AA> = \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> = \<BB>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> = \<BB>
[PROOF STEP]
interpret \<AA>\<BB>: subsemicategory \<alpha> \<AA> \<BB>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> = \<BB>
[PROOF STEP]
interpret \<BB>\<AA>: subsemicategory \<alpha> \<BB> \<AA>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> = \<BB>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> = \<BB>
[PROOF STEP]
proof(rule smc_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. semicategory ?\<alpha> \<AA>
 2. semicategory ?\<alpha> \<BB>
 3. \<AA>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
 4. \<AA>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
 5. \<AA>\<lparr>Dom\<rparr> = \<BB>\<lparr>Dom\<rparr>
 6. \<AA>\<lparr>Cod\<rparr> = \<BB>\<lparr>Cod\<rparr>
 7. \<AA>\<lparr>Comp\<rparr> = \<BB>\<lparr>Comp\<rparr>
[PROOF STEP]
from subdg_antisym[OF \<AA>\<BB>.subsmc_subdigraph \<BB>\<AA>.subsmc_subdigraph]
[PROOF STATE]
proof (chain)
picking this:
smc_dg \<AA> = smc_dg \<BB>
[PROOF STEP]
have
      "smc_dg \<AA>\<lparr>Obj\<rparr> = smc_dg \<BB>\<lparr>Obj\<rparr>" "smc_dg \<AA>\<lparr>Arr\<rparr> = smc_dg \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
smc_dg \<AA> = smc_dg \<BB>

goal (1 subgoal):
 1. smc_dg \<AA>\<lparr>Obj\<rparr> = smc_dg \<BB>\<lparr>Obj\<rparr> &&& smc_dg \<AA>\<lparr>Arr\<rparr> = smc_dg \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
smc_dg \<AA>\<lparr>Obj\<rparr> = smc_dg \<BB>\<lparr>Obj\<rparr>
smc_dg \<AA>\<lparr>Arr\<rparr> = smc_dg \<BB>\<lparr>Arr\<rparr>

goal (7 subgoals):
 1. semicategory ?\<alpha> \<AA>
 2. semicategory ?\<alpha> \<BB>
 3. \<AA>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
 4. \<AA>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
 5. \<AA>\<lparr>Dom\<rparr> = \<BB>\<lparr>Dom\<rparr>
 6. \<AA>\<lparr>Cod\<rparr> = \<BB>\<lparr>Cod\<rparr>
 7. \<AA>\<lparr>Comp\<rparr> = \<BB>\<lparr>Comp\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
smc_dg \<AA>\<lparr>Obj\<rparr> = smc_dg \<BB>\<lparr>Obj\<rparr>
smc_dg \<AA>\<lparr>Arr\<rparr> = smc_dg \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "\<AA>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>" and Arr: "\<AA>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
smc_dg \<AA>\<lparr>Obj\<rparr> = smc_dg \<BB>\<lparr>Obj\<rparr>
smc_dg \<AA>\<lparr>Arr\<rparr> = smc_dg \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<AA>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr> &&& \<AA>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding slicing_simps
[PROOF STATE]
proof (prove)
using this:
\<AA>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
\<AA>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<AA>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr> &&& \<AA>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<AA>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
\<AA>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>

goal (5 subgoals):
 1. semicategory ?\<alpha> \<AA>
 2. semicategory ?\<alpha> \<BB>
 3. \<AA>\<lparr>Dom\<rparr> = \<BB>\<lparr>Dom\<rparr>
 4. \<AA>\<lparr>Cod\<rparr> = \<BB>\<lparr>Cod\<rparr>
 5. \<AA>\<lparr>Comp\<rparr> = \<BB>\<lparr>Comp\<rparr>
[PROOF STEP]
show "\<AA>\<lparr>Dom\<rparr> = \<BB>\<lparr>Dom\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA>\<lparr>Dom\<rparr> = \<BB>\<lparr>Dom\<rparr>
[PROOF STEP]
by (rule vsv_eqI) (auto simp: smc_cs_simps \<AA>\<BB>.subsmc_dom_simp Arr)
[PROOF STATE]
proof (state)
this:
\<AA>\<lparr>Dom\<rparr> = \<BB>\<lparr>Dom\<rparr>

goal (4 subgoals):
 1. semicategory ?\<alpha> \<AA>
 2. semicategory ?\<alpha> \<BB>
 3. \<AA>\<lparr>Cod\<rparr> = \<BB>\<lparr>Cod\<rparr>
 4. \<AA>\<lparr>Comp\<rparr> = \<BB>\<lparr>Comp\<rparr>
[PROOF STEP]
show "\<AA>\<lparr>Cod\<rparr> = \<BB>\<lparr>Cod\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA>\<lparr>Cod\<rparr> = \<BB>\<lparr>Cod\<rparr>
[PROOF STEP]
by (rule vsv_eqI) (auto simp: smc_cs_simps \<BB>\<AA>.subsmc_cod_simp Arr)
[PROOF STATE]
proof (state)
this:
\<AA>\<lparr>Cod\<rparr> = \<BB>\<lparr>Cod\<rparr>

goal (3 subgoals):
 1. semicategory ?\<alpha> \<AA>
 2. semicategory ?\<alpha> \<BB>
 3. \<AA>\<lparr>Comp\<rparr> = \<BB>\<lparr>Comp\<rparr>
[PROOF STEP]
show "\<AA>\<lparr>Comp\<rparr> = \<BB>\<lparr>Comp\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA>\<lparr>Comp\<rparr> = \<BB>\<lparr>Comp\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<AA>\<lparr>Comp\<rparr>)
 2. vsv (\<BB>\<lparr>Comp\<rparr>)
 3. \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) = \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) \<Longrightarrow> \<AA>\<lparr>Comp\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>Comp\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) = \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) = \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)
[PROOF STEP]
proof(intro vsubset_antisym vsubsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
fix gf
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
assume "gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)"
[PROOF STATE]
proof (state)
this:
gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
obtain g f b c a
          where gf_def: "gf = [g, f]\<^sub>\<circ>"
            and g: "g : b \<mapsto>\<^bsub>\<AA>\<^esub> c"
            and f: "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
[PROOF STATE]
proof (prove)
using this:
gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)

goal (1 subgoal):
 1. (\<And>g f b c a. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g : b \<mapsto>\<^bsub>\<AA>\<^esub> c; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: \<AA>\<BB>.sdg.smc_Comp_vdomain)
[PROOF STATE]
proof (state)
this:
gf = [g, f]\<^sub>\<circ>
g : b \<mapsto>\<^bsub>\<AA>\<^esub> c
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
from g f
[PROOF STATE]
proof (chain)
picking this:
g : b \<mapsto>\<^bsub>\<AA>\<^esub> c
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
show "gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
g : b \<mapsto>\<^bsub>\<AA>\<^esub> c
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)
[PROOF STEP]
unfolding gf_def
[PROOF STATE]
proof (prove)
using this:
g : b \<mapsto>\<^bsub>\<AA>\<^esub> c
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)
[PROOF STEP]
by (meson \<AA>\<BB>.dg.smc_Comp_vdomainI \<AA>\<BB>.subsmc_is_arrD)
[PROOF STATE]
proof (state)
this:
gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
fix gf
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
assume "gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)"
[PROOF STATE]
proof (state)
this:
gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)
[PROOF STEP]
obtain g f b c a
          where gf_def: "gf = [g, f]\<^sub>\<circ>"
            and g: "g : b \<mapsto>\<^bsub>\<BB>\<^esub> c"
            and f: "f : a \<mapsto>\<^bsub>\<BB>\<^esub> b"
[PROOF STATE]
proof (prove)
using this:
gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)

goal (1 subgoal):
 1. (\<And>g f b c a. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g : b \<mapsto>\<^bsub>\<BB>\<^esub> c; f : a \<mapsto>\<^bsub>\<BB>\<^esub> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: \<AA>\<BB>.dg.smc_Comp_vdomain)
[PROOF STATE]
proof (state)
this:
gf = [g, f]\<^sub>\<circ>
g : b \<mapsto>\<^bsub>\<BB>\<^esub> c
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
from g f
[PROOF STATE]
proof (chain)
picking this:
g : b \<mapsto>\<^bsub>\<BB>\<^esub> c
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b
[PROOF STEP]
show "gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
g : b \<mapsto>\<^bsub>\<BB>\<^esub> c
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b

goal (1 subgoal):
 1. gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
unfolding gf_def
[PROOF STATE]
proof (prove)
using this:
g : b \<mapsto>\<^bsub>\<BB>\<^esub> c
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)
[PROOF STEP]
by (meson \<AA>\<BB>.sdg.smc_Comp_vdomainI \<BB>\<AA>.subsmc_is_arrD)
[PROOF STATE]
proof (state)
this:
gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) = \<D>\<^sub>\<circ> (\<BB>\<lparr>Comp\<rparr>)

goal (3 subgoals):
 1. vsv (\<AA>\<lparr>Comp\<rparr>)
 2. vsv (\<BB>\<lparr>Comp\<rparr>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) \<Longrightarrow> \<AA>\<lparr>Comp\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>Comp\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) \<Longrightarrow> \<AA>\<lparr>Comp\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>Comp\<rparr>\<lparr>a\<rparr>" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) \<Longrightarrow> \<AA>\<lparr>Comp\<rparr>\<lparr>a\<rparr> = \<BB>\<lparr>Comp\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (metis \<AA>\<BB>.sdg.smc_Comp_vdomain \<AA>\<BB>.subsmc_Comp_simp)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<AA>\<lparr>Comp\<rparr>) \<Longrightarrow> \<AA>\<lparr>Comp\<rparr>\<lparr>?a\<rparr> = \<BB>\<lparr>Comp\<rparr>\<lparr>?a\<rparr>

goal (2 subgoals):
 1. vsv (\<AA>\<lparr>Comp\<rparr>)
 2. vsv (\<BB>\<lparr>Comp\<rparr>)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<AA>\<lparr>Comp\<rparr> = \<BB>\<lparr>Comp\<rparr>

goal (2 subgoals):
 1. semicategory ?\<alpha> \<AA>
 2. semicategory ?\<alpha> \<BB>
[PROOF STEP]
qed (auto intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<AA> = \<BB>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_smcf_inc[slicing_commute]:
  "dghm_inc (smc_dg \<BB>) (smc_dg \<CC>) = smcf_dghm (smcf_inc \<BB> \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_inc (smc_dg \<BB>) (smc_dg \<CC>) = smcf_dghm (dghm_inc \<BB> \<CC>)
[PROOF STEP]
unfolding
    smcf_dghm_def dghm_inc_def smc_dg_def dg_field_simps dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [vid_on ([\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>, \<BB>\<lparr>1\<^sub>\<nat>\<rparr>, \<BB>\<lparr>2\<^sub>\<nat>\<rparr>, \<BB>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on ([\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>, \<BB>\<lparr>1\<^sub>\<nat>\<rparr>, \<BB>\<lparr>2\<^sub>\<nat>\<rparr>, \<BB>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>), [\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>, \<BB>\<lparr>1\<^sub>\<nat>\<rparr>, \<BB>\<lparr>2\<^sub>\<nat>\<rparr>, \<BB>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>, \<CC>\<lparr>1\<^sub>\<nat>\<rparr>, \<CC>\<lparr>2\<^sub>\<nat>\<rparr>, \<CC>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ> = [[vid_on (\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<BB>\<lparr>1\<^sub>\<nat>\<rparr>), \<BB>, \<CC>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [vid_on (\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<BB>\<lparr>1\<^sub>\<nat>\<rparr>), \<BB>, \<CC>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, [[vid_on (\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<BB>\<lparr>1\<^sub>\<nat>\<rparr>), \<BB>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [vid_on (\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<BB>\<lparr>1\<^sub>\<nat>\<rparr>), \<BB>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [vid_on (\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<BB>\<lparr>1\<^sub>\<nat>\<rparr>), \<BB>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [vid_on (\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<BB>\<lparr>1\<^sub>\<nat>\<rparr>), \<BB>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[vid_on (\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<BB>\<lparr>1\<^sub>\<nat>\<rparr>), \<BB>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [vid_on (\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<BB>\<lparr>1\<^sub>\<nat>\<rparr>), \<BB>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [vid_on (\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<BB>\<lparr>1\<^sub>\<nat>\<rparr>), \<BB>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [vid_on (\<BB>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<BB>\<lparr>1\<^sub>\<nat>\<rparr>), \<BB>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma (in subsemicategory)
  subsemicategory_smcf_inc_op_smc_is_semifunctor[smc_sub_cs_intros]:
  "smcf_inc (op_smc \<BB>) (op_smc \<CC>) : op_smc \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> op_smc \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_inc (op_smc \<BB>) (op_smc \<CC>) : op_smc \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> op_smc \<CC>
[PROOF STEP]
by
    (
      intro
        subsemicategory.subsmc_smcf_inc_is_ft_semifunctor
        subsmc_subsemicategory_op_smc
    )


[STATEMENT]
lemma (in subsemicategory) subdg_op_smc_smcf_inc[smc_op_simps]:
  "op_smcf (smcf_inc \<BB> \<CC>) = smcf_inc (op_smc \<BB>) (op_smc \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_smcf (dghm_inc \<BB> \<CC>) = dghm_inc (op_smc \<BB>) (op_smc \<CC>)
[PROOF STEP]
by
    (
      rule smcf_eqI[of \<alpha> \<open>op_smc \<BB>\<close> \<open>op_smc \<CC>\<close>],
      unfold smc_op_simps dghm_inc_components
    )
    (
      auto simp:
        is_ft_semifunctorD
        subsemicategory_smcf_inc_op_smc_is_semifunctor
        inc.is_semifunctor_op
    )


[STATEMENT]
lemma (in fl_subsemicategory) fl_subsemicategory_axioms'[smc_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<BB>' = \<BB>"
  shows "\<BB>' \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>'\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB>' \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>'\<^esub> \<CC>
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule fl_subsemicategory_axioms)


[STATEMENT]
lemma (in fl_subsemicategory) fl_subsemicategory_axioms''[smc_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<CC>' = \<CC>"
  shows "\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>'\<^esub> \<CC>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>'\<^esub> \<CC>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule fl_subsemicategory_axioms)


[STATEMENT]
lemma (in wide_subsemicategory) wide_subsemicategory_axioms'[smc_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<BB>' = \<BB>"
  shows "\<BB>' \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>'\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB>' \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>'\<^esub> \<CC>
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule wide_subsemicategory_axioms)


[STATEMENT]
lemma (in wide_subsemicategory) wide_subsemicategory_axioms''[smc_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<CC>' = \<CC>"
  shows "\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>'\<^esub> \<CC>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>'\<^esub> \<CC>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule wide_subsemicategory_axioms)


[STATEMENT]
lemma wide_subsmc_refl:
  assumes "semicategory \<alpha> \<AA>"
  shows "\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret semicategory \<alpha> \<AA>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semicategory \<alpha> \<AA>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by
      (
        auto intro:
          assms
          slicing_intros
          wide_subdg_refl
          wide_subsemicategoryI
          subsmc_refl
      )
[PROOF STATE]
proof (state)
this:
\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wide_subsmc_trans[trans]:
  assumes "\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<BB>" and "\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<AA>\<BB>: wide_subsemicategory \<alpha> \<AA> \<BB>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<BB>\<CC>: wide_subsemicategory \<alpha> \<BB> \<CC>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by
      (
        intro
          wide_subsemicategoryI
          subsmc_trans[
            OF \<AA>\<BB>.subsemicategory_axioms \<BB>\<CC>.subsemicategory_axioms
            ],
        rule wide_subdg_trans,
        rule \<AA>\<BB>.wide_subsmc_wide_subdigraph,
        rule \<BB>\<CC>.wide_subsmc_wide_subdigraph
     )
[PROOF STATE]
proof (state)
this:
\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wide_subsmc_antisym:
  assumes "\<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<BB>" and "\<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "\<AA> = \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> = \<BB>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> = \<BB>
[PROOF STEP]
interpret \<AA>\<BB>: wide_subsemicategory \<alpha> \<AA> \<BB>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> = \<BB>
[PROOF STEP]
interpret \<BB>\<AA>: wide_subsemicategory \<alpha> \<BB> \<AA>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<subseteq>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>w\<^sub>i\<^sub>d\<^sub>e\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> = \<BB>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> = \<BB>
[PROOF STEP]
by
      (
        rule subsmc_antisym[
          OF \<AA>\<BB>.subsemicategory_axioms \<BB>\<AA>.subsemicategory_axioms
          ]
      )
[PROOF STATE]
proof (state)
this:
\<AA> = \<BB>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_Label: "finite Label"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite Label
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite Label
[PROOF STEP]
have "Label \<subseteq> {xs. set xs \<subseteq> (UNIV::Proc set) \<and> length xs \<le> Suc f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Label \<subseteq> {xs. set xs \<subseteq> UNIV \<and> length xs \<le> Suc f}
[PROOF STEP]
by (auto simp: Label_def)
[PROOF STATE]
proof (state)
this:
Label \<subseteq> {xs. set xs \<subseteq> UNIV \<and> length xs \<le> Suc f}

goal (1 subgoal):
 1. finite Label
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Label \<subseteq> {xs. set xs \<subseteq> UNIV \<and> length xs \<le> Suc f}

goal (1 subgoal):
 1. finite Label
[PROOF STEP]
have "finite {xs. set xs \<subseteq> (UNIV::Proc set) \<and> length xs \<le> Suc f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {xs. set xs \<subseteq> UNIV \<and> length xs \<le> Suc f}
[PROOF STEP]
by (rule finite_lists_length_le) auto
[PROOF STATE]
proof (state)
this:
finite {xs. set xs \<subseteq> UNIV \<and> length xs \<le> Suc f}

goal (1 subgoal):
 1. finite Label
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Label \<subseteq> {xs. set xs \<subseteq> UNIV \<and> length xs \<le> Suc f}
finite {xs. set xs \<subseteq> UNIV \<and> length xs \<le> Suc f}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Label \<subseteq> {xs. set xs \<subseteq> UNIV \<and> length xs \<le> Suc f}
finite {xs. set xs \<subseteq> UNIV \<and> length xs \<le> Suc f}

goal (1 subgoal):
 1. finite Label
[PROOF STEP]
by (auto elim: finite_subset)
[PROOF STATE]
proof (state)
this:
finite Label

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_UNIV_Label: "finite (UNIV::Label set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite UNIV
[PROOF STEP]
from finite_Label
[PROOF STATE]
proof (chain)
picking this:
finite Label
[PROOF STEP]
have "finite (Abs_Label ` Label)"
[PROOF STATE]
proof (prove)
using this:
finite Label

goal (1 subgoal):
 1. finite (Abs_Label ` Label)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (Abs_Label ` Label)

goal (1 subgoal):
 1. finite UNIV
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (Abs_Label ` Label)

goal (1 subgoal):
 1. finite UNIV
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
finite (Abs_Label ` Label)

goal (1 subgoal):
 1. finite UNIV
[PROOF STEP]
fix l::Label
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite UNIV
[PROOF STEP]
have "l \<in> Abs_Label ` Label"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<in> Abs_Label ` Label
[PROOF STEP]
by (rule Abs_Label_cases) auto
[PROOF STATE]
proof (state)
this:
l \<in> Abs_Label ` Label

goal (1 subgoal):
 1. finite UNIV
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?l2 \<in> Abs_Label ` Label

goal (1 subgoal):
 1. finite UNIV
[PROOF STEP]
hence "(UNIV::Label set) = (Abs_Label ` Label)"
[PROOF STATE]
proof (prove)
using this:
?l2 \<in> Abs_Label ` Label

goal (1 subgoal):
 1. UNIV = Abs_Label ` Label
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
UNIV = Abs_Label ` Label

goal (1 subgoal):
 1. finite UNIV
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (Abs_Label ` Label)
UNIV = Abs_Label ` Label
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (Abs_Label ` Label)
UNIV = Abs_Label ` Label

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_Label_set [iff]: "finite (S :: Label set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S
[PROOF STEP]
using finite_UNIV_Label
[PROOF STATE]
proof (prove)
using this:
finite UNIV

goal (1 subgoal):
 1. finite S
[PROOF STEP]
by (auto intro: finite_subset)


[STATEMENT]
lemma length_lbl [intro]: "length_lbl l \<le> Suc f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length_lbl l \<le> Suc f
[PROOF STEP]
unfolding length_lbl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (Rep_Label l) \<le> Suc f
[PROOF STEP]
using Label_def Rep_Label
[PROOF STATE]
proof (prove)
using this:
Label = {xs. length xs \<le> Suc f \<and> distinct xs}
Rep_Label ?x \<in> Label

goal (1 subgoal):
 1. length (Rep_Label l) \<le> Suc f
[PROOF STEP]
by auto


[STATEMENT]
lemma cer:
assumes  "r \<in> {e,m,b,ov,s,f,d,m^-1,b^-1,ov^-1,s^-1,f^-1,d^-1}"
shows "e O r = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
assume a:"(x,y) \<in> e O r"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> e O r

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> e O r
[PROOF STEP]
obtain z where "(x,z) \<in> e" and "(z,y) \<in> r"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> e O r

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>(x, z) \<in> e; (z, y) \<in> r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, z) \<in> e
(z, y) \<in> r

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
from \<open>(x,z) \<in> e\<close>
[PROOF STATE]
proof (chain)
picking this:
(x, z) \<in> e
[PROOF STEP]
have "x = z"
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> e

goal (1 subgoal):
 1. x = z
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> e
((?p, ?q) \<in> e) = (?p = ?q)

goal (1 subgoal):
 1. x = z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = z

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
with \<open>(z,y)\<in> r\<close>
[PROOF STATE]
proof (chain)
picking this:
(z, y) \<in> r
x = z
[PROOF STEP]
have "(x,y) \<in> r"
[PROOF STATE]
proof (prove)
using this:
(z, y) \<in> r
x = z

goal (1 subgoal):
 1. (x, y) \<in> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> e O r \<Longrightarrow> (?x2, ?y2) \<in> r

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
note c1 = this
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> e O r \<Longrightarrow> (?x2, ?y2) \<in> r

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> e O r \<Longrightarrow> (?x2, ?y2) \<in> r

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
assume a:"(x,y) \<in>  r"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
have "(x,x) \<in> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, x) \<in> e
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
((?p, ?q) \<in> e) = (?p = ?q)

goal (1 subgoal):
 1. (x, x) \<in> e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x) \<in> e

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> r
(x, x) \<in> e
[PROOF STEP]
have "(x,y) \<in> e O r"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> r
(x, x) \<in> e

goal (1 subgoal):
 1. (x, y) \<in> e O r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x, y) \<in> e O r

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> r \<Longrightarrow> (?x2, ?y2) \<in> e O r

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
note c2 = this
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> r \<Longrightarrow> (?x2, ?y2) \<in> e O r

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
from c1 c2
[PROOF STATE]
proof (chain)
picking this:
(?x2, ?y2) \<in> e O r \<Longrightarrow> (?x2, ?y2) \<in> r
(?x2, ?y2) \<in> r \<Longrightarrow> (?x2, ?y2) \<in> e O r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(?x2, ?y2) \<in> e O r \<Longrightarrow> (?x2, ?y2) \<in> r
(?x2, ?y2) \<in> r \<Longrightarrow> (?x2, ?y2) \<in> e O r

goal (1 subgoal):
 1. e O r = r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e O r = r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cre:
assumes  "r \<in> {e,m,b,ov,s,f,d,m^-1,b^-1,ov^-1,s^-1,f^-1,d^-1}"
shows " r O e = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
assume a:"(x,y) \<in> r O e"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r O e

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> r O e
[PROOF STEP]
obtain z where "(x,z) \<in> r" and "(z,y) \<in> e"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> r O e

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>(x, z) \<in> r; (z, y) \<in> e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, z) \<in> r
(z, y) \<in> e

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
from \<open>(z,y) \<in> e\<close>
[PROOF STATE]
proof (chain)
picking this:
(z, y) \<in> e
[PROOF STEP]
have "z = y"
[PROOF STATE]
proof (prove)
using this:
(z, y) \<in> e

goal (1 subgoal):
 1. z = y
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
(z, y) \<in> e
((?p, ?q) \<in> e) = (?p = ?q)

goal (1 subgoal):
 1. z = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z = y

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
with \<open>(x,z)\<in> r\<close>
[PROOF STATE]
proof (chain)
picking this:
(x, z) \<in> r
z = y
[PROOF STEP]
have "(x,y) \<in> r"
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> r
z = y

goal (1 subgoal):
 1. (x, y) \<in> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> r O e \<Longrightarrow> (?x2, ?y2) \<in> r

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
note c1 = this
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> r O e \<Longrightarrow> (?x2, ?y2) \<in> r

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> r O e \<Longrightarrow> (?x2, ?y2) \<in> r

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
assume a:"(x,y) \<in>  r"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
have "(y,y) \<in> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y, y) \<in> e
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
((?p, ?q) \<in> e) = (?p = ?q)

goal (1 subgoal):
 1. (y, y) \<in> e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y, y) \<in> e

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> r
(y, y) \<in> e
[PROOF STEP]
have "(x,y) \<in> r O e"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> r
(y, y) \<in> e

goal (1 subgoal):
 1. (x, y) \<in> r O e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r O e

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> r \<Longrightarrow> (?x2, ?y2) \<in> r O e

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
note c2 = this
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> r \<Longrightarrow> (?x2, ?y2) \<in> r O e

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
from c1 c2
[PROOF STATE]
proof (chain)
picking this:
(?x2, ?y2) \<in> r O e \<Longrightarrow> (?x2, ?y2) \<in> r
(?x2, ?y2) \<in> r \<Longrightarrow> (?x2, ?y2) \<in> r O e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(?x2, ?y2) \<in> r O e \<Longrightarrow> (?x2, ?y2) \<in> r
(?x2, ?y2) \<in> r \<Longrightarrow> (?x2, ?y2) \<in> r O e

goal (1 subgoal):
 1. r O e = r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r O e = r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in arelations) cbb:"b O b \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b O b \<subseteq> b
[PROOF STEP]
by (r_compose r1:b r2:b r3:b)


[STATEMENT]
lemma  (in arelations)  cbm:"b O m \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b O m \<subseteq> b
[PROOF STEP]
by (r_compose r1:b r2:m r3:b)


[STATEMENT]
lemma cbov:"b O ov \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b O ov \<subseteq> b
[PROOF STEP]
apply (auto simp:b ov)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z t k l u v ta. \<lbrakk>x \<parallel> t; t \<parallel> y; k \<parallel> y; y \<parallel> u; u \<parallel> v; k \<parallel> l; l \<parallel> z; z \<parallel> v; l \<parallel> ta; ta \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
using M1 M5exist_var
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s
\<lbrakk>?x \<parallel> ?y; ?y \<parallel> ?z; ?z \<parallel> ?w\<rbrakk> \<Longrightarrow> \<exists>t. ?x \<parallel> t \<and> t \<parallel> ?w

goal (1 subgoal):
 1. \<And>x y z t k l u v ta. \<lbrakk>x \<parallel> t; t \<parallel> y; k \<parallel> y; y \<parallel> u; u \<parallel> v; k \<parallel> l; l \<parallel> z; z \<parallel> v; l \<parallel> ta; ta \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by blast


[STATEMENT]
lemma cbfi:"b O f^-1 \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b O f\<inverse> \<subseteq> b
[PROOF STEP]
apply (auto simp:b f)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z t k l u. \<lbrakk>x \<parallel> t; t \<parallel> y; k \<parallel> l; l \<parallel> z; z \<parallel> u; k \<parallel> y; y \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by (meson M1 M5exist_var)


[STATEMENT]
lemma cbdi:"b O d^-1 \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b O d\<inverse> \<subseteq> b
[PROOF STEP]
apply (auto simp: b d)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z t k l u v. \<lbrakk>x \<parallel> t; t \<parallel> y; k \<parallel> l; l \<parallel> z; z \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by (meson M1 M5exist_var)


[STATEMENT]
lemma cbs:"b O s \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b O s \<subseteq> b
[PROOF STEP]
apply (auto simp: b s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z t k u v. \<lbrakk>x \<parallel> t; t \<parallel> y; k \<parallel> y; y \<parallel> u; u \<parallel> v; k \<parallel> z; z \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by (meson M1 M5exist_var)


[STATEMENT]
lemma cbsi:"b O s^-1 \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b O s\<inverse> \<subseteq> b
[PROOF STEP]
apply (auto simp: b s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z t k u v. \<lbrakk>x \<parallel> t; t \<parallel> y; k \<parallel> z; z \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by (meson M1 M5exist_var)


[STATEMENT]
lemma (in arelations) cmb:"m O b \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m O b \<subseteq> b
[PROOF STEP]
by (r_compose r1:m r2:b r3:b)


[STATEMENT]
lemma cmm:"m O m \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m O m \<subseteq> b
[PROOF STEP]
by (auto simp: b m)


[STATEMENT]
lemma cmov:"m O ov \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m O ov \<subseteq> b
[PROOF STEP]
apply (auto simp:b m ov)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k l u v t. \<lbrakk>x \<parallel> y; k \<parallel> y; y \<parallel> u; u \<parallel> v; k \<parallel> l; l \<parallel> z; z \<parallel> v; l \<parallel> t; t \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
using M1 M5exist_var
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s
\<lbrakk>?x \<parallel> ?y; ?y \<parallel> ?z; ?z \<parallel> ?w\<rbrakk> \<Longrightarrow> \<exists>t. ?x \<parallel> t \<and> t \<parallel> ?w

goal (1 subgoal):
 1. \<And>x y z k l u v t. \<lbrakk>x \<parallel> y; k \<parallel> y; y \<parallel> u; u \<parallel> v; k \<parallel> l; l \<parallel> z; z \<parallel> v; l \<parallel> t; t \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by blast


[STATEMENT]
lemma cmdi:"m O d^-1 \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m O d\<inverse> \<subseteq> b
[PROOF STEP]
apply (auto simp add:m d b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k l u v. \<lbrakk>x \<parallel> y; k \<parallel> l; l \<parallel> z; z \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. \<And>x y z k l u v. \<lbrakk>x \<parallel> y; k \<parallel> l; l \<parallel> z; z \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by blast


[STATEMENT]
lemma cms:"m O s \<subseteq> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m O s \<subseteq> m
[PROOF STEP]
apply (auto simp add:m s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k u v. \<lbrakk>x \<parallel> y; k \<parallel> y; y \<parallel> u; u \<parallel> v; k \<parallel> z; z \<parallel> v\<rbrakk> \<Longrightarrow> x \<parallel> z
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. \<And>x y z k u v. \<lbrakk>x \<parallel> y; k \<parallel> y; y \<parallel> u; u \<parallel> v; k \<parallel> z; z \<parallel> v\<rbrakk> \<Longrightarrow> x \<parallel> z
[PROOF STEP]
by auto


[STATEMENT]
lemma cmsi:"m O s^-1 \<subseteq> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m O s\<inverse> \<subseteq> m
[PROOF STEP]
apply (auto simp add:m s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k u v. \<lbrakk>x \<parallel> y; k \<parallel> z; z \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> x \<parallel> z
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. \<And>x y z k u v. \<lbrakk>x \<parallel> y; k \<parallel> z; z \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> x \<parallel> z
[PROOF STEP]
by blast


[STATEMENT]
lemma covb:"ov O b \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov O b \<subseteq> b
[PROOF STEP]
apply (auto simp:ov b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k t l u v ta. \<lbrakk>k \<parallel> x; y \<parallel> t; t \<parallel> z; x \<parallel> u; u \<parallel> v; k \<parallel> l; l \<parallel> y; y \<parallel> v; l \<parallel> ta; ta \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
using M1 M5exist_var
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s
\<lbrakk>?x \<parallel> ?y; ?y \<parallel> ?z; ?z \<parallel> ?w\<rbrakk> \<Longrightarrow> \<exists>t. ?x \<parallel> t \<and> t \<parallel> ?w

goal (1 subgoal):
 1. \<And>x y z k t l u v ta. \<lbrakk>k \<parallel> x; y \<parallel> t; t \<parallel> z; x \<parallel> u; u \<parallel> v; k \<parallel> l; l \<parallel> y; y \<parallel> v; l \<parallel> ta; ta \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by blast


[STATEMENT]
lemma covm:"ov O m \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov O m \<subseteq> b
[PROOF STEP]
apply (auto simp:ov m b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k l u v t. \<lbrakk>y \<parallel> z; k \<parallel> x; x \<parallel> u; u \<parallel> v; k \<parallel> l; l \<parallel> y; y \<parallel> v; l \<parallel> t; t \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. \<And>x y z k l u v t. \<lbrakk>y \<parallel> z; k \<parallel> x; x \<parallel> u; u \<parallel> v; k \<parallel> l; l \<parallel> y; y \<parallel> v; l \<parallel> t; t \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by blast


[STATEMENT]
lemma covs:"ov O s \<subseteq> ov"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov O s \<subseteq> ov
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ov O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
fix p::"'a\<times>'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ov O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
assume "p \<in> ov O s"
[PROOF STATE]
proof (state)
this:
p \<in> ov O s

goal (1 subgoal):
 1. \<And>x. x \<in> ov O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> ov O s
[PROOF STEP]
obtain x y z where p:"p = (x,z)" and xyov:"(x,y)\<in> ov" and yzs:"(y,z) \<in> s"
[PROOF STATE]
proof (prove)
using this:
p \<in> ov O s

goal (1 subgoal):
 1. (\<And>x z y. \<lbrakk>p = (x, z); (x, y) \<in> ov; (y, z) \<in> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = (x, z)
(x, y) \<in> ov
(y, z) \<in> s

goal (1 subgoal):
 1. \<And>x. x \<in> ov O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
from xyov
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> ov
[PROOF STEP]
obtain r u v t k where rx:"r\<parallel>x" and xu:"x\<parallel>u" and uv:"u\<parallel>v" and rt:"r\<parallel>t" and tk:"t\<parallel>k" and ty:"t\<parallel>y" and yv:"y\<parallel>v" and ku:"k\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> ov

goal (1 subgoal):
 1. (\<And>r u v t k. \<lbrakk>r \<parallel> x; x \<parallel> u; u \<parallel> v; r \<parallel> t; t \<parallel> k; t \<parallel> y; y \<parallel> v; k \<parallel> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ov
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> ov
((?p, ?q) \<in> ov) = (\<exists>k l u v t. (k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v) \<and> (k \<parallel> l \<and> l \<parallel> ?q \<and> ?q \<parallel> v) \<and> l \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. (\<And>r u v t k. \<lbrakk>r \<parallel> x; x \<parallel> u; u \<parallel> v; r \<parallel> t; t \<parallel> k; t \<parallel> y; y \<parallel> v; k \<parallel> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<parallel> x
x \<parallel> u
u \<parallel> v
r \<parallel> t
t \<parallel> k
t \<parallel> y
y \<parallel> v
k \<parallel> u

goal (1 subgoal):
 1. \<And>x. x \<in> ov O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
from yzs
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> s
[PROOF STEP]
obtain l1 l2 where yl1:"y\<parallel>l1" and l1l2:"l1\<parallel>l2" and zl2:"z\<parallel>l2"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> s

goal (1 subgoal):
 1. (\<And>l1 l2. \<lbrakk>y \<parallel> l1; l1 \<parallel> l2; z \<parallel> l2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> s
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)

goal (1 subgoal):
 1. (\<And>l1 l2. \<lbrakk>y \<parallel> l1; l1 \<parallel> l2; z \<parallel> l2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<parallel> l1
l1 \<parallel> l2
z \<parallel> l2

goal (1 subgoal):
 1. \<And>x. x \<in> ov O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
from uv yl1 yv
[PROOF STATE]
proof (chain)
picking this:
u \<parallel> v
y \<parallel> l1
y \<parallel> v
[PROOF STEP]
have "u\<parallel>l1"
[PROOF STATE]
proof (prove)
using this:
u \<parallel> v
y \<parallel> l1
y \<parallel> v

goal (1 subgoal):
 1. u \<parallel> l1
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
u \<parallel> v
y \<parallel> l1
y \<parallel> v
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

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

goal (1 subgoal):
 1. \<And>x. x \<in> ov O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
with xu l1l2
[PROOF STATE]
proof (chain)
picking this:
x \<parallel> u
l1 \<parallel> l2
u \<parallel> l1
[PROOF STEP]
obtain ul1 where xul1:"x\<parallel>ul1" and ul1l2:"ul1\<parallel>l2"
[PROOF STATE]
proof (prove)
using this:
x \<parallel> u
l1 \<parallel> l2
u \<parallel> l1

goal (1 subgoal):
 1. (\<And>ul1. \<lbrakk>x \<parallel> ul1; ul1 \<parallel> l2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M5exist_var
[PROOF STATE]
proof (prove)
using this:
x \<parallel> u
l1 \<parallel> l2
u \<parallel> l1
\<lbrakk>?x \<parallel> ?y; ?y \<parallel> ?z; ?z \<parallel> ?w\<rbrakk> \<Longrightarrow> \<exists>t. ?x \<parallel> t \<and> t \<parallel> ?w

goal (1 subgoal):
 1. (\<And>ul1. \<lbrakk>x \<parallel> ul1; ul1 \<parallel> l2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<parallel> ul1
ul1 \<parallel> l2

goal (1 subgoal):
 1. \<And>x. x \<in> ov O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
from ku xu xul1 l1l2
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> u
x \<parallel> u
x \<parallel> ul1
l1 \<parallel> l2
[PROOF STEP]
have kul1:"k\<parallel>ul1"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> u
x \<parallel> u
x \<parallel> ul1
l1 \<parallel> l2

goal (1 subgoal):
 1. k \<parallel> ul1
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
k \<parallel> u
x \<parallel> u
x \<parallel> ul1
l1 \<parallel> l2
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

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

goal (1 subgoal):
 1. \<And>x. x \<in> ov O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
from ty yzs
[PROOF STATE]
proof (chain)
picking this:
t \<parallel> y
(y, z) \<in> s
[PROOF STEP]
have "t\<parallel>z"
[PROOF STATE]
proof (prove)
using this:
t \<parallel> y
(y, z) \<in> s

goal (1 subgoal):
 1. t \<parallel> z
[PROOF STEP]
using s M1
[PROOF STATE]
proof (prove)
using this:
t \<parallel> y
(y, z) \<in> s
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

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

goal (1 subgoal):
 1. \<And>x. x \<in> ov O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
with rx rt xul1 ul1l2 zl2 tk kul1
[PROOF STATE]
proof (chain)
picking this:
r \<parallel> x
r \<parallel> t
x \<parallel> ul1
ul1 \<parallel> l2
z \<parallel> l2
t \<parallel> k
k \<parallel> ul1
t \<parallel> z
[PROOF STEP]
have "(x,z) \<in> ov"
[PROOF STATE]
proof (prove)
using this:
r \<parallel> x
r \<parallel> t
x \<parallel> ul1
ul1 \<parallel> l2
z \<parallel> l2
t \<parallel> k
k \<parallel> ul1
t \<parallel> z

goal (1 subgoal):
 1. (x, z) \<in> ov
[PROOF STEP]
using ov
[PROOF STATE]
proof (prove)
using this:
r \<parallel> x
r \<parallel> t
x \<parallel> ul1
ul1 \<parallel> l2
z \<parallel> l2
t \<parallel> k
k \<parallel> ul1
t \<parallel> z
((?p, ?q) \<in> ov) = (\<exists>k l u v t. (k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v) \<and> (k \<parallel> l \<and> l \<parallel> ?q \<and> ?q \<parallel> v) \<and> l \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. (x, z) \<in> ov
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x, z) \<in> ov

goal (1 subgoal):
 1. \<And>x. x \<in> ov O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
p = (x, z)
(x, z) \<in> ov
[PROOF STEP]
show "p \<in> ov"
[PROOF STATE]
proof (prove)
using this:
p = (x, z)
(x, z) \<in> ov

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cfib:"f^-1 O b \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<inverse> O b \<subseteq> b
[PROOF STEP]
apply (auto simp:f b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z t k l u. \<lbrakk>y \<parallel> t; t \<parallel> z; k \<parallel> l; l \<parallel> y; y \<parallel> u; k \<parallel> x; x \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. \<And>x y z t k l u. \<lbrakk>y \<parallel> t; t \<parallel> z; k \<parallel> l; l \<parallel> y; y \<parallel> u; k \<parallel> x; x \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by blast


[STATEMENT]
lemma cfim:"f^-1 O m \<subseteq> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<inverse> O m \<subseteq> m
[PROOF STEP]
apply (auto simp:f m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k l u. \<lbrakk>y \<parallel> z; k \<parallel> l; l \<parallel> y; y \<parallel> u; k \<parallel> x; x \<parallel> u\<rbrakk> \<Longrightarrow> x \<parallel> z
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. \<And>x y z k l u. \<lbrakk>y \<parallel> z; k \<parallel> l; l \<parallel> y; y \<parallel> u; k \<parallel> x; x \<parallel> u\<rbrakk> \<Longrightarrow> x \<parallel> z
[PROOF STEP]
by auto


[STATEMENT]
lemma cfiov:"f^-1 O ov \<subseteq> ov"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<inverse> O ov \<subseteq> ov
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O ov \<Longrightarrow> x \<in> ov
[PROOF STEP]
fix p::"'a\<times>'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O ov \<Longrightarrow> x \<in> ov
[PROOF STEP]
assume "p \<in> f^-1 O ov"
[PROOF STATE]
proof (state)
this:
p \<in> f\<inverse> O ov

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O ov \<Longrightarrow> x \<in> ov
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> f\<inverse> O ov
[PROOF STEP]
obtain x y z where p:"p = (x,z)" and xyfi:"(x,y)\<in> f^-1" and yzov:"(y,z) \<in> ov"
[PROOF STATE]
proof (prove)
using this:
p \<in> f\<inverse> O ov

goal (1 subgoal):
 1. (\<And>x z y. \<lbrakk>p = (x, z); (x, y) \<in> f\<inverse>; (y, z) \<in> ov\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = (x, z)
(x, y) \<in> f\<inverse>
(y, z) \<in> ov

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O ov \<Longrightarrow> x \<in> ov
[PROOF STEP]
from xyfi yzov
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> f\<inverse>
(y, z) \<in> ov
[PROOF STEP]
obtain t' r u   where tpr:"t'\<parallel>r" and ry:"r\<parallel>y" and yu:"y\<parallel>u" and tpx:"t'\<parallel>x" and xu:"x\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> f\<inverse>
(y, z) \<in> ov

goal (1 subgoal):
 1. (\<And>t' r u. \<lbrakk>t' \<parallel> r; r \<parallel> y; y \<parallel> u; t' \<parallel> x; x \<parallel> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> f\<inverse>
(y, z) \<in> ov
((?p, ?q) \<in> f) = (\<exists>k l u. k \<parallel> l \<and> l \<parallel> ?p \<and> ?p \<parallel> u \<and> k \<parallel> ?q \<and> ?q \<parallel> u)

goal (1 subgoal):
 1. (\<And>t' r u. \<lbrakk>t' \<parallel> r; r \<parallel> y; y \<parallel> u; t' \<parallel> x; x \<parallel> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t' \<parallel> r
r \<parallel> y
y \<parallel> u
t' \<parallel> x
x \<parallel> u

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O ov \<Longrightarrow> x \<in> ov
[PROOF STEP]
from yzov  ry
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> ov
r \<parallel> y
[PROOF STEP]
obtain v k t u' where yup:"y\<parallel>u'" and upv:"u'\<parallel>v" and rk:"r\<parallel>k" and kz:"k\<parallel>z" and zv:"z\<parallel>v" and kt:"k\<parallel>t" and tup:"t\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> ov
r \<parallel> y

goal (1 subgoal):
 1. (\<And>u' v k t. \<lbrakk>y \<parallel> u'; u' \<parallel> v; r \<parallel> k; k \<parallel> z; z \<parallel> v; k \<parallel> t; t \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ov
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> ov
r \<parallel> y
((?p, ?q) \<in> ov) = (\<exists>k l u v t. (k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v) \<and> (k \<parallel> l \<and> l \<parallel> ?q \<and> ?q \<parallel> v) \<and> l \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. (\<And>u' v k t. \<lbrakk>y \<parallel> u'; u' \<parallel> v; r \<parallel> k; k \<parallel> z; z \<parallel> v; k \<parallel> t; t \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> ov
r \<parallel> y
((?p, ?q) \<in> ov) = (\<exists>k l u v t. (k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v) \<and> (k \<parallel> l \<and> l \<parallel> ?q \<and> ?q \<parallel> v) \<and> l \<parallel> t \<and> t \<parallel> u)
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. (\<And>u' v k t. \<lbrakk>y \<parallel> u'; u' \<parallel> v; r \<parallel> k; k \<parallel> z; z \<parallel> v; k \<parallel> t; t \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<parallel> u'
u' \<parallel> v
r \<parallel> k
k \<parallel> z
z \<parallel> v
k \<parallel> t
t \<parallel> u'

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O ov \<Longrightarrow> x \<in> ov
[PROOF STEP]
from yu xu yup
[PROOF STATE]
proof (chain)
picking this:
y \<parallel> u
x \<parallel> u
y \<parallel> u'
[PROOF STEP]
have xup:"x\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
y \<parallel> u
x \<parallel> u
y \<parallel> u'

goal (1 subgoal):
 1. x \<parallel> u'
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
y \<parallel> u
x \<parallel> u
y \<parallel> u'
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. x \<parallel> u'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<parallel> u'

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O ov \<Longrightarrow> x \<in> ov
[PROOF STEP]
from tpr rk kt
[PROOF STATE]
proof (chain)
picking this:
t' \<parallel> r
r \<parallel> k
k \<parallel> t
[PROOF STEP]
obtain r' where tprp:"t'\<parallel>r'" and rpt:"r'\<parallel>t"
[PROOF STATE]
proof (prove)
using this:
t' \<parallel> r
r \<parallel> k
k \<parallel> t

goal (1 subgoal):
 1. (\<And>r'. \<lbrakk>t' \<parallel> r'; r' \<parallel> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M5exist_var
[PROOF STATE]
proof (prove)
using this:
t' \<parallel> r
r \<parallel> k
k \<parallel> t
\<lbrakk>?x \<parallel> ?y; ?y \<parallel> ?z; ?z \<parallel> ?w\<rbrakk> \<Longrightarrow> \<exists>t. ?x \<parallel> t \<and> t \<parallel> ?w

goal (1 subgoal):
 1. (\<And>r'. \<lbrakk>t' \<parallel> r'; r' \<parallel> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t' \<parallel> r'
r' \<parallel> t

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O ov \<Longrightarrow> x \<in> ov
[PROOF STEP]
from kt rpt kz
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> t
r' \<parallel> t
k \<parallel> z
[PROOF STEP]
have rpz:"r'\<parallel>z"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> t
r' \<parallel> t
k \<parallel> z

goal (1 subgoal):
 1. r' \<parallel> z
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
k \<parallel> t
r' \<parallel> t
k \<parallel> z
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. r' \<parallel> z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r' \<parallel> z

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O ov \<Longrightarrow> x \<in> ov
[PROOF STEP]
from tprp rpz rpt tpx xup zv upv tup
[PROOF STATE]
proof (chain)
picking this:
t' \<parallel> r'
r' \<parallel> z
r' \<parallel> t
t' \<parallel> x
x \<parallel> u'
z \<parallel> v
u' \<parallel> v
t \<parallel> u'
[PROOF STEP]
have "(x,z) \<in> ov"
[PROOF STATE]
proof (prove)
using this:
t' \<parallel> r'
r' \<parallel> z
r' \<parallel> t
t' \<parallel> x
x \<parallel> u'
z \<parallel> v
u' \<parallel> v
t \<parallel> u'

goal (1 subgoal):
 1. (x, z) \<in> ov
[PROOF STEP]
using ov
[PROOF STATE]
proof (prove)
using this:
t' \<parallel> r'
r' \<parallel> z
r' \<parallel> t
t' \<parallel> x
x \<parallel> u'
z \<parallel> v
u' \<parallel> v
t \<parallel> u'
((?p, ?q) \<in> ov) = (\<exists>k l u v t. (k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v) \<and> (k \<parallel> l \<and> l \<parallel> ?q \<and> ?q \<parallel> v) \<and> l \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. (x, z) \<in> ov
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x, z) \<in> ov

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O ov \<Longrightarrow> x \<in> ov
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
p = (x, z)
(x, z) \<in> ov
[PROOF STEP]
show "p \<in> ov"
[PROOF STATE]
proof (prove)
using this:
p = (x, z)
(x, z) \<in> ov

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

goal:
No subgoals!
[PROOF STEP]
qed