--- a/thys2/ClosedFormsBounds.thy	Thu Mar 10 11:18:41 2022 +0000
+++ b/thys2/ClosedFormsBounds.thy	Thu Mar 10 15:53:46 2022 +0000
@@ -89,14 +89,46 @@
   
   sorry
 
+lemma rdistinct_equality1:
+  shows "a \<notin> ss \<Longrightarrow> rdistinct (a  # rs) ss = a # rdistinct rs (insert a ss) "
+  by auto
+
+lemma larger_acc_smaller_distinct_res0:
+  shows " ss \<subseteq> SS \<Longrightarrow> sum_list (map rsize (rdistinct rs SS)) \<le> sum_list (map rsize (rdistinct rs ss))"
+  apply(induct rs arbitrary: ss SS)
+  apply simp
+  apply(case_tac "a \<in> ss")
+   apply(subgoal_tac "a \<in> SS")
+    apply simp
+   apply blast
+  apply(case_tac "a \<in> SS")
+   apply simp
+   apply(subgoal_tac "insert a ss \<subseteq> SS")
+    apply simp
+  apply (simp add: trans_le_add2)
+  apply blast
+  apply(simp)
+  apply(subgoal_tac "insert a ss \<subseteq> insert a SS")
+   apply blast
+  by blast
+
+
+lemma larger_acc_smaller_distinct_res:
+  shows " (sum_list (map rsize (rdistinct rs ss))) \<ge> (sum_list (map rsize (rdistinct rs (insert a ss))))"
+  sorry
+
+lemma size_list_triangle1:
+  shows  "sum_list (map rsize (a # (rdistinct as ss))) \<ge> rsize a + sum_list (map rsize (rdistinct as (insert a ss)))"
+  by (simp add: larger_acc_smaller_distinct_res)
+
+
 lemma triangle_inequality_distinct:
   shows "sum_list (map rsize (rdistinct (a # rs) ss)) \<le> rsize a + (sum_list (map rsize (rdistinct rs ss)))"
-  apply(arbitrary: ss)
-   apply simp
   apply(case_tac "a \<in> ss")
    apply simp
-
-  sorry
+  apply(subst rdistinct_equality1)
+   apply simp
+  using size_list_triangle1 by auto
 
 lemma same_regex_property_after_map:
   shows "\<forall>s. P (f r2 s) \<Longrightarrow> \<forall>r \<in> set  (map (f r2) Ss). P r"