[STATEMENT]
lemma h_obs_distinguishes :
  assumes "observable M"
  and     "h_obs M q1 x y = Some q1'"
  and     "h_obs M q2 x y = None"
shows "distinguishes M q1 q2 [(x,y)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
using assms(2,3) LS_single_transition[of x y M]
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = None
([(x, y)] \<in> LS M ?q) = (\<exists>t\<in>FSM.transitions M. t_source t = ?q \<and> t_input t = x \<and> t_output t = y)

goal (1 subgoal):
 1. distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
unfolding distinguishes_def h_obs_Some[OF assms(1)] h_obs_None[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
{q'. (q1, x, y, q') \<in> FSM.transitions M} = {q1'}
\<nexists>q'. (q2, x, y, q') \<in> FSM.transitions M
([(x, y)] \<in> LS M ?q) = (\<exists>t\<in>FSM.transitions M. t_source t = ?q \<and> t_input t = x \<and> t_output t = y)

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<union> LS M q2 \<and> [(x, y)] \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
by (metis Int_iff UnI1 \<open>\<And>y x q. (h_obs M q x y = None) = (\<nexists>q'. (q, x, y, q') \<in> FSM.transitions M)\<close> assms(1) assms(2) fst_conv h_obs_language_iff option.distinct(1) snd_conv)