equal
deleted
inserted
replaced
3083 lemma concat_def: |
3083 lemma concat_def: |
3084 shows"[]@lst=lst" |
3084 shows"[]@lst=lst" |
3085 apply auto |
3085 apply auto |
3086 done |
3086 done |
3087 |
3087 |
|
3088 lemma derc_alt00: |
|
3089 assumes " bder c a >> bs" and "bder c (bsimp a) >> bs" |
|
3090 shows "bder c (bsimp_AALTs [] (flts [bsimp a])) >> bs" |
|
3091 oops |
|
3092 |
3088 lemma derc_alt: |
3093 lemma derc_alt: |
3089 assumes "bder c (AALTs [] as) >> bs" |
3094 assumes "bder c (AALTs [] as) >> bs" |
|
3095 (*QUESTION*) |
|
3096 and "\<forall> a \<in> as. (bder c a >> bs) \<Rightarrow> (bder c (bsimp a) >> bs)" |
3090 shows "bder c (bsimp(AALTs [] as)) >> bs" |
3097 shows "bder c (bsimp(AALTs [] as)) >> bs" |
3091 using assms |
3098 using assms |
3092 apply - |
3099 apply - |
3093 using contains_equiv_def |
3100 using contains_equiv_def |
3094 apply - |
3101 apply - |