# HG changeset patch
# User Chengsong
# Date 1568385551 -3600
# Node ID 97741a7b8b371717d35fa651bbd88b7d1785c79f
# Parent  eb08de92c4dcc1f66120872c46aa4f8b77eefebb
marked by QUESTION

diff -r eb08de92c4dc -r 97741a7b8b37 thys/BitCoded2CT.thy
--- a/thys/BitCoded2CT.thy	Fri Sep 13 13:50:54 2019 +0100
+++ b/thys/BitCoded2CT.thy	Fri Sep 13 15:39:11 2019 +0100
@@ -3085,8 +3085,15 @@
   apply auto
   done
 
+lemma derc_alt00:
+  assumes " bder c a >> bs" and "bder c (bsimp a) >> bs"
+  shows "bder c (bsimp_AALTs [] (flts [bsimp a])) >> bs"
+  oops
+
 lemma derc_alt:
-  assumes "bder c (AALTs [] as) >> bs"
+  assumes "bder c (AALTs [] as) >> bs" 
+(*QUESTION*)
+and "\<forall> a \<in> as. (bder c a >> bs) \<Rightarrow> (bder c (bsimp a) >> bs)"
   shows "bder c (bsimp(AALTs [] as)) >> bs"
   using assms
   apply -