equal
deleted
inserted
replaced
57 case (8 q) thus ?case by(cases q) (simp) |
57 case (8 q) thus ?case by(cases q) (simp) |
58 qed |
58 qed |
59 |
59 |
60 text \<open>Running times:\<close> |
60 text \<open>Running times:\<close> |
61 |
61 |
62 define_time_fun norm |
62 time_fun norm |
63 define_time_fun enq |
63 time_fun enq |
64 define_time_fun tl |
64 time_fun tl |
65 define_time_fun deq |
65 time_fun deq |
66 |
66 |
67 lemma T_tl_0: "T_tl xs = 0" |
67 lemma T_tl_0: "T_tl xs = 0" |
68 by(cases xs)auto |
68 by(cases xs)auto |
69 |
69 |
70 text \<open>Amortized running times:\<close> |
70 text \<open>Amortized running times:\<close> |