equal
deleted
inserted
replaced
24 thus ?thesis |
24 thus ?thesis |
25 by linarith |
25 by linarith |
26 next |
26 next |
27 assume *: "\<not> complete t" |
27 assume *: "\<not> complete t" |
28 hence "height t = min_height t + 1" |
28 hence "height t = min_height t + 1" |
29 using assms min_hight_le_height[of t] |
29 using assms min_height_le_height[of t] |
30 by(auto simp add: balanced_def complete_iff_height) |
30 by(auto simp add: balanced_def complete_iff_height) |
31 hence "2 ^ min_height t \<le> size1 t \<and> size1 t < 2 ^ (min_height t + 1)" |
31 hence "2 ^ min_height t \<le> size1 t \<and> size1 t < 2 ^ (min_height t + 1)" |
32 by (metis * min_height_size1 size1_height_if_incomplete) |
32 by (metis * min_height_size1 size1_height_if_incomplete) |
33 hence "2 powr min_height t \<le> size1 t \<and> size1 t < 2 powr (min_height t + 1)" |
33 hence "2 powr min_height t \<le> size1 t \<and> size1 t < 2 powr (min_height t + 1)" |
34 by(simp only: powr_realpow) |
34 by(simp only: powr_realpow) |
51 thus ?thesis |
51 thus ?thesis |
52 by linarith |
52 by linarith |
53 next |
53 next |
54 assume *: "\<not> complete t" |
54 assume *: "\<not> complete t" |
55 hence **: "height t = min_height t + 1" |
55 hence **: "height t = min_height t + 1" |
56 using assms min_hight_le_height[of t] |
56 using assms min_height_le_height[of t] |
57 by(auto simp add: balanced_def complete_iff_height) |
57 by(auto simp add: balanced_def complete_iff_height) |
58 hence 0: "2 ^ min_height t < size1 t \<and> size1 t \<le> 2 ^ (min_height t + 1)" |
58 hence 0: "2 ^ min_height t < size1 t \<and> size1 t \<le> 2 ^ (min_height t + 1)" |
59 by (metis "*" min_height_size1_if_incomplete size1_height) |
59 by (metis "*" min_height_size1_if_incomplete size1_height) |
60 hence "2 powr min_height t < size1 t \<and> size1 t \<le> 2 powr (min_height t + 1)" |
60 hence "2 powr min_height t < size1 t \<and> size1 t \<le> 2 powr (min_height t + 1)" |
61 by(simp only: powr_realpow) |
61 by(simp only: powr_realpow) |