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

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set_reduced M). distinguishes M q1 q2 io
[PROOF STEP]
define handlePair where "handlePair = (\<lambda> W (q,q') . if contains_distinguishing_trace M W q q'
                                then W
                                else insert W (get_distinguishing_sequence_from_ofsm_tables M q q'))"
[PROOF STATE]
proof (state)
this:
handlePair = (\<lambda>W (q, q'). if contains_distinguishing_trace M W q q' then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q q'))

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set_reduced M). distinguishes M q1 q2 io
[PROOF STEP]
have "distinguishing_set_reduced M = foldl handlePair empty pairs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinguishing_set_reduced M = foldl handlePair Prefix_Tree.empty pairs
[PROOF STEP]
unfolding distinguishing_set_reduced.simps handlePair_def pairs Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>W (q, q'). if contains_distinguishing_trace M W q q' then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q q')) Prefix_Tree.empty (filter (\<lambda>(q, q'). q \<noteq> q') (list_ordered_pairs (states_as_list M))) = foldl (\<lambda>W (q, q'). if contains_distinguishing_trace M W q q' then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q q')) Prefix_Tree.empty (filter (\<lambda>(x, y). x \<noteq> y) (list_ordered_pairs (states_as_list M)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
distinguishing_set_reduced M = foldl handlePair Prefix_Tree.empty pairs

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set_reduced M). distinguishes M q1 q2 io
[PROOF STEP]
have handlePair_subset: "\<And> W q q' . set W \<subseteq> set (handlePair W (q,q'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>W q q'. Prefix_Tree.set W \<subseteq> Prefix_Tree.set (handlePair W (q, q'))
[PROOF STEP]
unfolding handlePair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>W q q'. Prefix_Tree.set W \<subseteq> Prefix_Tree.set (case (q, q') of (q, q') \<Rightarrow> if contains_distinguishing_trace M W q q' then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q q'))
[PROOF STEP]
using insert_set
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (Prefix_Tree.insert ?t ?xs) = Prefix_Tree.set ?t \<union> {xs'. \<exists>xs''. ?xs = xs' @ xs''}

goal (1 subgoal):
 1. \<And>W q q'. Prefix_Tree.set W \<subseteq> Prefix_Tree.set (case (q, q') of (q, q') \<Rightarrow> if contains_distinguishing_trace M W q q' then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q q'))
[PROOF STEP]
unfolding case_prod_conv
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (Prefix_Tree.insert ?t ?xs) = Prefix_Tree.set ?t \<union> {xs'. \<exists>xs''. ?xs = xs' @ xs''}

goal (1 subgoal):
 1. \<And>W q q'. Prefix_Tree.set W \<subseteq> Prefix_Tree.set (if contains_distinguishing_trace M W q q' then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q q'))
[PROOF STEP]
by (metis (mono_tags) Un_upper1 order_refl)
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set ?W \<subseteq> Prefix_Tree.set (handlePair ?W (?q, ?q'))

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

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set_reduced M). distinguishes M q1 q2 io
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(q1, q2) \<in> list.set pairs \<or> (q2, q1) \<in> list.set pairs

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set_reduced M). distinguishes M q1 q2 io
[PROOF STEP]
have "\<And> pairs' . list.set pairs' \<subseteq> list.set pairs \<Longrightarrow> (q1,q2) \<in> list.set pairs' \<or> (q2,q1) \<in> list.set pairs' \<Longrightarrow> (\<exists> io \<in> set (foldl handlePair empty pairs') .  distinguishes M q1 q2 io)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pairs'. \<lbrakk>list.set pairs' \<subseteq> list.set pairs; (q1, q2) \<in> list.set pairs' \<or> (q2, q1) \<in> list.set pairs'\<rbrakk> \<Longrightarrow> \<exists>io\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty pairs'). distinguishes M q1 q2 io
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pairs'. \<lbrakk>list.set pairs' \<subseteq> list.set pairs; (q1, q2) \<in> list.set pairs' \<or> (q2, q1) \<in> list.set pairs'\<rbrakk> \<Longrightarrow> \<exists>io\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty pairs'). distinguishes M q1 q2 io
[PROOF STEP]
fix pairs'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pairs'. \<lbrakk>list.set pairs' \<subseteq> list.set pairs; (q1, q2) \<in> list.set pairs' \<or> (q2, q1) \<in> list.set pairs'\<rbrakk> \<Longrightarrow> \<exists>io\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty pairs'). distinguishes M q1 q2 io
[PROOF STEP]
assume "list.set pairs' \<subseteq> list.set pairs" and "(q1,q2) \<in> list.set pairs' \<or> (q2,q1) \<in> list.set pairs'"
[PROOF STATE]
proof (state)
this:
list.set pairs' \<subseteq> list.set pairs
(q1, q2) \<in> list.set pairs' \<or> (q2, q1) \<in> list.set pairs'

goal (1 subgoal):
 1. \<And>pairs'. \<lbrakk>list.set pairs' \<subseteq> list.set pairs; (q1, q2) \<in> list.set pairs' \<or> (q2, q1) \<in> list.set pairs'\<rbrakk> \<Longrightarrow> \<exists>io\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty pairs'). distinguishes M q1 q2 io
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list.set pairs' \<subseteq> list.set pairs
(q1, q2) \<in> list.set pairs' \<or> (q2, q1) \<in> list.set pairs'
[PROOF STEP]
show "(\<exists> io \<in> set (foldl handlePair empty pairs') .  distinguishes M q1 q2 io)"
[PROOF STATE]
proof (prove)
using this:
list.set pairs' \<subseteq> list.set pairs
(q1, q2) \<in> list.set pairs' \<or> (q2, q1) \<in> list.set pairs'

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty pairs'). distinguishes M q1 q2 io
[PROOF STEP]
proof (induction pairs' rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list.set [] \<subseteq> list.set pairs; (q1, q2) \<in> list.set [] \<or> (q2, q1) \<in> list.set []\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty [])) (distinguishes M q1 q2)
 2. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> list.set pairs; (q1, q2) \<in> list.set xs \<or> (q2, q1) \<in> list.set xs\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty xs)) (distinguishes M q1 q2); list.set (xs @ [x]) \<subseteq> list.set pairs; (q1, q2) \<in> list.set (xs @ [x]) \<or> (q2, q1) \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (xs @ [x]))) (distinguishes M q1 q2)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
list.set [] \<subseteq> list.set pairs
(q1, q2) \<in> list.set [] \<or> (q2, q1) \<in> list.set []

goal (2 subgoals):
 1. \<lbrakk>list.set [] \<subseteq> list.set pairs; (q1, q2) \<in> list.set [] \<or> (q2, q1) \<in> list.set []\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty [])) (distinguishes M q1 q2)
 2. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> list.set pairs; (q1, q2) \<in> list.set xs \<or> (q2, q1) \<in> list.set xs\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty xs)) (distinguishes M q1 q2); list.set (xs @ [x]) \<subseteq> list.set pairs; (q1, q2) \<in> list.set (xs @ [x]) \<or> (q2, q1) \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (xs @ [x]))) (distinguishes M q1 q2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list.set [] \<subseteq> list.set pairs
(q1, q2) \<in> list.set [] \<or> (q2, q1) \<in> list.set []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
list.set [] \<subseteq> list.set pairs
(q1, q2) \<in> list.set [] \<or> (q2, q1) \<in> list.set []

goal (1 subgoal):
 1. \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty []). distinguishes M q1 q2 a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty []). distinguishes M q1 q2 a

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> list.set pairs; (q1, q2) \<in> list.set xs \<or> (q2, q1) \<in> list.set xs\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty xs)) (distinguishes M q1 q2); list.set (xs @ [x]) \<subseteq> list.set pairs; (q1, q2) \<in> list.set (xs @ [x]) \<or> (q2, q1) \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (xs @ [x]))) (distinguishes M q1 q2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> list.set pairs; (q1, q2) \<in> list.set xs \<or> (q2, q1) \<in> list.set xs\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty xs)) (distinguishes M q1 q2); list.set (xs @ [x]) \<subseteq> list.set pairs; (q1, q2) \<in> list.set (xs @ [x]) \<or> (q2, q1) \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (xs @ [x]))) (distinguishes M q1 q2)
[PROOF STEP]
case (snoc qq qqs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>list.set qqs \<subseteq> list.set pairs; (q1, q2) \<in> list.set qqs \<or> (q2, q1) \<in> list.set qqs\<rbrakk> \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty qqs). distinguishes M q1 q2 a
list.set (qqs @ [qq]) \<subseteq> list.set pairs
(q1, q2) \<in> list.set (qqs @ [qq]) \<or> (q2, q1) \<in> list.set (qqs @ [qq])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> list.set pairs; (q1, q2) \<in> list.set xs \<or> (q2, q1) \<in> list.set xs\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty xs)) (distinguishes M q1 q2); list.set (xs @ [x]) \<subseteq> list.set pairs; (q1, q2) \<in> list.set (xs @ [x]) \<or> (q2, q1) \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (xs @ [x]))) (distinguishes M q1 q2)
[PROOF STEP]
define W where "W = foldl handlePair empty qqs"
[PROOF STATE]
proof (state)
this:
W = foldl handlePair Prefix_Tree.empty qqs

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> list.set pairs; (q1, q2) \<in> list.set xs \<or> (q2, q1) \<in> list.set xs\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty xs)) (distinguishes M q1 q2); list.set (xs @ [x]) \<subseteq> list.set pairs; (q1, q2) \<in> list.set (xs @ [x]) \<or> (q2, q1) \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (xs @ [x]))) (distinguishes M q1 q2)
[PROOF STEP]
have "foldl handlePair empty (qqs@[qq]) = handlePair W qq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = handlePair W qq
[PROOF STEP]
unfolding W_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = handlePair (foldl handlePair Prefix_Tree.empty qqs) qq
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = handlePair W qq

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> list.set pairs; (q1, q2) \<in> list.set xs \<or> (q2, q1) \<in> list.set xs\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty xs)) (distinguishes M q1 q2); list.set (xs @ [x]) \<subseteq> list.set pairs; (q1, q2) \<in> list.set (xs @ [x]) \<or> (q2, q1) \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (xs @ [x]))) (distinguishes M q1 q2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = handlePair W qq
[PROOF STEP]
have W_subset: "set W \<subseteq> set (foldl handlePair empty (qqs@[qq]))"
[PROOF STATE]
proof (prove)
using this:
foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = handlePair W qq

goal (1 subgoal):
 1. Prefix_Tree.set W \<subseteq> Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))
[PROOF STEP]
by (metis handlePair_subset prod.collapse)
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set W \<subseteq> Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> list.set pairs; (q1, q2) \<in> list.set xs \<or> (q2, q1) \<in> list.set xs\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty xs)) (distinguishes M q1 q2); list.set (xs @ [x]) \<subseteq> list.set pairs; (q1, q2) \<in> list.set (xs @ [x]) \<or> (q2, q1) \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (xs @ [x]))) (distinguishes M q1 q2)
[PROOF STEP]
have handlePair_sym : "handlePair W (q1,q2) = handlePair W (q2,q1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. handlePair W (q1, q2) = handlePair W (q2, q1)
[PROOF STEP]
unfolding handlePair_def case_prod_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if contains_distinguishing_trace M W q1 q2 then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q1 q2)) = (if contains_distinguishing_trace M W q2 q1 then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q2 q1))
[PROOF STEP]
unfolding contains_distinguishing_trace_correctness[OF assms(1,3,4)] contains_distinguishing_trace_correctness[OF assms(1,4,3)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>io. isin W io \<and> distinguishes M q1 q2 io then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q1 q2)) = (if \<exists>io. isin W io \<and> distinguishes M q2 q1 io then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q2 q1))
[PROOF STEP]
unfolding get_distinguishing_sequence_from_ofsm_tables_sym[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>io. isin W io \<and> distinguishes M q1 q2 io then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q2 q1)) = (if \<exists>io. isin W io \<and> distinguishes M q2 q1 io then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q2 q1))
[PROOF STEP]
using distinguishes_sym
[PROOF STATE]
proof (prove)
using this:
distinguishes ?M ?q1.0 ?q2.0 ?io \<Longrightarrow> distinguishes ?M ?q2.0 ?q1.0 ?io

goal (1 subgoal):
 1. (if \<exists>io. isin W io \<and> distinguishes M q1 q2 io then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q2 q1)) = (if \<exists>io. isin W io \<and> distinguishes M q2 q1 io then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q2 q1))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
handlePair W (q1, q2) = handlePair W (q2, q1)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> list.set pairs; (q1, q2) \<in> list.set xs \<or> (q2, q1) \<in> list.set xs\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty xs)) (distinguishes M q1 q2); list.set (xs @ [x]) \<subseteq> list.set pairs; (q1, q2) \<in> list.set (xs @ [x]) \<or> (q2, q1) \<in> list.set (xs @ [x])\<rbrakk> \<Longrightarrow> Bex (Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (xs @ [x]))) (distinguishes M q1 q2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
proof (cases "qq = (q1,q2) \<or> qq = (q2,q1)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. qq = (q1, q2) \<or> qq = (q2, q1) \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
 2. \<not> (qq = (q1, q2) \<or> qq = (q2, q1)) \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
qq = (q1, q2) \<or> qq = (q2, q1)

goal (2 subgoals):
 1. qq = (q1, q2) \<or> qq = (q2, q1) \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
 2. \<not> (qq = (q1, q2) \<or> qq = (q2, q1)) \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qq = (q1, q2) \<or> qq = (q2, q1)
[PROOF STEP]
have "foldl handlePair empty (qqs@[qq]) = handlePair W (q1,q2)"
[PROOF STATE]
proof (prove)
using this:
qq = (q1, q2) \<or> qq = (q2, q1)

goal (1 subgoal):
 1. foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = handlePair W (q1, q2)
[PROOF STEP]
unfolding \<open>foldl handlePair empty (qqs@[qq]) = handlePair W qq\<close>
[PROOF STATE]
proof (prove)
using this:
qq = (q1, q2) \<or> qq = (q2, q1)

goal (1 subgoal):
 1. handlePair W qq = handlePair W (q1, q2)
[PROOF STEP]
using handlePair_sym
[PROOF STATE]
proof (prove)
using this:
qq = (q1, q2) \<or> qq = (q2, q1)
handlePair W (q1, q2) = handlePair W (q2, q1)

goal (1 subgoal):
 1. handlePair W qq = handlePair W (q1, q2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = handlePair W (q1, q2)

goal (2 subgoals):
 1. qq = (q1, q2) \<or> qq = (q2, q1) \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
 2. \<not> (qq = (q1, q2) \<or> qq = (q2, q1)) \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
proof (cases "contains_distinguishing_trace M W q1 q2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. contains_distinguishing_trace M W q1 q2 \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
 2. \<not> contains_distinguishing_trace M W q1 q2 \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
contains_distinguishing_trace M W q1 q2

goal (2 subgoals):
 1. contains_distinguishing_trace M W q1 q2 \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
 2. \<not> contains_distinguishing_trace M W q1 q2 \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
contains_distinguishing_trace M W q1 q2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
contains_distinguishing_trace M W q1 q2

goal (1 subgoal):
 1. \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
unfolding contains_distinguishing_trace_correctness[OF assms(1,3,4)]
[PROOF STATE]
proof (prove)
using this:
\<exists>io. isin W io \<and> distinguishes M q1 q2 io

goal (1 subgoal):
 1. \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
using W_subset
[PROOF STATE]
proof (prove)
using this:
\<exists>io. isin W io \<and> distinguishes M q1 q2 io
Prefix_Tree.set W \<subseteq> Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))

goal (1 subgoal):
 1. \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a

goal (1 subgoal):
 1. \<not> contains_distinguishing_trace M W q1 q2 \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> contains_distinguishing_trace M W q1 q2 \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> contains_distinguishing_trace M W q1 q2

goal (1 subgoal):
 1. \<not> contains_distinguishing_trace M W q1 q2 \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> contains_distinguishing_trace M W q1 q2
[PROOF STEP]
have "foldl handlePair empty (qqs@[qq]) = insert W (get_distinguishing_sequence_from_ofsm_tables M q1 q2)"
[PROOF STATE]
proof (prove)
using this:
\<not> contains_distinguishing_trace M W q1 q2

goal (1 subgoal):
 1. foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
unfolding \<open>foldl handlePair empty (qqs@[qq]) = handlePair W (q1,q2)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> contains_distinguishing_trace M W q1 q2

goal (1 subgoal):
 1. handlePair W (q1, q2) = Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
unfolding handlePair_def case_prod_conv
[PROOF STATE]
proof (prove)
using this:
\<not> contains_distinguishing_trace M W q1 q2

goal (1 subgoal):
 1. (if contains_distinguishing_trace M W q1 q2 then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q1 q2)) = Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q1 q2)

goal (1 subgoal):
 1. \<not> contains_distinguishing_trace M W q1 q2 \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
[PROOF STEP]
have "get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> set (foldl handlePair empty (qqs@[qq]))"
[PROOF STATE]
proof (prove)
using this:
foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q1 q2)

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))
[PROOF STEP]
using insert_isin
[PROOF STATE]
proof (prove)
using this:
foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q1 q2)
?xs \<in> Prefix_Tree.set (Prefix_Tree.insert ?t ?xs)

goal (1 subgoal):
 1. get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))

goal (1 subgoal):
 1. \<not> contains_distinguishing_trace M W q1 q2 \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))

goal (1 subgoal):
 1. \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
using get_distinguishing_sequence_from_ofsm_tables_distinguishes[OF assms]
[PROOF STATE]
proof (prove)
using this:
get_distinguishing_sequence_from_ofsm_tables M q1 q2 \<in> Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))
distinguishes M q1 q2 (get_distinguishing_sequence_from_ofsm_tables M q1 q2)

goal (1 subgoal):
 1. \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a

goal (1 subgoal):
 1. \<not> (qq = (q1, q2) \<or> qq = (q2, q1)) \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (qq = (q1, q2) \<or> qq = (q2, q1)) \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (qq = (q1, q2) \<or> qq = (q2, q1))

goal (1 subgoal):
 1. \<not> (qq = (q1, q2) \<or> qq = (q2, q1)) \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (qq = (q1, q2) \<or> qq = (q2, q1))
[PROOF STEP]
have "(q1, q2) \<in> list.set qqs \<or> (q2, q1) \<in> list.set qqs"
[PROOF STATE]
proof (prove)
using this:
\<not> (qq = (q1, q2) \<or> qq = (q2, q1))

goal (1 subgoal):
 1. (q1, q2) \<in> list.set qqs \<or> (q2, q1) \<in> list.set qqs
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
\<not> (qq = (q1, q2) \<or> qq = (q2, q1))
list.set (qqs @ [qq]) \<subseteq> list.set pairs
(q1, q2) \<in> list.set (qqs @ [qq]) \<or> (q2, q1) \<in> list.set (qqs @ [qq])

goal (1 subgoal):
 1. (q1, q2) \<in> list.set qqs \<or> (q2, q1) \<in> list.set qqs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(q1, q2) \<in> list.set qqs \<or> (q2, q1) \<in> list.set qqs

goal (1 subgoal):
 1. \<not> (qq = (q1, q2) \<or> qq = (q2, q1)) \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q1, q2) \<in> list.set qqs \<or> (q2, q1) \<in> list.set qqs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(q1, q2) \<in> list.set qqs \<or> (q2, q1) \<in> list.set qqs

goal (1 subgoal):
 1. \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
using snoc W_subset
[PROOF STATE]
proof (prove)
using this:
(q1, q2) \<in> list.set qqs \<or> (q2, q1) \<in> list.set qqs
\<lbrakk>list.set qqs \<subseteq> list.set pairs; (q1, q2) \<in> list.set qqs \<or> (q2, q1) \<in> list.set qqs\<rbrakk> \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty qqs). distinguishes M q1 q2 a
list.set (qqs @ [qq]) \<subseteq> list.set pairs
(q1, q2) \<in> list.set (qqs @ [qq]) \<or> (q2, q1) \<in> list.set (qqs @ [qq])
Prefix_Tree.set W \<subseteq> Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))

goal (1 subgoal):
 1. \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
unfolding W_def
[PROOF STATE]
proof (prove)
using this:
(q1, q2) \<in> list.set qqs \<or> (q2, q1) \<in> list.set qqs
\<lbrakk>list.set qqs \<subseteq> list.set pairs; (q1, q2) \<in> list.set qqs \<or> (q2, q1) \<in> list.set qqs\<rbrakk> \<Longrightarrow> \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty qqs). distinguishes M q1 q2 a
list.set (qqs @ [qq]) \<subseteq> list.set pairs
(q1, q2) \<in> list.set (qqs @ [qq]) \<or> (q2, q1) \<in> list.set (qqs @ [qq])
Prefix_Tree.set (foldl handlePair Prefix_Tree.empty qqs) \<subseteq> Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))

goal (1 subgoal):
 1. \<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a
[PROOF STEP]
by (meson dual_order.trans list_prefix_subset subsetD)
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty (qqs @ [qq])). distinguishes M q1 q2 a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>io\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty pairs'). distinguishes M q1 q2 io

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>list.set ?pairs' \<subseteq> list.set pairs; (q1, q2) \<in> list.set ?pairs' \<or> (q2, q1) \<in> list.set ?pairs'\<rbrakk> \<Longrightarrow> \<exists>io\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty ?pairs'). distinguishes M q1 q2 io

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set_reduced M). distinguishes M q1 q2 io
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(q1, q2) \<in> list.set pairs \<or> (q2, q1) \<in> list.set pairs
\<lbrakk>list.set ?pairs' \<subseteq> list.set pairs; (q1, q2) \<in> list.set ?pairs' \<or> (q2, q1) \<in> list.set ?pairs'\<rbrakk> \<Longrightarrow> \<exists>io\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty ?pairs'). distinguishes M q1 q2 io
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(q1, q2) \<in> list.set pairs \<or> (q2, q1) \<in> list.set pairs
\<lbrakk>list.set ?pairs' \<subseteq> list.set pairs; (q1, q2) \<in> list.set ?pairs' \<or> (q2, q1) \<in> list.set ?pairs'\<rbrakk> \<Longrightarrow> \<exists>io\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty ?pairs'). distinguishes M q1 q2 io

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (distinguishing_set_reduced M). distinguishes M q1 q2 io
[PROOF STEP]
unfolding \<open>distinguishing_set_reduced M = foldl handlePair empty pairs\<close>
[PROOF STATE]
proof (prove)
using this:
(q1, q2) \<in> list.set pairs \<or> (q2, q1) \<in> list.set pairs
\<lbrakk>list.set ?pairs' \<subseteq> list.set pairs; (q1, q2) \<in> list.set ?pairs' \<or> (q2, q1) \<in> list.set ?pairs'\<rbrakk> \<Longrightarrow> \<exists>io\<in>Prefix_Tree.set (foldl handlePair Prefix_Tree.empty ?pairs'). distinguishes M q1 q2 io

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinguishing_set_reduced_finite :
  "finite_tree (distinguishing_set_reduced M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (distinguishing_set_reduced M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite_tree (distinguishing_set_reduced M)
[PROOF STEP]
define pairs where pairs: "pairs = filter (\<lambda> (x,y) . x \<noteq> y) (list_ordered_pairs (states_as_list M))"
[PROOF STATE]
proof (state)
this:
pairs = filter (\<lambda>(x, y). x \<noteq> y) (list_ordered_pairs (states_as_list M))

goal (1 subgoal):
 1. finite_tree (distinguishing_set_reduced M)
[PROOF STEP]
define handlePair where "handlePair = (\<lambda> W (q,q') . if contains_distinguishing_trace M W q q'
                                then W
                                else insert W (get_distinguishing_sequence_from_ofsm_tables M q q'))"
[PROOF STATE]
proof (state)
this:
handlePair = (\<lambda>W (q, q'). if contains_distinguishing_trace M W q q' then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q q'))

goal (1 subgoal):
 1. finite_tree (distinguishing_set_reduced M)
[PROOF STEP]
have "distinguishing_set_reduced M = foldl handlePair empty pairs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinguishing_set_reduced M = foldl handlePair Prefix_Tree.empty pairs
[PROOF STEP]
unfolding distinguishing_set_reduced.simps handlePair_def pairs Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>W (q, q'). if contains_distinguishing_trace M W q q' then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q q')) Prefix_Tree.empty (filter (\<lambda>(q, q'). q \<noteq> q') (list_ordered_pairs (states_as_list M))) = foldl (\<lambda>W (q, q'). if contains_distinguishing_trace M W q q' then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q q')) Prefix_Tree.empty (filter (\<lambda>(x, y). x \<noteq> y) (list_ordered_pairs (states_as_list M)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
distinguishing_set_reduced M = foldl handlePair Prefix_Tree.empty pairs

goal (1 subgoal):
 1. finite_tree (distinguishing_set_reduced M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (distinguishing_set_reduced M)
[PROOF STEP]
unfolding \<open>distinguishing_set_reduced M = foldl handlePair empty pairs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (foldl handlePair Prefix_Tree.empty pairs)
[PROOF STEP]
proof (induction pairs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite_tree (foldl handlePair Prefix_Tree.empty [])
 2. \<And>x xs. finite_tree (foldl handlePair Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl handlePair Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite_tree (foldl handlePair Prefix_Tree.empty [])
 2. \<And>x xs. finite_tree (foldl handlePair Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl handlePair Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (foldl handlePair Prefix_Tree.empty [])
[PROOF STEP]
using empty_finite_tree
[PROOF STATE]
proof (prove)
using this:
finite_tree Prefix_Tree.empty

goal (1 subgoal):
 1. finite_tree (foldl handlePair Prefix_Tree.empty [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (foldl handlePair Prefix_Tree.empty [])

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl handlePair Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl handlePair Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl handlePair Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl handlePair Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
case (snoc qq qqs)
[PROOF STATE]
proof (state)
this:
finite_tree (foldl handlePair Prefix_Tree.empty qqs)

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl handlePair Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl handlePair Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
define W where "W = foldl handlePair empty qqs"
[PROOF STATE]
proof (state)
this:
W = foldl handlePair Prefix_Tree.empty qqs

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl handlePair Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl handlePair Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
have "foldl handlePair empty (qqs@[qq]) = handlePair W qq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = handlePair W qq
[PROOF STEP]
unfolding W_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = handlePair (foldl handlePair Prefix_Tree.empty qqs) qq
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl handlePair Prefix_Tree.empty (qqs @ [qq]) = handlePair W qq

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl handlePair Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl handlePair Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
have "finite_tree W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree W
[PROOF STEP]
using snoc W_def
[PROOF STATE]
proof (prove)
using this:
finite_tree (foldl handlePair Prefix_Tree.empty qqs)
W = foldl handlePair Prefix_Tree.empty qqs

goal (1 subgoal):
 1. finite_tree W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree W

goal (1 subgoal):
 1. \<And>x xs. finite_tree (foldl handlePair Prefix_Tree.empty xs) \<Longrightarrow> finite_tree (foldl handlePair Prefix_Tree.empty (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite_tree W
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite_tree W

goal (1 subgoal):
 1. finite_tree (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))
[PROOF STEP]
unfolding \<open>foldl handlePair empty (qqs@[qq]) = handlePair W qq\<close>
[PROOF STATE]
proof (prove)
using this:
finite_tree W

goal (1 subgoal):
 1. finite_tree (handlePair W qq)
[PROOF STEP]
unfolding handlePair_def
[PROOF STATE]
proof (prove)
using this:
finite_tree W

goal (1 subgoal):
 1. finite_tree (case qq of (q, q') \<Rightarrow> if contains_distinguishing_trace M W q q' then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q q'))
[PROOF STEP]
using insert_finite_tree[of W]
[PROOF STATE]
proof (prove)
using this:
finite_tree W
finite_tree W \<Longrightarrow> finite_tree (Prefix_Tree.insert W ?xs)

goal (1 subgoal):
 1. finite_tree (case qq of (q, q') \<Rightarrow> if contains_distinguishing_trace M W q q' then W else Prefix_Tree.insert W (get_distinguishing_sequence_from_ofsm_tables M q q'))
[PROOF STEP]
by (simp add: case_prod_unfold)
[PROOF STATE]
proof (state)
this:
finite_tree (foldl handlePair Prefix_Tree.empty (qqs @ [qq]))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_distinguishing_set_distinguishes :
  assumes "observable M"
  and     "minimal M"
  and     "\<alpha> \<in> L M"
  and     "\<beta> \<in> L M"
  and     "after_initial M \<alpha> \<noteq> after_initial M \<beta>"
shows "\<exists> io \<in> set (add_distinguishing_set M ((\<alpha>,after_initial M \<alpha>),(\<beta>,after_initial M \<beta>)) t) \<union> (set (after t \<alpha>) \<inter> set (after t \<beta>)) . distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (add_distinguishing_set M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>). distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io
[PROOF STEP]
using distinguishing_set_distinguishes[OF assms(1,2) after_is_state[OF assms(1,3)] after_is_state[OF assms(1,4)] assms(5)]
[PROOF STATE]
proof (prove)
using this:
\<exists>io\<in>Prefix_Tree.set (distinguishing_set M). distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io

goal (1 subgoal):
 1. \<exists>io\<in>Prefix_Tree.set (add_distinguishing_set M ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) t) \<union> Prefix_Tree.set (Prefix_Tree.after t \<alpha>) \<inter> Prefix_Tree.set (Prefix_Tree.after t \<beta>). distinguishes M (after_initial M \<alpha>) (after_initial M \<beta>) io
[PROOF STEP]
by force


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

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


[STATEMENT]
lemma sort_unverified_transitions_by_state_cover_length_retains_set :
  "List.set xs = List.set (sort_unverified_transitions_by_state_cover_length M1 (get_state_cover M1) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set xs = list.set (sort_unverified_transitions_by_state_cover_length M1 (get_state_cover M1) xs)
[PROOF STEP]
unfolding sort_unverified_transitions_by_state_cover_length_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set xs = list.set (mergesort_by_rel (\<lambda>t1 t2. (case Mapping.lookup (mapping_of (map (\<lambda>t. (t, length (get_state_cover M1 (t_source t)) + length (get_state_cover M1 (t_target t)))) xs)) t1 of None \<Rightarrow> 2 * FSM.size M1 | Some w \<Rightarrow> w) \<le> (case Mapping.lookup (mapping_of (map (\<lambda>t. (t, length (get_state_cover M1 (t_source t)) + length (get_state_cover M1 (t_target t)))) xs)) t2 of None \<Rightarrow> 2 * FSM.size M1 | Some w \<Rightarrow> w)) xs)
[PROOF STEP]
unfolding set_mergesort_by_rel
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set xs = list.set xs
[PROOF STEP]
by simp


[STATEMENT]
lemma poincare_circle_in_disc:
  assumes "r > 0" and "z \<in> unit_disc" and "(ze, re) = poincare_circle_euclidean z r"
  shows "cmod ze < 1" "re > 0" "\<forall> x \<in> circle ze re. cmod x < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod ze < 1 &&& 0 < re &&& \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
let ?R = "(cosh r - 1) / 2"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
let ?z' = "to_complex z"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
let ?cz = "1 - (cmod ?z')\<^sup>2"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
let ?k = "?cz * ?R + 1"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
let ?ze = "?z' / ?k"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
let ?re = "?cz * sqrt(?R * (?R + 1)) / ?k"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
from \<open>z \<in> unit_disc\<close>
[PROOF STATE]
proof (chain)
picking this:
z \<in> unit_disc
[PROOF STEP]
obtain z' where z': "z = of_complex z'"
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc

goal (1 subgoal):
 1. (\<And>z'. z = of_complex z' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of z]
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc
z = \<infinity>\<^sub>h \<or> (\<exists>x. z = of_complex x)

goal (1 subgoal):
 1. (\<And>z'. z = of_complex z' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z = of_complex z'

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
hence "z' = ?z'"
[PROOF STATE]
proof (prove)
using this:
z = of_complex z'

goal (1 subgoal):
 1. z' = to_complex z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z' = to_complex z

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
obtain cz where cz: "cz = (1 - (cmod z')\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cz. cz = 1 - (cmod z')\<^sup>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cz = 1 - (cmod z')\<^sup>2

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
have "cz > 0" "cz \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < cz &&& cz \<le> 1
[PROOF STEP]
using \<open>z \<in> unit_disc\<close> z' cz
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc
z = of_complex z'
cz = 1 - (cmod z')\<^sup>2

goal (1 subgoal):
 1. 0 < cz &&& cz \<le> 1
[PROOF STEP]
using unit_disc_cmod_square_lt_1
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc
z = of_complex z'
cz = 1 - (cmod z')\<^sup>2
?z \<in> unit_disc \<Longrightarrow> (cmod (to_complex ?z))\<^sup>2 < 1

goal (1 subgoal):
 1. 0 < cz &&& cz \<le> 1
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
0 < cz
cz \<le> 1

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
obtain R where R: "R = ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>R. R = (cosh r - 1) / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R = (cosh r - 1) / 2

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
have "R > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < R
[PROOF STEP]
using cosh_gt_1[of r] \<open>r > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r \<Longrightarrow> 1 < cosh r
0 < r

goal (1 subgoal):
 1. 0 < R
[PROOF STEP]
by (subst R) simp
[PROOF STATE]
proof (state)
this:
0 < R

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
obtain k where k: "k = cz * R + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. k = cz * R + 1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = cz * R + 1

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
have "k > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < k
[PROOF STEP]
using k \<open>R > 0\<close> \<open>cz > 0\<close>
[PROOF STATE]
proof (prove)
using this:
k = cz * R + 1
0 < R
0 < cz

goal (1 subgoal):
 1. 1 < k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < k

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
hence "cmod k = k"
[PROOF STATE]
proof (prove)
using this:
1 < k

goal (1 subgoal):
 1. cmod (cor k) = k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod (cor k) = k

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
let ?RR = "cz * sqrt(R * (R + 1)) / k"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
have "cmod z' + cz * sqrt(R * (R + 1)) < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
have "((R+1)-R)\<^sup>2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (R + 1 - R)\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < (R + 1 - R)\<^sup>2

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
hence "(R+1)\<^sup>2 - 2*R*(R+1) + R\<^sup>2 > 0"
[PROOF STATE]
proof (prove)
using this:
0 < (R + 1 - R)\<^sup>2

goal (1 subgoal):
 1. 0 < (R + 1)\<^sup>2 - 2 * R * (R + 1) + R\<^sup>2
[PROOF STEP]
unfolding power2_diff
[PROOF STATE]
proof (prove)
using this:
0 < (R + 1)\<^sup>2 + R\<^sup>2 - 2 * (R + 1) * R

goal (1 subgoal):
 1. 0 < (R + 1)\<^sup>2 - 2 * R * (R + 1) + R\<^sup>2
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
0 < (R + 1)\<^sup>2 - 2 * R * (R + 1) + R\<^sup>2

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
hence "(R+1)\<^sup>2 + 2*R*(R+1) + R\<^sup>2 - 4*R*(R+1) > 0"
[PROOF STATE]
proof (prove)
using this:
0 < (R + 1)\<^sup>2 - 2 * R * (R + 1) + R\<^sup>2

goal (1 subgoal):
 1. 0 < (R + 1)\<^sup>2 + 2 * R * (R + 1) + R\<^sup>2 - 4 * R * (R + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < (R + 1)\<^sup>2 + 2 * R * (R + 1) + R\<^sup>2 - 4 * R * (R + 1)

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
hence "(2*R+1)\<^sup>2 / 4 > R*(R+1)"
[PROOF STATE]
proof (prove)
using this:
0 < (R + 1)\<^sup>2 + 2 * R * (R + 1) + R\<^sup>2 - 4 * R * (R + 1)

goal (1 subgoal):
 1. R * (R + 1) < (2 * R + 1)\<^sup>2 / 4
[PROOF STEP]
using power2_sum[of "R+1" R]
[PROOF STATE]
proof (prove)
using this:
0 < (R + 1)\<^sup>2 + 2 * R * (R + 1) + R\<^sup>2 - 4 * R * (R + 1)
(R + 1 + R)\<^sup>2 = (R + 1)\<^sup>2 + R\<^sup>2 + 2 * (R + 1) * R

goal (1 subgoal):
 1. R * (R + 1) < (2 * R + 1)\<^sup>2 / 4
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
R * (R + 1) < (2 * R + 1)\<^sup>2 / 4

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
hence "sqrt(R*(R+1)) < (2*R+1) / 2"
[PROOF STATE]
proof (prove)
using this:
R * (R + 1) < (2 * R + 1)\<^sup>2 / 4

goal (1 subgoal):
 1. sqrt (R * (R + 1)) < (2 * R + 1) / 2
[PROOF STEP]
using \<open>R > 0\<close>
[PROOF STATE]
proof (prove)
using this:
R * (R + 1) < (2 * R + 1)\<^sup>2 / 4
0 < R

goal (1 subgoal):
 1. sqrt (R * (R + 1)) < (2 * R + 1) / 2
[PROOF STEP]
by (smt arith_geo_mean_sqrt power_divide real_sqrt_four real_sqrt_pow2 zero_le_mult_iff)
[PROOF STATE]
proof (state)
this:
sqrt (R * (R + 1)) < (2 * R + 1) / 2

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
hence "sqrt(R*(R+1)) - R < 1/2"
[PROOF STATE]
proof (prove)
using this:
sqrt (R * (R + 1)) < (2 * R + 1) / 2

goal (1 subgoal):
 1. sqrt (R * (R + 1)) - R < 1 / 2
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
sqrt (R * (R + 1)) - R < 1 / 2

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
hence "(1 + (cmod z')) * (sqrt(R*(R+1)) - R) < (1 + (cmod z')) *  (1 / 2)"
[PROOF STATE]
proof (prove)
using this:
sqrt (R * (R + 1)) - R < 1 / 2

goal (1 subgoal):
 1. (1 + cmod z') * (sqrt (R * (R + 1)) - R) < (1 + cmod z') * (1 / 2)
[PROOF STEP]
by (subst mult_strict_left_mono, simp, smt norm_not_less_zero, simp)
[PROOF STATE]
proof (state)
this:
(1 + cmod z') * (sqrt (R * (R + 1)) - R) < (1 + cmod z') * (1 / 2)

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 + cmod z') * (sqrt (R * (R + 1)) - R) < (1 + cmod z') * (1 / 2)

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
have "... < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + cmod z') * (1 / 2) < 1
[PROOF STEP]
using \<open>z \<in> unit_disc\<close> z'
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc
z = of_complex z'

goal (1 subgoal):
 1. (1 + cmod z') * (1 / 2) < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1 + cmod z') * (1 / 2) < 1

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(1 + cmod z') * (sqrt (R * (R + 1)) - R) < 1
[PROOF STEP]
have "(1 - cmod z') * ((1 + cmod z') * (sqrt(R*(R+1)) - R)) < (1 - cmod z') * 1"
[PROOF STATE]
proof (prove)
using this:
(1 + cmod z') * (sqrt (R * (R + 1)) - R) < 1

goal (1 subgoal):
 1. (1 - cmod z') * ((1 + cmod z') * (sqrt (R * (R + 1)) - R)) < (1 - cmod z') * 1
[PROOF STEP]
using \<open>z \<in> unit_disc\<close> z'
[PROOF STATE]
proof (prove)
using this:
(1 + cmod z') * (sqrt (R * (R + 1)) - R) < 1
z \<in> unit_disc
z = of_complex z'

goal (1 subgoal):
 1. (1 - cmod z') * ((1 + cmod z') * (sqrt (R * (R + 1)) - R)) < (1 - cmod z') * 1
[PROOF STEP]
by (subst mult_strict_left_mono, simp_all)
[PROOF STATE]
proof (state)
this:
(1 - cmod z') * ((1 + cmod z') * (sqrt (R * (R + 1)) - R)) < (1 - cmod z') * 1

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
hence "cz * (sqrt (R*(R+1)) - R) < 1 - cmod z'"
[PROOF STATE]
proof (prove)
using this:
(1 - cmod z') * ((1 + cmod z') * (sqrt (R * (R + 1)) - R)) < (1 - cmod z') * 1

goal (1 subgoal):
 1. cz * (sqrt (R * (R + 1)) - R) < 1 - cmod z'
[PROOF STEP]
using square_diff_square_factored[of 1 "cmod z'"]
[PROOF STATE]
proof (prove)
using this:
(1 - cmod z') * ((1 + cmod z') * (sqrt (R * (R + 1)) - R)) < (1 - cmod z') * 1
1 * 1 - cmod z' * cmod z' = (1 + cmod z') * (1 - cmod z')

goal (1 subgoal):
 1. cz * (sqrt (R * (R + 1)) - R) < 1 - cmod z'
[PROOF STEP]
by (subst cz, subst (asm) mult.assoc[symmetric], simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
cz * (sqrt (R * (R + 1)) - R) < 1 - cmod z'

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
hence "cmod z' + cz * sqrt(R*(R+1)) < 1 + R * cz"
[PROOF STATE]
proof (prove)
using this:
cz * (sqrt (R * (R + 1)) - R) < 1 - cmod z'

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < 1 + R * cz
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
cmod z' + cz * sqrt (R * (R + 1)) < 1 + R * cz

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cmod z' + cz * sqrt (R * (R + 1)) < 1 + R * cz

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
cmod z' + cz * sqrt (R * (R + 1)) < 1 + R * cz
k = cz * R + 1

goal (1 subgoal):
 1. cmod z' + cz * sqrt (R * (R + 1)) < k
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
cmod z' + cz * sqrt (R * (R + 1)) < k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cmod z' + cz * sqrt (R * (R + 1)) < k

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
hence "cmod z' / k + cz * sqrt(R * (R + 1)) / k < 1"
[PROOF STATE]
proof (prove)
using this:
cmod z' + cz * sqrt (R * (R + 1)) < k

goal (1 subgoal):
 1. cmod z' / k + cz * sqrt (R * (R + 1)) / k < 1
[PROOF STEP]
using \<open>k > 1\<close>
[PROOF STATE]
proof (prove)
using this:
cmod z' + cz * sqrt (R * (R + 1)) < k
1 < k

goal (1 subgoal):
 1. cmod z' / k + cz * sqrt (R * (R + 1)) / k < 1
[PROOF STEP]
unfolding add_divide_distrib[symmetric]
[PROOF STATE]
proof (prove)
using this:
cmod z' + cz * sqrt (R * (R + 1)) < k
1 < k

goal (1 subgoal):
 1. (cmod z' + cz * sqrt (R * (R + 1))) / k < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod z' / k + cz * sqrt (R * (R + 1)) / k < 1

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
hence "cmod (z' / k) + cz * sqrt(R * (R + 1)) / k < 1"
[PROOF STATE]
proof (prove)
using this:
cmod z' / k + cz * sqrt (R * (R + 1)) / k < 1

goal (1 subgoal):
 1. cmod (z' / cor k) + cz * sqrt (R * (R + 1)) / k < 1
[PROOF STEP]
using \<open>k > 1\<close>
[PROOF STATE]
proof (prove)
using this:
cmod z' / k + cz * sqrt (R * (R + 1)) / k < 1
1 < k

goal (1 subgoal):
 1. cmod (z' / cor k) + cz * sqrt (R * (R + 1)) / k < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod (z' / cor k) + cz * sqrt (R * (R + 1)) / k < 1

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
hence "cmod ?ze + ?re < 1"
[PROOF STATE]
proof (prove)
using this:
cmod (z' / cor k) + cz * sqrt (R * (R + 1)) / k < 1

goal (1 subgoal):
 1. cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) + (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1) < 1
[PROOF STEP]
using k cz \<open>R = ?R\<close> z'
[PROOF STATE]
proof (prove)
using this:
cmod (z' / cor k) + cz * sqrt (R * (R + 1)) / k < 1
k = cz * R + 1
cz = 1 - (cmod z')\<^sup>2
R = (cosh r - 1) / 2
z = of_complex z'

goal (1 subgoal):
 1. cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) + (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1) < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) + (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1) < 1

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) + (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1) < 1

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
have "cz * sqrt(R * (R + 1)) / k > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < cz * sqrt (R * (R + 1)) / k
[PROOF STEP]
using \<open>cz > 0\<close> \<open>R > 0\<close> \<open>k > 1\<close>
[PROOF STATE]
proof (prove)
using this:
0 < cz
0 < R
1 < k

goal (1 subgoal):
 1. 0 < cz * sqrt (R * (R + 1)) / k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < cz * sqrt (R * (R + 1)) / k

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
hence "?re > 0"
[PROOF STATE]
proof (prove)
using this:
0 < cz * sqrt (R * (R + 1)) / k

goal (1 subgoal):
 1. 0 < (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
[PROOF STEP]
using k cz \<open>R = ?R\<close> z'
[PROOF STATE]
proof (prove)
using this:
0 < cz * sqrt (R * (R + 1)) / k
k = cz * R + 1
cz = 1 - (cmod z')\<^sup>2
R = (cosh r - 1) / 2
z = of_complex z'

goal (1 subgoal):
 1. 0 < (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
have "cmod ?ze < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) < 1
[PROOF STEP]
using \<open>cmod ?ze + ?re < 1\<close> \<open>?re > 0\<close>
[PROOF STATE]
proof (prove)
using this:
cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) + (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1) < 1
0 < (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)

goal (1 subgoal):
 1. cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) < 1

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) < 1

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
have "ze = ?ze" "re = ?re"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ze = to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1) &&& re = (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
[PROOF STEP]
using \<open>(ze, re) = poincare_circle_euclidean z r\<close>
[PROOF STATE]
proof (prove)
using this:
(ze, re) = poincare_circle_euclidean z r

goal (1 subgoal):
 1. ze = to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1) &&& re = (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
[PROOF STEP]
unfolding poincare_circle_euclidean_def Let_def
[PROOF STATE]
proof (prove)
using this:
(ze, re) = (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1), (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1))

goal (1 subgoal):
 1. ze = to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1) &&& re = (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
ze = to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
re = (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ze = to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
re = (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
have "\<forall> x \<in> circle ze re. cmod x \<le> cmod ze + re"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>circle ze re. cmod x \<le> cmod ze + re
[PROOF STEP]
using norm_triangle_ineq2[of _ ze]
[PROOF STATE]
proof (prove)
using this:
cmod ?a - cmod ze \<le> cmod (?a - ze)

goal (1 subgoal):
 1. \<forall>x\<in>circle ze re. cmod x \<le> cmod ze + re
[PROOF STEP]
unfolding circle_def
[PROOF STATE]
proof (prove)
using this:
cmod ?a - cmod ze \<le> cmod (?a - ze)

goal (1 subgoal):
 1. \<forall>x\<in>{z. cmod (z - ze) = re}. cmod x \<le> cmod ze + re
[PROOF STEP]
by (smt mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>circle ze re. cmod x \<le> cmod ze + re

goal (3 subgoals):
 1. cmod ze < 1
 2. 0 < re
 3. \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) + (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1) < 1
0 < (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) < 1
ze = to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
re = (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
\<forall>x\<in>circle ze re. cmod x \<le> cmod ze + re
[PROOF STEP]
show "cmod ze < 1" "re > 0" "\<forall> x \<in> circle ze re. cmod x < 1"
[PROOF STATE]
proof (prove)
using this:
cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) + (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1) < 1
0 < (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
cmod (to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)) < 1
ze = to_complex z / cor ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
re = (1 - (cmod (to_complex z))\<^sup>2) * sqrt ((cosh r - 1) / 2 * ((cosh r - 1) / 2 + 1)) / ((1 - (cmod (to_complex z))\<^sup>2) * ((cosh r - 1) / 2) + 1)
\<forall>x\<in>circle ze re. cmod x \<le> cmod ze + re

goal (1 subgoal):
 1. cmod ze < 1 &&& 0 < re &&& \<forall>x\<in>circle ze re. cmod x < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod ze < 1
0 < re
\<forall>x\<in>circle ze re. cmod x < 1

goal:
No subgoals!
[PROOF STEP]
qed