[STATEMENT]
lemma select_diverging_ofsm_table_io_sym :
  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"
  assumes "(select_diverging_ofsm_table_io M q1 q2 (Suc k)) = (io,(a,b))"
  shows "(select_diverging_ofsm_table_io M q2 q1 (Suc k)) = (io,(b,a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
define xs where xs: "xs = (List.product (inputs_as_list M) (outputs_as_list M))"
[PROOF STATE]
proof (state)
this:
xs = List.product (inputs_as_list M) (outputs_as_list M)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
define f1' where f1': "f1' = (\<lambda>(x, y) \<Rightarrow> (case (h_obs M q1 x y, 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 . states M)  ((Suc k) - 1) q1' \<noteq> ofsm_table M (\<lambda>q . states M)  ((Suc k) - 1) q2' then Some ((x, y), Some q1', Some q2') else None)))"
[PROOF STATE]
proof (state)
this:
f1' = (\<lambda>xa. case xa 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) (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)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
define f1 where f1: "f1 = (\<lambda>xs . (hd (List.map_filter f1' xs)))"
[PROOF STATE]
proof (state)
this:
f1 = (\<lambda>xs. hd (List.map_filter f1' xs))

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
define f2' where f2': "f2' = (\<lambda>(x, y) \<Rightarrow> (case (h_obs M q2 x y, h_obs M q1 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 . states M)  ((Suc k) - 1) q1' \<noteq> ofsm_table M (\<lambda>q . states M)  ((Suc k) - 1) q2' then Some ((x, y), Some q1', Some q2') else None)))"
[PROOF STATE]
proof (state)
this:
f2' = (\<lambda>xa. case xa of (x, y) \<Rightarrow> case (FSM.h_obs M q2 x y, FSM.h_obs M q1 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)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
define f2 where f2: "f2 = (\<lambda>xs . (hd (List.map_filter f2' xs)))"
[PROOF STATE]
proof (state)
this:
f2 = (\<lambda>xs. hd (List.map_filter f2' xs))

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[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))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. 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) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using select_diverging_ofsm_table_io_Some(1)[OF assms(1-4)]
[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. 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) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by meson
[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)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
have "\<And> xy io a b . f1' xy = Some (io,(a,b)) \<Longrightarrow> f2' xy = Some (io,(b,a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xy io a b. f1' xy = Some (io, a, b) \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xy io a b. f1' xy = Some (io, a, b) \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
fix xy io a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xy io a b. f1' xy = Some (io, a, b) \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
assume *: "f1' xy = Some (io,(a,b))"
[PROOF STATE]
proof (state)
this:
f1' xy = Some (io, a, b)

goal (1 subgoal):
 1. \<And>xy io a b. f1' xy = Some (io, a, b) \<Longrightarrow> f2' xy = Some (io, b, a)
[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. \<And>xy io a b. f1' xy = Some (io, a, b) \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
show "f2' xy = Some (io,(b,a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
proof (cases "h_obs M q1 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> f2' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> f2' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
proof (cases "h_obs M q2 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> f2' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> f2' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None

goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
using \<open>h_obs M q1 x y = None\<close> *
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = None
f1' xy = Some (io, a, b)

goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
unfolding f1' f2' \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = None
(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) (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) = Some (io, a, b)

goal (1 subgoal):
 1. (case (x, y) of (x, y) \<Rightarrow> case (FSM.h_obs M q2 x y, FSM.h_obs M q1 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) = Some (io, b, a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f2' xy = Some (io, b, a)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
case (Some q2')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
f1' xy = Some (io, a, b)

goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
unfolding f1' f2'
[PROOF STATE]
proof (prove)
using this:
(case xy 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) (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) = Some (io, a, b)

goal (1 subgoal):
 1. (case xy of (x, y) \<Rightarrow> case (FSM.h_obs M q2 x y, FSM.h_obs M q1 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) = Some (io, b, a)
[PROOF STEP]
unfolding case_prod_conv None Some \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
(case None of None \<Rightarrow> case Some q2' of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1' \<Rightarrow> case Some q2' of None \<Rightarrow> Some ((x, y), Some q1', None) | 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) = Some (io, a, b)

goal (1 subgoal):
 1. (case Some q2' of None \<Rightarrow> case None of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1' \<Rightarrow> case None of None \<Rightarrow> Some ((x, y), Some q1', None) | 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) = Some (io, b, a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f2' xy = Some (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f2' xy = Some (io, b, a)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
case (Some q1')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
proof (cases "h_obs M q2 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> f2' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> f2' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
f1' xy = Some (io, a, b)

goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
unfolding f1' f2'
[PROOF STATE]
proof (prove)
using this:
(case xy 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) (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) = Some (io, a, b)

goal (1 subgoal):
 1. (case xy of (x, y) \<Rightarrow> case (FSM.h_obs M q2 x y, FSM.h_obs M q1 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) = Some (io, b, a)
[PROOF STEP]
unfolding case_prod_conv None Some \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
(case Some q1' of None \<Rightarrow> case None of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1' \<Rightarrow> case None of None \<Rightarrow> Some ((x, y), Some q1', None) | 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) = Some (io, a, b)

goal (1 subgoal):
 1. (case None of None \<Rightarrow> case Some q1' of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1'a \<Rightarrow> case Some q1' of None \<Rightarrow> Some ((x, y), Some q1'a, None) | Some q2' \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1'a \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' then Some ((x, y), Some q1'a, Some q2') else None) = Some (io, b, a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f2' xy = Some (io, b, a)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
case (Some q2')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
have "ofsm_table M (\<lambda>q . states M)  ((Suc k) - 1) q2' \<noteq> ofsm_table M (\<lambda>q . states M)  ((Suc k) - 1) q1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1'
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
f1' xy = Some (io, a, b)

goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1'
[PROOF STEP]
unfolding f1' case_prod_conv \<open>h_obs M q1 x y = Some q1'\<close> Some \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
(case Some q1' of None \<Rightarrow> case Some q2' of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1' \<Rightarrow> case Some q2' of None \<Rightarrow> Some ((x, y), Some q1', None) | 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) = Some (io, a, b)

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

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

goal (1 subgoal):
 1. f1' (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)
[PROOF STEP]
unfolding f1' case_prod_conv \<open>h_obs M q1 x y = Some q1'\<close> Some
[PROOF STATE]
proof (prove)
using this:
ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1'

goal (1 subgoal):
 1. (case Some q1' of None \<Rightarrow> case Some q2' of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1' \<Rightarrow> case Some q2' of None \<Rightarrow> Some ((x, y), Some q1', None) | 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) = Some ((x, y), Some q1', Some q2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1' (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f1' (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)
[PROOF STEP]
have "io = (x,y)" and "b = h_obs M q2 x y" and "a = h_obs M q1 x y"
[PROOF STATE]
proof (prove)
using this:
f1' (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)

goal (1 subgoal):
 1. io = (x, y) &&& b = FSM.h_obs M q2 x y &&& a = FSM.h_obs M q1 x y
[PROOF STEP]
using * \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
f1' (x, y) = Some ((x, y), FSM.h_obs M q1 x y, FSM.h_obs M q2 x y)
f1' xy = Some (io, a, b)
xy = (x, y)

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

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f2' xy = Some (io, b, a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
unfolding f2'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case xy of (x, y) \<Rightarrow> case (FSM.h_obs M q2 x y, FSM.h_obs M q1 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) = Some (io, b, a)
[PROOF STEP]
unfolding case_prod_conv \<open>h_obs M q1 x y = Some q1'\<close> Some \<open>io = (x,y)\<close> \<open>b = h_obs M q2 x y\<close> \<open>a = h_obs M q1 x y\<close> \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case Some q2' of None \<Rightarrow> case Some q1' of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1'a \<Rightarrow> case Some q1' of None \<Rightarrow> Some ((x, y), Some q1'a, None) | Some q2' \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1'a \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' then Some ((x, y), Some q1'a, Some q2') else None) = Some ((x, y), Some q2', Some q1')
[PROOF STEP]
using \<open>ofsm_table M (\<lambda>q . states M)  ((Suc k) - 1) q2' \<noteq> ofsm_table M (\<lambda>q . states M)  ((Suc k) - 1) q1'\<close>
[PROOF STATE]
proof (prove)
using this:
ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1'

goal (1 subgoal):
 1. (case Some q2' of None \<Rightarrow> case Some q1' of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1'a \<Rightarrow> case Some q1' of None \<Rightarrow> Some ((x, y), Some q1'a, None) | Some q2' \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1'a \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' then Some ((x, y), Some q1'a, Some q2') else None) = Some ((x, y), Some q2', Some q1')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f2' xy = Some (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f2' xy = Some (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f2' xy = Some (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f1' ?xy = Some (?io, ?a, ?b) \<Longrightarrow> f2' ?xy = Some (?io, ?b, ?a)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f1' ?xy = Some (?io, ?a, ?b) \<Longrightarrow> f2' ?xy = Some (?io, ?b, ?a)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
have "\<And> xy io a b . f2' xy = Some (io,(a,b)) \<Longrightarrow> f1' xy = Some (io,(b,a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xy io a b. f2' xy = Some (io, a, b) \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xy io a b. f2' xy = Some (io, a, b) \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
fix xy io a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xy io a b. f2' xy = Some (io, a, b) \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
assume *: "f2' xy = Some (io,(a,b))"
[PROOF STATE]
proof (state)
this:
f2' xy = Some (io, a, b)

goal (1 subgoal):
 1. \<And>xy io a b. f2' xy = Some (io, a, b) \<Longrightarrow> f1' xy = Some (io, b, a)
[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. \<And>xy io a b. f2' xy = Some (io, a, b) \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
show "f1' xy = Some (io,(b,a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1' xy = Some (io, b, a)
[PROOF STEP]
proof (cases "h_obs M q1 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> f1' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q1 x y = None \<Longrightarrow> f1' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1' xy = Some (io, b, a)
[PROOF STEP]
proof (cases "h_obs M q2 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> f1' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> f1' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h_obs M q2 x y = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None

goal (1 subgoal):
 1. f1' xy = Some (io, b, a)
[PROOF STEP]
using \<open>h_obs M q1 x y = None\<close> *
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = None
f2' xy = Some (io, a, b)

goal (1 subgoal):
 1. f1' xy = Some (io, b, a)
[PROOF STEP]
unfolding f1' f2' \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q2 x y = None
FSM.h_obs M q1 x y = None
(case (x, y) of (x, y) \<Rightarrow> case (FSM.h_obs M q2 x y, FSM.h_obs M q1 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) = Some (io, a, b)

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) (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) = Some (io, b, a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1' xy = Some (io, b, a)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
case (Some q2')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1' xy = Some (io, b, a)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
f2' xy = Some (io, a, b)

goal (1 subgoal):
 1. f1' xy = Some (io, b, a)
[PROOF STEP]
unfolding f1' f2'
[PROOF STATE]
proof (prove)
using this:
(case xy of (x, y) \<Rightarrow> case (FSM.h_obs M q2 x y, FSM.h_obs M q1 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) = Some (io, a, b)

goal (1 subgoal):
 1. (case xy 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) (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) = Some (io, b, a)
[PROOF STEP]
unfolding case_prod_conv None Some \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
(case Some q2' of None \<Rightarrow> case None of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1' \<Rightarrow> case None of None \<Rightarrow> Some ((x, y), Some q1', None) | 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) = Some (io, a, b)

goal (1 subgoal):
 1. (case None of None \<Rightarrow> case Some q2' of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1' \<Rightarrow> case Some q2' of None \<Rightarrow> Some ((x, y), Some q1', None) | 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) = Some (io, b, a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1' xy = Some (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f1' xy = Some (io, b, a)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
case (Some q1')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q1 x y = Some q1'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q1 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1' xy = Some (io, b, a)
[PROOF STEP]
proof (cases "h_obs M q2 x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> f1' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = None

goal (2 subgoals):
 1. FSM.h_obs M q2 x y = None \<Longrightarrow> f1' xy = Some (io, b, a)
 2. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1' xy = Some (io, b, a)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
f2' xy = Some (io, a, b)

goal (1 subgoal):
 1. f1' xy = Some (io, b, a)
[PROOF STEP]
unfolding f1' f2'
[PROOF STATE]
proof (prove)
using this:
(case xy of (x, y) \<Rightarrow> case (FSM.h_obs M q2 x y, FSM.h_obs M q1 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) = Some (io, a, b)

goal (1 subgoal):
 1. (case xy 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) (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) = Some (io, b, a)
[PROOF STEP]
unfolding case_prod_conv None Some \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
(case None of None \<Rightarrow> case Some q1' of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1'a \<Rightarrow> case Some q1' of None \<Rightarrow> Some ((x, y), Some q1'a, None) | Some q2' \<Rightarrow> if ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1'a \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' then Some ((x, y), Some q1'a, Some q2') else None) = Some (io, a, b)

goal (1 subgoal):
 1. (case Some q1' of None \<Rightarrow> case None of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1' \<Rightarrow> case None of None \<Rightarrow> Some ((x, y), Some q1', None) | 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) = Some (io, b, a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1' xy = Some (io, b, a)

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
case (Some q2')
[PROOF STATE]
proof (state)
this:
FSM.h_obs M q2 x y = Some q2'

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
have "ofsm_table M (\<lambda>q . states M)  ((Suc k) - 1) q2' \<noteq> ofsm_table M (\<lambda>q . states M)  ((Suc k) - 1) q1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1'
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
f2' xy = Some (io, a, b)

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

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

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

goal (1 subgoal):
 1. f2' (x, y) = Some ((x, y), FSM.h_obs M q2 x y, FSM.h_obs M q1 x y)
[PROOF STEP]
unfolding f2' case_prod_conv \<open>h_obs M q1 x y = Some q1'\<close> Some
[PROOF STATE]
proof (prove)
using this:
ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1'

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

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f2' (x, y) = Some ((x, y), FSM.h_obs M q2 x y, FSM.h_obs M q1 x y)
[PROOF STEP]
have "io = (x,y)" and "b = h_obs M q1 x y" and "a = h_obs M q2 x y"
[PROOF STATE]
proof (prove)
using this:
f2' (x, y) = Some ((x, y), FSM.h_obs M q2 x y, FSM.h_obs M q1 x y)

goal (1 subgoal):
 1. io = (x, y) &&& b = FSM.h_obs M q1 x y &&& a = FSM.h_obs M q2 x y
[PROOF STEP]
using * \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
f2' (x, y) = Some ((x, y), FSM.h_obs M q2 x y, FSM.h_obs M q1 x y)
f2' xy = Some (io, a, b)
xy = (x, y)

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

goal (1 subgoal):
 1. \<And>a. FSM.h_obs M q2 x y = Some a \<Longrightarrow> f1' xy = Some (io, b, a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1' xy = Some (io, b, a)
[PROOF STEP]
unfolding f1'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case xy 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) (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) = Some (io, b, a)
[PROOF STEP]
unfolding case_prod_conv \<open>h_obs M q1 x y = Some q1'\<close> Some \<open>io = (x,y)\<close> \<open>b = h_obs M q1 x y\<close> \<open>a = h_obs M q2 x y\<close> \<open>xy = (x,y)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case Some q1' of None \<Rightarrow> case Some q2' of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1' \<Rightarrow> case Some q2' of None \<Rightarrow> Some ((x, y), Some q1', None) | 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) = Some ((x, y), Some q1', Some q2')
[PROOF STEP]
using \<open>ofsm_table M (\<lambda>q . states M)  ((Suc k) - 1) q2' \<noteq> ofsm_table M (\<lambda>q . states M)  ((Suc k) - 1) q1'\<close>
[PROOF STATE]
proof (prove)
using this:
ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q2' \<noteq> ofsm_table M (\<lambda>q. FSM.states M) (Suc k - 1) q1'

goal (1 subgoal):
 1. (case Some q1' of None \<Rightarrow> case Some q2' of None \<Rightarrow> None | Some q2' \<Rightarrow> Some ((x, y), None, Some q2') | Some q1' \<Rightarrow> case Some q2' of None \<Rightarrow> Some ((x, y), Some q1', None) | 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) = Some ((x, y), Some q1', Some q2')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f1' xy = Some (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f1' xy = Some (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f1' xy = Some (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f2' ?xy = Some (?io, ?a, ?b) \<Longrightarrow> f1' ?xy = Some (?io, ?b, ?a)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f1' ?xy = Some (?io, ?a, ?b) \<Longrightarrow> f2' ?xy = Some (?io, ?b, ?a)
f2' ?xy = Some (?io, ?a, ?b) \<Longrightarrow> f1' ?xy = Some (?io, ?b, ?a)
[PROOF STEP]
have "\<And> xy io a b . f2' xy = Some (io,(a,b)) \<longleftrightarrow> f1' xy = Some (io,(b,a))"
[PROOF STATE]
proof (prove)
using this:
f1' ?xy = Some (?io, ?a, ?b) \<Longrightarrow> f2' ?xy = Some (?io, ?b, ?a)
f2' ?xy = Some (?io, ?a, ?b) \<Longrightarrow> f1' ?xy = Some (?io, ?b, ?a)

goal (1 subgoal):
 1. \<And>xy io a b. (f2' xy = Some (io, a, b)) = (f1' xy = Some (io, b, a))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(f2' ?xy = Some (?io, ?a, ?b)) = (f1' ?xy = Some (?io, ?b, ?a))

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(f2' ?xy = Some (?io, ?a, ?b)) = (f1' ?xy = Some (?io, ?b, ?a))

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
have "\<And> xs . (\<And> xy io a b . f1' xy = Some (io,(a,b)) \<longleftrightarrow> f2' xy = Some (io,(b,a))) \<Longrightarrow> \<exists> xy \<in> list.set xs . f1' xy \<noteq> None \<Longrightarrow> f1 xs = (io,(a,b)) \<Longrightarrow> f2 xs = (io,(b,a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set xs. f1' xy \<noteq> None; f1 xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 xs = (io, b, a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set xs. f1' xy \<noteq> None; f1 xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 xs = (io, b, a)
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set xs. f1' xy \<noteq> None; f1 xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 xs = (io, b, a)
[PROOF STEP]
assume "(\<And> xy io a b . f1' xy = Some (io,(a,b)) \<longleftrightarrow> f2' xy = Some (io,(b,a)))"
                  "\<exists> xy \<in> list.set xs . f1' xy \<noteq> None"
                  "f1 xs = (io,(a,b))"
[PROOF STATE]
proof (state)
this:
(f1' ?xy = Some (?io, ?a, ?b)) = (f2' ?xy = Some (?io, ?b, ?a))
\<exists>xy\<in>list.set xs. f1' xy \<noteq> None
f1 xs = (io, a, b)

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set xs. f1' xy \<noteq> None; f1 xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 xs = (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(f1' ?xy = Some (?io, ?a, ?b)) = (f2' ?xy = Some (?io, ?b, ?a))
\<exists>xy\<in>list.set xs. f1' xy \<noteq> None
f1 xs = (io, a, b)
[PROOF STEP]
show "f2 xs = (io,(b,a))"
[PROOF STATE]
proof (prove)
using this:
(f1' ?xy = Some (?io, ?a, ?b)) = (f2' ?xy = Some (?io, ?b, ?a))
\<exists>xy\<in>list.set xs. f1' xy \<noteq> None
f1 xs = (io, a, b)

goal (1 subgoal):
 1. f2 xs = (io, b, a)
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set []. f1' xy \<noteq> None; f1 [] = (io, a, b)\<rbrakk> \<Longrightarrow> f2 [] = (io, b, a)
 2. \<And>aa xs. \<lbrakk>\<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set xs. f1' xy \<noteq> None; f1 xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 xs = (io, b, a); \<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set (aa # xs). f1' xy \<noteq> None; f1 (aa # xs) = (io, a, b)\<rbrakk> \<Longrightarrow> f2 (aa # xs) = (io, b, a)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
(f1' ?xy = Some (?io, ?a, ?b)) = (f2' ?xy = Some (?io, ?b, ?a))
\<exists>xy\<in>list.set []. f1' xy \<noteq> None
f1 [] = (io, a, b)

goal (2 subgoals):
 1. \<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set []. f1' xy \<noteq> None; f1 [] = (io, a, b)\<rbrakk> \<Longrightarrow> f2 [] = (io, b, a)
 2. \<And>aa xs. \<lbrakk>\<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set xs. f1' xy \<noteq> None; f1 xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 xs = (io, b, a); \<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set (aa # xs). f1' xy \<noteq> None; f1 (aa # xs) = (io, a, b)\<rbrakk> \<Longrightarrow> f2 (aa # xs) = (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(f1' ?xy = Some (?io, ?a, ?b)) = (f2' ?xy = Some (?io, ?b, ?a))
\<exists>xy\<in>list.set []. f1' xy \<noteq> None
f1 [] = (io, a, b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(f1' ?xy = Some (?io, ?a, ?b)) = (f2' ?xy = Some (?io, ?b, ?a))
\<exists>xy\<in>list.set []. f1' xy \<noteq> None
f1 [] = (io, a, b)

goal (1 subgoal):
 1. f2 [] = (io, b, a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f2 [] = (io, b, a)

goal (1 subgoal):
 1. \<And>aa xs. \<lbrakk>\<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set xs. f1' xy \<noteq> None; f1 xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 xs = (io, b, a); \<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set (aa # xs). f1' xy \<noteq> None; f1 (aa # xs) = (io, a, b)\<rbrakk> \<Longrightarrow> f2 (aa # xs) = (io, b, a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa xs. \<lbrakk>\<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set xs. f1' xy \<noteq> None; f1 xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 xs = (io, b, a); \<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set (aa # xs). f1' xy \<noteq> None; f1 (aa # xs) = (io, a, b)\<rbrakk> \<Longrightarrow> f2 (aa # xs) = (io, b, a)
[PROOF STEP]
case (Cons xy xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set xs. f1' xy \<noteq> None; f1 xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 xs = (io, b, a)
(f1' ?xy = Some (?io, ?a, ?b)) = (f2' ?xy = Some (?io, ?b, ?a))
\<exists>xy\<in>list.set (xy # xs). f1' xy \<noteq> None
f1 (xy # xs) = (io, a, b)

goal (1 subgoal):
 1. \<And>aa xs. \<lbrakk>\<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set xs. f1' xy \<noteq> None; f1 xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 xs = (io, b, a); \<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set (aa # xs). f1' xy \<noteq> None; f1 (aa # xs) = (io, a, b)\<rbrakk> \<Longrightarrow> f2 (aa # xs) = (io, b, a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2 (xy # xs) = (io, b, a)
[PROOF STEP]
proof (cases "f1' xy")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f1' xy = None \<Longrightarrow> f2 (xy # xs) = (io, b, a)
 2. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
f1' xy = None

goal (2 subgoals):
 1. f1' xy = None \<Longrightarrow> f2 (xy # xs) = (io, b, a)
 2. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f1' xy = None
[PROOF STEP]
have "\<nexists> io a b . f1' xy = Some (io,(a,b))"
[PROOF STATE]
proof (prove)
using this:
f1' xy = None

goal (1 subgoal):
 1. \<nexists>io a b. f1' xy = Some (io, a, b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>io a b. f1' xy = Some (io, a, b)

goal (2 subgoals):
 1. f1' xy = None \<Longrightarrow> f2 (xy # xs) = (io, b, a)
 2. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>io a b. f1' xy = Some (io, a, b)
[PROOF STEP]
have "f2' xy = None"
[PROOF STATE]
proof (prove)
using this:
\<nexists>io a b. f1' xy = Some (io, a, b)

goal (1 subgoal):
 1. f2' xy = None
[PROOF STEP]
using Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
\<nexists>io a b. f1' xy = Some (io, a, b)
(f1' ?xy = Some (?io, ?a, ?b)) = (f2' ?xy = Some (?io, ?b, ?a))

goal (1 subgoal):
 1. f2' xy = None
[PROOF STEP]
by (metis option.exhaust prod_cases3)
[PROOF STATE]
proof (state)
this:
f2' xy = None

goal (2 subgoals):
 1. f1' xy = None \<Longrightarrow> f2 (xy # xs) = (io, b, a)
 2. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f2' xy = None
[PROOF STEP]
have "f2 (xy#xs) = f2 xs"
[PROOF STATE]
proof (prove)
using this:
f2' xy = None

goal (1 subgoal):
 1. f2 (xy # xs) = f2 xs
[PROOF STEP]
unfolding f2 map_filter_simps
[PROOF STATE]
proof (prove)
using this:
f2' xy = None

goal (1 subgoal):
 1. hd (case f2' xy of None \<Rightarrow> List.map_filter f2' xs | Some y \<Rightarrow> y # List.map_filter f2' xs) = hd (List.map_filter f2' xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f2 (xy # xs) = f2 xs

goal (2 subgoals):
 1. f1' xy = None \<Longrightarrow> f2 (xy # xs) = (io, b, a)
 2. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f2 (xy # xs) = f2 xs

goal (2 subgoals):
 1. f1' xy = None \<Longrightarrow> f2 (xy # xs) = (io, b, a)
 2. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
have "f1 (xy#xs) = f1 xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1 (xy # xs) = f1 xs
[PROOF STEP]
using None
[PROOF STATE]
proof (prove)
using this:
f1' xy = None

goal (1 subgoal):
 1. f1 (xy # xs) = f1 xs
[PROOF STEP]
unfolding f1 map_filter_simps
[PROOF STATE]
proof (prove)
using this:
f1' xy = None

goal (1 subgoal):
 1. hd (case f1' xy of None \<Rightarrow> List.map_filter f1' xs | Some y \<Rightarrow> y # List.map_filter f1' xs) = hd (List.map_filter f1' xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1 (xy # xs) = f1 xs

goal (2 subgoals):
 1. f1' xy = None \<Longrightarrow> f2 (xy # xs) = (io, b, a)
 2. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f2 (xy # xs) = f2 xs
f1 (xy # xs) = f1 xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f2 (xy # xs) = f2 xs
f1 (xy # xs) = f1 xs

goal (1 subgoal):
 1. f2 (xy # xs) = (io, b, a)
[PROOF STEP]
using Cons.IH Cons.prems(1) Cons.prems(2) Cons.prems(3) None
[PROOF STATE]
proof (prove)
using this:
f2 (xy # xs) = f2 xs
f1 (xy # xs) = f1 xs
\<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set xs. f1' xy \<noteq> None; f1 xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 xs = (io, b, a)
(f1' ?xy = Some (?io, ?a, ?b)) = (f2' ?xy = Some (?io, ?b, ?a))
\<exists>xy\<in>list.set (xy # xs). f1' xy \<noteq> None
f1 (xy # xs) = (io, a, b)
f1' xy = None

goal (1 subgoal):
 1. f2 (xy # xs) = (io, b, a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f2 (xy # xs) = (io, b, a)

goal (1 subgoal):
 1. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
case (Some ioab)
[PROOF STATE]
proof (state)
this:
f1' xy = Some ioab

goal (1 subgoal):
 1. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f1' xy = Some ioab
[PROOF STEP]
have "f1 (xy#xs) = ioab"
[PROOF STATE]
proof (prove)
using this:
f1' xy = Some ioab

goal (1 subgoal):
 1. f1 (xy # xs) = ioab
[PROOF STEP]
unfolding f1 map_filter_simps
[PROOF STATE]
proof (prove)
using this:
f1' xy = Some ioab

goal (1 subgoal):
 1. hd (case f1' xy of None \<Rightarrow> List.map_filter f1' xs | Some y \<Rightarrow> y # List.map_filter f1' xs) = ioab
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f1 (xy # xs) = ioab

goal (1 subgoal):
 1. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f1 (xy # xs) = ioab
[PROOF STEP]
have "ioab = (io,(a,b))"
[PROOF STATE]
proof (prove)
using this:
f1 (xy # xs) = ioab

goal (1 subgoal):
 1. ioab = (io, a, b)
[PROOF STEP]
using Cons.prems(3)
[PROOF STATE]
proof (prove)
using this:
f1 (xy # xs) = ioab
f1 (xy # xs) = (io, a, b)

goal (1 subgoal):
 1. ioab = (io, a, b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ioab = (io, a, b)

goal (1 subgoal):
 1. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioab = (io, a, b)
[PROOF STEP]
have "f2' xy = Some (io,(b,a))"
[PROOF STATE]
proof (prove)
using this:
ioab = (io, a, b)

goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
using Cons.prems(1) Some
[PROOF STATE]
proof (prove)
using this:
ioab = (io, a, b)
(f1' ?xy = Some (?io, ?a, ?b)) = (f2' ?xy = Some (?io, ?b, ?a))
f1' xy = Some ioab

goal (1 subgoal):
 1. f2' xy = Some (io, b, a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f2' xy = Some (io, b, a)

goal (1 subgoal):
 1. \<And>aa. f1' xy = Some aa \<Longrightarrow> f2 (xy # xs) = (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f2' xy = Some (io, b, a)
[PROOF STEP]
show "f2 (xy#xs) = (io,(b,a))"
[PROOF STATE]
proof (prove)
using this:
f2' xy = Some (io, b, a)

goal (1 subgoal):
 1. f2 (xy # xs) = (io, b, a)
[PROOF STEP]
unfolding f2 map_filter_simps
[PROOF STATE]
proof (prove)
using this:
f2' xy = Some (io, b, a)

goal (1 subgoal):
 1. hd (case f2' xy of None \<Rightarrow> List.map_filter f2' xs | Some y \<Rightarrow> y # List.map_filter f2' xs) = (io, b, a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f2 (xy # xs) = (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f2 (xy # xs) = (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f2 xs = (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set ?xs. f1' xy \<noteq> None; f1 ?xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 ?xs = (io, b, a)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set ?xs. f1' xy \<noteq> None; f1 ?xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 ?xs = (io, b, a)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
have "f1 xs = (io,(a,b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1 xs = (io, a, b)
[PROOF STEP]
using \<open>(select_diverging_ofsm_table_io M q1 q2 (Suc k)) = (io,(a,b))\<close>
[PROOF STATE]
proof (prove)
using this:
select_diverging_ofsm_table_io M q1 q2 (Suc k) = (io, a, b)

goal (1 subgoal):
 1. f1 xs = (io, a, b)
[PROOF STEP]
unfolding select_diverging_ofsm_table_io.simps f1 f1' xs Let_def
[PROOF STATE]
proof (prove)
using this:
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))) = (io, a, b)

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))) = (io, a, b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1 xs = (io, a, b)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f1 xs = (io, a, b)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
have "\<exists> xy \<in> list.set xs . f1' xy \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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. \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
 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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
 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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
 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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
 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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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. \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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 "f1' (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. f1' (x, y) = Some ((x, y), None, Some q2')
[PROOF STEP]
unfolding f1'
[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) (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) = Some ((x, y), None, Some q2')
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f1' (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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f1' (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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
have "(x,y) \<in> list.set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> list.set xs
[PROOF STEP]
unfolding xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> list.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
list.set (outputs_as_list M) = FSM.outputs M

goal (1 subgoal):
 1. (x, y) \<in> list.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
list.set (outputs_as_list M) = FSM.outputs M
x \<in> FSM.inputs M
list.set (inputs_as_list M) = FSM.inputs M

goal (1 subgoal):
 1. (x, y) \<in> list.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
list.set (outputs_as_list M) = FSM.outputs M
x \<in> FSM.inputs M
list.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> list.set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(x, y) \<in> list.set xs

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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
 2. FSM.h_obs M q2 x y = None \<and> (\<exists>q1'. FSM.h_obs M q1 x y = Some q1') \<Longrightarrow> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f1' (x, y) = Some ((x, y), None, Some q2')
(x, y) \<in> list.set xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f1' (x, y) = Some ((x, y), None, Some q2')
(x, y) \<in> list.set xs

goal (1 subgoal):
 1. \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xy\<in>list.set xs. f1' xy \<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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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 "f1' (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. f1' (x, y) = Some ((x, y), Some q1', None)
[PROOF STEP]
unfolding f1'
[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) (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) = Some ((x, y), Some q1', None)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f1' (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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f1' (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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
have "(x,y) \<in> list.set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> list.set xs
[PROOF STEP]
unfolding xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> list.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
list.set (outputs_as_list M) = FSM.outputs M

goal (1 subgoal):
 1. (x, y) \<in> list.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
list.set (outputs_as_list M) = FSM.outputs M
x \<in> FSM.inputs M
list.set (inputs_as_list M) = FSM.inputs M

goal (1 subgoal):
 1. (x, y) \<in> list.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
list.set (outputs_as_list M) = FSM.outputs M
x \<in> FSM.inputs M
list.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> list.set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(x, y) \<in> list.set xs

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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f1' (x, y) = Some ((x, y), Some q1', None)
(x, y) \<in> list.set xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f1' (x, y) = Some ((x, y), Some q1', None)
(x, y) \<in> list.set xs

goal (1 subgoal):
 1. \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xy\<in>list.set xs. f1' xy \<noteq> None

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xy\<in>list.set xs. f1' xy \<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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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_observable[OF assms(1,2) minimise_initial_partition] ofsm_table_set_observable[OF assms(1,3) minimise_initial_partition]
[PROOF STATE]
proof (prove)
using this:
{q' \<in> FSM.states M. \<forall>io. length io \<le> Suc k \<longrightarrow> (io \<in> LS M q1) = (io \<in> LS M q') \<and> (io \<in> LS M q1 \<longrightarrow> FSM.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) = (io \<in> LS M q') \<and> (io \<in> LS M q2 \<longrightarrow> FSM.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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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'
[PROOF STEP]
have "((tl io) \<in> LS M q1') \<noteq> (tl io \<in> LS M 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'

goal (1 subgoal):
 1. (tl io \<in> LS M q1') \<noteq> (tl io \<in> LS M q2')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(tl io \<in> LS M q1') \<noteq> (tl io \<in> 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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(tl io \<in> LS M q1') \<noteq> (tl io \<in> 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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(tl io \<in> LS M q1') \<noteq> (tl io \<in> LS M q2')
length (tl io) \<le> k
[PROOF STEP]
have "q2' \<notin> ofsm_table M (\<lambda>q . states M)  k q1'"
[PROOF STATE]
proof (prove)
using this:
(tl io \<in> LS M q1') \<noteq> (tl io \<in> LS M q2')
length (tl io) \<le> k

goal (1 subgoal):
 1. q2' \<notin> ofsm_table M (\<lambda>q. FSM.states M) k q1'
[PROOF STEP]
unfolding ofsm_table_set_observable[OF assms(1) \<open>q1' \<in> states M\<close> minimise_initial_partition]
[PROOF STATE]
proof (prove)
using this:
(tl io \<in> LS M q1') \<noteq> (tl io \<in> LS M q2')
length (tl io) \<le> k

goal (1 subgoal):
 1. q2' \<notin> {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> FSM.after M q' io \<in> FSM.states M)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q2' \<notin> ofsm_table M (\<lambda>q. FSM.states M) k 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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q2' \<notin> ofsm_table M (\<lambda>q. FSM.states M) k 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)
using this:
q2' \<notin> ofsm_table M (\<lambda>q. FSM.states M) k q1'

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 (metis \<open>q2' \<in> FSM.states M\<close> ofsm_table_containment)
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[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 "f1' (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. f1' (x, y) = Some ((x, y), Some q1', Some q2')
[PROOF STEP]
unfolding f1'
[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) (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) = Some ((x, y), Some q1', Some q2')
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f1' (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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f1' (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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
have "(x,y) \<in> list.set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> list.set xs
[PROOF STEP]
unfolding xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> list.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
list.set (outputs_as_list M) = FSM.outputs M

goal (1 subgoal):
 1. (x, y) \<in> list.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
list.set (outputs_as_list M) = FSM.outputs M
t_input (q1, x, y, q1') \<in> FSM.inputs M
list.set (inputs_as_list M) = FSM.inputs M

goal (1 subgoal):
 1. (x, y) \<in> list.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
list.set (outputs_as_list M) = FSM.outputs M
t_input (q1, x, y, q1') \<in> FSM.inputs M
list.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> list.set (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(x, y) \<in> list.set xs

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> \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f1' (x, y) = Some ((x, y), Some q1', Some q2')
(x, y) \<in> list.set xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f1' (x, y) = Some ((x, y), Some q1', Some q2')
(x, y) \<in> list.set xs

goal (1 subgoal):
 1. \<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xy\<in>list.set xs. f1' xy \<noteq> None

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xy\<in>list.set xs. f1' xy \<noteq> None

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xy\<in>list.set xs. f1' xy \<noteq> None

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(f2' ?xy = Some (?io, ?a, ?b)) = (f1' ?xy = Some (?io, ?b, ?a))
\<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set ?xs. f1' xy \<noteq> None; f1 ?xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 ?xs = (io, b, a)
f1 xs = (io, a, b)
\<exists>xy\<in>list.set xs. f1' xy \<noteq> None
[PROOF STEP]
have "f2 xs = (io,(b,a))"
[PROOF STATE]
proof (prove)
using this:
(f2' ?xy = Some (?io, ?a, ?b)) = (f1' ?xy = Some (?io, ?b, ?a))
\<lbrakk>\<And>xy io a b. (f1' xy = Some (io, a, b)) = (f2' xy = Some (io, b, a)); \<exists>xy\<in>list.set ?xs. f1' xy \<noteq> None; f1 ?xs = (io, a, b)\<rbrakk> \<Longrightarrow> f2 ?xs = (io, b, a)
f1 xs = (io, a, b)
\<exists>xy\<in>list.set xs. f1' xy \<noteq> None

goal (1 subgoal):
 1. f2 xs = (io, b, a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f2 xs = (io, b, a)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f2 xs = (io, b, a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f2 xs = (io, b, a)

goal (1 subgoal):
 1. select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)
[PROOF STEP]
unfolding select_diverging_ofsm_table_io.simps f2 f2' xs Let_def
[PROOF STATE]
proof (prove)
using this:
hd (List.map_filter (\<lambda>(x, y). case (FSM.h_obs M q2 x y, FSM.h_obs M q1 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))) = (io, b, a)

goal (1 subgoal):
 1. hd (List.map_filter (\<lambda>(x, y). case (FSM.h_obs M q2 x y, FSM.h_obs M q1 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))) = (io, b, a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
select_diverging_ofsm_table_io M q2 q1 (Suc k) = (io, b, a)

goal:
No subgoals!
[PROOF STEP]
qed