[STATEMENT]
lemma the_cat_scospan_Comp_app_\<ff>\<bb>[cat_ss_cs_simps]:
  assumes "g = \<ff>\<^sub>S\<^sub>S" and "f = \<bb>\<^sub>S\<^sub>S"
  shows "g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
g = \<ff>\<^sub>S\<^sub>S
f = \<bb>\<^sub>S\<^sub>S
[PROOF STEP]
have "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable"
[PROOF STATE]
proof (prove)
using this:
g = \<ff>\<^sub>S\<^sub>S
f = \<bb>\<^sub>S\<^sub>S

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable
[PROOF STEP]
show "g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g
[PROOF STEP]
unfolding the_cat_scospan_components(5) assms
[PROOF STATE]
proof (prove)
using this:
[\<ff>\<^sub>S\<^sub>S, \<bb>\<^sub>S\<^sub>S]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable

goal (1 subgoal):
 1. (\<lambda>gf\<in>\<^sub>\<circ>cat_scospan_composable. if gf = [\<oo>\<^sub>S\<^sub>S, \<gg>\<^sub>S\<^sub>S]\<^sub>\<circ> \<Rightarrow> \<gg>\<^sub>S\<^sub>S | gf = [\<oo>\<^sub>S\<^sub>S, \<ff>\<^sub>S\<^sub>S]\<^sub>\<circ> \<Rightarrow> \<ff>\<^sub>S\<^sub>S | otherwise \<Rightarrow> gf\<lparr>[]\<^sub>\<circ>\<rparr>) \<lparr>\<ff>\<^sub>S\<^sub>S, \<bb>\<^sub>S\<^sub>S\<rparr>\<^sub>\<bullet> = \<ff>\<^sub>S\<^sub>S
[PROOF STEP]
using cat_ss_ineq
[PROOF STATE]
proof (prove)
using this:
[\<ff>\<^sub>S\<^sub>S, \<bb>\<^sub>S\<^sub>S]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable
\<aa>\<^sub>S\<^sub>S \<noteq> \<bb>\<^sub>S\<^sub>S
\<aa>\<^sub>S\<^sub>S \<noteq> \<oo>\<^sub>S\<^sub>S
\<bb>\<^sub>S\<^sub>S \<noteq> \<oo>\<^sub>S\<^sub>S
\<gg>\<^sub>S\<^sub>S \<noteq> \<ff>\<^sub>S\<^sub>S
\<gg>\<^sub>S\<^sub>S \<noteq> \<aa>\<^sub>S\<^sub>S
\<gg>\<^sub>S\<^sub>S \<noteq> \<bb>\<^sub>S\<^sub>S
\<gg>\<^sub>S\<^sub>S \<noteq> \<oo>\<^sub>S\<^sub>S
\<ff>\<^sub>S\<^sub>S \<noteq> \<aa>\<^sub>S\<^sub>S
\<ff>\<^sub>S\<^sub>S \<noteq> \<bb>\<^sub>S\<^sub>S
\<ff>\<^sub>S\<^sub>S \<noteq> \<oo>\<^sub>S\<^sub>S

goal (1 subgoal):
 1. (\<lambda>gf\<in>\<^sub>\<circ>cat_scospan_composable. if gf = [\<oo>\<^sub>S\<^sub>S, \<gg>\<^sub>S\<^sub>S]\<^sub>\<circ> \<Rightarrow> \<gg>\<^sub>S\<^sub>S | gf = [\<oo>\<^sub>S\<^sub>S, \<ff>\<^sub>S\<^sub>S]\<^sub>\<circ> \<Rightarrow> \<ff>\<^sub>S\<^sub>S | otherwise \<Rightarrow> gf\<lparr>[]\<^sub>\<circ>\<rparr>) \<lparr>\<ff>\<^sub>S\<^sub>S, \<bb>\<^sub>S\<^sub>S\<rparr>\<^sub>\<bullet> = \<ff>\<^sub>S\<^sub>S
[PROOF STEP]
by (auto simp: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g

goal:
No subgoals!
[PROOF STEP]
qed