1064 | "asize2 (AALTs cs rs) = Suc (Suc (sum_list (map asize2 rs)))"

  1064 | "asize2 (AALTs cs rs) = Suc (Suc (sum_list (map asize2 rs)))"

  1065 | "asize2 (ASEQ cs r1 r2) = Suc (asize2 r1 + asize2 r2)"

  1065 | "asize2 (ASEQ cs r1 r2) = Suc (asize2 r1 + asize2 r2)"

  1066 | "asize2 (ASTAR cs r) = Suc (asize2 r)"

  1066 | "asize2 (ASTAR cs r) = Suc (asize2 r)"

  1067 

  1067 

  1068 

  1068 

  1069 lemma asize2_fuse:

  1070 lemma asize2_fuse:

  1070   shows "asize2 (fuse bs r) = asize2 r"

  1071   shows "asize2 (fuse bs r) = asize2 r"

  1071   apply(induct r arbitrary: bs)

  1072   apply(induct r arbitrary: bs)

  1072   apply(auto)

  1073   apply(auto)

  1073   done

  1074   done

  1350     apply(rule order_trans)

  1351     apply(rule order_trans)

  1351      apply(rule card_Un_le)

  1352      apply(rule card_Un_le)

  1352   using binullable_intern apply blast

  1353   using binullable_intern apply blast

  1353   using binullable_intern apply blast

  1354   using binullable_intern apply blast

  1354   by (smt (verit, best) SEQs_eq_image add.commute add_Suc_right card_image_le dual_order.trans finite_pder trans_le_add2)

  1355   by (smt (verit, best) SEQs_eq_image add.commute add_Suc_right card_image_le dual_order.trans finite_pder trans_le_add2)

  1356 lemma

  1359 lemma

  1357   "card (pder c r) \<le> asize (bsimp (bder c (intern r)))"

  1360   "card (pder c r) \<le> asize (bsimp (bder c (intern r)))"

  1358   apply(induct c r rule: pder.induct)

  1361   apply(induct c r rule: pder.induct)

  1359        apply(simp)

  1362        apply(simp)

  1360       apply(simp)

  1363       apply(simp)

  1368      apply(rule pders_SEQs)

  1371      apply(rule pders_SEQs)

  1369   using finite_pder apply blast

  1372   using finite_pder apply blast

  1370   oops

  1373   oops

  1371   

  1374   

  1372 

  1375 

  1373 (* below is the idempotency of bsimp *)

  1378 (* below is the idempotency of bsimp *)

  1374 

  1379 

  1375 lemma bsimp_ASEQ_fuse:

  1380 lemma bsimp_ASEQ_fuse:

  1376   shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"

  1381   shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"

  1377   apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)

  1382   apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)