[STATEMENT]
lemma  product_target_split:
  assumes "target (q1,q2) p = (q1',q2')"
  shows "target q1 (left_path p) = q1'"
    and "target q2 (right_path p) = q2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target q1 (left_path p) = q1' &&& target q2 (right_path p) = q2'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
target (q1, q2) p = (q1', q2')

goal (1 subgoal):
 1. target q1 (left_path p) = q1' &&& target q2 (right_path p) = q2'
[PROOF STEP]
by (induction p arbitrary: q1 q2; force)+


[STATEMENT]
lemma target_single_transition[simp] : "target q1 [(q1, x, y, q1')] = q1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target q1 [(q1, x, y, q1')] = q1'
[PROOF STEP]
by auto


[STATEMENT]
lemma product_undefined_input :
  assumes "\<not> (\<exists> t \<in> transitions (product (from_FSM M q1) (from_FSM M q2)).
               t_source t = qq \<and> t_input t = x)"
  and "q1 \<in> states M"
  and "q2 \<in> states M"
shows "\<not> (\<exists> t1 \<in> transitions M. \<exists> t2 \<in> transitions M.
                 t_source t1 = fst qq \<and>
                 t_source t2 = snd qq \<and>
                 t_input t1 = x \<and> t_input t2 = x \<and> t_output t1 = t_output t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<exists>t1\<in>FSM.transitions M. \<exists>t2\<in>FSM.transitions M. t_source t1 = fst qq \<and> t_source t2 = snd qq \<and> t_input t1 = x \<and> t_input t2 = x \<and> t_output t1 = t_output t2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t1\<in>FSM.transitions M. \<exists>t2\<in>FSM.transitions M. t_source t1 = fst qq \<and> t_source t2 = snd qq \<and> t_input t1 = x \<and> t_input t2 = x \<and> t_output t1 = t_output t2 \<Longrightarrow> False
[PROOF STEP]
assume "\<exists> t1 \<in> transitions M. \<exists> t2 \<in> transitions M.
                 t_source t1 = fst qq \<and>
                 t_source t2 = snd qq \<and>
                 t_input t1 = x \<and> t_input t2 = x \<and> t_output t1 = t_output t2"
[PROOF STATE]
proof (state)
this:
\<exists>t1\<in>FSM.transitions M. \<exists>t2\<in>FSM.transitions M. t_source t1 = fst qq \<and> t_source t2 = snd qq \<and> t_input t1 = x \<and> t_input t2 = x \<and> t_output t1 = t_output t2

goal (1 subgoal):
 1. \<exists>t1\<in>FSM.transitions M. \<exists>t2\<in>FSM.transitions M. t_source t1 = fst qq \<and> t_source t2 = snd qq \<and> t_input t1 = x \<and> t_input t2 = x \<and> t_output t1 = t_output t2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t1\<in>FSM.transitions M. \<exists>t2\<in>FSM.transitions M. t_source t1 = fst qq \<and> t_source t2 = snd qq \<and> t_input t1 = x \<and> t_input t2 = x \<and> t_output t1 = t_output t2
[PROOF STEP]
obtain t1 t2 where "t1 \<in> transitions M"
                      and "t2 \<in> transitions M"
                      and "t_source t1 = fst qq"
                      and "t_source t2 = snd qq"
                      and "t_input t1 = x"
                      and "t_input t1 = t_input t2"
                      and "t_output t1 = t_output t2"
[PROOF STATE]
proof (prove)
using this:
\<exists>t1\<in>FSM.transitions M. \<exists>t2\<in>FSM.transitions M. t_source t1 = fst qq \<and> t_source t2 = snd qq \<and> t_input t1 = x \<and> t_input t2 = x \<and> t_output t1 = t_output t2

goal (1 subgoal):
 1. (\<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions M; t2 \<in> FSM.transitions M; t_source t1 = fst qq; t_source t2 = snd qq; t_input t1 = x; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
t1 \<in> FSM.transitions M
t2 \<in> FSM.transitions M
t_source t1 = fst qq
t_source t2 = snd qq
t_input t1 = x
t_input t1 = t_input t2
t_output t1 = t_output t2

goal (1 subgoal):
 1. \<exists>t1\<in>FSM.transitions M. \<exists>t2\<in>FSM.transitions M. t_source t1 = fst qq \<and> t_source t2 = snd qq \<and> t_input t1 = x \<and> t_input t2 = x \<and> t_output t1 = t_output t2 \<Longrightarrow> False
[PROOF STEP]
have "((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2) \<in> transitions (product (from_FSM M q1) (from_FSM M q2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2) \<in> FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
unfolding product_transitions_alt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2) \<in> {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions (from_FSM M q1) \<and> tB \<in> FSM.transitions (from_FSM M q2) \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
unfolding from_FSM_simps[OF assms(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2) \<in> {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions M \<and> tB \<in> FSM.transitions (from_FSM M q2) \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
unfolding from_FSM_simps[OF assms(3)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2) \<in> {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions M \<and> tB \<in> FSM.transitions M \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
using \<open>t1 \<in> transitions M\<close> \<open>t2 \<in> transitions M\<close> \<open>t_input t1 = t_input t2\<close> \<open>t_output t1 = t_output t2\<close>
[PROOF STATE]
proof (prove)
using this:
t1 \<in> FSM.transitions M
t2 \<in> FSM.transitions M
t_input t1 = t_input t2
t_output t1 = t_output t2

goal (1 subgoal):
 1. ((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2) \<in> {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions M \<and> tB \<in> FSM.transitions M \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2) \<in> FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. \<exists>t1\<in>FSM.transitions M. \<exists>t2\<in>FSM.transitions M. t_source t1 = fst qq \<and> t_source t2 = snd qq \<and> t_input t1 = x \<and> t_input t2 = x \<and> t_output t1 = t_output t2 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2) \<in> FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2) \<in> FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding \<open>t_source t1 = fst qq\<close> \<open>t_source t2 = snd qq\<close> \<open>t_input t1 = x\<close> prod.collapse
[PROOF STATE]
proof (prove)
using this:
(qq, x, t_output t1, t_target t1, t_target t2) \<in> FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
(qq, x, t_output t1, t_target t1, t_target t2) \<in> FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
\<not> (\<exists>t\<in>FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2)). t_source t = qq \<and> t_input t = x)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_from_reachable_next :
  assumes "((q1,q2),x,y,(q1',q2')) \<in> transitions (product (from_FSM M q1) (from_FSM M q2))"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
  shows   "(from_FSM (product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = (product (from_FSM M q1') (from_FSM M q2'))"
          (is "?P1 = ?P2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2') = Product_FSM.product (from_FSM M q1') (from_FSM M q2')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2') = Product_FSM.product (from_FSM M q1') (from_FSM M q2')
[PROOF STEP]
have "(q1,x,y,q1') \<in> transitions (from_FSM M q1)"
  and  "(q2,x,y,q2') \<in> transitions (from_FSM M q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q1, x, y, q1') \<in> FSM.transitions (from_FSM M q1) &&& (q2, x, y, q2') \<in> FSM.transitions (from_FSM M q2)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
((q1, q2), x, y, q1', q2') \<in> FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. (q1, x, y, q1') \<in> FSM.transitions (from_FSM M q1) &&& (q2, x, y, q2') \<in> FSM.transitions (from_FSM M q2)
[PROOF STEP]
unfolding product_transitions_def
[PROOF STATE]
proof (prove)
using this:
((q1, q2), x, y, q1', q2') \<in> {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions (from_FSM M q1) \<and> (qB, x, y, qB') \<in> FSM.transitions (from_FSM M q2)}

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

goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2') = Product_FSM.product (from_FSM M q1') (from_FSM M q2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q1, x, y, q1') \<in> FSM.transitions (from_FSM M q1)
(q2, x, y, q2') \<in> FSM.transitions (from_FSM M q2)
[PROOF STEP]
have "q1' \<in> states (from_FSM M q1)" and "q2' \<in> states (from_FSM M q2)"
[PROOF STATE]
proof (prove)
using this:
(q1, x, y, q1') \<in> FSM.transitions (from_FSM M q1)
(q2, x, y, q2') \<in> FSM.transitions (from_FSM M q2)

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

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

goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2') = Product_FSM.product (from_FSM M q1') (from_FSM M q2')
[PROOF STEP]
have "q1' \<in> states (from_FSM M q1')" and "q1' \<in> states M" and "q1 \<in> states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q1' \<in> FSM.states (from_FSM M q1') &&& q1' \<in> FSM.states M &&& q1 \<in> FSM.states M
[PROOF STEP]
using \<open>q1' \<in> FSM.states (FSM.from_FSM M q1)\<close> assms(2) reachable_state_is_state
[PROOF STATE]
proof (prove)
using this:
q1' \<in> FSM.states (from_FSM M q1)
q1 \<in> FSM.states M
?q \<in> reachable_states ?M \<Longrightarrow> ?q \<in> FSM.states ?M

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

goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2') = Product_FSM.product (from_FSM M q1') (from_FSM M q2')
[PROOF STEP]
have "q2' \<in> states (from_FSM M q2')" and "q2' \<in> states M" and "q2 \<in> states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q2' \<in> FSM.states (from_FSM M q2') &&& q2' \<in> FSM.states M &&& q2 \<in> FSM.states M
[PROOF STEP]
using \<open>q2' \<in> FSM.states (FSM.from_FSM M q2)\<close> assms(3) reachable_state_is_state
[PROOF STATE]
proof (prove)
using this:
q2' \<in> FSM.states (from_FSM M q2)
q2 \<in> FSM.states M
?q \<in> reachable_states ?M \<Longrightarrow> ?q \<in> FSM.states ?M

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

goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2') = Product_FSM.product (from_FSM M q1') (from_FSM M q2')
[PROOF STEP]
have "initial ?P1 = initial ?P2"
  and  "states ?P1 = states ?P2"
  and  "inputs ?P1 = inputs ?P2"
  and  "outputs ?P1 = outputs ?P2"
  and  "transitions ?P1 = transitions ?P2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.initial (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) &&& FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))) &&& FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) &&& FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) &&& FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
[PROOF STEP]
using from_FSM_simps[OF fsm_transition_target[OF assms(1)]]
[PROOF STATE]
proof (prove)
using this:
FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (t_target ((q1, q2), x, y, q1', q2'))) = t_target ((q1, q2), x, y, q1', q2')
FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (t_target ((q1, q2), x, y, q1', q2'))) = FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (t_target ((q1, q2), x, y, q1', q2'))) = FSM.outputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (t_target ((q1, q2), x, y, q1', q2'))) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (t_target ((q1, q2), x, y, q1', q2'))) = FSM.states (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. (FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.initial (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) &&& FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))) &&& FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) &&& FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) &&& FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
[PROOF STEP]
unfolding snd_conv
[PROOF STATE]
proof (prove)
using this:
FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = (q1', q2')
FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. (FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.initial (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) &&& FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))) &&& FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) &&& FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) &&& FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
[PROOF STEP]
unfolding product_simps
[PROOF STATE]
proof (prove)
using this:
FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = (q1', q2')
FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (from_FSM M q1) \<union> FSM.inputs (from_FSM M q2)
FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (from_FSM M q1) \<union> FSM.outputs (from_FSM M q2)
FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (from_FSM M q1) \<times> FSM.states (from_FSM M q2)

goal (1 subgoal):
 1. (FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = (FSM.initial (from_FSM M q1'), FSM.initial (from_FSM M q2')) &&& FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (from_FSM M q1') \<times> FSM.states (from_FSM M q2')) &&& FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (from_FSM M q1') \<union> FSM.inputs (from_FSM M q2') &&& FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (from_FSM M q1') \<union> FSM.outputs (from_FSM M q2') &&& FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
[PROOF STEP]
unfolding product_transitions_def
[PROOF STATE]
proof (prove)
using this:
FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = (q1', q2')
FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (from_FSM M q1) \<union> FSM.inputs (from_FSM M q2)
FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (from_FSM M q1) \<union> FSM.outputs (from_FSM M q2)
FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions (from_FSM M q1) \<and> (qB, x, y, qB') \<in> FSM.transitions (from_FSM M q2)}
FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (from_FSM M q1) \<times> FSM.states (from_FSM M q2)

goal (1 subgoal):
 1. (FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = (FSM.initial (from_FSM M q1'), FSM.initial (from_FSM M q2')) &&& FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (from_FSM M q1') \<times> FSM.states (from_FSM M q2')) &&& FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (from_FSM M q1') \<union> FSM.inputs (from_FSM M q2') &&& FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (from_FSM M q1') \<union> FSM.outputs (from_FSM M q2') &&& FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions (from_FSM M q1') \<and> (qB, x, y, qB') \<in> FSM.transitions (from_FSM M q2')}
[PROOF STEP]
unfolding from_FSM_simps[OF \<open>q1' \<in> states M\<close>] from_FSM_simps[OF \<open>q2' \<in> states M\<close>]
[PROOF STATE]
proof (prove)
using this:
FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = (q1', q2')
FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (from_FSM M q1) \<union> FSM.inputs (from_FSM M q2)
FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (from_FSM M q1) \<union> FSM.outputs (from_FSM M q2)
FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions (from_FSM M q1) \<and> (qB, x, y, qB') \<in> FSM.transitions (from_FSM M q2)}
FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (from_FSM M q1) \<times> FSM.states (from_FSM M q2)

goal (1 subgoal):
 1. (FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = (q1', q2') &&& FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states M \<times> FSM.states M) &&& FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs M \<union> FSM.inputs M &&& FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs M \<union> FSM.outputs M &&& FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions M \<and> (qB, x, y, qB') \<in> FSM.transitions M}
[PROOF STEP]
unfolding from_FSM_simps[OF \<open>q1 \<in> states M\<close>] from_FSM_simps[OF \<open>q2 \<in> states M\<close>]
[PROOF STATE]
proof (prove)
using this:
FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = (q1', q2')
FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs M \<union> FSM.inputs M
FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs M \<union> FSM.outputs M
FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions M \<and> (qB, x, y, qB') \<in> FSM.transitions M}
FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states M \<times> FSM.states M

goal (1 subgoal):
 1. (FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = (q1', q2') &&& FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states M \<times> FSM.states M) &&& FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs M \<union> FSM.inputs M &&& FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs M \<union> FSM.outputs M &&& FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions M \<and> (qB, x, y, qB') \<in> FSM.transitions M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.initial (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))

goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2') = Product_FSM.product (from_FSM M q1') (from_FSM M q2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.initial (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FSM.initial (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.initial (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.states (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.states (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.inputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.inputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.outputs (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.outputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
FSM.transitions (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))

goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2') = Product_FSM.product (from_FSM M q1') (from_FSM M q2')
[PROOF STEP]
by (transfer; auto)
[PROOF STATE]
proof (state)
this:
from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2') = Product_FSM.product (from_FSM M q1') (from_FSM M q2')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma from_FSM_product_inputs :
  assumes "q1 \<in> states M" and "q2 \<in> states M"
shows "(inputs (product (from_FSM M q1) (from_FSM M q2))) = (inputs M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = FSM.inputs M
[PROOF STEP]
by (simp add: assms(1) assms(2))


[STATEMENT]
lemma from_FSM_product_outputs :
  assumes "q1 \<in> states M" and "q2 \<in> states M"
shows "(outputs (product (from_FSM M q1) (from_FSM M q2))) = (outputs M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.outputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = FSM.outputs M
[PROOF STEP]
by (simp add: assms(1) assms(2))


[STATEMENT]
lemma from_FSM_product_initial :
  assumes "q1 \<in> states M" and "q2 \<in> states M"
shows "initial (product (from_FSM M q1) (from_FSM M q2)) = (q1,q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = (q1, q2)
[PROOF STEP]
by (simp add: assms(1) assms(2))


[STATEMENT]
lemma product_from_reachable_next' :
  assumes "t \<in> transitions (product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t))))"
  and     "fst (t_source t) \<in> states M"
  and     "snd (t_source t) \<in> states M"
shows "(from_FSM (product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t),snd (t_target t))) = (product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t)) = Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t)) = Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))
[PROOF STEP]
have "((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t

goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t)) = Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t

goal (1 subgoal):
 1. from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t)) = Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))
[PROOF STEP]
by (metis (no_types) assms(1) assms(2) assms(3) product_from_reachable_next)
[PROOF STATE]
proof (state)
this:
from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t)) = Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_from_reachable_next'_path :
  assumes "t \<in> transitions (product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t))))"
  and     "fst (t_source t) \<in> states M"
  and     "snd (t_source t) \<in> states M"
  shows "path (from_FSM (product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t),snd (t_target t))) (fst (t_target t),snd (t_target t)) p = path (product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t),snd (t_target t)) p"
    (is "path ?P1 ?q p = path ?P2 ?q p")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) p = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) p = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) p
[PROOF STEP]
have i1: "initial ?P1 = ?q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) = (fst (t_target t), snd (t_target t))
[PROOF STEP]
using assms(1) fsm_transition_target
[PROOF STATE]
proof (prove)
using this:
t \<in> FSM.transitions (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t))))
?t \<in> FSM.transitions ?M \<Longrightarrow> t_target ?t \<in> FSM.states ?M

goal (1 subgoal):
 1. FSM.initial (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) = (fst (t_target t), snd (t_target t))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
FSM.initial (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) = (fst (t_target t), snd (t_target t))

goal (1 subgoal):
 1. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) p = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) p
[PROOF STEP]
have i2: "initial ?P2 = ?q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) = (fst (t_target t), snd (t_target t))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. FSM.initial (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) = (fst (t_target t), snd (t_target t))
[PROOF STEP]
have "((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t

goal (1 subgoal):
 1. FSM.initial (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) = (fst (t_target t), snd (t_target t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t

goal (1 subgoal):
 1. FSM.initial (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) = (fst (t_target t), snd (t_target t))
[PROOF STEP]
by (metis (no_types) assms(1) assms(2) assms(3) i1 product_from_reachable_next)
[PROOF STATE]
proof (state)
this:
FSM.initial (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) = (fst (t_target t), snd (t_target t))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
FSM.initial (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) = (fst (t_target t), snd (t_target t))

goal (1 subgoal):
 1. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) p = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) p
[PROOF STEP]
have h12: "transitions ?P1 = transitions ?P2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.transitions (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) = FSM.transitions (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t))))
[PROOF STEP]
using product_from_reachable_next'[OF assms]
[PROOF STATE]
proof (prove)
using this:
from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t)) = Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))

goal (1 subgoal):
 1. FSM.transitions (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) = FSM.transitions (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
FSM.transitions (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) = FSM.transitions (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t))))

goal (1 subgoal):
 1. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) p = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) p = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) p
[PROOF STEP]
proof (induction p rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) [] = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) []
 2. \<And>x xs. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) xs = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) xs \<Longrightarrow> path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) (xs @ [x]) = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) (xs @ [x])
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) [] = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) []
 2. \<And>x xs. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) xs = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) xs \<Longrightarrow> path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) (xs @ [x]) = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) (xs @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) [] = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) []
[PROOF STEP]
by (metis (full_types) i1 i2 fsm_initial path.nil)
[PROOF STATE]
proof (state)
this:
path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) [] = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) []

goal (1 subgoal):
 1. \<And>x xs. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) xs = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) xs \<Longrightarrow> path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) (xs @ [x]) = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) (xs @ [x])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) xs = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) xs \<Longrightarrow> path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) (xs @ [x]) = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) (xs @ [x])
[PROOF STEP]
case (snoc t p)
[PROOF STATE]
proof (state)
this:
path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) p = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) p

goal (1 subgoal):
 1. \<And>x xs. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) xs = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) xs \<Longrightarrow> path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) (xs @ [x]) = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) (xs @ [x])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) (p @ [t]) = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) (p @ [t])
[PROOF STEP]
by (metis h12 path_append_transition path_append_transition_elim(1) path_append_transition_elim(2) path_append_transition_elim(3) snoc.IH)
[PROOF STATE]
proof (state)
this:
path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) (p @ [t]) = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) (p @ [t])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
path (from_FSM (Product_FSM.product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t)))) (fst (t_target t), snd (t_target t))) (fst (t_target t), snd (t_target t)) p = path (Product_FSM.product (from_FSM M (fst (t_target t))) (from_FSM M (snd (t_target t)))) (fst (t_target t), snd (t_target t)) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_from_transition:
  assumes "(q1',q2') \<in> states (product (from_FSM M q1) (from_FSM M q2))"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
shows "transitions (product (from_FSM M q1') (from_FSM M q2')) = transitions (product (from_FSM M q1) (from_FSM M q2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
have "q1' \<in> states M" and "q2' \<in> states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q1' \<in> FSM.states M &&& q2' \<in> FSM.states M
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
(q1', q2') \<in> FSM.states (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. q1' \<in> FSM.states M &&& q2' \<in> FSM.states M
[PROOF STEP]
unfolding product_simps from_FSM_simps[OF assms(2)] from_FSM_simps[OF assms(3)]
[PROOF STATE]
proof (prove)
using this:
(q1', q2') \<in> FSM.states M \<times> 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. FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
unfolding product_transitions_def from_FSM_simps[OF \<open>q1 \<in> states M\<close>] from_FSM_simps[OF \<open>q1' \<in> states M\<close>] from_FSM_simps[OF \<open>q2 \<in> states M\<close>] from_FSM_simps[OF \<open>q2' \<in> states M\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions M \<and> (qB, x, y, qB') \<in> FSM.transitions M} = {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions M \<and> (qB, x, y, qB') \<in> FSM.transitions M}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_from_path:
  assumes "(q1',q2') \<in> states (product (from_FSM M q1) (from_FSM M q2))"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
      and "path (product (from_FSM M q1') (from_FSM M q2')) (q1',q2') p"
    shows "path (product (from_FSM M q1) (from_FSM M q2)) (q1',q2') p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2') p
[PROOF STEP]
by (metis (no_types, lifting) assms(1) assms(2) assms(3) assms(4) from_FSM_path_initial from_FSM_simps(5) from_from mem_Sigma_iff product_path product_simps(2))


[STATEMENT]
lemma product_from_path_previous :
  assumes "path (product (from_FSM M (fst (t_target t)))
                         (from_FSM M (snd (t_target t))))
                (t_target t) p"                                           (is "path ?Pt (t_target t) p")
      and "t \<in> transitions (product (from_FSM M q1) (from_FSM M q2))"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
    shows "path (product (from_FSM M q1) (from_FSM M q2)) (t_target t) p" (is "path ?P (t_target t) p")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (t_target t) p
[PROOF STEP]
by (metis assms(1) assms(2) assms(3) assms(4) fsm_transition_target prod.collapse product_from_path)


[STATEMENT]
lemma product_from_transition_shared_state :
  assumes "t \<in> transitions (product (from_FSM M q1') (from_FSM M q2'))"
  and     "(q1',q2') \<in> states (product (from_FSM M q1) (from_FSM M q2))"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
shows "t \<in> transitions (product (from_FSM M q1) (from_FSM M q2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
by (metis assms product_from_transition)


[STATEMENT]
lemma product_from_not_completely_specified :
  assumes "\<not> completely_specified_state (product (from_FSM M q1) (from_FSM M q2)) (q1',q2')"
  and     "(q1',q2') \<in> states (product (from_FSM M q1) (from_FSM M q2))"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
    shows  "\<not> completely_specified_state (product (from_FSM M q1') (from_FSM M q2')) (q1',q2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')
[PROOF STEP]
have "q1' \<in> states M" and "q2' \<in> states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q1' \<in> FSM.states M &&& q2' \<in> FSM.states M
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(q1', q2') \<in> FSM.states (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. q1' \<in> FSM.states M &&& q2' \<in> FSM.states M
[PROOF STEP]
unfolding product_simps from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)]
[PROOF STATE]
proof (prove)
using this:
(q1', q2') \<in> FSM.states M \<times> 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. \<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')
[PROOF STEP]
using from_FSM_product_inputs[OF assms(3) assms(4)]
[PROOF STATE]
proof (prove)
using this:
FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = FSM.inputs M

goal (1 subgoal):
 1. \<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')
[PROOF STEP]
using from_FSM_product_inputs[OF \<open>q1' \<in> states M\<close> \<open>q2' \<in> states M\<close> ]
[PROOF STATE]
proof (prove)
using this:
FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = FSM.inputs M
FSM.inputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.inputs M

goal (1 subgoal):
 1. \<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = FSM.inputs M; FSM.inputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.inputs M\<rbrakk> \<Longrightarrow> \<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')
[PROOF STEP]
have "FSM.transitions (Product_FSM.product (FSM.from_FSM M q1') (FSM.from_FSM M q2')) = FSM.transitions (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
by (metis (no_types) \<open>(q1', q2') \<in> FSM.states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))\<close> assms(3) assms(4) product_from_transition)
[PROOF STATE]
proof (state)
this:
FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. \<lbrakk>FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = FSM.inputs M; FSM.inputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.inputs M\<rbrakk> \<Longrightarrow> \<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. \<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')
[PROOF STEP]
using \<open>FSM.inputs (Product_FSM.product (FSM.from_FSM M q1') (FSM.from_FSM M q2')) = FSM.inputs M\<close> \<open>FSM.inputs (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) = FSM.inputs M\<close> \<open>\<not> completely_specified_state (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) (q1', q2')\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.transitions (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.inputs (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) = FSM.inputs M
FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = FSM.inputs M
\<not> completely_specified_state (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')

goal (1 subgoal):
 1. \<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> completely_specified_state (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma from_product_initial_paths_ex :
  assumes "q1 \<in> states M"
  and     "q2 \<in> states M"
shows  "(\<exists>p1 p2.
         path (from_FSM M q1) (initial (from_FSM M q1)) p1 \<and>
         path (from_FSM M q2) (initial (from_FSM M q2)) p2 \<and>
         target (initial (from_FSM M q1)) p1 = q1 \<and>
         target (initial (from_FSM M q2)) p2 = q2 \<and> p_io p1 = p_io p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p1 p2. path (from_FSM M q1) (FSM.initial (from_FSM M q1)) p1 \<and> path (from_FSM M q2) (FSM.initial (from_FSM M q2)) p2 \<and> target (FSM.initial (from_FSM M q1)) p1 = q1 \<and> target (FSM.initial (from_FSM M q2)) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p1 p2. path (from_FSM M q1) (FSM.initial (from_FSM M q1)) p1 \<and> path (from_FSM M q2) (FSM.initial (from_FSM M q2)) p2 \<and> target (FSM.initial (from_FSM M q1)) p1 = q1 \<and> target (FSM.initial (from_FSM M q2)) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
have "path (from_FSM M q1) (initial (from_FSM M q1)) []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (from_FSM M q1) (FSM.initial (from_FSM M q1)) []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path (from_FSM M q1) (FSM.initial (from_FSM M q1)) []

goal (1 subgoal):
 1. \<exists>p1 p2. path (from_FSM M q1) (FSM.initial (from_FSM M q1)) p1 \<and> path (from_FSM M q2) (FSM.initial (from_FSM M q2)) p2 \<and> target (FSM.initial (from_FSM M q1)) p1 = q1 \<and> target (FSM.initial (from_FSM M q2)) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path (from_FSM M q1) (FSM.initial (from_FSM M q1)) []

goal (1 subgoal):
 1. \<exists>p1 p2. path (from_FSM M q1) (FSM.initial (from_FSM M q1)) p1 \<and> path (from_FSM M q2) (FSM.initial (from_FSM M q2)) p2 \<and> target (FSM.initial (from_FSM M q1)) p1 = q1 \<and> target (FSM.initial (from_FSM M q2)) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
have "path (from_FSM M q2) (initial (from_FSM M q2)) []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (from_FSM M q2) (FSM.initial (from_FSM M q2)) []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path (from_FSM M q2) (FSM.initial (from_FSM M q2)) []

goal (1 subgoal):
 1. \<exists>p1 p2. path (from_FSM M q1) (FSM.initial (from_FSM M q1)) p1 \<and> path (from_FSM M q2) (FSM.initial (from_FSM M q2)) p2 \<and> target (FSM.initial (from_FSM M q1)) p1 = q1 \<and> target (FSM.initial (from_FSM M q2)) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path (from_FSM M q2) (FSM.initial (from_FSM M q2)) []

goal (1 subgoal):
 1. \<exists>p1 p2. path (from_FSM M q1) (FSM.initial (from_FSM M q1)) p1 \<and> path (from_FSM M q2) (FSM.initial (from_FSM M q2)) p2 \<and> target (FSM.initial (from_FSM M q1)) p1 = q1 \<and> target (FSM.initial (from_FSM M q2)) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
have "
         target (initial (from_FSM M q1)) [] = q1 \<and>
         target (initial (from_FSM M q2)) [] = q2 \<and> p_io [] = p_io []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial (from_FSM M q1)) [] = q1 \<and> target (FSM.initial (from_FSM M q2)) [] = q2 \<and> p_io [] = p_io []
[PROOF STEP]
unfolding from_FSM_simps[OF assms(1)] from_FSM_simps[OF assms(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target q1 [] = q1 \<and> target q2 [] = q2 \<and> p_io [] = p_io []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target (FSM.initial (from_FSM M q1)) [] = q1 \<and> target (FSM.initial (from_FSM M q2)) [] = q2 \<and> p_io [] = p_io []

goal (1 subgoal):
 1. \<exists>p1 p2. path (from_FSM M q1) (FSM.initial (from_FSM M q1)) p1 \<and> path (from_FSM M q2) (FSM.initial (from_FSM M q2)) p2 \<and> target (FSM.initial (from_FSM M q1)) p1 = q1 \<and> target (FSM.initial (from_FSM M q2)) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path (from_FSM M q1) (FSM.initial (from_FSM M q1)) []
path (from_FSM M q2) (FSM.initial (from_FSM M q2)) []
target (FSM.initial (from_FSM M q1)) [] = q1 \<and> target (FSM.initial (from_FSM M q2)) [] = q2 \<and> p_io [] = p_io []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path (from_FSM M q1) (FSM.initial (from_FSM M q1)) []
path (from_FSM M q2) (FSM.initial (from_FSM M q2)) []
target (FSM.initial (from_FSM M q1)) [] = q1 \<and> target (FSM.initial (from_FSM M q2)) [] = q2 \<and> p_io [] = p_io []

goal (1 subgoal):
 1. \<exists>p1 p2. path (from_FSM M q1) (FSM.initial (from_FSM M q1)) p1 \<and> path (from_FSM M q2) (FSM.initial (from_FSM M q2)) p2 \<and> target (FSM.initial (from_FSM M q1)) p1 = q1 \<and> target (FSM.initial (from_FSM M q2)) p2 = q2 \<and> p_io p1 = p_io p2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p1 p2. path (from_FSM M q1) (FSM.initial (from_FSM M q1)) p1 \<and> path (from_FSM M q2) (FSM.initial (from_FSM M q2)) p2 \<and> target (FSM.initial (from_FSM M q1)) p1 = q1 \<and> target (FSM.initial (from_FSM M q2)) p2 = q2 \<and> p_io p1 = p_io p2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_observable :
  assumes "observable M1"
  and     "observable M2"
shows "observable (product M1 M2)" (is "observable ?P")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. observable (Product_FSM.product M1 M2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. observable (Product_FSM.product M1 M2)
[PROOF STEP]
have "\<And> t1 t2 . t1 \<in> transitions ?P \<Longrightarrow> t2 \<in> transitions ?P \<Longrightarrow> t_source t1 = t_source t2 \<Longrightarrow> t_input t1 = t_input t2 \<Longrightarrow> t_output t1 = t_output t2 \<Longrightarrow> t_target t1 = t_target t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions (Product_FSM.product M1 M2); t2 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source t1 = t_source t2; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions (Product_FSM.product M1 M2); t2 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source t1 = t_source t2; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
fix t1 t2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions (Product_FSM.product M1 M2); t2 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source t1 = t_source t2; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
assume "t1 \<in> transitions ?P" and "t2 \<in> transitions ?P" and "t_source t1 = t_source t2" and "t_input t1 = t_input t2" and "t_output t1 = t_output t2"
[PROOF STATE]
proof (state)
this:
t1 \<in> FSM.transitions (Product_FSM.product M1 M2)
t2 \<in> FSM.transitions (Product_FSM.product M1 M2)
t_source t1 = t_source t2
t_input t1 = t_input t2
t_output t1 = t_output t2

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions (Product_FSM.product M1 M2); t2 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source t1 = t_source t2; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
let ?t1L = "(fst (t_source t1), t_input t1, t_output t1, fst (t_target t1))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions (Product_FSM.product M1 M2); t2 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source t1 = t_source t2; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
let ?t1R = "(snd (t_source t1), t_input t1, t_output t1, snd (t_target t1))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions (Product_FSM.product M1 M2); t2 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source t1 = t_source t2; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
let ?t2L = "(fst (t_source t2), t_input t2, t_output t2, fst (t_target t2))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions (Product_FSM.product M1 M2); t2 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source t1 = t_source t2; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
let ?t2R = "(snd (t_source t2), t_input t2, t_output t2, snd (t_target t2))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions (Product_FSM.product M1 M2); t2 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source t1 = t_source t2; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
have "t_target ?t1L = t_target ?t2L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_target (fst (t_source t1), t_input t1, t_output t1, fst (t_target t1)) = t_target (fst (t_source t2), t_input t2, t_output t2, fst (t_target t2))
[PROOF STEP]
using product_transition_split(1)[OF \<open>t1 \<in> transitions ?P\<close>]
            product_transition_split(1)[OF \<open>t2 \<in> transitions ?P\<close>]
            \<open>observable M1\<close>
            \<open>t_source t1 = t_source t2\<close>
            \<open>t_input t1 = t_input t2\<close>
            \<open>t_output t1 = t_output t2\<close>
[PROOF STATE]
proof (prove)
using this:
(fst (t_source t1), t_input t1, t_output t1, fst (t_target t1)) \<in> FSM.transitions M1
(fst (t_source t2), t_input t2, t_output t2, fst (t_target t2)) \<in> FSM.transitions M1
observable M1
t_source t1 = t_source t2
t_input t1 = t_input t2
t_output t1 = t_output t2

goal (1 subgoal):
 1. t_target (fst (t_source t1), t_input t1, t_output t1, fst (t_target t1)) = t_target (fst (t_source t2), t_input t2, t_output t2, fst (t_target t2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t_target (fst (t_source t1), t_input t1, t_output t1, fst (t_target t1)) = t_target (fst (t_source t2), t_input t2, t_output t2, fst (t_target t2))

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions (Product_FSM.product M1 M2); t2 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source t1 = t_source t2; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t_target (fst (t_source t1), t_input t1, t_output t1, fst (t_target t1)) = t_target (fst (t_source t2), t_input t2, t_output t2, fst (t_target t2))

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions (Product_FSM.product M1 M2); t2 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source t1 = t_source t2; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
have "t_target ?t1R = t_target ?t2R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_target (snd (t_source t1), t_input t1, t_output t1, snd (t_target t1)) = t_target (snd (t_source t2), t_input t2, t_output t2, snd (t_target t2))
[PROOF STEP]
using product_transition_split(2)[OF \<open>t1 \<in> transitions ?P\<close>]
            product_transition_split(2)[OF \<open>t2 \<in> transitions ?P\<close>]
            \<open>observable M2\<close>
            \<open>t_source t1 = t_source t2\<close>
            \<open>t_input t1 = t_input t2\<close>
            \<open>t_output t1 = t_output t2\<close>
[PROOF STATE]
proof (prove)
using this:
(snd (t_source t1), t_input t1, t_output t1, snd (t_target t1)) \<in> FSM.transitions M2
(snd (t_source t2), t_input t2, t_output t2, snd (t_target t2)) \<in> FSM.transitions M2
observable M2
t_source t1 = t_source t2
t_input t1 = t_input t2
t_output t1 = t_output t2

goal (1 subgoal):
 1. t_target (snd (t_source t1), t_input t1, t_output t1, snd (t_target t1)) = t_target (snd (t_source t2), t_input t2, t_output t2, snd (t_target t2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t_target (snd (t_source t1), t_input t1, t_output t1, snd (t_target t1)) = t_target (snd (t_source t2), t_input t2, t_output t2, snd (t_target t2))

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>t1 \<in> FSM.transitions (Product_FSM.product M1 M2); t2 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source t1 = t_source t2; t_input t1 = t_input t2; t_output t1 = t_output t2\<rbrakk> \<Longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t_target (fst (t_source t1), t_input t1, t_output t1, fst (t_target t1)) = t_target (fst (t_source t2), t_input t2, t_output t2, fst (t_target t2))
t_target (snd (t_source t1), t_input t1, t_output t1, snd (t_target t1)) = t_target (snd (t_source t2), t_input t2, t_output t2, snd (t_target t2))
[PROOF STEP]
show "t_target t1 = t_target t2"
[PROOF STATE]
proof (prove)
using this:
t_target (fst (t_source t1), t_input t1, t_output t1, fst (t_target t1)) = t_target (fst (t_source t2), t_input t2, t_output t2, fst (t_target t2))
t_target (snd (t_source t1), t_input t1, t_output t1, snd (t_target t1)) = t_target (snd (t_source t2), t_input t2, t_output t2, snd (t_target t2))

goal (1 subgoal):
 1. t_target t1 = t_target t2
[PROOF STEP]
by (metis prod.exhaust_sel snd_conv)
[PROOF STATE]
proof (state)
this:
t_target t1 = t_target t2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?t1.0 \<in> FSM.transitions (Product_FSM.product M1 M2); ?t2.0 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source ?t1.0 = t_source ?t2.0; t_input ?t1.0 = t_input ?t2.0; t_output ?t1.0 = t_output ?t2.0\<rbrakk> \<Longrightarrow> t_target ?t1.0 = t_target ?t2.0

goal (1 subgoal):
 1. observable (Product_FSM.product M1 M2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?t1.0 \<in> FSM.transitions (Product_FSM.product M1 M2); ?t2.0 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source ?t1.0 = t_source ?t2.0; t_input ?t1.0 = t_input ?t2.0; t_output ?t1.0 = t_output ?t2.0\<rbrakk> \<Longrightarrow> t_target ?t1.0 = t_target ?t2.0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t1.0 \<in> FSM.transitions (Product_FSM.product M1 M2); ?t2.0 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source ?t1.0 = t_source ?t2.0; t_input ?t1.0 = t_input ?t2.0; t_output ?t1.0 = t_output ?t2.0\<rbrakk> \<Longrightarrow> t_target ?t1.0 = t_target ?t2.0

goal (1 subgoal):
 1. observable (Product_FSM.product M1 M2)
[PROOF STEP]
unfolding observable.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t1.0 \<in> FSM.transitions (Product_FSM.product M1 M2); ?t2.0 \<in> FSM.transitions (Product_FSM.product M1 M2); t_source ?t1.0 = t_source ?t2.0; t_input ?t1.0 = t_input ?t2.0; t_output ?t1.0 = t_output ?t2.0\<rbrakk> \<Longrightarrow> t_target ?t1.0 = t_target ?t2.0

goal (1 subgoal):
 1. \<forall>t1\<in>FSM.transitions (Product_FSM.product M1 M2). \<forall>t2\<in>FSM.transitions (Product_FSM.product M1 M2). t_source t1 = t_source t2 \<and> t_input t1 = t_input t2 \<and> t_output t1 = t_output t2 \<longrightarrow> t_target t1 = t_target t2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
observable (Product_FSM.product M1 M2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_observable_self_transitions :
  assumes "q \<in> reachable_states (product M M)"
  and     "observable M"
shows "fst q = snd q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst q = snd q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst q = snd q
[PROOF STEP]
let ?P = "product M M"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst q = snd q
[PROOF STEP]
have "\<And> p . path ?P (initial ?P) p \<Longrightarrow> fst (target (initial ?P) p) = snd (target (initial ?P) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) p) = snd (target (FSM.initial (Product_FSM.product M M)) p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) p) = snd (target (FSM.initial (Product_FSM.product M M)) p)
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) p) = snd (target (FSM.initial (Product_FSM.product M M)) p)
[PROOF STEP]
assume "path ?P (initial ?P) p"
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p

goal (1 subgoal):
 1. \<And>p. path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) p) = snd (target (FSM.initial (Product_FSM.product M M)) p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p
[PROOF STEP]
show "fst (target (initial ?P) p) = snd (target (initial ?P) p)"
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p

goal (1 subgoal):
 1. fst (target (FSM.initial (Product_FSM.product M M)) p) = snd (target (FSM.initial (Product_FSM.product M M)) p)
[PROOF STEP]
proof (induction p rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) [] \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) []) = snd (target (FSM.initial (Product_FSM.product M M)) [])
 2. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) []

goal (2 subgoals):
 1. path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) [] \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) []) = snd (target (FSM.initial (Product_FSM.product M M)) [])
 2. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) []

goal (1 subgoal):
 1. fst (target (FSM.initial (Product_FSM.product M M)) []) = snd (target (FSM.initial (Product_FSM.product M M)) [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (target (FSM.initial (Product_FSM.product M M)) []) = snd (target (FSM.initial (Product_FSM.product M M)) [])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
case (snoc t p)
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) p) = snd (target (FSM.initial (Product_FSM.product M M)) p)
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (p @ [t])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
have "path ?P (initial ?P) p" and "path ?P (target (initial ?P) p) [t]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p &&& path (Product_FSM.product M M) (target (FSM.initial (Product_FSM.product M M)) p) [t]
[PROOF STEP]
using path_append_elim[of ?P "initial ?P" p "[t]", OF \<open>path (product M M) (initial (product M M)) (p @ [t])\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p; path (Product_FSM.product M M) (target (FSM.initial (Product_FSM.product M M)) p) [t]\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p &&& path (Product_FSM.product M M) (target (FSM.initial (Product_FSM.product M M)) p) [t]
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p
path (Product_FSM.product M M) (target (FSM.initial (Product_FSM.product M M)) p) [t]

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p
path (Product_FSM.product M M) (target (FSM.initial (Product_FSM.product M M)) p) [t]
[PROOF STEP]
have "t \<in> transitions ?P"
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p
path (Product_FSM.product M M) (target (FSM.initial (Product_FSM.product M M)) p) [t]

goal (1 subgoal):
 1. t \<in> FSM.transitions (Product_FSM.product M M)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> FSM.transitions (Product_FSM.product M M)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
have "t_source t = target (initial ?P) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_source t = target (FSM.initial (Product_FSM.product M M)) p
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (p @ [t])

goal (1 subgoal):
 1. t_source t = target (FSM.initial (Product_FSM.product M M)) p
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
t_source t = target (FSM.initial (Product_FSM.product M M)) p

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
let ?t1 = "(fst (t_source t), t_input t, t_output t, fst (t_target t))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
let ?t2 = "(snd (t_source t), t_input t, t_output t, snd (t_target t))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
have "?t1 \<in> transitions M" and "?t2 \<in> transitions M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions M &&& (snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions M
[PROOF STEP]
using product_transition_split[OF \<open>t \<in> transitions ?P\<close>]
[PROOF STATE]
proof (prove)
using this:
(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions M
(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions M

goal (1 subgoal):
 1. (fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions M &&& (snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions M
(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions M

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions M
(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions M

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
have "t_source ?t1 = t_source ?t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_source (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_source (snd (t_source t), t_input t, t_output t, snd (t_target t))
[PROOF STEP]
using \<open>t_source t = target (initial ?P) p\<close> snoc.IH[OF \<open>path ?P (initial ?P) p\<close>]
[PROOF STATE]
proof (prove)
using this:
t_source t = target (FSM.initial (Product_FSM.product M M)) p
fst (target (FSM.initial (Product_FSM.product M M)) p) = snd (target (FSM.initial (Product_FSM.product M M)) p)

goal (1 subgoal):
 1. t_source (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_source (snd (t_source t), t_input t, t_output t, snd (t_target t))
[PROOF STEP]
by (metis fst_conv)
[PROOF STATE]
proof (state)
this:
t_source (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_source (snd (t_source t), t_input t, t_output t, snd (t_target t))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t_source (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_source (snd (t_source t), t_input t, t_output t, snd (t_target t))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
have "t_input ?t1 = t_input ?t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_input (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_input (snd (t_source t), t_input t, t_output t, snd (t_target t))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t_input (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_input (snd (t_source t), t_input t, t_output t, snd (t_target t))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t_input (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_input (snd (t_source t), t_input t, t_output t, snd (t_target t))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
have "t_output ?t1 = t_output ?t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_output (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_output (snd (t_source t), t_input t, t_output t, snd (t_target t))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t_output (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_output (snd (t_source t), t_input t, t_output t, snd (t_target t))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions M
(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions M
t_source (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_source (snd (t_source t), t_input t, t_output t, snd (t_target t))
t_input (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_input (snd (t_source t), t_input t, t_output t, snd (t_target t))
t_output (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_output (snd (t_source t), t_input t, t_output t, snd (t_target t))
[PROOF STEP]
have "t_target ?t1 = t_target ?t2"
[PROOF STATE]
proof (prove)
using this:
(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions M
(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions M
t_source (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_source (snd (t_source t), t_input t, t_output t, snd (t_target t))
t_input (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_input (snd (t_source t), t_input t, t_output t, snd (t_target t))
t_output (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_output (snd (t_source t), t_input t, t_output t, snd (t_target t))

goal (1 subgoal):
 1. t_target (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_target (snd (t_source t), t_input t, t_output t, snd (t_target t))
[PROOF STEP]
using \<open>observable M\<close>
[PROOF STATE]
proof (prove)
using this:
(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions M
(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions M
t_source (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_source (snd (t_source t), t_input t, t_output t, snd (t_target t))
t_input (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_input (snd (t_source t), t_input t, t_output t, snd (t_target t))
t_output (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_output (snd (t_source t), t_input t, t_output t, snd (t_target t))
observable M

goal (1 subgoal):
 1. t_target (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_target (snd (t_source t), t_input t, t_output t, snd (t_target t))
[PROOF STEP]
unfolding observable.simps
[PROOF STATE]
proof (prove)
using this:
(fst (t_source t), t_input t, t_output t, fst (t_target t)) \<in> FSM.transitions M
(snd (t_source t), t_input t, t_output t, snd (t_target t)) \<in> FSM.transitions M
t_source (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_source (snd (t_source t), t_input t, t_output t, snd (t_target t))
t_input (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_input (snd (t_source t), t_input t, t_output t, snd (t_target t))
t_output (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_output (snd (t_source t), t_input t, t_output t, snd (t_target t))
\<forall>t1\<in>FSM.transitions M. \<forall>t2\<in>FSM.transitions M. t_source t1 = t_source t2 \<and> t_input t1 = t_input t2 \<and> t_output t1 = t_output t2 \<longrightarrow> t_target t1 = t_target t2

goal (1 subgoal):
 1. t_target (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_target (snd (t_source t), t_input t, t_output t, snd (t_target t))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t_target (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_target (snd (t_source t), t_input t, t_output t, snd (t_target t))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t_target (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_target (snd (t_source t), t_input t, t_output t, snd (t_target t))
[PROOF STEP]
have "fst (t_target t) = snd (t_target t)"
[PROOF STATE]
proof (prove)
using this:
t_target (fst (t_source t), t_input t, t_output t, fst (t_target t)) = t_target (snd (t_source t), t_input t, t_output t, snd (t_target t))

goal (1 subgoal):
 1. fst (t_target t) = snd (t_target t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (t_target t) = snd (t_target t)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) xs \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) xs) = snd (target (FSM.initial (Product_FSM.product M M)) xs); path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) (xs @ [x])\<rbrakk> \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) (xs @ [x])) = snd (target (FSM.initial (Product_FSM.product M M)) (xs @ [x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (t_target t) = snd (t_target t)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fst (t_target t) = snd (t_target t)

goal (1 subgoal):
 1. fst (target (FSM.initial (Product_FSM.product M M)) (p @ [t])) = snd (target (FSM.initial (Product_FSM.product M M)) (p @ [t]))
[PROOF STEP]
unfolding target.simps visited_states.simps
[PROOF STATE]
proof (prove)
using this:
fst (t_target t) = snd (t_target t)

goal (1 subgoal):
 1. fst (last (FSM.initial (Product_FSM.product M M) # map t_target (p @ [t]))) = snd (last (FSM.initial (Product_FSM.product M M) # map t_target (p @ [t])))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (t_target t) = snd (t_target t) \<Longrightarrow> fst (last (FSM.initial (Product_FSM.product M M) # map t_target (p @ [t]))) = snd (last (FSM.initial (Product_FSM.product M M) # map t_target (p @ [t])))
[PROOF STEP]
show "fst (last (initial (product M M) # map t_target (p @ [t]))) = snd (last (initial (product M M) # map t_target (p @ [t])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (last (FSM.initial (Product_FSM.product M M) # map t_target (p @ [t]))) = snd (last (FSM.initial (Product_FSM.product M M) # map t_target (p @ [t])))
[PROOF STEP]
using \<open>fst (t_target t) = snd (t_target t)\<close> last_map last_snoc length_append_singleton length_map
[PROOF STATE]
proof (prove)
using this:
fst (t_target t) = snd (t_target t)
?xs \<noteq> [] \<Longrightarrow> last (map ?f ?xs) = ?f (last ?xs)
last (?xs @ [?x]) = ?x
length (?xs @ [?x]) = Suc (length ?xs)
length (map ?f ?xs) = length ?xs

goal (1 subgoal):
 1. fst (last (FSM.initial (Product_FSM.product M M) # map t_target (p @ [t]))) = snd (last (FSM.initial (Product_FSM.product M M) # map t_target (p @ [t])))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst (last (FSM.initial (Product_FSM.product M M) # map t_target (p @ [t]))) = snd (last (FSM.initial (Product_FSM.product M M) # map t_target (p @ [t])))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst (target (FSM.initial (Product_FSM.product M M)) (p @ [t])) = snd (target (FSM.initial (Product_FSM.product M M)) (p @ [t]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst (target (FSM.initial (Product_FSM.product M M)) p) = snd (target (FSM.initial (Product_FSM.product M M)) p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) ?p \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) ?p) = snd (target (FSM.initial (Product_FSM.product M M)) ?p)

goal (1 subgoal):
 1. fst q = snd q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) ?p \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) ?p) = snd (target (FSM.initial (Product_FSM.product M M)) ?p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) ?p \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) ?p) = snd (target (FSM.initial (Product_FSM.product M M)) ?p)

goal (1 subgoal):
 1. fst q = snd q
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) ?p \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) ?p) = snd (target (FSM.initial (Product_FSM.product M M)) ?p)
q \<in> reachable_states (Product_FSM.product M M)

goal (1 subgoal):
 1. fst q = snd q
[PROOF STEP]
unfolding reachable_states_def
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) ?p \<Longrightarrow> fst (target (FSM.initial (Product_FSM.product M M)) ?p) = snd (target (FSM.initial (Product_FSM.product M M)) ?p)
q \<in> {target (FSM.initial (Product_FSM.product M M)) p |p. path (Product_FSM.product M M) (FSM.initial (Product_FSM.product M M)) p}

goal (1 subgoal):
 1. fst q = snd q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst q = snd q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zip_path_eq_left :
  assumes "length xs1 = length xs2"
  and     "length xs2 = length ys1"
  and     "length ys1 = length ys2"
  and     "zip_path xs1 xs2 = zip_path ys1 ys2"
shows "xs1 = ys1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs1 = ys1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs1 = length xs2
length xs2 = length ys1
length ys1 = length ys2
zip_path xs1 xs2 = zip_path ys1 ys2

goal (1 subgoal):
 1. xs1 = ys1
[PROOF STEP]
by (induction xs1 xs2 ys1 ys2 rule: list_induct4; auto)


[STATEMENT]
lemma zip_path_eq_right :
  assumes "length xs1 = length xs2"
  and     "length xs2 = length ys1"
  and     "length ys1 = length ys2"
  and     "p_io xs2 = p_io ys2"
  and     "zip_path xs1 xs2 = zip_path ys1 ys2"
shows "xs2 = ys2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs2 = ys2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs1 = length xs2
length xs2 = length ys1
length ys1 = length ys2
p_io xs2 = p_io ys2
zip_path xs1 xs2 = zip_path ys1 ys2

goal (1 subgoal):
 1. xs2 = ys2
[PROOF STEP]
by (induction xs1 xs2 ys1 ys2 rule: list_induct4; auto)


[STATEMENT]
lemma zip_path_merge :
  "(zip_path (left_path p) (right_path p)) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zip_path (left_path p) (right_path p) = p
[PROOF STEP]
by (induction p; auto)