equal
deleted
inserted
replaced
4427 by (metis (mono_tags, lifting) append_Nil2 dropWhile_eq_drop hd_dropWhile |
4427 by (metis (mono_tags, lifting) append_Nil2 dropWhile_eq_drop hd_dropWhile |
4428 takeWhile_dropWhile_id takeWhile_eq_all_conv) |
4428 takeWhile_dropWhile_id takeWhile_eq_all_conv) |
4429 have 1: "x \<notin> set ?pref" by (metis (full_types) set_takeWhileD) |
4429 have 1: "x \<notin> set ?pref" by (metis (full_types) set_takeWhileD) |
4430 have 2: "xs = ?pref @ x # tl ?rest" |
4430 have 2: "xs = ?pref @ x # tl ?rest" |
4431 by (metis rest append_eq_conv_conj hd_Cons_tl takeWhile_eq_take) |
4431 by (metis rest append_eq_conv_conj hd_Cons_tl takeWhile_eq_take) |
4432 have "count_list (tl ?rest) x = n"using [[metis_suggest_of]] |
4432 have "count_list (tl ?rest) x = n" |
4433 using assms rest 1 2 count_notin count_list_append[of ?pref "x # tl ?rest" x] by simp |
4433 using assms rest 1 2 count_notin count_list_append[of ?pref "x # tl ?rest" x] by simp |
4434 with 1 2 show ?thesis by blast |
4434 with 1 2 show ?thesis by blast |
4435 qed |
4435 qed |
4436 |
4436 |
4437 lemma split_list_cycles: |
4437 lemma split_list_cycles: |