[STATEMENT]
lemma RP_from_R :
  assumes "\<And> q P . (q,P) \<in> PS \<Longrightarrow> is_preamble P M q"
  and     "\<And> q P io x y y' . (q,P) \<in> PS \<Longrightarrow> io@[(x,y)] \<in> L P \<Longrightarrow> io@[(x,y')] \<in> L M' \<Longrightarrow> io@[(x,y')] \<in> L P"
  and     "completely_specified M'"
  and     "inputs M' = inputs M"
shows "(RP M q q' pP p PS M' = R M q q' pP p)
          \<or> (\<exists> P' pP' . (q',P') \<in> PS \<and>
                        path P' (initial P') pP' \<and>
                        target (initial P') pP' = q' \<and>
                        path M (initial M) pP' \<and>
                        target (initial M) pP' = q' \<and>
                        p_io pP' \<in> L M' \<and>
                        RP M q q' pP p PS M' =
                        insert pP' (R M q q' pP p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists> P' pP' . (q',P') \<in> PS \<and> path P' (initial P') pP' \<and> target (initial P') pP' = q' \<and> path M (initial M) pP' \<and> target (initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)))"
[PROOF STATE]
proof (state)
this:
\<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)))

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)))
[PROOF STEP]
have "(RP M q q' pP p PS M' \<noteq> R M q q' pP p)"
       and  "\<not> (\<exists> P' pP' . (q',P') \<in> PS \<and>
                            path P' (initial P') pP' \<and>
                            target (initial P') pP' = q' \<and>
                            path M (initial M) pP' \<and>
                            target (initial M) pP' = q' \<and>
                            p_io pP' \<in> L M' \<and>
                            RP M q q' pP p PS M' = insert pP' (R M q q' pP p))"
[PROOF STATE]
proof (prove)
using this:
\<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)))

goal (1 subgoal):
 1. RP M q q' pP p PS M' \<noteq> R M q q' pP p &&& \<nexists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
RP M q q' pP p PS M' \<noteq> R M q q' pP p
\<nexists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
let ?p = "SOME pP' . \<exists> P' .  (q',P') \<in> PS \<and> path P' (initial P') pP' \<and> target (initial P') pP' = q' \<and> p_io pP' \<in> L M'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
have "\<exists> P' .  (q',P') \<in> PS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P'. (q', P') \<in> PS
[PROOF STEP]
using \<open>(RP M q q' pP p PS M' \<noteq> R M q q' pP p)\<close>
[PROOF STATE]
proof (prove)
using this:
RP M q q' pP p PS M' \<noteq> R M q q' pP p

goal (1 subgoal):
 1. \<exists>P'. (q', P') \<in> PS
[PROOF STEP]
unfolding RP_def
[PROOF STATE]
proof (prove)
using this:
(if \<exists>P'. (q', P') \<in> PS then insert (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') (R M q q' pP p) else R M q q' pP p) \<noteq> R M q q' pP p

goal (1 subgoal):
 1. \<exists>P'. (q', P') \<in> PS
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>P'. (q', P') \<in> PS

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P'. (q', P') \<in> PS
[PROOF STEP]
obtain P' where "(q',P') \<in> PS"
[PROOF STATE]
proof (prove)
using this:
\<exists>P'. (q', P') \<in> PS

goal (1 subgoal):
 1. (\<And>P'. (q', P') \<in> PS \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(q', P') \<in> PS

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q', P') \<in> PS
[PROOF STEP]
have "is_preamble P' M q'"
[PROOF STATE]
proof (prove)
using this:
(q', P') \<in> PS

goal (1 subgoal):
 1. is_preamble P' M q'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(q', P') \<in> PS
(?q, ?P) \<in> PS \<Longrightarrow> is_preamble ?P M ?q
\<lbrakk>(?q, ?P) \<in> PS; ?io @ [(?x, ?y)] \<in> L ?P; ?io @ [(?x, ?y')] \<in> L M'\<rbrakk> \<Longrightarrow> ?io @ [(?x, ?y')] \<in> L ?P
completely_specified M'
FSM.inputs M' = FSM.inputs M

goal (1 subgoal):
 1. is_preamble P' M q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_preamble P' M q'

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
obtain pP' where "path P' (initial P') pP'" and "target (initial P') pP' = q'" and "p_io pP' \<in> L M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pP'. \<lbrakk>path P' (FSM.initial P') pP'; target (FSM.initial P') pP' = q'; p_io pP' \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using preamble_pass_path[OF \<open>is_preamble P' M q'\<close>
          assms(2)[OF \<open>(q',P') \<in> PS\<close>] assms(3,4)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L P'; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, ?y1 io x y y')] \<in> L P'; \<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L P'; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L M'; \<And>p. \<lbrakk>path P' (FSM.initial P') p; target (FSM.initial P') p = q'; p_io p \<in> L M'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>pP'. \<lbrakk>path P' (FSM.initial P') pP'; target (FSM.initial P') pP' = q'; p_io pP' \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
path P' (FSM.initial P') pP'
target (FSM.initial P') pP' = q'
p_io pP' \<in> L M'

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path P' (FSM.initial P') pP'
target (FSM.initial P') pP' = q'
p_io pP' \<in> L M'
[PROOF STEP]
have "\<exists> pP' . \<exists> P' .  (q',P') \<in> PS \<and> path P' (initial P') pP' \<and> target (initial P') pP' = q' \<and> p_io pP' \<in> L M'"
[PROOF STATE]
proof (prove)
using this:
path P' (FSM.initial P') pP'
target (FSM.initial P') pP' = q'
p_io pP' \<in> L M'

goal (1 subgoal):
 1. \<exists>pP' P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M'
[PROOF STEP]
using \<open>(q',P') \<in> PS\<close>
[PROOF STATE]
proof (prove)
using this:
path P' (FSM.initial P') pP'
target (FSM.initial P') pP' = q'
p_io pP' \<in> L M'
(q', P') \<in> PS

goal (1 subgoal):
 1. \<exists>pP' P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>pP' P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M'

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
have "\<exists> P' .  (q',P') \<in> PS \<and> path P' (initial P') ?p \<and> target (initial P') ?p = q' \<and> p_io ?p \<in> L M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<and> target (FSM.initial P') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q' \<and> p_io (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<in> L M'
[PROOF STEP]
using someI_ex[OF \<open>\<exists> pP' . \<exists> P' .  (q',P') \<in> PS \<and> path P' (initial P') pP' \<and> target (initial P') pP' = q' \<and> p_io pP' \<in> L M'\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') (SOME x. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') x \<and> target (FSM.initial P') x = q' \<and> p_io x \<in> L M') \<and> target (FSM.initial P') (SOME x. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') x \<and> target (FSM.initial P') x = q' \<and> p_io x \<in> L M') = q' \<and> p_io (SOME x. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') x \<and> target (FSM.initial P') x = q' \<and> p_io x \<in> L M') \<in> L M'

goal (1 subgoal):
 1. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<and> target (FSM.initial P') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q' \<and> p_io (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<in> L M'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<and> target (FSM.initial P') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q' \<and> p_io (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<in> L M'

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<and> target (FSM.initial P') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q' \<and> p_io (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<in> L M'
[PROOF STEP]
obtain P'' where "(q',P'') \<in> PS" and "path P'' (initial P'') ?p" and "target (initial P'') ?p = q'" and "p_io ?p \<in> L M'"
[PROOF STATE]
proof (prove)
using this:
\<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<and> target (FSM.initial P') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q' \<and> p_io (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<in> L M'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>(q', P'') \<in> PS; path P'' (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M'); target (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'; p_io (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(q', P'') \<in> PS
path P'' (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')
target (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'
p_io (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<in> L M'

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q', P'') \<in> PS
path P'' (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')
target (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'
p_io (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<in> L M'
[PROOF STEP]
have "is_preamble P'' M q'"
[PROOF STATE]
proof (prove)
using this:
(q', P'') \<in> PS
path P'' (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')
target (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'
p_io (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<in> L M'

goal (1 subgoal):
 1. is_preamble P'' M q'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(q', P'') \<in> PS
path P'' (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')
target (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'
p_io (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<in> L M'
(?q, ?P) \<in> PS \<Longrightarrow> is_preamble ?P M ?q
\<lbrakk>(?q, ?P) \<in> PS; ?io @ [(?x, ?y)] \<in> L ?P; ?io @ [(?x, ?y')] \<in> L M'\<rbrakk> \<Longrightarrow> ?io @ [(?x, ?y')] \<in> L ?P
completely_specified M'
FSM.inputs M' = FSM.inputs M

goal (1 subgoal):
 1. is_preamble P'' M q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_preamble P'' M q'

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
have "initial P'' = initial M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial P'' = FSM.initial M
[PROOF STEP]
using \<open>is_preamble P'' M q'\<close>
[PROOF STATE]
proof (prove)
using this:
is_preamble P'' M q'

goal (1 subgoal):
 1. FSM.initial P'' = FSM.initial M
[PROOF STEP]
unfolding is_preamble_def
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P'' \<and> single_input P'' \<and> is_submachine P'' M \<and> q' \<in> reachable_states P'' \<and> deadlock_state P'' q' \<and> (\<forall>q'a\<in>reachable_states P''. (q' = q'a \<or> \<not> deadlock_state P'' q'a) \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P''. t_source t = q'a \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q'a \<and> t_input t' = x \<longrightarrow> t' \<in> FSM.transitions P'')))

goal (1 subgoal):
 1. FSM.initial P'' = FSM.initial M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.initial P'' = FSM.initial M

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
have "path M (initial M) ?p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path M (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')
[PROOF STEP]
using \<open>is_preamble P'' M q'\<close>
[PROOF STATE]
proof (prove)
using this:
is_preamble P'' M q'

goal (1 subgoal):
 1. path M (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')
[PROOF STEP]
unfolding is_preamble_def
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P'' \<and> single_input P'' \<and> is_submachine P'' M \<and> q' \<in> reachable_states P'' \<and> deadlock_state P'' q' \<and> (\<forall>q'a\<in>reachable_states P''. (q' = q'a \<or> \<not> deadlock_state P'' q'a) \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P''. t_source t = q'a \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q'a \<and> t_input t' = x \<longrightarrow> t' \<in> FSM.transitions P'')))

goal (1 subgoal):
 1. path M (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')
[PROOF STEP]
using submachine_path_initial
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P'' \<and> single_input P'' \<and> is_submachine P'' M \<and> q' \<in> reachable_states P'' \<and> deadlock_state P'' q' \<and> (\<forall>q'a\<in>reachable_states P''. (q' = q'a \<or> \<not> deadlock_state P'' q'a) \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P''. t_source t = q'a \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q'a \<and> t_input t' = x \<longrightarrow> t' \<in> FSM.transitions P'')))
\<lbrakk>is_submachine ?A ?B; path ?A (FSM.initial ?A) ?p\<rbrakk> \<Longrightarrow> path ?B (FSM.initial ?B) ?p

goal (1 subgoal):
 1. path M (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')
[PROOF STEP]
using \<open>path P'' (FSM.initial P'') ?p\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P'' \<and> single_input P'' \<and> is_submachine P'' M \<and> q' \<in> reachable_states P'' \<and> deadlock_state P'' q' \<and> (\<forall>q'a\<in>reachable_states P''. (q' = q'a \<or> \<not> deadlock_state P'' q'a) \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P''. t_source t = q'a \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q'a \<and> t_input t' = x \<longrightarrow> t' \<in> FSM.transitions P'')))
\<lbrakk>is_submachine ?A ?B; path ?A (FSM.initial ?A) ?p\<rbrakk> \<Longrightarrow> path ?B (FSM.initial ?B) ?p
path P'' (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')

goal (1 subgoal):
 1. path M (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
have "target (initial M) ?p = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'
[PROOF STEP]
using \<open>target (initial P'') ?p = q'\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'

goal (1 subgoal):
 1. target (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'
[PROOF STEP]
unfolding \<open>initial P'' = initial M\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'

goal (1 subgoal):
 1. target (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
target (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
have "RP M q q' pP p PS M' = insert ?p (R M q q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RP M q q' pP p PS M' = insert (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') (R M q q' pP p)
[PROOF STEP]
using \<open>\<exists> P' .  (q',P') \<in> PS\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>P'. (q', P') \<in> PS

goal (1 subgoal):
 1. RP M q q' pP p PS M' = insert (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') (R M q q' pP p)
[PROOF STEP]
unfolding RP_def
[PROOF STATE]
proof (prove)
using this:
\<exists>P'. (q', P') \<in> PS

goal (1 subgoal):
 1. (if \<exists>P'. (q', P') \<in> PS then insert (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') (R M q q' pP p) else R M q q' pP p) = insert (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') (R M q q' pP p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
RP M q q' pP p PS M' = insert (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') (R M q q' pP p)

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
RP M q q' pP p PS M' = insert (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') (R M q q' pP p)
[PROOF STEP]
have "(\<exists> P' pP' . (q',P') \<in> PS \<and>
                          path P' (initial P') pP' \<and>
                          target (initial P') pP' = q' \<and>
                          path M (initial M) pP' \<and>
                          target (initial M) pP' = q' \<and>
                          p_io pP' \<in> L M' \<and>
                          RP M q q' pP p PS M' = insert pP' (R M q q' pP p))"
[PROOF STATE]
proof (prove)
using this:
RP M q q' pP p PS M' = insert (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') (R M q q' pP p)

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)
[PROOF STEP]
using \<open>(q',P'') \<in> PS\<close> \<open>path P'' (initial P'') ?p\<close> \<open>target (initial P'') ?p = q'\<close>
          \<open>path M (initial M) ?p\<close> \<open>target (initial M) ?p = q'\<close> \<open>p_io ?p \<in> L M'\<close>
[PROOF STATE]
proof (prove)
using this:
RP M q q' pP p PS M' = insert (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') (R M q q' pP p)
(q', P'') \<in> PS
path P'' (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')
target (FSM.initial P'') (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'
path M (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M')
target (FSM.initial M) (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') = q'
p_io (SOME pP'. \<exists>P'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> p_io pP' \<in> L M') \<in> L M'

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)

goal (1 subgoal):
 1. \<not> (RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>\<not> (\<exists> P' pP' . (q',P') \<in> PS \<and> path P' (initial P') pP' \<and> target (initial P') pP' = q' \<and> path M (initial M) pP' \<and> target (initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)
\<nexists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma RP_from_R_inserted :
  assumes "\<And> q P . (q,P) \<in> PS \<Longrightarrow> is_preamble P M q"
  and     "\<And> q P io x y y' . (q,P) \<in> PS \<Longrightarrow> io@[(x,y)] \<in> L P \<Longrightarrow> io@[(x,y')] \<in> L M' \<Longrightarrow> io@[(x,y')] \<in> L P"
  and     "completely_specified M'"
  and     "inputs M' = inputs M"
  and     "pP' \<in> RP M q q' pP p PS M'"
  and     "pP' \<notin> R M q q' pP p"
obtains P' where  "(q',P') \<in> PS"
                  "path P' (initial P') pP'"
                  "target (initial P') pP' = q'"
                  "path M (initial M) pP'"
                  "target (initial M) pP' = q'"
                  "p_io pP' \<in> L M'"
                  "RP M q q' pP p PS M' = insert pP' (R M q q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pP'; target (FSM.initial P') pP' = q'; path M (FSM.initial M) pP'; target (FSM.initial M) pP' = q'; p_io pP' \<in> L M'; RP M q q' pP p PS M' = insert pP' (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pP'; target (FSM.initial P') pP' = q'; path M (FSM.initial M) pP'; target (FSM.initial M) pP' = q'; p_io pP' \<in> L M'; RP M q q' pP p PS M' = insert pP' (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "(RP M q q' pP p PS M' \<noteq> R M q q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RP M q q' pP p PS M' \<noteq> R M q q' pP p
[PROOF STEP]
using assms(5,6)
[PROOF STATE]
proof (prove)
using this:
pP' \<in> RP M q q' pP p PS M'
pP' \<notin> R M q q' pP p

goal (1 subgoal):
 1. RP M q q' pP p PS M' \<noteq> R M q q' pP p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
RP M q q' pP p PS M' \<noteq> R M q q' pP p

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pP'; target (FSM.initial P') pP' = q'; path M (FSM.initial M) pP'; target (FSM.initial M) pP' = q'; p_io pP' \<in> L M'; RP M q q' pP p PS M' = insert pP' (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
RP M q q' pP p PS M' \<noteq> R M q q' pP p
[PROOF STEP]
have "(\<exists>P' pP'.
              (q', P') \<in> PS \<and>
              path P' (FSM.initial P') pP' \<and>
              target (FSM.initial P') pP' = q' \<and>
              path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))"
[PROOF STATE]
proof (prove)
using this:
RP M q q' pP p PS M' \<noteq> R M q q' pP p

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)
[PROOF STEP]
using RP_from_R[OF assms(1-4), of PS _ _ q q' pP p]
[PROOF STATE]
proof (prove)
using this:
RP M q q' pP p PS M' \<noteq> R M q q' pP p
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> (?q1 q P io x y y', P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, ?y1 q P io x y y')] \<in> L P; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pP'; target (FSM.initial P') pP' = q'; path M (FSM.initial M) pP'; target (FSM.initial M) pP' = q'; p_io pP' \<in> L M'; RP M q q' pP p PS M' = insert pP' (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)
[PROOF STEP]
obtain P' pP'' where "(q', P') \<in> PS"
                            "path P' (FSM.initial P') pP''"
                            "target (FSM.initial P') pP'' = q'"
                            "path M (FSM.initial M) pP''"
                            "target (FSM.initial M) pP'' = q'"
                            "p_io pP'' \<in> L M'"
                            "RP M q q' pP p PS M' = insert pP'' (R M q q' pP p)"
[PROOF STATE]
proof (prove)
using this:
\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p)

goal (1 subgoal):
 1. (\<And>P' pP''. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pP''; target (FSM.initial P') pP'' = q'; path M (FSM.initial M) pP''; target (FSM.initial M) pP'' = q'; p_io pP'' \<in> L M'; RP M q q' pP p PS M' = insert pP'' (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q', P') \<in> PS
path P' (FSM.initial P') pP''
target (FSM.initial P') pP'' = q'
path M (FSM.initial M) pP''
target (FSM.initial M) pP'' = q'
p_io pP'' \<in> L M'
RP M q q' pP p PS M' = insert pP'' (R M q q' pP p)

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pP'; target (FSM.initial P') pP' = q'; path M (FSM.initial M) pP'; target (FSM.initial M) pP' = q'; p_io pP' \<in> L M'; RP M q q' pP p PS M' = insert pP' (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(q', P') \<in> PS
path P' (FSM.initial P') pP''
target (FSM.initial P') pP'' = q'
path M (FSM.initial M) pP''
target (FSM.initial M) pP'' = q'
p_io pP'' \<in> L M'
RP M q q' pP p PS M' = insert pP'' (R M q q' pP p)

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pP'; target (FSM.initial P') pP' = q'; path M (FSM.initial M) pP'; target (FSM.initial M) pP' = q'; p_io pP' \<in> L M'; RP M q q' pP p PS M' = insert pP' (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "pP'' = pP'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pP'' = pP'
[PROOF STEP]
using \<open>RP M q q' pP p PS M' = insert pP'' (R M q q' pP p)\<close> assms(5,6)
[PROOF STATE]
proof (prove)
using this:
RP M q q' pP p PS M' = insert pP'' (R M q q' pP p)
pP' \<in> RP M q q' pP p PS M'
pP' \<notin> R M q q' pP p

goal (1 subgoal):
 1. pP'' = pP'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pP'' = pP'

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pP'; target (FSM.initial P') pP' = q'; path M (FSM.initial M) pP'; target (FSM.initial M) pP' = q'; p_io pP' \<in> L M'; RP M q q' pP p PS M' = insert pP' (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(q', P') \<in> PS
path P' (FSM.initial P') pP''
target (FSM.initial P') pP'' = q'
path M (FSM.initial M) pP''
target (FSM.initial M) pP'' = q'
p_io pP'' \<in> L M'
RP M q q' pP p PS M' = insert pP'' (R M q q' pP p)
pP'' = pP'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(q', P') \<in> PS
path P' (FSM.initial P') pP''
target (FSM.initial P') pP'' = q'
path M (FSM.initial M) pP''
target (FSM.initial M) pP'' = q'
p_io pP'' \<in> L M'
RP M q q' pP p PS M' = insert pP'' (R M q q' pP p)
pP'' = pP'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of P']
[PROOF STATE]
proof (prove)
using this:
(q', P') \<in> PS
path P' (FSM.initial P') pP''
target (FSM.initial P') pP'' = q'
path M (FSM.initial M) pP''
target (FSM.initial M) pP'' = q'
p_io pP'' \<in> L M'
RP M q q' pP p PS M' = insert pP'' (R M q q' pP p)
pP'' = pP'
\<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pP'; target (FSM.initial P') pP' = q'; path M (FSM.initial M) pP'; target (FSM.initial M) pP' = q'; p_io pP' \<in> L M'; RP M q q' pP p PS M' = insert pP' (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding \<open>pP'' = pP'\<close>
[PROOF STATE]
proof (prove)
using this:
(q', P') \<in> PS
path P' (FSM.initial P') pP'
target (FSM.initial P') pP' = q'
path M (FSM.initial M) pP'
target (FSM.initial M) pP' = q'
p_io pP' \<in> L M'
RP M q q' pP p PS M' = insert pP' (R M q q' pP p)
pP' = pP'
\<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pP'; target (FSM.initial P') pP' = q'; path M (FSM.initial M) pP'; target (FSM.initial M) pP' = q'; p_io pP' \<in> L M'; RP M q q' pP p PS M' = insert pP' (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_R :
  assumes "path M q p"
  shows "finite (R M q q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (R M q q' pP p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (R M q q' pP p)
[PROOF STEP]
have "\<And> p' . p' \<in> (R M q q' pP p) \<Longrightarrow> p' \<in> set (prefixes (pP@p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> set (prefixes (pP @ p))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> set (prefixes (pP @ p))
[PROOF STEP]
fix p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> set (prefixes (pP @ p))
[PROOF STEP]
assume "p' \<in> (R M q q' pP p)"
[PROOF STATE]
proof (state)
this:
p' \<in> R M q q' pP p

goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> set (prefixes (pP @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' \<in> R M q q' pP p
[PROOF STEP]
obtain p'' where "p' = pP @ p''"
[PROOF STATE]
proof (prove)
using this:
p' \<in> R M q q' pP p

goal (1 subgoal):
 1. (\<And>p''. p' = pP @ p'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}

goal (1 subgoal):
 1. (\<And>p''. p' = pP @ p'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p' = pP @ p''

goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> set (prefixes (pP @ p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' = pP @ p''
[PROOF STEP]
obtain p''' where "p = p'' @ p'''"
[PROOF STATE]
proof (prove)
using this:
p' = pP @ p''

goal (1 subgoal):
 1. (\<And>p'''. p = p'' @ p''' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>p' \<in> (R M q q' pP p)\<close>
[PROOF STATE]
proof (prove)
using this:
p' = pP @ p''
p' \<in> R M q q' pP p

goal (1 subgoal):
 1. (\<And>p'''. p = p'' @ p''' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
p' = pP @ p''
p' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}

goal (1 subgoal):
 1. (\<And>p'''. p = p'' @ p''' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p = p'' @ p'''

goal (1 subgoal):
 1. \<And>p'. p' \<in> R M q q' pP p \<Longrightarrow> p' \<in> set (prefixes (pP @ p))
[PROOF STEP]
show "p' \<in> set (prefixes (pP@p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' \<in> set (prefixes (pP @ p))
[PROOF STEP]
unfolding prefixes_set \<open>p' = pP @ p''\<close> \<open>p = p'' @ p'''\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pP @ p'' \<in> {xs'. \<exists>xs''. xs' @ xs'' = pP @ p'' @ p'''}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p' \<in> set (prefixes (pP @ p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?p' \<in> R M q q' pP p \<Longrightarrow> ?p' \<in> set (prefixes (pP @ p))

goal (1 subgoal):
 1. finite (R M q q' pP p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?p' \<in> R M q q' pP p \<Longrightarrow> ?p' \<in> set (prefixes (pP @ p))
[PROOF STEP]
have "(R M q q' pP p) \<subseteq> set (prefixes (pP@p))"
[PROOF STATE]
proof (prove)
using this:
?p' \<in> R M q q' pP p \<Longrightarrow> ?p' \<in> set (prefixes (pP @ p))

goal (1 subgoal):
 1. R M q q' pP p \<subseteq> set (prefixes (pP @ p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R M q q' pP p \<subseteq> set (prefixes (pP @ p))

goal (1 subgoal):
 1. finite (R M q q' pP p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
R M q q' pP p \<subseteq> set (prefixes (pP @ p))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R M q q' pP p \<subseteq> set (prefixes (pP @ p))

goal (1 subgoal):
 1. finite (R M q q' pP p)
[PROOF STEP]
using rev_finite_subset
[PROOF STATE]
proof (prove)
using this:
R M q q' pP p \<subseteq> set (prefixes (pP @ p))
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (R M q q' pP p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (R M q q' pP p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_RP :
  assumes "path M q p"
  and     "\<And> q P . (q,P) \<in> PS \<Longrightarrow> is_preamble P M q"
  and     "\<And> q P io x y y' . (q,P) \<in> PS \<Longrightarrow> io@[(x,y)] \<in> L P \<Longrightarrow> io@[(x,y')] \<in> L M' \<Longrightarrow> io@[(x,y')] \<in> L P"
  and     "completely_specified M'"
  and     "inputs M' = inputs M"
shows "finite (RP M q q' pP p PS M')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (RP M q q' pP p PS M')
[PROOF STEP]
using finite_R[OF assms(1), of q' pP ]
        RP_from_R[OF assms(2,3,4,5), of PS _ _ q q' pP p]
[PROOF STATE]
proof (prove)
using this:
finite (R M q q' pP p)
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> (?q1 q P io x y y', P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, ?y1 q P io x y y')] \<in> L P; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> RP M q q' pP p PS M' = R M q q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M q q' pP p PS M' = insert pP' (R M q q' pP p))

goal (1 subgoal):
 1. finite (RP M q q' pP p PS M')
[PROOF STEP]
by force


[STATEMENT]
lemma R_component_ob :
  assumes "pR' \<in> R M q q' pP p"
  obtains pR where "pR' = pP@pR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pR. pR' = pP @ pR \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pR' \<in> R M q q' pP p

goal (1 subgoal):
 1. (\<And>pR. pR' = pP @ pR \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
pR' \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}

goal (1 subgoal):
 1. (\<And>pR. pR' = pP @ pR \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma R_component :
  assumes "(pP@pR) \<in> R M q q' pP p"
shows "pR = take (length pR) p"
and   "length pR \<le> length p"
and   "t_target (p ! (length pR - 1)) = q'"
and   "pR \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pR = take (length pR) p &&& length pR \<le> length p) &&& t_target (p ! (length pR - 1)) = q' &&& pR \<noteq> []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pR = take (length pR) p
 2. length pR \<le> length p
 3. t_target (p ! (length pR - 1)) = q'
 4. pR \<noteq> []
[PROOF STEP]
let ?R = "R M q q' p"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pR = take (length pR) p
 2. length pR \<le> length p
 3. t_target (p ! (length pR - 1)) = q'
 4. pR \<noteq> []
[PROOF STEP]
have "pR \<noteq> []" and "target q pR = q'" and "\<exists> p'' . p = pR@p''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pR \<noteq> [] &&& target q pR = q' &&& \<exists>p''. p = pR @ p''
[PROOF STEP]
using \<open>pP@pR \<in> R M q q' pP p\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR \<in> R M q q' pP p

goal (1 subgoal):
 1. pR \<noteq> [] &&& target q pR = q' &&& \<exists>p''. p = pR @ p''
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
pP @ pR \<in> {pP @ p' |p'. p' \<noteq> [] \<and> target q p' = q' \<and> (\<exists>p''. p = p' @ p'')}

goal (1 subgoal):
 1. pR \<noteq> [] &&& target q pR = q' &&& \<exists>p''. p = pR @ p''
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
pR \<noteq> []
target q pR = q'
\<exists>p''. p = pR @ p''

goal (4 subgoals):
 1. pR = take (length pR) p
 2. length pR \<le> length p
 3. t_target (p ! (length pR - 1)) = q'
 4. pR \<noteq> []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR \<noteq> []
target q pR = q'
\<exists>p''. p = pR @ p''
[PROOF STEP]
obtain pR' where "p = pR@pR'"
[PROOF STATE]
proof (prove)
using this:
pR \<noteq> []
target q pR = q'
\<exists>p''. p = pR @ p''

goal (1 subgoal):
 1. (\<And>pR'. p = pR @ pR' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p = pR @ pR'

goal (4 subgoals):
 1. pR = take (length pR) p
 2. length pR \<le> length p
 3. t_target (p ! (length pR - 1)) = q'
 4. pR \<noteq> []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = pR @ pR'
[PROOF STEP]
show "pR = take (length pR) p" and "length pR \<le> length p"
[PROOF STATE]
proof (prove)
using this:
p = pR @ pR'

goal (1 subgoal):
 1. pR = take (length pR) p &&& length pR \<le> length p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pR = take (length pR) p
length pR \<le> length p

goal (2 subgoals):
 1. t_target (p ! (length pR - 1)) = q'
 2. pR \<noteq> []
[PROOF STEP]
show "t_target (p ! (length pR - 1)) = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_target (p ! (length pR - 1)) = q'
[PROOF STEP]
using \<open>pR \<noteq> []\<close> \<open>target q pR = q'\<close>
[PROOF STATE]
proof (prove)
using this:
pR \<noteq> []
target q pR = q'

goal (1 subgoal):
 1. t_target (p ! (length pR - 1)) = q'
[PROOF STEP]
unfolding target.simps visited_states.simps
[PROOF STATE]
proof (prove)
using this:
pR \<noteq> []
last (q # map t_target pR) = q'

goal (1 subgoal):
 1. t_target (p ! (length pR - 1)) = q'
[PROOF STEP]
by (metis (no_types, lifting) Suc_diff_1 \<open>pR = take (length pR) p\<close>
          append_butlast_last_id last.simps last_map length_butlast lessI list.map_disc_iff
          not_gr_zero nth_append_length nth_take take_eq_Nil)
[PROOF STATE]
proof (state)
this:
t_target (p ! (length pR - 1)) = q'

goal (1 subgoal):
 1. pR \<noteq> []
[PROOF STEP]
show "pR \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pR \<noteq> []
[PROOF STEP]
using \<open>pR \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
pR \<noteq> []

goal (1 subgoal):
 1. pR \<noteq> []
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
pR \<noteq> []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R_component_observable :
  assumes "pP@pR \<in> R M (target (initial M) pP) q' pP p"
  and     "observable M"
  and     "path M (initial M) pP"
  and     "path M (target (initial M) pP) p"
shows "io_targets M (p_io pP @ p_io pR) (initial M) = {target (target (initial M) pP) (take (length pR) p)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
have "pR = take (length pR) p"
  and  "length pR \<le> length p"
  and  "t_target (p ! (length pR - 1)) = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pR = take (length pR) p &&& length pR \<le> length p &&& t_target (p ! (length pR - 1)) = q'
[PROOF STEP]
using R_component[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
pR = take (length pR) p
length pR \<le> length p
t_target (p ! (length pR - 1)) = q'
pR \<noteq> []

goal (1 subgoal):
 1. pR = take (length pR) p &&& length pR \<le> length p &&& t_target (p ! (length pR - 1)) = q'
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
pR = take (length pR) p
length pR \<le> length p
t_target (p ! (length pR - 1)) = q'

goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
let ?q = "(target (initial M) pP)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
have "path M ?q (take (length pR) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path M (target (FSM.initial M) pP) (take (length pR) p)
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
path M (target (FSM.initial M) pP) p

goal (1 subgoal):
 1. path M (target (FSM.initial M) pP) (take (length pR) p)
[PROOF STEP]
by (simp add: path_prefix_take)
[PROOF STATE]
proof (state)
this:
path M (target (FSM.initial M) pP) (take (length pR) p)

goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
have "p_io (take (length pR) p) = p_io pR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (take (length pR) p) = p_io pR
[PROOF STEP]
using \<open>pR = take (length pR) p\<close>
[PROOF STATE]
proof (prove)
using this:
pR = take (length pR) p

goal (1 subgoal):
 1. p_io (take (length pR) p) = p_io pR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_io (take (length pR) p) = p_io pR

goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
have *:"path M (initial M) (pP @ (take (length pR) p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path M (FSM.initial M) (pP @ take (length pR) p)
[PROOF STEP]
using \<open>path M (initial M) pP\<close> \<open>path M ?q (take (length pR) p)\<close>
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) pP
path M (target (FSM.initial M) pP) (take (length pR) p)

goal (1 subgoal):
 1. path M (FSM.initial M) (pP @ take (length pR) p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) (pP @ take (length pR) p)

goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
have **:"p_io (pP @ (take (length pR) p)) = (p_io pP @ p_io pR)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (pP @ take (length pR) p) = p_io pP @ p_io pR
[PROOF STEP]
using \<open>p_io (take (length pR) p) = p_io pR\<close>
[PROOF STATE]
proof (prove)
using this:
p_io (take (length pR) p) = p_io pR

goal (1 subgoal):
 1. p_io (pP @ take (length pR) p) = p_io pP @ p_io pR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_io (pP @ take (length pR) p) = p_io pP @ p_io pR

goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
have "target (initial M) (pP @ (take (length pR) p)) = target ?q (take (length pR) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial M) (pP @ take (length pR) p) = target (target (FSM.initial M) pP) (take (length pR) p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target (FSM.initial M) (pP @ take (length pR) p) = target (target (FSM.initial M) pP) (take (length pR) p)

goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target (FSM.initial M) (pP @ take (length pR) p) = target (target (FSM.initial M) pP) (take (length pR) p)
[PROOF STEP]
have "target ?q (take (length pR) p) \<in> io_targets M (p_io pP @ p_io pR) (initial M)"
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) (pP @ take (length pR) p) = target (target (FSM.initial M) pP) (take (length pR) p)

goal (1 subgoal):
 1. target (target (FSM.initial M) pP) (take (length pR) p) \<in> io_targets M (p_io pP @ p_io pR) (FSM.initial M)
[PROOF STEP]
unfolding io_targets.simps
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) (pP @ take (length pR) p) = target (target (FSM.initial M) pP) (take (length pR) p)

goal (1 subgoal):
 1. target (target (FSM.initial M) pP) (take (length pR) p) \<in> {target (FSM.initial M) p |p. path M (FSM.initial M) p \<and> p_io p = p_io pP @ p_io pR}
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) (pP @ take (length pR) p) = target (target (FSM.initial M) pP) (take (length pR) p)
path M (FSM.initial M) (pP @ take (length pR) p)
p_io (pP @ take (length pR) p) = p_io pP @ p_io pR

goal (1 subgoal):
 1. target (target (FSM.initial M) pP) (take (length pR) p) \<in> {target (FSM.initial M) p |p. path M (FSM.initial M) p \<and> p_io p = p_io pP @ p_io pR}
[PROOF STEP]
by (metis (mono_tags, lifting) mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
target (target (FSM.initial M) pP) (take (length pR) p) \<in> io_targets M (p_io pP @ p_io pR) (FSM.initial M)

goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
show "io_targets M (p_io pP @ p_io pR) (initial M) = {target ?q (take (length pR) p)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
using observable_io_targets[OF \<open>observable M\<close> language_state_containment[OF * **]]
[PROOF STATE]
proof (prove)
using this:
(\<And>q'. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {q'} \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}
[PROOF STEP]
by (metis (no_types) \<open>target (target (FSM.initial M) pP) (take (length pR) p) \<in> io_targets M (p_io pP @ p_io pR) (FSM.initial M)\<close> singleton_iff)
[PROOF STATE]
proof (state)
this:
io_targets M (p_io pP @ p_io pR) (FSM.initial M) = {target (target (FSM.initial M) pP) (take (length pR) p)}

goal:
No subgoals!
[PROOF STEP]
qed