equal
deleted
inserted
replaced
367 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
367 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
368 apply(lifting concat2) |
368 apply(lifting concat2) |
369 apply(cleaning) |
369 apply(cleaning) |
370 apply (simp add: finsert_def fconcat_def comp_def) |
370 apply (simp add: finsert_def fconcat_def comp_def) |
371 apply cleaning |
371 apply cleaning |
|
372 (* ID PROBLEM *) |
|
373 apply(simp add: id_def[symmetric] id_simps) |
372 done |
374 done |
373 |
375 |
374 text {* raw section *} |
376 text {* raw section *} |
375 |
377 |
376 lemma map_rsp_aux: |
378 lemma map_rsp_aux: |