--- a/thys4/posix/FBound.thy	Mon Aug 29 23:16:28 2022 +0100
+++ b/thys4/posix/FBound.thy	Tue Aug 30 12:41:52 2022 +0100
@@ -247,9 +247,73 @@
   apply simp
   done
 
+lemma aux_aux_aux:
+  shows "map rerase (flts (map bsimp rs)) = map rerase rs \<Longrightarrow> map rerase (map bsimp rs) = map rerase rs"
+  oops
+
+inductive leq1 ("_ \<le>1 _" [80, 80] 80) where  
+  "r1 \<le>1 r1"
+| "AZERO \<le>1 ASEQ bs AZERO r" 
+| "AZERO \<le>1 ASEQ bs r AZERO"
+| "fuse (bs @ bs1) r2 \<le>1 ASEQ bs (AONE bs1) r2"
+| " AALTs bs (rs1 @ rs) \<le>1 AALTs bs (rs1 @( AZERO # rs))"
+| "r2 \<le>1 r1 \<Longrightarrow> AALTs bs (rs1 @ r2 # rs) \<le>1 AALTs bs (rs1 @ r1 # rs)"
+| "AALTs bs1 (rsa @ (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs1 (rsa @ (AALTs bs1 rs1) # rsb)"
+| "rerase a1 = rerase a2 \<Longrightarrow> AALTs bs (rsa @ [a1] @ rsb @ rsc) \<le>1 AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc) "
+| "r1 \<le>1 r2 \<Longrightarrow> r1  \<le>1 ASEQ bs (AONE bs1) r2"
+
+lemma leq1_less_or_equal: shows
+"r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2"
+  apply(induct rule: leq1.induct)
+          apply simp+
+  sorry
+
+lemma bsimp_leq1:
+  shows "bsimp r \<le>1 r"
+
+  sorry
+
+
+lemma arexpfiniteaux4_aux:
+  shows" \<lbrakk>rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs) \<rbrakk>
+       \<Longrightarrow> map rerase (map bsimp rs) = map rerase rs"
+  apply(induct rs)
+   apply simp
+  apply simp
+  apply auto
+   prefer 2
+
+  sorry
+
+lemma arexpfiniteaux4:
+  shows"
+       \<lbrakk>\<And>x. \<lbrakk>x \<in> set rs; rerase (bsimp x) = rerase x\<rbrakk> \<Longrightarrow> bsimp x = x;
+        rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs)\<rbrakk>
+       \<Longrightarrow> bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {}) = AALTs bs1 rs"
+  apply(induct rs)
+  apply simp
+  
+
+
+
+
+
+  sorry
+
+
+
 
 lemma arexp_finite1:
   shows "rerase (bsimp b) = rerase b \<Longrightarrow> bsimp b = b"
+  apply(induct rule: bsimp.induct)
+        apply simp
+        apply (smt (verit) arexpfiniteaux1 arexpfiniteaux2 arexpfiniteaux3 bsimp_ASEQ1 rerase.simps(5) rrexp.inject(2))
+  apply simp
+  
+  using arexpfiniteaux4 apply blast
+      apply simp+
+  done
+(*
   apply(induct b)
         apply simp+
          apply(case_tac "bsimp b2 = AZERO")
@@ -265,6 +329,8 @@
   apply simp
 
   sorry
+*)
+
 
 lemma bitcodes_unchanging2:
   assumes "bsimp a = b"