--- a/thys/BitCoded2.thy	Tue Aug 20 23:42:28 2019 +0200
+++ b/thys/BitCoded2.thy	Wed Aug 21 10:29:34 2019 +0200
@@ -3784,8 +3784,58 @@
   apply(simp)
   done
 
-
-
+lemma COUNTEREXAMPLE:
+  assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
+  shows "bsimp (bder c (bsimp r)) = bsimp (bder c r)"
+  apply(simp_all add: assms)
+  oops
+
+lemma COUNTEREXAMPLE:
+  assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
+  shows "bsimp r = r"
+  apply(simp_all add: assms)
+  oops
+
+lemma COUNTEREXAMPLE:
+  assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
+  shows "bsimp r = XXX"
+  and   "bder c r = XXX"
+  and   "bsimp (bder c (bsimp r)) = XXX"
+  and   "bsimp (bder c r) = XXX"
+  apply(simp_all add: assms)
+  oops
+
+lemma COUNTEREXAMPLE_contains1:
+  assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
+  and   "bsimp (bder c r) >> bs"
+  shows "bsimp (bder c (bsimp r)) >> bs"
+  using assms 
+  apply(auto elim!: contains.cases)
+   apply(rule Etrans)
+    apply(rule contains.intros)
+    apply(rule contains.intros)
+   apply(simp)
+  apply(rule Etrans)
+    apply(rule contains.intros)
+    apply(rule contains.intros)
+  apply(simp)
+  done
+
+lemma COUNTEREXAMPLE_contains2:
+  assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
+  and   "bsimp (bder c (bsimp r)) >> bs"
+  shows "bsimp (bder c r) >> bs" 
+  using assms 
+  apply(auto elim!: contains.cases)
+   apply(rule Etrans)
+    apply(rule contains.intros)
+    apply(rule contains.intros)
+   apply(simp)
+  apply(rule Etrans)
+    apply(rule contains.intros)
+    apply(rule contains.intros)
+  apply(simp)
+  done
 
 
 end
\ No newline at end of file