[STATEMENT]
lemma R_count :
  assumes "minimal_sequence_to_failure_extending_preamble_path M M' PS pP io"
  and     "observable M"
  and     "observable M'"
  and     "\<And> q P. (q, P) \<in> PS \<Longrightarrow> is_preamble P M q"
  and     "path M (target (initial M) pP) p"
  and     "butlast io = p_io p @ ioX"
shows "card (\<Union> (image (\<lambda> pR . io_targets M' (p_io pR) (initial M')) (R M (target (initial M) pP) q' pP p))) = card (R M (target (initial M) pP) q' pP p)"
  (is "card ?Tgts = card ?R")
and   "\<And> pR . pR \<in> (R M (target (initial M) pP) q' pP p) \<Longrightarrow> \<exists> q . io_targets M' (p_io pR) (initial M') = {q}"
and   "\<And> pR1 pR2 . pR1 \<in> (R M (target (initial M) pP) q' pP p) \<Longrightarrow>
                    pR2 \<in> (R M (target (initial M) pP) q' pP p) \<Longrightarrow>
                    pR1 \<noteq> pR2 \<Longrightarrow>
                    io_targets M' (p_io pR1) (initial M') \<inter> io_targets M' (p_io pR2) (initial M') = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p) &&& (\<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}) &&& (\<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "sequence_to_failure_extending_preamble_path M M' PS pP io"
  and  "\<And> p' io' . sequence_to_failure_extending_preamble_path M M' PS p' io' \<Longrightarrow> length io \<le> length io'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sequence_to_failure_extending_preamble_path M M' PS pP io &&& (\<And>p' io'. sequence_to_failure_extending_preamble_path M M' PS p' io' \<Longrightarrow> length io \<le> length io')
[PROOF STEP]
using \<open>minimal_sequence_to_failure_extending_preamble_path M M' PS pP io\<close>
[PROOF STATE]
proof (prove)
using this:
minimal_sequence_to_failure_extending_preamble_path M M' PS pP io

goal (1 subgoal):
 1. sequence_to_failure_extending_preamble_path M M' PS pP io &&& (\<And>p' io'. sequence_to_failure_extending_preamble_path M M' PS p' io' \<Longrightarrow> length io \<le> length io')
[PROOF STEP]
unfolding minimal_sequence_to_failure_extending_preamble_path_def
[PROOF STATE]
proof (prove)
using this:
sequence_to_failure_extending_preamble_path M M' PS pP io \<and> (\<forall>p' io'. sequence_to_failure_extending_preamble_path M M' PS p' io' \<longrightarrow> length io \<le> length io')

goal (1 subgoal):
 1. sequence_to_failure_extending_preamble_path M M' PS pP io &&& (\<And>p' io'. sequence_to_failure_extending_preamble_path M M' PS p' io' \<Longrightarrow> length io \<le> length io')
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
sequence_to_failure_extending_preamble_path M M' PS pP io
sequence_to_failure_extending_preamble_path M M' PS ?p' ?io' \<Longrightarrow> length io \<le> length ?io'

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
obtain q P where "(q,P) \<in> PS"
              and  "path P (initial P) pP"
              and  "target (initial P) pP = q"
              and  "((p_io pP) @ butlast io) \<in> L M"
              and  "((p_io pP) @ io) \<notin> L M"
              and  "((p_io pP) @ io) \<in> L M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q P. \<lbrakk>(q, P) \<in> PS; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; p_io pP @ butlast io \<in> L M; p_io pP @ io \<notin> L M; p_io pP @ io \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>sequence_to_failure_extending_preamble_path M M' PS pP io\<close>
[PROOF STATE]
proof (prove)
using this:
sequence_to_failure_extending_preamble_path M M' PS pP io

goal (1 subgoal):
 1. (\<And>q P. \<lbrakk>(q, P) \<in> PS; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; p_io pP @ butlast io \<in> L M; p_io pP @ io \<notin> L M; p_io pP @ io \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding sequence_to_failure_extending_preamble_path_def
[PROOF STATE]
proof (prove)
using this:
\<exists>q P. q \<in> FSM.states M \<and> (q, P) \<in> PS \<and> path P (FSM.initial P) pP \<and> target (FSM.initial P) pP = q \<and> p_io pP @ butlast io \<in> L M \<and> p_io pP @ io \<notin> L M \<and> p_io pP @ io \<in> L M'

goal (1 subgoal):
 1. (\<And>q P. \<lbrakk>(q, P) \<in> PS; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; p_io pP @ butlast io \<in> L M; p_io pP @ io \<notin> L M; p_io pP @ io \<in> L M'\<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
p_io pP @ butlast io \<in> L M
p_io pP @ io \<notin> L M
p_io pP @ io \<in> L M'

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "is_preamble P M q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_preamble P M q
[PROOF STEP]
using \<open>(q,P) \<in> PS\<close> \<open>\<And> q P. (q, P) \<in> PS \<Longrightarrow> is_preamble P M q\<close>
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> PS
(?q, ?P) \<in> PS \<Longrightarrow> is_preamble ?P M ?q

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

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_preamble P M q
[PROOF STEP]
have "q \<in> states M"
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q

goal (1 subgoal):
 1. q \<in> FSM.states 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'\<in>reachable_states P. (q = q' \<or> \<not> deadlock_state P q') \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P. t_source t = q' \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q' \<and> t_input t' = x \<longrightarrow> t' \<in> FSM.transitions P)))

goal (1 subgoal):
 1. q \<in> FSM.states M
[PROOF STEP]
by (metis \<open>path P (FSM.initial P) pP\<close> \<open>target (FSM.initial P) pP = q\<close> path_target_is_state submachine_path)
[PROOF STATE]
proof (state)
this:
q \<in> FSM.states M

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[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'\<in>reachable_states P. (q = q' \<or> \<not> deadlock_state P q') \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P. t_source t = q' \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q' \<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 (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "path M (initial M) pP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path M (FSM.initial M) pP
[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) pP
[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'\<in>reachable_states P. (q = q' \<or> \<not> deadlock_state P q') \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P. t_source t = q' \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q' \<and> t_input t' = x \<longrightarrow> t' \<in> FSM.transitions P)))

goal (1 subgoal):
 1. path M (FSM.initial M) pP
[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'\<in>reachable_states P. (q = q' \<or> \<not> deadlock_state P q') \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P. t_source t = q' \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q' \<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) pP
[PROOF STEP]
using \<open>path P (FSM.initial P) pP\<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'\<in>reachable_states P. (q = q' \<or> \<not> deadlock_state P q') \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P. t_source t = q' \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q' \<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) pP

goal (1 subgoal):
 1. path M (FSM.initial M) pP
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) pP

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "target (initial M) pP = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial M) pP = q
[PROOF STEP]
using \<open>target (initial P) pP = q\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial P) pP = q

goal (1 subgoal):
 1. target (FSM.initial M) pP = q
[PROOF STEP]
unfolding \<open>initial P = initial M\<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) pP = q

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target (FSM.initial M) pP = q
[PROOF STEP]
have "path M q p"
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pP = q

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

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

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "io \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io \<noteq> []
[PROOF STEP]
using \<open>((p_io pP) @ butlast io) \<in> L M\<close> \<open>((p_io pP) @ io) \<notin> L M\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pP @ butlast io \<in> L M
p_io pP @ io \<notin> L M

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

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
(* get the full path along (butlast io) in M, of which p is a (possibly proper) prefix *)
[PROOF STATE]
proof (state)
this:
io \<noteq> []

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
obtain pX where "path M (target (initial M) pP) (p@pX)" and "p_io (p@pX) = butlast io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "p_io pP @ p_io p @ ioX \<in> L M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io pP @ p_io p @ ioX \<in> L M
[PROOF STEP]
using \<open>((p_io pP) @ butlast io) \<in> L M\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pP @ butlast io \<in> L M

goal (1 subgoal):
 1. p_io pP @ p_io p @ ioX \<in> L M
[PROOF STEP]
unfolding \<open>butlast io = p_io p @ ioX\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pP @ p_io p @ ioX \<in> L M

goal (1 subgoal):
 1. p_io pP @ p_io p @ ioX \<in> L M
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
p_io pP @ p_io p @ ioX \<in> L M

goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain p1 p23 where "path M (FSM.initial M) p1"
                    and "path M (target (FSM.initial M) p1) p23"
                    and "p_io p1 = p_io pP"
                    and "p_io p23 = p_io p @ ioX"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p1 p23. \<lbrakk>path M (FSM.initial M) p1; path M (target (FSM.initial M) p1) p23; p_io p1 = p_io pP; p_io p23 = p_io p @ ioX\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using language_state_split[OF \<open>p_io pP @ p_io p @ ioX \<in> L M\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>p1 p2. \<lbrakk>path M (FSM.initial M) p1; path M (target (FSM.initial M) p1) p2; p_io p1 = p_io pP; p_io p2 = p_io p @ ioX\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p1 p23. \<lbrakk>path M (FSM.initial M) p1; path M (target (FSM.initial M) p1) p23; p_io p1 = p_io pP; p_io p23 = p_io p @ ioX\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) p1
path M (target (FSM.initial M) p1) p23
p_io p1 = p_io pP
p_io p23 = p_io p @ ioX

goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "p1 = pP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 = pP
[PROOF STEP]
using observable_path_unique[OF \<open>observable M\<close> \<open>path M (FSM.initial M) p1\<close> \<open>path M (FSM.initial M) pP\<close> \<open>p_io p1 = p_io pP\<close>]
[PROOF STATE]
proof (prove)
using this:
p1 = pP

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

goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p1 = pP
[PROOF STEP]
have "path M (target (FSM.initial M) pP) p23"
[PROOF STATE]
proof (prove)
using this:
p1 = pP

goal (1 subgoal):
 1. path M (target (FSM.initial M) pP) p23
[PROOF STEP]
using \<open>path M (target (FSM.initial M) p1) p23\<close>
[PROOF STATE]
proof (prove)
using this:
p1 = pP
path M (target (FSM.initial M) p1) p23

goal (1 subgoal):
 1. path M (target (FSM.initial M) pP) p23
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path M (target (FSM.initial M) pP) p23

goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path M (target (FSM.initial M) pP) p23
[PROOF STEP]
have "p_io p @ ioX \<in> LS M (target (initial M) pP)"
[PROOF STATE]
proof (prove)
using this:
path M (target (FSM.initial M) pP) p23

goal (1 subgoal):
 1. p_io p @ ioX \<in> LS M (target (FSM.initial M) pP)
[PROOF STEP]
using \<open>p_io p23 = p_io p @ ioX\<close> language_state_containment
[PROOF STATE]
proof (prove)
using this:
path M (target (FSM.initial M) pP) p23
p_io p23 = p_io p @ ioX
\<lbrakk>path ?M ?q ?p; p_io ?p = ?io\<rbrakk> \<Longrightarrow> ?io \<in> LS ?M ?q

goal (1 subgoal):
 1. p_io p @ ioX \<in> LS M (target (FSM.initial M) pP)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_io p @ ioX \<in> LS M (target (FSM.initial M) pP)

goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain p2 p3 where "path M (target (FSM.initial M) pP) p2"
                   and "path M (target (target (FSM.initial M) pP) p2) p3"
                   and "p_io p2 = p_io p"
                   and "p_io p3 = ioX"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p2 p3. \<lbrakk>path M (target (FSM.initial M) pP) p2; path M (target (target (FSM.initial M) pP) p2) p3; p_io p2 = p_io p; p_io p3 = ioX\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using language_state_split[OF \<open>p_io p @ ioX \<in> LS M (target (initial M) pP)\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>p1 p2. \<lbrakk>path M (target (FSM.initial M) pP) p1; path M (target (target (FSM.initial M) pP) p1) p2; p_io p1 = p_io p; p_io p2 = ioX\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p2 p3. \<lbrakk>path M (target (FSM.initial M) pP) p2; path M (target (target (FSM.initial M) pP) p2) p3; p_io p2 = p_io p; p_io p3 = ioX\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path M (target (FSM.initial M) pP) p2
path M (target (target (FSM.initial M) pP) p2) p3
p_io p2 = p_io p
p_io p3 = ioX

goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "p2 = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p2 = p
[PROOF STEP]
using observable_path_unique[OF \<open>observable M\<close> \<open>path M (target (FSM.initial M) pP) p2\<close> \<open>path M (target (FSM.initial M) pP) p\<close> \<open>p_io p2 = p_io p\<close>]
[PROOF STATE]
proof (prove)
using this:
p2 = p

goal (1 subgoal):
 1. p2 = p
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
p2 = p

goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p2 = p
[PROOF STEP]
have "path M (target (FSM.initial M) pP) (p@p3)"
[PROOF STATE]
proof (prove)
using this:
p2 = p

goal (1 subgoal):
 1. path M (target (FSM.initial M) pP) (p @ p3)
[PROOF STEP]
using \<open>path M (target (FSM.initial M) pP) p\<close> \<open>path M (target (target (FSM.initial M) pP) p2) p3\<close>
[PROOF STATE]
proof (prove)
using this:
p2 = p
path M (target (FSM.initial M) pP) p
path M (target (target (FSM.initial M) pP) p2) p3

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

goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path M (target (FSM.initial M) pP) (p @ p3)

goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "p_io (p@p3) = butlast io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (p @ p3) = butlast io
[PROOF STEP]
unfolding \<open>butlast io = p_io p @ ioX\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (p @ p3) = p_io p @ ioX
[PROOF STEP]
using \<open>p_io p3 = ioX\<close>
[PROOF STATE]
proof (prove)
using this:
p_io p3 = ioX

goal (1 subgoal):
 1. p_io (p @ p3) = p_io p @ ioX
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_io (p @ p3) = butlast io

goal (1 subgoal):
 1. (\<And>pX. \<lbrakk>path M (target (FSM.initial M) pP) (p @ pX); p_io (p @ pX) = butlast io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path M (target (FSM.initial M) pP) (p @ p3)
p_io (p @ p3) = butlast io
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path M (target (FSM.initial M) pP) (p @ p3)
p_io (p @ p3) = butlast io

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of p3]
[PROOF STATE]
proof (prove)
using this:
path M (target (FSM.initial M) pP) (p @ p3)
p_io (p @ p3) = butlast io
\<lbrakk>path M (target (FSM.initial M) pP) (p @ p3); p_io (p @ p3) = butlast io\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
path M (target (FSM.initial M) pP) (p @ pX)
p_io (p @ pX) = butlast io

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
(* finiteness properties *)
[PROOF STATE]
proof (state)
this:
path M (target (FSM.initial M) pP) (p @ pX)
p_io (p @ pX) = butlast io

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "finite ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
using finite_R[OF \<open>path M (target (initial M) pP) p\<close>]
[PROOF STATE]
proof (prove)
using this:
finite (R M (target (FSM.initial M) pP) ?q' ?pP p)

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

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (R M (target (FSM.initial M) pP) q' pP p)

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "\<And> pR . pR \<in> ?R \<Longrightarrow> finite (io_targets M' (p_io pR) (initial M'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> finite (io_targets M' (p_io pR) (FSM.initial M'))
[PROOF STEP]
using io_targets_finite
[PROOF STATE]
proof (prove)
using this:
finite (io_targets ?M ?io ?q)

goal (1 subgoal):
 1. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> finite (io_targets M' (p_io pR) (FSM.initial M'))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> finite (io_targets M' (p_io ?pR) (FSM.initial M'))

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (R M (target (FSM.initial M) pP) q' pP p)
?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> finite (io_targets M' (p_io ?pR) (FSM.initial M'))
[PROOF STEP]
have "finite ?Tgts"
[PROOF STATE]
proof (prove)
using this:
finite (R M (target (FSM.initial M) pP) q' pP p)
?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> finite (io_targets M' (p_io ?pR) (FSM.initial M'))

goal (1 subgoal):
 1. finite (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M'))

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
(* path properties *)
[PROOF STATE]
proof (state)
this:
finite (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M'))

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
obtain pP' p' where "path M' (FSM.initial M') pP'"
                and   "path M' (target (FSM.initial M') pP') p'"
                and   "p_io pP' = p_io pP"
                and   "p_io p' = io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pP' p'. \<lbrakk>path M' (FSM.initial M') pP'; path M' (target (FSM.initial M') pP') p'; p_io pP' = p_io pP; p_io p' = io\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using language_state_split[OF \<open>((p_io pP) @ io) \<in> L M'\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>p1 p2. \<lbrakk>path M' (FSM.initial M') p1; path M' (target (FSM.initial M') p1) p2; p_io p1 = p_io pP; p_io p2 = io\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "length p \<le> length (butlast io)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p \<le> length (butlast io)
[PROOF STEP]
using \<open>butlast io = p_io p @ ioX\<close>
[PROOF STATE]
proof (prove)
using this:
butlast io = p_io p @ ioX

goal (1 subgoal):
 1. length p \<le> length (butlast io)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length p \<le> length (butlast io)

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length p \<le> length (butlast io)

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "length (butlast io) < length io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (butlast io) < length io
[PROOF STEP]
using \<open>io \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
io \<noteq> []

goal (1 subgoal):
 1. length (butlast io) < length io
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (butlast io) < length io

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length p \<le> length (butlast io)
length (butlast io) < length io
[PROOF STEP]
have "length p < length p'"
[PROOF STATE]
proof (prove)
using this:
length p \<le> length (butlast io)
length (butlast io) < length io

goal (1 subgoal):
 1. length p < length p'
[PROOF STEP]
unfolding \<open>p_io p' = io\<close> length_map[of "(\<lambda> t . (t_input t, t_output t))", symmetric]
[PROOF STATE]
proof (prove)
using this:
length (p_io p) \<le> length (butlast io)
length (butlast io) < length io

goal (1 subgoal):
 1. length (p_io p) < length io
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length p < length p'

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
let ?q = "(target (FSM.initial M') pP')"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "\<And> pR . pP@pR \<in> ?R \<Longrightarrow> path M' ?q (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
fix pR
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
assume "pP@pR \<in> ?R"
[PROOF STATE]
proof (state)
this:
pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p
[PROOF STEP]
have  "pR = take (length pR) p \<and> length pR \<le> length p"
[PROOF STATE]
proof (prove)
using this:
pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p

goal (1 subgoal):
 1. pR = take (length pR) p \<and> length pR \<le> length p
[PROOF STEP]
using R_component(1,2)
[PROOF STATE]
proof (prove)
using this:
pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p
?pP @ ?pR \<in> R ?M ?q ?q' ?pP ?p \<Longrightarrow> ?pR = take (length ?pR) ?p
?pP @ ?pR \<in> R ?M ?q ?q' ?pP ?p \<Longrightarrow> length ?pR \<le> length ?p

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

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR = take (length pR) p \<and> length pR \<le> length p
[PROOF STEP]
have "p_io pR = take (length pR) (butlast io)"
[PROOF STATE]
proof (prove)
using this:
pR = take (length pR) p \<and> length pR \<le> length p

goal (1 subgoal):
 1. p_io pR = take (length pR) (butlast io)
[PROOF STEP]
unfolding \<open>butlast io = p_io p @ ioX\<close>
[PROOF STATE]
proof (prove)
using this:
pR = take (length pR) p \<and> length pR \<le> length p

goal (1 subgoal):
 1. p_io pR = take (length pR) (p_io p @ ioX)
[PROOF STEP]
by (metis (no_types, lifting) length_map take_le take_map)
[PROOF STATE]
proof (state)
this:
p_io pR = take (length pR) (butlast io)

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p_io pR = take (length pR) (butlast io)

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
have "p_io (take (length pR) p') = take (length pR) io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (take (length pR) p') = take (length pR) io
[PROOF STEP]
by (metis (full_types) \<open>p_io p' = io\<close> take_map)
[PROOF STATE]
proof (state)
this:
p_io (take (length pR) p') = take (length pR) io

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p_io (take (length pR) p') = take (length pR) io

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
have "take (length pR) (butlast io) = take (length pR) io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length pR) (butlast io) = take (length pR) io
[PROOF STEP]
by (meson \<open>length (butlast io) < length io\<close> \<open>length p \<le> length (butlast io)\<close>
            \<open>pR = take (length pR) p \<and> length pR \<le> length p\<close> dual_order.strict_trans2 take_butlast)
[PROOF STATE]
proof (state)
this:
take (length pR) (butlast io) = take (length pR) io

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p_io pR = take (length pR) (butlast io)
p_io (take (length pR) p') = take (length pR) io
take (length pR) (butlast io) = take (length pR) io
[PROOF STEP]
have "p_io (take (length pR) p') = p_io pR"
[PROOF STATE]
proof (prove)
using this:
p_io pR = take (length pR) (butlast io)
p_io (take (length pR) p') = take (length pR) io
take (length pR) (butlast io) = take (length pR) io

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

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p_io (take (length pR) p') = p_io pR

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[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 \<open>path M' (target (FSM.initial M') pP') p'\<close>
[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. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p_io (take (length pR) p') = p_io pR
path M' (target (FSM.initial M') pP') (take (length pR) p')
[PROOF STEP]
show "path M' ?q (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR"
[PROOF STATE]
proof (prove)
using this:
p_io (take (length pR) p') = p_io pR
path M' (target (FSM.initial M') pP') (take (length pR) p')

goal (1 subgoal):
 1. path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path M' (target (FSM.initial M') pP') (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pP @ ?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length ?pR) p') \<and> p_io (take (length ?pR) p') = p_io ?pR

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
(* every element in R reaches exactly one state in M' *)
[PROOF STATE]
proof (state)
this:
pP @ ?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length ?pR) p') \<and> p_io (take (length ?pR) p') = p_io ?pR

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have singleton_prop': "\<And> pR . pP@pR \<in> ?R \<Longrightarrow> io_targets M' (p_io (pP@pR)) (initial M') = {target ?q (take (length pR) p')}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io (pP @ 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. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io (pP @ pR)) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR) p')}
[PROOF STEP]
fix pR
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io (pP @ pR)) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR) p')}
[PROOF STEP]
assume "pP@pR \<in> ?R"
[PROOF STATE]
proof (state)
this:
pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p

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

goal (1 subgoal):
 1. path M' (target (FSM.initial M') pP') (take (length pR) p') &&& p_io (take (length pR) p') = p_io pR
[PROOF STEP]
using \<open>\<And> pR . pP@pR \<in> ?R \<Longrightarrow> path M' ?q (take (length pR) p') \<and> p_io (take (length pR) p') = p_io pR\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p
pP @ ?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> path M' (target (FSM.initial M') pP') (take (length ?pR) p') \<and> p_io (take (length ?pR) p') = p_io ?pR

goal (1 subgoal):
 1. path M' (target (FSM.initial M') pP') (take (length pR) p') &&& p_io (take (length pR) p') = p_io pR
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
path M' (target (FSM.initial M') pP') (take (length pR) p')
p_io (take (length pR) p') = p_io pR

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io (pP @ 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. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io (pP @ 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@pR))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (pP' @ take (length pR) p') = p_io (pP @ pR)
[PROOF STEP]
using \<open>p_io pP' = p_io pP\<close> \<open>p_io (take (length pR) p') = p_io pR\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pP' = p_io pP
p_io (take (length pR) p') = p_io pR

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

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io (pP @ 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. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io (pP @ 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@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 @ 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 @ 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 @ 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 @ 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 @ pR)) (FSM.initial M')

goal (1 subgoal):
 1. \<And>pR. pP @ pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io (pP @ pR)) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR) p')}
[PROOF STEP]
show "io_targets M' (p_io (pP@pR)) (initial M') = {target ?q (take (length pR) p')}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io (pP @ 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 @ pR)) (FSM.initial M') = {q'} \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ 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@pR)) (FSM.initial M')\<close> singleton_iff)
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io (pP @ pR)) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR) p')}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pP @ ?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io (pP @ ?pR)) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length ?pR) p')}

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have singleton_prop: "\<And> pR . pR \<in> ?R \<Longrightarrow> io_targets M' (p_io pR) (initial M') = {target ?q (take (length pR - length pP) p')}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR - length pP) p')}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR - length pP) p')}
[PROOF STEP]
fix pR
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR - length pP) p')}
[PROOF STEP]
assume "pR \<in> ?R"
[PROOF STATE]
proof (state)
this:
pR \<in> R M (target (FSM.initial M) pP) q' pP p

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

goal (1 subgoal):
 1. (\<And>pR'. pR = pP @ pR' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using R_component_ob[of _ M "(target (FSM.initial M) pP)" q' pP p]
[PROOF STATE]
proof (prove)
using this:
pR \<in> R M (target (FSM.initial M) pP) q' pP p
\<lbrakk>?pR' \<in> R M (target (FSM.initial M) pP) q' pP p; \<And>pR. ?pR' = pP @ pR \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR - length pP) p')}
[PROOF STEP]
have **: "(length (pP @ pR') - length pP) = length pR'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (pP @ pR') - length pP = length pR'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (pP @ pR') - length pP = length pR'

goal (1 subgoal):
 1. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR - length pP) p')}
[PROOF STEP]
show "io_targets M' (p_io pR) (initial M') = {target ?q (take (length pR - length pP) p')}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR - length pP) p')}
[PROOF STEP]
using singleton_prop'[of pR'] \<open>pR \<in> ?R\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR' \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io (pP @ pR')) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR') p')}
pR \<in> R M (target (FSM.initial M) pP) q' pP p

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

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR')) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR') p')}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR - length pP) p')}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io ?pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length ?pR - length pP) p')}

goal (3 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io ?pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length ?pR - length pP) p')}
[PROOF STEP]
show "\<And> pR . pR \<in> ?R \<Longrightarrow> \<exists> q . io_targets M' (p_io pR) (initial M') = {q}"
[PROOF STATE]
proof (prove)
using this:
?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io ?pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length ?pR - length pP) p')}

goal (1 subgoal):
 1. \<And>pR. pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io ?pR) (FSM.initial M') = {q}

goal (2 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
(* distinct elements in R reach distinct states in M' *)
[PROOF STATE]
proof (state)
this:
?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>q. io_targets M' (p_io ?pR) (FSM.initial M') = {q}

goal (2 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have pairwise_dist_prop': "\<And> pR1 pR2 . pP@pR1 \<in> ?R \<Longrightarrow> pP@pR2 \<in> ?R \<Longrightarrow> pR1 \<noteq> pR2 \<Longrightarrow> io_targets M' (p_io (pP@pR1)) (initial M') \<inter> io_targets M' (p_io (pP@pR2)) (initial M') = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
have diff_prop: "\<And> pR1 pR2 . pP@pR1 \<in> ?R \<Longrightarrow> pP@pR2 \<in> ?R \<Longrightarrow> length pR1 < length pR2 \<Longrightarrow> io_targets M' (p_io (pP@pR1)) (initial M') \<inter> io_targets M' (p_io (pP@pR2)) (initial M') = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
fix pR1 pR2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
assume "pP@pR1 \<in> ?R" and "pP@pR2 \<in> ?R" and "length pR1 < length pR2"
[PROOF STATE]
proof (state)
this:
pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p
pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p
length pR1 < length pR2

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
let ?i = "length pR1 - 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
let ?j = "length pR2 - 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
have "pR1 = take (length pR1) p" and \<open>length pR1 \<le> length p\<close> and "t_target (p ! ?i) = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pR1 = take (length pR1) p &&& length pR1 \<le> length p &&& t_target (p ! (length pR1 - 1)) = q'
[PROOF STEP]
using R_component[OF \<open>pP@pR1 \<in> ?R\<close>]
[PROOF STATE]
proof (prove)
using this:
pR1 = take (length pR1) p
length pR1 \<le> length p
t_target (p ! (length pR1 - 1)) = q'
pR1 \<noteq> []

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

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
have "length pR1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length pR1 \<noteq> 0
[PROOF STEP]
using \<open>pP@pR1 \<in> ?R\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p

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

goal (1 subgoal):
 1. length pR1 \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length pR1 \<noteq> 0

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length pR1 \<noteq> 0
[PROOF STEP]
have "?i < ?j"
[PROOF STATE]
proof (prove)
using this:
length pR1 \<noteq> 0

goal (1 subgoal):
 1. length pR1 - 1 < length pR2 - 1
[PROOF STEP]
using \<open>length pR1 < length pR2\<close>
[PROOF STATE]
proof (prove)
using this:
length pR1 \<noteq> 0
length pR1 < length pR2

goal (1 subgoal):
 1. length pR1 - 1 < length pR2 - 1
[PROOF STEP]
by (simp add: less_diff_conv)
[PROOF STATE]
proof (state)
this:
length pR1 - 1 < length pR2 - 1

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
have "pR2 = take (length pR2) p" and \<open>length pR2 \<le> length p\<close> and "t_target (p ! ?j) = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pR2 = take (length pR2) p &&& length pR2 \<le> length p &&& t_target (p ! (length pR2 - 1)) = q'
[PROOF STEP]
using R_component[OF \<open>pP@pR2 \<in> ?R\<close>]
[PROOF STATE]
proof (prove)
using this:
pR2 = take (length pR2) p
length pR2 \<le> length p
t_target (p ! (length pR2 - 1)) = q'
pR2 \<noteq> []

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

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR2 = take (length pR2) p
length pR2 \<le> length p
t_target (p ! (length pR2 - 1)) = q'
[PROOF STEP]
have "?j < length (butlast io)"
[PROOF STATE]
proof (prove)
using this:
pR2 = take (length pR2) p
length pR2 \<le> length p
t_target (p ! (length pR2 - 1)) = q'

goal (1 subgoal):
 1. length pR2 - 1 < length (butlast io)
[PROOF STEP]
using \<open>length p \<le> length (butlast io)\<close> \<open>length pR1 < length pR2\<close>
[PROOF STATE]
proof (prove)
using this:
pR2 = take (length pR2) p
length pR2 \<le> length p
t_target (p ! (length pR2 - 1)) = q'
length p \<le> length (butlast io)
length pR1 < length pR2

goal (1 subgoal):
 1. length pR2 - 1 < length (butlast io)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
length pR2 - 1 < length (butlast io)

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
have "?q \<in> io_targets M' (p_io pP) (FSM.initial M')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial M') pP' \<in> io_targets M' (p_io pP) (FSM.initial M')
[PROOF STEP]
unfolding \<open>p_io pP' = p_io pP\<close>[symmetric] io_targets.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial M') pP' \<in> {target (FSM.initial M') p |p. path M' (FSM.initial M') p \<and> p_io p = p_io pP'}
[PROOF STEP]
using \<open>path M' (initial M') pP'\<close>
[PROOF STATE]
proof (prove)
using this:
path M' (FSM.initial M') pP'

goal (1 subgoal):
 1. target (FSM.initial M') pP' \<in> {target (FSM.initial M') p |p. path M' (FSM.initial M') p \<and> p_io p = p_io pP'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target (FSM.initial M') pP' \<in> io_targets M' (p_io pP) (FSM.initial M')

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
have "t_target (p ! ?i) = t_target (p ! ?j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_target (p ! (length pR1 - 1)) = t_target (p ! (length pR2 - 1))
[PROOF STEP]
using \<open>t_target (p ! ?i) = q'\<close> \<open>t_target (p ! ?j) = q'\<close>
[PROOF STATE]
proof (prove)
using this:
t_target (p ! (length pR1 - 1)) = q'
t_target (p ! (length pR2 - 1)) = q'

goal (1 subgoal):
 1. t_target (p ! (length pR1 - 1)) = t_target (p ! (length pR2 - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t_target (p ! (length pR1 - 1)) = t_target (p ! (length pR2 - 1))

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t_target (p ! (length pR1 - 1)) = t_target (p ! (length pR2 - 1))

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
have "(p @ pX) ! ?i = p ! ?i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p @ pX) ! (length pR1 - 1) = p ! (length pR1 - 1)
[PROOF STEP]
by (meson \<open>length pR1 < length pR2\<close> \<open>length pR2 \<le> length p\<close> less_imp_diff_less less_le_trans nth_append)
[PROOF STATE]
proof (state)
this:
(p @ pX) ! (length pR1 - 1) = p ! (length pR1 - 1)

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(p @ pX) ! (length pR1 - 1) = p ! (length pR1 - 1)

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
have "(p @ pX) ! ?j = p ! ?j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p @ pX) ! (length pR2 - 1) = p ! (length pR2 - 1)
[PROOF STEP]
by (metis (no_types) \<open>length pR1 < length pR2\<close> \<open>pR2 = take (length pR2) p\<close> diff_less less_imp_diff_less less_nat_zero_code less_numeral_extra(1) not_le_imp_less not_less_iff_gr_or_eq nth_append take_all)
[PROOF STATE]
proof (state)
this:
(p @ pX) ! (length pR2 - 1) = p ! (length pR2 - 1)

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t_target (p ! (length pR1 - 1)) = t_target (p ! (length pR2 - 1))
(p @ pX) ! (length pR1 - 1) = p ! (length pR1 - 1)
(p @ pX) ! (length pR2 - 1) = p ! (length pR2 - 1)
[PROOF STEP]
have "t_target (p' ! ?i) \<noteq> t_target (p' ! ?j)"
[PROOF STATE]
proof (prove)
using this:
t_target (p ! (length pR1 - 1)) = t_target (p ! (length pR2 - 1))
(p @ pX) ! (length pR1 - 1) = p ! (length pR1 - 1)
(p @ pX) ! (length pR2 - 1) = p ! (length pR2 - 1)

goal (1 subgoal):
 1. t_target (p' ! (length pR1 - 1)) \<noteq> t_target (p' ! (length pR2 - 1))
[PROOF STEP]
using minimal_sequence_to_failure_extending_preamble_no_repetitions_along_path[OF assms(1,2) \<open>path M (target (initial M) pP) (p@pX)\<close> \<open>p_io (p @ pX) = butlast io\<close> \<open>?q \<in> io_targets M' (p_io pP) (FSM.initial M')\<close> \<open>path M' (target (FSM.initial M') pP') p'\<close> \<open>p_io p' = io\<close> \<open>?i < ?j\<close> \<open>?j < length (butlast io)\<close> assms(4)]
[PROOF STATE]
proof (prove)
using this:
t_target (p ! (length pR1 - 1)) = t_target (p ! (length pR2 - 1))
(p @ pX) ! (length pR1 - 1) = p ! (length pR1 - 1)
(p @ pX) ! (length pR2 - 1) = p ! (length pR2 - 1)
(\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS) \<Longrightarrow> t_target ((p @ pX) ! (length pR1 - 1)) \<noteq> t_target ((p @ pX) ! (length pR2 - 1)) \<or> t_target (p' ! (length pR1 - 1)) \<noteq> t_target (p' ! (length pR2 - 1))

goal (1 subgoal):
 1. t_target (p' ! (length pR1 - 1)) \<noteq> t_target (p' ! (length pR2 - 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t_target (p' ! (length pR1 - 1)) \<noteq> t_target (p' ! (length pR2 - 1))

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
have t1: "io_targets M' (p_io (pP@pR1)) (initial M') = {t_target (p' ! ?i)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {t_target (p' ! (length pR1 - 1))}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {t_target (p' ! (length pR1 - 1))}
[PROOF STEP]
have "(p' ! ?i) = last (take (length pR1) p')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' ! (length pR1 - 1) = last (take (length pR1) p')
[PROOF STEP]
using \<open>length pR1 \<le> length p\<close> \<open>length p < length p'\<close>
[PROOF STATE]
proof (prove)
using this:
length pR1 \<le> length p
length p < length p'

goal (1 subgoal):
 1. p' ! (length pR1 - 1) = last (take (length pR1) p')
[PROOF STEP]
by (metis Suc_diff_1 \<open>length pR1 \<noteq> 0\<close> dual_order.strict_trans2 length_0_conv length_greater_0_conv less_imp_diff_less take_last_index)
[PROOF STATE]
proof (state)
this:
p' ! (length pR1 - 1) = last (take (length pR1) p')

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {t_target (p' ! (length pR1 - 1))}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' ! (length pR1 - 1) = last (take (length pR1) p')
[PROOF STEP]
have *: "target (target (FSM.initial M') pP') (take (length pR1) p') = t_target (p' ! ?i)"
[PROOF STATE]
proof (prove)
using this:
p' ! (length pR1 - 1) = last (take (length pR1) p')

goal (1 subgoal):
 1. target (target (FSM.initial M') pP') (take (length pR1) p') = t_target (p' ! (length pR1 - 1))
[PROOF STEP]
unfolding target.simps visited_states.simps
[PROOF STATE]
proof (prove)
using this:
p' ! (length pR1 - 1) = last (take (length pR1) p')

goal (1 subgoal):
 1. last (last (FSM.initial M' # map t_target pP') # map t_target (take (length pR1) p')) = t_target (p' ! (length pR1 - 1))
[PROOF STEP]
by (metis (no_types, lifting) \<open>length p < length p'\<close> \<open>length pR1 \<noteq> 0\<close> gr_implies_not_zero last.simps last_map length_0_conv map_is_Nil_conv take_eq_Nil)
[PROOF STATE]
proof (state)
this:
target (target (FSM.initial M') pP') (take (length pR1) p') = t_target (p' ! (length pR1 - 1))

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {t_target (p' ! (length pR1 - 1))}
[PROOF STEP]
have **: "(length (pP @ pR1) - length pP) = length pR1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (pP @ pR1) - length pP = length pR1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (pP @ pR1) - length pP = length pR1

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {t_target (p' ! (length pR1 - 1))}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {t_target (p' ! (length pR1 - 1))}
[PROOF STEP]
using singleton_prop[OF \<open>pP@pR1 \<in> ?R\<close>]
[PROOF STATE]
proof (prove)
using this:
io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length (pP @ pR1) - length pP) p')}

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {t_target (p' ! (length pR1 - 1))}
[PROOF STEP]
unfolding * **
[PROOF STATE]
proof (prove)
using this:
io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {t_target (p' ! (length pR1 - 1))}

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {t_target (p' ! (length pR1 - 1))}
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {t_target (p' ! (length pR1 - 1))}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {t_target (p' ! (length pR1 - 1))}

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
have t2: "io_targets M' (p_io (pP@pR2)) (initial M') = {t_target (p' ! ?j)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {t_target (p' ! (length pR2 - 1))}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {t_target (p' ! (length pR2 - 1))}
[PROOF STEP]
have "(p' ! ?j) = last (take (length pR2) p')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' ! (length pR2 - 1) = last (take (length pR2) p')
[PROOF STEP]
using \<open>length pR2 \<le> length p\<close> \<open>length p < length p'\<close>
[PROOF STATE]
proof (prove)
using this:
length pR2 \<le> length p
length p < length p'

goal (1 subgoal):
 1. p' ! (length pR2 - 1) = last (take (length pR2) p')
[PROOF STEP]
by (metis Suc_diff_1 \<open>length pR1 - 1 < length pR2 - 1\<close> le_less_trans less_imp_diff_less
                linorder_neqE_nat not_less_zero take_last_index zero_less_diff)
[PROOF STATE]
proof (state)
this:
p' ! (length pR2 - 1) = last (take (length pR2) p')

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {t_target (p' ! (length pR2 - 1))}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p' ! (length pR2 - 1) = last (take (length pR2) p')
[PROOF STEP]
have *: "target (target (FSM.initial M') pP') (take (length pR2) p') = t_target (p' ! ?j)"
[PROOF STATE]
proof (prove)
using this:
p' ! (length pR2 - 1) = last (take (length pR2) p')

goal (1 subgoal):
 1. target (target (FSM.initial M') pP') (take (length pR2) p') = t_target (p' ! (length pR2 - 1))
[PROOF STEP]
unfolding target.simps visited_states.simps
[PROOF STATE]
proof (prove)
using this:
p' ! (length pR2 - 1) = last (take (length pR2) p')

goal (1 subgoal):
 1. last (last (FSM.initial M' # map t_target pP') # map t_target (take (length pR2) p')) = t_target (p' ! (length pR2 - 1))
[PROOF STEP]
by (metis (no_types, lifting) Nil_is_map_conv \<open>length p < length p'\<close> \<open>length pR1 < length pR2\<close>
                last.simps last_map list.size(3) not_less_zero take_eq_Nil)
[PROOF STATE]
proof (state)
this:
target (target (FSM.initial M') pP') (take (length pR2) p') = t_target (p' ! (length pR2 - 1))

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {t_target (p' ! (length pR2 - 1))}
[PROOF STEP]
have **: "(length (pP @ pR2) - length pP) = length pR2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (pP @ pR2) - length pP = length pR2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (pP @ pR2) - length pP = length pR2

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {t_target (p' ! (length pR2 - 1))}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {t_target (p' ! (length pR2 - 1))}
[PROOF STEP]
using singleton_prop'[OF \<open>pP@pR2 \<in> ?R\<close>]
[PROOF STATE]
proof (prove)
using this:
io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR2) p')}

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {t_target (p' ! (length pR2 - 1))}
[PROOF STEP]
unfolding * **
[PROOF STATE]
proof (prove)
using this:
io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {t_target (p' ! (length pR2 - 1))}

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {t_target (p' ! (length pR2 - 1))}
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {t_target (p' ! (length pR2 - 1))}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {t_target (p' ! (length pR2 - 1))}

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; length pR1 < length pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
show "io_targets M' (p_io (pP@pR1)) (initial M') \<inter> io_targets M' (p_io (pP@pR2)) (initial M') = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
using \<open>t_target (p' ! ?i) \<noteq> t_target (p' ! ?j)\<close>
[PROOF STATE]
proof (prove)
using this:
t_target (p' ! (length pR1 - 1)) \<noteq> t_target (p' ! (length pR2 - 1))

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
unfolding t1 t2
[PROOF STATE]
proof (prove)
using this:
t_target (p' ! (length pR1 - 1)) \<noteq> t_target (p' ! (length pR2 - 1))

goal (1 subgoal):
 1. {t_target (p' ! (length pR1 - 1))} \<inter> {t_target (p' ! (length pR2 - 1))} = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>pP @ ?pR1.0 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ ?pR2.0 \<in> R M (target (FSM.initial M) pP) q' pP p; length ?pR1.0 < length ?pR2.0\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ ?pR1.0)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ ?pR2.0)) (FSM.initial M') = {}

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
fix pR1 pR2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
assume "pP@pR1 \<in> ?R" and "pP@pR2 \<in> ?R" and "pR1 \<noteq> pR2"
[PROOF STATE]
proof (state)
this:
pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p
pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p
pR1 \<noteq> pR2

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p
pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p
pR1 \<noteq> pR2
[PROOF STEP]
have "length pR1 \<noteq> length pR2"
[PROOF STATE]
proof (prove)
using this:
pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p
pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p
pR1 \<noteq> pR2

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

goal (1 subgoal):
 1. length pR1 \<noteq> length pR2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length pR1 \<noteq> length pR2

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length pR1 \<noteq> length pR2
[PROOF STEP]
consider (a) "length pR1 < length pR2" | (b) "length pR2 < length pR1"
[PROOF STATE]
proof (prove)
using this:
length pR1 \<noteq> length pR2

goal (1 subgoal):
 1. \<lbrakk>length pR1 < length pR2 \<Longrightarrow> thesis; length pR2 < length pR1 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using nat_neq_iff
[PROOF STATE]
proof (prove)
using this:
length pR1 \<noteq> length pR2
(?m \<noteq> ?n) = (?m < ?n \<or> ?n < ?m)

goal (1 subgoal):
 1. \<lbrakk>length pR1 < length pR2 \<Longrightarrow> thesis; length pR2 < length pR1 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>length pR1 < length pR2 \<Longrightarrow> ?thesis; length pR2 < length pR1 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pP @ pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length pR1 < length pR2 \<Longrightarrow> ?thesis; length pR2 < length pR1 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "io_targets M' (p_io (pP@pR1)) (initial M') \<inter> io_targets M' (p_io (pP@pR2)) (initial M') = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length pR1 < length pR2 \<Longrightarrow> ?thesis; length pR2 < length pR1 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length pR1 < length pR2 \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
 2. length pR2 < length pR1 \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
case a
[PROOF STATE]
proof (state)
this:
length pR1 < length pR2

goal (2 subgoals):
 1. length pR1 < length pR2 \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
 2. length pR2 < length pR1 \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
using diff_prop[OF \<open>pP@pR1 \<in> ?R\<close> \<open>pP@pR2 \<in> ?R\<close> a]
[PROOF STATE]
proof (prove)
using this:
io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}

goal (1 subgoal):
 1. length pR2 < length pR1 \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length pR2 < length pR1 \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
case b
[PROOF STATE]
proof (state)
this:
length pR2 < length pR1

goal (1 subgoal):
 1. length pR2 < length pR1 \<Longrightarrow> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
using diff_prop[OF \<open>pP@pR2 \<in> ?R\<close> \<open>pP@pR1 \<in> ?R\<close> b]
[PROOF STATE]
proof (prove)
using this:
io_targets M' (p_io (pP @ pR2)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR1)) (FSM.initial M') = {}

goal (1 subgoal):
 1. io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io (pP @ pR1)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ pR2)) (FSM.initial M') = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>pP @ ?pR1.0 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ ?pR2.0 \<in> R M (target (FSM.initial M) pP) q' pP p; ?pR1.0 \<noteq> ?pR2.0\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ ?pR1.0)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ ?pR2.0)) (FSM.initial M') = {}

goal (2 subgoals):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
 2. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>pP @ ?pR1.0 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ ?pR2.0 \<in> R M (target (FSM.initial M) pP) q' pP p; ?pR1.0 \<noteq> ?pR2.0\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ ?pR1.0)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ ?pR2.0)) (FSM.initial M') = {}
[PROOF STEP]
show pairwise_dist_prop: "\<And> pR1 pR2 . pR1 \<in> ?R \<Longrightarrow> pR2 \<in> ?R \<Longrightarrow> pR1 \<noteq> pR2 \<Longrightarrow> io_targets M' (p_io pR1) (initial M') \<inter> io_targets M' (p_io pR2) (initial M') = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>pP @ ?pR1.0 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ ?pR2.0 \<in> R M (target (FSM.initial M) pP) q' pP p; ?pR1.0 \<noteq> ?pR2.0\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ ?pR1.0)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ ?pR2.0)) (FSM.initial M') = {}

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
using R_component_ob
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>pP @ ?pR1.0 \<in> R M (target (FSM.initial M) pP) q' pP p; pP @ ?pR2.0 \<in> R M (target (FSM.initial M) pP) q' pP p; ?pR1.0 \<noteq> ?pR2.0\<rbrakk> \<Longrightarrow> io_targets M' (p_io (pP @ ?pR1.0)) (FSM.initial M') \<inter> io_targets M' (p_io (pP @ ?pR2.0)) (FSM.initial M') = {}
\<lbrakk>?pR' \<in> R ?M ?q ?q' ?pP ?p; \<And>pR. ?pR' = ?pP @ pR \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p; pR2 \<in> R M (target (FSM.initial M) pP) q' pP p; pR1 \<noteq> pR2\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
\<lbrakk>?pR1.0 \<in> R M (target (FSM.initial M) pP) q' pP p; ?pR2.0 \<in> R M (target (FSM.initial M) pP) q' pP p; ?pR1.0 \<noteq> ?pR2.0\<rbrakk> \<Longrightarrow> io_targets M' (p_io ?pR1.0) (FSM.initial M') \<inter> io_targets M' (p_io ?pR2.0) (FSM.initial M') = {}

goal (1 subgoal):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
(* combining results *)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?pR1.0 \<in> R M (target (FSM.initial M) pP) q' pP p; ?pR2.0 \<in> R M (target (FSM.initial M) pP) q' pP p; ?pR1.0 \<noteq> ?pR2.0\<rbrakk> \<Longrightarrow> io_targets M' (p_io ?pR1.0) (FSM.initial M') \<inter> io_targets M' (p_io ?pR2.0) (FSM.initial M') = {}

goal (1 subgoal):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
let ?f = "(\<lambda> pR . io_targets M' (p_io pR) (initial M'))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
have p1: "(\<And>S1 S2. S1 \<in> ?R \<Longrightarrow> S2 \<in> ?R \<Longrightarrow> S1 = S2 \<or> ?f S1 \<inter> ?f S2 = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S1 S2. \<lbrakk>S1 \<in> R M (target (FSM.initial M) pP) q' pP p; S2 \<in> R M (target (FSM.initial M) pP) q' pP p\<rbrakk> \<Longrightarrow> S1 = S2 \<or> io_targets M' (p_io S1) (FSM.initial M') \<inter> io_targets M' (p_io S2) (FSM.initial M') = {}
[PROOF STEP]
using pairwise_dist_prop
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?pR1.0 \<in> R M (target (FSM.initial M) pP) q' pP p; ?pR2.0 \<in> R M (target (FSM.initial M) pP) q' pP p; ?pR1.0 \<noteq> ?pR2.0\<rbrakk> \<Longrightarrow> io_targets M' (p_io ?pR1.0) (FSM.initial M') \<inter> io_targets M' (p_io ?pR2.0) (FSM.initial M') = {}

goal (1 subgoal):
 1. \<And>S1 S2. \<lbrakk>S1 \<in> R M (target (FSM.initial M) pP) q' pP p; S2 \<in> R M (target (FSM.initial M) pP) q' pP p\<rbrakk> \<Longrightarrow> S1 = S2 \<or> io_targets M' (p_io S1) (FSM.initial M') \<inter> io_targets M' (p_io S2) (FSM.initial M') = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?S1.1 \<in> R M (target (FSM.initial M) pP) q' pP p; ?S2.1 \<in> R M (target (FSM.initial M) pP) q' pP p\<rbrakk> \<Longrightarrow> ?S1.1 = ?S2.1 \<or> io_targets M' (p_io ?S1.1) (FSM.initial M') \<inter> io_targets M' (p_io ?S2.1) (FSM.initial M') = {}

goal (1 subgoal):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
have p2: "(\<And>S. S \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io S) (FSM.initial M') \<noteq> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. S \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io S) (FSM.initial M') \<noteq> {}
[PROOF STEP]
using singleton_prop
[PROOF STATE]
proof (prove)
using this:
?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io ?pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length ?pR - length pP) p')}

goal (1 subgoal):
 1. \<And>S. S \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io S) (FSM.initial M') \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?S1 \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io ?S1) (FSM.initial M') \<noteq> {}

goal (1 subgoal):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
have c1: "card (R M (target (FSM.initial M) pP) q' pP p) = card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (R M (target (FSM.initial M) pP) q' pP p) = card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
using card_union_of_distinct[of ?R, OF p1 \<open>finite ?R\<close> p2]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>S1 S2. \<lbrakk>S1 \<in> R M (target (FSM.initial M) pP) q' pP p; S2 \<in> R M (target (FSM.initial M) pP) q' pP p\<rbrakk> \<Longrightarrow> S1 \<in> R M (target (FSM.initial M) pP) q' pP p; \<And>S1 S2. \<lbrakk>S1 \<in> R M (target (FSM.initial M) pP) q' pP p; S2 \<in> R M (target (FSM.initial M) pP) q' pP p\<rbrakk> \<Longrightarrow> S2 \<in> R M (target (FSM.initial M) pP) q' pP p; \<And>S. S \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> S \<in> R M (target (FSM.initial M) pP) q' pP p\<rbrakk> \<Longrightarrow> card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p) = card (R M (target (FSM.initial M) pP) q' pP p)

goal (1 subgoal):
 1. card (R M (target (FSM.initial M) pP) q' pP p) = card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
card (R M (target (FSM.initial M) pP) q' pP p) = card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p)

goal (1 subgoal):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
have p3: "(\<And>S. S \<in> (\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>t. S = {t})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. S \<in> (\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>t. S = {t}
[PROOF STEP]
using singleton_prop
[PROOF STATE]
proof (prove)
using this:
?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io ?pR) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length ?pR - length pP) p')}

goal (1 subgoal):
 1. \<And>S. S \<in> (\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>t. S = {t}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?S1 \<in> (\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> \<exists>t. ?S1 = {t}

goal (1 subgoal):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
have c2:"card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p) = card (\<Union>S\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io S) (FSM.initial M'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p) = card (\<Union>S\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io S) (FSM.initial M'))
[PROOF STEP]
using card_union_of_singletons[of "((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p)", OF p3]
[PROOF STATE]
proof (prove)
using this:
(\<And>S. S \<in> (\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> S \<in> (\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>S\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io S) (FSM.initial M')) = card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p)

goal (1 subgoal):
 1. card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p) = card (\<Union>S\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io S) (FSM.initial M'))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` R M (target (FSM.initial M) pP) q' pP p) = card (\<Union>S\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io S) (FSM.initial M'))

goal (1 subgoal):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
show "card ?Tgts = card ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
unfolding c1 c2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (\<Union>S\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io S) (FSM.initial M'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (\<Union>pR\<in>R M (target (FSM.initial M) pP) q' pP p. io_targets M' (p_io pR) (FSM.initial M')) = card (R M (target (FSM.initial M) pP) q' pP p)

goal:
No subgoals!
[PROOF STEP]
qed