{"entities":{"Q5236557":{"pageid":7266125,"ns":120,"title":"Item:Q5236557","lastrevid":100612208,"modified":"2026-06-05T22:34:41Z","type":"item","id":"Q5236557","labels":{"en":{"language":"en","value":"A case study in programming coinductive proofs: Howe's method"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7114858"}},"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":"Q5236557$E255C3A7-74E4-41B2-B92F-FD8D61B33B26","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b616fd62478cffc6f10d3526ca5aa22d4ccca768","datavalue":{"value":{"text":"A case study in programming coinductive proofs: Howe\u2019s method","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5236557$BAC73EFE-FAB4-4F6E-8286-6F968FCA1E7B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"36e523fa625daa115dab9a47b636f31e69c3fc69","datavalue":{"value":"1430.68418","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5236557$F961A702-5628-40D6-AE18-02BB9B3C8D03","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f478040714f184e0c41f1fa84c1ba25bcacfe186","datavalue":{"value":"10.1017/S0960129518000415","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5236557$0AC9853A-02CF-4A1F-BB4F-E6A8A0EE3B53","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8135914452c3b1bd839ce74f3161ea4765c65f58","datavalue":{"value":{"entity-type":"item","numeric-id":287276,"id":"Q287276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$62E2D815-D01D-41E1-BC29-34779CA7B07F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8825a5f48e59e5b1e1510e59d52fce48da47c37b","datavalue":{"value":{"entity-type":"item","numeric-id":229739,"id":"Q229739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$F19F34C5-87B4-4937-8A79-03A184627F4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"737d28b070ce0e465798910a7ca8a8d691df24ea","datavalue":{"value":{"entity-type":"item","numeric-id":2931779,"id":"Q2931779"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$AE84FEBE-0FC5-4338-9251-FF00F1A61DC0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a53527e88e2413966f3c8ce14c92b878c452756d","datavalue":{"value":{"entity-type":"item","numeric-id":2709784,"id":"Q2709784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$067327F5-457E-43E2-97B3-27360C5DC4B8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"69528ab356cbcd2b53ea1b91a6f142ab0edc04fe","datavalue":{"value":{"time":"+2019-10-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5236557$6B41A459-449F-4C7C-BFAE-D2D1B2638344","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5236557$D5CB454B-C0FB-469D-ABF3-7A62C4759760","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5236557$5BBCAB7A-C473-4DEA-81D2-89ECFEBFC50C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5236557$0192DDED-D688-40B6-864D-7B94DA7737DD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"aa53dc981e3b2f904bd6b5cce10d984534435581","datavalue":{"value":"7114858","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5236557$2118E43A-5D9E-40C9-B6F3-E2EBD97BFC3B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"32c4c1126d2e4aefe4cff937dd992e10025c7d4a","datavalue":{"value":{"entity-type":"item","numeric-id":40287,"id":"Q40287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$66556332-5B2C-45F8-BC91-4A2F050A69E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0ca68d9e60f39b64375620b23802b5755dae3004","datavalue":{"value":{"entity-type":"item","numeric-id":13181,"id":"Q13181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$70844327-91F3-4D68-8573-71C2CDB8197D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a8e56b54ce67b3f3451fae93e0a157bd7197fba1","datavalue":{"value":{"entity-type":"item","numeric-id":21444,"id":"Q21444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$5C0A9E83-C87B-4C41-A11A-D8459F1D17B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"040fe209bf9959da562393c0e37eb31592733af3","datavalue":{"value":{"entity-type":"item","numeric-id":18957,"id":"Q18957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$7334AE69-B1E4-42A3-8F0A-02487A96C165","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a8b05ec686e5cf36ec21c150af705733aeafe240","datavalue":{"value":{"entity-type":"item","numeric-id":21443,"id":"Q21443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$D4047A1F-1FAF-4F11-9429-5B5FAA6D708F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"be9a1fdbfd35f7a816de32e6d9d9a2a21796c942","datavalue":{"value":{"entity-type":"item","numeric-id":14061,"id":"Q14061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$14083B51-055A-4C3A-A729-D4DE1FCC7FA0","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":"Q5236557$7B5CB796-37A2-4E44-97F4-455559E22D91","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"555a6bc000d2f039cfc9a1bcf575e75116c38a03","datavalue":{"value":"Q113857439","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5236557$E133FC5C-FED5-4D06-919F-6E2189F6B8F5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca11fe1f982499343bac9427de06937796502fa1","datavalue":{"value":{"entity-type":"item","numeric-id":5854733,"id":"Q5854733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$DB8306F0-D818-42A9-A3A4-5FDF9E1FD074","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"02420b55b611e11c71fb1baf0d07be65f4765be8","datavalue":{"value":{"entity-type":"item","numeric-id":5244799,"id":"Q5244799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$26201543-A569-49FE-AB18-94391D18F865","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"435cf13af67db4829ca178e89f130660572eba08","datavalue":{"value":{"entity-type":"item","numeric-id":5371960,"id":"Q5371960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$F48882BA-657D-4373-9630-EF5DAA8F4038","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"57ea5885832b9f867e6bed74c7137f05eec86479","datavalue":{"value":{"entity-type":"item","numeric-id":2931780,"id":"Q2931780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$D803C7D7-2EEF-4D2E-BDCE-F6E37A66A35D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8daf58587decdee95f676a746bd278ed5978d708","datavalue":{"value":{"entity-type":"item","numeric-id":2639646,"id":"Q2639646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$9499D68C-7D9A-42E2-9971-8D5EA0EF2B1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e540e9037d6b40bc6045b99bb685bc55f586971","datavalue":{"value":{"entity-type":"item","numeric-id":5899009,"id":"Q5899009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$D3FBC4FC-05EA-45BD-AA9E-D3F7D9E28579","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"840c436709544b9e020f8c895cf807de817d2fa7","datavalue":{"value":{"entity-type":"item","numeric-id":4945209,"id":"Q4945209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$E58EEC2D-FA3E-475D-8202-52AB2FDC52C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68ef8bd5491561954e053fb17a1031115fe3ad2f","datavalue":{"value":{"entity-type":"item","numeric-id":5195258,"id":"Q5195258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$013A05E1-12E7-4F0B-B093-ECB199874FCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb1b7ba883393415c2d36d90450052b088071aaa","datavalue":{"value":{"entity-type":"item","numeric-id":3395094,"id":"Q3395094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$E4B8807A-66BE-4BEB-ACB7-9CEA491F54DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c70a06f78fc76ccdc546da5eeba08398205a2ab2","datavalue":{"value":{"entity-type":"item","numeric-id":5890661,"id":"Q5890661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$BB9FAA45-8D9C-4F63-8625-5CD1C569DA4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52bc2eece43ed61a28c0516dc0b9048a4a049547","datavalue":{"value":{"entity-type":"item","numeric-id":2392480,"id":"Q2392480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$08F3BF67-5B7E-4ED2-85E4-B0034ECFD461","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db61eae6405ea4040df4fc3178f4852033f053c3","datavalue":{"value":{"entity-type":"item","numeric-id":1687535,"id":"Q1687535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$206AD987-8D7D-438C-A6D1-3727158F3445","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"228e40236d38aec5a149d907ee03718626a60ccb","datavalue":{"value":{"entity-type":"item","numeric-id":2942890,"id":"Q2942890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$80BF1779-1432-4C5C-9132-675FC7CE4997","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49e822b9519102ec9cf37138315fbebea8b02bed","datavalue":{"value":{"entity-type":"item","numeric-id":4691187,"id":"Q4691187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$271B15C9-D637-4E33-944A-BF9EB06F33E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9159ab811fea29e4217d139fe47c9288447836f7","datavalue":{"value":{"entity-type":"item","numeric-id":4593089,"id":"Q4593089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$6A8BC524-CA14-4477-B1F7-E53AD2AD1316","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd3637f322544aae9daf432caf7314a879834a0e","datavalue":{"value":{"entity-type":"item","numeric-id":2864153,"id":"Q2864153"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$9EC6B3CD-7116-44CA-8D2C-CAE05832C161","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ea3d89d9caeecb4ce96d5251e582d3bc04e60e3","datavalue":{"value":{"entity-type":"item","numeric-id":438569,"id":"Q438569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$45C1DAC4-B5B5-45D4-A0DE-CC2183C24E05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c8061bdff8d9877d2f27aa012efd61f9a2baf74","datavalue":{"value":{"entity-type":"item","numeric-id":1426872,"id":"Q1426872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$F79B8EEA-0DE6-4570-B8B3-2E67D14DAC9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50a57ad67cddac85a1ec8508c32d92cfd4c3ce3a","datavalue":{"value":{"entity-type":"item","numeric-id":2754137,"id":"Q2754137"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$6574EE62-280B-4A6D-800A-BC15ADFBCB23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$20E2F80A-A70F-4C85-9355-50AA4FEE55B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4db8f7fa996304ee694716b3fc5e63d2e83c95b","datavalue":{"value":{"entity-type":"item","numeric-id":4365103,"id":"Q4365103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$9709A0F0-CB5E-4D4D-ACED-AFAC2F0873AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bce890db8f764308dc9d80705e866747b01fc19","datavalue":{"value":{"entity-type":"item","numeric-id":1589654,"id":"Q1589654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$EDA3AD21-479F-47AE-A8BC-14031D65C3B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef8e8a1bd6a36d7048ab6f3cc2d1559d18184388","datavalue":{"value":{"entity-type":"item","numeric-id":1917068,"id":"Q1917068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$EB63964F-04F6-43D9-9A66-A9515D1781F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40cf805708d5244e0778594004beeb56a3aa4f91","datavalue":{"value":{"entity-type":"item","numeric-id":4993349,"id":"Q4993349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$6AEA9321-6FA1-4057-AE86-16B8CBE3DC55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6063e4a144bafe1447ae8b10555347d26c418f1d","datavalue":{"value":{"entity-type":"item","numeric-id":3189797,"id":"Q3189797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$65D3568F-BB38-4122-92F2-BEF6BCEDE20A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2cfd9276b29fad8afcdadbaa91529b52a92d469","datavalue":{"value":{"entity-type":"item","numeric-id":4939702,"id":"Q4939702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$91791ACC-F705-4879-891A-A0DD5ED8D5C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ceef3820186ecaca212e35a14a25eaea029f2d8b","datavalue":{"value":{"entity-type":"item","numeric-id":4222839,"id":"Q4222839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$A1535827-74BE-4BCB-8143-3228CE90F427","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d380a2f18f4b02ba06d230258197a946757b5301","datavalue":{"value":{"entity-type":"item","numeric-id":2891520,"id":"Q2891520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$436BBCC8-25A1-4C55-8CA6-000EFD44F844","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d06ce65b366ea27e58c7fffc25863f35a8053f5c","datavalue":{"value":{"entity-type":"item","numeric-id":5277739,"id":"Q5277739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$E2F2D451-FE74-4168-9B24-27B58E4D3FA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6fe3949a60e4535ad5a0b04a8726d37af9ca0c6","datavalue":{"value":{"entity-type":"item","numeric-id":1249567,"id":"Q1249567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$2752CC28-7045-40F0-B970-78D65636ECA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"197d74f5936655045aac39c4e29d461e14c3e18b","datavalue":{"value":{"entity-type":"item","numeric-id":2844810,"id":"Q2844810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$F6D960FE-153C-4B58-B8F0-D3D8CE65204C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"748a5362203b0e3c8347ebddbc722eb15910d45b","datavalue":{"value":{"entity-type":"item","numeric-id":5712312,"id":"Q5712312"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$6E1C0D72-93C2-40E8-907D-37C2B3F42FCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"45d621c08d6b6b648b2f02de3b6f7c65499ed1c5","datavalue":{"value":{"entity-type":"item","numeric-id":5277812,"id":"Q5277812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$2B9E0360-73E4-4DEC-AA80-1998B29CF8B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef704b25a56efa5b64e7d48076eb438fae5430f6","datavalue":{"value":{"entity-type":"item","numeric-id":5740353,"id":"Q5740353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$B08EEF39-6D1B-4A04-8160-C8C4CE63E844","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"441ab522372dbc56337549e9359e4e2646de59a9","datavalue":{"value":{"entity-type":"item","numeric-id":850496,"id":"Q850496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$5CCF5D97-35E8-4622-8901-E9FF1F1B159E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88dd97334618a8abcb30d6b953aa7791488fcf62","datavalue":{"value":{"entity-type":"item","numeric-id":3189856,"id":"Q3189856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$5B590B08-7C04-47D4-AB87-C231AB240D66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6b19eae06ce0ec3719d39a65466af8f728d39032","datavalue":{"value":{"entity-type":"item","numeric-id":4912883,"id":"Q4912883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$FF6DA45C-D60D-4060-B091-8AB5E4EBEB14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db64b11464b9db48e2a389bd15fbba45af72595f","datavalue":{"value":{"entity-type":"item","numeric-id":5277845,"id":"Q5277845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$59C14DBF-5D64-4CDA-9CDA-82CB3A5AD58D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c251862798025af0ed73cb57538684bb7c1e6c74","datavalue":{"value":{"entity-type":"item","numeric-id":3454100,"id":"Q3454100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$917DAFCB-A48D-4C18-B1D3-FB028F148AEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a90a510f27550100d45a2ef21dd83bca5c9e1966","datavalue":{"value":{"entity-type":"item","numeric-id":5747747,"id":"Q5747747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$690E0D6F-47B7-45B5-B472-BF0C5874CC0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"232426b4a336ce9f56636b166cfd296a7cb0f2d0","datavalue":{"value":{"entity-type":"item","numeric-id":4225152,"id":"Q4225152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$E3D4B3D4-308E-4173-8F0A-497DE0553034","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f01ca5b15c47313f7b671862581171333a66b86d","datavalue":{"value":{"entity-type":"item","numeric-id":5713333,"id":"Q5713333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$8F8A1CDD-ACFE-4E66-B4DA-93579D8CEDC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98edad3dda6c3e0d16bb29f0b88b1d7d3ea29372","datavalue":{"value":{"entity-type":"item","numeric-id":5411983,"id":"Q5411983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$3C5E62BA-04D7-4DC0-90AD-AC22C5C859A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ca7d3d7743469415e0b8a942df4c8fb49dca870","datavalue":{"value":{"entity-type":"item","numeric-id":2985784,"id":"Q2985784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$DB556500-2D07-43E6-9F9F-F2D67D04846B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c34d25a135933d7bf5547de5ec4476805acc9a84","datavalue":{"value":{"entity-type":"item","numeric-id":2946601,"id":"Q2946601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$35044847-9899-4C1C-B0C8-0B89C80AC91B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"39c8c114ed91e2eb27d97fbae8c341950e41db76","datavalue":{"value":{"entity-type":"item","numeric-id":1948276,"id":"Q1948276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5236557$2EADDB10-351C-4C60-8FEB-B24F599B79C9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"437a4c437d8263d00b48a0575b6cdd090f34dee7","datavalue":{"value":"https://doi.org/10.1017/s0960129518000415","type":"string"},"datatype":"url"},"type":"statement","id":"Q5236557$E989889D-7EE5-4888-966B-EDA5F09F3012","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8b616b72f12c95c111042d7e20c6161ec3b257b8","datavalue":{"value":"W2899165262","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5236557$0BCFED56-2DD7-4F72-9D72-210D1D578987","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"058758f3ede8cf6908f9bf9e85cb8f830d733728","datavalue":{"value":{"entity-type":"item","numeric-id":4691187,"id":"Q4691187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"075b21642f1d5b4801f91802454f588b943af5ff","datavalue":{"value":{"amount":"+0.8100125193595886","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":"Q5236557$26DC32EB-9284-433F-8F42-CF9A78520A77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c0e5426d4c0e5bba93b5ee526cdb5460471ed3ca","datavalue":{"value":{"entity-type":"item","numeric-id":2844810,"id":"Q2844810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16dede1c85efc7b50185fbb3e9dc85666951ca4e","datavalue":{"value":{"amount":"+0.7827931642532349","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":"Q5236557$9D9F0BEA-0838-4EB2-A9BD-8FE168285485","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d4b130ba3f3ab353eb95092c98b979c20e43019","datavalue":{"value":{"entity-type":"item","numeric-id":3454100,"id":"Q3454100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0621b53bb2edd32dd4196678ba08f6a60e99e50e","datavalue":{"value":{"amount":"+0.7797847390174866","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":"Q5236557$094E9A06-129C-4514-A10B-E61130294335","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d137986f3dc22bc7b0d815cd3bc6f3b059425f28","datavalue":{"value":{"entity-type":"item","numeric-id":1589654,"id":"Q1589654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71dd02b70333a8c597ca09669cad0f88fd43eb23","datavalue":{"value":{"amount":"+0.7509082555770874","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":"Q5236557$FC0AFC02-55B6-408B-8158-5E47DFC9142F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"70286fac7be6acb12f06a88f182bfec6859f4591","datavalue":{"value":{"entity-type":"item","numeric-id":2863895,"id":"Q2863895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"34a43dad3a7bfb4f96ce0fbea253d3942207fcaf","datavalue":{"value":{"amount":"+0.7465705871582031","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":"Q5236557$07B5AAC7-E3B3-4069-81AD-4310A39E931A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A case study in programming coinductive proofs: Howe's method","badges":[]}}}}}