diff --git a/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy
--- a/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy
@@ -1,107 +1,108 @@
 section \<open>Deterministic Büchi Automata Combinations\<close>
 
 theory DBA_Combine
 imports DBA DGBA
 begin
 
   global_interpretation degeneralization: automaton_degeneralization_trace
     dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\<lambda> P w r p. gen infs P r"
     dba dba.alphabet dba.initial dba.transition dba.accepting "\<lambda> P w r p. infs P r"
+    fst id
     defines degeneralize = degeneralization.degeneralize
-    by unfold_locales auto
+    by (unfold_locales) (auto simp flip: sscan_smap)
 
   lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded DBA.language_def]
   lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded DBA.nodes_def]
   lemmas degeneralize_nodes_card = degeneralization.degeneralize_nodes_card[folded DBA.nodes_def]
 
   global_interpretation intersection: automaton_intersection_trace
     dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\<lambda> P w r p. infs P r"
     dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\<lambda> P w r p. infs P r"
     dgba.dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\<lambda> P w r p. gen infs P r"
     "\<lambda> c\<^sub>1 c\<^sub>2. [c\<^sub>1 \<circ> fst, c\<^sub>2 \<circ> snd]"
     defines intersect' = intersection.combine
     by unfold_locales auto
 
   lemmas intersect'_language[simp] = intersection.combine_language[folded DGBA.language_def]
   lemmas intersect'_nodes_finite = intersection.combine_nodes_finite[folded DGBA.nodes_def]
   lemmas intersect'_nodes_card = intersection.combine_nodes_card[folded DGBA.nodes_def]
 
   global_interpretation union: automaton_union_trace
     dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\<lambda> P w r p. infs P r"
     dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\<lambda> P w r p. infs P r"
     dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\<lambda> P w r p. infs P r"
     "\<lambda> c\<^sub>1 c\<^sub>2 pq. (c\<^sub>1 \<circ> fst) pq \<or> (c\<^sub>2 \<circ> snd) pq"
     defines union = union.combine
     by (unfold_locales) (simp del: comp_apply)
 
   lemmas union_language = union.combine_language
   lemmas union_nodes_finite = union.combine_nodes_finite
   lemmas union_nodes_card = union.combine_nodes_card
 
   global_interpretation intersection_list: automaton_intersection_list_trace
     dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\<lambda> P w r p. infs P r"
     dgba.dgba dgba.alphabet dgba.initial dgba.transition dgba.accepting "\<lambda> P w r p. gen infs P r"
     "\<lambda> cs. map (\<lambda> k pp. (cs ! k) (pp ! k)) [0 ..< length cs]"
     defines intersect_list' = intersection_list.combine
     by (unfold_locales) (auto simp: gen_def comp_def)
 
   lemmas intersect_list'_language[simp] = intersection_list.combine_language[folded DGBA.language_def]
   lemmas intersect_list'_nodes_finite = intersection_list.combine_nodes_finite[folded DGBA.nodes_def]
   lemmas intersect_list'_nodes_card = intersection_list.combine_nodes_card[folded DGBA.nodes_def]
 
   global_interpretation union_list: automaton_union_list_trace
     dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\<lambda> P w r p. infs P r"
     dba.dba dba.alphabet dba.initial dba.transition dba.accepting "\<lambda> P w r p. infs P r"
     "\<lambda> cs pp. \<exists> k < length cs. (cs ! k) (pp ! k)"
     defines union_list = union_list.combine
     by (unfold_locales) (simp add: comp_def)
 
   lemmas union_list_language = union_list.combine_language
   lemmas union_list_nodes_finite = union_list.combine_nodes_finite
   lemmas union_list_nodes_card = union_list.combine_nodes_card
 
   (* TODO: these compound definitions are annoying, can we move those into Deterministic theory *)
 
   abbreviation intersect where "intersect A B \<equiv> degeneralize (intersect' A B)"
 
   lemma intersect_language[simp]: "DBA.language (intersect A B) = DBA.language A \<inter> DBA.language B"
     by simp
   lemma intersect_nodes_finite:
     assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)"
     shows "finite (DBA.nodes (intersect A B))"
     using intersect'_nodes_finite assms by simp
   lemma intersect_nodes_card:
     assumes "finite (DBA.nodes A)" "finite (DBA.nodes B)"
     shows "card (DBA.nodes (intersect A B)) \<le> 2 * card (DBA.nodes A) * card (DBA.nodes B)"
   proof -
     have "card (DBA.nodes (intersect A B)) \<le>
       max 1 (length (dgba.accepting (intersect' A B))) * card (DGBA.nodes (intersect' A B))"
       using degeneralize_nodes_card by this
     also have "length (dgba.accepting (intersect' A B)) = 2" by simp
     also have "card (DGBA.nodes (intersect' A B)) \<le> card (DBA.nodes A) * card (DBA.nodes B)"
       using intersect'_nodes_card assms by this
     finally show ?thesis by simp
   qed
 
   abbreviation intersect_list where "intersect_list AA \<equiv> degeneralize (intersect_list' AA)"
 
   lemma intersect_list_language[simp]: "DBA.language (intersect_list AA) = \<Inter> (DBA.language ` set AA)"
     by simp
   lemma intersect_list_nodes_finite:
     assumes "list_all (finite \<circ> DBA.nodes) AA"
     shows "finite (DBA.nodes (intersect_list AA))"
     using intersect_list'_nodes_finite assms by simp
   lemma intersect_list_nodes_card:
     assumes "list_all (finite \<circ> DBA.nodes) AA"
     shows "card (DBA.nodes (intersect_list AA)) \<le> max 1 (length AA) * prod_list (map (card \<circ> DBA.nodes) AA)"
   proof -
     have "card (DBA.nodes (intersect_list AA)) \<le>
       max 1 (length (dgba.accepting (intersect_list' AA))) * card (DGBA.nodes (intersect_list' AA))"
       using degeneralize_nodes_card by this
     also have "length (dgba.accepting (intersect_list' AA)) = length AA" by simp
     also have "card (DGBA.nodes (intersect_list' AA)) \<le> prod_list (map (card \<circ> DBA.nodes) AA)"
       using intersect_list'_nodes_card assms by this
     finally show ?thesis by simp
   qed
 
 end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy
--- a/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy
@@ -1,109 +1,110 @@
 section \<open>Deterministic Co-Büchi Automata Combinations\<close>
 
 theory DCA_Combine
 imports DCA DGCA
 begin
 
   global_interpretation degeneralization: automaton_degeneralization_trace
     dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\<lambda> P w r p. cogen fins P r"
     dca dca.alphabet dca.initial dca.transition dca.rejecting "\<lambda> P w r p. fins P r"
+    fst id
     defines degeneralize = degeneralization.degeneralize
-    by unfold_locales auto
+    by (unfold_locales) (auto simp flip: sscan_smap)
 
   lemmas degeneralize_language[simp] = degeneralization.degeneralize_language[folded DCA.language_def]
   lemmas degeneralize_nodes_finite[iff] = degeneralization.degeneralize_nodes_finite[folded DCA.nodes_def]
   lemmas degeneralize_nodes_card = degeneralization.degeneralize_nodes_card[folded DCA.nodes_def]
 
   global_interpretation intersection: automaton_intersection_trace
     dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\<lambda> P w r p. fins P r"
     dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\<lambda> P w r p. fins P r"
     dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\<lambda> P w r p. fins P r"
     "\<lambda> c\<^sub>1 c\<^sub>2 pq. (c\<^sub>1 \<circ> fst) pq \<or> (c\<^sub>2 \<circ> snd) pq"
     defines intersect = intersection.combine
     by (unfold_locales) (simp del: comp_apply)
 
   lemmas intersect_language = intersection.combine_language
   lemmas intersect_nodes_finite = intersection.combine_nodes_finite
   lemmas intersect_nodes_card = intersection.combine_nodes_card
 
   global_interpretation union: automaton_union_trace
     dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\<lambda> P w r p. fins P r"
     dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\<lambda> P w r p. fins P r"
     dgca.dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\<lambda> P w r p. cogen fins P r"
     "\<lambda> c\<^sub>1 c\<^sub>2. [c\<^sub>1 \<circ> fst, c\<^sub>2 \<circ> snd]"
     defines union' = union.combine
     by unfold_locales auto
 
   lemmas union'_language[simp] = union.combine_language[folded DGCA.language_def]
   lemmas union'_nodes_finite = union.combine_nodes_finite[folded DGCA.nodes_def]
   lemmas union'_nodes_card = union.combine_nodes_card[folded DGCA.nodes_def]
 
   global_interpretation intersection_list: automaton_intersection_list_trace
     dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\<lambda> P w r p. fins P r"
     dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\<lambda> P w r p. fins P r"
     "\<lambda> cs pp. \<exists> k < length cs. (cs ! k) (pp ! k)"
     defines intersect_list = intersection_list.combine
     by (unfold_locales) (simp add: comp_def)
 
   lemmas intersect_list_language = intersection_list.combine_language
   lemmas intersect_list_nodes_finite = intersection_list.combine_nodes_finite
   lemmas intersect_list_nodes_card = intersection_list.combine_nodes_card
 
   global_interpretation union_list: automaton_union_list_trace
     dca.dca dca.alphabet dca.initial dca.transition dca.rejecting "\<lambda> P w r p. fins P r"
     dgca.dgca dgca.alphabet dgca.initial dgca.transition dgca.rejecting "\<lambda> P w r p. cogen fins P r"
     "\<lambda> cs. map (\<lambda> k pp. (cs ! k) (pp ! k)) [0 ..< length cs]"
     defines union_list' = union_list.combine
     by (unfold_locales) (auto simp: cogen_def comp_def)
 
   lemmas union_list'_language[simp] = union_list.combine_language[folded DGCA.language_def]
   lemmas union_list'_nodes_finite = union_list.combine_nodes_finite[folded DGCA.nodes_def]
   lemmas union_list'_nodes_card = union_list.combine_nodes_card[folded DGCA.nodes_def]
 
   abbreviation union where "union A B \<equiv> degeneralize (union' A B)"
 
   lemma union_language[simp]:
     assumes "dca.alphabet A = dca.alphabet B"
     shows "DCA.language (union A B) = DCA.language A \<union> DCA.language B"
     using assms by simp
   lemma union_nodes_finite:
     assumes "finite (DCA.nodes A)" "finite (DCA.nodes B)"
     shows "finite (DCA.nodes (union A B))"
     using union'_nodes_finite assms by simp
   lemma union_nodes_card:
     assumes "finite (DCA.nodes A)" "finite (DCA.nodes B)"
     shows "card (DCA.nodes (union A B)) \<le> 2 * card (DCA.nodes A) * card (DCA.nodes B)"
   proof -
     have "card (DCA.nodes (union A B)) \<le>
       max 1 (length (dgca.rejecting (union' A B))) * card (DGCA.nodes (union' A B))"
       using degeneralize_nodes_card by this
     also have "length (dgca.rejecting (union' A B)) = 2" by simp
     also have "card (DGCA.nodes (union' A B)) \<le> card (DCA.nodes A) * card (DCA.nodes B)"
       using union'_nodes_card assms by this
     finally show ?thesis by simp
   qed
 
   abbreviation union_list where "union_list AA \<equiv> degeneralize (union_list' AA)"
 
   lemma union_list_language[simp]:
     assumes "\<Inter> (dca.alphabet ` set AA) = \<Union> (dca.alphabet ` set AA)"
     shows "DCA.language (union_list AA) = \<Union> (DCA.language ` set AA)"
     using assms by simp
   lemma union_list_nodes_finite:
     assumes "list_all (finite \<circ> DCA.nodes) AA"
     shows "finite (DCA.nodes (union_list AA))"
     using union_list'_nodes_finite assms by simp
   lemma union_list_nodes_card:
     assumes "list_all (finite \<circ> DCA.nodes) AA"
     shows "card (DCA.nodes (union_list AA)) \<le> max 1 (length AA) * prod_list (map (card \<circ> DCA.nodes) AA)"
   proof -
     have "card (DCA.nodes (union_list AA)) \<le>
       max 1 (length (dgca.rejecting (union_list' AA))) * card (DGCA.nodes (union_list' AA))"
       using degeneralize_nodes_card by this
     also have "length (dgca.rejecting (union_list' AA)) = length AA" by simp
     also have "card (DGCA.nodes (union_list' AA)) \<le> prod_list (map (card \<circ> DCA.nodes) AA)"
       using union_list'_nodes_card assms by this
     finally show ?thesis by simp
   qed
 
 end
\ No newline at end of file
diff --git a/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy b/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy
--- a/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy
+++ b/thys/Transition_Systems_and_Automata/Automata/Deterministic.thy
@@ -1,557 +1,564 @@
 theory Deterministic
 imports
   "../Transition_Systems/Transition_System"
   "../Transition_Systems/Transition_System_Extra"
   "../Transition_Systems/Transition_System_Construction"
   "../Basic/Degeneralization"
 begin
 
   type_synonym ('label, 'state) trans = "'label \<Rightarrow> 'state \<Rightarrow> 'state"
 
   (* TODO: is there a way to be less verbose in these locales? do we need to specify all the types? *)
   locale automaton =
     fixes automaton :: "'label set \<Rightarrow> 'state \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition \<Rightarrow> 'automaton"
     fixes alphabet :: "'automaton \<Rightarrow> 'label set"
     fixes initial :: "'automaton \<Rightarrow> 'state"
     fixes transition :: "'automaton \<Rightarrow> ('label, 'state) trans"
     fixes condition :: "'automaton \<Rightarrow> 'condition"
     assumes automaton[simp]: "automaton (alphabet A) (initial A) (transition A) (condition A) = A"
     assumes alphabet[simp]: "alphabet (automaton a i t c) = a"
     assumes initial[simp]: "initial (automaton a i t c) = i"
     assumes transition[simp]: "transition (automaton a i t c) = t"
     assumes condition[simp]: "condition (automaton a i t c) = c"
   begin
 
     (* TODO: is there a way to use defines without renaming the constants? *)
     sublocale transition_system_initial
       "transition A" "\<lambda> a p. a \<in> alphabet A" "\<lambda> p. p = initial A"
       for A
       defines path' = path and run' = run and reachable' = reachable and nodes' = nodes
       by this
 
     (* TODO: maybe this should be stated in terms of the lists and streams constants (adjust language_alphabet proof) *)
     lemma path_alt_def: "path A w p \<longleftrightarrow> set w \<subseteq> alphabet A"
     unfolding lists_iff_set[symmetric]
     proof
       show "w \<in> lists (alphabet A)" if "path A w p" using that by (induct arbitrary: p) (auto)
       show "path A w p" if "w \<in> lists (alphabet A)" using that by (induct arbitrary: p) (auto)
     qed
     lemma run_alt_def: "run A w p \<longleftrightarrow> sset w \<subseteq> alphabet A"
     unfolding streams_iff_sset[symmetric]
     proof
       show "w \<in> streams (alphabet A)" if "run A w p"
         using that by (coinduction arbitrary: w p) (force elim: run.cases)
       show "run A w p" if "w \<in> streams (alphabet A)"
         using that by (coinduction arbitrary: w p) (force elim: streams.cases)
     qed
 
   end
 
   (* TODO: create analogous locale for DFAs (automaton_path) *)
   locale automaton_trace =
     automaton automaton alphabet initial transition condition
     for automaton :: "'label set \<Rightarrow> 'state \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition \<Rightarrow> 'automaton"
     and alphabet :: "'automaton \<Rightarrow> 'label set"
     and initial :: "'automaton \<Rightarrow> 'state"
     and transition :: "'automaton \<Rightarrow> ('label, 'state) trans"
     and condition :: "'automaton \<Rightarrow> 'condition"
     +
     fixes test :: "'condition \<Rightarrow> 'label stream \<Rightarrow> 'state stream \<Rightarrow> 'state \<Rightarrow> bool"
   begin
 
     definition language :: "'automaton \<Rightarrow> 'label stream set" where
       "language A \<equiv> {w. run A w (initial A) \<and> test (condition A) w (trace A w (initial A)) (initial A)}"
   
     lemma language[intro]:
       assumes "run A w (initial A)" "test (condition A) w (trace A w (initial A)) (initial A)"
       shows "w \<in> language A"
       using assms unfolding language_def by auto
     lemma language_elim[elim]:
       assumes "w \<in> language A"
       obtains "run A w (initial A)" "test (condition A) w (trace A w (initial A)) (initial A)"
       using assms unfolding language_def by auto
   
     lemma language_alphabet: "language A \<subseteq> streams (alphabet A)"
       unfolding language_def run_alt_def using sset_streams by auto
 
   end
 
   locale automaton_degeneralization =
     a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 +
     b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2
-    for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'state pred gen \<Rightarrow> 'automaton\<^sub>1"
+    for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'item pred gen \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state) trans"
-    and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state pred gen"
-    and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state degen \<Rightarrow> ('label, 'state degen) trans \<Rightarrow> 'state degen pred \<Rightarrow> 'automaton\<^sub>2"
+    and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'item pred gen"
+    and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state degen \<Rightarrow> ('label, 'state degen) trans \<Rightarrow> 'item_degen pred \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state degen"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state degen) trans"
-    and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state degen pred"
+    and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'item_degen pred"
+    +
+    fixes item :: "'state \<times> 'label \<times> 'state \<Rightarrow> 'item"
+    fixes translate :: "'item_degen \<Rightarrow> 'item degen"
   begin
 
     definition degeneralize :: "'automaton\<^sub>1 \<Rightarrow> 'automaton\<^sub>2" where
       "degeneralize A \<equiv> automaton\<^sub>2
         (alphabet\<^sub>1 A)
         (initial\<^sub>1 A, 0)
-        (\<lambda> a (p, k). (transition\<^sub>1 A a p, count (condition\<^sub>1 A) p k))
-        (degen (condition\<^sub>1 A))"
+        (\<lambda> a (p, k). (transition\<^sub>1 A a p, count (condition\<^sub>1 A) (item (p, a, transition\<^sub>1 A a p)) k))
+        (degen (condition\<^sub>1 A) \<circ> translate)"
 
     lemma degeneralize_simps[simp]:
       "alphabet\<^sub>2 (degeneralize A) = alphabet\<^sub>1 A"
       "initial\<^sub>2 (degeneralize A) = (initial\<^sub>1 A, 0)"
-      "transition\<^sub>2 (degeneralize A) a (p, k) = (transition\<^sub>1 A a p, count (condition\<^sub>1 A) p k)"
-      "condition\<^sub>2 (degeneralize A) = degen (condition\<^sub>1 A)"
+      "transition\<^sub>2 (degeneralize A) a (p, k) =
+        (transition\<^sub>1 A a p, count (condition\<^sub>1 A) (item (p, a, transition\<^sub>1 A a p)) k)"
+      "condition\<^sub>2 (degeneralize A) = degen (condition\<^sub>1 A) \<circ> translate"
       unfolding degeneralize_def by auto
 
     lemma degeneralize_target[simp]: "b.target (degeneralize A) w (p, k) =
-      (a.target A w p, fold (count (condition\<^sub>1 A)) (butlast (p # a.states A w p)) k)"
+      (a.target A w p, fold (count (condition\<^sub>1 A) \<circ> item) (p # a.states A w p || w || a.states A w p) k)"
       by (induct w arbitrary: p k) (auto)
     lemma degeneralize_states[simp]: "b.states (degeneralize A) w (p, k) =
-      a.states A w p || scan (count (condition\<^sub>1 A)) (p # a.states A w p) k"
+      a.states A w p || scan (count (condition\<^sub>1 A) \<circ> item) (p # a.states A w p || w || a.states A w p) k"
       by (induct w arbitrary: p k) (auto)
     lemma degeneralize_trace[simp]: "b.trace (degeneralize A) w (p, k) =
-      a.trace A w p ||| sscan (count (condition\<^sub>1 A)) (p ## a.trace A w p) k"
-      by (coinduction arbitrary: w p k) (auto)
+      a.trace A w p ||| sscan (count (condition\<^sub>1 A) \<circ> item) (p ## a.trace A w p ||| w ||| a.trace A w p) k"
+      by (coinduction arbitrary: w p k) (auto, metis sscan.code)
 
     lemma degeneralize_path[iff]: "b.path (degeneralize A) w (p, k) \<longleftrightarrow> a.path A w p"
       unfolding a.path_alt_def b.path_alt_def by simp
     lemma degeneralize_run[iff]: "b.run (degeneralize A) w (p, k) \<longleftrightarrow> a.run A w p"
       unfolding a.run_alt_def b.run_alt_def by simp
 
     lemma degeneralize_reachable_fst[simp]: "fst ` b.reachable (degeneralize A) (p, k) = a.reachable A p"
       unfolding a.reachable_alt_def b.reachable_alt_def image_def by simp
     lemma degeneralize_reachable_snd_empty[simp]:
       assumes "condition\<^sub>1 A = []"
       shows "snd ` b.reachable (degeneralize A) (p, k) = {k}"
     proof -
       have "snd ql = k" if "ql \<in> b.reachable (degeneralize A) (p, k)" for ql
         using that assms by induct auto
       then show ?thesis by auto
     qed
     lemma degeneralize_reachable_empty[simp]:
       assumes "condition\<^sub>1 A = []"
       shows "b.reachable (degeneralize A) (p, k) = a.reachable A p \<times> {k}"
       using degeneralize_reachable_fst degeneralize_reachable_snd_empty assms
       by (metis prod_singleton(2))
     lemma degeneralize_reachable_snd:
       "snd ` b.reachable (degeneralize A) (p, k) \<subseteq> insert k {0 ..< length (condition\<^sub>1 A)}"
       by (cases "condition\<^sub>1 A = []") (auto)
     lemma degeneralize_reachable:
       "b.reachable (degeneralize A) (p, k) \<subseteq> a.reachable A p \<times> insert k {0 ..< length (condition\<^sub>1 A)}"
       by (cases "condition\<^sub>1 A = []") (auto 0 3)
 
     lemma degeneralize_nodes_fst[simp]: "fst ` b.nodes (degeneralize A) = a.nodes A"
       unfolding a.nodes_alt_def b.nodes_alt_def by simp
     lemma degeneralize_nodes_snd_empty:
       assumes "condition\<^sub>1 A = []"
       shows "snd ` b.nodes (degeneralize A) = {0}"
       using assms unfolding b.nodes_alt_def by auto
     lemma degeneralize_nodes_empty:
       assumes "condition\<^sub>1 A = []"
       shows "b.nodes (degeneralize A) = a.nodes A \<times> {0}"
       using assms unfolding b.nodes_alt_def by auto
     lemma degeneralize_nodes_snd:
       "snd ` b.nodes (degeneralize A) \<subseteq> insert 0 {0 ..< length (condition\<^sub>1 A)}"
       using degeneralize_reachable_snd unfolding b.nodes_alt_def by auto
     lemma degeneralize_nodes:
       "b.nodes (degeneralize A) \<subseteq> a.nodes A \<times> insert 0 {0 ..< length (condition\<^sub>1 A)}"
       using degeneralize_reachable unfolding a.nodes_alt_def b.nodes_alt_def by simp
   
     lemma degeneralize_nodes_finite[iff]: "finite (b.nodes (degeneralize A)) \<longleftrightarrow> finite (a.nodes A)"
     proof
       show "finite (a.nodes A)" if "finite (b.nodes (degeneralize A))"
         using that by (auto simp flip: degeneralize_nodes_fst)
       show "finite (b.nodes (degeneralize A))" if "finite (a.nodes A)"
         using finite_subset degeneralize_nodes that by blast
     qed
     lemma degeneralize_nodes_card: "card (b.nodes (degeneralize A)) \<le>
       max 1 (length (condition\<^sub>1 A)) * card (a.nodes A)"
     proof (cases "finite (a.nodes A)")
       case True
       have "card (b.nodes (degeneralize A)) \<le> card (a.nodes A \<times> insert 0 {0 ..< length (condition\<^sub>1 A)})"
         using degeneralize_nodes True by (blast intro: card_mono)
       also have "\<dots> = card (insert 0 {0 ..< length (condition\<^sub>1 A)}) * card (a.nodes A)"
         unfolding card_cartesian_product by simp
       also have "card (insert 0 {0 ..< length (condition\<^sub>1 A)}) = max 1 (length (condition\<^sub>1 A))"
         by (simp add: card_insert_if Suc_leI max_absorb2)
       finally show ?thesis by this
     next
       case False
       then have "card (a.nodes A) = 0" "card (b.nodes (degeneralize A)) = 0" by auto
       then show ?thesis by simp
     qed
 
   end
 
   locale automaton_degeneralization_trace =
     automaton_degeneralization
       automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1
-      automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 +
+      automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2
+      item translate +
     a: automaton_trace automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 +
     b: automaton_trace automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2
-    for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'state pred gen \<Rightarrow> 'automaton\<^sub>1"
+    for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'item pred gen \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state) trans"
-    and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state pred gen"
-    and test\<^sub>1 :: "'state pred gen \<Rightarrow> 'label stream \<Rightarrow> 'state stream \<Rightarrow> 'state \<Rightarrow> bool"
-    and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state degen \<Rightarrow> ('label, 'state degen) trans \<Rightarrow> 'state degen pred \<Rightarrow> 'automaton\<^sub>2"
+    and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'item pred gen"
+    and test\<^sub>1 :: "'item pred gen \<Rightarrow> 'label stream \<Rightarrow> 'state stream \<Rightarrow> 'state \<Rightarrow> bool"
+    and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state degen \<Rightarrow> ('label, 'state degen) trans \<Rightarrow> 'item_degen pred \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state degen"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state degen) trans"
-    and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state degen pred"
-    and test\<^sub>2 :: "'state degen pred \<Rightarrow> 'label stream \<Rightarrow> 'state degen stream \<Rightarrow> 'state degen \<Rightarrow> bool"
+    and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'item_degen pred"
+    and test\<^sub>2 :: "'item_degen pred \<Rightarrow> 'label stream \<Rightarrow> 'state degen stream \<Rightarrow> 'state degen \<Rightarrow> bool"
+    and item :: "'state \<times> 'label \<times> 'state \<Rightarrow> 'item"
+    and translate :: "'item_degen \<Rightarrow> 'item degen"
     +
-    assumes test[iff]: "test\<^sub>2 (degen cs) w (r ||| sscan (count cs) (p ## r) k) (p, k) \<longleftrightarrow> test\<^sub>1 cs w r p"
+    assumes test[iff]: "test\<^sub>2 (degen cs \<circ> translate) w
+      (r ||| sscan (count cs \<circ> item) (p ## r ||| w ||| r) k) (p, k) \<longleftrightarrow> test\<^sub>1 cs w r p"
   begin
 
-    lemma degeneralize_language[simp]: "b.language (degeneralize A) = a.language A"
-      by (force simp del: sscan_scons)
+    lemma degeneralize_language[simp]: "b.language (degeneralize A) = a.language A" by force
 
   end
 
   locale automaton_combination =
     a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 +
     b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 +
     c: automaton automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state\<^sub>1 \<Rightarrow> ('label, 'state\<^sub>1) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state\<^sub>1"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state\<^sub>1) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>2) trans \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state\<^sub>2"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>2) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     and automaton\<^sub>3 :: "'label set \<Rightarrow> 'state\<^sub>1 \<times> 'state\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) trans \<Rightarrow>
       'condition\<^sub>3 \<Rightarrow> 'automaton\<^sub>3"
     and alphabet\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'label set"
     and initial\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'state\<^sub>1 \<times> 'state\<^sub>2"
     and transition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) trans"
     and condition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'condition\<^sub>3"
     +
     fixes condition :: "'condition\<^sub>1 \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'condition\<^sub>3"
   begin
 
     definition combine :: "'automaton\<^sub>1 \<Rightarrow> 'automaton\<^sub>2 \<Rightarrow> 'automaton\<^sub>3" where
       "combine A B \<equiv> automaton\<^sub>3
         (alphabet\<^sub>1 A \<inter> alphabet\<^sub>2 B)
         (initial\<^sub>1 A, initial\<^sub>2 B)
         (\<lambda> a (p, q). (transition\<^sub>1 A a p, transition\<^sub>2 B a q))
         (condition (condition\<^sub>1 A) (condition\<^sub>2 B))"
 
     lemma combine_simps[simp]:
       "alphabet\<^sub>3 (combine A B) = alphabet\<^sub>1 A \<inter> alphabet\<^sub>2 B"
       "initial\<^sub>3 (combine A B) = (initial\<^sub>1 A, initial\<^sub>2 B)"
       "transition\<^sub>3 (combine A B) a (p, q) = (transition\<^sub>1 A a p, transition\<^sub>2 B a q)"
       "condition\<^sub>3 (combine A B) = condition (condition\<^sub>1 A) (condition\<^sub>2 B)"
       unfolding combine_def by auto
 
     lemma combine_target[simp]: "c.target (combine A B) w (p, q) = (a.target A w p, b.target B w q)"
       by (induct w arbitrary: p q) (auto)
     lemma combine_states[simp]: "c.states (combine A B) w (p, q) = a.states A w p || b.states B w q"
       by (induct w arbitrary: p q) (auto)
     lemma combine_trace[simp]: "c.trace (combine A B) w (p, q) = a.trace A w p ||| b.trace B w q"
       by (coinduction arbitrary: w p q) (auto)
 
     lemma combine_path[iff]: "c.path (combine A B) w (p, q) \<longleftrightarrow> a.path A w p \<and> b.path B w q"
       unfolding a.path_alt_def b.path_alt_def c.path_alt_def by simp
     lemma combine_run[iff]: "c.run (combine A B) w (p, q) \<longleftrightarrow> a.run A w p \<and> b.run B w q"
       unfolding a.run_alt_def b.run_alt_def c.run_alt_def by simp
 
     lemma combine_reachable[simp]: "c.reachable (combine A B) (p, q) \<subseteq> a.reachable A p \<times> b.reachable B q"
       unfolding c.reachable_alt_def by auto
     lemma combine_nodes[simp]: "c.nodes (combine A B) \<subseteq> a.nodes A \<times> b.nodes B"
       unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def by auto
     lemma combine_reachable_fst[simp]:
       assumes "alphabet\<^sub>1 A \<subseteq> alphabet\<^sub>2 B"
       shows "fst ` c.reachable (combine A B) (p, q) = a.reachable A p"
       using assms
       unfolding a.reachable_alt_def a.path_alt_def
       unfolding b.reachable_alt_def b.path_alt_def
       unfolding c.reachable_alt_def c.path_alt_def
       by auto force
     lemma combine_reachable_snd[simp]:
       assumes "alphabet\<^sub>1 A \<supseteq> alphabet\<^sub>2 B"
       shows "snd ` c.reachable (combine A B) (p, q) = b.reachable B q"
       using assms
       unfolding a.reachable_alt_def a.path_alt_def
       unfolding b.reachable_alt_def b.path_alt_def
       unfolding c.reachable_alt_def c.path_alt_def
       by auto force
     lemma combine_nodes_fst[simp]:
       assumes "alphabet\<^sub>1 A \<subseteq> alphabet\<^sub>2 B"
       shows "fst ` c.nodes (combine A B) = a.nodes A"
       using assms combine_reachable_fst
       unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def
       by fastforce
     lemma combine_nodes_snd[simp]:
       assumes "alphabet\<^sub>1 A \<supseteq> alphabet\<^sub>2 B"
       shows "snd ` c.nodes (combine A B) = b.nodes B"
       using assms combine_reachable_snd
       unfolding a.nodes_alt_def b.nodes_alt_def c.nodes_alt_def
       by fastforce
 
     lemma combine_nodes_finite[intro]:
       assumes "finite (a.nodes A)" "finite (b.nodes B)"
       shows "finite (c.nodes (combine A B))"
     proof (rule finite_subset)
       show "c.nodes (combine A B) \<subseteq> a.nodes A \<times> b.nodes B" using combine_nodes by this
       show "finite (a.nodes A \<times> b.nodes B)" using assms by simp
     qed
     lemma combine_nodes_finite_strong[iff]:
       assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B"
       shows "finite (c.nodes (combine A B)) \<longleftrightarrow> finite (a.nodes A) \<and> finite (b.nodes B)"
     proof safe
       show "finite (a.nodes A)" if "finite (c.nodes (combine A B))"
         using combine_nodes_fst assms that by (metis finite_imageI equalityD1)
       show "finite (b.nodes B)" if "finite (c.nodes (combine A B))"
         using combine_nodes_snd assms that by (metis finite_imageI equalityD2)
       show "finite (c.nodes (combine A B))" if "finite (a.nodes A)" "finite (b.nodes B)"
         using that by rule
     qed
     lemma combine_nodes_card[intro]:
       assumes "finite (a.nodes A)" "finite (b.nodes B)"
       shows "card (c.nodes (combine A B)) \<le> card (a.nodes A) * card (b.nodes B)"
     proof -
       have "card (c.nodes (combine A B)) \<le> card (a.nodes A \<times> b.nodes B)"
       proof (rule card_mono)
         show "finite (a.nodes A \<times> b.nodes B)" using assms by simp
         show "c.nodes (combine A B) \<subseteq> a.nodes A \<times> b.nodes B" using combine_nodes by this
       qed
       also have "\<dots> = card (a.nodes A) * card (b.nodes B)" using card_cartesian_product by this
       finally show ?thesis by this
     qed
     lemma combine_nodes_card_strong[intro]:
       assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B"
       shows "card (c.nodes (combine A B)) \<le> card (a.nodes A) * card (b.nodes B)"
     proof (cases "finite (a.nodes A) \<and> finite (b.nodes B)")
       case True
       show ?thesis using True by auto
     next
       case False
       have 1: "card (c.nodes (combine A B)) = 0" using False assms by simp
       have 2: "card (a.nodes A) * card (b.nodes B) = 0" using False by auto
       show ?thesis using 1 2 by simp
     qed
 
   end
 
   locale automaton_intersection_trace =
     automaton_combination
       automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1
       automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2
       automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition +
     a: automaton_trace automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 +
     b: automaton_trace automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 +
     c: automaton_trace automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state\<^sub>1 \<Rightarrow> ('label, 'state\<^sub>1) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state\<^sub>1"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state\<^sub>1) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and test\<^sub>1 :: "'condition\<^sub>1 \<Rightarrow> 'label stream \<Rightarrow> 'state\<^sub>1 stream \<Rightarrow> 'state\<^sub>1 \<Rightarrow> bool"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>2) trans \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state\<^sub>2"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>2) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     and test\<^sub>2 :: "'condition\<^sub>2 \<Rightarrow> 'label stream \<Rightarrow> 'state\<^sub>2 stream \<Rightarrow> 'state\<^sub>2 \<Rightarrow> bool"
     and automaton\<^sub>3 :: "'label set \<Rightarrow> 'state\<^sub>1 \<times> 'state\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) trans \<Rightarrow>
       'condition\<^sub>3 \<Rightarrow> 'automaton\<^sub>3"
     and alphabet\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'label set"
     and initial\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'state\<^sub>1 \<times> 'state\<^sub>2"
     and transition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) trans"
     and condition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'condition\<^sub>3"
     and test\<^sub>3 :: "'condition\<^sub>3 \<Rightarrow> 'label stream \<Rightarrow> ('state\<^sub>1 \<times> 'state\<^sub>2) stream \<Rightarrow> 'state\<^sub>1 \<times> 'state\<^sub>2 \<Rightarrow> bool"
     and condition :: "'condition\<^sub>1 \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'condition\<^sub>3"
     +
     assumes test[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (r ||| s) (p, q) \<longleftrightarrow> test\<^sub>1 c\<^sub>1 w r p \<and> test\<^sub>2 c\<^sub>2 w s q"
   begin
 
     lemma combine_language[simp]: "c.language (combine A B) = a.language A \<inter> b.language B" by force
 
   end
 
   locale automaton_union_trace =
     automaton_combination
       automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1
       automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2
       automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 condition +
     a: automaton_trace automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 +
     b: automaton_trace automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2 +
     c: automaton_trace automaton\<^sub>3 alphabet\<^sub>3 initial\<^sub>3 transition\<^sub>3 condition\<^sub>3 test\<^sub>3
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state\<^sub>1 \<Rightarrow> ('label, 'state\<^sub>1) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state\<^sub>1"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state\<^sub>1) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and test\<^sub>1 :: "'condition\<^sub>1 \<Rightarrow> 'label stream \<Rightarrow> 'state\<^sub>1 stream \<Rightarrow> 'state\<^sub>1 \<Rightarrow> bool"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>2) trans \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state\<^sub>2"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>2) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     and test\<^sub>2 :: "'condition\<^sub>2 \<Rightarrow> 'label stream \<Rightarrow> 'state\<^sub>2 stream \<Rightarrow> 'state\<^sub>2 \<Rightarrow> bool"
     and automaton\<^sub>3 :: "'label set \<Rightarrow> 'state\<^sub>1 \<times> 'state\<^sub>2 \<Rightarrow> ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) trans \<Rightarrow>
       'condition\<^sub>3 \<Rightarrow> 'automaton\<^sub>3"
     and alphabet\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'label set"
     and initial\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'state\<^sub>1 \<times> 'state\<^sub>2"
     and transition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> ('label, 'state\<^sub>1 \<times> 'state\<^sub>2) trans"
     and condition\<^sub>3 :: "'automaton\<^sub>3 \<Rightarrow> 'condition\<^sub>3"
     and test\<^sub>3 :: "'condition\<^sub>3 \<Rightarrow> 'label stream \<Rightarrow> ('state\<^sub>1 \<times> 'state\<^sub>2) stream \<Rightarrow> 'state\<^sub>1 \<times> 'state\<^sub>2 \<Rightarrow> bool"
     and condition :: "'condition\<^sub>1 \<Rightarrow> 'condition\<^sub>2 \<Rightarrow> 'condition\<^sub>3"
     +
     assumes test[iff]: "test\<^sub>3 (condition c\<^sub>1 c\<^sub>2) w (r ||| s) (p, q) \<longleftrightarrow> test\<^sub>1 c\<^sub>1 w r p \<or> test\<^sub>2 c\<^sub>2 w s q"
   begin
 
     lemma combine_language[simp]:
       assumes "alphabet\<^sub>1 A = alphabet\<^sub>2 B"
       shows "c.language (combine A B) = a.language A \<union> b.language B"
       using assms by (force simp: a.run_alt_def b.run_alt_def)
 
   end
 
   (* TODO: complete this in analogy to the pair case *)
   locale automaton_combination_list =
     a: automaton automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 +
     b: automaton automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state list \<Rightarrow> ('label, 'state list) trans \<Rightarrow>
       'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state list"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state list) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     +
     fixes condition :: "'condition\<^sub>1 list \<Rightarrow> 'condition\<^sub>2"
   begin
 
     definition combine :: "'automaton\<^sub>1 list \<Rightarrow> 'automaton\<^sub>2" where
       "combine AA \<equiv> automaton\<^sub>2
         (\<Inter> (alphabet\<^sub>1 ` set AA))
         (map initial\<^sub>1 AA)
         (\<lambda> a pp. map2 (\<lambda> A p. transition\<^sub>1 A a p) AA pp)
         (condition (map condition\<^sub>1 AA))"
 
     lemma combine_simps[simp]:
       "alphabet\<^sub>2 (combine AA) = \<Inter> (alphabet\<^sub>1 ` set AA)"
       "initial\<^sub>2 (combine AA) = map initial\<^sub>1 AA"
       "transition\<^sub>2 (combine AA) a pp = map2 (\<lambda> A p. transition\<^sub>1 A a p) AA pp"
       "condition\<^sub>2 (combine AA) = condition (map condition\<^sub>1 AA)"
       unfolding combine_def by auto
 
     (* TODO: get rid of indices, express this using stranspose and listset *)
     lemma combine_trace_smap:
       assumes "length pp = length AA" "k < length AA"
       shows "smap (\<lambda> pp. pp ! k) (b.trace (combine AA) w pp) = a.trace (AA ! k) w (pp ! k)"
       using assms by (coinduction arbitrary: w pp) (force)
     lemma combine_nodes_length:
       assumes "pp \<in> b.nodes (combine AA)"
       shows "length pp = length AA"
       using assms by induct auto
     lemma combine_nodes[intro]:
       assumes "pp \<in> b.nodes (combine AA)" "k < length pp"
       shows "pp ! k \<in> a.nodes (AA ! k)"
       using assms by induct auto
 
     lemma combine_nodes_finite[intro]:
       assumes "list_all (finite \<circ> a.nodes) AA"
       shows "finite (b.nodes (combine AA))"
     proof (rule finite_subset)
       (* TODO: this is used more than once, make top level theorem *)
       show "b.nodes (combine AA) \<subseteq> listset (map a.nodes AA)"
         by (force simp: listset_member list_all2_conv_all_nth combine_nodes_length)
       show "finite (listset (map a.nodes AA))" using list.pred_map assms by auto
     qed
     lemma combine_nodes_card:
       assumes "list_all (finite \<circ> a.nodes) AA"
       shows "card (b.nodes (combine AA)) \<le> prod_list (map (card \<circ> a.nodes) AA)"
     proof -
       have "card (b.nodes (combine AA)) \<le> card (listset (map a.nodes AA))"
       proof (rule card_mono)
         show "finite (listset (map a.nodes AA))" using list.pred_map assms by auto
         show "b.nodes (combine AA) \<subseteq> listset (map a.nodes AA)"
           by (force simp: listset_member list_all2_conv_all_nth combine_nodes_length)
       qed
       also have "\<dots> = prod_list (map (card \<circ> a.nodes) AA)" by simp
       finally show ?thesis by this
     qed
 
   end
 
   locale automaton_intersection_list_trace =
     automaton_combination_list
       automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1
       automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 condition +
     a: automaton_trace automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 +
     b: automaton_trace automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and test\<^sub>1 :: "'condition\<^sub>1 \<Rightarrow> 'label stream \<Rightarrow> 'state stream \<Rightarrow> 'state \<Rightarrow> bool"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state list \<Rightarrow> ('label, 'state list) trans \<Rightarrow>
       'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state list"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state list) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     and test\<^sub>2 :: "'condition\<^sub>2 \<Rightarrow> 'label stream \<Rightarrow> 'state list stream \<Rightarrow> 'state list \<Rightarrow> bool"
     and condition :: "'condition\<^sub>1 list \<Rightarrow> 'condition\<^sub>2"
     +
     assumes test[iff]: "test\<^sub>2 (condition cs) w rs ps \<longleftrightarrow>
       (\<forall> k < length cs. test\<^sub>1 (cs ! k) w (smap (\<lambda> ps. ps ! k) rs) (ps ! k))"
   begin
 
     lemma combine_language[simp]: "b.language (combine AA) = \<Inter> (a.language ` set AA)"
       unfolding a.language_def b.language_def
       unfolding a.run_alt_def b.run_alt_def
       by (fastforce simp: set_conv_nth combine_trace_smap)
 
   end
 
   locale automaton_union_list_trace =
     automaton_combination_list
       automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1
       automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 condition +
     a: automaton_trace automaton\<^sub>1 alphabet\<^sub>1 initial\<^sub>1 transition\<^sub>1 condition\<^sub>1 test\<^sub>1 +
     b: automaton_trace automaton\<^sub>2 alphabet\<^sub>2 initial\<^sub>2 transition\<^sub>2 condition\<^sub>2 test\<^sub>2
     for automaton\<^sub>1 :: "'label set \<Rightarrow> 'state \<Rightarrow> ('label, 'state) trans \<Rightarrow> 'condition\<^sub>1 \<Rightarrow> 'automaton\<^sub>1"
     and alphabet\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'label set"
     and initial\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'state"
     and transition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> ('label, 'state) trans"
     and condition\<^sub>1 :: "'automaton\<^sub>1 \<Rightarrow> 'condition\<^sub>1"
     and test\<^sub>1 :: "'condition\<^sub>1 \<Rightarrow> 'label stream \<Rightarrow> 'state stream \<Rightarrow> 'state \<Rightarrow> bool"
     and automaton\<^sub>2 :: "'label set \<Rightarrow> 'state list \<Rightarrow> ('label, 'state list) trans \<Rightarrow>
       'condition\<^sub>2 \<Rightarrow> 'automaton\<^sub>2"
     and alphabet\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'label set"
     and initial\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'state list"
     and transition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> ('label, 'state list) trans"
     and condition\<^sub>2 :: "'automaton\<^sub>2 \<Rightarrow> 'condition\<^sub>2"
     and test\<^sub>2 :: "'condition\<^sub>2 \<Rightarrow> 'label stream \<Rightarrow> 'state list stream \<Rightarrow> 'state list \<Rightarrow> bool"
     and condition :: "'condition\<^sub>1 list \<Rightarrow> 'condition\<^sub>2"
     +
     assumes test[iff]: "test\<^sub>2 (condition cs) w rs ps \<longleftrightarrow>
       (\<exists> k < length cs. test\<^sub>1 (cs ! k) w (smap (\<lambda> ps. ps ! k) rs) (ps ! k))"
   begin
 
     lemma combine_language[simp]:
       assumes "\<Inter> (alphabet\<^sub>1 ` set AA) = \<Union> (alphabet\<^sub>1 ` set AA)"
       shows "b.language (combine AA) = \<Union> (a.language ` set AA)"
       using assms
       unfolding a.language_def b.language_def
       unfolding a.run_alt_def b.run_alt_def
       by (fastforce simp: set_conv_nth combine_trace_smap)
 
   end
 
 end
\ No newline at end of file