[STATEMENT]
lemma assemble_distinguishing_sequence_from_ofsm_table_sym :
  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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 k = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 k
[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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 k
[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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 0
 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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 k; 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) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 0
 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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 k; 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) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 0 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 0

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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 k; 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) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 k; 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) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[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 = assemble_distinguishing_sequence_from_ofsm_table M ?q2.0 ?q1.0 k
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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 k; 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) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
obtain xy a b where "select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy,(a,b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xy a b. select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, a, b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod_cases3
[PROOF STATE]
proof (prove)
using this:
(\<And>a b c. ?y = (a, b, c) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>xy a b. select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, a, b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, a, b)

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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 k; 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) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, a, b)
[PROOF STEP]
have "select_diverging_ofsm_table_io M q2 q1 (Suc k) = (xy,(b, a))"
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, a, b)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (xy, b, a)
[PROOF STEP]
using select_diverging_ofsm_table_io_sym[OF assms(1) Suc.prems]
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, a, b)
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (?io, ?a, ?b) \<Longrightarrow> select_diverging_ofsm_table_io M q2 q1 (Suc k) = (?io, ?b, ?a)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (xy, b, a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q2 q1 (Suc k) = (xy, b, a)

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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 k; 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) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
consider "\<exists> q1' q2' . a = Some q1' \<and> b = Some q2'" | "a = None \<or> b = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> thesis; a = None \<or> b = None \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using option.exhaust_sel
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?option = None \<Longrightarrow> ?P; ?option = Some (the ?option) \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<lbrakk>\<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> thesis; a = None \<or> b = None \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> ?thesis; a = None \<or> b = 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 = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 k; 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) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> ?thesis; a = None \<or> b = None \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> ?thesis; a = None \<or> b = None \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
 2. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<exists>q1' q2'. a = Some q1' \<and> b = Some q2'

goal (2 subgoals):
 1. \<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
 2. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>q1' q2'. a = Some q1' \<and> b = Some q2'
[PROOF STEP]
obtain q1' q2' where "select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy,(Some q1', Some q2'))"
[PROOF STATE]
proof (prove)
using this:
\<exists>q1' q2'. a = Some q1' \<and> b = Some q2'

goal (1 subgoal):
 1. (\<And>q1' q2'. select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, Some q1', Some q2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy,(a,b))\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>q1' q2'. a = Some q1' \<and> b = Some q2'
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, a, b)

goal (1 subgoal):
 1. (\<And>q1' q2'. select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, Some q1', Some q2') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, Some q1', Some q2')

goal (2 subgoals):
 1. \<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
 2. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, Some q1', Some q2')
[PROOF STEP]
have "select_diverging_ofsm_table_io M q2 q1 (Suc k) = (xy,(Some q2', Some q1'))"
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, Some q1', Some q2')

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (xy, Some q2', Some q1')
[PROOF STEP]
using select_diverging_ofsm_table_io_sym[OF assms(1) Suc.prems]
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, Some q1', Some q2')
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (?io, ?a, ?b) \<Longrightarrow> select_diverging_ofsm_table_io M q2 q1 (Suc k) = (?io, ?b, ?a)

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

goal (2 subgoals):
 1. \<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
 2. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
obtain x y where "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 "\<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 "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(1)[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 (2 subgoals):
 1. \<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
 2. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking 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
[PROOF STEP]
have "xy = (x,y)" and "h_obs M q1 x y = Some q1'" and "h_obs M q2 x y = Some q2'"
[PROOF STATE]
proof (prove)
using 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. xy = (x, y) &&& FSM.h_obs M q1 x y = Some q1' &&& FSM.h_obs M q2 x y = Some q2'
[PROOF STEP]
using \<open>select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy,(Some q1', Some q2'))\<close>
[PROOF STATE]
proof (prove)
using 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
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, Some q1', Some q2')

goal (1 subgoal):
 1. xy = (x, y) &&& FSM.h_obs M q1 x y = Some q1' &&& FSM.h_obs M q2 x y = Some q2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xy = (x, y)
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = Some q2'

goal (2 subgoals):
 1. \<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
 2. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xy = (x, y)
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = Some q2'
[PROOF STEP]
have "q1' \<in> states M" and "q2' \<in> states M"
[PROOF STATE]
proof (prove)
using this:
xy = (x, y)
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. q1' \<in> FSM.states M &&& q2' \<in> FSM.states M
[PROOF STEP]
unfolding h_obs_Some[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
xy = (x, y)
{q'. (q1, x, y, q') \<in> FSM.transitions M} = {q1'}
{q'. (q2, x, y, q') \<in> FSM.transitions M} = {q2'}

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

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

goal (2 subgoals):
 1. \<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
 2. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
q1' \<in> FSM.states M
q2' \<in> FSM.states M

goal (2 subgoals):
 1. \<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
 2. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[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) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2'
[PROOF STEP]
using \<open>h_obs M q1 x y = Some q1'\<close> \<open>h_obs M q2 x y = Some q2'\<close> \<open>\<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'\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = Some 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'

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

goal (2 subgoals):
 1. \<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
 2. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking 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'
[PROOF STEP]
have "assemble_distinguishing_sequence_from_ofsm_table M  q1' q2' k = assemble_distinguishing_sequence_from_ofsm_table M  q2' q1' k"
[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 = assemble_distinguishing_sequence_from_ofsm_table M q2' q1' k
[PROOF STEP]
using Suc.IH
[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'
\<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 = assemble_distinguishing_sequence_from_ofsm_table M ?q2.0 ?q1.0 k

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

goal (2 subgoals):
 1. \<exists>q1' q2'. a = Some q1' \<and> b = Some q2' \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
 2. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k = assemble_distinguishing_sequence_from_ofsm_table M q2' q1' k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k = assemble_distinguishing_sequence_from_ofsm_table M q2' q1' k

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
using \<open>select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy,(Some q1', Some q2'))\<close>
            \<open>select_diverging_ofsm_table_io M q2 q1 (Suc k) = (xy,(Some q2', Some q1'))\<close>
[PROOF STATE]
proof (prove)
using this:
assemble_distinguishing_sequence_from_ofsm_table M q1' q2' k = assemble_distinguishing_sequence_from_ofsm_table M q2' q1' k
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy, Some q1', Some q2')
select_diverging_ofsm_table_io M q2 q1 (Suc k) = (xy, Some q2', Some q1')

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

goal (1 subgoal):
 1. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
a = None \<or> b = None

goal (1 subgoal):
 1. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
obtain x y where "xy = (x,y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. xy = (x, y) \<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. xy = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
xy = (x, y)

goal (1 subgoal):
 1. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
have helper: "\<And> f f1 f2 .(case ((x,y),(a,b)) of ((x,y),(Some a',Some b')) \<Rightarrow> f1 x y a' b' | ((x,y),_) \<Rightarrow> f2 x y) = f2 x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f1 f2. (case ((x, y), a, b) of ((x, y), None, b) \<Rightarrow> f2 x y | ((x, y), Some a', None) \<Rightarrow> f2 x y | ((x, y), Some a', Some b') \<Rightarrow> f1 x y a' b') = f2 x y
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
a = None \<or> b = None

goal (1 subgoal):
 1. \<And>f f1 f2. (case ((x, y), a, b) of ((x, y), None, b) \<Rightarrow> f2 x y | ((x, y), Some a', None) \<Rightarrow> f2 x y | ((x, y), Some a', Some b') \<Rightarrow> f1 x y a' b') = f2 x y
[PROOF STEP]
by (metis case_prod_conv option.case_eq_if)
[PROOF STATE]
proof (state)
this:
(case ((x, y), a, b) of ((x, y), None, b) \<Rightarrow> ?f2.0 x y | ((x, y), Some a', None) \<Rightarrow> ?f2.0 x y | ((x, y), Some a', Some b') \<Rightarrow> ?f1.0 x y a' b') = ?f2.0 x y

goal (1 subgoal):
 1. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
have helper2: "\<And> f f1 f2 .(case ((x,y),(b,a)) of ((x,y),(Some a',Some b')) \<Rightarrow> f1 x y a' b' | ((x,y),_) \<Rightarrow> f2 x y) = f2 x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f1 f2. (case ((x, y), b, a) of ((x, y), None, b) \<Rightarrow> f2 x y | ((x, y), Some a', None) \<Rightarrow> f2 x y | ((x, y), Some a', Some b') \<Rightarrow> f1 x y a' b') = f2 x y
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
a = None \<or> b = None

goal (1 subgoal):
 1. \<And>f f1 f2. (case ((x, y), b, a) of ((x, y), None, b) \<Rightarrow> f2 x y | ((x, y), Some a', None) \<Rightarrow> f2 x y | ((x, y), Some a', Some b') \<Rightarrow> f1 x y a' b') = f2 x y
[PROOF STEP]
by (metis case_prod_conv option.case_eq_if)
[PROOF STATE]
proof (state)
this:
(case ((x, y), b, a) of ((x, y), None, b) \<Rightarrow> ?f2.1 x y | ((x, y), Some a', None) \<Rightarrow> ?f2.1 x y | ((x, y), Some a', Some b') \<Rightarrow> ?f1.1 x y a' b') = ?f2.1 x y

goal (1 subgoal):
 1. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
have "assemble_distinguishing_sequence_from_ofsm_table M  q1 q2 (Suc k) = [xy]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [xy]
[PROOF STEP]
unfolding assemble_distinguishing_sequence_from_ofsm_table.simps
                \<open>select_diverging_ofsm_table_io M q1 q2 (Suc k) = (xy,(a, b))\<close>  \<open>xy = (x,y)\<close> helper
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x, y)] = [(x, y)]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [xy]

goal (1 subgoal):
 1. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [xy]

goal (1 subgoal):
 1. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
have "assemble_distinguishing_sequence_from_ofsm_table M  q2 q1 (Suc k) = [xy]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k) = [xy]
[PROOF STEP]
unfolding assemble_distinguishing_sequence_from_ofsm_table.simps
                \<open>select_diverging_ofsm_table_io M q2 q1 (Suc k) = (xy,(b, a))\<close>  \<open>xy = (x,y)\<close> helper2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x, y)] = [(x, y)]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k) = [xy]

goal (1 subgoal):
 1. a = None \<or> b = None \<Longrightarrow> assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [xy]
assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k) = [xy]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = [xy]
assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k) = [xy]

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (Suc k) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (Suc k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_first_distinct_ofsm_table_sym :
  assumes "q1 \<in> FSM.states M"
      and "q2 \<in> FSM.states M"
      and "ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2"
shows  "find_first_distinct_ofsm_table M q1 q2 = find_first_distinct_ofsm_table M q2 q1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 0 = find_first_distinct_ofsm_table_gt M q2 q1 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 0 = find_first_distinct_ofsm_table_gt M q2 q1 0
[PROOF STEP]
have "\<And> q1 q2 . q1 \<in> FSM.states M \<Longrightarrow> q2 \<in> FSM.states M \<Longrightarrow> ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2 \<Longrightarrow> find_first_distinct_ofsm_table M q2 q1 < find_first_distinct_ofsm_table M q1 q2 \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2; find_first_distinct_ofsm_table_gt M q2 q1 0 < find_first_distinct_ofsm_table_gt M q1 q2 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2; find_first_distinct_ofsm_table_gt M q2 q1 0 < find_first_distinct_ofsm_table_gt M q1 q2 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix q1 q2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2; find_first_distinct_ofsm_table_gt M q2 q1 0 < find_first_distinct_ofsm_table_gt M q1 q2 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "q1 \<in> FSM.states M" and "q2 \<in> FSM.states M"
                 and "ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2"
                 and "find_first_distinct_ofsm_table M q2 q1 < find_first_distinct_ofsm_table M q1 q2"
[PROOF STATE]
proof (state)
this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2
find_first_distinct_ofsm_table_gt M q2 q1 0 < find_first_distinct_ofsm_table_gt M q1 q2 0

goal (1 subgoal):
 1. \<And>q1 q2. \<lbrakk>q1 \<in> FSM.states M; q2 \<in> FSM.states M; ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2; find_first_distinct_ofsm_table_gt M q2 q1 0 < find_first_distinct_ofsm_table_gt M q1 q2 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using find_first_distinct_ofsm_table_is_first(1)[OF \<open>q1 \<in> FSM.states M\<close> \<open>q2 \<in> FSM.states M\<close> \<open>ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2\<close>]
            find_first_distinct_ofsm_table_is_first(2)[OF \<open>q1 \<in> FSM.states M\<close> \<open>q2 \<in> FSM.states M\<close> \<open>ofsm_table_fix M (\<lambda>q . states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q . states M) 0 q2\<close> \<open>find_first_distinct_ofsm_table M q2 q1 < find_first_distinct_ofsm_table M q1 q2\<close>]
            \<open>find_first_distinct_ofsm_table M q2 q1 < find_first_distinct_ofsm_table M q1 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
ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q2 q1 0) q1 = ofsm_table M (\<lambda>q. FSM.states M) (find_first_distinct_ofsm_table_gt M q2 q1 0) q2
find_first_distinct_ofsm_table_gt M q2 q1 0 < find_first_distinct_ofsm_table_gt M q1 q2 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q1.0 \<in> FSM.states M; ?q2.0 \<in> FSM.states M; ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q1.0 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q2.0; find_first_distinct_ofsm_table_gt M ?q2.0 ?q1.0 0 < find_first_distinct_ofsm_table_gt M ?q1.0 ?q2.0 0\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 0 = find_first_distinct_ofsm_table_gt M q2 q1 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?q1.0 \<in> FSM.states M; ?q2.0 \<in> FSM.states M; ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q1.0 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q2.0; find_first_distinct_ofsm_table_gt M ?q2.0 ?q1.0 0 < find_first_distinct_ofsm_table_gt M ?q1.0 ?q2.0 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q1.0 \<in> FSM.states M; ?q2.0 \<in> FSM.states M; ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q1.0 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q2.0; find_first_distinct_ofsm_table_gt M ?q2.0 ?q1.0 0 < find_first_distinct_ofsm_table_gt M ?q1.0 ?q2.0 0\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 0 = find_first_distinct_ofsm_table_gt M q2 q1 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q1.0 \<in> FSM.states M; ?q2.0 \<in> FSM.states M; ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q1.0 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 ?q2.0; find_first_distinct_ofsm_table_gt M ?q2.0 ?q1.0 0 < find_first_distinct_ofsm_table_gt M ?q1.0 ?q2.0 0\<rbrakk> \<Longrightarrow> False
q1 \<in> FSM.states M
q2 \<in> FSM.states M
ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q1 \<noteq> ofsm_table_fix M (\<lambda>q. FSM.states M) 0 q2

goal (1 subgoal):
 1. find_first_distinct_ofsm_table_gt M q1 q2 0 = find_first_distinct_ofsm_table_gt M q2 q1 0
[PROOF STEP]
by (metis linorder_neqE_nat)
[PROOF STATE]
proof (state)
this:
find_first_distinct_ofsm_table_gt M q1 q2 0 = find_first_distinct_ofsm_table_gt M q2 q1 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma get_distinguishing_sequence_from_ofsm_tables_sym :
  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 = get_distinguishing_sequence_from_ofsm_tables M q2 q1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 = get_distinguishing_sequence_from_ofsm_tables M q2 q1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 = get_distinguishing_sequence_from_ofsm_tables M q2 q1
[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 (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 = get_distinguishing_sequence_from_ofsm_tables M q2 q1
[PROOF STEP]
let ?k = "find_first_distinct_ofsm_table_gt M q1 q2 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 = get_distinguishing_sequence_from_ofsm_tables M q2 q1
[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 (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 = get_distinguishing_sequence_from_ofsm_tables M q2 q1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 = get_distinguishing_sequence_from_ofsm_tables M q2 q1
[PROOF STEP]
using assemble_distinguishing_sequence_from_ofsm_table_sym[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) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (find_first_distinct_ofsm_table_gt M q1 q2 0)

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 = get_distinguishing_sequence_from_ofsm_tables M q2 q1
[PROOF STEP]
unfolding get_distinguishing_sequence_from_ofsm_tables.simps Let_def
              find_first_distinct_ofsm_table_sym[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:
assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q2 q1 0) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (find_first_distinct_ofsm_table_gt M q2 q1 0)

goal (1 subgoal):
 1. assemble_distinguishing_sequence_from_ofsm_table M q1 q2 (find_first_distinct_ofsm_table_gt M q2 q1 0) = assemble_distinguishing_sequence_from_ofsm_table M q2 q1 (find_first_distinct_ofsm_table_gt M q2 q1 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 = get_distinguishing_sequence_from_ofsm_tables M q2 q1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_distinguishing_sequence_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "\<alpha> \<in> L M"
  and     "\<beta> \<in> L M"
  and     "after_initial M \<alpha> \<noteq> after_initial M \<beta>"
shows "\<exists> io \<in> set (add_distinguishing_sequence M ((\<alpha>,after_initial M \<alpha>),(\<beta>,after_initial M \<beta>)) t) \<union> (set (after t \<alpha>) \<inter> set (after t \<beta>)) .  distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>). distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>). distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io
[PROOF STEP]
have "set (add_distinguishing_sequence M ((\<alpha>,after_initial M \<alpha>),(\<beta>,after_initial M \<beta>)) t) = set (insert empty (get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) = Prefix_Tree.set (Prefix_Tree.insert Prefix_Tree.empty (get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) = Prefix_Tree.set (Prefix_Tree.insert Prefix_Tree.empty (get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>)))

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>). distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) = Prefix_Tree.set (Prefix_Tree.insert Prefix_Tree.empty (get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>)))
[PROOF STEP]
have "get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>) \<in> set (add_distinguishing_sequence M ((\<alpha>,after_initial M \<alpha>),(\<beta>,after_initial M \<beta>)) t) \<union> (set (after t \<alpha>) \<inter> set (after t \<beta>))"
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) = Prefix_Tree.set (Prefix_Tree.insert Prefix_Tree.empty (get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>)))

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>) \<in> Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>)
[PROOF STEP]
unfolding insert_set
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) = Prefix_Tree.set Prefix_Tree.empty \<union> {xs'. \<exists>xs''. get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>) = xs' @ xs''}

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>) \<in> Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>) \<in> Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>). distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>) \<in> Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>) \<in> Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>). distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io
[PROOF STEP]
using get_distinguishing_sequence_from_ofsm_tables_is_distinguishing_trace(1,2)[OF assms(1,2) after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)] assms(5)]
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>) \<in> Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>)
get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>) \<in> LS M (after_initial M \<alpha>) \<union> LS M (after_initial M \<beta>)
get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>) \<notin> LS M (after_initial M \<alpha>) \<inter> LS M (after_initial M \<beta>)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>). distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io
[PROOF STEP]
by (meson distinguishes_def)
[PROOF STATE]
proof (state)
this:
\<exists>io\<in>Prefix_Tree.set (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>). distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_distinguishing_sequence_finite :
  "finite_tree (add_distinguishing_sequence M ((\<alpha>,after_initial M \<alpha>),(\<beta>,after_initial M \<beta>)) t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (add_distinguishing_sequence M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t)
[PROOF STEP]
unfolding add_distinguishing_sequence.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (Prefix_Tree.insert Prefix_Tree.empty (get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>)))
[PROOF STEP]
using insert_finite_tree[OF empty_finite_tree]
[PROOF STATE]
proof (prove)
using this:
finite_tree (Prefix_Tree.insert Prefix_Tree.empty ?xs)

goal (1 subgoal):
 1. finite_tree (Prefix_Tree.insert Prefix_Tree.empty (get_distinguishing_sequence_from_ofsm_tables M (after_initial M \<alpha>) (after_initial M \<beta>)))
[PROOF STEP]
by metis


[STATEMENT]
lemma get_HSI_elem :
  assumes "q2 \<in> states M"
  and     "q2 \<noteq> q1"
shows "get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> set (get_HSI M q1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (get_HSI M q1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (get_HSI M q1)
[PROOF STEP]
have "q2 \<in> list.set (filter ((\<noteq>) q1) (states_as_list M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q2 \<in> list.set (filter ((\<noteq>) q1) (states_as_list M))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q2 \<in> FSM.states M
q2 \<noteq> q1

goal (1 subgoal):
 1. q2 \<in> list.set (filter ((\<noteq>) q1) (states_as_list M))
[PROOF STEP]
unfolding states_as_list_set[of M,symmetric]
[PROOF STATE]
proof (prove)
using this:
q2 \<in> list.set (states_as_list M)
q2 \<noteq> q1

goal (1 subgoal):
 1. q2 \<in> list.set (filter ((\<noteq>) q1) (states_as_list M))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q2 \<in> list.set (filter ((\<noteq>) q1) (states_as_list M))

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (get_HSI M q1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q2 \<in> list.set (filter ((\<noteq>) q1) (states_as_list M))
[PROOF STEP]
have *:"get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> list.set (map (\<lambda>q' . get_distinguishing_sequence_from_ofsm_tables M q1 q') (filter ((\<noteq>) q1) (states_as_list M)))"
[PROOF STATE]
proof (prove)
using this:
q2 \<in> list.set (filter ((\<noteq>) q1) (states_as_list M))

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> list.set (map (get_distinguishing_sequence_from_ofsm_tables M q1) (filter ((\<noteq>) q1) (states_as_list M)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> list.set (map (get_distinguishing_sequence_from_ofsm_tables M q1) (filter ((\<noteq>) q1) (states_as_list M)))

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (get_HSI M q1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (get_HSI M q1)
[PROOF STEP]
using from_list_set_elem[OF *]
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (from_list (map (get_distinguishing_sequence_from_ofsm_tables M q1) (filter ((\<noteq>) q1) (states_as_list M))))

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (get_HSI M q1)
[PROOF STEP]
unfolding get_HSI.simps
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (from_list (map (get_distinguishing_sequence_from_ofsm_tables M q1) (filter ((\<noteq>) q1) (states_as_list M))))

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (from_list (map (get_distinguishing_sequence_from_ofsm_tables M q1) (filter ((\<noteq>) q1) (states_as_list M))))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (get_HSI M q1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma get_HSI_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "q1 \<in> states M" and "q2 \<in> states M" and "q1 \<noteq> q2"
shows "\<exists> io \<in> set (get_HSI M q1) \<inter> set (get_HSI M q2) . distinguishes M q1 q2 io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (get_HSI M q1) \<inter> Prefix_Tree.set (get_HSI M q2). distinguishes M q1 q2 io
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (get_HSI M q1) \<inter> Prefix_Tree.set (get_HSI M q2). distinguishes M q1 q2 io
[PROOF STEP]
have "get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> set (get_HSI M q1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q1)
[PROOF STEP]
using get_HSI_elem[OF assms(4), of q1] assms(5)
[PROOF STATE]
proof (prove)
using this:
q2 \<noteq> q1 \<Longrightarrow> get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (get_HSI M q1)
q1 \<noteq> q2

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q1)
[PROOF STEP]
unfolding get_distinguishing_sequence_from_ofsm_tables_sym[OF assms]
[PROOF STATE]
proof (prove)
using this:
q2 \<noteq> q1 \<Longrightarrow> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q1)
q1 \<noteq> q2

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q1)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q1)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (get_HSI M q1) \<inter> Prefix_Tree.set (get_HSI M q2). distinguishes M q1 q2 io
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q1)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (get_HSI M q1) \<inter> Prefix_Tree.set (get_HSI M q2). distinguishes M q1 q2 io
[PROOF STEP]
have "get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> set (get_HSI M q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q2)
[PROOF STEP]
using get_HSI_elem[OF assms(3)] assms(5)
[PROOF STATE]
proof (prove)
using this:
q1 \<noteq> ?q1.0 \<Longrightarrow> get_distinguishing_sequence_from_ofsm_tables M ?q1.0 q1 \<in> Prefix_Tree.set (get_HSI M ?q1.0)
q1 \<noteq> q2

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q2)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q2)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (get_HSI M q1) \<inter> Prefix_Tree.set (get_HSI M q2). distinguishes M q1 q2 io
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q2)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (get_HSI M q1) \<inter> Prefix_Tree.set (get_HSI M q2). distinguishes M q1 q2 io
[PROOF STEP]
have "distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q2 q1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q2 q1)
[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 q2 q1)
[PROOF STEP]
unfolding get_distinguishing_sequence_from_ofsm_tables_sym[OF assms]
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> LS M q1 \<union> LS M q2
get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<notin> LS M q1 \<inter> LS M q2

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

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

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (get_HSI M q1) \<inter> Prefix_Tree.set (get_HSI M q2). distinguishes M q1 q2 io
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q1)
get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q2)
distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q2 q1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q1)
get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (get_HSI M q2)
distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q2 q1)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (get_HSI M q1) \<inter> Prefix_Tree.set (get_HSI M q2). distinguishes M q1 q2 io
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>io\<in>Prefix_Tree.set (get_HSI M q1) \<inter> Prefix_Tree.set (get_HSI M q2). distinguishes M q1 q2 io

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma get_HSI_finite :
  "finite_tree (get_HSI M q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (get_HSI M q)
[PROOF STEP]
unfolding get_HSI.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))
[PROOF STEP]
using from_list_finite_tree
[PROOF STATE]
proof (prove)
using this:
finite_tree (from_list ?xs)

goal (1 subgoal):
 1. finite_tree (from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))
[PROOF STEP]
by metis


[STATEMENT]
lemma distinguishing_set_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
  and     "q1 \<noteq> q2"
shows "\<exists> io \<in> set (distinguishing_set M) .  distinguishes M q1 q2 io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M q1 q2 io
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M q1 q2 io
[PROOF STEP]
define pairs where pairs: "pairs = filter (\<lambda> (x,y) . x \<noteq> y) (list_ordered_pairs (states_as_list M))"
[PROOF STATE]
proof (state)
this:
pairs = filter (\<lambda>(x, y). x \<noteq> y) (list_ordered_pairs (states_as_list M))

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pairs = filter (\<lambda>(x, y). x \<noteq> y) (list_ordered_pairs (states_as_list M))
[PROOF STEP]
have *: "distinguishing_set M = from_list (map (case_prod (get_distinguishing_sequence_from_ofsm_tables M)) pairs)"
[PROOF STATE]
proof (prove)
using this:
pairs = filter (\<lambda>(x, y). x \<noteq> y) (list_ordered_pairs (states_as_list M))

goal (1 subgoal):
 1. distinguishing_set M = from_list (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinguishing_set M = from_list (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M q1 q2 io
[PROOF STEP]
have "q1 \<in> list.set (states_as_list M)" and "q2 \<in> list.set (states_as_list M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q1 \<in> list.set (states_as_list M) &&& q2 \<in> list.set (states_as_list M)
[PROOF STEP]
unfolding states_as_list_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q1 \<in> FSM.states M &&& q2 \<in> FSM.states M
[PROOF STEP]
using assms(3,4)
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. q1 \<in> FSM.states M &&& q2 \<in> FSM.states M
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
q1 \<in> list.set (states_as_list M)
q2 \<in> list.set (states_as_list M)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q1 \<in> list.set (states_as_list M)
q2 \<in> list.set (states_as_list M)
[PROOF STEP]
have "(q1,q2) \<in> list.set pairs \<or> (q2,q1) \<in> list.set pairs"
[PROOF STATE]
proof (prove)
using this:
q1 \<in> list.set (states_as_list M)
q2 \<in> list.set (states_as_list M)

goal (1 subgoal):
 1. (q1, q2) \<in> list.set pairs \<or> (q2, q1) \<in> list.set pairs
[PROOF STEP]
using list_ordered_pairs_set_containment[OF _ _ assms(5)] assms(5)
[PROOF STATE]
proof (prove)
using this:
q1 \<in> list.set (states_as_list M)
q2 \<in> list.set (states_as_list M)
\<lbrakk>q1 \<in> list.set ?xs; q2 \<in> list.set ?xs\<rbrakk> \<Longrightarrow> (q1, q2) \<in> list.set (list_ordered_pairs ?xs) \<or> (q2, q1) \<in> list.set (list_ordered_pairs ?xs)
q1 \<noteq> q2

goal (1 subgoal):
 1. (q1, q2) \<in> list.set pairs \<or> (q2, q1) \<in> list.set pairs
[PROOF STEP]
unfolding pairs
[PROOF STATE]
proof (prove)
using this:
q1 \<in> list.set (states_as_list M)
q2 \<in> list.set (states_as_list M)
\<lbrakk>q1 \<in> list.set ?xs; q2 \<in> list.set ?xs\<rbrakk> \<Longrightarrow> (q1, q2) \<in> list.set (list_ordered_pairs ?xs) \<or> (q2, q1) \<in> list.set (list_ordered_pairs ?xs)
q1 \<noteq> q2

goal (1 subgoal):
 1. (q1, q2) \<in> list.set (filter (\<lambda>(x, y). x \<noteq> y) (list_ordered_pairs (states_as_list M))) \<or> (q2, q1) \<in> list.set (filter (\<lambda>(x, y). x \<noteq> y) (list_ordered_pairs (states_as_list M)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(q1, q2) \<in> list.set pairs \<or> (q2, q1) \<in> list.set pairs

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q1, q2) \<in> list.set pairs \<or> (q2, q1) \<in> list.set pairs
[PROOF STEP]
have "get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> list.set (map (case_prod (get_distinguishing_sequence_from_ofsm_tables M)) pairs)
              | get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> list.set (map (case_prod (get_distinguishing_sequence_from_ofsm_tables M)) pairs)"
[PROOF STATE]
proof (prove)
using this:
(q1, q2) \<in> list.set pairs \<or> (q2, q1) \<in> list.set pairs

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs) \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs)
[PROOF STEP]
by (metis image_iff old.prod.case set_map)
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs) \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs) \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs)
[PROOF STEP]
have "get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> set (distinguishing_set M)
              \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> set (distinguishing_set M)"
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs) \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs)

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (distinguishing_set M) \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (distinguishing_set M)
[PROOF STEP]
unfolding * from_list_set
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs) \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs)

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Set.insert [] {xs''. \<exists>xs' xs'''. xs' \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs) \<and> xs' = xs'' @ xs'''} \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Set.insert [] {xs''. \<exists>xs' xs'''. xs' \<in> list.set (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) pairs) \<and> xs' = xs'' @ xs'''}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (distinguishing_set M) \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (distinguishing_set M)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (distinguishing_set M) \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (distinguishing_set M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (distinguishing_set M) \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (distinguishing_set M)

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M q1 q2 io
[PROOF STEP]
using get_distinguishing_sequence_from_ofsm_tables_is_distinguishing_trace(1,2)[OF assms]
          get_distinguishing_sequence_from_ofsm_tables_is_distinguishing_trace(1,2)[OF assms(1,2,4,3)] assms(5)
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (distinguishing_set M) \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (distinguishing_set M)
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
q2 \<noteq> q1 \<Longrightarrow> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> LS M q2 \<union> LS M q1
q2 \<noteq> q1 \<Longrightarrow> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<notin> LS M q2 \<inter> LS M q1
q1 \<noteq> q2

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M q1 q2 io
[PROOF STEP]
unfolding distinguishes_def
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (distinguishing_set M) \<or> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> Prefix_Tree.set (distinguishing_set M)
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
q2 \<noteq> q1 \<Longrightarrow> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<in> LS M q2 \<union> LS M q1
q2 \<noteq> q1 \<Longrightarrow> get_distinguishing_sequence_from_ofsm_tables M q2 q1 \<notin> LS M q2 \<inter> LS M q1
q1 \<noteq> q2

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set M). io \<in> LS M q1 \<union> LS M q2 \<and> io \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M q1 q2 io

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinguishing_set_finite :
  "finite_tree (distinguishing_set M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (distinguishing_set M)
[PROOF STEP]
unfolding distinguishing_set.simps Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (from_list (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) (filter (\<lambda>(x, y). x \<noteq> y) (list_ordered_pairs (states_as_list M)))))
[PROOF STEP]
using from_list_finite_tree
[PROOF STATE]
proof (prove)
using this:
finite_tree (from_list ?xs)

goal (1 subgoal):
 1. finite_tree (from_list (map (\<lambda>(x, y). get_distinguishing_sequence_from_ofsm_tables M x y) (filter (\<lambda>(x, y). x \<noteq> y) (list_ordered_pairs (states_as_list M)))))
[PROOF STEP]
by metis


[STATEMENT]
lemma intersection_is_distinguishing_code[code] :
  "intersection_is_distinguishing M (MPT t1) q1 (MPT t2) q2 =
    (\<exists> (x,y) \<in> Mapping.keys t1 \<inter> Mapping.keys t2 .
      case h_obs M q1 x y of
        None \<Rightarrow> h_obs M q2 x y \<noteq> None |
        Some q1' \<Rightarrow> (case h_obs M q2 x y of
          None \<Rightarrow> True |
          Some q2' \<Rightarrow> intersection_is_distinguishing M (the (Mapping.lookup t1 (x,y))) q1' (the (Mapping.lookup  t2 (x,y))) q2'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intersection_is_distinguishing M (MPT t1) q1 (MPT t2) q2 = (\<exists>(x, y)\<in>Mapping.keys t1 \<inter> Mapping.keys t2. case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some q2' \<Rightarrow> intersection_is_distinguishing M (the (Mapping.lookup t1 (x, y))) q1' (the (Mapping.lookup t2 (x, y))) q2')
[PROOF STEP]
unfolding intersection_is_distinguishing.simps MPT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>(x, y)\<in>dom (Mapping.lookup t1) \<inter> dom (Mapping.lookup t2). case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some xa \<Rightarrow> intersection_is_distinguishing M (the (Mapping.lookup t1 (x, y))) q1' (the (Mapping.lookup t2 (x, y))) xa) = (\<exists>(x, y)\<in>Mapping.keys t1 \<inter> Mapping.keys t2. case FSM.h_obs M q1 x y of None \<Rightarrow> FSM.h_obs M q2 x y \<noteq> None | Some q1' \<Rightarrow> case FSM.h_obs M q2 x y of None \<Rightarrow> True | Some q2' \<Rightarrow> intersection_is_distinguishing M (the (Mapping.lookup t1 (x, y))) q1' (the (Mapping.lookup t2 (x, y))) q2')
[PROOF STEP]
by (simp add: keys_dom_lookup)