--- a/thys3/ClosedFormsBounds.thy	Fri Jul 01 13:02:15 2022 +0100
+++ b/thys3/ClosedFormsBounds.thy	Mon Jul 04 12:27:13 2022 +0100
@@ -2,6 +2,8 @@
 theory ClosedFormsBounds
   imports "GeneralRegexBound" "ClosedForms"
 begin
+
+
 lemma alts_ders_lambda_shape_ders:
   shows "\<forall>r \<in> set (map (\<lambda>r. rders_simp r ( s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 s"
   by (simp add: image_iff)
@@ -14,6 +16,12 @@
   apply simp
   by simp
 
+lemma distinct_list_size_len_bounded:
+  assumes "\<forall>r \<in> set rs. rsize r \<le> N" "length rs \<le> lrs"
+  shows "rsizes rs \<le> lrs * N "
+  using assms
+  by (metis rlist_bound dual_order.trans mult.commute mult_le_mono1)
+
 lemma alts_closed_form_bounded: 
   assumes "\<forall>r \<in> set rs. \<forall>s. rsize (rders_simp r s) \<le> N"
   shows "rsize (rders_simp (RALTS rs) s) \<le> max (Suc (N * (length rs))) (rsize (RALTS rs))"
@@ -310,11 +318,6 @@
   by (simp add: larger_acc_smaller_distinct_res)
 
 
-lemma distinct_list_size_len_bounded:
-  assumes "\<forall>r \<in> set rs. rsize r \<le> N" "length rs \<le> lrs"
-  shows "rsizes rs \<le> lrs * N "
-  using assms
-  by (metis rlist_bound dual_order.trans mult.commute mult_le_mono1)