[STATEMENT]
lemma seqI [simp]:
    assumes "arr f" and "arr g" and "dom g = cod f"
    shows "seq g f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seq g f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. seq g f
[PROOF STEP]
have "ide (cod f) \<and> seq (cod f) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (cod f) \<and> seq (cod f) f
[PROOF STEP]
using assms(1) has_codomain_iff_arr codomains_def cod_in_codomains ext
[PROOF STATE]
proof (prove)
using this:
arr f
(codomains ?f \<noteq> {}) = arr ?f
codomains ?f \<equiv> {b. ide b \<and> b \<cdot> ?f \<noteq> null}
codomains ?f \<noteq> {} \<Longrightarrow> cod ?f \<in> codomains ?f
?g \<cdot> ?f \<noteq> null \<Longrightarrow> seq ?g ?f

goal (1 subgoal):
 1. ide (cod f) \<and> seq (cod f) f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ide (cod f) \<and> seq (cod f) f

goal (1 subgoal):
 1. seq g f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ide (cod f) \<and> seq (cod f) f

goal (1 subgoal):
 1. seq g f
[PROOF STEP]
have "ide (cod f) \<and> seq g (cod f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (cod f) \<and> seq g (cod f)
[PROOF STEP]
using assms(2-3) domains_def domains_simp ext
[PROOF STATE]
proof (prove)
using this:
arr g
local.dom g = cod f
domains ?f \<equiv> {a. ide a \<and> ?f \<cdot> a \<noteq> null}
arr ?f \<Longrightarrow> domains ?f = {local.dom ?f}
?g \<cdot> ?f \<noteq> null \<Longrightarrow> seq ?g ?f

goal (1 subgoal):
 1. ide (cod f) \<and> seq g (cod f)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ide (cod f) \<and> seq g (cod f)

goal (1 subgoal):
 1. seq g f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ide (cod f) \<and> seq (cod f) f
ide (cod f) \<and> seq g (cod f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ide (cod f) \<and> seq (cod f) f
ide (cod f) \<and> seq g (cod f)

goal (1 subgoal):
 1. seq g f
[PROOF STEP]
using match_4 ide_def ext
[PROOF STATE]
proof (prove)
using this:
ide (cod f) \<and> seq (cod f) f
ide (cod f) \<and> seq g (cod f)
\<lbrakk>seq ?g ?f; seq ?h ?g\<rbrakk> \<Longrightarrow> seq ?h (?g \<cdot> ?f)
ide ?a \<equiv> ?a \<cdot> ?a \<noteq> null \<and> (\<forall>f. (f \<cdot> ?a \<noteq> null \<longrightarrow> f \<cdot> ?a = f) \<and> (?a \<cdot> f \<noteq> null \<longrightarrow> ?a \<cdot> f = f))
?g \<cdot> ?f \<noteq> null \<Longrightarrow> seq ?g ?f

goal (1 subgoal):
 1. seq g f
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
seq g f

goal:
No subgoals!
[PROOF STEP]
qed