{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T20:19:23Z","timestamp":1762373963279,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540432876"},{"type":"electronic","value":"9783540458425"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45842-5_15","type":"book-chapter","created":{"date-parts":[[2007,5,27]],"date-time":"2007-05-27T00:00:38Z","timestamp":1180224038000},"page":"233-242","source":"Crossref","is-referenced-by-count":6,"title":["An Inductive Version of Nash-Williams\u2019 Minimal-Bad-Sequence Argument for Higman\u2019s Lemma"],"prefix":"10.1007","author":[{"given":"Monika","family":"Seisenberger","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,14]]},"reference":[{"key":"15_CR1","unstructured":"Thierry Coquand and Daniel Fridlender. A proof of Higman\u2019s lemma by structural induction, 1994. ftp:\/\/ftp.cs.chalmers.se\/pub\/users\/coquand\/open1.ps.Z"},{"key":"15_CR2","unstructured":"Daniel Fridlender. Higman\u2019s Lemma in Type Theory. PhD thesis, Chalmers University of Technology and University of G\u00f6teburg, Sweden, Oktober 1997."},{"key":"15_CR3","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"2","author":"Graham Higman","year":"1952","unstructured":"Graham Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc., 2:326\u2013336, 1952.","journal-title":"Proc. London Math. Soc."},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Alberto Marcone. On the logical strength of Nash-Williams\u2019 theorem on trans-finite sequences. In: Logic: from Foundations to Applications; European logic colloquium, pp. 327\u2013351, 1996.","DOI":"10.1093\/oso\/9780198538622.003.0014"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Chetan R. Murthy and James R. Russell. A Constructive proof of Higman\u2019s Lemma. In Proc. Fifth Symp. on Logic in Comp. Science, pp. 257\u2013267, 1990.","DOI":"10.1109\/LICS.1990.113752"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Chetan R. Murthy. An Evaluation Semantics for Classical Proofs. In Proc. Sixth Symp. on Logic in Computer Science, pp. 96\u2013109, 1991.","DOI":"10.1109\/LICS.1991.151634"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Crispin St. J. A. Nash-Williams. On well-quasi-ordering finite trees. Proc. Cambridge Phil. Soc., 59:833\u2013835, 1963.","DOI":"10.1017\/S0305004100003844"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0168-0072(93)90192-G","volume":"60","author":"M. Rathjen","year":"1993","unstructured":"Michael Rathjen and Andreas Weiermann. Proof-theoretic investigations on Kruskal\u2019s theorem. Annals of Pure and Applied Logic, 60:49\u201388, 1993.","journal-title":"Annals of Pure and Applied Logic"},{"key":"15_CR9","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1006\/aima.1993.1004","volume":"97","author":"F. Richman","year":"1993","unstructured":"Fred Richman and Gabriel Stolzenberg. Well Quasi-Ordered Sets. Advances in Math., 97:145\u2013153, 1993.","journal-title":"Advances in Math."},{"key":"15_CR10","unstructured":"Monika Seisenberger. Kruskal\u2019s tree theorem in a constructive theory of inductive definitions In: Reuniting the Antipodes-C onstructive and Nonstandard Views of the Continuum. Synthese Library, Kluwer, Dordrecht, forthcoming."},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BF02007558","volume":"25","author":"K. Sch\u00fctte","year":"1985","unstructured":"Kurt Sch\u00fctte and Stephen G. Simpson. Ein in der reinen Zahlentheorie unbeweisbarer Satz \u00fcber endliche Folgen von nat\u00fcrlichen Zahlen. Archiv f\u00fcr Mathematische Logik und Grundlagenforschung, 25:75\u201389, 1985.","journal-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforschung"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Stephen G. Simpson. Nonprovability of certain combinatorial properties of finite trees. In L.A. Harrington, et al., eds., Harvey Friedman\u2019s Research on the Foundations of Mathematics, pp. 87\u2013117. North-Holland, Amsterdam, 1985.","DOI":"10.1016\/S0049-237X(09)70156-9"},{"key":"15_CR13","unstructured":"Diana Schmidt. Well-orderings and their maximal order types, 1979. Habilitationsschrift, Mathematisches Institut der Universit\u00e4t Heidelberg."},{"key":"15_CR14","unstructured":"Wim Veldman. An intuitionistic proof of Kruskal\u2019s Theorem. Report no. 0017, Department of Mathematics, University of Nijmegen, 2000."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45842-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T18:24:07Z","timestamp":1737051847000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45842-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540432876","9783540458425"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45842-5_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}