{"entities":{"Q5858675":{"pageid":7888226,"ns":120,"title":"Item:Q5858675","lastrevid":58592886,"modified":"2026-04-05T22:06:06Z","type":"item","id":"Q5858675","labels":{"en":{"language":"en","value":"Mendler-style iso-(co)inductive predicates: a strongly normalizing approach"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7333177"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5858675$B20FBB6A-9723-4778-8262-14ED6047262E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"19ffe9529373c6253dbde6c51abf2865fd385df7","datavalue":{"value":"1458.68039","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5858675$39DFD181-5F8A-42C1-A3E9-44C2A935C19E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"617513ed20293f92b2f67987461eb17d18d83c6e","datavalue":{"value":{"entity-type":"item","numeric-id":2133447,"id":"Q2133447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5858675$A380CE7E-28AD-4CEF-834F-B92945ADAAC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"77349d7f7398c47e6d2065cd0d80588fae809ad3","datavalue":{"value":{"entity-type":"item","numeric-id":2133448,"id":"Q2133448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5858675$E0C1A207-058F-44F3-8CB5-0AE89CFC24AF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0b45cef9412c58362fb90282c6cf1861e657771c","datavalue":{"value":{"time":"+2021-04-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5858675$2062EA08-BB57-429B-9D3B-B97214989439","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b0847724b8c57e38967d9028be767b60a61412fb","datavalue":{"value":"https://arxiv.org/abs/1203.6158","type":"string"},"datatype":"url"},"type":"statement","id":"Q5858675$386B0A9A-0C87-4685-9580-A16D9D4AA726","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"a70d34e118e8d26de0dca87d8e327d769f59cd43","datavalue":{"value":"http://eptcs.web.cse.unsw.edu.au/paper.cgi?LSFA2011.3","type":"string"},"datatype":"url"},"type":"statement","id":"Q5858675$E833A7B0-2CFC-4050-BF3A-18A21000640E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5858675$70E368FC-7FEF-4C16-9FF4-A30ADA13D80B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f6d4b3012578fba2d8ab6b9e39d328cad9def57","datavalue":{"value":"03B16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5858675$74CD07A0-AF97-4D0C-B6C8-981D72F1AD69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5858675$CD161247-CFCA-4810-A62A-C57D4A0FCBF0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8f1ec298da95faedd3e3f07fe9da1d18371f048c","datavalue":{"value":"7333177","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5858675$B5EEACCD-AB52-479A-840A-E8418551E7CF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a994b05c59909fd48d553ad27ff25f663f6cccc4","datavalue":{"value":"Mendler-style","type":"string"},"datatype":"string"},"type":"statement","id":"Q5858675$A513DC49-A47C-47B4-87D5-13217937A49B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"88903df03255edcd8d8963ceb92ff3489eaf8257","datavalue":{"value":"(co)inductive definitions","type":"string"},"datatype":"string"},"type":"statement","id":"Q5858675$817BD286-B8D7-4440-9515-4494C97D0E6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b5aeae98b8a496fe3563717c2c8e4677938faaf5","datavalue":{"value":"primitive (co)recursion","type":"string"},"datatype":"string"},"type":"statement","id":"Q5858675$B510CF7F-0B5D-4F5A-899D-4935B72BF559","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af462e56ed2ce88a42c8df0ec7f2dc6a55ded212","datavalue":{"value":"strong normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q5858675$2F2ADEA6-B046-4B23-8192-CB561D4CEDCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"accf14b1f4c136bbc725f7158f92ae0977037e88","datavalue":{"value":"saturated set","type":"string"},"datatype":"string"},"type":"statement","id":"Q5858675$8CBD932B-492A-4A77-B4C2-A31F06065724","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9f3b357383dfba43d890912524abefb4bc1f78f9","datavalue":{"value":"monotonization","type":"string"},"datatype":"string"},"type":"statement","id":"Q5858675$34B34825-2889-44CA-AA66-617772EEFE77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e01102226a676edcf182ed47a9896bd215db761","datavalue":{"value":"second-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5858675$BEBAD318-7E28-4CBF-9A2D-566E4A735977","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe2af07b9c34ae931dc9e9986f8e4653ba857344","datavalue":{"value":"programming with proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q5858675$0CA10BB9-8BFF-4FD3-9012-5C7E853BBFD1","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5858675$98DFB8AB-2D75-46AE-B78F-8C6AFB419BCB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b319842903f038d9cfe413b03724f930ebd2648d","datavalue":{"value":{"entity-type":"item","numeric-id":5283417,"id":"Q5283417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb1325c4bb03971d5f835807d8a60ad4419b97cd","datavalue":{"value":{"amount":"+0.7633436322212219","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5858675$AE41F4D8-3BDC-4E9F-9E18-AE95F1B09D73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8781836b753ae48b141e6bc20052f587f98a2634","datavalue":{"value":{"entity-type":"item","numeric-id":5108017,"id":"Q5108017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06e7043f9de192e8605b5592efa1a9c25e287731","datavalue":{"value":{"amount":"+0.7424860000610352","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5858675$E33CAFCA-DB3E-4E1F-A04B-A2041BA82BE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ab8f2efce65f1bb0e13fc4caa073a89436edf6c","datavalue":{"value":{"entity-type":"item","numeric-id":1769440,"id":"Q1769440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"efc63173f64f0b2fac2270a37cfc046435ddd2db","datavalue":{"value":{"amount":"+0.7193727493286133","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5858675$AE59A7E4-7E7A-49F6-8ADA-57E84D490EC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb6f4d19852f6a35f19949a6cb60887291a2d447","datavalue":{"value":{"entity-type":"item","numeric-id":2766796,"id":"Q2766796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"500bcca19ce629515892ee3c10a8b5a623e59906","datavalue":{"value":{"amount":"+0.7153014540672302","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5858675$CBD83B84-CBD3-4D9A-9762-237591FD53B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b6479083c3a9fa4c0241ba0f47f848bad11418f","datavalue":{"value":{"entity-type":"item","numeric-id":2856633,"id":"Q2856633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0cd45cd2b79b312600b51a9f421cd1bd78d8a5c2","datavalue":{"value":{"amount":"+0.7007372975349426","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5858675$E46A2541-15FD-4AA2-B407-9E3341E2BE3B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5858675","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5858675"}}}}}