[STATEMENT]
lemma observable_minimal_path_to_failure :
  assumes "\<not> (L M' \<subseteq> L M)"
  and     "observable M"
  and     "observable M'"
  and     "inputs M' = inputs M"
  and     "completely_specified M"
  and     "completely_specified M'"
obtains p p' t t' where "path M (initial M) (p@[t])"
                  and   "path M' (initial M') (p'@[t'])"
                  and   "p_io p' = p_io p"
                  and   "t_input t' = t_input t"
                  and   "\<not>(\<exists> t'' . t'' \<in> transitions M \<and> t_source t'' = target (initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p t p' t'. \<lbrakk>path M (FSM.initial M) (p @ [t]); path M' (FSM.initial M') (p' @ [t']); p_io p' = p_io p; t_input t' = t_input t; \<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p t p' t'. \<lbrakk>path M (FSM.initial M) (p @ [t]); path M' (FSM.initial M') (p' @ [t']); p_io p' = p_io p; t_input t' = t_input t; \<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain io x y y' where "io@[(x,y)] \<in> L M" and "io@[(x,y')] \<notin>  L M" and "io@[(x,y')] \<in> L M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using minimal_io_seq_to_failure[OF assms(1,4,5)]
[PROOF STATE]
proof (prove)
using this:
(\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io @ [(x, y)] \<in> L M
io @ [(x, y')] \<notin> L M
io @ [(x, y')] \<in> L M'

goal (1 subgoal):
 1. (\<And>p t p' t'. \<lbrakk>path M (FSM.initial M) (p @ [t]); path M' (FSM.initial M') (p' @ [t']); p_io p' = p_io p; t_input t' = t_input t; \<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain p t where "path M (initial M) (p@[t])" and "p_io p = io" and "t_input t = x" and "t_output t = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p t. \<lbrakk>path M (FSM.initial M) (p @ [t]); p_io p = io; t_input t = x; t_output t = y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using language_append_path_ob[OF \<open>io@[(x,y)] \<in> L M\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>p t. \<lbrakk>path M (FSM.initial M) (p @ [t]); p_io p = io; t_input t = x; t_output t = y\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p t. \<lbrakk>path M (FSM.initial M) (p @ [t]); p_io p = io; t_input t = x; t_output t = y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) (p @ [t])
p_io p = io
t_input t = x
t_output t = y

goal (1 subgoal):
 1. (\<And>p t p' t'. \<lbrakk>path M (FSM.initial M) (p @ [t]); path M' (FSM.initial M') (p' @ [t']); p_io p' = p_io p; t_input t' = t_input t; \<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) (p @ [t])
p_io p = io
t_input t = x
t_output t = y

goal (1 subgoal):
 1. (\<And>p t p' t'. \<lbrakk>path M (FSM.initial M) (p @ [t]); path M' (FSM.initial M') (p' @ [t']); p_io p' = p_io p; t_input t' = t_input t; \<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain p' t' where "path M' (initial M') (p'@[t'])" and "p_io p' = io" and "t_input t' = x" and "t_output t' = y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p' t'. \<lbrakk>path M' (FSM.initial M') (p' @ [t']); p_io p' = io; t_input t' = x; t_output t' = y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using language_append_path_ob[OF \<open>io@[(x,y')] \<in> L M'\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>p t. \<lbrakk>path M' (FSM.initial M') (p @ [t]); p_io p = io; t_input t = x; t_output t = y'\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. (\<And>p t p' t'. \<lbrakk>path M (FSM.initial M) (p @ [t]); path M' (FSM.initial M') (p' @ [t']); p_io p' = p_io p; t_input t' = t_input t; \<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path M' (FSM.initial M') (p' @ [t'])
p_io p' = io
t_input t' = x
t_output t' = y'

goal (1 subgoal):
 1. (\<And>p t p' t'. \<lbrakk>path M (FSM.initial M) (p @ [t]); path M' (FSM.initial M') (p' @ [t']); p_io p' = p_io p; t_input t' = t_input t; \<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<not>(\<exists> t'' . t'' \<in> transitions M \<and> t_source t'' = target (initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t' \<Longrightarrow> False
[PROOF STEP]
assume "\<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'"
[PROOF STATE]
proof (state)
this:
\<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'

goal (1 subgoal):
 1. \<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'
[PROOF STEP]
obtain t'' where "t'' \<in> FSM.transitions M" and "t_source t'' = target (FSM.initial M) p" and "t_input t'' = x" and "t_output t'' = y'"
[PROOF STATE]
proof (prove)
using this:
\<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'

goal (1 subgoal):
 1. (\<And>t''. \<lbrakk>t'' \<in> FSM.transitions M; t_source t'' = target (FSM.initial M) p; t_input t'' = x; t_output t'' = y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<open>t_input t = x\<close> \<open>t_output t' = y'\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = x \<and> t_output t'' = y'

goal (1 subgoal):
 1. (\<And>t''. \<lbrakk>t'' \<in> FSM.transitions M; t_source t'' = target (FSM.initial M) p; t_input t'' = x; t_output t'' = y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t'' \<in> FSM.transitions M
t_source t'' = target (FSM.initial M) p
t_input t'' = x
t_output t'' = y'

goal (1 subgoal):
 1. \<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t'' \<in> FSM.transitions M
t_source t'' = target (FSM.initial M) p
t_input t'' = x
t_output t'' = y'
[PROOF STEP]
have "path M (initial M) (p@[t''])"
[PROOF STATE]
proof (prove)
using this:
t'' \<in> FSM.transitions M
t_source t'' = target (FSM.initial M) p
t_input t'' = x
t_output t'' = y'

goal (1 subgoal):
 1. path M (FSM.initial M) (p @ [t''])
[PROOF STEP]
using \<open>path M (initial M) (p@[t])\<close>
[PROOF STATE]
proof (prove)
using this:
t'' \<in> FSM.transitions M
t_source t'' = target (FSM.initial M) p
t_input t'' = x
t_output t'' = y'
path M (FSM.initial M) (p @ [t])

goal (1 subgoal):
 1. path M (FSM.initial M) (p @ [t''])
[PROOF STEP]
by (meson path_append_elim path_append_transition)
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) (p @ [t''])

goal (1 subgoal):
 1. \<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) (p @ [t''])

goal (1 subgoal):
 1. \<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t' \<Longrightarrow> False
[PROOF STEP]
have "p_io (p@[t'']) = io@[(x,y')]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (p @ [t'']) = io @ [(x, y')]
[PROOF STEP]
using \<open>p_io p = io\<close> \<open>t_input t'' = x\<close> \<open>t_output t'' = y'\<close>
[PROOF STATE]
proof (prove)
using this:
p_io p = io
t_input t'' = x
t_output t'' = y'

goal (1 subgoal):
 1. p_io (p @ [t'']) = io @ [(x, y')]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_io (p @ [t'']) = io @ [(x, y')]

goal (1 subgoal):
 1. \<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t' \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path M (FSM.initial M) (p @ [t''])
p_io (p @ [t'']) = io @ [(x, y')]
[PROOF STEP]
have "io@[(x,y')] \<in> L M"
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) (p @ [t''])
p_io (p @ [t'']) = io @ [(x, y')]

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L M
[PROOF STEP]
using language_state_containment
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) (p @ [t''])
p_io (p @ [t'']) = io @ [(x, y')]
\<lbrakk>path ?M ?q ?p; p_io ?p = ?io\<rbrakk> \<Longrightarrow> ?io \<in> LS ?M ?q

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L M
[PROOF STEP]
by (metis (mono_tags, lifting))
[PROOF STATE]
proof (state)
this:
io @ [(x, y')] \<in> L M

goal (1 subgoal):
 1. \<exists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io @ [(x, y')] \<in> L M
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
io @ [(x, y')] \<in> L M

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>io@[(x,y')] \<notin> L M\<close>
[PROOF STATE]
proof (prove)
using this:
io @ [(x, y')] \<in> L M
io @ [(x, y')] \<notin> L M

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'

goal (1 subgoal):
 1. (\<And>p t p' t'. \<lbrakk>path M (FSM.initial M) (p @ [t]); path M' (FSM.initial M') (p' @ [t']); p_io p' = p_io p; t_input t' = t_input t; \<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path M (FSM.initial M) (p @ [t])
p_io p = io
t_input t = x
t_output t = y
path M' (FSM.initial M') (p' @ [t'])
p_io p' = io
t_input t' = x
t_output t' = y'
\<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) (p @ [t])
p_io p = io
t_input t = x
t_output t = y
path M' (FSM.initial M') (p' @ [t'])
p_io p' = io
t_input t' = x
t_output t' = y'
\<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of p t p' t']
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) (p @ [t])
p_io p = io
t_input t = x
t_output t = y
path M' (FSM.initial M') (p' @ [t'])
p_io p' = io
t_input t' = x
t_output t' = y'
\<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'
\<lbrakk>path M (FSM.initial M) (p @ [t]); path M' (FSM.initial M') (p' @ [t']); p_io p' = p_io p; t_input t' = t_input t; \<nexists>t''. t'' \<in> FSM.transitions M \<and> t_source t'' = target (FSM.initial M) p \<and> t_input t'' = t_input t \<and> t_output t'' = t_output t'\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed