equal
deleted
inserted
replaced
277 using leq1.intros(1) leq1.intros(16) apply force |
277 using leq1.intros(1) leq1.intros(16) apply force |
278 apply (simp add: leq1.intros(1) leq1.intros(16)) |
278 apply (simp add: leq1.intros(1) leq1.intros(16)) |
279 using leq1.intros(1) leq1.intros(16) by force |
279 using leq1.intros(1) leq1.intros(16) by force |
280 |
280 |
281 lemma dB_leq12: |
281 lemma dB_leq12: |
282 shows "AALTs bs (distinctWith rs1 eq1 (set rs2)) \<le>1 AALTs bs (rs1 @ rs2)" |
282 shows "AALTs bs (rs1 @ (distinctWith rs1 eq1 (set rs2))) \<le>1 AALTs bs (rs1 @ rs2)" |
|
283 apply(induct rs1 arbitrary: rs2) |
|
284 apply simp |
283 sorry |
285 sorry |
284 |
286 |
285 |
287 |
286 lemma dB_leq1: |
288 lemma dB_leq1: |
287 shows "AALTs bs (distinctWith rs eq1 {}) \<le>1 AALTs bs rs" |
289 shows "AALTs bs (distinctWith rs eq1 {}) \<le>1 AALTs bs rs" |
288 by (metis append.right_neutral dB_leq12 list.set(1)) |
290 sorry |
|
291 |
289 |
292 |
290 |
293 |
291 |
294 |
292 lemma stupid_leq1_1: |
295 lemma stupid_leq1_1: |
293 shows " rerase r2 \<noteq> RSEQ r (RSEQ RONE (rerase r2))" |
296 shows " rerase r2 \<noteq> RSEQ r (RSEQ RONE (rerase r2))" |