diff -r fd068f39ac23 -r ce4e5151a836 thys4/posix/FBound.thy
--- a/thys4/posix/FBound.thy	Mon Sep 12 23:32:18 2022 +0200
+++ b/thys4/posix/FBound.thy	Thu Sep 22 00:31:09 2022 +0100
@@ -619,7 +619,8 @@
   by (simp add: scomp_size_reduction)
   
 lemma leq1_eq1_equal:
-  shows "\<lbrakk>r1 \<le>1 r2;
+  shows "\<lbrakk>r1 \<le>1 r2; bsimp r2 = r1 \<rbrakk> \<Longrightarrow> r1 = r2 \<or> s_complexity r1 < s_complexity r2"
+  sorry