--- a/thys4/posix/FBound.thy	Sat Sep 10 22:30:22 2022 +0100
+++ b/thys4/posix/FBound.thy	Mon Sep 12 23:32:18 2022 +0200
@@ -560,7 +560,16 @@
 
 lemma scompsize_aux:
   shows "s_complexity (AALTs bs (rs1 @ distinctWith rs2 eq1 (set rs1))) \<le> s_complexity (AALTs bs (rs1 @ rs2))"
-  sorry
+  apply(induct rs2 arbitrary: rs1)
+   apply simp
+  apply simp
+  apply(case_tac "\<exists>x \<in> set rs1. a ~1 x")
+  using trans_le_add2 apply blast
+  apply simp
+  
+  by (metis List.set_insert)
+
+  
 
 
 
@@ -589,7 +598,28 @@
    apply auto
   by (metis eq_imp_le le_imp_less_Suc less_imp_le_nat rerase_fuse scomp_rerase2)
 
+lemma prf22:
+  shows "\<lbrakk>r1 \<le>1 r2; \<not> r1 ~1 r2\<rbrakk> \<Longrightarrow> s_complexity r1 \<noteq> s_complexity r2"
+  apply(induct rule:eq1.induct)
+                      apply simp+
+                      apply auto
 
+  sorry
+
+
+
+lemma compl_rrewrite_down1:
+  shows "r1 \<le>1 r2 \<Longrightarrow> r1 ~1 r2 \<or> s_complexity r1 < s_complexity r2"
+    apply(subgoal_tac "s_complexity r1 \<le> s_complexity r2")
+  apply(case_tac "r1 ~1 r2")
+    apply simp
+   apply(subgoal_tac "s_complexity r1 \<noteq> s_complexity r2")
+    apply simp
+  using prf22 apply blast
+  by (simp add: scomp_size_reduction)
+  
+lemma leq1_eq1_equal:
+  shows "\<lbrakk>r1 \<le>1 r2;
 
 
 
@@ -598,6 +628,7 @@
 
 lemma compl_rrewrite_down:
   shows "r1 \<le>1 r2 \<Longrightarrow>r1 = r2 \<or> s_complexity r1 < s_complexity r2"
+  apply(subgoal_tac "s_complexity r1 \<le> s_complexity r2")
   
   apply(induct rule: leq1.induct)
                     apply simp