[STATEMENT]
lemma RP_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"
  and     "\<And> q P io x y y' . (q,P) \<in> PS \<Longrightarrow> io@[(x,y)] \<in> L P \<Longrightarrow> io@[(x,y')] \<in> L M' \<Longrightarrow> io@[(x,y')] \<in> L P"
  and     "completely_specified M'"
  and     "inputs M' = inputs M"
shows "card (\<Union> (image (\<lambda> pR . io_targets M' (p_io pR) (initial M')) (RP M (target (initial M) pP) q' pP p PS M')))
        = card (RP M (target (initial M) pP) q' pP p PS M')"
  (is "card ?Tgts = card ?RP")
and "\<And> pR . pR \<in> (RP M (target (initial M) pP) q' pP p PS M') \<Longrightarrow> \<exists> q . io_targets M' (p_io pR) (initial M') = {q}"
and "\<And> pR1 pR2 . pR1 \<in> (RP M (target (initial M) pP) q' pP p PS M') \<Longrightarrow> pR2 \<in> (RP M (target (initial M) pP) q' pP p PS M') \<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>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') &&& (\<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}) &&& (\<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
 2. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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 ?P1 = "card (\<Union> (image (\<lambda> pR . io_targets M' (p_io pR) (initial M')) (RP M (target (initial M) pP) q' pP p PS M'))) = card (RP M (target (initial M) pP) q' pP p PS M')"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
 2. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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 ?P2 = "\<forall> pR . pR \<in> (RP M (target (initial M) pP) q' pP p PS M') \<longrightarrow> (\<exists> q . io_targets M' (p_io pR) (initial M') = {q})"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
 2. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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 ?P3 = "\<forall> pR1 pR2 . pR1 \<in> (RP M (target (initial M) pP) q' pP p PS M') \<longrightarrow> pR2 \<in> (RP M (target (initial M) pP) q' pP p PS M') \<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 (state)
goal (3 subgoals):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
 2. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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 ?combined_goals = "?P1 \<and> ?P2 \<and> ?P3"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
 2. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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 (initial M) pP)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
 2. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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 ?R = "R M ?q q' pP p"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
 2. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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]
consider (a) "(?RP = ?R)" |
           (b) "(\<exists> P' pP' . (q',P') \<in> PS \<and>
                            path P' (initial P') pP' \<and>
                            target (initial P') pP' = q' \<and>
                            path M (initial M) pP' \<and>
                            target (initial M) pP' = q' \<and>
                            p_io pP' \<in> L M' \<and>
                            ?RP = insert pP' ?R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>RP M (target (FSM.initial M) pP) q' pP p PS M' = R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> thesis; \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using RP_from_R[OF assms(4,7,8,9), of PS _ _ ?q q' pP p]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> (?q1 q P io x y y', P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, ?y1 q P io x y y')] \<in> L P; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> RP M (target (FSM.initial M) pP) q' pP p PS M' = R M (target (FSM.initial M) pP) q' pP p \<or> (\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p))

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

goal (3 subgoals):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
 2. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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>RP M (target (FSM.initial M) pP) q' pP p PS M' = R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> ?thesis; \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
have ?combined_goals
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>RP M (target (FSM.initial M) pP) q' pP p PS M' = R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> ?thesis; \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. RP M (target (FSM.initial M) pP) q' pP p PS M' = R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
 2. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
case a
[PROOF STATE]
proof (state)
this:
RP M (target (FSM.initial M) pP) q' pP p PS M' = R M (target (FSM.initial M) pP) q' pP p

goal (2 subgoals):
 1. RP M (target (FSM.initial M) pP) q' pP p PS M' = R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
 2. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
unfolding a
[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> (\<forall>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> (\<forall>pR1 pR2. pR1 \<in> R M (target (FSM.initial M) pP) q' pP p \<longrightarrow> pR2 \<in> R M (target (FSM.initial M) pP) q' pP p \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
using R_count[OF assms(1-6)]
[PROOF STATE]
proof (prove)
using this:
(\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS) \<Longrightarrow> 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)
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; ?pR \<in> R M (target (FSM.initial M) pP) ?q' pP p\<rbrakk> \<Longrightarrow> \<exists>q. io_targets M' (p_io ?pR) (FSM.initial M') = {q}
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; ?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) \<and> (\<forall>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> (\<forall>pR1 pR2. pR1 \<in> R M (target (FSM.initial M) pP) q' pP p \<longrightarrow> pR2 \<in> R M (target (FSM.initial M) pP) q' pP p \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
case b
[PROOF STATE]
proof (state)
this:
\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p)

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
(* properties from R_count *)
[PROOF STATE]
proof (state)
this:
\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p)

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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:
io \<noteq> []

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
have "finite ?RP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (RP M (target (FSM.initial M) pP) q' pP p PS M')
[PROOF STEP]
using finite_RP[OF \<open>path M (target (initial M) pP) p\<close> assms(4,7,8,9)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q P. (q, P) \<in> ?PS \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> ?PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> (?q1 q P io x y y', P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> ?PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, ?y1 q P io x y y')] \<in> L P; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> ?PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> finite (RP M (target (FSM.initial M) pP) ?q' ?pP p ?PS M')

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

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (RP M (target (FSM.initial M) pP) q' pP p PS M')

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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> ?RP \<Longrightarrow> finite (io_targets M' (p_io pR) (initial M'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<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> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> finite (io_targets M' (p_io pR) (FSM.initial M'))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> finite (io_targets M' (p_io ?pR) (FSM.initial M'))

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (RP M (target (FSM.initial M) pP) q' pP p PS M')
?pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> finite (io_targets M' (p_io ?pR) (FSM.initial M'))
[PROOF STEP]
have "finite ?Tgts"
[PROOF STATE]
proof (prove)
using this:
finite (RP M (target (FSM.initial M) pP) q' pP p PS M')
?pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> finite (io_targets M' (p_io ?pR) (FSM.initial M'))

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

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M'))

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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]
by (metis (no_types, lifting) assms(6) 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]
using \<open>length p \<le> length (butlast io)\<close> \<open>pR = take (length pR) p \<and> length pR \<le> length p\<close>
              butlast_take_le dual_order.trans
[PROOF STATE]
proof (prove)
using this:
length p \<le> length (butlast io)
pR = take (length pR) p \<and> length pR \<le> length p
?i \<le> length (butlast ?xs) \<Longrightarrow> take ?i (butlast ?xs) = take ?i ?xs
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

goal (1 subgoal):
 1. take (length pR) (butlast io) = take (length pR) io
[PROOF STEP]
by blast
[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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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'_R: "\<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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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_R: "\<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'_R[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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
(* RP props *)
[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 (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
from b
[PROOF STATE]
proof (chain)
picking this:
\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p)
[PROOF STEP]
obtain P' pP'' where "(q',P') \<in> PS"
                          and   "path P' (initial P') pP''"
                          and   "target (initial P') pP'' = q'"
                          and   "path M (initial M) pP''"
                          and   "target (initial M) pP'' = q'"
                          and   "p_io pP'' \<in> L M'"
                          and   "?RP = insert pP'' ?R"
[PROOF STATE]
proof (prove)
using this:
\<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p)

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

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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 assms(4)[OF \<open>(q',P') \<in> PS\<close>]
[PROOF STATE]
proof (prove)
using this:
is_preamble P' M q'

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

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

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
(* revisiting singleton_prop *)
[PROOF STATE]
proof (state)
this:
FSM.initial P' = FSM.initial M

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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> ?RP \<Longrightarrow> pR \<in> ?R \<or> pR = pP''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> pR \<in> R M (target (FSM.initial M) pP) q' pP p \<or> pR = pP''
[PROOF STEP]
using \<open>?RP = insert pP'' ?R\<close>
[PROOF STATE]
proof (prove)
using this:
RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP'' (R M (target (FSM.initial M) pP) q' pP p)

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

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> ?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<or> ?pR = pP''
[PROOF STEP]
have rp_cases[consumes 1, case_names in_R inserted]: "\<And> pR P . (pR \<in> ?RP) \<Longrightarrow> (pR \<in> ?R \<Longrightarrow> P) \<Longrightarrow> (pR = pP'' \<Longrightarrow> P) \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
using this:
?pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> ?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<or> ?pR = pP''

goal (1 subgoal):
 1. \<And>pR P. \<lbrakk>pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> P; pR = pP'' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>?pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> ?P; ?pR = pP'' \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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_RP: "\<And> pR . pR \<in> ?RP \<Longrightarrow> \<exists> q . io_targets M' (p_io pR) (initial M') = {q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
fix pR
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
assume "pR \<in> ?RP"
[PROOF STATE]
proof (state)
this:
pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'

goal (1 subgoal):
 1. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'
[PROOF STEP]
show "\<exists> q . io_targets M' (p_io pR) (initial M') = {q}"
[PROOF STATE]
proof (prove)
using this:
pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'

goal (1 subgoal):
 1. \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
proof (cases rule: rp_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 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}
 2. pR = pP'' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
case in_R
[PROOF STATE]
proof (state)
this:
pR \<in> R M (target (FSM.initial M) pP) q' pP p

goal (2 subgoals):
 1. 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}
 2. pR = pP'' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR \<in> R M (target (FSM.initial M) pP) q' pP p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pR \<in> R M (target (FSM.initial M) pP) q' pP p

goal (1 subgoal):
 1. \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
using singleton_prop_R
[PROOF STATE]
proof (prove)
using this:
pR \<in> R M (target (FSM.initial M) pP) q' pP p
?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. \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}

goal (1 subgoal):
 1. pR = pP'' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pR = pP'' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
case inserted
[PROOF STATE]
proof (state)
this:
pR = pP''

goal (1 subgoal):
 1. pR = pP'' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
using observable_io_targets[OF \<open>observable M'\<close> \<open>p_io pP'' \<in> L M'\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>q'. io_targets M' (p_io pP'') (FSM.initial M') = {q'} \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
[PROOF STEP]
unfolding inserted
[PROOF STATE]
proof (prove)
using this:
(\<And>q'. io_targets M' (p_io pP'') (FSM.initial M') = {q'} \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>q. io_targets M' (p_io pP'') (FSM.initial M') = {q}
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}

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

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io ?pR) (FSM.initial M') = {q}
[PROOF STEP]
have ?P2
[PROOF STATE]
proof (prove)
using this:
?pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io ?pR) (FSM.initial M') = {q}

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

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
(* distinctness in RP *)
[PROOF STATE]
proof (state)
this:
\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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_RP: "\<And> pR1 pR2 . pR1 \<in> ?RP \<Longrightarrow> pR2 \<in> ?RP \<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. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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 (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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_R: "\<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)
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_count(3)[OF assms(1-6)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; ?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>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 force
[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. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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_PS: "\<And> pR1 . pR1 \<in> ?RP \<Longrightarrow> pR1 \<noteq> pP'' \<Longrightarrow> io_targets M' (p_io pR1) (initial M') \<inter> io_targets M' (p_io pP'') (initial M') = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pR1. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR1 \<noteq> pP''\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pP'') (FSM.initial M') = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR1. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR1 \<noteq> pP''\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pP'') (FSM.initial M') = {}
[PROOF STEP]
fix pR1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR1. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR1 \<noteq> pP''\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pP'') (FSM.initial M') = {}
[PROOF STEP]
assume "pR1 \<in> ?RP" and "pR1 \<noteq> pP''"
[PROOF STATE]
proof (state)
this:
pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'
pR1 \<noteq> pP''

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

goal (1 subgoal):
 1. pR1 \<in> R M (target (FSM.initial M) pP) q' pP p
[PROOF STEP]
using \<open>\<And> pR . pR \<in> ?RP \<Longrightarrow> pR \<in> ?R \<or> pR = pP''\<close>
[PROOF STATE]
proof (prove)
using this:
pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'
pR1 \<noteq> pP''
?pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> ?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<or> ?pR = pP''

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>pR1. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR1 \<noteq> pP''\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pP'') (FSM.initial M') = {}
[PROOF STEP]
let ?i = "(length pR') - 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR1. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR1 \<noteq> pP''\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pP'') (FSM.initial M') = {}
[PROOF STEP]
have "?i < length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length pR' - 1 < length p
[PROOF STEP]
using \<open>length pR' \<le> length p\<close> \<open>pR' \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
length pR' \<le> length p
pR' \<noteq> []

goal (1 subgoal):
 1. length pR' - 1 < length p
[PROOF STEP]
using diff_less dual_order.strict_trans1 less_numeral_extra(1)
[PROOF STATE]
proof (prove)
using this:
length pR' \<le> length p
pR' \<noteq> []
\<lbrakk>0 < ?n; 0 < ?m\<rbrakk> \<Longrightarrow> ?m - ?n < ?m
\<lbrakk>?b \<le> ?a; ?c < ?b\<rbrakk> \<Longrightarrow> ?c < ?a
(0::?'a) < (1::?'a)

goal (1 subgoal):
 1. length pR' - 1 < length p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length pR' - 1 < length p

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

goal (1 subgoal):
 1. length pR' - 1 < length (butlast io)
[PROOF STEP]
using \<open>length p \<le> length (butlast io)\<close> less_le_trans
[PROOF STATE]
proof (prove)
using this:
length pR' - 1 < length p
length p \<le> length (butlast io)
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z

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

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

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

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

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

goal (1 subgoal):
 1. last (last (FSM.initial M' # map t_target pP') # map t_target (take (length pR') p')) = t_target (p' ! (length pR' - 1))
[PROOF STEP]
by (metis (no_types, lifting) \<open>length p < length p'\<close> \<open>pR' \<noteq> []\<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 pR') p') = t_target (p' ! (length pR' - 1))

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

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') = {t_target (p' ! (length pR' - 1))}
[PROOF STEP]
have "io_targets M' (p_io pR1) (initial M') = {target ?q (take (length pR') p')}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR') p')}
[PROOF STEP]
using singleton_prop'_R \<open>pR1 \<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')}
pR1 \<in> R M (target (FSM.initial M) pP) q' pP p

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

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') = {t_target (p' ! (length pR' - 1))}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
target (target (FSM.initial M') pP') (take (length pR') p') = t_target (p' ! (length pR' - 1))
io_targets M' (p_io pR1) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR') p')}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
target (target (FSM.initial M') pP') (take (length pR') p') = t_target (p' ! (length pR' - 1))
io_targets M' (p_io pR1) (FSM.initial M') = {target (target (FSM.initial M') pP') (take (length pR') p')}

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

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

goal (1 subgoal):
 1. \<And>pR1. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR1 \<noteq> pP''\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pP'') (FSM.initial M') = {}
[PROOF STEP]
have "t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (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)
goal (1 subgoal):
 1. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (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 (1 subgoal):
 1. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')
[PROOF STEP]
(* get index properties *)
[PROOF STATE]
proof (state)
this:
path M (target (FSM.initial M) pP) (p @ pX)
p_io (p @ pX) = butlast io

goal (1 subgoal):
 1. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')
[PROOF STEP]
have "target (FSM.initial M') pP' \<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]
using \<open>p_io pP' = p_io pP\<close> \<open>path M' (FSM.initial M') pP'\<close> observable_path_io_target
[PROOF STATE]
proof (prove)
using this:
p_io pP' = p_io pP
path M' (FSM.initial M') pP'
\<lbrakk>observable ?M; path ?M ?q ?p\<rbrakk> \<Longrightarrow> io_targets ?M (p_io ?p) ?q = {target ?q ?p}

goal (1 subgoal):
 1. target (FSM.initial M') pP' \<in> io_targets M' (p_io pP) (FSM.initial M')
[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. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')
[PROOF STEP]
have "(t_target (p ! (length pR' - 1)), P') \<in> PS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t_target (p ! (length pR' - 1)), P') \<in> PS
[PROOF STEP]
using \<open>(q',P') \<in> PS\<close>
[PROOF STATE]
proof (prove)
using this:
(q', P') \<in> PS

goal (1 subgoal):
 1. (t_target (p ! (length pR' - 1)), P') \<in> PS
[PROOF STEP]
unfolding \<open>t_target (p ! (length pR' - 1)) = q'\<close>
[PROOF STATE]
proof (prove)
using this:
(q', P') \<in> PS

goal (1 subgoal):
 1. (q', P') \<in> PS
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
(t_target (p ! (length pR' - 1)), P') \<in> PS

goal (1 subgoal):
 1. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(t_target (p ! (length pR' - 1)), P') \<in> PS
[PROOF STEP]
have "(t_target ((p @ pX) ! ?i), P') \<in> PS"
[PROOF STATE]
proof (prove)
using this:
(t_target (p ! (length pR' - 1)), P') \<in> PS

goal (1 subgoal):
 1. (t_target ((p @ pX) ! (length pR' - 1)), P') \<in> PS
[PROOF STEP]
by (metis \<open>length pR' - 1 < length p\<close> nth_append)
[PROOF STATE]
proof (state)
this:
(t_target ((p @ pX) ! (length pR' - 1)), P') \<in> PS

goal (1 subgoal):
 1. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')
[PROOF STEP]
have "target (FSM.initial P') pP'' = t_target (p ! (length pR' - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial P') pP'' = t_target (p ! (length pR' - 1))
[PROOF STEP]
unfolding \<open>target (initial M) pP'' = q'\<close> \<open>t_target (p ! (length pR' - 1)) = q'\<close> \<open>initial P' = initial M\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q' = q'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
target (FSM.initial P') pP'' = t_target (p ! (length pR' - 1))

goal (1 subgoal):
 1. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target (FSM.initial P') pP'' = t_target (p ! (length pR' - 1))
[PROOF STEP]
have "target (FSM.initial P') pP'' = t_target ((p @ pX) ! ?i)"
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial P') pP'' = t_target (p ! (length pR' - 1))

goal (1 subgoal):
 1. target (FSM.initial P') pP'' = t_target ((p @ pX) ! (length pR' - 1))
[PROOF STEP]
by (metis \<open>length pR' - 1 < length p\<close> nth_append)
[PROOF STATE]
proof (state)
this:
target (FSM.initial P') pP'' = t_target ((p @ pX) ! (length pR' - 1))

goal (1 subgoal):
 1. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')
[PROOF STEP]
using minimal_sequence_to_failure_extending_preamble_no_repetitions_with_other_preambles
                    [OF assms(1,2) \<open>path M (target (initial M) pP) (p@pX)\<close> \<open>p_io (p@pX) = butlast io\<close>
                        \<open>target (FSM.initial M') pP' \<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> assms(4)
                        \<open>?i < length (butlast io)\<close> \<open>(t_target ((p @ pX) ! ?i), P') \<in> PS\<close>
                        \<open>path P' (initial P') pP''\<close> \<open>target (FSM.initial P') pP'' = t_target ((p @ pX) ! ?i)\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS) \<Longrightarrow> t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')

goal (1 subgoal):
 1. t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')

goal (1 subgoal):
 1. \<And>pR1. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR1 \<noteq> pP''\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pP'') (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')
[PROOF STEP]
show "io_targets M' (p_io pR1) (initial M') \<inter> io_targets M' (p_io pP'') (initial M') = {}"
[PROOF STATE]
proof (prove)
using this:
t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pP'') (FSM.initial M') = {}
[PROOF STEP]
unfolding \<open>io_targets M' (p_io pR1) (initial M') = {t_target (p' ! ?i)}\<close>
[PROOF STATE]
proof (prove)
using this:
t_target (p' ! (length pR' - 1)) \<notin> io_targets M' (p_io pP'') (FSM.initial M')

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

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

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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]
fix pR1 pR2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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]
assume "pR1 \<in> ?RP" and "pR2 \<in> ?RP" and "pR1 \<noteq> pR2"
[PROOF STATE]
proof (state)
this:
pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'
pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'
pR1 \<noteq> pR2

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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:
pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'
pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'
pR1 \<noteq> pR2
[PROOF STEP]
consider (a) "pR1 \<in> ?R \<and> pR2 \<in> ?R" |
                    (b) "pR1 = pP''" |
                    (c) "pR2 = pP''"
[PROOF STATE]
proof (prove)
using this:
pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'
pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'
pR1 \<noteq> pR2

goal (1 subgoal):
 1. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p \<and> pR2 \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> thesis; pR1 = pP'' \<Longrightarrow> thesis; pR2 = pP'' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<And> pR . pR \<in> ?RP \<Longrightarrow> pR \<in> ?R \<or> pR = pP''\<close> \<open>pR1 \<noteq> pR2\<close>
[PROOF STATE]
proof (prove)
using this:
pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'
pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'
pR1 \<noteq> pR2
?pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> ?pR \<in> R M (target (FSM.initial M) pP) q' pP p \<or> ?pR = pP''
pR1 \<noteq> pR2

goal (1 subgoal):
 1. \<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p \<and> pR2 \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> thesis; pR1 = pP'' \<Longrightarrow> thesis; pR2 = pP'' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p \<and> pR2 \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> ?thesis; pR1 = pP'' \<Longrightarrow> ?thesis; pR2 = pP'' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p \<and> pR2 \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> ?thesis; pR1 = pP'' \<Longrightarrow> ?thesis; pR2 = pP'' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "io_targets M' (p_io pR1) (initial M') \<inter> io_targets M' (p_io pR2) (initial M') = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>pR1 \<in> R M (target (FSM.initial M) pP) q' pP p \<and> pR2 \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> ?thesis; pR1 = pP'' \<Longrightarrow> ?thesis; pR2 = pP'' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (3 subgoals):
 1. pR1 \<in> R M (target (FSM.initial M) pP) q' pP p \<and> pR2 \<in> R M (target (FSM.initial M) pP) q' pP p \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
 2. pR1 = pP'' \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
 3. pR2 = pP'' \<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:
pR1 \<in> R M (target (FSM.initial M) pP) q' pP p \<and> pR2 \<in> R M (target (FSM.initial M) pP) q' pP p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pR1 \<in> R M (target (FSM.initial M) pP) q' pP p \<and> pR2 \<in> R M (target (FSM.initial M) pP) q' pP p

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
using pairwise_dist_prop_R[of pR1 pR2, OF _ _ \<open>pR1 \<noteq> pR2\<close>]
[PROOF STATE]
proof (prove)
using this:
pR1 \<in> R M (target (FSM.initial M) pP) q' pP p \<and> pR2 \<in> R M (target (FSM.initial M) pP) q' pP p
\<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\<rbrakk> \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}

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

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

goal (2 subgoals):
 1. pR1 = pP'' \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
 2. pR2 = pP'' \<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:
pR1 = pP''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pR1 = pP''

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
using pairwise_dist_prop_PS[OF \<open>pR2 \<in> ?RP\<close>] \<open>pR1 \<noteq> pR2\<close>
[PROOF STATE]
proof (prove)
using this:
pR1 = pP''
pR2 \<noteq> pP'' \<Longrightarrow> io_targets M' (p_io pR2) (FSM.initial M') \<inter> io_targets M' (p_io pP'') (FSM.initial M') = {}
pR1 \<noteq> pR2

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

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

goal (1 subgoal):
 1. pR2 = pP'' \<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:
pR2 = pP''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pR2 = pP''

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
using pairwise_dist_prop_PS[OF \<open>pR1 \<in> ?RP\<close>] \<open>pR1 \<noteq> pR2\<close>
[PROOF STATE]
proof (prove)
using this:
pR2 = pP''
pR1 \<noteq> pP'' \<Longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pP'') (FSM.initial M') = {}
pR1 \<noteq> pR2

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?pR1.0 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?pR2.0 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?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. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<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>?pR1.0 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?pR2.0 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?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') = {}
[PROOF STEP]
have ?P3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?pR1.0 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?pR2.0 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?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. \<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
let ?f = "(\<lambda> pR . io_targets M' (p_io pR) (initial M'))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
have p1: "(\<And>S1 S2. S1 \<in> ?RP \<Longrightarrow> S2 \<in> ?RP \<Longrightarrow> S1 = S2 \<or> ?f S1 \<inter> ?f S2 = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S1 S2. \<lbrakk>S1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; S2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'\<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_RP
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?pR1.0 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?pR2.0 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?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> RP M (target (FSM.initial M) pP) q' pP p PS M'; S2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'\<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> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?S2.1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'\<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. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
have p2: "(\<And>S. S \<in> ?RP \<Longrightarrow> io_targets M' (p_io S) (FSM.initial M') \<noteq> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. S \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> io_targets M' (p_io S) (FSM.initial M') \<noteq> {}
[PROOF STEP]
using singleton_prop_RP
[PROOF STATE]
proof (prove)
using this:
?pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io ?pR) (FSM.initial M') = {q}

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

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
have c1: "card ?RP = card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` ?RP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (RP M (target (FSM.initial M) pP) q' pP p PS M') = card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` RP M (target (FSM.initial M) pP) q' pP p PS M')
[PROOF STEP]
using card_union_of_distinct[of ?RP, OF p1 \<open>finite ?RP\<close> p2]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>S1 S2. \<lbrakk>S1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; S2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'\<rbrakk> \<Longrightarrow> S1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; \<And>S1 S2. \<lbrakk>S1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; S2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'\<rbrakk> \<Longrightarrow> S2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; \<And>S. S \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> S \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'\<rbrakk> \<Longrightarrow> card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` RP M (target (FSM.initial M) pP) q' pP p PS M') = card (RP M (target (FSM.initial M) pP) q' pP p PS M')

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

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
have p3: "(\<And>S. S \<in> (\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` ?RP \<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')) ` RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>t. S = {t}
[PROOF STEP]
using singleton_prop_RP
[PROOF STATE]
proof (prove)
using this:
?pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io ?pR) (FSM.initial M') = {q}

goal (1 subgoal):
 1. \<And>S. S \<in> (\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` RP M (target (FSM.initial M) pP) q' pP p PS M' \<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')) ` RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>t. ?S1 = {t}

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
have c2:"card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` ?RP) = card (\<Union>S\<in>?RP. 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')) ` RP M (target (FSM.initial M) pP) q' pP p PS M') = card (\<Union>S\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. 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')) ` ?RP)", OF p3]
[PROOF STATE]
proof (prove)
using this:
(\<And>S. S \<in> (\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> S \<in> (\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` RP M (target (FSM.initial M) pP) q' pP p PS M') \<Longrightarrow> card (\<Union>S\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io S) (FSM.initial M')) = card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` RP M (target (FSM.initial M) pP) q' pP p PS M')

goal (1 subgoal):
 1. card ((\<lambda>S. io_targets M' (p_io S) (FSM.initial M')) ` RP M (target (FSM.initial M) pP) q' pP p PS M') = card (\<Union>S\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. 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')) ` RP M (target (FSM.initial M) pP) q' pP p PS M') = card (\<Union>S\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io S) (FSM.initial M'))

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
have ?P1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
[PROOF STEP]
unfolding c1 c2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (\<Union>S\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io S) (FSM.initial M'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')

goal (1 subgoal):
 1. \<exists>P' pP'. (q', P') \<in> PS \<and> path P' (FSM.initial P') pP' \<and> target (FSM.initial P') pP' = q' \<and> path M (FSM.initial M) pP' \<and> target (FSM.initial M) pP' = q' \<and> p_io pP' \<in> L M' \<and> RP M (target (FSM.initial M) pP) q' pP p PS M' = insert pP' (R M (target (FSM.initial M) pP) q' pP p) \<Longrightarrow> card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
show ?combined_goals
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
using \<open>?P1\<close> \<open>?P2\<close> \<open>?P3\<close>
[PROOF STATE]
proof (prove)
using this:
card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})
\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}

goal (1 subgoal):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})

goal (3 subgoals):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
 2. \<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}
 3. \<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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:
card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})
[PROOF STEP]
show "card (\<Union> (image (\<lambda> pR . io_targets M' (p_io pR) (initial M')) (RP M (target (initial M) pP) q' pP p PS M'))) = card (RP M (target (initial M) pP) q' pP p PS M')"
       and  "\<And> pR . pR \<in> (RP M (target (initial M) pP) q' pP p PS M') \<Longrightarrow> \<exists> q . io_targets M' (p_io pR) (initial M') = {q}"
       and  "\<And> pR1 pR2 . pR1 \<in> (RP M (target (initial M) pP) q' pP p PS M') \<Longrightarrow> pR2 \<in> (RP M (target (initial M) pP) q' pP p PS M') \<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:
card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') \<and> (\<forall>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> (\<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q})) \<and> (\<forall>pR1 pR2. pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<longrightarrow> pR1 \<noteq> pR2 \<longrightarrow> io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {})

goal (1 subgoal):
 1. card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M') &&& (\<And>pR. pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io pR) (FSM.initial M') = {q}) &&& (\<And>pR1 pR2. \<lbrakk>pR1 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; pR2 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; 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 blast+
[PROOF STATE]
proof (state)
this:
card (\<Union>pR\<in>RP M (target (FSM.initial M) pP) q' pP p PS M'. io_targets M' (p_io pR) (FSM.initial M')) = card (RP M (target (FSM.initial M) pP) q' pP p PS M')
?pR \<in> RP M (target (FSM.initial M) pP) q' pP p PS M' \<Longrightarrow> \<exists>q. io_targets M' (p_io ?pR) (FSM.initial M') = {q}
\<lbrakk>?pR1.0 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?pR2.0 \<in> RP M (target (FSM.initial M) pP) q' pP p PS M'; ?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:
No subgoals!
[PROOF STEP]
qed