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

   249 | "r2 \<le>1 r1 \<Longrightarrow> ASEQ bs r  r2 \<le>1 ASEQ bs r r1"

   250 | "r2 \<le>1 r1 \<Longrightarrow> ASEQ bs r2 r  \<le>1 ASEQ bs r1 r"

   251 | "r \<le>1 r' \<Longrightarrow> ASTAR bs r \<le>1 ASTAR bs r'"

   252 | "AZERO \<le>1 AALTs bs []"

   253 | "fuse bs r \<le>1 AALTs bs [r]"

   254 | "\<lbrakk>r1' \<le>1 r1;  r2' \<le>1 r2\<rbrakk> \<Longrightarrow> bsimp_ASEQ bs1 r1' r2' \<le>1 ASEQ bs1 r1 r2"

   255 

   256 lemma stupid_leq1_1:

   257   shows " rerase  r2 \<noteq> RSEQ r (RSEQ RONE (rerase r2))"

   258   apply(induct r2)

   259         apply simp+

   260   done

   261 

   262 lemma leq1_size:

   263   shows "r1 \<le>1 r2 \<Longrightarrow> asize r1 \<le> asize r2"

   264   apply (induct rule: leq1.induct)

   265                apply simp+

   266   apply (metis asize_rsize le_SucI le_add2 plus_1_eq_Suc rerase_fuse)

   267            apply simp

   268           apply simp

   269   

   270           apply (metis (mono_tags, lifting) asize_rsize comp_apply dual_order.eq_iff le_SucI map_eq_conv rerase_fuse)

   271   apply simp+

   272   apply (metis Suc_n_not_le_n asize_rsize linorder_le_cases rerase_fuse)

   273   apply(case_tac "r1' = AZERO")

   274    apply simp

   275   apply(case_tac "\<exists>bs1. r1' = AONE bs1")

   276    apply(erule exE)

   277    apply simp

   278   apply (metis asize_rsize le_SucI rerase_fuse trans_le_add2)

   279   by (smt (verit, best) Suc_eq_plus1 ab_semigroup_add_class.add_ac(1) add.commute add.right_neutral add_cancel_right_right add_mono_thms_linordered_semiring(1) asize.simps(5) asize_rsize nat_add_left_cancel_le order.trans order_trans plus_1_eq_Suc rSEQ_mono rerase_bsimp_ASEQ rsize.simps(5))

   280 

   281 

   282 

   283 lemma size_deciding_equality:

   284   shows "asize r1 \<noteq> asize r2 \<Longrightarrow> r1 \<noteq> r2 "

   285   apply auto

   286   done

   287 

   288 lemma size_deciding_equality2:

   289   shows "rerase r1 = rerase r2 \<Longrightarrow> asize r1 = asize r2"

   290   by (metis asize_rsize)

   291 

   292 lemma size_deciding_equality3:

   293   shows "asize r1 \<noteq> asize r2 \<Longrightarrow> rerase r1 \<noteq> rerase r2"

   294   by (metis asize_rsize)

   295 

   296 lemma size_deciding_equality4:

   297   shows "rerase a1 = r2 \<Longrightarrow> asize a1 = rsize r2"

   298   by (metis asize_rsize)

   299 

   300 lemma size_deciding_equality5:

   301   shows "asize a1 \<noteq> rsize r2 \<Longrightarrow>rerase a1 \<noteq> r2"

   302   by (metis asize_rsize)

   303 

   304 lemma leq1_trans1:

   305   shows " r1 \<le>1 r2 \<Longrightarrow>  rerase r1 \<noteq> RSEQ r (rerase r2)"

   306   apply(induct rule: leq1.induct)

   307                apply simp+

   308   using rerase_fuse stupid_leq1_1 apply presburger

   309            apply simp+

   310         apply(subgoal_tac "asize r1 \<noteq> rsize (RSEQ r (RSEQ RONE (rerase r2)))")

   311   using size_deciding_equality5 apply blast

   312   using asize_rsize leq1_size apply fastforce

   313        apply simp+

   314   apply(subgoal_tac "rsize (rerase (fuse bs ra)) \<noteq> rsize (RSEQ r (RALTS [rerase ra]))")

   315   

   316   apply force

   317   apply simp

   318   apply(simp add: asize_rsize)

   319   by (simp add: rerase_fuse size_deciding_equality4)

   320 

   321   

   322 

   323   

   413   

   414   sorry

   415 

   416 

   417 

   418 lemma bsimp_reduces:

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

   420   apply(induct rule: bsimp.induct)

   421         apply simp

   455