[STATEMENT]
lemma assemble_distinguishing_sequence_from_ofsm_table_distinguishes :
  assumes "observable M"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
  and     "ofsm_table M (\<lambda>q . states M) k q1 \<noteq> ofsm_table M (\<lambda>q . states M) k q2"
shows "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2"
and   "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2"
and   "butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 &&& assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 &&& butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2
 2. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2
 3. butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2
        \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2
        \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
using assms(2,3,4)
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table M (\<lambda>q. FSM.states M) k q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
proof (induction k arbitrary: q1 q2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) 0 q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0 \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0 \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0) \<in> LS M q1 \<inter> LS M q2
 2. \<And>k q1 q2. \<lbrakk>\<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) k q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2; q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) 0 q2

goal (2 subgoals):
 1. \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) 0 q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0 \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0 \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0) \<in> LS M q1 \<inter> LS M q2
 2. \<And>k q1 q2. \<lbrakk>\<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) k q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2; q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) 0 q2

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0 \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0 \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0 \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0 \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0) \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. \<And>k q1 q2. \<lbrakk>\<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) k q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2; q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k q1 q2. \<lbrakk>\<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) k q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2; q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q1.0 \<in> FSM.states M; ?q2.0 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) k ?q1.0 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k ?q2.0\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M ?q1.0 ?q2.0 k \<in> LS M ?q1.0 \<union> LS M ?q2.0 \<and> assemble_distinguishing_sequence_from_ofsm_table M ?q1.0 ?q2.0 k \<notin> LS M ?q1.0 \<inter> LS M ?q2.0 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M ?q1.0 ?q2.0 k) \<in> LS M ?q1.0 \<inter> LS M ?q2.0
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q2

goal (1 subgoal):
 1. \<And>k q1 q2. \<lbrakk>\<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) k q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2; q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
obtain x y where s1: "select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x,y),(h_obs M q1 x y, h_obs M q2 x y))"
                 and s2: "\<And> q1' q2' . h_obs M q1 x y = Some q1' \<Longrightarrow> h_obs M q2 x y = Some q2' \<Longrightarrow> ofsm_table M (\<lambda>q . states M) k q1' \<noteq> ofsm_table M (\<lambda>q . states M) k q2'"
                 and s3: "h_obs M q1 x y \<noteq> None \<or> h_obs M q2 x y \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y); \<And>q1' q2'. \<lbrakk>FSM.h_obs M q1 x y = Some q1'; FSM.h_obs M q2 x y = Some q2'\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2'; FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using select_diverging_ofsm_table_io_Some[OF assms(1) Suc.prems]
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. \<lbrakk>select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y); \<And>q1' q2'. \<lbrakk>FSM.h_obs M q1 x y = Some q1'; FSM.h_obs M q2 x y = Some q2'\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2'; FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y); \<And>q1' q2'. \<lbrakk>FSM.h_obs M q1 x y = Some q1'; FSM.h_obs M q2 x y = Some q2'\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2'; FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)
\<lbrakk>FSM.h_obs M q1 x y = Some ?q1'; FSM.h_obs M q2 x y = Some ?q2'\<rbrakk> \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k ?q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k ?q2'
FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None

goal (1 subgoal):
 1. \<And>k q1 q2. \<lbrakk>\<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) k q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2; q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
consider (a) "h_obs M q1 x y = None \<and> h_obs M q2 x y \<noteq> None" |
             (b) "h_obs M q1 x y \<noteq> None \<and> h_obs M q2 x y = None" |
             (c) "h_obs M q1 x y \<noteq> None \<and> h_obs M q2 x y \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> thesis; FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> thesis; FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using s3
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None

goal (1 subgoal):
 1. \<lbrakk>FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> thesis; FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> thesis; FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> ?thesis; FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> ?thesis; FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>k q1 q2. \<lbrakk>\<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) k q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2; q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k) q2\<rbrakk> \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> ?thesis; FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> ?thesis; FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> ?thesis; FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> ?thesis; FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 3. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
case a
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None

goal (3 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 3. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
obtain q2' where "h_obs M q1 x y = None" and "h_obs M q2 x y = Some q2'"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None

goal (1 subgoal):
 1. (\<And>q2'. \<lbrakk>FSM.h_obs M q1 x y = None; FSM.h_obs M q2 x y = Some q2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = None
FSM.h_obs M q2 x y = Some q2'

goal (3 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 3. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q1 x y = None
FSM.h_obs M q2 x y = Some q2'
[PROOF STEP]
have "select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x,y),(None, Some q2'))"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = None
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), None, Some q2')
[PROOF STEP]
using s1
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = None
FSM.h_obs M q2 x y = Some q2'
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), None, Some q2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), None, Some q2')

goal (3 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 3. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), None, Some q2')
[PROOF STEP]
have *:"assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x,y)]"
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), None, Some q2')

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]

goal (3 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 3. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "[(x,y)] \<in> LS M q1 \<union> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<union> LS M q2
[PROOF STEP]
using \<open>h_obs M q2 x y = Some q2'\<close> LS_single_transition[of x y M]
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = Some q2'
([(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
[PROOF STEP]
by (metis UnI2 h_obs_None[OF \<open>observable M\<close>] a fst_conv snd_conv)
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q1 \<union> LS M q2

goal (3 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 3. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q1 \<union> LS M q2

goal (3 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 3. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "[(x,y)] \<notin> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x, y)] \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
using \<open>h_obs M q1 x y = None\<close> LS_single_transition[of x y M]
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 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. [(x, y)] \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
unfolding h_obs_None[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
\<nexists>q'. (q1, 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)] \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
[(x, y)] \<notin> LS M q1 \<inter> LS M q2

goal (3 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 3. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[(x, y)] \<notin> LS M q1 \<inter> LS M q2

goal (3 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 3. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "butlast [(x,y)] \<in> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
using Suc.prems(1,2)
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2

goal (3 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 3. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[(x, y)] \<in> LS M q1 \<union> LS M q2
[(x, y)] \<notin> LS M q1 \<inter> LS M q2
butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q1 \<union> LS M q2
[(x, y)] \<notin> LS M q1 \<inter> LS M q2
butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q1 \<union> LS M q2
[(x, y)] \<notin> LS M q1 \<inter> LS M q2
butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2

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 \<and> butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2

goal (2 subgoals):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
case b
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None
[PROOF STEP]
obtain q1' where "h_obs M q2 x y = None" and "h_obs M q1 x y = Some q1'"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None

goal (1 subgoal):
 1. (\<And>q1'. \<lbrakk>FSM.h_obs M q2 x y = None; FSM.h_obs M q1 x y = Some q1'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = Some q1'

goal (2 subgoals):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = Some q1'
[PROOF STEP]
have "select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x,y),(Some q1',None))"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), Some q1', None)
[PROOF STEP]
using s1
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = Some q1'
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), Some q1', None)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), Some q1', None)

goal (2 subgoals):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), Some q1', None)
[PROOF STEP]
have *:"assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x,y)]"
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), Some q1', None)

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]

goal (2 subgoals):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "[(x,y)] \<in> LS M q1 \<union> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<union> LS M q2
[PROOF STEP]
using \<open>h_obs M q1 x y = Some q1'\<close> LS_single_transition[of x y M]
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = Some q1'
([(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
[PROOF STEP]
by (metis UnI1 assms(1) b fst_conv h_obs_None snd_conv)
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q1 \<union> LS M q2

goal (2 subgoals):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q1 \<union> LS M q2

goal (2 subgoals):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "[(x,y)] \<notin> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x, y)] \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
using \<open>h_obs M q2 x y = None\<close> LS_single_transition[of x y M]
[PROOF STATE]
proof (prove)
using this:
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. [(x, y)] \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
unfolding h_obs_None[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
\<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)] \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
[(x, y)] \<notin> LS M q1 \<inter> LS M q2

goal (2 subgoals):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[(x, y)] \<notin> LS M q1 \<inter> LS M q2

goal (2 subgoals):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "butlast [(x,y)] \<in> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
using Suc.prems(1,2)
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2

goal (2 subgoals):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
 2. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[(x, y)] \<in> LS M q1 \<union> LS M q2
[(x, y)] \<notin> LS M q1 \<inter> LS M q2
butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q1 \<union> LS M q2
[(x, y)] \<notin> LS M q1 \<inter> LS M q2
butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q1 \<union> LS M q2
[(x, y)] \<notin> LS M q1 \<inter> LS M q2
butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2

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 \<and> butlast [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
case c
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
obtain q1' q2' where "h_obs M q1 x y = Some q1'" and "h_obs M q2 x y = Some q2'"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None

goal (1 subgoal):
 1. (\<And>q1' q2'. \<lbrakk>FSM.h_obs M q1 x y = Some q1'; FSM.h_obs M q2 x y = Some q2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = Some q2'
[PROOF STEP]
have "select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x,y),(Some q1', Some q2'))"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), Some q1', Some q2')
[PROOF STEP]
using s1
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = Some q2'
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), Some q1', Some q2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), Some q1', Some q2')

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), Some q1', Some q2')
[PROOF STEP]
have "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (x,y) # (assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k)"
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), Some q1', Some q2')

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (x, y) # assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (x, y) # assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (x, y) # assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
define subseq where subseq: "subseq = (assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k)"
[PROOF STATE]
proof (state)
this:
subseq = assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (x, y) # assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k
subseq = assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k
[PROOF STEP]
have *:"assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (x,y) # subseq"
[PROOF STATE]
proof (prove)
using this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (x, y) # assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k
subseq = assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (x, y) # subseq
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = (x, y) # subseq

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "(q1,x,y,q1') \<in> transitions M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q1, x, y, q1') \<in> FSM.transitions M
[PROOF STEP]
using \<open>h_obs M q1 x y = Some q1'\<close> h_obs_Some[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = Some q1'
(FSM.h_obs M ?q ?x ?y = Some ?q') = ({q'. (?q, ?x, ?y, q') \<in> FSM.transitions M} = {?q'})

goal (1 subgoal):
 1. (q1, x, y, q1') \<in> FSM.transitions M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q1, x, y, q1') \<in> FSM.transitions M

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q1, x, y, q1') \<in> FSM.transitions M
[PROOF STEP]
have "q1' \<in> states M"
[PROOF STATE]
proof (prove)
using this:
(q1, x, y, q1') \<in> FSM.transitions M

goal (1 subgoal):
 1. q1' \<in> FSM.states M
[PROOF STEP]
using fsm_transition_target
[PROOF STATE]
proof (prove)
using this:
(q1, x, y, q1') \<in> FSM.transitions M
?t \<in> FSM.transitions ?M \<Longrightarrow> t_target ?t \<in> FSM.states ?M

goal (1 subgoal):
 1. q1' \<in> FSM.states M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q1' \<in> FSM.states M

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "(q2,x,y,q2') \<in> transitions M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q2, x, y, q2') \<in> FSM.transitions M
[PROOF STEP]
using \<open>h_obs M q2 x y = Some q2'\<close> h_obs_Some[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = Some q2'
(FSM.h_obs M ?q ?x ?y = Some ?q') = ({q'. (?q, ?x, ?y, q') \<in> FSM.transitions M} = {?q'})

goal (1 subgoal):
 1. (q2, x, y, q2') \<in> FSM.transitions M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q2, x, y, q2') \<in> FSM.transitions M

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q2, x, y, q2') \<in> FSM.transitions M
[PROOF STEP]
have "q2' \<in> states M"
[PROOF STATE]
proof (prove)
using this:
(q2, x, y, q2') \<in> FSM.transitions M

goal (1 subgoal):
 1. q2' \<in> FSM.states M
[PROOF STEP]
using fsm_transition_target
[PROOF STATE]
proof (prove)
using this:
(q2, x, y, q2') \<in> FSM.transitions M
?t \<in> FSM.transitions ?M \<Longrightarrow> t_target ?t \<in> FSM.states ?M

goal (1 subgoal):
 1. q2' \<in> FSM.states M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q2' \<in> FSM.states M

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have i1: "subseq \<in> LS M q1' \<union> LS M q2'"
      and  i2: "subseq \<notin> LS M q1' \<inter> LS M q2'"
      and  i3: "butlast subseq \<in> LS M q1' \<inter> LS M q2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseq \<in> LS M q1' \<union> LS M q2' &&& subseq \<notin> LS M q1' \<inter> LS M q2' &&& butlast subseq \<in> LS M q1' \<inter> LS M q2'
[PROOF STEP]
using Suc.IH[OF \<open>q1' \<in> states M\<close> \<open>q2' \<in> states M\<close> s2[OF \<open>h_obs M q1 x y = Some q1'\<close> \<open>h_obs M q2 x y = Some q2'\<close>]]
[PROOF STATE]
proof (prove)
using this:
assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k \<in> LS M q1' \<union> LS M q2' \<and> assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k \<notin> LS M q1' \<inter> LS M q2' \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k) \<in> LS M q1' \<inter> LS M q2'

goal (1 subgoal):
 1. subseq \<in> LS M q1' \<union> LS M q2' &&& subseq \<notin> LS M q1' \<inter> LS M q2' &&& butlast subseq \<in> LS M q1' \<inter> LS M q2'
[PROOF STEP]
unfolding subseq
[PROOF STATE]
proof (prove)
using this:
assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k \<in> LS M q1' \<union> LS M q2' \<and> assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k \<notin> LS M q1' \<inter> LS M q2' \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k) \<in> LS M q1' \<inter> LS M q2'

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k \<in> LS M q1' \<union> LS M q2' &&& assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k \<notin> LS M q1' \<inter> LS M q2' &&& butlast (assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k) \<in> LS M q1' \<inter> LS M q2'
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
subseq \<in> LS M q1' \<union> LS M q2'
subseq \<notin> LS M q1' \<inter> LS M q2'
butlast subseq \<in> LS M q1' \<inter> LS M q2'

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "(x,y) # subseq \<in> LS M q1 \<union> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) # subseq \<in> LS M q1 \<union> LS M q2
[PROOF STEP]
using i1 \<open>(q1,x,y,q1') \<in> transitions M\<close> \<open>(q2,x,y,q2') \<in> transitions M\<close>
[PROOF STATE]
proof (prove)
using this:
subseq \<in> LS M q1' \<union> LS M q2'
(q1, x, y, q1') \<in> FSM.transitions M
(q2, x, y, q2') \<in> FSM.transitions M

goal (1 subgoal):
 1. (x, y) # subseq \<in> LS M q1 \<union> LS M q2
[PROOF STEP]
by (metis LS_prepend_transition Un_iff fst_conv snd_conv)
[PROOF STATE]
proof (state)
this:
(x, y) # subseq \<in> LS M q1 \<union> LS M q2

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x, y) # subseq \<in> LS M q1 \<union> LS M q2

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "(x,y) # subseq \<notin> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) # subseq \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
using observable_language_transition_target[OF \<open>observable M\<close> \<open>(q1,x,y,q1') \<in> transitions M\<close>, of subseq]
              observable_language_transition_target[OF \<open>observable M\<close> \<open>(q2,x,y,q2') \<in> transitions M\<close>, of subseq]
              i2
[PROOF STATE]
proof (prove)
using this:
(t_input (q1, x, y, q1'), t_output (q1, x, y, q1')) # subseq \<in> LS M (t_source (q1, x, y, q1')) \<Longrightarrow> subseq \<in> LS M (t_target (q1, x, y, q1'))
(t_input (q2, x, y, q2'), t_output (q2, x, y, q2')) # subseq \<in> LS M (t_source (q2, x, y, q2')) \<Longrightarrow> subseq \<in> LS M (t_target (q2, x, y, q2'))
subseq \<notin> LS M q1' \<inter> LS M q2'

goal (1 subgoal):
 1. (x, y) # subseq \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
unfolding fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
(x, y) # subseq \<in> LS M q1 \<Longrightarrow> subseq \<in> LS M q1'
(x, y) # subseq \<in> LS M q2 \<Longrightarrow> subseq \<in> LS M q2'
subseq \<notin> LS M q1' \<inter> LS M q2'

goal (1 subgoal):
 1. (x, y) # subseq \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x, y) # subseq \<notin> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x, y) # subseq \<notin> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "butlast ((x,y) # subseq) \<in> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast ((x, y) # subseq) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
using i3 \<open>(q1,x,y,q1') \<in> transitions M\<close> \<open>(q2,x,y,q2') \<in> transitions M\<close>
[PROOF STATE]
proof (prove)
using this:
butlast subseq \<in> LS M q1' \<inter> LS M q2'
(q1, x, y, q1') \<in> FSM.transitions M
(q2, x, y, q2') \<in> FSM.transitions M

goal (1 subgoal):
 1. butlast ((x, y) # subseq) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
by (metis Int_iff LS_prepend_transition LS_single_transition append_butlast_last_id butlast.simps(2) fst_conv language_prefix snd_conv)
[PROOF STATE]
proof (state)
this:
butlast ((x, y) # subseq) \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<and> FSM.h_obs M q2 x y \<noteq> None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x, y) # subseq \<in> LS M q1 \<union> LS M q2
(x, y) # subseq \<notin> LS M q1 \<inter> LS M q2
butlast ((x, y) # subseq) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x, y) # subseq \<in> LS M q1 \<union> LS M q2
(x, y) # subseq \<notin> LS M q1 \<inter> LS M q2
butlast ((x, y) # subseq) \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
(x, y) # subseq \<in> LS M q1 \<union> LS M q2
(x, y) # subseq \<notin> LS M q1 \<inter> LS M q2
butlast ((x, y) # subseq) \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. (x, y) # subseq \<in> LS M q1 \<union> LS M q2 \<and> (x, y) # subseq \<notin> LS M q1 \<inter> LS M q2 \<and> butlast ((x, y) # subseq) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<in> LS M q1 \<inter> LS M q2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2

goal (3 subgoals):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2
 2. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2
 3. butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
show "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2"
       and  "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2"
       and  "butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
using this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 \<and> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 \<and> butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2 &&& assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2 &&& butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<in> LS M q1 \<union> LS M q2
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k \<notin> LS M q1 \<inter> LS M q2
butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<in> LS M q1 \<inter> LS M q2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma assemble_distinguishing_sequence_from_ofsm_table_length :
  "length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<le> k
[PROOF STEP]
proof (induction k arbitrary: q1 q2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q1 q2. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0) \<le> 0
 2. \<And>k q1 q2. (\<And>q1 q2. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<le> k) \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>q1 q2. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0) \<le> 0
 2. \<And>k q1 q2. (\<And>q1 q2. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<le> k) \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0) \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0) \<le> 0

goal (1 subgoal):
 1. \<And>k q1 q2. (\<And>q1 q2. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<le> k) \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k q1 q2. (\<And>q1 q2. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<le> k) \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
length (assemble_distinguishing_sequence_from_ofsm_table M ?q1.0 ?q2.0 k) \<le> k

goal (1 subgoal):
 1. \<And>k q1 q2. (\<And>q1 q2. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<le> k) \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
obtain x y A B where *:"select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x,y),A,B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y A B. select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), A, B) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = (x1, x2) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>x y A B. select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), A, B) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((x, y), A, B)

goal (1 subgoal):
 1. \<And>k q1 q2. (\<And>q1 q2. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k) \<le> k) \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
proof (cases A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = None \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
 2. \<And>a. A = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
A = None

goal (2 subgoals):
 1. A = None \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
 2. \<And>a. A = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = None
[PROOF STEP]
have "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x,y)]"
[PROOF STATE]
proof (prove)
using this:
A = None

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]
[PROOF STEP]
unfolding assemble_distinguishing_sequence_from_ofsm_table.simps * case_prod_conv
[PROOF STATE]
proof (prove)
using this:
A = None

goal (1 subgoal):
 1. (case A of None \<Rightarrow> [(x, y)] | Some q1' \<Rightarrow> case B of None \<Rightarrow> [(x, y)] | Some q2' \<Rightarrow> (x, y) # assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k) = [(x, y)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]

goal (2 subgoals):
 1. A = None \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
 2. \<And>a. A = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]

goal (1 subgoal):
 1. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
by (metis Suc_le_length_iff length_Cons list.distinct(1) not_less_eq_eq)
[PROOF STATE]
proof (state)
this:
length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k

goal (1 subgoal):
 1. \<And>a. A = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. A = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
case (Some q1')
[PROOF STATE]
proof (state)
this:
A = Some q1'

goal (1 subgoal):
 1. \<And>a. A = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
proof (cases B)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. B = None \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
 2. \<And>a. B = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
B = None

goal (2 subgoals):
 1. B = None \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
 2. \<And>a. B = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B = None
[PROOF STEP]
have "assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x,y)]"
[PROOF STATE]
proof (prove)
using this:
B = None

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]
[PROOF STEP]
unfolding assemble_distinguishing_sequence_from_ofsm_table.simps * case_prod_conv Some
[PROOF STATE]
proof (prove)
using this:
B = None

goal (1 subgoal):
 1. (case Some q1' of None \<Rightarrow> [(x, y)] | Some q1' \<Rightarrow> case B of None \<Rightarrow> [(x, y)] | Some q2' \<Rightarrow> (x, y) # assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k) = [(x, y)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]

goal (2 subgoals):
 1. B = None \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
 2. \<And>a. B = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [(x, y)]

goal (1 subgoal):
 1. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
by (metis Suc_le_length_iff length_Cons list.distinct(1) not_less_eq_eq)
[PROOF STATE]
proof (state)
this:
length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k

goal (1 subgoal):
 1. \<And>a. B = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. B = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
case (Some q2')
[PROOF STATE]
proof (state)
this:
B = Some q2'

goal (1 subgoal):
 1. \<And>a. B = Some a \<Longrightarrow> length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k
[PROOF STEP]
unfolding assemble_distinguishing_sequence_from_ofsm_table.simps * \<open>A = Some q1'\<close> Some case_prod_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (case Some q1' of None \<Rightarrow> [(x, y)] | Some q1' \<Rightarrow> case Some q2' of None \<Rightarrow> [(x, y)] | Some q2' \<Rightarrow> (x, y) # assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k) \<le> Suc k
[PROOF STEP]
using Suc.IH[of q1' q2']
[PROOF STATE]
proof (prove)
using this:
length (assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k) \<le> k

goal (1 subgoal):
 1. length (case Some q1' of None \<Rightarrow> [(x, y)] | Some q1' \<Rightarrow> case Some q2' of None \<Rightarrow> [(x, y)] | Some q2' \<Rightarrow> (x, y) # assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k) \<le> Suc k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k)) \<le> Suc k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ofsm_table_fix_partition_fixpoint_trivial_partition :
  assumes "q \<in> states M"
shows "ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) (size M - 1) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q
[PROOF STEP]
have "((\<lambda>q. FSM.states M) ` FSM.states M) = {states M}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>q. FSM.states M) ` FSM.states M = {FSM.states M}
[PROOF STEP]
using fsm_initial[of M]
[PROOF STATE]
proof (prove)
using this:
FSM.initial M \<in> FSM.states M

goal (1 subgoal):
 1. (\<lambda>q. FSM.states M) ` FSM.states M = {FSM.states M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>q. FSM.states M) ` FSM.states M = {FSM.states M}

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>q. FSM.states M) ` FSM.states M = {FSM.states M}
[PROOF STEP]
have *:"card ((\<lambda>q. FSM.states M) ` FSM.states M) = 1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>q. FSM.states M) ` FSM.states M = {FSM.states M}

goal (1 subgoal):
 1. card ((\<lambda>q. FSM.states M) ` FSM.states M) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ((\<lambda>q. FSM.states M) ` FSM.states M) = 1

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q
[PROOF STEP]
using ofsm_table_fix_partition_fixpoint[OF minimise_initial_partition _ assms, of "size M"]
[PROOF STATE]
proof (prove)
using this:
FSM.size M \<le> FSM.size M \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - card ((\<lambda>q. FSM.states M) ` FSM.states M)) q = ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
FSM.size M \<le> FSM.size M \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q = ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = ofsm_table M (\<lambda>q. FSM.states M) (FSM.size M - 1) q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma get_distinguishing_sequence_from_ofsm_tables_is_distinguishing_trace :
  assumes "observable M"
  and     "minimal M"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
  and     "q1 \<noteq> q2"
shows "get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2"
and   "get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2"
and   "butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<in> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2 &&& get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2 &&& butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2
 2. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2
 3. butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
using \<open>minimal M\<close>
[PROOF STATE]
proof (prove)
using this:
minimal M

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
unfolding minimal_observable_code[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
\<forall>q\<in>FSM.states M. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = {q}

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
using assms(3,4,5)
[PROOF STATE]
proof (prove)
using this:
\<forall>q\<in>FSM.states M. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q = {q}
q1 \<in> FSM.states M
q2 \<in> FSM.states M
q1 \<noteq> q2

goal (1 subgoal):
 1. ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (3 subgoals):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2
 2. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2
 3. butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
let ?k = "find_first_distinct_ofsm_table_gt M q1 q2 0"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2
 2. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2
 3. butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "ofsm_table M (\<lambda>q . states M) ?k q1 \<noteq> ofsm_table M (\<lambda>q . states M) ?k q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q2
[PROOF STEP]
using find_first_distinct_ofsm_table_is_first(1)[OF assms(3,4) \<open>ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2\<close>]
[PROOF STATE]
proof (prove)
using this:
ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q2

goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q1 \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q1 q2 0) q2

goal (3 subgoals):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2
 2. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2
 3. butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
have *:"get_distinguishing_sequence_from_ofsm_tables M q1 q2 = assemble_distinguishing_sequence_from_ofsm_table M q1 q2 ?k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 = assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q1 q2 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 = assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q1 q2 0)

goal (3 subgoals):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2
 2. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2
 3. butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
show "get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2"
  and  "get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2"
  and  "butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<in> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2 &&& get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2 &&& butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
using assemble_distinguishing_sequence_from_ofsm_table_distinguishes[OF assms(1,3,4) \<open>ofsm_table M (\<lambda>q . states M) ?k q1 \<noteq> ofsm_table M (\<lambda>q . states M) ?k q2\<close>]
[PROOF STATE]
proof (prove)
using this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q1 q2 0) \<in> LS M q1 \<union> LS M q2
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q1 q2 0) \<notin> LS M q1 \<inter> LS M q2
butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q1 q2 0)) \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2 &&& get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2 &&& butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q1 q2 0) \<in> LS M q1 \<union> LS M q2
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q1 q2 0) \<notin> LS M q1 \<inter> LS M q2
butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q1 q2 0)) \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q1 q2 0) \<in> LS M q1 \<union> LS M q2 &&& assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q1 q2 0) \<notin> LS M q1 \<inter> LS M q2 &&& butlast (assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q1 q2 0)) \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2
butlast (get_distinguishing_sequence_from_ofsm_tables M q1 q2) \<in> LS M q1 \<inter> LS M q2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma get_distinguishing_sequence_from_ofsm_tables_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
  and     "q1 \<noteq> q2"
shows "distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
using get_distinguishing_sequence_from_ofsm_tables_is_distinguishing_trace(1,2)[OF assms]
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
unfolding distinguishes_def
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> LS M q1 \<union> LS M q2 \<and> get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
by blast