[STATEMENT]
lemma select_diverging_ofsm_table_io_Some :
  assumes "observable M"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
  and     "ofsm_table M (\<lambda>q . states M) (Suc k) q1 \<noteq> ofsm_table M (\<lambda>q . states M) (Suc k) q2"
obtains 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]
proof -
[PROOF STATE]
proof (state)
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]
let ?res = "select_diverging_ofsm_table_io M q1 q2 (Suc k)"
[PROOF STATE]
proof (state)
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]
define f where f: "f = (\<lambda> (x,y) . case (h_obs M q1 x y, h_obs M q2 x y)
                                of
                                  (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q . states M) k q1' \<noteq> ofsm_table M (\<lambda>q . states M) k q2'
                                                            then Some ((x,y),(Some q1', Some q2'))
                                                            else None |
                                  (None,None) \<Rightarrow> None |
                                  (Some q1', None) \<Rightarrow> Some ((x,y),(Some q1', None)) |
                                  (None, Some q2') \<Rightarrow> Some ((x,y),(None, Some q2')))"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>(x, y). case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2' then Some ((x, y), Some q1', Some q2') else None)

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]
have f1: "\<And> x y . f (x,y) \<noteq> None \<Longrightarrow> f (x,y) = Some ((x,y),(h_obs M q1 x y, h_obs M q2 x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. f (x, y) \<noteq> None \<Longrightarrow> f (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f (x, y) \<noteq> None \<Longrightarrow> f (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f (x, y) \<noteq> None \<Longrightarrow> f (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)
[PROOF STEP]
assume "f (x,y) \<noteq> None"
[PROOF STATE]
proof (state)
this:
f (x, y) \<noteq> None

goal (1 subgoal):
 1. \<And>x y. f (x, y) \<noteq> None \<Longrightarrow> f (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (x, y) \<noteq> None
[PROOF STEP]
show "f (x,y) = Some ((x,y),(h_obs M q1 x y, h_obs M q2 x y))"
[PROOF STATE]
proof (prove)
using this:
f (x, y) \<noteq> None

goal (1 subgoal):
 1. f (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
using this:
(case (x, y) of (x, y) \<Rightarrow> case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2' then Some ((x, y), Some q1', Some q2') else None) \<noteq> None

goal (1 subgoal):
 1. (case (x, y) of (x, y) \<Rightarrow> case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2' then Some ((x, y), Some q1', Some q2') else None) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)
[PROOF STEP]
by (cases "h_obs M q1 x y"; cases "h_obs M q2 x y"; auto)
[PROOF STATE]
proof (state)
this:
f (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (?x, ?y) \<noteq> None \<Longrightarrow> f (?x, ?y) = Some ((?x, ?y), FSM.h_obs M q1 ?x ?y, FSM.h_obs M q2 ?x ?y)

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]
have f2 : "\<And> q1' q2' x y . f (x,y) = Some ((x,y),(Some q1', Some q2')) \<Longrightarrow> 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. \<And>q1' q2' x y. f (x, y) = Some ((x, y), Some q1', Some q2') \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q1' q2' x y. f (x, y) = Some ((x, y), Some q1', Some q2') \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2'
[PROOF STEP]
fix q1' q2' x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q1' q2' x y. f (x, y) = Some ((x, y), Some q1', Some q2') \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2'
[PROOF STEP]
assume *: "f (x,y) = Some ((x,y),(Some q1', Some q2'))"
[PROOF STATE]
proof (state)
this:
f (x, y) = Some ((x, y), Some q1', Some q2')

goal (1 subgoal):
 1. \<And>q1' q2' x y. f (x, y) = Some ((x, y), Some q1', Some q2') \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (x, y) = Some ((x, y), Some q1', Some q2')
[PROOF STEP]
have **: "f (x,y) = Some ((x,y),(h_obs M q1 x y, h_obs M q2 x y))"
[PROOF STATE]
proof (prove)
using this:
f (x, y) = Some ((x, y), Some q1', Some q2')

goal (1 subgoal):
 1. f (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
f (x, y) = Some ((x, y), Some q1', Some q2')
f (?x, ?y) \<noteq> None \<Longrightarrow> f (?x, ?y) = Some ((?x, ?y), FSM.h_obs M q1 ?x ?y, FSM.h_obs M q2 ?x ?y)

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

goal (1 subgoal):
 1. \<And>q1' q2' x y. f (x, y) = Some ((x, y), Some q1', Some q2') \<Longrightarrow> ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2'
[PROOF STEP]
show "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 * **
[PROOF STATE]
proof (prove)
using this:
f (x, y) = Some ((x, y), Some q1', Some q2')
f (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)

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]
unfolding f
[PROOF STATE]
proof (prove)
using this:
(case (x, y) of (x, y) \<Rightarrow> case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2' then Some ((x, y), Some q1', Some q2') else None) = Some ((x, y), Some q1', Some q2')
(case (x, y) of (x, y) \<Rightarrow> case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2' then Some ((x, y), Some q1', Some q2') else None) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)

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 (cases "h_obs M q1 x y"; cases "h_obs M q2 x y"; auto)
[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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (?x, ?y) = Some ((?x, ?y), Some ?q1', Some ?q2') \<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. (\<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]
have f3: "\<And> x y . f (x,y) \<noteq> None \<Longrightarrow> 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. f (x, y) \<noteq> None \<Longrightarrow> FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f (x, y) \<noteq> None \<Longrightarrow> FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f (x, y) \<noteq> None \<Longrightarrow> FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
assume "f (x,y) \<noteq> None"
[PROOF STATE]
proof (state)
this:
f (x, y) \<noteq> None

goal (1 subgoal):
 1. \<And>x y. f (x, y) \<noteq> None \<Longrightarrow> FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (x, y) \<noteq> None
[PROOF STEP]
show "h_obs M q1 x y \<noteq> None \<or> h_obs M q2 x y \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
f (x, y) \<noteq> None

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
using this:
(case (x, y) of (x, y) \<Rightarrow> case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2' then Some ((x, y), Some q1', Some q2') else None) \<noteq> None

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
by (cases "h_obs M q1 x y"; cases "h_obs M q2 x y"; auto)
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y \<noteq> None \<or> FSM.h_obs M q2 x y \<noteq> None

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (?x, ?y) \<noteq> None \<Longrightarrow> FSM.h_obs M q1 ?x ?y \<noteq> None \<or> FSM.h_obs M q2 ?x ?y \<noteq> None

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]
have *: "select_diverging_ofsm_table_io M q1 q2 (Suc k) = hd (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) = hd (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
unfolding f select_diverging_ofsm_table_io.simps Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (List.map_filter (\<lambda>(x, y). case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' then Some ((x, y), Some q1', Some q2') else None) (List.product (inputs_as_list M) (outputs_as_list M))) = hd (List.map_filter (\<lambda>(x, y). case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2' then Some ((x, y), Some q1', Some q2') else None) (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
using diff_Suc_1
[PROOF STATE]
proof (prove)
using this:
Suc ?n - 1 = ?n

goal (1 subgoal):
 1. hd (List.map_filter (\<lambda>(x, y). case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' then Some ((x, y), Some q1', Some q2') else None) (List.product (inputs_as_list M) (outputs_as_list M))) = hd (List.map_filter (\<lambda>(x, y). case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2' then Some ((x, y), Some q1', Some q2') else None) (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = hd (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))

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]
let ?P = "\<forall> x y . x \<in> inputs M \<longrightarrow> y \<in> outputs M \<longrightarrow> (h_obs M q1 x y = None \<longleftrightarrow> h_obs M q2 x y = None)"
[PROOF STATE]
proof (state)
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]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (cases ?P)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
 2. \<not> (\<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None)) \<Longrightarrow> thesis
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None))

goal (2 subgoals):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
 2. \<not> (\<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None)) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None))
[PROOF STEP]
obtain x y where "x \<in> inputs M" and "y \<in> outputs M" and "\<not> (h_obs M q1 x y = None \<longleftrightarrow> h_obs M q2 x y = None)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None))

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

goal (2 subgoals):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
 2. \<not> (\<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None)) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> FSM.inputs M
y \<in> FSM.outputs M
(FSM.h_obs M q1 x y = None) \<noteq> (FSM.h_obs M q2 x y = None)
[PROOF STEP]
consider "h_obs M q1 x y = None \<and> (\<exists> q2' . h_obs M q2 x y = Some q2')" |
                  "h_obs M q2 x y = None \<and> (\<exists> q1' . h_obs M q1 x y = Some q1')"
[PROOF STATE]
proof (prove)
using this:
x \<in> FSM.inputs M
y \<in> FSM.outputs M
(FSM.h_obs M q1 x y = None) \<noteq> (FSM.h_obs M q2 x y = None)

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

goal (2 subgoals):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
 2. \<not> (\<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None)) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> ?thesis; FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> ?thesis; FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2')

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2')
[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> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2')

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 (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[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 "f (x,y) = Some ((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. f (x, y) = Some ((x, y), None, Some q2')
[PROOF STEP]
unfolding f
[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. (case (x, y) of (x, y) \<Rightarrow> case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2' then Some ((x, y), Some q1', Some q2') else None) = Some ((x, y), None, Some q2')
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f (x, y) = Some ((x, y), None, Some q2')

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f (x, y) = Some ((x, y), None, Some q2')

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
have "(x,y) \<in> set (List.product(inputs_as_list M) (outputs_as_list M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
using \<open>y \<in> outputs M\<close> outputs_as_list_set[of M]
[PROOF STATE]
proof (prove)
using this:
y \<in> FSM.outputs M
set (outputs_as_list M) = FSM.outputs M

goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
using \<open>x \<in> inputs M\<close> inputs_as_list_set[of M]
[PROOF STATE]
proof (prove)
using this:
y \<in> FSM.outputs M
set (outputs_as_list M) = FSM.outputs M
x \<in> FSM.inputs M
set (inputs_as_list M) = FSM.inputs M

goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
using image_iff
[PROOF STATE]
proof (prove)
using this:
y \<in> FSM.outputs M
set (outputs_as_list M) = FSM.outputs M
x \<in> FSM.inputs M
set (inputs_as_list M) = FSM.inputs M
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)

goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (x, y) = Some ((x, y), None, Some q2')
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
have "(List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M))) \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
f (x, y) = Some ((x, y), None, Some q2')
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))

goal (1 subgoal):
 1. List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []
[PROOF STEP]
unfolding List.map_filter_def
[PROOF STATE]
proof (prove)
using this:
f (x, y) = Some ((x, y), None, Some q2')
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))

goal (1 subgoal):
 1. map (the \<circ> f) (filter (\<lambda>x. f x \<noteq> None) (List.product (inputs_as_list M) (outputs_as_list M))) \<noteq> []
[PROOF STEP]
by (metis (mono_tags, lifting) Nil_is_map_conv filter_empty_conv option.discI)
[PROOF STATE]
proof (state)
this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []
[PROOF STEP]
have **: "?res \<in> set (List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M)))"
[PROOF STATE]
proof (prove)
using this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []

goal (1 subgoal):
 1. hd (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M))) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
using hd_in_set
[PROOF STATE]
proof (prove)
using this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []
?xs \<noteq> [] \<Longrightarrow> hd ?xs \<in> set ?xs

goal (1 subgoal):
 1. hd (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M))) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
obtain xR yR where "(xR,yR) \<in> set (List.product(inputs_as_list M) (outputs_as_list M))"
                     and res: "f (xR,yR) = Some ?res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xR yR. \<lbrakk>(xR, yR) \<in> set (List.product (inputs_as_list M) (outputs_as_list M)); f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using map_filter_elem[OF **]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. \<lbrakk>x \<in> set (List.product (inputs_as_list M) (outputs_as_list M)); f x = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>xR yR. \<lbrakk>(xR, yR) \<in> set (List.product (inputs_as_list M) (outputs_as_list M)); f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.exhaust_sel)
[PROOF STATE]
proof (state)
this:
(xR, yR) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
have p1: "?res = ((xR,yR),(h_obs M q1 xR yR, h_obs M q2 xR yR))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
[PROOF STEP]
using res f1
[PROOF STATE]
proof (prove)
using this:
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))
f (?x, ?y) \<noteq> None \<Longrightarrow> f (?x, ?y) = Some ((?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) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
[PROOF STEP]
by (metis option.distinct(1) option.sel)
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
[PROOF STEP]
have p2: "\<And> q1' q2' . h_obs M q1 xR yR = Some q1' \<Longrightarrow> h_obs M q2 xR yR = Some q2' \<Longrightarrow> ofsm_table M (\<lambda>q . states M) k q1' \<noteq> ofsm_table M (\<lambda>q . states M) k q2'"
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)

goal (1 subgoal):
 1. \<And>q1' q2'. \<lbrakk>FSM.h_obs M q1 xR yR = Some q1'; FSM.h_obs M q2 xR yR = 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'
[PROOF STEP]
using res f1 f2
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))
f (?x, ?y) \<noteq> None \<Longrightarrow> f (?x, ?y) = Some ((?x, ?y), FSM.h_obs M q1 ?x ?y, FSM.h_obs M q2 ?x ?y)
f (?x, ?y) = Some ((?x, ?y), Some ?q1', Some ?q2') \<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. \<And>q1' q2'. \<lbrakk>FSM.h_obs M q1 xR yR = Some q1'; FSM.h_obs M q2 xR yR = 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'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>FSM.h_obs M q1 xR yR = Some ?q1'; FSM.h_obs M q2 xR yR = 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 (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
have p3: "h_obs M q1 xR yR \<noteq> None \<or> h_obs M q2 xR yR \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.h_obs M q1 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None
[PROOF STEP]
using res f3
[PROOF STATE]
proof (prove)
using this:
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))
f (?x, ?y) \<noteq> None \<Longrightarrow> FSM.h_obs M q1 ?x ?y \<noteq> None \<or> FSM.h_obs M q2 ?x ?y \<noteq> None

goal (1 subgoal):
 1. FSM.h_obs M q1 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<and> (\<exists>q2'. FSM.h_obs M q2 x y = Some q2') \<Longrightarrow> thesis
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that p1 p2 p3
[PROOF STATE]
proof (prove)
using this:
\<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
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
\<lbrakk>FSM.h_obs M q1 xR yR = Some ?q1'; FSM.h_obs M q2 xR yR = 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 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None

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

goal (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1')

goal (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1')
[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 q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1')

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 (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[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 "f (x,y) = Some ((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. f (x, y) = Some ((x, y), Some q1', None)
[PROOF STEP]
unfolding f
[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. (case (x, y) of (x, y) \<Rightarrow> case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2' then Some ((x, y), Some q1', Some q2') else None) = Some ((x, y), Some q1', None)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f (x, y) = Some ((x, y), Some q1', None)

goal (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f (x, y) = Some ((x, y), Some q1', None)

goal (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
have "(x,y) \<in> set (List.product(inputs_as_list M) (outputs_as_list M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
using \<open>y \<in> outputs M\<close> outputs_as_list_set[of M]
[PROOF STATE]
proof (prove)
using this:
y \<in> FSM.outputs M
set (outputs_as_list M) = FSM.outputs M

goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
using \<open>x \<in> inputs M\<close> inputs_as_list_set[of M]
[PROOF STATE]
proof (prove)
using this:
y \<in> FSM.outputs M
set (outputs_as_list M) = FSM.outputs M
x \<in> FSM.inputs M
set (inputs_as_list M) = FSM.inputs M

goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
using image_iff
[PROOF STATE]
proof (prove)
using this:
y \<in> FSM.outputs M
set (outputs_as_list M) = FSM.outputs M
x \<in> FSM.inputs M
set (inputs_as_list M) = FSM.inputs M
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)

goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))

goal (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (x, y) = Some ((x, y), Some q1', None)
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
have "(List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M))) \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
f (x, y) = Some ((x, y), Some q1', None)
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))

goal (1 subgoal):
 1. List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []
[PROOF STEP]
unfolding List.map_filter_def
[PROOF STATE]
proof (prove)
using this:
f (x, y) = Some ((x, y), Some q1', None)
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))

goal (1 subgoal):
 1. map (the \<circ> f) (filter (\<lambda>x. f x \<noteq> None) (List.product (inputs_as_list M) (outputs_as_list M))) \<noteq> []
[PROOF STEP]
by (metis (mono_tags, lifting) Nil_is_map_conv filter_empty_conv option.discI)
[PROOF STATE]
proof (state)
this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []

goal (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []
[PROOF STEP]
have **: "?res \<in> set (List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M)))"
[PROOF STATE]
proof (prove)
using this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []

goal (1 subgoal):
 1. hd (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M))) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
using hd_in_set
[PROOF STATE]
proof (prove)
using this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []
?xs \<noteq> [] \<Longrightarrow> hd ?xs \<in> set ?xs

goal (1 subgoal):
 1. hd (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M))) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))

goal (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
obtain xR yR where "(xR,yR) \<in> set (List.product(inputs_as_list M) (outputs_as_list M))"
                     and res: "f (xR,yR) = Some ?res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xR yR. \<lbrakk>(xR, yR) \<in> set (List.product (inputs_as_list M) (outputs_as_list M)); f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using map_filter_elem[OF **]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. \<lbrakk>x \<in> set (List.product (inputs_as_list M) (outputs_as_list M)); f x = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>xR yR. \<lbrakk>(xR, yR) \<in> set (List.product (inputs_as_list M) (outputs_as_list M)); f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.exhaust_sel)
[PROOF STATE]
proof (state)
this:
(xR, yR) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))

goal (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
have p1: "?res = ((xR,yR),(h_obs M q1 xR yR, h_obs M q2 xR yR))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
[PROOF STEP]
using res f1
[PROOF STATE]
proof (prove)
using this:
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))
f (?x, ?y) \<noteq> None \<Longrightarrow> f (?x, ?y) = Some ((?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) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
[PROOF STEP]
by (metis option.distinct(1) option.sel)
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)

goal (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
[PROOF STEP]
have p2: "\<And> q1' q2' . h_obs M q1 xR yR = Some q1' \<Longrightarrow> h_obs M q2 xR yR = Some q2' \<Longrightarrow> ofsm_table M (\<lambda>q . states M) k q1' \<noteq> ofsm_table M (\<lambda>q . states M) k q2'"
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)

goal (1 subgoal):
 1. \<And>q1' q2'. \<lbrakk>FSM.h_obs M q1 xR yR = Some q1'; FSM.h_obs M q2 xR yR = 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'
[PROOF STEP]
using res f1 f2
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))
f (?x, ?y) \<noteq> None \<Longrightarrow> f (?x, ?y) = Some ((?x, ?y), FSM.h_obs M q1 ?x ?y, FSM.h_obs M q2 ?x ?y)
f (?x, ?y) = Some ((?x, ?y), Some ?q1', Some ?q2') \<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. \<And>q1' q2'. \<lbrakk>FSM.h_obs M q1 xR yR = Some q1'; FSM.h_obs M q2 xR yR = 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'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>FSM.h_obs M q1 xR yR = Some ?q1'; FSM.h_obs M q2 xR yR = 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. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
have p3: "h_obs M q1 xR yR \<noteq> None \<or> h_obs M q2 xR yR \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.h_obs M q1 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None
[PROOF STEP]
using res f3
[PROOF STATE]
proof (prove)
using this:
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))
f (?x, ?y) \<noteq> None \<Longrightarrow> FSM.h_obs M q1 ?x ?y \<noteq> None \<or> FSM.h_obs M q2 ?x ?y \<noteq> None

goal (1 subgoal):
 1. FSM.h_obs M q1 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None

goal (1 subgoal):
 1. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that p1 p2 p3
[PROOF STATE]
proof (prove)
using this:
\<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
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
\<lbrakk>FSM.h_obs M q1 xR yR = Some ?q1'; FSM.h_obs M q2 xR yR = 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 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None)

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
obtain io where "length io \<le> Suc k" and "io \<in> LS M q1 \<union> LS M q2" and "io \<notin> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>io. \<lbrakk>length io \<le> Suc k; io \<in> LS M q1 \<union> LS M q2; io \<notin> LS M q1 \<inter> LS M q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>ofsm_table M (\<lambda>q . states M) (Suc k) q1 \<noteq> ofsm_table M (\<lambda>q . states M) (Suc k) q2\<close>
[PROOF STATE]
proof (prove)
using this:
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>io. \<lbrakk>length io \<le> Suc k; io \<in> LS M q1 \<union> LS M q2; io \<notin> LS M q1 \<inter> LS M q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ofsm_table_set[OF assms(2) minimise_initial_partition] ofsm_table_set[OF assms(3) minimise_initial_partition]
[PROOF STATE]
proof (prove)
using this:
{q' \<in> FSM.states M. \<forall>io. length io \<le> Suc k \<longrightarrow> is_in_language M q1 io = is_in_language M q' io \<and> (is_in_language M q1 io \<longrightarrow> after M q' io \<in> FSM.states M)} \<noteq> {q' \<in> FSM.states M. \<forall>io. length io \<le> Suc k \<longrightarrow> is_in_language M q2 io = is_in_language M q' io \<and> (is_in_language M q2 io \<longrightarrow> after M q' io \<in> FSM.states M)}

goal (1 subgoal):
 1. (\<And>io. \<lbrakk>length io \<le> Suc k; io \<in> LS M q1 \<union> LS M q2; io \<notin> LS M q1 \<inter> LS M q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_in_language_iff[OF assms(1,2)] is_in_language_iff[OF assms(1,3)]
[PROOF STATE]
proof (prove)
using this:
{q' \<in> FSM.states M. \<forall>io. length io \<le> Suc k \<longrightarrow> (io \<in> LS M q1) = is_in_language M q' io \<and> (io \<in> LS M q1 \<longrightarrow> after M q' io \<in> FSM.states M)} \<noteq> {q' \<in> FSM.states M. \<forall>io. length io \<le> Suc k \<longrightarrow> (io \<in> LS M q2) = is_in_language M q' io \<and> (io \<in> LS M q2 \<longrightarrow> after M q' io \<in> FSM.states M)}

goal (1 subgoal):
 1. (\<And>io. \<lbrakk>length io \<le> Suc k; io \<in> LS M q1 \<union> LS M q2; io \<notin> LS M q1 \<inter> LS M q2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length io \<le> Suc k
io \<in> LS M q1 \<union> LS M q2
io \<notin> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length io \<le> Suc k
io \<in> LS M q1 \<union> LS M q2
io \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
have "io \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
length io \<le> Suc k
io \<in> LS M q1 \<union> LS M q2
io \<notin> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. io \<noteq> []
[PROOF STEP]
using assms(2) assms(3)
[PROOF STATE]
proof (prove)
using this:
length io \<le> Suc k
io \<in> LS M q1 \<union> LS M q2
io \<notin> LS M q1 \<inter> LS M q2
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. io \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io \<noteq> []

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<noteq> []
[PROOF STEP]
have "io = [hd io] @ tl io"
[PROOF STATE]
proof (prove)
using this:
io \<noteq> []

goal (1 subgoal):
 1. io = [hd io] @ tl io
[PROOF STEP]
by (metis append.left_neutral append_Cons list.exhaust_sel)
[PROOF STATE]
proof (state)
this:
io = [hd io] @ tl io

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io = [hd io] @ tl io
[PROOF STEP]
obtain x y where "hd io = (x,y)"
[PROOF STATE]
proof (prove)
using this:
io = [hd io] @ tl io

goal (1 subgoal):
 1. (\<And>x y. hd io = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson prod.exhaust_sel)
[PROOF STATE]
proof (state)
this:
hd io = (x, y)

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
have "[(x,y)] \<in> LS M q1 \<inter> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(x, y)] \<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>io \<in> LS M q1 \<union> LS M q2\<close> language_prefix \<open>hd io = (x,y)\<close> \<open>io = [hd io] @ tl io\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> LS M q1 \<union> LS M q2
?io1.0 @ ?io2.0 \<in> LS ?M ?q \<Longrightarrow> ?io1.0 \<in> LS ?M ?q
hd io = (x, y)
io = [hd io] @ tl io

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

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x, y)] \<in> LS M q1 \<union> LS M q2
[PROOF STEP]
have "x \<in> inputs M" and "y \<in> outputs M"
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q1 \<union> LS M q2

goal (1 subgoal):
 1. x \<in> FSM.inputs M &&& y \<in> FSM.outputs M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> FSM.inputs M
y \<in> FSM.outputs M

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
consider "[(x,y)] \<in> LS M q1" | "[(x,y)] \<in> LS M q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>[(x, y)] \<in> LS M q1 \<Longrightarrow> thesis; [(x, y)] \<in> LS M q2 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using \<open>[(x,y)] \<in> LS M q1 \<union> LS M q2\<close>
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q1 \<union> LS M q2

goal (1 subgoal):
 1. \<lbrakk>[(x, y)] \<in> LS M q1 \<Longrightarrow> thesis; [(x, y)] \<in> LS M q2 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>[(x, y)] \<in> LS M q1 \<Longrightarrow> ?thesis; [(x, y)] \<in> LS M q2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>[(x, y)] \<in> LS M q1 \<Longrightarrow> ?thesis; [(x, y)] \<in> LS M q2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>[(x, y)] \<in> LS M q1 \<Longrightarrow> ?thesis; [(x, y)] \<in> LS M q2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [(x, y)] \<in> LS M q1 \<Longrightarrow> [(x, y)] \<in> LS M q1 \<inter> LS M q2
 2. [(x, y)] \<in> LS M q2 \<Longrightarrow> [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q1

goal (2 subgoals):
 1. [(x, y)] \<in> LS M q1 \<Longrightarrow> [(x, y)] \<in> LS M q1 \<inter> LS M q2
 2. [(x, y)] \<in> LS M q2 \<Longrightarrow> [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x, y)] \<in> LS M q1
[PROOF STEP]
have "h_obs M q1 x y \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q1

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None
[PROOF STEP]
using h_obs_None[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q1
(FSM.h_obs M ?q ?x ?y = None) = (\<nexists>q'. (?q, ?x, ?y, q') \<in> FSM.transitions M)

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None
[PROOF STEP]
unfolding LS_single_transition
[PROOF STATE]
proof (prove)
using this:
\<exists>t\<in>FSM.transitions M. t_source t = q1 \<and> t_input t = x \<and> t_output t = y
(FSM.h_obs M ?q ?x ?y = None) = (\<nexists>q'. (?q, ?x, ?y, q') \<in> FSM.transitions M)

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y \<noteq> None

goal (2 subgoals):
 1. [(x, y)] \<in> LS M q1 \<Longrightarrow> [(x, y)] \<in> LS M q1 \<inter> LS M q2
 2. [(x, y)] \<in> LS M q2 \<Longrightarrow> [(x, y)] \<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
[PROOF STEP]
have "h_obs M q2 x y \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y \<noteq> None

goal (1 subgoal):
 1. FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
using True \<open>x \<in> inputs M\<close> \<open>y \<in> outputs M\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y \<noteq> None
\<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None)
x \<in> FSM.inputs M
y \<in> FSM.outputs M

goal (1 subgoal):
 1. FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y \<noteq> None

goal (2 subgoals):
 1. [(x, y)] \<in> LS M q1 \<Longrightarrow> [(x, y)] \<in> LS M q1 \<inter> LS M q2
 2. [(x, y)] \<in> LS M q2 \<Longrightarrow> [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y \<noteq> None

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
using 1 h_obs_None[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y \<noteq> None
[(x, y)] \<in> LS M q1
(FSM.h_obs M ?q ?x ?y = None) = (\<nexists>q'. (?q, ?x, ?y, q') \<in> FSM.transitions M)

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

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q2 \<Longrightarrow> [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(x, y)] \<in> LS M q2 \<Longrightarrow> [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q2

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q2 \<Longrightarrow> [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x, y)] \<in> LS M q2
[PROOF STEP]
have "h_obs M q2 x y \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q2

goal (1 subgoal):
 1. FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
using h_obs_None[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q2
(FSM.h_obs M ?q ?x ?y = None) = (\<nexists>q'. (?q, ?x, ?y, q') \<in> FSM.transitions M)

goal (1 subgoal):
 1. FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
unfolding LS_single_transition
[PROOF STATE]
proof (prove)
using this:
\<exists>t\<in>FSM.transitions M. t_source t = q2 \<and> t_input t = x \<and> t_output t = y
(FSM.h_obs M ?q ?x ?y = None) = (\<nexists>q'. (?q, ?x, ?y, q') \<in> FSM.transitions M)

goal (1 subgoal):
 1. FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y \<noteq> None

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q2 \<Longrightarrow> [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y \<noteq> None
[PROOF STEP]
have "h_obs M q1 x y \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y \<noteq> None

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None
[PROOF STEP]
using True \<open>x \<in> inputs M\<close> \<open>y \<in> outputs M\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y \<noteq> None
\<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None)
x \<in> FSM.inputs M
y \<in> FSM.outputs M

goal (1 subgoal):
 1. FSM.h_obs M q1 x y \<noteq> None
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y \<noteq> None

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q2 \<Longrightarrow> [(x, y)] \<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
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y \<noteq> None

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
using 2 h_obs_None[OF \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y \<noteq> None
[(x, y)] \<in> LS M q2
(FSM.h_obs M ?q ?x ?y = None) = (\<nexists>q'. (?q, ?x, ?y, q') \<in> FSM.transitions M)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q1 \<inter> LS M q2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(x, y)] \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(x, y)] \<in> LS M q1 \<inter> LS M q2
[PROOF STEP]
obtain q1' q2' where "(q1,x,y,q1') \<in> transitions M"
                          and "(q2,x,y,q2') \<in> transitions M"
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q1 \<inter> LS M q2

goal (1 subgoal):
 1. (\<And>q1' q2'. \<lbrakk>(q1, x, y, q1') \<in> FSM.transitions M; (q2, x, y, q2') \<in> FSM.transitions M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using LS_single_transition
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<in> LS M q1 \<inter> LS M 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. (\<And>q1' q2'. \<lbrakk>(q1, x, y, q1') \<in> FSM.transitions M; (q2, x, y, q2') \<in> FSM.transitions M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(q1, x, y, q1') \<in> FSM.transitions M
(q2, x, y, q2') \<in> FSM.transitions M

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q1, x, y, q1') \<in> FSM.transitions M
(q2, x, y, q2') \<in> FSM.transitions M
[PROOF STEP]
have "q1' \<in> states M" and "q2' \<in> states M"
[PROOF STATE]
proof (prove)
using this:
(q1, x, y, q1') \<in> FSM.transitions M
(q2, x, y, q2') \<in> FSM.transitions M

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:
(q1, x, y, q1') \<in> FSM.transitions M
(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. q1' \<in> FSM.states M &&& q2' \<in> FSM.states M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q1' \<in> FSM.states M
q2' \<in> FSM.states M

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
have "tl io \<in> LS M q1' \<union> LS M q2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl io \<in> LS M q1' \<union> LS M q2'
[PROOF STEP]
using observable_language_transition_target[OF \<open>observable M\<close> \<open>(q1,x,y,q1') \<in> transitions M\<close>]
            observable_language_transition_target[OF \<open>observable M\<close> \<open>(q2,x,y,q2') \<in> transitions M\<close>]
            \<open>io \<in> LS M q1 \<union> LS M q2\<close>
[PROOF STATE]
proof (prove)
using this:
(t_input (q1, x, y, q1'), t_output (q1, x, y, q1')) # ?io \<in> LS M (t_source (q1, x, y, q1')) \<Longrightarrow> ?io \<in> LS M (t_target (q1, x, y, q1'))
(t_input (q2, x, y, q2'), t_output (q2, x, y, q2')) # ?io \<in> LS M (t_source (q2, x, y, q2')) \<Longrightarrow> ?io \<in> LS M (t_target (q2, x, y, q2'))
io \<in> LS M q1 \<union> LS M q2

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

goal (1 subgoal):
 1. tl io \<in> LS M q1' \<union> LS M q2'
[PROOF STEP]
by (metis Un_iff \<open>hd io = (x, y)\<close> \<open>io = [hd io] @ tl io\<close> append_Cons append_Nil)
[PROOF STATE]
proof (state)
this:
tl io \<in> LS M q1' \<union> LS M q2'

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tl io \<in> LS M q1' \<union> LS M q2'

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
have "tl io \<notin> LS M q1' \<inter> LS M q2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl io \<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>]
            observable_language_transition_target[OF \<open>observable M\<close> \<open>(q2,x,y,q2') \<in> transitions M\<close>]
            \<open>io \<in> LS M q1 \<union> LS M q2\<close>
[PROOF STATE]
proof (prove)
using this:
(t_input (q1, x, y, q1'), t_output (q1, x, y, q1')) # ?io \<in> LS M (t_source (q1, x, y, q1')) \<Longrightarrow> ?io \<in> LS M (t_target (q1, x, y, q1'))
(t_input (q2, x, y, q2'), t_output (q2, x, y, q2')) # ?io \<in> LS M (t_source (q2, x, y, q2')) \<Longrightarrow> ?io \<in> LS M (t_target (q2, x, y, q2'))
io \<in> LS M q1 \<union> LS M q2

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

goal (1 subgoal):
 1. tl io \<notin> LS M q1' \<inter> LS M q2'
[PROOF STEP]
by (metis Int_iff LS_prepend_transition \<open>(q1, x, y, q1') \<in> FSM.transitions M\<close> \<open>(q2, x, y, q2') \<in> FSM.transitions M\<close> \<open>hd io = (x, y)\<close> \<open>io \<noteq> []\<close> \<open>io \<notin> LS M q1 \<inter> LS M q2\<close> fst_conv list.collapse snd_conv)
[PROOF STATE]
proof (state)
this:
tl io \<notin> LS M q1' \<inter> LS M q2'

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tl io \<notin> LS M q1' \<inter> LS M q2'

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
have "length (tl io) \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (tl io) \<le> k
[PROOF STEP]
using \<open>length io \<le> Suc k\<close>
[PROOF STATE]
proof (prove)
using this:
length io \<le> Suc k

goal (1 subgoal):
 1. length (tl io) \<le> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (tl io) \<le> k

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
tl io \<in> LS M q1' \<union> LS M q2'
tl io \<notin> LS M q1' \<inter> LS M q2'
length (tl io) \<le> 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)
using this:
tl io \<in> LS M q1' \<union> LS M q2'
tl io \<notin> LS M q1' \<inter> LS M q2'
length (tl io) \<le> k

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]
unfolding ofsm_table_set_observable[OF assms(1) \<open>q1' \<in> states M\<close> minimise_initial_partition]  ofsm_table_set_observable[OF assms(1) \<open>q2' \<in> states M\<close> minimise_initial_partition]
[PROOF STATE]
proof (prove)
using this:
tl io \<in> LS M q1' \<union> LS M q2'
tl io \<notin> LS M q1' \<inter> LS M q2'
length (tl io) \<le> k

goal (1 subgoal):
 1. {q' \<in> FSM.states M. \<forall>io. length io \<le> k \<longrightarrow> (io \<in> LS M q1') = (io \<in> LS M q') \<and> (io \<in> LS M q1' \<longrightarrow> after M q' io \<in> FSM.states M)} \<noteq> {q' \<in> FSM.states M. \<forall>io. length io \<le> k \<longrightarrow> (io \<in> LS M q2') = (io \<in> LS M q') \<and> (io \<in> LS M q2' \<longrightarrow> after M q' io \<in> FSM.states M)}
[PROOF STEP]
using \<open>q1' \<in> states M\<close> \<open>q2' \<in> states M\<close> after_is_state[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
tl io \<in> LS M q1' \<union> LS M q2'
tl io \<notin> LS M q1' \<inter> LS M q2'
length (tl io) \<le> k
q1' \<in> FSM.states M
q2' \<in> FSM.states M
?io \<in> LS M ?q \<Longrightarrow> after M ?q ?io \<in> FSM.states M

goal (1 subgoal):
 1. {q' \<in> FSM.states M. \<forall>io. length io \<le> k \<longrightarrow> (io \<in> LS M q1') = (io \<in> LS M q') \<and> (io \<in> LS M q1' \<longrightarrow> after M q' io \<in> FSM.states M)} \<noteq> {q' \<in> FSM.states M. \<forall>io. length io \<le> k \<longrightarrow> (io \<in> LS M q2') = (io \<in> LS M q') \<and> (io \<in> LS M q2' \<longrightarrow> after M q' io \<in> FSM.states M)}
[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 (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[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 (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
have "h_obs M q1 x y = Some q1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.h_obs M q1 x y = Some q1'
[PROOF STEP]
using \<open>(q1,x,y,q1') \<in> transitions M\<close> \<open>observable M\<close>
[PROOF STATE]
proof (prove)
using this:
(q1, x, y, q1') \<in> FSM.transitions M
observable M

goal (1 subgoal):
 1. FSM.h_obs M q1 x y = Some q1'
[PROOF STEP]
unfolding h_obs_Some[OF \<open>observable M\<close>] observable_alt_def
[PROOF STATE]
proof (prove)
using this:
(q1, x, y, q1') \<in> FSM.transitions M
\<forall>q1 x y q1' q1''. (q1, x, y, q1') \<in> FSM.transitions M \<and> (q1, x, y, q1'') \<in> FSM.transitions M \<longrightarrow> q1' = q1''

goal (1 subgoal):
 1. {q'. (q1, x, y, q') \<in> FSM.transitions M} = {q1'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
have "h_obs M q2 x y = Some q2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.h_obs M q2 x y = Some q2'
[PROOF STEP]
using \<open>(q2,x,y,q2') \<in> transitions M\<close> \<open>observable M\<close>
[PROOF STATE]
proof (prove)
using this:
(q2, x, y, q2') \<in> FSM.transitions M
observable M

goal (1 subgoal):
 1. FSM.h_obs M q2 x y = Some q2'
[PROOF STEP]
unfolding h_obs_Some[OF \<open>observable M\<close>] observable_alt_def
[PROOF STATE]
proof (prove)
using this:
(q2, x, y, q2') \<in> FSM.transitions M
\<forall>q1 x y q1' q1''. (q1, x, y, q1') \<in> FSM.transitions M \<and> (q1, x, y, q1'') \<in> FSM.transitions M \<longrightarrow> q1' = q1''

goal (1 subgoal):
 1. {q'. (q2, x, y, q') \<in> FSM.transitions M} = {q2'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
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 = Some q1'
FSM.h_obs M q2 x y = Some q2'
[PROOF STEP]
have "f (x,y) = Some ((x,y),(Some q1', Some q2'))"
[PROOF STATE]
proof (prove)
using this:
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 = Some q1'
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. f (x, y) = Some ((x, y), Some q1', Some q2')
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
using this:
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 = Some q1'
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. (case (x, y) of (x, y) \<Rightarrow> case (FSM.h_obs M q1 x y, FSM.h_obs M q2 x y) of (None, None) \<Rightarrow> None | (None, Some q2') \<Rightarrow> Some ((x, y), None, Some q2') | (Some q1', None) \<Rightarrow> Some ((x, y), Some q1', None) | (Some q1', Some q2') \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) k q1' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) k q2' then Some ((x, y), Some q1', Some q2') else None) = Some ((x, y), Some q1', Some q2')
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f (x, y) = Some ((x, y), Some q1', Some q2')

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f (x, y) = Some ((x, y), Some q1', Some q2')

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
have "(x,y) \<in> set (List.product(inputs_as_list M) (outputs_as_list M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
using fsm_transition_output[OF \<open>(q1,x,y,q1') \<in> transitions M\<close>] outputs_as_list_set[of M]
[PROOF STATE]
proof (prove)
using this:
t_output (q1, x, y, q1') \<in> FSM.outputs M
set (outputs_as_list M) = FSM.outputs M

goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
using fsm_transition_input[OF \<open>(q1,x,y,q1') \<in> transitions M\<close>] inputs_as_list_set[of M]
[PROOF STATE]
proof (prove)
using this:
t_output (q1, x, y, q1') \<in> FSM.outputs M
set (outputs_as_list M) = FSM.outputs M
t_input (q1, x, y, q1') \<in> FSM.inputs M
set (inputs_as_list M) = FSM.inputs M

goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
using image_iff
[PROOF STATE]
proof (prove)
using this:
t_output (q1, x, y, q1') \<in> FSM.outputs M
set (outputs_as_list M) = FSM.outputs M
t_input (q1, x, y, q1') \<in> FSM.inputs M
set (inputs_as_list M) = FSM.inputs M
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)

goal (1 subgoal):
 1. (x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (x, y) = Some ((x, y), Some q1', Some q2')
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
have "(List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M))) \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
f (x, y) = Some ((x, y), Some q1', Some q2')
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))

goal (1 subgoal):
 1. List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []
[PROOF STEP]
unfolding List.map_filter_def
[PROOF STATE]
proof (prove)
using this:
f (x, y) = Some ((x, y), Some q1', Some q2')
(x, y) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))

goal (1 subgoal):
 1. map (the \<circ> f) (filter (\<lambda>x. f x \<noteq> None) (List.product (inputs_as_list M) (outputs_as_list M))) \<noteq> []
[PROOF STEP]
by (metis (mono_tags, lifting) Nil_is_map_conv filter_empty_conv option.discI)
[PROOF STATE]
proof (state)
this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []
[PROOF STEP]
have **: "?res \<in> set (List.map_filter f (List.product(inputs_as_list M) (outputs_as_list M)))"
[PROOF STATE]
proof (prove)
using this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []

goal (1 subgoal):
 1. hd (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M))) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
using hd_in_set
[PROOF STATE]
proof (prove)
using this:
List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)) \<noteq> []
?xs \<noteq> [] \<Longrightarrow> hd ?xs \<in> set ?xs

goal (1 subgoal):
 1. hd (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M))) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) \<in> set (List.map_filter f (List.product (inputs_as_list M) (outputs_as_list M)))

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
obtain xR yR where "(xR,yR) \<in> set (List.product(inputs_as_list M) (outputs_as_list M))"
                   and res: "f (xR,yR) = Some ?res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xR yR. \<lbrakk>(xR, yR) \<in> set (List.product (inputs_as_list M) (outputs_as_list M)); f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using map_filter_elem[OF **]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. \<lbrakk>x \<in> set (List.product (inputs_as_list M) (outputs_as_list M)); f x = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>xR yR. \<lbrakk>(xR, yR) \<in> set (List.product (inputs_as_list M) (outputs_as_list M)); f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.exhaust_sel)
[PROOF STATE]
proof (state)
this:
(xR, yR) \<in> set (List.product (inputs_as_list M) (outputs_as_list M))
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
have p1: "?res = ((xR,yR),(h_obs M q1 xR yR, h_obs M q2 xR yR))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
[PROOF STEP]
using res f1
[PROOF STATE]
proof (prove)
using this:
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))
f (?x, ?y) \<noteq> None \<Longrightarrow> f (?x, ?y) = Some ((?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) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
[PROOF STEP]
by (metis option.distinct(1) option.sel)
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
[PROOF STEP]
have p2: "\<And> q1' q2' . h_obs M q1 xR yR = Some q1' \<Longrightarrow> h_obs M q2 xR yR = Some q2' \<Longrightarrow> ofsm_table M (\<lambda>q . states M) k q1' \<noteq> ofsm_table M (\<lambda>q . states M) k q2'"
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)

goal (1 subgoal):
 1. \<And>q1' q2'. \<lbrakk>FSM.h_obs M q1 xR yR = Some q1'; FSM.h_obs M q2 xR yR = 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'
[PROOF STEP]
using res f1 f2
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))
f (?x, ?y) \<noteq> None \<Longrightarrow> f (?x, ?y) = Some ((?x, ?y), FSM.h_obs M q1 ?x ?y, FSM.h_obs M q2 ?x ?y)
f (?x, ?y) = Some ((?x, ?y), Some ?q1', Some ?q2') \<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. \<And>q1' q2'. \<lbrakk>FSM.h_obs M q1 xR yR = Some q1'; FSM.h_obs M q2 xR yR = 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'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>FSM.h_obs M q1 xR yR = Some ?q1'; FSM.h_obs M q2 xR yR = 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. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
have p3: "h_obs M q1 xR yR \<noteq> None \<or> h_obs M q2 xR yR \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.h_obs M q1 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None
[PROOF STEP]
using res f3
[PROOF STATE]
proof (prove)
using this:
f (xR, yR) = Some (select_diverging_ofsm_table_io M q1 q2 (Suc k))
f (?x, ?y) \<noteq> None \<Longrightarrow> FSM.h_obs M q1 ?x ?y \<noteq> None \<or> FSM.h_obs M q2 ?x ?y \<noteq> None

goal (1 subgoal):
 1. FSM.h_obs M q1 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None

goal (1 subgoal):
 1. \<forall>x y. x \<in> FSM.inputs M \<longrightarrow> y \<in> FSM.outputs M \<longrightarrow> (FSM.h_obs M q1 x y = None) = (FSM.h_obs M q2 x y = None) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that p1 p2 p3
[PROOF STATE]
proof (prove)
using this:
\<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
select_diverging_ofsm_table_io M q1 q2 (Suc k) = ((xR, yR), FSM.h_obs M q1 xR yR, FSM.h_obs M q2 xR yR)
\<lbrakk>FSM.h_obs M q1 xR yR = Some ?q1'; FSM.h_obs M q2 xR yR = 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 xR yR \<noteq> None \<or> FSM.h_obs M q2 xR yR \<noteq> None

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed