equal
deleted
inserted
replaced
331 case (3 xs ys xss) |
331 case (3 xs ys xss) |
332 let ?xss = "xs # ys # xss" |
332 let ?xss = "xs # ys # xss" |
333 let ?xss2 = "merge_adj ?xss" |
333 let ?xss2 = "merge_adj ?xss" |
334 obtain k' where k': "k = Suc k'" using "3.prems"(2) |
334 obtain k' where k': "k = Suc k'" using "3.prems"(2) |
335 by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust) |
335 by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust) |
336 have "even (length xss)" using "3.prems"(2) even_Suc_Suc_iff by fastforce |
336 have "even (length ?xss)" using "3.prems"(2) k' by auto |
337 from "3.prems"(1) length_merge_adj[OF this] |
337 from length_merge_adj[OF this "3.prems"(1)] |
338 have *: "\<forall>x \<in> set(merge_adj ?xss). length x = 2*m" by(auto simp: length_merge) |
338 have *: "\<forall>x \<in> set(merge_adj ?xss). length x = 2*m" . |
339 have **: "length ?xss2 = 2 ^ k'" using "3.prems"(2) k' by auto |
339 have **: "length ?xss2 = 2 ^ k'" using "3.prems"(2) k' by auto |
340 have "c_merge_all ?xss = c_merge_adj ?xss + c_merge_all ?xss2" by simp |
340 have "c_merge_all ?xss = c_merge_adj ?xss + c_merge_all ?xss2" by simp |
341 also have "\<dots> \<le> m * 2^k + c_merge_all ?xss2" |
341 also have "\<dots> \<le> m * 2^k + c_merge_all ?xss2" |
342 using "3.prems"(2) c_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps) |
342 using "3.prems"(2) c_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps) |
343 also have "\<dots> \<le> m * 2^k + (2*m) * k' * 2^k'" |
343 also have "\<dots> \<le> m * 2^k + (2*m) * k' * 2^k'" |