250 lemma aux_aux_aux:

   251   shows "map rerase (flts (map bsimp rs)) = map rerase rs \<Longrightarrow> map rerase (map bsimp rs) = map rerase rs"

   252   oops

   253 

   254 inductive leq1 ("_ \<le>1 _" [80, 80] 80) where  

   255   "r1 \<le>1 r1"

   256 | "AZERO \<le>1 ASEQ bs AZERO r" 

   257 | "AZERO \<le>1 ASEQ bs r AZERO"

   258 | "fuse (bs @ bs1) r2 \<le>1 ASEQ bs (AONE bs1) r2"

   259 | " AALTs bs (rs1 @ rs) \<le>1 AALTs bs (rs1 @( AZERO # rs))"

   260 | "r2 \<le>1 r1 \<Longrightarrow> AALTs bs (rs1 @ r2 # rs) \<le>1 AALTs bs (rs1 @ r1 # rs)"

   261 | "AALTs bs1 (rsa @ (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs1 (rsa @ (AALTs bs1 rs1) # rsb)"

   262 | "rerase a1 = rerase a2 \<Longrightarrow> AALTs bs (rsa @ [a1] @ rsb @ rsc) \<le>1 AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc) "

   263 | "r1 \<le>1 r2 \<Longrightarrow> r1  \<le>1 ASEQ bs (AONE bs1) r2"

   264 

   265 lemma leq1_less_or_equal: shows

   266 "r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2"

   267   apply(induct rule: leq1.induct)

   268           apply simp+

   269   sorry

   270 

   271 lemma bsimp_leq1:

   272   shows "bsimp r \<le>1 r"

   273 

   274   sorry

   275 

   276 

   277 lemma arexpfiniteaux4_aux:

   278   shows" \<lbrakk>rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs) \<rbrakk>

   279        \<Longrightarrow> map rerase (map bsimp rs) = map rerase rs"

   280   apply(induct rs)

   281    apply simp

   282   apply simp

   283   apply auto

   284    prefer 2

   285 

   286   sorry

   287 

   288 lemma arexpfiniteaux4:

   289   shows"

   290        \<lbrakk>\<And>x. \<lbrakk>x \<in> set rs; rerase (bsimp x) = rerase x\<rbrakk> \<Longrightarrow> bsimp x = x;

   291         rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs)\<rbrakk>

   292        \<Longrightarrow> bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {}) = AALTs bs1 rs"

   293   apply(induct rs)

   294   apply simp

   295   

   296 

   297 

   298 

   299 

   300 

   301   sorry

   302 

   303 

   304 

   308   apply(induct rule: bsimp.induct)

   309         apply simp

   310         apply (smt (verit) arexpfiniteaux1 arexpfiniteaux2 arexpfiniteaux3 bsimp_ASEQ1 rerase.simps(5) rrexp.inject(2))

   311   apply simp

   312   

   313   using arexpfiniteaux4 apply blast

   314       apply simp+

   315   done

   316 (*

   332 *)

   333