[STATEMENT]
lemma llist_le_anti_sym:
  fixes s:: "'a llist"
  assumes st: "s \<le> t"
  and ts: "t \<le> s"
  shows "s = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
have "s \<in> UNIV\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> UNIV\<^sup>\<infinity>

goal (1 subgoal):
 1. s = t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> UNIV\<^sup>\<infinity>

goal (1 subgoal):
 1. s = t
[PROOF STEP]
proof (cases rule: alllstsE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<in> UNIV\<^sup>\<star> \<Longrightarrow> s = t
 2. s \<in> UNIV\<^sup>\<omega> \<Longrightarrow> s = t
[PROOF STEP]
case finite
[PROOF STATE]
proof (state)
this:
s \<in> UNIV\<^sup>\<star>

goal (2 subgoals):
 1. s \<in> UNIV\<^sup>\<star> \<Longrightarrow> s = t
 2. s \<in> UNIV\<^sup>\<omega> \<Longrightarrow> s = t
[PROOF STEP]
hence "\<forall> t.  s \<le> t \<and> t \<le> s \<longrightarrow> s = t"
[PROOF STATE]
proof (prove)
using this:
s \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. \<forall>t. s \<le> t \<and> t \<le> s \<longrightarrow> s = t
[PROOF STEP]
proof (induct rule: finlsts.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>t. LNil \<le> t \<and> t \<le> LNil \<longrightarrow> LNil = t
 2. \<And>l a. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<forall>t. l \<le> t \<and> t \<le> l \<longrightarrow> l = t; a \<in> UNIV\<rbrakk> \<Longrightarrow> \<forall>t. a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<forall>t. LNil \<le> t \<and> t \<le> LNil \<longrightarrow> LNil = t
 2. \<And>l a. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<forall>t. l \<le> t \<and> t \<le> l \<longrightarrow> l = t; a \<in> UNIV\<rbrakk> \<Longrightarrow> \<forall>t. a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. LNil \<le> t \<and> t \<le> LNil \<longrightarrow> LNil = t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>t. LNil \<le> t \<and> t \<le> LNil \<longrightarrow> LNil = t

goal (1 subgoal):
 1. \<And>l a. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<forall>t. l \<le> t \<and> t \<le> l \<longrightarrow> l = t; a \<in> UNIV\<rbrakk> \<Longrightarrow> \<forall>t. a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l a. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<forall>t. l \<le> t \<and> t \<le> l \<longrightarrow> l = t; a \<in> UNIV\<rbrakk> \<Longrightarrow> \<forall>t. a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t
[PROOF STEP]
case (LCons_fin l a)
[PROOF STATE]
proof (state)
this:
l \<in> UNIV\<^sup>\<star>
\<forall>t. l \<le> t \<and> t \<le> l \<longrightarrow> l = t
a \<in> UNIV

goal (1 subgoal):
 1. \<And>l a. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<forall>t. l \<le> t \<and> t \<le> l \<longrightarrow> l = t; a \<in> UNIV\<rbrakk> \<Longrightarrow> \<forall>t. a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t
[PROOF STEP]
from LCons_fin
[PROOF STATE]
proof (chain)
picking this:
l \<in> UNIV\<^sup>\<star>
\<forall>t. l \<le> t \<and> t \<le> l \<longrightarrow> l = t
a \<in> UNIV
[PROOF STEP]
show  "a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t"
[PROOF STATE]
proof (prove)
using this:
l \<in> UNIV\<^sup>\<star>
\<forall>t. l \<le> t \<and> t \<le> l \<longrightarrow> l = t
a \<in> UNIV

goal (1 subgoal):
 1. a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t
[PROOF STEP]
by (cases "t") blast+
[PROOF STATE]
proof (state)
this:
a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t. a ## l \<le> t \<and> t \<le> a ## l \<longrightarrow> a ## l = t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t. s \<le> t \<and> t \<le> s \<longrightarrow> s = t

goal (2 subgoals):
 1. s \<in> UNIV\<^sup>\<star> \<Longrightarrow> s = t
 2. s \<in> UNIV\<^sup>\<omega> \<Longrightarrow> s = t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>t. s \<le> t \<and> t \<le> s \<longrightarrow> s = t

goal (1 subgoal):
 1. s = t
[PROOF STEP]
using st ts
[PROOF STATE]
proof (prove)
using this:
\<forall>t. s \<le> t \<and> t \<le> s \<longrightarrow> s = t
s \<le> t
t \<le> s

goal (1 subgoal):
 1. s = t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s = t

goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<omega> \<Longrightarrow> s = t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<omega> \<Longrightarrow> s = t
[PROOF STEP]
case infinite
[PROOF STATE]
proof (state)
this:
s \<in> UNIV\<^sup>\<omega>

goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<omega> \<Longrightarrow> s = t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> UNIV\<^sup>\<omega>

goal (1 subgoal):
 1. s = t
[PROOF STEP]
using st
[PROOF STATE]
proof (prove)
using this:
s \<in> UNIV\<^sup>\<omega>
s \<le> t

goal (1 subgoal):
 1. s = t
[PROOF STEP]
by (simp add: llist_inf_le)
[PROOF STATE]
proof (state)
this:
s = t

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma llist_less_le_not_le:
  fixes s :: "'a llist"
  shows "(s < t) = (s \<le> t \<and> \<not> t \<le> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s < t) = (s \<le> t \<and> \<not> t \<le> s)
[PROOF STEP]
by (auto simp add: llist_less_def dest: llist_le_anti_sym)


[STATEMENT]
lemma llist_le_finT [simp]:
 "r\<le>s \<Longrightarrow> s \<in> A\<^sup>\<star> \<Longrightarrow> r \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<le> s; s \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>r \<le> s; s \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
assume rs: "r\<le>s" and sfin: "s \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (state)
this:
r \<le> s
s \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. \<lbrakk>r \<le> s; s \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
from sfin
[PROOF STATE]
proof (chain)
picking this:
s \<in> A\<^sup>\<star>
[PROOF STEP]
have "\<forall>r. r\<le>s \<longrightarrow> r\<in>A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
s \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. \<forall>r\<le>s. r \<in> A\<^sup>\<star>
[PROOF STEP]
proof (induct "s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> \<forall>r\<le>l. r \<in> A\<^sup>\<star>
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; \<forall>r\<le>l. r \<in> A\<^sup>\<star>; a \<in> A\<rbrakk> \<Longrightarrow> \<forall>r\<le>a ## l. r \<in> A\<^sup>\<star>
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
l_ = LNil

goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> \<forall>r\<le>l. r \<in> A\<^sup>\<star>
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; \<forall>r\<le>l. r \<in> A\<^sup>\<star>; a \<in> A\<rbrakk> \<Longrightarrow> \<forall>r\<le>a ## l. r \<in> A\<^sup>\<star>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l_ = LNil

goal (1 subgoal):
 1. \<forall>r\<le>l_. r \<in> A\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>r\<le>l_. r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; \<forall>r\<le>l. r \<in> A\<^sup>\<star>; a \<in> A\<rbrakk> \<Longrightarrow> \<forall>r\<le>a ## l. r \<in> A\<^sup>\<star>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; \<forall>r\<le>l. r \<in> A\<^sup>\<star>; a \<in> A\<rbrakk> \<Longrightarrow> \<forall>r\<le>a ## l. r \<in> A\<^sup>\<star>
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> A\<^sup>\<star>
\<forall>r\<le>l. r \<in> A\<^sup>\<star>
a \<in> A

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; \<forall>r\<le>l. r \<in> A\<^sup>\<star>; a \<in> A\<rbrakk> \<Longrightarrow> \<forall>r\<le>a ## l. r \<in> A\<^sup>\<star>
[PROOF STEP]
show  ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r\<le>a ## l. r \<in> A\<^sup>\<star>
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. r \<le> a ## l \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. r \<le> a ## l \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
assume ral: "r \<le> a ## l"
[PROOF STATE]
proof (state)
this:
r \<le> a ## l

goal (1 subgoal):
 1. \<And>r. r \<le> a ## l \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
thus "r \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
r \<le> a ## l

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
using LCons_fin
[PROOF STATE]
proof (prove)
using this:
r \<le> a ## l
l \<in> A\<^sup>\<star>
\<forall>r\<le>l. r \<in> A\<^sup>\<star>
a \<in> A

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
by (cases r) auto
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>r\<le>a ## l. r \<in> A\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>r\<le>s. r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. \<lbrakk>r \<le> s; s \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
with rs
[PROOF STATE]
proof (chain)
picking this:
r \<le> s
\<forall>r\<le>s. r \<in> A\<^sup>\<star>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<le> s
\<forall>r\<le>s. r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma llist_less_finT [iff]:
 "r<s \<Longrightarrow> s \<in> A\<^sup>\<star> \<Longrightarrow> r \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r < s; s \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
by (auto simp: less_le)


[STATEMENT]
lemma LNil_less_LCons [iff]: "LNil < a ## t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LNil < a ## t
[PROOF STEP]
by (simp add: less_le)


[STATEMENT]
lemma not_less_LNil [iff]:
  "\<not> r < LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> r < LNil
[PROOF STEP]
by (auto simp: less_le)


[STATEMENT]
lemma less_LCons [iff]:
  " (a ## r < b ## t) = (a = b \<and> r < t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a ## r < b ## t) = (a = b \<and> r < t)
[PROOF STEP]
by (auto simp: less_le)


[STATEMENT]
lemma llength_mono [iff]:
  assumes"r \<in> A\<^sup>\<star>"
  shows "s<r \<Longrightarrow> llength s < llength r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < r \<Longrightarrow> LList2.llength s < LList2.llength r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. s < r \<Longrightarrow> LList2.llength s < LList2.llength r
[PROOF STEP]
proof(induct "r" arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l s. \<lbrakk>l = LNil; s < l\<rbrakk> \<Longrightarrow> LList2.llength s < LList2.llength l
 2. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. s < l \<Longrightarrow> LList2.llength s < LList2.llength l; a \<in> A; s < a ## l\<rbrakk> \<Longrightarrow> LList2.llength s < LList2.llength (a ## l)
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
l_ = LNil
s < l_

goal (2 subgoals):
 1. \<And>l s. \<lbrakk>l = LNil; s < l\<rbrakk> \<Longrightarrow> LList2.llength s < LList2.llength l
 2. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. s < l \<Longrightarrow> LList2.llength s < LList2.llength l; a \<in> A; s < a ## l\<rbrakk> \<Longrightarrow> LList2.llength s < LList2.llength (a ## l)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l_ = LNil
s < l_

goal (1 subgoal):
 1. LList2.llength s < LList2.llength l_
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LList2.llength s < LList2.llength l_

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. s < l \<Longrightarrow> LList2.llength s < LList2.llength l; a \<in> A; s < a ## l\<rbrakk> \<Longrightarrow> LList2.llength s < LList2.llength (a ## l)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. s < l \<Longrightarrow> LList2.llength s < LList2.llength l; a \<in> A; s < a ## l\<rbrakk> \<Longrightarrow> LList2.llength s < LList2.llength (a ## l)
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> A\<^sup>\<star>
?s < l \<Longrightarrow> LList2.llength ?s < LList2.llength l
a \<in> A
s < a ## l

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. s < l \<Longrightarrow> LList2.llength s < LList2.llength l; a \<in> A; s < a ## l\<rbrakk> \<Longrightarrow> LList2.llength s < LList2.llength (a ## l)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<star>
?s < l \<Longrightarrow> LList2.llength ?s < LList2.llength l
a \<in> A
s < a ## l

goal (1 subgoal):
 1. LList2.llength s < LList2.llength (a ## l)
[PROOF STEP]
by (cases s) (auto simp: llength_LCons [of _ UNIV])
[PROOF STATE]
proof (state)
this:
LList2.llength s < LList2.llength (a ## l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma le_lappend [iff]: "r \<le> r @@ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> r @@ s
[PROOF STEP]
by (auto simp: llist_le_def)


[STATEMENT]
lemma take_inf_less:
  "t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<down> i < t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<down> i < t
[PROOF STEP]
proof (induct i arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<down> 0 < t
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<down> i < t; t \<in> UNIV\<^sup>\<omega>\<rbrakk> \<Longrightarrow> t \<down> Suc i < t
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t \<in> UNIV\<^sup>\<omega>

goal (2 subgoals):
 1. \<And>t. t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<down> 0 < t
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<down> i < t; t \<in> UNIV\<^sup>\<omega>\<rbrakk> \<Longrightarrow> t \<down> Suc i < t
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
t \<in> UNIV\<^sup>\<omega>

goal (1 subgoal):
 1. t \<down> 0 < t
[PROOF STEP]
by (auto elim: inflsts_cases)
[PROOF STATE]
proof (state)
this:
t \<down> 0 < t

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<down> i < t; t \<in> UNIV\<^sup>\<omega>\<rbrakk> \<Longrightarrow> t \<down> Suc i < t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<down> i < t; t \<in> UNIV\<^sup>\<omega>\<rbrakk> \<Longrightarrow> t \<down> Suc i < t
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
?t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> ?t \<down> i < ?t
t \<in> UNIV\<^sup>\<omega>

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<down> i < t; t \<in> UNIV\<^sup>\<omega>\<rbrakk> \<Longrightarrow> t \<down> Suc i < t
[PROOF STEP]
from \<open>t \<in> UNIV\<^sup>\<omega>\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<in> UNIV\<^sup>\<omega>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
t \<in> UNIV\<^sup>\<omega>

goal (1 subgoal):
 1. t \<down> Suc i < t
[PROOF STEP]
proof (cases "t")
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<omega>; a \<in> UNIV; t = a ## l\<rbrakk> \<Longrightarrow> t \<down> Suc i < t
[PROOF STEP]
case (LCons a l)
[PROOF STATE]
proof (state)
this:
l \<in> UNIV\<^sup>\<omega>
a \<in> UNIV
t = a ## l

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<omega>; a \<in> UNIV; t = a ## l\<rbrakk> \<Longrightarrow> t \<down> Suc i < t
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
?t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> ?t \<down> i < ?t
t \<in> UNIV\<^sup>\<omega>
l \<in> UNIV\<^sup>\<omega>
a \<in> UNIV
t = a ## l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> ?t \<down> i < ?t
t \<in> UNIV\<^sup>\<omega>
l \<in> UNIV\<^sup>\<omega>
a \<in> UNIV
t = a ## l

goal (1 subgoal):
 1. t \<down> Suc i < t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<down> Suc i < t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<down> Suc i < t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lapp_take_less:
  assumes iless: "i < llength r"
  shows "(r @@ s) \<down> i < r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r @@ s) \<down> i < r
[PROOF STEP]
proof (cases "r \<in> UNIV\<^sup>\<star>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<in> UNIV\<^sup>\<star> \<Longrightarrow> (r @@ s) \<down> i < r
 2. r \<notin> UNIV\<^sup>\<star> \<Longrightarrow> (r @@ s) \<down> i < r
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
r \<in> UNIV\<^sup>\<star>

goal (2 subgoals):
 1. r \<in> UNIV\<^sup>\<star> \<Longrightarrow> (r @@ s) \<down> i < r
 2. r \<notin> UNIV\<^sup>\<star> \<Longrightarrow> (r @@ s) \<down> i < r
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. (r @@ s) \<down> i < r
[PROOF STEP]
using iless
[PROOF STATE]
proof (prove)
using this:
r \<in> UNIV\<^sup>\<star>
i < LList2.llength r

goal (1 subgoal):
 1. (r @@ s) \<down> i < r
[PROOF STEP]
proof(induct i arbitrary: r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>r \<in> UNIV\<^sup>\<star>; 0 < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> 0 < r
 2. \<And>i r. \<lbrakk>\<And>r. \<lbrakk>r \<in> UNIV\<^sup>\<star>; i < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> i < r; r \<in> UNIV\<^sup>\<star>; Suc i < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> Suc i < r
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
r \<in> UNIV\<^sup>\<star>
0 < LList2.llength r

goal (2 subgoals):
 1. \<And>r. \<lbrakk>r \<in> UNIV\<^sup>\<star>; 0 < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> 0 < r
 2. \<And>i r. \<lbrakk>\<And>r. \<lbrakk>r \<in> UNIV\<^sup>\<star>; i < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> i < r; r \<in> UNIV\<^sup>\<star>; Suc i < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> Suc i < r
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
r \<in> UNIV\<^sup>\<star>
0 < LList2.llength r

goal (1 subgoal):
 1. (r @@ s) \<down> 0 < r
[PROOF STEP]
by (cases "r") auto
[PROOF STATE]
proof (state)
this:
(r @@ s) \<down> 0 < r

goal (1 subgoal):
 1. \<And>i r. \<lbrakk>\<And>r. \<lbrakk>r \<in> UNIV\<^sup>\<star>; i < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> i < r; r \<in> UNIV\<^sup>\<star>; Suc i < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> Suc i < r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i r. \<lbrakk>\<And>r. \<lbrakk>r \<in> UNIV\<^sup>\<star>; i < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> i < r; r \<in> UNIV\<^sup>\<star>; Suc i < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> Suc i < r
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?r \<in> UNIV\<^sup>\<star>; j < LList2.llength ?r\<rbrakk> \<Longrightarrow> (?r @@ s) \<down> j < ?r
r \<in> UNIV\<^sup>\<star>
Suc j < LList2.llength r

goal (1 subgoal):
 1. \<And>i r. \<lbrakk>\<And>r. \<lbrakk>r \<in> UNIV\<^sup>\<star>; i < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> i < r; r \<in> UNIV\<^sup>\<star>; Suc i < LList2.llength r\<rbrakk> \<Longrightarrow> (r @@ s) \<down> Suc i < r
[PROOF STEP]
from \<open>r \<in> UNIV\<^sup>\<star>\<close> \<open>Suc j < llength r\<close> \<open>\<And>r. \<lbrakk>r \<in> UNIV\<^sup>\<star>; j < llength r\<rbrakk> \<Longrightarrow> lappend r s \<down> j < r\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<in> UNIV\<^sup>\<star>
Suc j < LList2.llength r
\<lbrakk>?r \<in> UNIV\<^sup>\<star>; j < LList2.llength ?r\<rbrakk> \<Longrightarrow> (?r @@ s) \<down> j < ?r
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
r \<in> UNIV\<^sup>\<star>
Suc j < LList2.llength r
\<lbrakk>?r \<in> UNIV\<^sup>\<star>; j < LList2.llength ?r\<rbrakk> \<Longrightarrow> (?r @@ s) \<down> j < ?r

goal (1 subgoal):
 1. (r @@ s) \<down> Suc j < r
[PROOF STEP]
by (cases) auto
[PROOF STATE]
proof (state)
this:
(r @@ s) \<down> Suc j < r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(r @@ s) \<down> i < r

goal (1 subgoal):
 1. r \<notin> UNIV\<^sup>\<star> \<Longrightarrow> (r @@ s) \<down> i < r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<notin> UNIV\<^sup>\<star> \<Longrightarrow> (r @@ s) \<down> i < r
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
r \<notin> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. r \<notin> UNIV\<^sup>\<star> \<Longrightarrow> (r @@ s) \<down> i < r
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<notin> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. (r @@ s) \<down> i < r
[PROOF STEP]
by (simp add: take_inf_less)
[PROOF STATE]
proof (state)
this:
(r @@ s) \<down> i < r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finpref_LNil [simp]:
  "finpref A LNil = {LNil}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finpref A LNil = {LNil}
[PROOF STEP]
by (auto simp: finpref_def)


[STATEMENT]
lemma finpref_fin: "x \<in> finpref A s \<Longrightarrow> x \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> finpref A s \<Longrightarrow> x \<in> A\<^sup>\<star>
[PROOF STEP]
by (auto simp: finpref_def)


[STATEMENT]
lemma finpref_mono2: "s \<le> t \<Longrightarrow> finpref A s \<subseteq> finpref A t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<le> t \<Longrightarrow> finpref A s \<subseteq> finpref A t
[PROOF STEP]
by (unfold finpref_def) (auto dest: llist_le_trans)


[STATEMENT]
lemma suff_LNil [simp]:
  "suff A LNil = A\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suff A LNil = A\<^sup>\<infinity>
[PROOF STEP]
by (simp add: suff_def)


[STATEMENT]
lemma suff_all: "x \<in> suff A s \<Longrightarrow> x \<in> A\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> suff A s \<Longrightarrow> x \<in> A\<^sup>\<infinity>
[PROOF STEP]
by (auto simp: suff_def)


[STATEMENT]
lemma suff_mono2: "s \<le> t \<Longrightarrow> suff A t \<subseteq> suff A s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<le> t \<Longrightarrow> suff A t \<subseteq> suff A s
[PROOF STEP]
by (unfold suff_def) (auto dest: llist_le_trans)


[STATEMENT]
lemma suff_appE:
  assumes rA: "r \<in> A\<^sup>\<star>"
  and  tsuff: "t \<in> suff A r"
  obtains s where "s \<in> A\<^sup>\<infinity>" "t = r@@s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> A\<^sup>\<infinity>; t = r @@ s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> A\<^sup>\<infinity>; t = r @@ s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from tsuff
[PROOF STATE]
proof (chain)
picking this:
t \<in> suff A r
[PROOF STEP]
obtain s where
    tA: "t \<in> A\<^sup>\<infinity>" and trs: "t = r @@ s"
[PROOF STATE]
proof (prove)
using this:
t \<in> suff A r

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>t \<in> A\<^sup>\<infinity>; t = r @@ s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: suff_def llist_le_def)
[PROOF STATE]
proof (state)
this:
t \<in> A\<^sup>\<infinity>
t = r @@ s

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> A\<^sup>\<infinity>; t = r @@ s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from rA trs tA
[PROOF STATE]
proof (chain)
picking this:
r \<in> A\<^sup>\<star>
t = r @@ s
t \<in> A\<^sup>\<infinity>
[PROOF STEP]
have "s \<in> A\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
using this:
r \<in> A\<^sup>\<star>
t = r @@ s
t \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. s \<in> A\<^sup>\<infinity>
[PROOF STEP]
by (auto simp: lapp_allT_iff)
[PROOF STATE]
proof (state)
this:
s \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> A\<^sup>\<infinity>; t = r @@ s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using trs
[PROOF STATE]
proof (prove)
using this:
s \<in> A\<^sup>\<infinity>
t = r @@ s

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma LNil_suff [iff]: "(LNil \<in> suff A s) = (s = LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LNil \<in> suff A s) = (s = LNil)
[PROOF STEP]
by (auto simp: suff_def)


[STATEMENT]
lemma finpref_suff [dest]:
  "\<lbrakk> r \<in> finpref A t; t\<in>A\<^sup>\<infinity> \<rbrakk> \<Longrightarrow> t \<in> suff A r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> finpref A t; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> t \<in> suff A r
[PROOF STEP]
by (auto simp: finpref_def suff_def)


[STATEMENT]
lemma suff_finpref:
  "\<lbrakk> t \<in> suff A r; r\<in>A\<^sup>\<star> \<rbrakk> \<Longrightarrow> r \<in> finpref A t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> suff A r; r \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> r \<in> finpref A t
[PROOF STEP]
by (auto simp: finpref_def suff_def)


[STATEMENT]
lemma suff_finpref_iff:
  "\<lbrakk> r\<in>A\<^sup>\<star>; t\<in>A\<^sup>\<infinity> \<rbrakk> \<Longrightarrow> (r \<in> finpref A t) = (t \<in> suff A r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> (r \<in> finpref A t) = (t \<in> suff A r)
[PROOF STEP]
by (auto simp: finpref_def suff_def)


[STATEMENT]
lemma infsuff_inf: "x \<in> infsuff A s \<Longrightarrow> x \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> infsuff A s \<Longrightarrow> x \<in> A\<^sup>\<omega>
[PROOF STEP]
by (auto simp: infsuff_def)


[STATEMENT]
lemma infsuff_mono2: "s \<le> t \<Longrightarrow> infsuff A t \<subseteq> infsuff A s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<le> t \<Longrightarrow> infsuff A t \<subseteq> infsuff A s
[PROOF STEP]
by (unfold infsuff_def) (auto dest: llist_le_trans)


[STATEMENT]
lemma infsuff_appE:
  assumes   rA: "r \<in> A\<^sup>\<star>"
  and tinfsuff: "t \<in> infsuff A r"
  obtains s where "s \<in> A\<^sup>\<omega>" "t = r@@s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> A\<^sup>\<omega>; t = r @@ s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> A\<^sup>\<omega>; t = r @@ s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from tinfsuff
[PROOF STATE]
proof (chain)
picking this:
t \<in> infsuff A r
[PROOF STEP]
obtain s where
    tA: "t \<in> A\<^sup>\<omega>" and trs: "t = r @@ s"
[PROOF STATE]
proof (prove)
using this:
t \<in> infsuff A r

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>t \<in> A\<^sup>\<omega>; t = r @@ s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: infsuff_def llist_le_def)
[PROOF STATE]
proof (state)
this:
t \<in> A\<^sup>\<omega>
t = r @@ s

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> A\<^sup>\<omega>; t = r @@ s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from rA trs tA
[PROOF STATE]
proof (chain)
picking this:
r \<in> A\<^sup>\<star>
t = r @@ s
t \<in> A\<^sup>\<omega>
[PROOF STEP]
have "s \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
using this:
r \<in> A\<^sup>\<star>
t = r @@ s
t \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. s \<in> A\<^sup>\<omega>
[PROOF STEP]
by (auto dest: app_invT)
[PROOF STATE]
proof (state)
this:
s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> A\<^sup>\<omega>; t = r @@ s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using trs
[PROOF STATE]
proof (prove)
using this:
s \<in> A\<^sup>\<omega>
t = r @@ s

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finpref_infsuff [dest]:
  "\<lbrakk> r \<in> finpref A t; t\<in>A\<^sup>\<omega> \<rbrakk> \<Longrightarrow> t \<in> infsuff A r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> finpref A t; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> t \<in> infsuff A r
[PROOF STEP]
by (auto simp: finpref_def infsuff_def)


[STATEMENT]
lemma infsuff_finpref:
  "\<lbrakk> t \<in> infsuff A r; r\<in>A\<^sup>\<star> \<rbrakk> \<Longrightarrow> r \<in> finpref A t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> infsuff A r; r \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> r \<in> finpref A t
[PROOF STEP]
by (auto simp: finpref_def infsuff_def)


[STATEMENT]
lemma infsuff_finpref_iff [iff]:
  "\<lbrakk> r\<in>A\<^sup>\<star>; t\<in>A\<^sup>\<omega> \<rbrakk> \<Longrightarrow> (t \<in> finpref A r) = (r \<in> infsuff A t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> (t \<in> finpref A r) = (r \<in> infsuff A t)
[PROOF STEP]
by (auto simp: finpref_def infsuff_def)


[STATEMENT]
lemma prefix_lemma:
  assumes xinf: "x \<in> A\<^sup>\<omega>"
  and yinf: "y \<in> A\<^sup>\<omega>"
  and R: "\<And> s. \<lbrakk> s \<in> A\<^sup>\<star>; s \<le> x\<rbrakk> \<Longrightarrow> s \<le> y"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
let ?r = "\<lambda>x y. x\<in>A\<^sup>\<omega> \<and> y\<in>A\<^sup>\<omega> \<and> finpref A x \<subseteq> finpref A y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
have "?r x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A\<^sup>\<omega> \<and> y \<in> A\<^sup>\<omega> \<and> finpref A x \<subseteq> finpref A y
[PROOF STEP]
using xinf yinf
[PROOF STATE]
proof (prove)
using this:
x \<in> A\<^sup>\<omega>
y \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. x \<in> A\<^sup>\<omega> \<and> y \<in> A\<^sup>\<omega> \<and> finpref A x \<subseteq> finpref A y
[PROOF STEP]
by (auto simp: finpref_def intro: R)
[PROOF STATE]
proof (state)
this:
x \<in> A\<^sup>\<omega> \<and> y \<in> A\<^sup>\<omega> \<and> finpref A x \<subseteq> finpref A y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> A\<^sup>\<omega> \<and> y \<in> A\<^sup>\<omega> \<and> finpref A x \<subseteq> finpref A y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof (coinduct rule: llist.coinduct_strong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>llist llist'. llist \<in> A\<^sup>\<omega> \<and> llist' \<in> A\<^sup>\<omega> \<and> finpref A llist \<subseteq> finpref A llist' \<Longrightarrow> lnull llist = lnull llist' \<and> (\<not> lnull llist \<longrightarrow> \<not> lnull llist' \<longrightarrow> lhd llist = lhd llist' \<and> (ltl llist \<in> A\<^sup>\<omega> \<and> ltl llist' \<in> A\<^sup>\<omega> \<and> finpref A (ltl llist) \<subseteq> finpref A (ltl llist') \<or> ltl llist = ltl llist'))
[PROOF STEP]
case (Eq_llist a b)
[PROOF STATE]
proof (state)
this:
a \<in> A\<^sup>\<omega> \<and> b \<in> A\<^sup>\<omega> \<and> finpref A a \<subseteq> finpref A b

goal (1 subgoal):
 1. \<And>llist llist'. llist \<in> A\<^sup>\<omega> \<and> llist' \<in> A\<^sup>\<omega> \<and> finpref A llist \<subseteq> finpref A llist' \<Longrightarrow> lnull llist = lnull llist' \<and> (\<not> lnull llist \<longrightarrow> \<not> lnull llist' \<longrightarrow> lhd llist = lhd llist' \<and> (ltl llist \<in> A\<^sup>\<omega> \<and> ltl llist' \<in> A\<^sup>\<omega> \<and> finpref A (ltl llist) \<subseteq> finpref A (ltl llist') \<or> ltl llist = ltl llist'))
[PROOF STEP]
hence ainf: "a \<in> A\<^sup>\<omega>"
      and binf: "b \<in> A\<^sup>\<omega>" and pref: "finpref A a \<subseteq> finpref A b"
[PROOF STATE]
proof (prove)
using this:
a \<in> A\<^sup>\<omega> \<and> b \<in> A\<^sup>\<omega> \<and> finpref A a \<subseteq> finpref A b

goal (1 subgoal):
 1. a \<in> A\<^sup>\<omega> &&& b \<in> A\<^sup>\<omega> &&& finpref A a \<subseteq> finpref A b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> A\<^sup>\<omega>
b \<in> A\<^sup>\<omega>
finpref A a \<subseteq> finpref A b

goal (1 subgoal):
 1. \<And>llist llist'. llist \<in> A\<^sup>\<omega> \<and> llist' \<in> A\<^sup>\<omega> \<and> finpref A llist \<subseteq> finpref A llist' \<Longrightarrow> lnull llist = lnull llist' \<and> (\<not> lnull llist \<longrightarrow> \<not> lnull llist' \<longrightarrow> lhd llist = lhd llist' \<and> (ltl llist \<in> A\<^sup>\<omega> \<and> ltl llist' \<in> A\<^sup>\<omega> \<and> finpref A (ltl llist) \<subseteq> finpref A (ltl llist') \<or> ltl llist = ltl llist'))
[PROOF STEP]
from ainf
[PROOF STATE]
proof (chain)
picking this:
a \<in> A\<^sup>\<omega>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa l. \<lbrakk>l \<in> A\<^sup>\<omega>; aa \<in> A; a = aa ## l\<rbrakk> \<Longrightarrow> lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))
[PROOF STEP]
case (LCons a' l')
[PROOF STATE]
proof (state)
this:
l' \<in> A\<^sup>\<omega>
a' \<in> A
a = a' ## l'

goal (1 subgoal):
 1. \<And>aa l. \<lbrakk>l \<in> A\<^sup>\<omega>; aa \<in> A; a = aa ## l\<rbrakk> \<Longrightarrow> lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))
[PROOF STEP]
note acons = this
[PROOF STATE]
proof (state)
this:
l' \<in> A\<^sup>\<omega>
a' \<in> A
a = a' ## l'

goal (1 subgoal):
 1. \<And>aa l. \<lbrakk>l \<in> A\<^sup>\<omega>; aa \<in> A; a = aa ## l\<rbrakk> \<Longrightarrow> lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))
[PROOF STEP]
with binf
[PROOF STATE]
proof (chain)
picking this:
b \<in> A\<^sup>\<omega>
l' \<in> A\<^sup>\<omega>
a' \<in> A
a = a' ## l'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in> A\<^sup>\<omega>
l' \<in> A\<^sup>\<omega>
a' \<in> A
a = a' ## l'

goal (1 subgoal):
 1. lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))
[PROOF STEP]
proof (cases b)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa l. \<lbrakk>l' \<in> A\<^sup>\<omega>; a' \<in> A; a = a' ## l'; l \<in> A\<^sup>\<omega>; aa \<in> A; b = aa ## l\<rbrakk> \<Longrightarrow> lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))
[PROOF STEP]
case (LCons b' l'')
[PROOF STATE]
proof (state)
this:
l'' \<in> A\<^sup>\<omega>
b' \<in> A
b = b' ## l''

goal (1 subgoal):
 1. \<And>aa l. \<lbrakk>l' \<in> A\<^sup>\<omega>; a' \<in> A; a = a' ## l'; l \<in> A\<^sup>\<omega>; aa \<in> A; b = aa ## l\<rbrakk> \<Longrightarrow> lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))
[PROOF STEP]
with acons pref
[PROOF STATE]
proof (chain)
picking this:
l' \<in> A\<^sup>\<omega>
a' \<in> A
a = a' ## l'
finpref A a \<subseteq> finpref A b
l'' \<in> A\<^sup>\<omega>
b' \<in> A
b = b' ## l''
[PROOF STEP]
have "a' = b'" "finpref A l' \<subseteq> finpref A l''"
[PROOF STATE]
proof (prove)
using this:
l' \<in> A\<^sup>\<omega>
a' \<in> A
a = a' ## l'
finpref A a \<subseteq> finpref A b
l'' \<in> A\<^sup>\<omega>
b' \<in> A
b = b' ## l''

goal (1 subgoal):
 1. a' = b' &&& finpref A l' \<subseteq> finpref A l''
[PROOF STEP]
by (auto simp: finpref_def)
[PROOF STATE]
proof (state)
this:
a' = b'
finpref A l' \<subseteq> finpref A l''

goal (1 subgoal):
 1. \<And>aa l. \<lbrakk>l' \<in> A\<^sup>\<omega>; a' \<in> A; a = a' ## l'; l \<in> A\<^sup>\<omega>; aa \<in> A; b = aa ## l\<rbrakk> \<Longrightarrow> lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a' = b'
finpref A l' \<subseteq> finpref A l''

goal (1 subgoal):
 1. lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))
[PROOF STEP]
using acons LCons
[PROOF STATE]
proof (prove)
using this:
a' = b'
finpref A l' \<subseteq> finpref A l''
l' \<in> A\<^sup>\<omega>
a' \<in> A
a = a' ## l'
l'' \<in> A\<^sup>\<omega>
b' \<in> A
b = b' ## l''

goal (1 subgoal):
 1. lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lnull a = lnull b \<and> (\<not> lnull a \<longrightarrow> \<not> lnull b \<longrightarrow> lhd a = lhd b \<and> (ltl a \<in> A\<^sup>\<omega> \<and> ltl b \<in> A\<^sup>\<omega> \<and> finpref A (ltl a) \<subseteq> finpref A (ltl b) \<or> ltl a = ltl b))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_neqE:
"\<lbrakk> x \<in>  A\<^sup>\<omega>; y \<in> A\<^sup>\<omega>; x \<noteq> y;
  \<And>s. \<lbrakk> s\<in>A\<^sup>\<star>; s \<le> x; \<not> s \<le> y\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A\<^sup>\<omega>; y \<in> A\<^sup>\<omega>; x \<noteq> y; \<And>s. \<lbrakk>s \<in> A\<^sup>\<star>; s \<le> x; \<not> s \<le> y\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by (auto intro!: prefix_lemma)


[STATEMENT]
lemma pref_locally_linear:
  fixes s::"'a llist"
  assumes sx: "s \<le> x"
  and   tx: "t \<le> x"
  shows "s \<le> t \<or> t \<le> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<le> t \<or> t \<le> s
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<le> t \<or> t \<le> s
[PROOF STEP]
have "s \<in> UNIV\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> UNIV\<^sup>\<infinity>

goal (1 subgoal):
 1. s \<le> t \<or> t \<le> s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> UNIV\<^sup>\<infinity>

goal (1 subgoal):
 1. s \<le> t \<or> t \<le> s
[PROOF STEP]
proof (cases rule: alllstsE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<in> UNIV\<^sup>\<star> \<Longrightarrow> s \<le> t \<or> t \<le> s
 2. s \<in> UNIV\<^sup>\<omega> \<Longrightarrow> s \<le> t \<or> t \<le> s
[PROOF STEP]
case infinite
[PROOF STATE]
proof (state)
this:
s \<in> UNIV\<^sup>\<omega>

goal (2 subgoals):
 1. s \<in> UNIV\<^sup>\<star> \<Longrightarrow> s \<le> t \<or> t \<le> s
 2. s \<in> UNIV\<^sup>\<omega> \<Longrightarrow> s \<le> t \<or> t \<le> s
[PROOF STEP]
with sx tx
[PROOF STATE]
proof (chain)
picking this:
s \<le> x
t \<le> x
s \<in> UNIV\<^sup>\<omega>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<le> x
t \<le> x
s \<in> UNIV\<^sup>\<omega>

goal (1 subgoal):
 1. s \<le> t \<or> t \<le> s
[PROOF STEP]
by (auto simp: llist_inf_le)
[PROOF STATE]
proof (state)
this:
s \<le> t \<or> t \<le> s

goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<star> \<Longrightarrow> s \<le> t \<or> t \<le> s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<star> \<Longrightarrow> s \<le> t \<or> t \<le> s
[PROOF STEP]
case finite
[PROOF STATE]
proof (state)
this:
s \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<star> \<Longrightarrow> s \<le> t \<or> t \<le> s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. s \<le> t \<or> t \<le> s
[PROOF STEP]
using sx tx
[PROOF STATE]
proof (prove)
using this:
s \<in> UNIV\<^sup>\<star>
s \<le> x
t \<le> x

goal (1 subgoal):
 1. s \<le> t \<or> t \<le> s
[PROOF STEP]
proof (induct "s" arbitrary: x t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l x t. \<lbrakk>l = LNil; l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> l \<le> t \<or> t \<le> l
 2. \<And>a l x t. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<And>x t. \<lbrakk>l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> l \<le> t \<or> t \<le> l; a \<in> UNIV; a ## l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> a ## l \<le> t \<or> t \<le> a ## l
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
l_ = LNil
l_ \<le> x
t \<le> x

goal (2 subgoals):
 1. \<And>l x t. \<lbrakk>l = LNil; l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> l \<le> t \<or> t \<le> l
 2. \<And>a l x t. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<And>x t. \<lbrakk>l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> l \<le> t \<or> t \<le> l; a \<in> UNIV; a ## l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> a ## l \<le> t \<or> t \<le> a ## l
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l_ = LNil
l_ \<le> x
t \<le> x

goal (1 subgoal):
 1. l_ \<le> t \<or> t \<le> l_
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l_ \<le> t \<or> t \<le> l_

goal (1 subgoal):
 1. \<And>a l x t. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<And>x t. \<lbrakk>l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> l \<le> t \<or> t \<le> l; a \<in> UNIV; a ## l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> a ## l \<le> t \<or> t \<le> a ## l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l x t. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<And>x t. \<lbrakk>l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> l \<le> t \<or> t \<le> l; a \<in> UNIV; a ## l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> a ## l \<le> t \<or> t \<le> a ## l
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> UNIV\<^sup>\<star>
\<lbrakk>l \<le> ?x; ?t \<le> ?x\<rbrakk> \<Longrightarrow> l \<le> ?t \<or> ?t \<le> l
a \<in> UNIV
a ## l \<le> x
t \<le> x

goal (1 subgoal):
 1. \<And>a l x t. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<And>x t. \<lbrakk>l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> l \<le> t \<or> t \<le> l; a \<in> UNIV; a ## l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> a ## l \<le> t \<or> t \<le> a ## l
[PROOF STEP]
note alx = \<open>a ## l \<le> x\<close>
[PROOF STATE]
proof (state)
this:
a ## l \<le> x

goal (1 subgoal):
 1. \<And>a l x t. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<And>x t. \<lbrakk>l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> l \<le> t \<or> t \<le> l; a \<in> UNIV; a ## l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> a ## l \<le> t \<or> t \<le> a ## l
[PROOF STEP]
note tx = \<open>t \<le> x\<close>
[PROOF STATE]
proof (state)
this:
t \<le> x

goal (1 subgoal):
 1. \<And>a l x t. \<lbrakk>l \<in> UNIV\<^sup>\<star>; \<And>x t. \<lbrakk>l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> l \<le> t \<or> t \<le> l; a \<in> UNIV; a ## l \<le> x; t \<le> x\<rbrakk> \<Longrightarrow> a ## l \<le> t \<or> t \<le> a ## l
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ## l \<le> t \<or> t \<le> a ## l
[PROOF STEP]
proof(rule disjCI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> t \<le> a ## l \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
assume tal: "\<not> t \<le> a ## l"
[PROOF STATE]
proof (state)
this:
\<not> t \<le> a ## l

goal (1 subgoal):
 1. \<not> t \<le> a ## l \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
show "LCons a l \<le> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ## l \<le> t
[PROOF STEP]
proof (cases t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t = LNil \<Longrightarrow> a ## l \<le> t
 2. \<And>x21 x22. t = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
case LNil
[PROOF STATE]
proof (state)
this:
t = LNil

goal (2 subgoals):
 1. t = LNil \<Longrightarrow> a ## l \<le> t
 2. \<And>x21 x22. t = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = LNil

goal (1 subgoal):
 1. a ## l \<le> t
[PROOF STEP]
using tal
[PROOF STATE]
proof (prove)
using this:
t = LNil
\<not> t \<le> a ## l

goal (1 subgoal):
 1. a ## l \<le> t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a ## l \<le> t

goal (1 subgoal):
 1. \<And>x21 x22. t = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. t = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
case (LCons b ts)
[PROOF STATE]
proof (state)
this:
t = b ## ts

goal (1 subgoal):
 1. \<And>x21 x22. t = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
note tcons = this
[PROOF STATE]
proof (state)
this:
t = b ## ts

goal (1 subgoal):
 1. \<And>x21 x22. t = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ## l \<le> t
[PROOF STEP]
proof (cases x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = LNil \<Longrightarrow> a ## l \<le> t
 2. \<And>x21 x22. x = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
case LNil
[PROOF STATE]
proof (state)
this:
x = LNil

goal (2 subgoals):
 1. x = LNil \<Longrightarrow> a ## l \<le> t
 2. \<And>x21 x22. x = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = LNil

goal (1 subgoal):
 1. a ## l \<le> t
[PROOF STEP]
using alx
[PROOF STATE]
proof (prove)
using this:
x = LNil
a ## l \<le> x

goal (1 subgoal):
 1. a ## l \<le> t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a ## l \<le> t

goal (1 subgoal):
 1. \<And>x21 x22. x = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. x = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
case (LCons c xs)
[PROOF STATE]
proof (state)
this:
x = c ## xs

goal (1 subgoal):
 1. \<And>x21 x22. x = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
from alx  LCons
[PROOF STATE]
proof (chain)
picking this:
a ## l \<le> x
x = c ## xs
[PROOF STEP]
have ac: "a = c" and lxs: "l \<le> xs"
[PROOF STATE]
proof (prove)
using this:
a ## l \<le> x
x = c ## xs

goal (1 subgoal):
 1. a = c &&& l \<le> xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = c
l \<le> xs

goal (1 subgoal):
 1. \<And>x21 x22. x = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
from tx tcons LCons
[PROOF STATE]
proof (chain)
picking this:
t \<le> x
t = b ## ts
x = c ## xs
[PROOF STEP]
have bc: "b = c" and tsxs: "ts \<le> xs"
[PROOF STATE]
proof (prove)
using this:
t \<le> x
t = b ## ts
x = c ## xs

goal (1 subgoal):
 1. b = c &&& ts \<le> xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b = c
ts \<le> xs

goal (1 subgoal):
 1. \<And>x21 x22. x = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
from tcons tal ac bc
[PROOF STATE]
proof (chain)
picking this:
t = b ## ts
\<not> t \<le> a ## l
a = c
b = c
[PROOF STEP]
have tsl: "\<not> ts \<le> l"
[PROOF STATE]
proof (prove)
using this:
t = b ## ts
\<not> t \<le> a ## l
a = c
b = c

goal (1 subgoal):
 1. \<not> ts \<le> l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> ts \<le> l

goal (1 subgoal):
 1. \<And>x21 x22. x = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
from LCons_fin lxs tsxs tsl
[PROOF STATE]
proof (chain)
picking this:
l \<in> UNIV\<^sup>\<star>
\<lbrakk>l \<le> ?x; ?t \<le> ?x\<rbrakk> \<Longrightarrow> l \<le> ?t \<or> ?t \<le> l
a \<in> UNIV
a ## l \<le> x
t \<le> x
l \<le> xs
ts \<le> xs
\<not> ts \<le> l
[PROOF STEP]
have "l \<le> ts"
[PROOF STATE]
proof (prove)
using this:
l \<in> UNIV\<^sup>\<star>
\<lbrakk>l \<le> ?x; ?t \<le> ?x\<rbrakk> \<Longrightarrow> l \<le> ?t \<or> ?t \<le> l
a \<in> UNIV
a ## l \<le> x
t \<le> x
l \<le> xs
ts \<le> xs
\<not> ts \<le> l

goal (1 subgoal):
 1. l \<le> ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<le> ts

goal (1 subgoal):
 1. \<And>x21 x22. x = x21 ## x22 \<Longrightarrow> a ## l \<le> t
[PROOF STEP]
with tcons ac bc
[PROOF STATE]
proof (chain)
picking this:
t = b ## ts
a = c
b = c
l \<le> ts
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = b ## ts
a = c
b = c
l \<le> ts

goal (1 subgoal):
 1. a ## l \<le> t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a ## l \<le> t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a ## l \<le> t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a ## l \<le> t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a ## l \<le> t \<or> t \<le> a ## l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s \<le> t \<or> t \<le> s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s \<le> t \<or> t \<le> s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pfinpref_iff [iff]:
  "(x \<in> pfinpref A s) = (x \<in> finpref A s \<and> x \<noteq> LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> pfinpref A s) = (x \<in> finpref A s \<and> x \<noteq> LNil)
[PROOF STEP]
by (auto simp: pfinpref_def)


[STATEMENT]
lemma safetyI:
  "(\<And>t. \<lbrakk>t \<in>  A\<^sup>\<infinity>; \<forall> r \<in> finpref A t. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P\<rbrakk> \<Longrightarrow> t \<in> P)
  \<Longrightarrow> safety A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> A\<^sup>\<infinity>; \<forall>r\<in>finpref A t. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P\<rbrakk> \<Longrightarrow> t \<in> P) \<Longrightarrow> safety A P
[PROOF STEP]
by (unfold safety_def) blast


[STATEMENT]
lemma safetyD:
  "\<lbrakk> safety A P;  t \<in> A\<^sup>\<infinity>;
    \<And>r. r \<in> finpref A t \<Longrightarrow> \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P
  \<rbrakk> \<Longrightarrow> t \<in> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safety A P; t \<in> A\<^sup>\<infinity>; \<And>r. r \<in> finpref A t \<Longrightarrow> \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P\<rbrakk> \<Longrightarrow> t \<in> P
[PROOF STEP]
by (unfold safety_def) blast


[STATEMENT]
lemma safetyE:
  "\<lbrakk> safety A P;
    \<forall> t \<in> A\<^sup>\<infinity>. (\<forall> r \<in> finpref A t. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P) \<longrightarrow> t \<in> P \<Longrightarrow> R
   \<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safety A P; \<forall>t\<in>A\<^sup>\<infinity>. (\<forall>r\<in>finpref A t. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) \<longrightarrow> t \<in> P \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by (unfold safety_def) blast


[STATEMENT]
lemma safety_prefix_closed:
  "safety UNIV P \<Longrightarrow> prefix_closed P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. safety UNIV P \<Longrightarrow> prefix_closed P
[PROOF STEP]
by (auto dest!: safetyD
       simp: prefix_closed_def finpref_def llist_le_def lappend_assoc)
    blast


[STATEMENT]
lemma livenessI:
  "(\<And>s. s\<in> A\<^sup>\<star> \<Longrightarrow> \<exists> t \<in> A\<^sup>\<infinity>. s @@ t \<in> P) \<Longrightarrow> liveness A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. s \<in> A\<^sup>\<star> \<Longrightarrow> \<exists>t\<in>A\<^sup>\<infinity>. s @@ t \<in> P) \<Longrightarrow> liveness A P
[PROOF STEP]
by (auto simp: liveness_def)


[STATEMENT]
lemma livenessE:
  "\<lbrakk> liveness A P; \<And>t. \<lbrakk>  t \<in> A\<^sup>\<infinity>; s @@ t \<in> P\<rbrakk> \<Longrightarrow> R; s \<notin> A\<^sup>\<star> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>liveness A P; \<And>t. \<lbrakk>t \<in> A\<^sup>\<infinity>; s @@ t \<in> P\<rbrakk> \<Longrightarrow> R; s \<notin> A\<^sup>\<star> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by (auto simp: liveness_def)


[STATEMENT]
lemma possafetyI:
  "(\<And>t. \<lbrakk>t \<in>  A\<^sup>\<spadesuit>; \<forall> r \<in> pfinpref A t. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P\<rbrakk> \<Longrightarrow> t \<in> P)
  \<Longrightarrow> possafety A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> A\<^sup>\<spadesuit>; \<forall>r\<in>pfinpref A t. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P\<rbrakk> \<Longrightarrow> t \<in> P) \<Longrightarrow> possafety A P
[PROOF STEP]
by (unfold possafety_def) blast


[STATEMENT]
lemma possafetyD:
  "\<lbrakk> possafety A P;  t \<in> A\<^sup>\<spadesuit>;
    \<And>r. r \<in> pfinpref A t \<Longrightarrow> \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P
  \<rbrakk> \<Longrightarrow> t \<in> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>possafety A P; t \<in> A\<^sup>\<spadesuit>; \<And>r. r \<in> pfinpref A t \<Longrightarrow> \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P\<rbrakk> \<Longrightarrow> t \<in> P
[PROOF STEP]
by (unfold possafety_def) blast


[STATEMENT]
lemma possafetyE:
  "\<lbrakk> possafety A P;
    \<forall> t \<in> A\<^sup>\<spadesuit>. (\<forall> r \<in> pfinpref A t. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P) \<longrightarrow> t \<in> P \<Longrightarrow> R
   \<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>possafety A P; \<forall>t\<in>A\<^sup>\<spadesuit>. (\<forall>r\<in>pfinpref A t. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) \<longrightarrow> t \<in> P \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by (unfold possafety_def) blast


[STATEMENT]
lemma possafety_pprefix_closed:
  assumes psafety: "possafety UNIV P"
  shows "pprefix_closed P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pprefix_closed P
[PROOF STEP]
unfolding pprefix_closed_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>P. \<forall>s. s \<le> t \<and> s \<noteq> LNil \<longrightarrow> s \<in> P
[PROOF STEP]
proof(intro ballI allI impI, erule conjE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t s. \<lbrakk>t \<in> P; s \<le> t; s \<noteq> LNil\<rbrakk> \<Longrightarrow> s \<in> P
[PROOF STEP]
fix t s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t s. \<lbrakk>t \<in> P; s \<le> t; s \<noteq> LNil\<rbrakk> \<Longrightarrow> s \<in> P
[PROOF STEP]
assume tP: "t \<in> P" and st: "s \<le> t" and spos: "s \<noteq> LNil"
[PROOF STATE]
proof (state)
this:
t \<in> P
s \<le> t
s \<noteq> LNil

goal (1 subgoal):
 1. \<And>t s. \<lbrakk>t \<in> P; s \<le> t; s \<noteq> LNil\<rbrakk> \<Longrightarrow> s \<in> P
[PROOF STEP]
from psafety
[PROOF STATE]
proof (chain)
picking this:
possafety UNIV P
[PROOF STEP]
show "s \<in> P"
[PROOF STATE]
proof (prove)
using this:
possafety UNIV P

goal (1 subgoal):
 1. s \<in> P
[PROOF STEP]
proof (rule possafetyD)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<in> UNIV\<^sup>\<spadesuit>
 2. \<And>r. r \<in> pfinpref UNIV s \<Longrightarrow> \<exists>s\<in>UNIV\<^sup>\<infinity>. r @@ s \<in> P
[PROOF STEP]
from spos
[PROOF STATE]
proof (chain)
picking this:
s \<noteq> LNil
[PROOF STEP]
show  "s \<in> UNIV\<^sup>\<spadesuit>"
[PROOF STATE]
proof (prove)
using this:
s \<noteq> LNil

goal (1 subgoal):
 1. s \<in> UNIV\<^sup>\<spadesuit>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> UNIV\<^sup>\<spadesuit>

goal (1 subgoal):
 1. \<And>r. r \<in> pfinpref UNIV s \<Longrightarrow> \<exists>s\<in>UNIV\<^sup>\<infinity>. r @@ s \<in> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. r \<in> pfinpref UNIV s \<Longrightarrow> \<exists>s\<in>UNIV\<^sup>\<infinity>. r @@ s \<in> P
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. r \<in> pfinpref UNIV s \<Longrightarrow> \<exists>s\<in>UNIV\<^sup>\<infinity>. r @@ s \<in> P
[PROOF STEP]
assume "r \<in> pfinpref UNIV s"
[PROOF STATE]
proof (state)
this:
r \<in> pfinpref UNIV s

goal (1 subgoal):
 1. \<And>r. r \<in> pfinpref UNIV s \<Longrightarrow> \<exists>s\<in>UNIV\<^sup>\<infinity>. r @@ s \<in> P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> pfinpref UNIV s
[PROOF STEP]
obtain u where scons: "s = r @@ u"
[PROOF STATE]
proof (prove)
using this:
r \<in> pfinpref UNIV s

goal (1 subgoal):
 1. (\<And>u. s = r @@ u \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: pfinpref_def finpref_def llist_le_def)
[PROOF STATE]
proof (state)
this:
s = r @@ u

goal (1 subgoal):
 1. \<And>r. r \<in> pfinpref UNIV s \<Longrightarrow> \<exists>s\<in>UNIV\<^sup>\<infinity>. r @@ s \<in> P
[PROOF STEP]
with st
[PROOF STATE]
proof (chain)
picking this:
s \<le> t
s = r @@ u
[PROOF STEP]
obtain v where "t = r @@ u @@ v"
[PROOF STATE]
proof (prove)
using this:
s \<le> t
s = r @@ u

goal (1 subgoal):
 1. (\<And>v. t = r @@ u @@ v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: lappend_assoc llist_le_def)
[PROOF STATE]
proof (state)
this:
t = r @@ u @@ v

goal (1 subgoal):
 1. \<And>r. r \<in> pfinpref UNIV s \<Longrightarrow> \<exists>s\<in>UNIV\<^sup>\<infinity>. r @@ s \<in> P
[PROOF STEP]
with tP
[PROOF STATE]
proof (chain)
picking this:
t \<in> P
t = r @@ u @@ v
[PROOF STEP]
show "\<exists>s\<in>UNIV\<^sup>\<infinity>. r @@ s \<in> P"
[PROOF STATE]
proof (prove)
using this:
t \<in> P
t = r @@ u @@ v

goal (1 subgoal):
 1. \<exists>s\<in>UNIV\<^sup>\<infinity>. r @@ s \<in> P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s\<in>UNIV\<^sup>\<infinity>. r @@ s \<in> P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s \<in> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poslivenessI:
  "(\<And>s. s\<in> A\<^sup>\<clubsuit> \<Longrightarrow> \<exists> t \<in> A\<^sup>\<infinity>. s @@ t \<in> P) \<Longrightarrow> posliveness A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. s \<in> A\<^sup>\<clubsuit> \<Longrightarrow> \<exists>t\<in>A\<^sup>\<infinity>. s @@ t \<in> P) \<Longrightarrow> posliveness A P
[PROOF STEP]
by (auto simp: posliveness_def)


[STATEMENT]
lemma poslivenessE:
  "\<lbrakk> posliveness A P; \<And>t. \<lbrakk>  t \<in> A\<^sup>\<infinity>; s @@ t \<in> P\<rbrakk> \<Longrightarrow> R; s \<notin> A\<^sup>\<clubsuit> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>posliveness A P; \<And>t. \<lbrakk>t \<in> A\<^sup>\<infinity>; s @@ t \<in> P\<rbrakk> \<Longrightarrow> R; s \<notin> A\<^sup>\<clubsuit> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by (auto simp: posliveness_def)


[STATEMENT]
lemma cat_GRPH_components:
  shows "cat_GRPH \<alpha>\<lparr>Obj\<rparr> = set {\<CC>. digraph \<alpha> \<CC>}"
    and "cat_GRPH \<alpha>\<lparr>Arr\<rparr> = all_dghms \<alpha>"
    and "cat_GRPH \<alpha>\<lparr>Dom\<rparr> = (\<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>)"
    and "cat_GRPH \<alpha>\<lparr>Cod\<rparr> = (\<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>)"
    and "cat_GRPH \<alpha>\<lparr>Comp\<rparr> =
      (\<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>0\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>)"
    and "cat_GRPH \<alpha>\<lparr>CId\<rparr> = (\<lambda>\<CC>\<in>\<^sub>\<circ>set {\<CC>. digraph \<alpha> \<CC>}. dghm_id \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cat_GRPH \<alpha>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {\<CC>. digraph \<alpha> \<CC>} &&& cat_GRPH \<alpha>\<lparr>Arr\<rparr> = all_dghms \<alpha> &&& cat_GRPH \<alpha>\<lparr>Dom\<rparr> = (\<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>)) &&& cat_GRPH \<alpha>\<lparr>Cod\<rparr> = (\<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>) &&& cat_GRPH \<alpha>\<lparr>Comp\<rparr> = (\<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>) &&& cat_GRPH \<alpha>\<lparr>CId\<rparr> = VLambda (ZFC_in_HOL.set {\<CC>. digraph \<alpha> \<CC>}) dghm_id
[PROOF STEP]
unfolding cat_GRPH_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([ZFC_in_HOL.set (Collect (digraph \<alpha>)), all_dghms \<alpha>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>, \<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = ZFC_in_HOL.set {\<CC>. digraph \<alpha> \<CC>} &&& [ZFC_in_HOL.set (Collect (digraph \<alpha>)), all_dghms \<alpha>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>, \<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = all_dghms \<alpha> &&& [ZFC_in_HOL.set (Collect (digraph \<alpha>)), all_dghms \<alpha>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>, \<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = (\<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>)) &&& [ZFC_in_HOL.set (Collect (digraph \<alpha>)), all_dghms \<alpha>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>, \<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = (\<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>) &&& [ZFC_in_HOL.set (Collect (digraph \<alpha>)), all_dghms \<alpha>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>, \<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = (\<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>) &&& [ZFC_in_HOL.set (Collect (digraph \<alpha>)), all_dghms \<alpha>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>, \<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id]\<^sub>\<circ>\<lparr>5\<^sub>\<nat>\<rparr> = VLambda (ZFC_in_HOL.set {\<CC>. digraph \<alpha> \<CC>}) dghm_id
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma cat_smc_GRPH: "cat_smc (cat_GRPH \<alpha>) = smc_GRPH \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_smc (cat_GRPH \<alpha>) = smc_GRPH \<alpha>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (cat_smc (cat_GRPH \<alpha>))
 2. vsv (smc_GRPH \<alpha>)
 3. \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) = \<D>\<^sub>\<circ> (smc_GRPH \<alpha>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) \<Longrightarrow> cat_smc (cat_GRPH \<alpha>)\<lparr>a\<rparr> = smc_GRPH \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) = 5\<^sub>\<nat>
[PROOF STEP]
unfolding cat_smc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [cat_GRPH \<alpha>\<lparr>Obj\<rparr>, cat_GRPH \<alpha>\<lparr>Arr\<rparr>, cat_GRPH \<alpha>\<lparr>Dom\<rparr>, cat_GRPH \<alpha>\<lparr>Cod\<rparr>, cat_GRPH \<alpha>\<lparr>Comp\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) = 5\<^sub>\<nat>

goal (4 subgoals):
 1. vsv (cat_smc (cat_GRPH \<alpha>))
 2. vsv (smc_GRPH \<alpha>)
 3. \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) = \<D>\<^sub>\<circ> (smc_GRPH \<alpha>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) \<Longrightarrow> cat_smc (cat_GRPH \<alpha>)\<lparr>a\<rparr> = smc_GRPH \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
have dom_rhs: "\<D>\<^sub>\<circ> (smc_GRPH \<alpha>) = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (smc_GRPH \<alpha>) = 5\<^sub>\<nat>
[PROOF STEP]
unfolding smc_GRPH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [ZFC_in_HOL.set (Collect (digraph \<alpha>)), all_dghms \<alpha>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>, \<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (smc_GRPH \<alpha>) = 5\<^sub>\<nat>

goal (4 subgoals):
 1. vsv (cat_smc (cat_GRPH \<alpha>))
 2. vsv (smc_GRPH \<alpha>)
 3. \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) = \<D>\<^sub>\<circ> (smc_GRPH \<alpha>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) \<Longrightarrow> cat_smc (cat_GRPH \<alpha>)\<lparr>a\<rparr> = smc_GRPH \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) = \<D>\<^sub>\<circ> (smc_GRPH \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) = \<D>\<^sub>\<circ> (smc_GRPH \<alpha>)
[PROOF STEP]
unfolding dom_lhs dom_rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5\<^sub>\<nat> = 5\<^sub>\<nat>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) = \<D>\<^sub>\<circ> (smc_GRPH \<alpha>)

goal (3 subgoals):
 1. vsv (cat_smc (cat_GRPH \<alpha>))
 2. vsv (smc_GRPH \<alpha>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) \<Longrightarrow> cat_smc (cat_GRPH \<alpha>)\<lparr>a\<rparr> = smc_GRPH \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
show
    "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) \<Longrightarrow> cat_smc (cat_GRPH \<alpha>)\<lparr>a\<rparr> = smc_GRPH \<alpha>\<lparr>a\<rparr>"
    for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) \<Longrightarrow> cat_smc (cat_GRPH \<alpha>)\<lparr>a\<rparr> = smc_GRPH \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
by
      (
        unfold dom_lhs,
        elim_in_numeral,
        unfold cat_smc_def dg_field_simps cat_GRPH_def smc_GRPH_def
      )
      (auto simp: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_GRPH \<alpha>)) \<Longrightarrow> cat_smc (cat_GRPH \<alpha>)\<lparr>?a\<rparr> = smc_GRPH \<alpha>\<lparr>?a\<rparr>

goal (2 subgoals):
 1. vsv (cat_smc (cat_GRPH \<alpha>))
 2. vsv (smc_GRPH \<alpha>)
[PROOF STEP]
qed (auto simp: cat_smc_def smc_GRPH_def)


[STATEMENT]
lemma cat_GRPH_CId_app[cat_GRPH_simps]:
  assumes "digraph \<alpha> \<CC>"
  shows "cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<CC>\<rparr> = dghm_id \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<CC>\<rparr> = dghm_id \<CC>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<CC>

goal (1 subgoal):
 1. cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<CC>\<rparr> = dghm_id \<CC>
[PROOF STEP]
unfolding cat_GRPH_components
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<CC>

goal (1 subgoal):
 1. VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id\<lparr>\<CC>\<rparr> = dghm_id \<CC>
[PROOF STEP]
by simp


[STATEMENT]
lemma cat_GRPH_CId_vdomain: "\<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) = set {\<CC>. digraph \<alpha> \<CC>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) = ZFC_in_HOL.set {\<CC>. digraph \<alpha> \<CC>}
[PROOF STEP]
unfolding cat_GRPH_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id) = ZFC_in_HOL.set {\<CC>. digraph \<alpha> \<CC>}
[PROOF STEP]
by auto


[STATEMENT]
lemma cat_GRPH_CId_vrange: "\<R>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) \<subseteq>\<^sub>\<circ> all_dghms \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) \<subseteq>\<^sub>\<circ> all_dghms \<alpha>
[PROOF STEP]
proof(rule vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> all_dghms \<alpha>
[PROOF STEP]
fix \<HH>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> all_dghms \<alpha>
[PROOF STEP]
assume "\<HH> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>)"
[PROOF STATE]
proof (state)
this:
\<HH> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> all_dghms \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<HH> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>)
[PROOF STEP]
obtain \<AA>
    where \<HH>_def: "\<HH> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>" and \<AA>: "\<AA> \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<HH> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>)

goal (1 subgoal):
 1. (\<And>\<AA>. \<lbrakk>\<HH> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>; \<AA> \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding cat_GRPH_components
[PROOF STATE]
proof (prove)
using this:
\<HH> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id)

goal (1 subgoal):
 1. (\<And>\<AA>. \<lbrakk>\<HH> = VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id\<lparr>\<AA>\<rparr>; \<AA> \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<HH> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
\<AA> \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> all_dghms \<alpha>
[PROOF STEP]
from \<AA>
[PROOF STATE]
proof (chain)
picking this:
\<AA> \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>)
[PROOF STEP]
have \<HH>_def': "\<HH> = dghm_id \<AA>"
[PROOF STATE]
proof (prove)
using this:
\<AA> \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>)

goal (1 subgoal):
 1. \<HH> = dghm_id \<AA>
[PROOF STEP]
unfolding \<HH>_def cat_GRPH_CId_vdomain
[PROOF STATE]
proof (prove)
using this:
\<AA> \<in>\<^sub>\<circ> ZFC_in_HOL.set (Collect (digraph \<alpha>))

goal (1 subgoal):
 1. cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr> = dghm_id \<AA>
[PROOF STEP]
by (auto simp: cat_GRPH_CId_app)
[PROOF STATE]
proof (state)
this:
\<HH> = dghm_id \<AA>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> all_dghms \<alpha>
[PROOF STEP]
from \<AA> digraph.dg_dghm_id_is_dghm
[PROOF STATE]
proof (chain)
picking this:
\<AA> \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>)
digraph ?\<alpha> ?\<CC> \<Longrightarrow> dghm_id ?\<CC> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<CC>
[PROOF STEP]
show "\<HH> \<in>\<^sub>\<circ> all_dghms \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<AA> \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>)
digraph ?\<alpha> ?\<CC> \<Longrightarrow> dghm_id ?\<CC> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<CC>

goal (1 subgoal):
 1. \<HH> \<in>\<^sub>\<circ> all_dghms \<alpha>
[PROOF STEP]
unfolding \<HH>_def' cat_GRPH_CId_vdomain
[PROOF STATE]
proof (prove)
using this:
\<AA> \<in>\<^sub>\<circ> ZFC_in_HOL.set (Collect (digraph \<alpha>))
digraph ?\<alpha> ?\<CC> \<Longrightarrow> dghm_id ?\<CC> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<CC>

goal (1 subgoal):
 1. dghm_id \<AA> \<in>\<^sub>\<circ> all_dghms \<alpha>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<HH> \<in>\<^sub>\<circ> all_dghms \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in \<Z>) tiny_category_cat_GRPH:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "tiny_category \<beta> (cat_GRPH \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tiny_category \<beta> (cat_GRPH \<alpha>)
[PROOF STEP]
proof(intro tiny_categoryI)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<Z> \<beta>
 2. vfsequence (cat_GRPH \<alpha>)
 3. vsv (cat_GRPH \<alpha>\<lparr>CId\<rparr>)
 4. vcard (cat_GRPH \<alpha>) = 6\<^sub>\<nat>
 5. tiny_semicategory \<beta> (cat_smc (cat_GRPH \<alpha>))
 6. \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) = cat_GRPH \<alpha>\<lparr>Obj\<rparr>
 7. \<And>a. a \<in>\<^sub>\<circ> cat_GRPH \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> a
 8. \<And>a b f. f : a \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> b \<Longrightarrow> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> f = f
 9. \<And>b c f. f : b \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
interpret \<beta>: \<Z> \<beta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> \<beta>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<Z> \<beta>
 2. vfsequence (cat_GRPH \<alpha>)
 3. vsv (cat_GRPH \<alpha>\<lparr>CId\<rparr>)
 4. vcard (cat_GRPH \<alpha>) = 6\<^sub>\<nat>
 5. tiny_semicategory \<beta> (cat_smc (cat_GRPH \<alpha>))
 6. \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) = cat_GRPH \<alpha>\<lparr>Obj\<rparr>
 7. \<And>a. a \<in>\<^sub>\<circ> cat_GRPH \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> a
 8. \<And>a b f. f : a \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> b \<Longrightarrow> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> f = f
 9. \<And>b c f. f : b \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "vfsequence (cat_GRPH \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (cat_GRPH \<alpha>)
[PROOF STEP]
unfolding cat_GRPH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [ZFC_in_HOL.set (Collect (digraph \<alpha>)), all_dghms \<alpha>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>, \<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (cat_GRPH \<alpha>)

goal (8 subgoals):
 1. \<Z> \<beta>
 2. vsv (cat_GRPH \<alpha>\<lparr>CId\<rparr>)
 3. vcard (cat_GRPH \<alpha>) = 6\<^sub>\<nat>
 4. tiny_semicategory \<beta> (cat_smc (cat_GRPH \<alpha>))
 5. \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) = cat_GRPH \<alpha>\<lparr>Obj\<rparr>
 6. \<And>a. a \<in>\<^sub>\<circ> cat_GRPH \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> a
 7. \<And>a b f. f : a \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> b \<Longrightarrow> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> f = f
 8. \<And>b c f. f : b \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "vcard (cat_GRPH \<alpha>) = 6\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (cat_GRPH \<alpha>) = 6\<^sub>\<nat>
[PROOF STEP]
unfolding cat_GRPH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [ZFC_in_HOL.set (Collect (digraph \<alpha>)), all_dghms \<alpha>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomDom\<rparr>, \<lambda>\<FF>\<in>\<^sub>\<circ>all_dghms \<alpha>. \<FF>\<lparr>HomCod\<rparr>, \<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (dg_GRPH \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (ZFC_in_HOL.set (Collect (digraph \<alpha>))) dghm_id]\<^sub>\<circ> = 6\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (cat_GRPH \<alpha>) = 6\<^sub>\<nat>

goal (7 subgoals):
 1. \<Z> \<beta>
 2. vsv (cat_GRPH \<alpha>\<lparr>CId\<rparr>)
 3. tiny_semicategory \<beta> (cat_smc (cat_GRPH \<alpha>))
 4. \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) = cat_GRPH \<alpha>\<lparr>Obj\<rparr>
 5. \<And>a. a \<in>\<^sub>\<circ> cat_GRPH \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> a
 6. \<And>a b f. f : a \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> b \<Longrightarrow> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> f = f
 7. \<And>b c f. f : b \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = \<FF>"
    if "\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>" for \<FF> \<AA> \<BB>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = \<FF>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = \<FF>
[PROOF STEP]
unfolding cat_GRPH_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = \<FF>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cat_GRPH_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
?\<FF> : ?\<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> ?\<BB> \<Longrightarrow> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>?\<BB>\<rparr> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> ?\<FF> = ?\<FF>

goal (6 subgoals):
 1. \<Z> \<beta>
 2. vsv (cat_GRPH \<alpha>\<lparr>CId\<rparr>)
 3. tiny_semicategory \<beta> (cat_smc (cat_GRPH \<alpha>))
 4. \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) = cat_GRPH \<alpha>\<lparr>Obj\<rparr>
 5. \<And>a. a \<in>\<^sub>\<circ> cat_GRPH \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> a
 6. \<And>b c f. f : b \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "\<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr> = \<FF>"
    if "\<FF> : \<BB> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<CC>" for \<FF> \<BB> \<CC>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr> = \<FF>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<BB> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr> = \<FF>
[PROOF STEP]
unfolding cat_GRPH_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr> = \<FF>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cat_GRPH_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
?\<FF> : ?\<BB> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> ?\<CC> \<Longrightarrow> ?\<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>?\<BB>\<rparr> = ?\<FF>

goal (5 subgoals):
 1. \<Z> \<beta>
 2. vsv (cat_GRPH \<alpha>\<lparr>CId\<rparr>)
 3. tiny_semicategory \<beta> (cat_smc (cat_GRPH \<alpha>))
 4. \<D>\<^sub>\<circ> (cat_GRPH \<alpha>\<lparr>CId\<rparr>) = cat_GRPH \<alpha>\<lparr>Obj\<rparr>
 5. \<And>a. a \<in>\<^sub>\<circ> cat_GRPH \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> a
[PROOF STEP]
qed
  (
    simp_all add:
      assms
      cat_smc_GRPH
      cat_GRPH_components
      digraph.dg_dghm_id_is_dghm
      cat_GRPH_is_arr_iff
      tiny_semicategory_smc_GRPH
  )


[STATEMENT]
lemma cat_GRPH_is_iso_arrI:
  assumes "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
[PROOF STEP]
proof(intro is_iso_arrI is_inverseI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
 2. ?g : ?b1 \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> ?a1
 3. \<FF> : ?a1 \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> ?b1
 4. ?g \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>?a1\<rparr>
 5. \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> ?g = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>?b1\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
show \<FF>: "\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
[PROOF STEP]
unfolding cat_GRPH_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>

goal (4 subgoals):
 1. ?g : ?b1 \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> ?a1
 2. \<FF> : ?a1 \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> ?b1
 3. ?g \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>?a1\<rparr>
 4. \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> ?g = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>?b1\<rparr>
[PROOF STEP]
note iso_thms = is_iso_dghm_is_iso_arr[OF assms]
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>

goal (4 subgoals):
 1. ?g : ?b1 \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> ?a1
 2. \<FF> : ?a1 \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> ?b1
 3. ?g \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>?a1\<rparr>
 4. \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> ?g = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>?b1\<rparr>
[PROOF STEP]
from iso_thms(1)
[PROOF STATE]
proof (chain)
picking this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show inv_\<FF>: "inv_dghm \<FF> : \<BB> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<AA>
[PROOF STEP]
unfolding cat_GRPH_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> : \<BB> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<AA>

goal (3 subgoals):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
 2. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
 3. \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> inv_dghm \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
show "\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
[PROOF STEP]
unfolding cat_GRPH_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>

goal (2 subgoals):
 1. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
 2. \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> inv_dghm \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have \<AA>: "digraph \<alpha> \<AA>" and \<BB>: "digraph \<alpha> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. digraph \<alpha> \<AA> &&& digraph \<alpha> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (2 subgoals):
 1. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
 2. \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> inv_dghm \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
show "inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
[PROOF STEP]
unfolding cat_GRPH_CId_app[OF \<AA>] cat_GRPH_Comp_app[OF inv_\<FF> \<FF>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
[PROOF STEP]
by (rule iso_thms(2))
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>

goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> inv_dghm \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
show "\<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> inv_dghm \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> inv_dghm \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
unfolding cat_GRPH_CId_app[OF \<BB>] cat_GRPH_Comp_app[OF \<FF> inv_\<FF>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
by (rule iso_thms(3))
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> inv_dghm \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed