[STATEMENT]
lemma product_transitions_alt_def :
  "transitions (product A B) = {((t_source tA, t_source tB),t_input tA, t_output tA, (t_target tA, t_target tB)) | tA tB . tA \<in> transitions A \<and> tB \<in> transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}"
  (is "?T1 = ?T2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.transitions (Product_FSM.product A B) = {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. FSM.transitions (Product_FSM.product A B) = {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
have "\<And> t . t \<in> ?T1 \<Longrightarrow> t \<in> ?T2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> FSM.transitions (Product_FSM.product A B) \<Longrightarrow> t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> FSM.transitions (Product_FSM.product A B) \<Longrightarrow> t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
fix tt
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> FSM.transitions (Product_FSM.product A B) \<Longrightarrow> t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
assume "tt \<in> ?T1"
[PROOF STATE]
proof (state)
this:
tt \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. \<And>t. t \<in> FSM.transitions (Product_FSM.product A B) \<Longrightarrow> t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tt \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
obtain qA qB x y qA' qB' where "tt = ((qA,qB),x,y,(qA',qB'))" and "(qA,x,y,qA') \<in> transitions A" and "(qB,x,y,qB') \<in> transitions B"
[PROOF STATE]
proof (prove)
using this:
tt \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. (\<And>qA qB x y qA' qB'. \<lbrakk>tt = ((qA, qB), x, y, qA', qB'); (qA, x, y, qA') \<in> FSM.transitions A; (qB, x, y, qB') \<in> FSM.transitions B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding product_transitions_def
[PROOF STATE]
proof (prove)
using this:
tt \<in> {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions A \<and> (qB, x, y, qB') \<in> FSM.transitions B}

goal (1 subgoal):
 1. (\<And>qA qB x y qA' qB'. \<lbrakk>tt = ((qA, qB), x, y, qA', qB'); (qA, x, y, qA') \<in> FSM.transitions A; (qB, x, y, qB') \<in> FSM.transitions B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
tt = ((qA, qB), x, y, qA', qB')
(qA, x, y, qA') \<in> FSM.transitions A
(qB, x, y, qB') \<in> FSM.transitions B

goal (1 subgoal):
 1. \<And>t. t \<in> FSM.transitions (Product_FSM.product A B) \<Longrightarrow> t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tt = ((qA, qB), x, y, qA', qB')
(qA, x, y, qA') \<in> FSM.transitions A
(qB, x, y, qB') \<in> FSM.transitions B
[PROOF STEP]
have "((t_source (qA,x,y,qA'), t_source (qB,x,y,qB')),t_input (qA,x,y,qA'), t_output (qA,x,y,qA'), (t_target (qA,x,y,qA'), t_target (qB,x,y,qB'))) \<in> ?T2"
[PROOF STATE]
proof (prove)
using this:
tt = ((qA, qB), x, y, qA', qB')
(qA, x, y, qA') \<in> FSM.transitions A
(qB, x, y, qB') \<in> FSM.transitions B

goal (1 subgoal):
 1. ((t_source (qA, x, y, qA'), t_source (qB, x, y, qB')), t_input (qA, x, y, qA'), t_output (qA, x, y, qA'), t_target (qA, x, y, qA'), t_target (qB, x, y, qB')) \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((t_source (qA, x, y, qA'), t_source (qB, x, y, qB')), t_input (qA, x, y, qA'), t_output (qA, x, y, qA'), t_target (qA, x, y, qA'), t_target (qB, x, y, qB')) \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}

goal (1 subgoal):
 1. \<And>t. t \<in> FSM.transitions (Product_FSM.product A B) \<Longrightarrow> t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((t_source (qA, x, y, qA'), t_source (qB, x, y, qB')), t_input (qA, x, y, qA'), t_output (qA, x, y, qA'), t_target (qA, x, y, qA'), t_target (qB, x, y, qB')) \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
show "tt \<in> ?T2"
[PROOF STATE]
proof (prove)
using this:
((t_source (qA, x, y, qA'), t_source (qB, x, y, qB')), t_input (qA, x, y, qA'), t_output (qA, x, y, qA'), t_target (qA, x, y, qA'), t_target (qB, x, y, qB')) \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}

goal (1 subgoal):
 1. tt \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
unfolding \<open>tt = ((qA,qB),x,y,(qA',qB'))\<close> fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
((qA, qB), x, y, qA', qB') \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}

goal (1 subgoal):
 1. ((qA, qB), x, y, qA', qB') \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
tt \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?t \<in> FSM.transitions (Product_FSM.product A B) \<Longrightarrow> ?t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}

goal (1 subgoal):
 1. FSM.transitions (Product_FSM.product A B) = {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?t \<in> FSM.transitions (Product_FSM.product A B) \<Longrightarrow> ?t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}

goal (1 subgoal):
 1. FSM.transitions (Product_FSM.product A B) = {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
have "\<And> t . t \<in> ?T2 \<Longrightarrow> t \<in> ?T1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB} \<Longrightarrow> t \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB} \<Longrightarrow> t \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
fix tt
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB} \<Longrightarrow> t \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
assume "tt \<in> ?T2"
[PROOF STATE]
proof (state)
this:
tt \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}

goal (1 subgoal):
 1. \<And>t. t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB} \<Longrightarrow> t \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tt \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
obtain tA tB where "tt = ((t_source tA, t_source tB),t_input tA, t_output tA, (t_target tA, t_target tB))"
                        and "tA \<in> transitions A" and "tB \<in> transitions B" and "t_input tA = t_input tB" and "t_output tA = t_output tB"
[PROOF STATE]
proof (prove)
using this:
tt \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}

goal (1 subgoal):
 1. (\<And>tA tB. \<lbrakk>tt = ((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB); tA \<in> FSM.transitions A; tB \<in> FSM.transitions B; t_input tA = t_input tB; t_output tA = t_output tB\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
tt = ((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB)
tA \<in> FSM.transitions A
tB \<in> FSM.transitions B
t_input tA = t_input tB
t_output tA = t_output tB

goal (1 subgoal):
 1. \<And>t. t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB} \<Longrightarrow> t \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tt = ((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB)
tA \<in> FSM.transitions A
tB \<in> FSM.transitions B
t_input tA = t_input tB
t_output tA = t_output tB
[PROOF STEP]
have "(t_source tA, t_input tA, t_output tA, t_target tA) \<in> transitions A"
         and  "(t_source tB, t_input tA, t_output tA, t_target tB) \<in> transitions B"
[PROOF STATE]
proof (prove)
using this:
tt = ((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB)
tA \<in> FSM.transitions A
tB \<in> FSM.transitions B
t_input tA = t_input tB
t_output tA = t_output tB

goal (1 subgoal):
 1. (t_source tA, t_input tA, t_output tA, t_target tA) \<in> FSM.transitions A &&& (t_source tB, t_input tA, t_output tA, t_target tB) \<in> FSM.transitions B
[PROOF STEP]
by (metis prod.collapse)+
[PROOF STATE]
proof (state)
this:
(t_source tA, t_input tA, t_output tA, t_target tA) \<in> FSM.transitions A
(t_source tB, t_input tA, t_output tA, t_target tB) \<in> FSM.transitions B

goal (1 subgoal):
 1. \<And>t. t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB} \<Longrightarrow> t \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(t_source tA, t_input tA, t_output tA, t_target tA) \<in> FSM.transitions A
(t_source tB, t_input tA, t_output tA, t_target tB) \<in> FSM.transitions B
[PROOF STEP]
show "tt \<in> ?T1"
[PROOF STATE]
proof (prove)
using this:
(t_source tA, t_input tA, t_output tA, t_target tA) \<in> FSM.transitions A
(t_source tB, t_input tA, t_output tA, t_target tB) \<in> FSM.transitions B

goal (1 subgoal):
 1. tt \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
unfolding product_transitions_def \<open>tt = ((t_source tA, t_source tB),t_input tA, t_output tA, (t_target tA, t_target tB))\<close>
[PROOF STATE]
proof (prove)
using this:
(t_source tA, t_input tA, t_output tA, t_target tA) \<in> FSM.transitions A
(t_source tB, t_input tA, t_output tA, t_target tB) \<in> FSM.transitions B

goal (1 subgoal):
 1. ((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) \<in> {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions A \<and> (qB, x, y, qB') \<in> FSM.transitions B}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
tt \<in> FSM.transitions (Product_FSM.product A B)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB} \<Longrightarrow> ?t \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. FSM.transitions (Product_FSM.product A B) = {((t_source tA, t_source tB), t_input tA, t_output tA, t_target tA, t_target tB) |tA tB. tA \<in> FSM.transitions A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?t \<in> FSM.transitions (Product_FSM.product A B) \<Longrightarrow> ?t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
?t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB} \<Longrightarrow> ?t \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?t \<in> FSM.transitions (Product_FSM.product A B) \<Longrightarrow> ?t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB}
?t \<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 A \<and> tB \<in> FSM.transitions B \<and> t_input tA = t_input tB \<and> t_output tA = t_output tB} \<Longrightarrow> ?t \<in> FSM.transitions (Product_FSM.product A B)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zip_path_last : "length xs = length ys \<Longrightarrow> (zip_path (xs @ [x]) (ys @ [y])) = (zip_path xs ys)@(zip_path [x] [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ zip_path [x] [y]
[PROOF STEP]
by (induction xs ys rule: list_induct2; simp)


[STATEMENT]
lemma product_path_from_paths :
  assumes "path A (initial A) p1"
      and "path B (initial B) p2"
      and "p_io p1 = p_io p2"
    shows "path (product A B) (initial (product A B)) (zip_path p1 p2)"
      and "target (initial (product A B)) (zip_path p1 p2) = (target (initial A) p1, target (initial B) p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) &&& target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2)
 2. target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
have "initial (product A B) = (initial A, initial B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial (Product_FSM.product A B) = (FSM.initial A, FSM.initial B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.initial (Product_FSM.product A B) = (FSM.initial A, FSM.initial B)

goal (2 subgoals):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2)
 2. target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.initial (Product_FSM.product A B) = (FSM.initial A, FSM.initial B)
[PROOF STEP]
have "(initial A, initial B) \<in> states (product A B)"
[PROOF STATE]
proof (prove)
using this:
FSM.initial (Product_FSM.product A B) = (FSM.initial A, FSM.initial B)

goal (1 subgoal):
 1. (FSM.initial A, FSM.initial B) \<in> FSM.states (Product_FSM.product A B)
[PROOF STEP]
by (metis fsm_initial)
[PROOF STATE]
proof (state)
this:
(FSM.initial A, FSM.initial B) \<in> FSM.states (Product_FSM.product A B)

goal (2 subgoals):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2)
 2. target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
have "length p1 = length p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p1 = length p2
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
p_io p1 = p_io p2

goal (1 subgoal):
 1. length p1 = length p2
[PROOF STEP]
using map_eq_imp_length_eq
[PROOF STATE]
proof (prove)
using this:
p_io p1 = p_io p2
map ?f ?xs = map ?g ?ys \<Longrightarrow> length ?xs = length ?ys

goal (1 subgoal):
 1. length p1 = length p2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length p1 = length p2

goal (2 subgoals):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2)
 2. target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length p1 = length p2
[PROOF STEP]
have c: "path (product A B) (initial (product A B)) (zip_path p1 p2)
                \<and> target (initial (product A B)) (zip_path p1 p2) = (target (initial A) p1, target (initial B) p2)"
[PROOF STATE]
proof (prove)
using this:
length p1 = length p2

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length p1 = length p2
path A (FSM.initial A) p1
path B (FSM.initial B) p2
p_io p1 = p_io p2

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
proof (induction p1 p2 rule: rev_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>path A (FSM.initial A) []; path B (FSM.initial B) []; p_io [] = p_io []\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] []) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) []
path B (FSM.initial B) []
p_io [] = p_io []

goal (2 subgoals):
 1. \<lbrakk>path A (FSM.initial A) []; path B (FSM.initial B) []; p_io [] = p_io []\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] []) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path A (FSM.initial A) []
path B (FSM.initial B) []
p_io [] = p_io []
[PROOF STEP]
have "path (product A B) (initial (product A B)) (zip_path [] [])"
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) []
path B (FSM.initial B) []
p_io [] = p_io []

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] [])
[PROOF STEP]
using \<open>initial (product A B) = (initial A, initial B)\<close> \<open>(initial A, initial B) \<in> states (product A B)\<close>
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) []
path B (FSM.initial B) []
p_io [] = p_io []
FSM.initial (Product_FSM.product A B) = (FSM.initial A, FSM.initial B)
(FSM.initial A, FSM.initial B) \<in> FSM.states (Product_FSM.product A B)

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] [])
[PROOF STEP]
by (metis Nil_is_map_conv path.nil zip_Nil)
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] [])

goal (2 subgoals):
 1. \<lbrakk>path A (FSM.initial A) []; path B (FSM.initial B) []; p_io [] = p_io []\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] []) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] [])

goal (2 subgoals):
 1. \<lbrakk>path A (FSM.initial A) []; path B (FSM.initial B) []; p_io [] = p_io []\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] []) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "target (initial (product A B)) (zip_path [] []) = (target (initial A) [], target (initial B) [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])
[PROOF STEP]
using \<open>initial (product A B) = (initial A, initial B)\<close>
[PROOF STATE]
proof (prove)
using this:
FSM.initial (Product_FSM.product A B) = (FSM.initial A, FSM.initial B)

goal (1 subgoal):
 1. target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])

goal (2 subgoals):
 1. \<lbrakk>path A (FSM.initial A) []; path B (FSM.initial B) []; p_io [] = p_io []\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] []) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] [])
target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] [])
target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] []) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path [] []) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path [] []) = (target (FSM.initial A) [], target (FSM.initial B) [])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
case (snoc x xs y ys)
[PROOF STATE]
proof (state)
this:
length xs = length ys
\<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys)
path A (FSM.initial A) (xs @ [x])
path B (FSM.initial B) (ys @ [y])
p_io (xs @ [x]) = p_io (ys @ [y])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "path A (initial A) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path A (FSM.initial A) xs
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) (xs @ [x])

goal (1 subgoal):
 1. path A (FSM.initial A) xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) xs

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) xs

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "path B (initial B) ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path B (FSM.initial B) ys
[PROOF STEP]
using snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
path B (FSM.initial B) (ys @ [y])

goal (1 subgoal):
 1. path B (FSM.initial B) ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path B (FSM.initial B) ys

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path B (FSM.initial B) ys

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "p_io xs = p_io ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io xs = p_io ys
[PROOF STEP]
using snoc.prems(3)
[PROOF STATE]
proof (prove)
using this:
p_io (xs @ [x]) = p_io (ys @ [y])

goal (1 subgoal):
 1. p_io xs = p_io ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_io xs = p_io ys

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path A (FSM.initial A) xs
path B (FSM.initial B) ys
p_io xs = p_io ys
[PROOF STEP]
have *:"path (product A B) (initial (product A B)) (zip_path xs ys)"
                and **:"target (initial (product A B)) (zip_path xs ys) = (target (initial A) xs, target (initial B) ys)"
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) xs
path B (FSM.initial B) ys
p_io xs = p_io ys

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) &&& target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys)
[PROOF STEP]
using snoc.IH
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) xs
path B (FSM.initial B) ys
p_io xs = p_io ys
\<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys)

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) &&& target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys)
target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys)
target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys)
[PROOF STEP]
have "(target (initial A) xs, target (initial B) ys) \<in> states (product A B)"
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys)
target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys)

goal (1 subgoal):
 1. (target (FSM.initial A) xs, target (FSM.initial B) ys) \<in> FSM.states (Product_FSM.product A B)
[PROOF STEP]
by (metis (no_types, lifting) path_target_is_state)
[PROOF STATE]
proof (state)
this:
(target (FSM.initial A) xs, target (FSM.initial B) ys) \<in> FSM.states (Product_FSM.product A B)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(target (FSM.initial A) xs, target (FSM.initial B) ys) \<in> FSM.states (Product_FSM.product A B)
[PROOF STEP]
have "(t_source x, t_source y) \<in> states (product A B)"
[PROOF STATE]
proof (prove)
using this:
(target (FSM.initial A) xs, target (FSM.initial B) ys) \<in> FSM.states (Product_FSM.product A B)

goal (1 subgoal):
 1. (t_source x, t_source y) \<in> FSM.states (Product_FSM.product A B)
[PROOF STEP]
using snoc.prems(1-2)
[PROOF STATE]
proof (prove)
using this:
(target (FSM.initial A) xs, target (FSM.initial B) ys) \<in> FSM.states (Product_FSM.product A B)
path A (FSM.initial A) (xs @ [x])
path B (FSM.initial B) (ys @ [y])

goal (1 subgoal):
 1. (t_source x, t_source y) \<in> FSM.states (Product_FSM.product A B)
[PROOF STEP]
by (metis path_cons_elim path_suffix)
[PROOF STATE]
proof (state)
this:
(t_source x, t_source y) \<in> FSM.states (Product_FSM.product A B)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "x \<in> transitions A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> FSM.transitions A
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) (xs @ [x])

goal (1 subgoal):
 1. x \<in> FSM.transitions A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> FSM.transitions A

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> FSM.transitions A

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "y \<in> transitions B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> FSM.transitions B
[PROOF STEP]
using snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
path B (FSM.initial B) (ys @ [y])

goal (1 subgoal):
 1. y \<in> FSM.transitions B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> FSM.transitions B

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> FSM.transitions B

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "t_input x = t_input y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_input x = t_input y
[PROOF STEP]
using snoc.prems(3)
[PROOF STATE]
proof (prove)
using this:
p_io (xs @ [x]) = p_io (ys @ [y])

goal (1 subgoal):
 1. t_input x = t_input y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t_input x = t_input y

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t_input x = t_input y

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "t_output x = t_output y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_output x = t_output y
[PROOF STEP]
using snoc.prems(3)
[PROOF STATE]
proof (prove)
using this:
p_io (xs @ [x]) = p_io (ys @ [y])

goal (1 subgoal):
 1. t_output x = t_output y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t_output x = t_output y

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> FSM.transitions A
y \<in> FSM.transitions B
t_input x = t_input y
t_output x = t_output y
[PROOF STEP]
have "((t_source x, t_source y), t_input x, t_output x, (t_target x, t_target y)) \<in> transitions (product A B)"
[PROOF STATE]
proof (prove)
using this:
x \<in> FSM.transitions A
y \<in> FSM.transitions B
t_input x = t_input y
t_output x = t_output y

goal (1 subgoal):
 1. ((t_source x, t_source y), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
unfolding product_transitions_alt_def
[PROOF STATE]
proof (prove)
using this:
x \<in> FSM.transitions A
y \<in> FSM.transitions B
t_input x = t_input y
t_output x = t_output y

goal (1 subgoal):
 1. ((t_source x, t_source y), t_input x, t_output x, t_target x, t_target y) \<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 A \<and> tB \<in> FSM.transitions B \<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 x, t_source y), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((t_source x, t_source y), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "t_source x = target (initial A) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_source x = target (FSM.initial A) xs
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) (xs @ [x])

goal (1 subgoal):
 1. t_source x = target (FSM.initial A) xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t_source x = target (FSM.initial A) xs

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t_source x = target (FSM.initial A) xs

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "t_source y = target (initial B) ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_source y = target (FSM.initial B) ys
[PROOF STEP]
using snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
path B (FSM.initial B) (ys @ [y])

goal (1 subgoal):
 1. t_source y = target (FSM.initial B) ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t_source y = target (FSM.initial B) ys

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((t_source x, t_source y), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)
t_source x = target (FSM.initial A) xs
t_source y = target (FSM.initial B) ys
[PROOF STEP]
have "((target (initial A) xs, target (initial B) ys), t_input x, t_output x, (t_target x, t_target y)) \<in> transitions (product A B)"
[PROOF STATE]
proof (prove)
using this:
((t_source x, t_source y), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)
t_source x = target (FSM.initial A) xs
t_source y = target (FSM.initial B) ys

goal (1 subgoal):
 1. ((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
using \<open>(t_source x, t_source y) \<in> states (product A B)\<close>
[PROOF STATE]
proof (prove)
using this:
((t_source x, t_source y), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)
t_source x = target (FSM.initial A) xs
t_source y = target (FSM.initial B) ys
(t_source x, t_source y) \<in> FSM.states (Product_FSM.product A B)

goal (1 subgoal):
 1. ((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)
[PROOF STEP]
have ***: "path (product A B) (initial (product A B)) ((zip_path xs ys)@[((target (initial A) xs, target (initial B) ys), t_input x, t_output x, (t_target x, t_target y))])"
[PROOF STATE]
proof (prove)
using this:
((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)])
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y) \<in> FSM.transitions (Product_FSM.product A B)
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys)
target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys)

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)])
[PROOF STEP]
by (metis (no_types, lifting) fst_conv path_append_transition)
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "t_target x = target (initial A) (xs@[x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_target x = target (FSM.initial A) (xs @ [x])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t_target x = target (FSM.initial A) (xs @ [x])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t_target x = target (FSM.initial A) (xs @ [x])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "t_target y = target (initial B) (ys@[y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_target y = target (FSM.initial B) (ys @ [y])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t_target y = target (FSM.initial B) (ys @ [y])

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t_target x = target (FSM.initial A) (xs @ [x])
t_target y = target (FSM.initial B) (ys @ [y])
[PROOF STEP]
have ****: "target (initial (product A B)) ((zip_path xs ys)@[((target (initial A) xs, target (initial B) ys), t_input x, t_output x, (t_target x, t_target y))])
                            = (target (initial A) (xs@[x]), target (initial B) (ys@[y]))"
[PROOF STATE]
proof (prove)
using this:
t_target x = target (FSM.initial A) (xs @ [x])
t_target y = target (FSM.initial B) (ys @ [y])

goal (1 subgoal):
 1. target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "(zip_path [x] [y]) = [((target (initial A) xs, target (initial B) ys), t_input x, t_output x, (t_target x, t_target y))]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zip_path [x] [y] = [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]
[PROOF STEP]
using \<open>t_source x = target (initial A) xs\<close> \<open>t_source y = target (initial B) ys\<close>
[PROOF STATE]
proof (prove)
using this:
t_source x = target (FSM.initial A) xs
t_source y = target (FSM.initial B) ys

goal (1 subgoal):
 1. zip_path [x] [y] = [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zip_path [x] [y] = [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
zip_path [x] [y] = [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "(zip_path (xs @ [x]) (ys @ [y])) = (zip_path xs ys)@(zip_path [x] [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ zip_path [x] [y]
[PROOF STEP]
using zip_path_last[of xs ys x y, OF snoc.hyps]
[PROOF STATE]
proof (prove)
using this:
zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ zip_path [x] [y]

goal (1 subgoal):
 1. zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ zip_path [x] [y]
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ zip_path [x] [y]

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
zip_path [x] [y] = [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]
zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ zip_path [x] [y]
[PROOF STEP]
have *****:"(zip_path (xs@[x]) (ys@[y]))
                            = (zip_path xs ys)@[((target (initial A) xs, target (initial B) ys), t_input x, t_output x, (t_target x, t_target y))]"
[PROOF STATE]
proof (prove)
using this:
zip_path [x] [y] = [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]
zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ zip_path [x] [y]

goal (1 subgoal):
 1. zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]
[PROOF STEP]
have "path (product A B) (initial (product A B)) (zip_path (xs@[x]) (ys@[y]))"
[PROOF STATE]
proof (prove)
using this:
zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y]))
[PROOF STEP]
using ***
[PROOF STATE]
proof (prove)
using this:
zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)])

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y]))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y]))

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y]))

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
have "target (initial (product A B)) (zip_path (xs@[x]) (ys@[y]))
                      = (target (initial A) (xs@[x]), target (initial B) (ys@[y]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
using **** *****
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
zip_path (xs @ [x]) (ys @ [y]) = zip_path xs ys @ [((target (FSM.initial A) xs, target (FSM.initial B) ys), t_input x, t_output x, t_target x, t_target y)]

goal (1 subgoal):
 1. target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>path A (FSM.initial A) xs; path B (FSM.initial B) ys; p_io xs = p_io ys\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path xs ys) = (target (FSM.initial A) xs, target (FSM.initial B) ys); path A (FSM.initial A) (xs @ [x]); path B (FSM.initial B) (ys @ [y]); p_io (xs @ [x]) = p_io (ys @ [y])\<rbrakk> \<Longrightarrow> path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y]))
target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y]))
target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path (xs @ [x]) (ys @ [y])) = (target (FSM.initial A) (xs @ [x]), target (FSM.initial B) (ys @ [y]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)

goal (2 subgoals):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2)
 2. target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
from c
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
show "path (product A B) (initial (product A B)) (zip_path p1 p2)"
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)

goal (1 subgoal):
 1. path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2)

goal (1 subgoal):
 1. target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
from c
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
show "target (initial (product A B)) (zip_path p1 p2)
                  = (target (initial A) p1, target (initial B) p2)"
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) \<and> target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)

goal (1 subgoal):
 1. target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target (FSM.initial (Product_FSM.product A B)) (zip_path p1 p2) = (target (FSM.initial A) p1, target (FSM.initial B) p2)

goal:
No subgoals!
[PROOF STEP]
qed