{"entities":{"Q5051990":{"pageid":7081567,"ns":120,"title":"Item:Q5051990","lastrevid":56906667,"modified":"2026-03-24T13:43:44Z","type":"item","id":"Q5051990","labels":{"en":{"language":"en","value":"Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7620649"}},"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":"Q5051990$714127C6-3B99-4275-8AFC-DB757F6DCF68","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5bcaaf5d921ef272da0c881005bcb57a33f54ff1","datavalue":{"value":{"text":"Fold\u2013unfold lemmas for reasoning about recursive programs using the Coq proof assistant","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5051990$094155D3-D572-4996-8AFF-C5F6C8D517F0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"69686ced461f818ef1ffd7aad88538899ba2caac","datavalue":{"value":"10.1017/S0956796822000107","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5051990$43E3B246-9991-4704-A021-721ABC2DA14B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2f7ebf08f82ce515e0740dc978f18c660e5f4735","datavalue":{"value":{"entity-type":"item","numeric-id":232933,"id":"Q232933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$972E2E00-2821-4F65-831D-EE340F07877A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c0cefd96801130048cf3f8ae21032b5cf52d744d","datavalue":{"value":{"entity-type":"item","numeric-id":2713363,"id":"Q2713363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$15F4CCC8-3F85-4BC2-92AA-E044A0257814","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0574a4bff222e9fd97c080fbc50c618f266d2baa","datavalue":{"value":{"time":"+2022-11-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5051990$332100F0-475E-4E76-855D-E40A35DF36B9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5051990$C51035A0-C5BC-49FF-B9C6-1B93F7FD64BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5051990$C51EDD80-08C4-44EC-B5E6-8B73FC79D676","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2bddd9cbfc2b1f309ec6c1e05454333ffde74fa2","datavalue":{"value":"7620649","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5051990$D533B881-30A2-4AFA-872B-C56E2B0556C5","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$A3933B0B-21F5-4B68-AAF3-1B8F3E471AEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$66258049-DF08-4A9F-A104-52BCF544B3D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$ED4A6E5C-1319-444C-90B4-BB2B0EA7A8EC","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":"Q5051990$2EF15103-82A4-4CF8-B138-08CAEE83E164","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"929a7f2a89678e9e8a6c6588af2c0b8f7111ef19","datavalue":{"value":"Q124817274","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5051990$7B0D362D-6135-4EC0-AD4C-D1F35B9F615F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$DE1F1E3B-072C-4AF5-AA27-1C3B880E4699","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c28df2712119352cfc70833dae3c4445fb4c54d0","datavalue":{"value":{"entity-type":"item","numeric-id":4082975,"id":"Q4082975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$529F7F28-06B9-46A1-995E-D1FACDB5F5F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c5ae7e408b1d1201c271e00762d47096e39a012","datavalue":{"value":{"entity-type":"item","numeric-id":4111080,"id":"Q4111080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$8E3BD925-E613-4756-B322-E79285D1E30C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca8ffb67b00ea8cbeeaf44ae8b6f3bc27fbc2d2b","datavalue":{"value":{"entity-type":"item","numeric-id":5618896,"id":"Q5618896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$244C6CB8-0BC5-4C08-99A4-5AE5833B62CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b02cebc44c2831878b18e904086383fc947d3037","datavalue":{"value":{"entity-type":"item","numeric-id":5417200,"id":"Q5417200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$511272ED-FFF3-48C9-AB82-37EF25EEE4F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61aa0c1501e4e99ad1129785d2af5d578d0a74d2","datavalue":{"value":{"entity-type":"item","numeric-id":4972067,"id":"Q4972067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$568720A3-001E-488E-9927-20C3EA8E842B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d107e7288f76241c9969f07b1333f62e32911b2e","datavalue":{"value":{"entity-type":"item","numeric-id":5074057,"id":"Q5074057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$564F595E-7C14-42A2-AA35-F7AE7B1EE300","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"795a1b195850936176023b19afd668563f624074","datavalue":{"value":{"entity-type":"item","numeric-id":5472881,"id":"Q5472881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$10BED52D-CCA1-4EB0-A096-25F86EBCB232","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82e4be35d0888519e5872195dc487ef081b60487","datavalue":{"value":{"entity-type":"item","numeric-id":1583366,"id":"Q1583366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$B6522F42-370F-49D6-B543-8801B4A15C08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e06246cd6673d30ef14749aae27286b480929b9","datavalue":{"value":{"entity-type":"item","numeric-id":4501772,"id":"Q4501772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$E1D569CB-15B8-435C-85B0-653C01440EEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"901ba45472e1a0a3be8b2e40215973355027ef09","datavalue":{"value":{"entity-type":"item","numeric-id":2949209,"id":"Q2949209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$E5F409BE-A98D-49C7-BDD8-F80425155A81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"41e036cb48b37a0cafe96d5a6bf3f3f6ac1308a9","datavalue":{"value":{"entity-type":"item","numeric-id":3685171,"id":"Q3685171"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$B0B06E38-5DC3-4061-A817-5CE3C4EC3A4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab124a7373ba82029ffdcc597bda7b4f27aee620","datavalue":{"value":{"entity-type":"item","numeric-id":5287559,"id":"Q5287559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$359F8674-9930-4A78-9410-290A3A2BBB1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"914ef8719678eb4ee59028ba65b4741c8aa1bc8e","datavalue":{"value":{"entity-type":"item","numeric-id":4124327,"id":"Q4124327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$C7835ACC-78C4-45AE-8688-369052004295","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$06245DBC-490F-4291-9986-8A22981A4B3C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"10e7b04aa841b66f5fe62d00ae09530613b561e0","datavalue":{"value":{"entity-type":"item","numeric-id":3434629,"id":"Q3434629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6dfb29f3b59bc3fcc112c1b6b05759962e3bf09","datavalue":{"value":{"amount":"+0.7514500617980957","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":"Q5051990$D646FBB3-B873-4E54-B7EF-B6ED514DF8FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"562ef86fd32348776dc59a658e645f201dfc1d4b","datavalue":{"value":{"entity-type":"item","numeric-id":5713936,"id":"Q5713936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"182fee9bd4d0faee949dc50d6edcac8ca74d6b86","datavalue":{"value":{"amount":"+0.7057561874389648","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":"Q5051990$E2C17838-D2E7-4031-8582-77702DCB0C4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f43dd9c852cf867e617df44f7b06a7ba5f542fa6","datavalue":{"value":{"entity-type":"item","numeric-id":5234276,"id":"Q5234276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35b041ebeb79b0a98dfba04cce05cc1676a983de","datavalue":{"value":{"amount":"+0.6874063014984131","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":"Q5051990$B9D0D33E-2071-4C49-B555-446DC1C072A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b400db7f0493ae4017b7b62a2ed6376ec704a0d","datavalue":{"value":{"entity-type":"item","numeric-id":1687755,"id":"Q1687755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b824202b8cd4a4d5cd431d7cd092512a753e1e42","datavalue":{"value":{"amount":"+0.6863483190536499","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":"Q5051990$15B1410E-1C7E-4BCB-891A-B5EC7F3026E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39e61c9806f592cf7e6bb582cded65ec23f8675e","datavalue":{"value":{"entity-type":"item","numeric-id":2754027,"id":"Q2754027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eba91dc20cb76a1d5347e64a0b48afb5fef7f364","datavalue":{"value":{"amount":"+0.6836174726486206","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":"Q5051990$EC5366BF-540B-4C5A-878C-92C0DA217F0D","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5051990$B1156707-DE72-4171-8BDF-AD857BD18C8F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5051990","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5051990"}}}}}