{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:40:53Z","timestamp":1761324053719,"version":"3.37.3"},"reference-count":14,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,6,13]],"date-time":"2016-06-13T00:00:00Z","timestamp":1465776000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft (DE)","doi-asserted-by":"publisher","award":["RTG 1480 (PUMA)"],"award-info":[{"award-number":["RTG 1480 (PUMA)"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,4]]},"DOI":"10.1007\/s10817-016-9378-0","type":"journal-article","created":{"date-parts":[[2016,6,13]],"date-time":"2016-06-13T07:14:41Z","timestamp":1465802081000},"page":"483-508","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Proving Divide and Conquer Complexities in Isabelle\/HOL"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4263-6571","authenticated-orcid":false,"given":"Manuel","family":"Eberl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,13]]},"reference":[{"issue":"2","key":"9378_CR1","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1023\/A:1018373005182","volume":"10","author":"M Akra","year":"1998","unstructured":"Akra, M., Bazzi, L.: On the solution of linear recurrence equations. Comput. Optim. Appl. 10(2), 195\u2013210 (1998). doi:\n                        10.1023\/A:1018373005182","journal-title":"Comput. Optim. Appl."},{"key":"9378_CR2","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-540-25984-8_27","volume-title":"Automated Reasoning, Lecture Notes in Computer Science","author":"J Avigad","year":"2004","unstructured":"Avigad, J., Donnelly, K.: Formalizing \n                        $$O$$\n                        \n                            \n                                            \n                                O\n                            \n                        \n                     notation in Isabelle\/HOL. In: Basin, D., Rusinowitch, M. (eds.) Automated Reasoning, Lecture Notes in Computer Science, pp. 357\u2013371. Springer, Berlin (2004). doi:\n                        10.1007\/978-3-540-25984-8_27"},{"key":"9378_CR3","unstructured":"Avigad, J., H\u00f6lzl, J., Serafin, L.: A formally verified proof of the central limit theorem. CoRR abs\/1405.7012 (2014). Presented at the Isabelle Workshop 2014"},{"issue":"2","key":"9378_CR4","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014). doi:\n                        10.1007\/s10817-013-9284-7","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9378_CR5","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s00453-002-1003-4","volume":"36","author":"L Bazzi","year":"2003","unstructured":"Bazzi, L., Mitter, S.K.: The solution of linear probabilistic recurrence relations. Algorithmica 36(1), 41\u201357 (2003). doi:\n                        10.1007\/s00453-002-1003-4","journal-title":"Algorithmica"},{"issue":"5","key":"9378_CR6","doi-asserted-by":"publisher","first-page":"1546","DOI":"10.1109\/18.259639","volume":"39","author":"CG Boncelet Jr","year":"1993","unstructured":"Boncelet Jr., C.G.: Block arithmetic coding for source compression. IEEE Trans. Inf. Theory 39(5), 1546\u20131554 (1993). doi:\n                        10.1109\/18.259639","journal-title":"IEEE Trans. Inf. Theory"},{"key":"9378_CR7","volume-title":"Introduction to Algorithms, 4th printing","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 4th printing, 3rd edn. The MIT Press, Cambridge (2009)","edition":"3"},{"issue":"3","key":"9378_CR8","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/2487241.2487242","volume":"60","author":"M Drmota","year":"2013","unstructured":"Drmota, M., Szpankowski, W.: A Master theorem for discrete divide and conquer recurrences. J. ACM 60(3), 16:1\u201316:49 (2013). doi:\n                        10.1145\/2487241.2487242","journal-title":"J. ACM"},{"key":"9378_CR9","unstructured":"Eberl, M.: The Akra\u2013Bazzi Theorem and the Master Theorem. Archive of Formal Proofs (2015). \n                        http:\/\/www.isa-afp.org\/entries\/Akra_Bazzi.shtml\n                        \n                    , Formal proof development"},{"key":"9378_CR10","unstructured":"Eberl, M.: Landau Symbols. Archive of Formal Proofs (2015). \n                        http:\/\/www.isa-afp.org\/entries\/Landau_Symbols.shtml\n                        \n                    , Formal proof development"},{"key":"9378_CR11","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming. Lecture Notes in Computer Science","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming. Lecture Notes in Computer Science, vol. 6009, pp. 103\u2013117. Springer, Berlin (2010). doi:\n                        10.1007\/978-3-642-12251-4_9"},{"key":"9378_CR12","unstructured":"H\u00f6lzl, J.: Proving inequalities over reals with computation in Isabelle\/HOL. In: Reis, G.D., Th\u00e9ry, L. (eds.) Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS\u201909), pp. 38\u201345. Munich (2009)"},{"key":"9378_CR13","unstructured":"Krauss, A.: Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen, Institut f\u00fcr Informatik (2009). \n                        http:\/\/nbn-resolving.de\/urn\/resolver.pl?urn:nbn:de:bvb:91-diss-20090722-681651-1-1"},{"key":"9378_CR14","unstructured":"Leighton, T.: Notes on Better Master Theorems for Divide-and-Conquer Recurrences (1996). \n                        http:\/\/courses.csail.mit.edu\/6.046\/spring04\/handouts\/akrabazzi.pdf"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9378-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9378-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9378-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9378-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T04:58:32Z","timestamp":1488344312000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9378-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,13]]},"references-count":14,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,4]]}},"alternative-id":["9378"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9378-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2016,6,13]]}}}