equal
deleted
inserted
replaced
1017 have as: "L(erase a2) \<subseteq> L(erase a1)" by fact |
1017 have as: "L(erase a2) \<subseteq> L(erase a1)" by fact |
1018 show "map (bder c) (bs @ [a1] @ rsa @ [a2] @ rsb) s\<leadsto>* map (bder c) (bs @ [a1] @ rsa @ rsb)" |
1018 show "map (bder c) (bs @ [a1] @ rsa @ [a2] @ rsb) s\<leadsto>* map (bder c) (bs @ [a1] @ rsa @ rsb)" |
1019 apply(simp only: map_append) |
1019 apply(simp only: map_append) |
1020 apply(simp only: map_single) |
1020 apply(simp only: map_single) |
1021 apply(rule rs_in_rstar) |
1021 apply(rule rs_in_rstar) |
1022 thm rrewrite_srewrite.intros |
1022 thm rrewrite_srewrite.intros |
1023 apply(rule rrewrite_srewrite.ss6) |
1023 apply(rule rrewrite_srewrite.ss6) |
1024 using as |
1024 using as |
1025 apply(auto simp add: der_correctness Der_def) |
1025 apply(auto simp add: der_correctness Der_def) |
1026 done |
1026 done |
1027 (*next |
1027 (*next |