{"entities":{"Q928672":{"pageid":930520,"ns":120,"title":"Item:Q928672","lastrevid":65442879,"modified":"2026-04-12T02:38:02Z","type":"item","id":"Q928672","labels":{"en":{"language":"en","value":"Nominal techniques in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5287724"}},"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":"Q928672$1669C5C1-7B52-4629-A753-85BA48EA7357","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7f8cba01cb75861c3150d3d6ae9771717ed7563e","datavalue":{"value":{"text":"Nominal techniques in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q928672$C461B9A7-BFA5-4E68-8BED-355D8724A242","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d62ecea2179003a4206d002685348e822757e882","datavalue":{"value":"1140.68061","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928672$4CBB6983-4E6D-4E22-A5A8-3619366533B1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8be13823e57b532010d417bfefa3b5133f759f9a","datavalue":{"value":{"entity-type":"item","numeric-id":860832,"id":"Q860832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$0E457494-B541-4159-B263-6FC71856E525","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$021C2D69-8D6E-4F1D-AC68-EF73EF664384","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f1c0b93a352a714c61ccd46766a52600d36f8c2","datavalue":{"value":{"time":"+2008-06-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q928672$9088FA81-26FC-4C86-9DB3-72F06F33F6DB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928672$2E399B9D-1EB6-48A4-B02C-A270A64882BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928672$A23869E6-1BBF-4A5A-B382-04EDDA712B02","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"eef7de903ea8071d12026b15fe437c01bc462f27","datavalue":{"value":"5287724","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928672$610C7C08-5DA3-4617-B1E9-51F51CA75BE5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9b6f999d95ff8c21d42c74db6f102df64501e26","datavalue":{"value":"Lambda-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q928672$1CB239EB-3A88-4CFB-A1E0-AB79CC0805E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5b0785b96c214c256ff909c10e300837f56c701","datavalue":{"value":"Nominal logic work","type":"string"},"datatype":"string"},"type":"statement","id":"Q928672$AAC08FAB-294C-4A5E-88FD-7B337FC66601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e3bb276ae4ef9c48ed65139062799af125995c57","datavalue":{"value":"Theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q928672$388F4678-1FB7-4EAA-AFC5-9A4E90358FAF","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$A0E297E8-B54F-4F48-9861-575D4839D56D","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":"Q928672$1885E28F-4A47-40DE-8D62-6F854DC2EDAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$751DE4EF-FDC8-4094-AA6C-9183D11A4C54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8be5ee5254d2a781e0ec7bc0b35265c3f1813a9a","datavalue":{"value":{"entity-type":"item","numeric-id":22078,"id":"Q22078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$7AFD7731-FE29-4DF8-AA41-52163DAA78EC","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":"Q928672$48C41229-9D4A-4753-8B4A-EAE4B031DA59","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3d444f31307fe984809b50b9ff11f5fc1bbb6e33","datavalue":{"value":"https://doi.org/10.1007/s10817-008-9097-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q928672$63C94615-0147-456B-B093-5C93FEB28CF3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e761fc3aae9b23b6be63855760f97b4ac51fab94","datavalue":{"value":"W2037026294","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928672$0A97B135-EF2D-4745-8779-B390E1AF2E99","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ff630e3c1b7657cd6a825eab62ba0fd151f65cf","datavalue":{"value":{"entity-type":"item","numeric-id":4484329,"id":"Q4484329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$33C02889-5A12-4421-9632-3E7424877DB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c50237c8bde09d6668086722c62e1080ba158cf","datavalue":{"value":{"entity-type":"item","numeric-id":3189820,"id":"Q3189820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$A44688E8-687E-4D8B-AED5-D916CB790CCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79ce8544fc5a0489695eae9a558cb4d34b573281","datavalue":{"value":{"entity-type":"item","numeric-id":5477646,"id":"Q5477646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$EEEE62D8-992A-4FE0-99A5-9EF4068D4493","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"956c663a8c65ca7a493106b21f9b04a9a741383f","datavalue":{"value":{"entity-type":"item","numeric-id":1155602,"id":"Q1155602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$C17922F8-660F-4F96-8385-3745AA6E657C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce39ca711bf99c74f8bdce078c27fed133ff4aa7","datavalue":{"value":{"entity-type":"item","numeric-id":5758048,"id":"Q5758048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$C89924FD-32C8-4071-A4F3-A9538A08310C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e723c31e56f2487bba3b93f0d7637a4943535187","datavalue":{"value":{"entity-type":"item","numeric-id":3024831,"id":"Q3024831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$1C4D53A6-0506-4906-8AE8-67A4D0C2B9A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5927659804eca2a32583cb94f8cceb03b87d2078","datavalue":{"value":{"entity-type":"item","numeric-id":1854337,"id":"Q1854337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$5A8FD19C-50EA-4965-91EF-EFB0CD1FB30D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"882e318ac9b6bbd79e82dcc1ce3fe340042f5778","datavalue":{"value":{"entity-type":"item","numeric-id":699761,"id":"Q699761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$D49614BA-DD5E-4BD5-8669-CC739EC96F19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$9A41684C-6E74-450C-99ED-44D2A9A90132","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8c55f09c39173f168f9ee166ab49eb8e620c679","datavalue":{"value":{"entity-type":"item","numeric-id":5477651,"id":"Q5477651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$0ECCB0A2-42C6-4815-A352-2810F6675E49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40bf03b14ee12a3cdbc67fa7b1fe5ffcff272071","datavalue":{"value":{"entity-type":"item","numeric-id":3851084,"id":"Q3851084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$D4C4F9F2-9FA7-41DD-B640-F0D969FB12A9","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":"Q928672$FCF97A25-FBB2-41E8-A79E-DC564BAF4554","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de8d5484c75fe2a14b4f198a80db5c6efdf1db82","datavalue":{"value":{"entity-type":"item","numeric-id":5464650,"id":"Q5464650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$AE0111BE-103A-4140-AA1B-0127B2380E34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c193b2b170f7626fc739837cea7c223c4266fe6c","datavalue":{"value":{"entity-type":"item","numeric-id":853738,"id":"Q853738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$9D5E7DD0-3674-4CC4-8589-25DF2D50A874","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b8c3a63f5113f0209622b58f18640a08a06fa7","datavalue":{"value":{"entity-type":"item","numeric-id":1887151,"id":"Q1887151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$BA2124F4-CD7D-48C7-8880-B380E4520C6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1851616a00610aaeabd4291b4d22573878184fd4","datavalue":{"value":{"entity-type":"item","numeric-id":3546313,"id":"Q3546313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$47650DCA-C6D7-4556-BBEF-3130616E37A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"01a01883223d871962fc4212da8007cec3702b73","datavalue":{"value":{"entity-type":"item","numeric-id":2723408,"id":"Q2723408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$7C73542A-C9F2-40D0-87BD-3DBC2FB140E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c382f571059f65c71d7c5267e06c23fa2d98eb72","datavalue":{"value":{"entity-type":"item","numeric-id":5917605,"id":"Q5917605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$D949413D-58B5-45A8-A476-E72730C25CE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5dccdbb6fa19cb81346a7b093ebc4768c7c2f275","datavalue":{"value":{"entity-type":"item","numeric-id":3189858,"id":"Q3189858"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$FCFA9B93-FD47-4DF7-860B-7FFA9E2CA36E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"939be0771ea627d569d52a0b8c1f463c5ec167f7","datavalue":{"value":{"entity-type":"item","numeric-id":3613430,"id":"Q3613430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$1BD7D7F8-0434-4EB8-A4E2-6F7B4863D4C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29dee98229347c3ff5d61b43b45d8e001f181167","datavalue":{"value":{"entity-type":"item","numeric-id":3608761,"id":"Q3608761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$2B3204C6-50D7-4067-BF3D-1A2F31DA333F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ade402c8643377c95736cc4de881776c386a1875","datavalue":{"value":{"entity-type":"item","numeric-id":1882909,"id":"Q1882909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$6EA3E2BB-0098-4FAE-B7B4-C967A665A634","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4f8f6dff394ac274489a2a8165abb84f760b4be","datavalue":{"value":{"entity-type":"item","numeric-id":5394605,"id":"Q5394605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$59C38C63-5CE4-460F-B602-AB6774D03FC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84db7b031663473052f5c9fdfcfae885713c2faa","datavalue":{"value":{"entity-type":"item","numeric-id":5756773,"id":"Q5756773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928672$B9D5D9E5-696D-4022-869D-05FE2126858C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8e4e04e0d0632c7411bda04d999e41f0fe4efef4","datavalue":{"value":"10.1007/S10817-008-9097-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928672$71F3147D-9D49-44FE-9D59-749C67100FB7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a8121b45f5a2121f5d02e937ed3d255985aa611","datavalue":{"value":{"entity-type":"item","numeric-id":5394605,"id":"Q5394605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ed0d4a8002d98ae475e924c65685a1d36c2409a","datavalue":{"value":{"amount":"+1.0000001","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q928672$AD6BCD25-B66D-44B1-AFDF-50049723DFC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6ac105ce3172a3ea2919fdfcd7f106a4b9e2e84","datavalue":{"value":{"entity-type":"item","numeric-id":2871861,"id":"Q2871861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e8c3a612e59547cb6e897fedeee6ffa37a58f900","datavalue":{"value":{"amount":"+0.9033743","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q928672$4138A3DD-2DDB-4CF2-943E-F71099FDA593","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c7e211299ce00a98c8197ac854eb2bb7a7b76c1","datavalue":{"value":{"entity-type":"item","numeric-id":5747640,"id":"Q5747640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a82b8eba506eaf9075893284b9cc849b37b00d1","datavalue":{"value":{"amount":"+0.89557505","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q928672$340BC173-C1E5-4802-8D2D-05314DC0CF7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"408e6eb37370f869866c0d5e2e591da6ab9b54f4","datavalue":{"value":{"entity-type":"item","numeric-id":3613430,"id":"Q3613430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fef695a5e3b588319bb3e7c5672af8eb51401707","datavalue":{"value":{"amount":"+0.8816345","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q928672$A5971CB0-AF30-42CC-9266-9E76F136A1ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fd5c2832aabbf4b304824c9b3020a0ed9253b4e","datavalue":{"value":{"entity-type":"item","numeric-id":4823141,"id":"Q4823141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb972e1e2c108dba281096b3ba0b10ba5933dac6","datavalue":{"value":{"amount":"+0.87777317","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q928672$3D0894F5-016F-42A3-A999-675B98F1A1F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c581e669ae9408182aff3af608d0ce1c9f3579f4","datavalue":{"value":{"entity-type":"item","numeric-id":5747671,"id":"Q5747671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c535833a8f891512f36adcca22c6741fabd6c151","datavalue":{"value":{"amount":"+0.8750846","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q928672$03BFBE78-DEED-48D9-93CD-A4282CA8EBE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"023c6174d36bd63198106c3557769fe109aec9e2","datavalue":{"value":{"entity-type":"item","numeric-id":1314276,"id":"Q1314276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b309e68e62c05282a747bbad3f7e96f07d60f444","datavalue":{"value":{"amount":"+0.8698789","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q928672$0FC8742D-8389-480C-B3C9-24092BCB92F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f007afffaa9d82c697dfde08e38474d46ab399f3","datavalue":{"value":{"entity-type":"item","numeric-id":1739913,"id":"Q1739913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7b6ee583c8d7fa012f860c2beb77ee2ae96fd33c","datavalue":{"value":{"amount":"+0.86943877","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q928672$02E63186-4250-48FE-923F-107179EEF8D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"19914ff8362a88c613e25c3bea458e1c7b08dd0c","datavalue":{"value":{"entity-type":"item","numeric-id":2945636,"id":"Q2945636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7b6ee583c8d7fa012f860c2beb77ee2ae96fd33c","datavalue":{"value":{"amount":"+0.86943877","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q928672$C0FF8AAE-9CAE-48AB-8D37-008CC3715F18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b403893b3853ccc2d56f9e150dc2696721cc1178","datavalue":{"value":{"entity-type":"item","numeric-id":5891628,"id":"Q5891628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"513a2d374eff1ed70f0d75879b1af515768dee0e","datavalue":{"value":{"amount":"+0.86925215","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q928672$35D1E603-252E-4B17-B2E7-18FA99E464A4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Nominal techniques in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Nominal_techniques_in_Isabelle/HOL"}}}}}