[STATEMENT]
lemma rtrancl_join_join:
  assumes "(a, b) \<in> A\<^sup>*" and "(b, c) \<in> A\<^sup>\<down>" shows "(a, c) \<in> A\<^sup>\<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>\<down>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>\<down>
[PROOF STEP]
from \<open>(b, c) \<in> A\<^sup>\<down>\<close>
[PROOF STATE]
proof (chain)
picking this:
(b, c) \<in> A\<^sup>\<down>
[PROOF STEP]
obtain b' where "(b, b') \<in> A\<^sup>*" and "(b', c) \<in> (A\<inverse>)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(b, c) \<in> A\<^sup>\<down>

goal (1 subgoal):
 1. (\<And>b'. \<lbrakk>(b, b') \<in> A\<^sup>*; (b', c) \<in> (A\<inverse>)\<^sup>*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding join_def
[PROOF STATE]
proof (prove)
using this:
(b, c) \<in> A\<^sup>* O (A\<inverse>)\<^sup>*

goal (1 subgoal):
 1. (\<And>b'. \<lbrakk>(b, b') \<in> A\<^sup>*; (b', c) \<in> (A\<inverse>)\<^sup>*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(b, b') \<in> A\<^sup>*
(b', c) \<in> (A\<inverse>)\<^sup>*

goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>\<down>
[PROOF STEP]
with \<open>(a, b) \<in> A\<^sup>*\<close>
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> A\<^sup>*
(b, b') \<in> A\<^sup>*
(b', c) \<in> (A\<inverse>)\<^sup>*
[PROOF STEP]
have "(a, b') \<in> A\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> A\<^sup>*
(b, b') \<in> A\<^sup>*
(b', c) \<in> (A\<inverse>)\<^sup>*

goal (1 subgoal):
 1. (a, b') \<in> A\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(a, b') \<in> A\<^sup>*

goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>\<down>
[PROOF STEP]
with \<open>(b', c) \<in> (A\<inverse>)\<^sup>*\<close>
[PROOF STATE]
proof (chain)
picking this:
(b', c) \<in> (A\<inverse>)\<^sup>*
(a, b') \<in> A\<^sup>*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(b', c) \<in> (A\<inverse>)\<^sup>*
(a, b') \<in> A\<^sup>*

goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>\<down>
[PROOF STEP]
unfolding join_def
[PROOF STATE]
proof (prove)
using this:
(b', c) \<in> (A\<inverse>)\<^sup>*
(a, b') \<in> A\<^sup>*

goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>* O (A\<inverse>)\<^sup>*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, c) \<in> A\<^sup>\<down>

goal:
No subgoals!
[PROOF STEP]
qed