[STATEMENT]
lemma RP_target:
  assumes "pR \<in> (RP M q q' pP p PS M')"
  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 "target (initial M) pR = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial M) pR = q'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. target (FSM.initial M) pR = q'
[PROOF STEP]
show "target (initial M) pR = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial M) pR = q'
[PROOF STEP]
proof (cases "pR \<in> R M q q' pP p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pR \<in> R M q q' pP p \<Longrightarrow> target (FSM.initial M) pR = q'
 2. pR \<notin> R M q q' pP p \<Longrightarrow> target (FSM.initial M) pR = q'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pR \<in> R M q q' pP p

goal (2 subgoals):
 1. pR \<in> R M q q' pP p \<Longrightarrow> target (FSM.initial M) pR = q'
 2. pR \<notin> R M q q' pP p \<Longrightarrow> target (FSM.initial M) pR = q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR \<in> R M q q' pP p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pR \<in> R M q q' pP p

goal (1 subgoal):
 1. target (FSM.initial M) pR = q'
[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. target (FSM.initial M) pR = q'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
target (FSM.initial M) pR = q'

goal (1 subgoal):
 1. pR \<notin> R M q q' pP p \<Longrightarrow> target (FSM.initial M) pR = q'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pR \<notin> R M q q' pP p \<Longrightarrow> target (FSM.initial M) pR = q'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
pR \<notin> R M q q' pP p

goal (1 subgoal):
 1. pR \<notin> R M q q' pP p \<Longrightarrow> target (FSM.initial M) pR = q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR \<notin> R M q q' pP p
[PROOF STEP]
have "RP M q q' pP p PS M' \<noteq> R M q q' pP p"
[PROOF STATE]
proof (prove)
using this:
pR \<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]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
pR \<notin> R M q q' pP p
pR \<in> RP M q q' pP p PS M'

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. pR \<notin> R M q q' pP p \<Longrightarrow> target (FSM.initial M) pR = q'
[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(2-5), 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. pR \<notin> R M q q' pP p \<Longrightarrow> target (FSM.initial M) pR = q'
[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 pP' where "target (FSM.initial M) pP' = q'" and "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>pP'. \<lbrakk>target (FSM.initial M) pP' = q'; 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:
target (FSM.initial M) pP' = q'
RP M q q' pP p PS M' = insert pP' (R M q q' pP p)

goal (1 subgoal):
 1. pR \<notin> R M q q' pP p \<Longrightarrow> target (FSM.initial M) pR = q'
[PROOF STEP]
have "pR = pP'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pR = pP'
[PROOF STEP]
using \<open>RP M q q' pP p PS M' = insert pP' (R M q q' pP p)\<close> \<open>pR \<in> (RP M q q' pP p PS M')\<close> False
[PROOF STATE]
proof (prove)
using this:
RP M q q' pP p PS M' = insert pP' (R M q q' pP p)
pR \<in> RP M q q' pP p PS M'
pR \<notin> R M q q' pP p

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

goal (1 subgoal):
 1. pR \<notin> R M q q' pP p \<Longrightarrow> target (FSM.initial M) pR = q'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial M) pR = q'
[PROOF STEP]
using \<open>target (FSM.initial M) pP' = q'\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pP' = q'

goal (1 subgoal):
 1. target (FSM.initial M) pR = q'
[PROOF STEP]
unfolding \<open>pR = pP'\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pP' = q'

goal (1 subgoal):
 1. target (FSM.initial M) pP' = q'
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
target (FSM.initial M) pR = q'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
target (FSM.initial M) pR = q'

goal:
No subgoals!
[PROOF STEP]
qed