--- a/thys/BitCodedCT.thy	Thu Aug 22 01:11:07 2019 +0200
+++ b/thys/BitCodedCT.thy	Thu Aug 22 09:40:48 2019 +0100
@@ -3010,6 +3010,37 @@
   apply(simp add: flts_append)
   done
 
+lemma hardest:
+  shows "bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]))) =
+       bsimp (AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2)))"
+  apply(case_tac "bsimp a1")
+       apply(case_tac "bsimp a2")
+            apply simp
+           apply simp
+  apply(rule_tac t="bsimp a1" 
+and s="AZERO" in subst)
+           apply simp
+  apply(rule_tac t="bsimp a2" 
+and s="ACHAR x31 x32" in subst)
+           apply simp
+          apply simp
+  apply(rule_tac t="bsimp a1" 
+and s="AZERO" in subst)
+           apply simp
+  apply(rule_tac t="bsimp a2" 
+and s="ASEQ x41 x42 x43" in subst)
+           apply simp
+         apply(case_tac "bnullable x42")
+          apply(simp only: bder.simps)
+          apply(simp)
+  apply(case_tac "flts
+              [bsimp_ASEQ [] (bsimp (bder c x42)) (bsimp x43),
+               bsimp (fuse (bmkeps x42) (bder c x43))]")
+           apply(simp)
+          apply simp
+(*counterexample finder*)
+
+
 lemma XXX2a_long_without_good:
   shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
   apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)