equal
deleted
inserted
replaced
104 shows "bmkeps (fuse bs r) = bs @ bmkeps r" |
104 shows "bmkeps (fuse bs r) = bs @ bmkeps r" |
105 using assms |
105 using assms |
106 apply(induct r rule: bnullable.induct) |
106 apply(induct r rule: bnullable.induct) |
107 apply(auto) |
107 apply(auto) |
108 apply (metis append.assoc bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
108 apply (metis append.assoc bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
109 apply(case_tac n) |
|
110 apply(auto) |
|
111 done |
109 done |
112 |
110 |
113 lemma bmkepss_fuse: |
111 lemma bmkepss_fuse: |
114 assumes "bnullables rs" |
112 assumes "bnullables rs" |
115 shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs" |
113 shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs" |