# Theory Product_FSM

```section ‹Product Machines›

text ‹This theory defines the construction of product machines.
A product machine of two finite state machines essentially represents all possible parallel
executions of those two machines.›

theory Product_FSM
imports FSM
begin

lift_definition product :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ ('a × 'd,'b,'c) fsm" is FSM_Impl.product
proof -
fix A :: "('a,'b,'c) fsm_impl"
fix B :: "('d,'b,'c) fsm_impl"
assume "well_formed_fsm A" and "well_formed_fsm B"

then have p1a: "fsm_impl.initial A ∈ fsm_impl.states A"
and p2a: "finite (fsm_impl.states A)"
and p3a: "finite (fsm_impl.inputs A)"
and p4a: "finite (fsm_impl.outputs A)"
and p5a: "finite (fsm_impl.transitions A)"
and p6a: "(∀t∈fsm_impl.transitions A.
t_source t ∈ fsm_impl.states A ∧
t_input t ∈ fsm_impl.inputs A ∧ t_target t ∈ fsm_impl.states A ∧
t_output t ∈ fsm_impl.outputs A)"
and p1b: "fsm_impl.initial B ∈ fsm_impl.states B"
and p2b: "finite (fsm_impl.states B)"
and p3b: "finite (fsm_impl.inputs B)"
and p4b: "finite (fsm_impl.outputs B)"
and p5b: "finite (fsm_impl.transitions B)"
and p6b: "(∀t∈fsm_impl.transitions B.
t_source t ∈ fsm_impl.states B ∧
t_input t ∈ fsm_impl.inputs B ∧ t_target t ∈ fsm_impl.states B ∧
t_output t ∈ fsm_impl.outputs B)"
by simp+

let ?P = "FSM_Impl.product A B"

have "fsm_impl.initial ?P ∈ fsm_impl.states ?P"
using p1a p1b by auto
moreover have "finite (fsm_impl.states ?P)"
using p2a p2b by auto
moreover have "finite (fsm_impl.inputs ?P)"
using p3a p3b by auto
moreover have "finite (fsm_impl.outputs ?P)"
using p4a p4b by auto
moreover have "finite (fsm_impl.transitions ?P)"
using p5a p5b unfolding product_code_naive by auto
moreover have "(∀t∈fsm_impl.transitions ?P.
t_source t ∈ fsm_impl.states ?P ∧
t_input t ∈ fsm_impl.inputs ?P ∧ t_target t ∈ fsm_impl.states ?P ∧
t_output t ∈ fsm_impl.outputs ?P)"
using p6a p6b by auto

ultimately show "well_formed_fsm (FSM_Impl.product A B)"
by blast
qed

abbreviation "left_path p ≡ map (λt. (fst (t_source t), t_input t, t_output t, fst (t_target t))) p"
abbreviation "right_path p ≡ map (λt. (snd (t_source t), t_input t, t_output t, snd (t_target t))) p"
abbreviation "zip_path p1 p2 ≡ (map (λ t . ((t_source (fst t), t_source (snd t)), t_input (fst t), t_output (fst t), (t_target (fst t), t_target (snd t))))
(zip p1 p2))"

lemma product_simps[simp]:
"initial (product A B) = (initial A, initial B)"
"states (product A B) = (states A) × (states B)"
"inputs (product A B) = inputs A ∪ inputs B"
"outputs (product A B) = outputs A ∪ outputs B"
by (transfer; simp)+

lemma product_transitions_def :
"transitions (product A B) = {((qA,qB),x,y,(qA',qB')) | qA qB x y qA' qB' . (qA,x,y,qA') ∈ transitions A ∧ (qB,x,y,qB') ∈ transitions B}"
by (transfer; simp)+

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 ∈ transitions A ∧ tB ∈ transitions B ∧ t_input tA = t_input tB ∧ t_output tA = t_output tB}"
(is "?T1 = ?T2")
proof -
have "⋀ t . t ∈ ?T1 ⟹ t ∈ ?T2"
proof -
fix tt assume "tt ∈ ?T1"
then obtain qA qB x y qA' qB' where "tt = ((qA,qB),x,y,(qA',qB'))" and "(qA,x,y,qA') ∈ transitions A" and "(qB,x,y,qB') ∈ transitions B"
unfolding product_transitions_def by blast
then 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'))) ∈ ?T2"
by auto
then show "tt ∈ ?T2"
unfolding ‹tt = ((qA,qB),x,y,(qA',qB'))› fst_conv snd_conv by assumption
qed
moreover have "⋀ t . t ∈ ?T2 ⟹ t ∈ ?T1"
proof -
fix tt assume "tt ∈ ?T2"
then 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 ∈ transitions A" and "tB ∈ transitions B" and "t_input tA = t_input tB" and "t_output tA = t_output tB"
by blast
then have "(t_source tA, t_input tA, t_output tA, t_target tA) ∈ transitions A"
and  "(t_source tB, t_input tA, t_output tA, t_target tB) ∈ transitions B"
by (metis prod.collapse)+
then show "tt ∈ ?T1"
unfolding product_transitions_def ‹tt = ((t_source tA, t_source tB),t_input tA, t_output tA, (t_target tA, t_target tB))› by blast
qed
ultimately show ?thesis by blast
qed

lemma zip_path_last : "length xs = length ys ⟹ (zip_path (xs @ [x]) (ys @ [y])) = (zip_path xs ys)@(zip_path [x] [y])"
by (induction xs ys rule: list_induct2; simp)

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 -
have "initial (product A B) = (initial A, initial B)" by auto
then have "(initial A, initial B) ∈ states (product A B)"
by (metis fsm_initial)

have "length p1 = length p2" using assms(3)
using map_eq_imp_length_eq by blast
then have c: "path (product A B) (initial (product A B)) (zip_path p1 p2)
∧ target (initial (product A B)) (zip_path p1 p2) = (target (initial A) p1, target (initial B) p2)"
using assms proof (induction p1 p2 rule: rev_induct2)
case Nil

then have "path (product A B) (initial (product A B)) (zip_path [] [])"
using ‹initial (product A B) = (initial A, initial B)› ‹(initial A, initial B) ∈ states (product A B)›
by (metis Nil_is_map_conv path.nil zip_Nil)
moreover have "target (initial (product A B)) (zip_path [] []) = (target (initial A) [], target (initial B) [])"
using ‹initial (product A B) = (initial A, initial B)› by auto
ultimately show ?case by fast
next
case (snoc x xs y ys)

have "path A (initial A) xs" using snoc.prems(1) by auto
moreover have "path B (initial B) ys" using snoc.prems(2) by auto
moreover have "p_io xs = p_io ys" using snoc.prems(3) by auto
ultimately 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)"
using snoc.IH by blast+
then have "(target (initial A) xs, target (initial B) ys) ∈ states (product A B)"
by (metis (no_types, lifting) path_target_is_state)
then have "(t_source x, t_source y) ∈ states (product A B)"
using snoc.prems(1-2)  by (metis path_cons_elim path_suffix)

have "x ∈ transitions A" using snoc.prems(1) by auto
moreover have "y ∈ transitions B" using snoc.prems(2) by auto
moreover have "t_input x = t_input y" using snoc.prems(3) by auto
moreover have "t_output x = t_output y" using snoc.prems(3) by auto
ultimately have "((t_source x, t_source y), t_input x, t_output x, (t_target x, t_target y)) ∈ transitions (product A B)"
unfolding product_transitions_alt_def by blast

moreover have "t_source x = target (initial A) xs" using snoc.prems(1) by auto
moreover have "t_source y = target (initial B) ys" using snoc.prems(2) by auto
ultimately have "((target (initial A) xs, target (initial B) ys), t_input x, t_output x, (t_target x, t_target y)) ∈ transitions (product A B)"
using ‹(t_source x, t_source y) ∈ states (product A B)›
by simp
then 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))])"
using * **
by (metis (no_types, lifting) fst_conv path_append_transition)

have "t_target x = target (initial A) (xs@[x])" by auto
moreover have "t_target y = target (initial B) (ys@[y])" by auto
ultimately 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]))"
by fastforce

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))]"
using ‹t_source x = target (initial A) xs› ‹t_source y = target (initial B) ys› by auto
moreover have "(zip_path (xs @ [x]) (ys @ [y])) = (zip_path xs ys)@(zip_path [x] [y])"
using zip_path_last[of xs ys x y, OF snoc.hyps]  by assumption
ultimately 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))]"
by auto
then have "path (product A B) (initial (product A B)) (zip_path (xs@[x]) (ys@[y]))"
using *** by presburger
moreover have "target (initial (product A B)) (zip_path (xs@[x]) (ys@[y]))
= (target (initial A) (xs@[x]), target (initial B) (ys@[y]))"
using **** ***** by auto
ultimately show ?case by linarith
qed

from c show "path (product A B) (initial (product A B)) (zip_path p1 p2)"
by auto
from c show "target (initial (product A B)) (zip_path p1 p2)
= (target (initial A) p1, target (initial B) p2)"
by auto
qed

lemma paths_from_product_path :
assumes "path (product A B) (initial (product A B)) p"
shows   "path A (initial A) (left_path p)"
and "path B (initial B) (right_path p)"
and "target (initial A) (left_path p) = fst (target (initial (product A B)) p)"
and "target (initial B) (right_path p) = snd (target (initial (product A B)) p)"
proof -
have "path A (initial A) (left_path p)
∧ path B (initial B) (right_path p)
∧ target (initial A) (left_path p) = fst (target (initial (product A B)) p)
∧ target (initial B) (right_path p) = snd (target (initial (product A B)) p)"
using assms proof (induction p rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc t p)
then have "path (product A B) (initial (product A B)) p" by fast
then have "path A (initial A) (left_path p)"
and "path B (initial B) (right_path p)"
and "target (initial A) (left_path p) = fst (target (initial (product A B)) p)"
and "target (initial B) (right_path p) = snd (target (initial (product A B)) p)"
using snoc.IH  by fastforce+

then have "t_source t = (target (initial A) (left_path p), target (initial B) (right_path p))"
using snoc.prems by (metis (no_types, lifting) path_cons_elim path_suffix prod.collapse)

have ***: "target (initial A) (left_path (p@[t]))= fst (target (initial (product A B)) (p@[t]))"
by fastforce
have ****: "target (initial B) (right_path (p@[t]))= snd (target (initial (product A B)) (p@[t]))"
by fastforce

have "t ∈ transitions (product A B)" using snoc.prems by auto

then have "(fst (t_source t), t_input t, t_output t, fst (t_target t)) ∈ transitions A"
unfolding product_transitions_alt_def by force
moreover have "target (initial A) (left_path p) = fst (t_source t)"
using ‹t_source t = (target (initial A) (left_path p), target (initial B) (right_path p))› by auto
ultimately have "path A (initial A) ((left_path p)@[(fst (t_source t), t_input t, t_output t, fst (t_target t))])"
by (simp add: ‹path A (initial A) (map (λt. (fst (t_source t), t_input t, t_output t, fst (t_target t))) p)› path_append_transition)
then have *: "path A (initial A) (left_path (p@[t]))" by auto

have "(snd (t_source t), t_input t, t_output t, snd (t_target t)) ∈ transitions B"
using ‹t ∈ transitions (product A B)› unfolding product_transitions_alt_def by auto
moreover have "target (initial B) (right_path p) = snd (t_source t)"
using ‹t_source t = (target (initial A) (left_path p), target (initial B) (right_path p))› by auto
ultimately have "path B (initial B) ((right_path p)@[(snd (t_source t), t_input t, t_output t, snd (t_target t))])"
by (simp add: ‹path B (initial B) (map (λt. (snd (t_source t), t_input t, t_output t, snd (t_target t))) p)› path_append_transition)
then have **: "path B (initial B) (right_path (p@[t]))" by auto

show ?case using * ** *** **** by blast
qed

then show "path A (initial A) (left_path p)"
and "path B (initial B) (right_path p)"
and "target (initial A) (left_path p) = fst (target (initial (product A B)) p)"
and "target (initial B) (right_path p) = snd (target (initial (product A B)) p)" by linarith+
qed

lemma zip_path_left_right[simp] :
"(zip_path (left_path p) (right_path p)) = p" by (induction p; auto)

lemma product_reachable_state_paths :
assumes "(q1,q2) ∈ reachable_states (product A B)"
obtains p1 p2
where "path A (initial A) p1"
and   "path B (initial B) p2"
and   "target (initial A) p1 = q1"
and   "target (initial B) p2 = q2"
and   "p_io p1 = p_io p2"
and   "path (product A B) (initial (product A B)) (zip_path p1 p2)"
and   "target (initial (product A B)) (zip_path p1 p2) = (q1,q2)"
proof -
let ?P = "product A B"
from assms obtain p where "path ?P (initial ?P) p" and "target (initial ?P) p = (q1,q2)"
unfolding reachable_states_def by auto

have "path A (initial A) (left_path p)"
and "path B (initial B) (right_path p)"
and "target (initial A) (left_path p) = q1"
and "target (initial B) (right_path p) = q2"
using paths_from_product_path[OF ‹path ?P (initial ?P) p›] ‹target (initial ?P) p = (q1,q2)› by auto

moreover have "p_io (left_path p) = p_io (right_path p)" by auto
moreover have "path (product A B) (initial (product A B)) (zip_path (left_path p) (right_path p))"
using ‹path ?P (initial ?P) p› by auto
moreover have "target (initial (product A B)) (zip_path (left_path p) (right_path p)) = (q1,q2)"
using ‹target (initial ?P) p = (q1,q2)› by auto
ultimately show ?thesis using that by blast
qed

lemma product_reachable_states[iff] :
"(q1,q2) ∈ reachable_states (product A B) ⟷ (∃ p1 p2 . path A (initial A) p1 ∧ path B (initial B) p2 ∧ target (initial A) p1 = q1 ∧ target (initial B) p2 = q2 ∧ p_io p1 = p_io p2)"
proof
show "(q1,q2) ∈ reachable_states (product A B) ⟹ (∃ p1 p2 . path A (initial A) p1 ∧ path B (initial B) p2 ∧ target (initial A) p1 = q1 ∧ target (initial B) p2 = q2 ∧ p_io p1 = p_io p2)"
using product_reachable_state_paths[of q1 q2 A B] by blast
show "(∃ p1 p2 . path A (initial A) p1 ∧ path B (initial B) p2 ∧ target (initial A) p1 = q1 ∧ target (initial B) p2 = q2 ∧ p_io p1 = p_io p2) ⟹ (q1,q2) ∈ reachable_states (product A B)"
proof -
assume "(∃ p1 p2 . path A (initial A) p1 ∧ path B (initial B) p2 ∧ target (initial A) p1 = q1 ∧ target (initial B) p2 = q2 ∧ p_io p1 = p_io p2)"
then obtain p1 p2 where "path A (initial A) p1 ∧ path B (initial B) p2 ∧ target (initial A) p1 = q1 ∧ target (initial B) p2 = q2 ∧ p_io p1 = p_io p2"
by blast
then show ?thesis
using product_path_from_paths[of A p1 B p2] unfolding reachable_states_def
by (metis (mono_tags, lifting) mem_Collect_eq)
qed
qed

lemma left_path_zip : "length p1 = length p2 ⟹ left_path (zip_path p1 p2) = p1"
by (induction p1 p2 rule: list_induct2; simp)

lemma right_path_zip : "length p1 = length p2 ⟹ p_io p1 = p_io p2 ⟹ right_path (zip_path p1 p2) = p2"
by (induction p1 p2 rule: list_induct2; simp)

lemma zip_path_append_left_right : "length p1 = length p2 ⟹ zip_path (p1@(left_path p)) (p2@(right_path p)) = (zip_path p1 p2)@p"
proof (induction p1 p2 rule: list_induct2)
case Nil
then show ?case by (induction p; simp)
next
case (Cons x xs y ys)
then show ?case by simp
qed

lemma product_path:
"path (product A B) (q1,q2) p ⟷ (path A q1 (left_path p) ∧ path B q2 (right_path p))"
proof (induction p arbitrary: q1 q2)
case Nil
then show ?case by auto
next
case (Cons t p)

have "path (Product_FSM.product A B) (q1, q2) (t # p) ⟹ (path A q1 (left_path (t # p)) ∧ path B q2 (right_path (t # p)))"
proof -
assume "path (Product_FSM.product A B) (q1, q2) (t # p)"
then obtain x y qA' qB' where "t = ((q1,q2),x,y,(qA',qB'))" using prod.collapse
by (metis path_cons_elim)
then have "((q1,q2),x,y,(qA',qB')) ∈ transitions (product A B)"
using ‹path (Product_FSM.product A B) (q1, q2) (t # p)› by auto
then have "(q1, x, y, qA') ∈ FSM.transitions A" and "(q2, x, y, qB') ∈ FSM.transitions B"
unfolding product_transitions_def by blast+
moreover have "(path A qA' (left_path p) ∧ path B qB' (right_path p))"
using Cons.IH[of qA' qB'] ‹path (Product_FSM.product A B) (q1, q2) (t # p)› unfolding ‹t = ((q1,q2),x,y,(qA',qB'))› by auto
ultimately show ?thesis
unfolding ‹t = ((q1,q2),x,y,(qA',qB'))›
qed

moreover have "path A q1 (left_path (t # p)) ⟹ path B q2 (right_path (t # p)) ⟹ path (Product_FSM.product A B) (q1, q2) (t # p)"
proof -
assume "path A q1 (left_path (t # p))" and "path B q2 (right_path (t # p))"
then obtain x y qA' qB' where "t = ((q1,q2),x,y,(qA',qB'))" using prod.collapse
by (metis (no_types, lifting) fst_conv list.simps(9) path_cons_elim)
then have "(q1, x, y, qA') ∈ FSM.transitions A" and "(q2, x, y, qB') ∈ FSM.transitions B"
using ‹path A q1 (left_path (t # p))› ‹path B q2 (right_path (t # p))› by auto
then have "((q1,q2),x,y,(qA',qB')) ∈ transitions (product A B)"
unfolding product_transitions_def by blast
moreover have "path (Product_FSM.product A B) (qA', qB') p"
using Cons.IH[of qA' qB'] ‹path A q1 (left_path (t # p))› ‹path B q2 (right_path (t # p))› unfolding ‹t = ((q1,q2),x,y,(qA',qB'))› by auto
ultimately show "path (Product_FSM.product A B) (q1, q2) (t # p)"
unfolding ‹t = ((q1,q2),x,y,(qA',qB'))›
qed

ultimately show ?case by force
qed

lemma product_path_rev:
assumes "p_io p1 = p_io p2"
shows "path (product A B) (q1,q2) (zip_path p1 p2) ⟷ (path A q1 p1 ∧ path B q2 p2)"
proof -
have "length p1 = length p2" using assms
using map_eq_imp_length_eq by blast
then have "(map (λ t . (fst (t_source t), t_input t, t_output t, fst (t_target t))) (map (λ t . ((t_source (fst t), t_source (snd t)), t_input (fst t), t_output (fst t), (t_target (fst t), t_target (snd t)))) (zip p1 p2))) = p1"
by (induction p1 p2 arbitrary: q1 q2 rule: list_induct2; auto)

moreover have "(map (λ t . (snd (t_source t), t_input t, t_output t, snd (t_target t))) (map (λ t . ((t_source (fst t), t_source (snd t)), t_input (fst t), t_output (fst t), (t_target (fst t), t_target (snd t)))) (zip p1 p2))) = p2"
using ‹length p1 = length p2› assms by (induction p1 p2 arbitrary: q1 q2 rule: list_induct2; auto)

ultimately show ?thesis using product_path[of A B q1 q2 "(map (λ t . ((t_source (fst t), t_source (snd t)), t_input (fst t), t_output (fst t), (t_target (fst t), t_target (snd t)))) (zip p1 p2))"]
by auto
qed

lemma product_language_state :
shows "LS (product A B) (q1,q2) = LS A q1 ∩ LS B q2"
proof
show "LS (product A B) (q1, q2) ⊆ LS A q1 ∩ LS B q2"
proof
fix io assume "io ∈ LS (product A B) (q1, q2)"
then obtain p where "io = p_io p"
and "path (product A B) (q1,q2) p"
by auto
then obtain p1 p2 where "path A q1 p1"
and "path B q2 p2"
and "io = p_io p1"
and "io = p_io p2"
using product_path[of A B q1 q2 p] by fastforce
then show "io ∈ LS A q1 ∩ LS B q2"
unfolding LS.simps by blast
qed

show "LS A q1 ∩ LS B q2 ⊆ LS (product A B) (q1, q2)"
proof
fix io assume "io ∈ LS A q1 ∩ LS B q2"
then obtain p1 p2 where "path A q1 p1"
and "path B q2 p2"
and "io = p_io p1"
and "io = p_io p2"
and "p_io p1 = p_io p2"
by auto

let ?p = "zip_path p1 p2"

have "length p1 = length p2"
using ‹p_io p1 = p_io p2› map_eq_imp_length_eq by blast
moreover have "p_io ?p = p_io (map fst (zip p1 p2))" by auto
ultimately have "p_io ?p = p_io p1" by auto

then have "p_io ?p = io"
using ‹io = p_io p1› by auto
moreover have "path (product A B) (q1, q2) ?p"
using product_path_rev[OF ‹p_io p1 = p_io p2›, of A B q1 q2] ‹path A q1 p1› ‹path B q2 p2› by auto
ultimately show "io ∈ LS (product A B) (q1, q2)"
unfolding LS.simps by blast
qed
qed

lemma product_language : "L (product A B) = L A ∩ L B"
unfolding product_simps product_language_state by blast

lemma product_transition_split_ob :
assumes "t ∈ transitions (product A B)"
obtains t1 t2
where "t1 ∈ transitions A ∧ t_source t1 = fst (t_source t) ∧ t_input t1 = t_input t ∧ t_output t1 = t_output t ∧ t_target t1 = fst (t_target t)"
and "t2 ∈ transitions B ∧ t_source t2 = snd (t_source t) ∧ t_input t2 = t_input t ∧ t_output t2 = t_output t ∧ t_target t2 = snd (t_target t)"
using assms unfolding product_transitions_alt_def
by auto

lemma product_transition_split :
assumes "t ∈ transitions (product A B)"
shows "(fst (t_source t), t_input t, t_output t, fst (t_target t)) ∈ transitions A"
and "(snd (t_source t), t_input t, t_output t, snd (t_target t)) ∈ transitions B"
using product_transition_split_ob[OF assms] prod.collapse by fastforce+

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'"
using assms by (induction p arbitrary: q1 q2; force)+

lemma target_single_transition[simp] : "target q1 [(q1, x, y, q1')] = q1'"
by auto

lemma product_undefined_input :
assumes "¬ (∃ t ∈ transitions (product (from_FSM M q1) (from_FSM M q2)).
t_source t = qq ∧ t_input t = x)"
and "q1 ∈ states M"
and "q2 ∈ states M"
shows "¬ (∃ t1 ∈ transitions M. ∃ t2 ∈ transitions M.
t_source t1 = fst qq ∧
t_source t2 = snd qq ∧
t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2)"
proof
assume "∃ t1 ∈ transitions M. ∃ t2 ∈ transitions M.
t_source t1 = fst qq ∧
t_source t2 = snd qq ∧
t_input t1 = x ∧ t_input t2 = x ∧ t_output t1 = t_output t2"
then obtain t1 t2 where "t1 ∈ transitions M"
and "t2 ∈ 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"
by force

have "((t_source t1, t_source t2), t_input t1, t_output t1, t_target t1, t_target t2) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))"
unfolding product_transitions_alt_def
unfolding from_FSM_simps[OF assms(2)]
unfolding from_FSM_simps[OF assms(3)]
using ‹t1 ∈ transitions M› ‹t2 ∈ transitions M› ‹t_input t1 = t_input t2› ‹t_output t1 = t_output t2› by blast
then show False
unfolding ‹t_source t1 = fst qq› ‹t_source t2 = snd qq› ‹t_input t1 = x› prod.collapse
using assms(1) by auto
qed

subsection ‹Product Machines and Changing Initial States›

lemma product_from_reachable_next :
assumes "((q1,q2),x,y,(q1',q2')) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))"
and     "q1 ∈ states M"
and     "q2 ∈ 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 -
have "(q1,x,y,q1') ∈ transitions (from_FSM M q1)"
and  "(q2,x,y,q2') ∈ transitions (from_FSM M q2)"
using assms(1) unfolding product_transitions_def by blast+
then have "q1' ∈ states (from_FSM M q1)" and "q2' ∈ states (from_FSM M q2)"
using fsm_transition_target by auto

have "q1' ∈ states (from_FSM M q1')" and "q1' ∈ states M" and "q1 ∈ states M"
using ‹q1' ∈ FSM.states (FSM.from_FSM M q1)› assms(2) reachable_state_is_state by fastforce+
have "q2' ∈ states (from_FSM M q2')" and "q2' ∈ states M" and "q2 ∈ states M"
using ‹q2' ∈ FSM.states (FSM.from_FSM M q2)› assms(3) reachable_state_is_state by fastforce+

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"
using from_FSM_simps[OF fsm_transition_target[OF assms(1)]]
unfolding snd_conv
unfolding product_simps
unfolding product_transitions_def
unfolding from_FSM_simps[OF ‹q1' ∈ states M›] from_FSM_simps[OF ‹q2' ∈ states M›]
unfolding from_FSM_simps[OF ‹q1 ∈ states M›] from_FSM_simps[OF ‹q2 ∈ states M›]
by auto

then show ?thesis by (transfer; auto)
qed

lemma from_FSM_product_inputs :
assumes "q1 ∈ states M" and "q2 ∈ states M"
shows "(inputs (product (from_FSM M q1) (from_FSM M q2))) = (inputs M)"

lemma from_FSM_product_outputs :
assumes "q1 ∈ states M" and "q2 ∈ states M"
shows "(outputs (product (from_FSM M q1) (from_FSM M q2))) = (outputs M)"

lemma from_FSM_product_initial :
assumes "q1 ∈ states M" and "q2 ∈ states M"
shows "initial (product (from_FSM M q1) (from_FSM M q2)) = (q1,q2)"

lemma product_from_reachable_next' :
assumes "t ∈ transitions (product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t))))"
and     "fst (t_source t) ∈ states M"
and     "snd (t_source t) ∈ 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 -
have "((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t"
by simp
then show ?thesis
by (metis (no_types) assms(1) assms(2) assms(3) product_from_reachable_next)
qed

lemma product_from_reachable_next'_path :
assumes "t ∈ transitions (product (from_FSM M (fst (t_source t))) (from_FSM M (snd (t_source t))))"
and     "fst (t_source t) ∈ states M"
and     "snd (t_source t) ∈ 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 -
have i1: "initial ?P1 = ?q"
using assms(1) fsm_transition_target by fastforce
have i2: "initial ?P2 = ?q"
proof -
have "((fst (t_source t), snd (t_source t)), t_input t, t_output t, fst (t_target t), snd (t_target t)) = t"
by auto
then show ?thesis
by (metis (no_types) assms(1) assms(2) assms(3) i1 product_from_reachable_next)
qed

have h12: "transitions ?P1 = transitions ?P2" using product_from_reachable_next'[OF assms] by simp

show ?thesis proof (induction p rule: rev_induct)
case Nil
then show ?case
by (metis (full_types) i1 i2 fsm_initial path.nil)
next
case (snoc t p)
show ?case
by (metis h12 path_append_transition path_append_transition_elim(1) path_append_transition_elim(2) path_append_transition_elim(3) snoc.IH)
qed
qed

lemma product_from_transition:
assumes "(q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2))"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "transitions (product (from_FSM M q1') (from_FSM M q2')) = transitions (product (from_FSM M q1) (from_FSM M q2))"
proof -
have "q1' ∈ states M" and "q2' ∈ states M"
using assms(1) unfolding product_simps from_FSM_simps[OF assms(2)] from_FSM_simps[OF assms(3)] by auto
show ?thesis
unfolding product_transitions_def from_FSM_simps[OF ‹q1 ∈ states M›] from_FSM_simps[OF ‹q1' ∈ states M›] from_FSM_simps[OF ‹q2 ∈ states M›] from_FSM_simps[OF ‹q2' ∈ states M›] by blast
qed

lemma product_from_path:
assumes "(q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2))"
and     "q1 ∈ states M"
and     "q2 ∈ 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"
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))

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 ∈ transitions (product (from_FSM M q1) (from_FSM M q2))"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "path (product (from_FSM M q1) (from_FSM M q2)) (t_target t) p" (is "path ?P (t_target t) p")
by (metis assms(1) assms(2) assms(3) assms(4) fsm_transition_target prod.collapse product_from_path)

lemma product_from_transition_shared_state :
assumes "t ∈ transitions (product (from_FSM M q1') (from_FSM M q2'))"
and     "(q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2))"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "t ∈ transitions (product (from_FSM M q1) (from_FSM M q2))"
by (metis assms product_from_transition)

lemma product_from_not_completely_specified :
assumes "¬ completely_specified_state (product (from_FSM M q1) (from_FSM M q2)) (q1',q2')"
and     "(q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2))"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows  "¬ completely_specified_state (product (from_FSM M q1') (from_FSM M q2')) (q1',q2')"
proof -
have "q1' ∈ states M" and "q2' ∈ states M"
using assms(2) unfolding product_simps from_FSM_simps[OF assms(3)] from_FSM_simps[OF assms(4)] by auto
show ?thesis

using from_FSM_product_inputs[OF assms(3) assms(4)]
using from_FSM_product_inputs[OF ‹q1' ∈ states M› ‹q2' ∈ states M› ]
proof -
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))"
by (metis (no_types) ‹(q1', q2') ∈ FSM.states (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2))› assms(3) assms(4) product_from_transition)
then show ?thesis
using ‹FSM.inputs (Product_FSM.product (FSM.from_FSM M q1') (FSM.from_FSM M q2')) = FSM.inputs M› ‹FSM.inputs (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) = FSM.inputs M› ‹¬ completely_specified_state (Product_FSM.product (FSM.from_FSM M q1) (FSM.from_FSM M q2)) (q1', q2')› by fastforce
qed
qed

lemma from_product_initial_paths_ex :
assumes "q1 ∈ states M"
and     "q2 ∈ states M"
shows  "(∃p1 p2.
path (from_FSM M q1) (initial (from_FSM M q1)) p1 ∧
path (from_FSM M q2) (initial (from_FSM M q2)) p2 ∧
target (initial (from_FSM M q1)) p1 = q1 ∧
target (initial (from_FSM M q2)) p2 = q2 ∧ p_io p1 = p_io p2)"
proof -
have "path (from_FSM M q1) (initial (from_FSM M q1)) []" by blast
moreover have "path (from_FSM M q2) (initial (from_FSM M q2)) []" by blast
moreover have "
target (initial (from_FSM M q1)) [] = q1 ∧
target (initial (from_FSM M q2)) [] = q2 ∧ p_io [] = p_io []"
unfolding from_FSM_simps[OF assms(1)] from_FSM_simps[OF assms(2)] by auto
ultimately show ?thesis by blast
qed

lemma product_observable :
assumes "observable M1"
and     "observable M2"
shows "observable (product M1 M2)" (is "observable ?P")
proof -
have "⋀ t1 t2 . t1 ∈ transitions ?P ⟹ t2 ∈ transitions ?P ⟹ t_source t1 = t_source t2 ⟹ t_input t1 = t_input t2 ⟹ t_output t1 = t_output t2 ⟹ t_target t1 = t_target t2"
proof -
fix t1 t2 assume "t1 ∈ transitions ?P" and "t2 ∈ transitions ?P" and "t_source t1 = t_source t2" and "t_input t1 = t_input t2" and "t_output t1 = t_output t2"

let ?t1L = "(fst (t_source t1), t_input t1, t_output t1, fst (t_target t1))"
let ?t1R = "(snd (t_source t1), t_input t1, t_output t1, snd (t_target t1))"
let ?t2L = "(fst (t_source t2), t_input t2, t_output t2, fst (t_target t2))"
let ?t2R = "(snd (t_source t2), t_input t2, t_output t2, snd (t_target t2))"

have "t_target ?t1L = t_target ?t2L"
using product_transition_split(1)[OF ‹t1 ∈ transitions ?P›]
product_transition_split(1)[OF ‹t2 ∈ transitions ?P›]
‹observable M1›
‹t_source t1 = t_source t2›
‹t_input t1 = t_input t2›
‹t_output t1 = t_output t2› by auto
moreover have "t_target ?t1R = t_target ?t2R"
using product_transition_split(2)[OF ‹t1 ∈ transitions ?P›]
product_transition_split(2)[OF ‹t2 ∈ transitions ?P›]
‹observable M2›
‹t_source t1 = t_source t2›
‹t_input t1 = t_input t2›
‹t_output t1 = t_output t2› by auto
ultimately show "t_target t1 = t_target t2"
by (metis prod.exhaust_sel snd_conv)
qed
then show ?thesis unfolding observable.simps by blast
qed

lemma product_observable_self_transitions :
assumes "q ∈ reachable_states (product M M)"
and     "observable M"
shows "fst q = snd q"
proof -
let ?P = "product M M"

have "⋀ p . path ?P (initial ?P) p ⟹ fst (target (initial ?P) p) = snd (target (initial ?P) p)"
proof -
fix p assume "path ?P (initial ?P) p"
then show "fst (target (initial ?P) p) = snd (target (initial ?P) p)"
proof (induction p rule: rev_induct)
case Nil
then show ?case by simp
next
case (snoc t p)

have "path ?P (initial ?P) p" and "path ?P (target (initial ?P) p) [t]"
using path_append_elim[of ?P "initial ?P" p "[t]", OF ‹path (product M M) (initial (product M M)) (p @ [t])›] by blast+
then have "t ∈ transitions ?P"
by blast
have "t_source t = target (initial ?P) p"
using snoc.prems by fastforce

let ?t1 = "(fst (t_source t), t_input t, t_output t, fst (t_target t))"
let ?t2 = "(snd (t_source t), t_input t, t_output t, snd (t_target t))"
have "?t1 ∈ transitions M" and "?t2 ∈ transitions M"
using product_transition_split[OF ‹t ∈ transitions ?P›] by auto
moreover have "t_source ?t1 = t_source ?t2"
using ‹t_source t = target (initial ?P) p› snoc.IH[OF ‹path ?P (initial ?P) p›]
by (metis fst_conv)
moreover have "t_input ?t1 = t_input ?t2"
by auto
moreover have "t_output ?t1 = t_output ?t2"
by auto
ultimately have "t_target ?t1 = t_target ?t2"
using ‹observable M› unfolding observable.simps by blast
then have "fst (t_target t) = snd (t_target t)"
by auto
then show ?case unfolding target.simps visited_states.simps
proof -
show "fst (last (initial (product M M) # map t_target (p @ [t]))) = snd (last (initial (product M M) # map t_target (p @ [t])))"
using ‹fst (t_target t) = snd (t_target t)› last_map last_snoc length_append_singleton length_map by force
qed
qed
qed

then show ?thesis
using assms(1) unfolding reachable_states_def
by blast
qed

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"
using assms by (induction xs1 xs2 ys1 ys2 rule: list_induct4; auto)

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"
using assms by (induction xs1 xs2 ys1 ys2 rule: list_induct4; auto)

lemma zip_path_merge :
"(zip_path (left_path p) (right_path p)) = p"
by (induction p; auto)

lemma product_from_reachable_path' :
assumes "path (product (from_FSM M q1) (from_FSM M q2)) (q1', q2') p"
and     "q1 ∈ reachable_states M"
and     "q2 ∈ reachable_states M"
shows "path (product (from_FSM M q1') (from_FSM M q2')) (q1', q2') p"
by (meson assms(1) assms(2) assms(3) from_FSM_path from_FSM_path_rev_initial product_path reachable_state_is_state)

lemma product_from :
assumes "q1 ∈ states M"
and     "q2 ∈ states M"
shows "product (from_FSM M q1) (from_FSM M q2) = from_FSM (product M M) (q1,q2)" (is "?PF = ?FP")
proof -
have "(q1,q2) ∈ states (product M M)"
using assms unfolding product_simps by auto

have "initial ?FP = initial ?PF"
and  "inputs ?FP = inputs ?PF"
and  "outputs ?FP = outputs ?PF"
and  "states ?FP = states ?PF"
and  "transitions ?FP = transitions ?PF"
unfolding product_simps
from_FSM_simps[OF assms(1)]
from_FSM_simps[OF assms(2)]
from_FSM_simps[OF ‹(q1,q2) ∈ states (product M M)›]
product_transitions_def
by auto
then show ?thesis by (transfer; auto)
qed

lemma product_from_from :
assumes "(q1',q2') ∈ states (product (from_FSM M q1) (from_FSM M q2))"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "(product (from_FSM M q1') (from_FSM M q2')) = (from_FSM (product (from_FSM M q1) (from_FSM M q2)) (q1',q2'))"
using product_from
by (metis (no_types, lifting) assms(1) assms(2) assms(3) from_FSM_simps(5) from_from mem_Sigma_iff product_simps(2))

lemma submachine_transition_product_from :
assumes "is_submachine S (product (from_FSM M q1) (from_FSM M q2))"
and     "((q1,q2),x,y,(q1',q2')) ∈ transitions S"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "is_submachine (from_FSM S (q1',q2')) (product (from_FSM M q1') (from_FSM M q2'))"
proof -
have "((q1,q2),x,y,(q1',q2')) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))"
using assms(1) assms(2) by auto
have "(q1',q2') ∈ states S" using fsm_transition_target assms(2) by auto
show ?thesis
using product_from_reachable_next[OF ‹((q1,q2),x,y,(q1',q2')) ∈ transitions (product (from_FSM M q1) (from_FSM M q2))› assms(3,4)]
submachine_from[OF assms(1) ‹(q1',q2') ∈ states S›]
by simp
qed

lemma submachine_transition_complete_product_from :
assumes "is_submachine S (product (from_FSM M q1) (from_FSM M q2))"
and "completely_specified S"
and "((q1,q2),x,y,(q1',q2')) ∈ transitions S"
and     "q1 ∈ states M"
and     "q2 ∈ states M"
shows "completely_specified (from_FSM S (q1',q2'))"
proof -
let ?P = "(product (from_FSM M q1) (from_FSM M q2))"
let ?P' = "(product (from_FSM M q1') (from_FSM M q2'))"
let ?F = "(from_FSM S (q1',q2'))"

have "initial ?P = (q1,q2)"
by (simp add: assms(4) assms(5) reachable_state_is_state)

then have "initial S = (q1,q2)"
using assms(1) by (metis is_submachine.simps)
then have "(q1',q2') ∈ states S"
using assms(3)
using fsm_transition_target by fastforce
then have "states ?F = states S"
using from_FSM_simps(5) by simp
moreover have "inputs ?F = inputs S"
using from_FSM_simps(2) ‹(q1',q2') ∈ states S› by simp
ultimately show "completely_specified ?F"
using assms(2) unfolding completely_specified.simps
by (meson assms(2) completely_specified.elims(2) from_FSM_completely_specified)
qed

subsection ‹Calculating Acyclic Intersection Languages›

lemma acyclic_product :
assumes "acyclic B"
shows "acyclic (product A B)"
proof -
show "acyclic (product A B)"
proof (rule ccontr)
assume "¬ FSM.acyclic (Product_FSM.product A B)"
then obtain p where "path (product A B) (initial (product A B)) p" and "¬ distinct (visited_states (initial (product A B)) p)"
by auto

have "path B (initial B) (right_path p)"
using product_path[of A B] ‹path (product A B) (initial (product A B)) p›
unfolding product_simps
by auto

moreover have "¬ distinct (visited_states (initial B) (right_path p))"
proof -
obtain i j where "i < j" and "j < length ((initial A, initial B) # map t_target p)" and "((initial A, initial B) # map t_target p) ! i = ((initial A, initial B) # map t_target p) ! j"
using ‹¬ distinct (visited_states (initial (product A B)) p)›
unfolding visited_states.simps product_simps
using non_distinct_repetition_indices by blast

then have "snd (((initial A, initial B) # map t_target p) ! i) = snd (((initial A, initial B) # map t_target p) ! j)"
by simp

have * :"i < length ((initial B) # map t_target (right_path p))"
and  **:"j < length ((initial B) # map t_target (right_path p))"
using ‹i < j› ‹j < length ((initial A, initial B) # map t_target p)› by auto

have right_nth: "⋀ i . i < length ((initial B) # map t_target (right_path p)) ⟹ ((initial B) # map t_target (right_path p)) ! i = snd (((initial A, initial B) # map t_target p) ! i)"
proof -
have "((initial B) # map t_target (right_path p)) ! 0 = snd (((initial A, initial B) # map t_target p) ! 0)"
by simp
moreover have "⋀ i . Suc i < length ((initial B) # map t_target (right_path p)) ⟹ ((initial B) # map t_target (right_path p)) ! Suc i = snd (((initial A, initial B) # map t_target p) ! Suc i)"
by auto
ultimately show "⋀ i . i < length ((initial B) # map t_target (right_path p)) ⟹ ((initial B) # map t_target (right_path p)) ! i = snd (((initial A, initial B) # map t_target p) ! i)"
using less_Suc_eq_0_disj by auto
qed

have "((initial B) # map t_target (right_path p)) ! i = ((initial B) # map t_target (right_path p)) ! j"
using ‹snd (((initial A, initial B) # map t_target p) ! i) = snd (((initial A, initial B) # map t_target p) ! j)›
unfolding right_nth[OF *] right_nth[OF **]
by assumption
then show ?thesis
unfolding visited_states.simps product_simps
using non_distinct_repetition_indices_rev[OF ‹i < j› **] by blast
qed
ultimately show "False"
using ‹acyclic B› unfolding acyclic.simps by blast
qed
qed

lemma acyclic_product_path_length :
assumes "acyclic B"
and     "path (product A B) (initial (product A B)) p"
shows "length p < size B"
proof -
have *:"path B (initial B) (right_path p)"
using product_path[of A B] ‹path (product A B) (initial (product A B)) p›
unfolding product_simps
by auto
then have **: "distinct (visited_states (initial B) (right_path p))"
using assms unfolding acyclic.simps by blast

have "length (right_path p) < size B"
using acyclic_path_length_limit[OF * **] by assumption
then show "length p < size B"
by auto
qed

lemma acyclic_language_alt_def :
assumes "acyclic A"
shows "image p_io (acyclic_paths_up_to_length A (initial A) (size A - 1)) = L A"
proof -
let ?ps = "acyclic_paths_up_to_length A (initial A) (size A - 1)"
have "⋀ p . path A (initial A) p ⟹ length p ≤ FSM.size A - 1"
using acyclic_path_length_limit assms unfolding acyclic.simps
by fastforce
then have "?ps = {p. path A (initial A) p}"
using assms unfolding acyclic_paths_up_to_length.simps acyclic.simps by blast
then show ?thesis unfolding LS.simps by blast
qed

definition acyclic_language_intersection :: "('a,'b,'c) fsm ⇒ ('d,'b,'c) fsm ⇒ ('b × 'c) list set" where
"acyclic_language_intersection M A = (let P = product M A in image p_io (acyclic_paths_up_to_length P (initial P) (size A - 1)))"

lemma acyclic_language_intersection_completeness :
assumes "acyclic A"
shows "acyclic_language_intersection M A = L M ∩ L A"
proof -
let ?P = "product M A"
let ?ps = "acyclic_paths_up_to_length ?P (initial ?P) (size A - 1)"

have "L ?P = L M ∩ L A"
using product_language by blast

have "⋀ p . path ?P (initial ?P) p ⟹ length p ≤ FSM.size A - 1"
using acyclic_product_path_length[OF assms]
by fastforce
then have "?ps = {p. path ?P (initial ?P) p}"
using acyclic_product[OF assms] unfolding acyclic_paths_up_to_length.simps acyclic.simps by blast
then have "image p_io ?ps = L ?P"
unfolding LS.simps by blast
then show ?thesis
using product_language unfolding acyclic_language_intersection_def Let_def by blast
qed

end```