{"entities":{"Q672051":{"pageid":673900,"ns":120,"title":"Item:Q672051","lastrevid":63452511,"modified":"2026-04-11T13:15:49Z","type":"item","id":"Q672051","labels":{"en":{"language":"en","value":"Using induction and rewriting to verify and complete parameterized specifications"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 984752"}},"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":"Q672051$1D98F085-1D4F-43D1-9794-AA57B6DABCEF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8479c4bc9715e9f19af627f483b5b3f183115858","datavalue":{"value":{"text":"Using induction and rewriting to verify and complete parameterized specifications","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q672051$EFC2CD4C-9790-4358-812D-194DBC034A5A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6500d7286517911a185adbe94a3fb7e06cc540dd","datavalue":{"value":"0874.68198","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q672051$2E85A8A1-1566-4E7E-9FFC-ED5447D617D3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d003b17148f391f27745d10bdb975af05acefb52","datavalue":{"value":"10.1016/S0304-3975(96)80708-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q672051$7F3689FC-6645-40FB-89B1-812FB21419BA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6b3a8b345d1b3ec000ad6c59a5dcb5ae454f5a56","datavalue":{"value":{"entity-type":"item","numeric-id":420846,"id":"Q420846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$1A1FE1DF-0D62-4F6F-92A1-FE1B9B68C946","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$F3CABCF3-7828-4405-B95D-BB73E22DC4C0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b79c82e669aca3d97718bc55c57512b326a2a4ab","datavalue":{"value":{"time":"+1997-02-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q672051$05797074-33D1-41F8-863C-BD1BF0A73142","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q672051$2D63C931-184E-4D08-BAE6-3697D3862767","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q672051$6E3C6D50-D2F4-4537-9B8A-F20EECEFCD2A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6e82c38d982513bbf7200e1ee4c5bb1910c1ad43","datavalue":{"value":"984752","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q672051$7D777F0B-16AC-48C9-8A6B-D97882364D12","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"742acadec2058a1daf33969cf122f1e00d23a668","datavalue":{"value":"Theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q672051$8D2D1B38-ACD6-46D7-B49D-EB86DFD1CC06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba2abb3539be76c93b58519ff322e0c9ebf4e64a","datavalue":{"value":"Sufficient completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q672051$2EB4A6E3-A606-4838-98F6-452244935209","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6da8474f8d21c50120e9b92a90a5c2c42dcc47f1","datavalue":{"value":"Implicit induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q672051$E30F02C9-3C01-4514-83FE-AC3C1E659FA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fc85015729331bee3374f9565b0bcd48d7e98579","datavalue":{"value":"Parameterized conditional specifications","type":"string"},"datatype":"string"},"type":"statement","id":"Q672051$E5D979DC-83B5-4CEE-9C91-FA2E1AA8A769","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f20b94fdbe18dfd6d46086a7f2203c1fd2c14cda","datavalue":{"value":"Term rewriting systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q672051$727370C8-6FEF-4F80-8B4A-8A0C08543F2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6bb3e6707ad691979c2eb28424fc978c7482b8ec","datavalue":{"value":"specification and validation of software","type":"string"},"datatype":"string"},"type":"statement","id":"Q672051$124C189F-FCD6-49FC-BFB4-8A40013A6447","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$237DB3DD-7473-4323-A942-2482A4EE6101","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":"Q672051$E6EF2851-78D0-4943-8A07-C99E9AAF5AEE","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0843e7f8e29d84aa6b7b4f9a110eadf9b3b1959","datavalue":{"value":{"entity-type":"item","numeric-id":1134541,"id":"Q1134541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$81748120-C0C6-48DE-836D-52ABD01788F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33b8955ae00ed7abb114fe381a6f8a5cfac44817","datavalue":{"value":{"entity-type":"item","numeric-id":1327704,"id":"Q1327704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$D37B776A-5383-4B2C-BD8B-170219EDB9CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cd3b148804ef99eb053efde16a24963181caba8","datavalue":{"value":{"entity-type":"item","numeric-id":4537505,"id":"Q4537505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$57E0EB9B-5E58-4B28-B993-39DA400E26D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7199b61e16a84b76da4670f962685e538ce1a13b","datavalue":{"value":{"entity-type":"item","numeric-id":1891255,"id":"Q1891255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$76AF5FE3-694E-4B1F-9FA5-FE241CF2E16C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"032e011dae6771ddc94bd3b2d7b810721cac8c5d","datavalue":{"value":{"entity-type":"item","numeric-id":4849648,"id":"Q4849648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$1259D2AC-A2A5-4D0A-A497-EC4FC4234ACB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aad2711eb9c64a58dada485191047b8af29959d","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$7CD374B1-F055-4661-95CB-E559F8FA2D6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13fea1ac3ee9372cea794388ddfec6d158b780a2","datavalue":{"value":{"entity-type":"item","numeric-id":5055712,"id":"Q5055712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$C6744DBD-B44C-4489-80AB-9C1608ADDF5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c91a62fc73d328b39f05fc8fae0c1a2a5426db9a","datavalue":{"value":{"entity-type":"item","numeric-id":685548,"id":"Q685548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$2764231C-0449-4866-883F-3D220252A154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcf8150531dd139e92d199e5424737b99d920576","datavalue":{"value":{"entity-type":"item","numeric-id":3785921,"id":"Q3785921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$8D9CF265-6B1B-4D30-990E-D6606566A422","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d6d3f5f0e6d39b0610560c479018fc71a2adcd20","datavalue":{"value":{"entity-type":"item","numeric-id":1098624,"id":"Q1098624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$908002ED-B9F3-40C9-BE88-CD402ABAE9F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a01d4a91dcf05e247efe3d36d8b1cf5c4792f88","datavalue":{"value":{"entity-type":"item","numeric-id":4385532,"id":"Q4385532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$16E10D10-DF07-4751-8A8E-65443E6DA1E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35f820e9c2b45f8f035a710ad26c0ff0e5c7ae48","datavalue":{"value":{"entity-type":"item","numeric-id":3221381,"id":"Q3221381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$F8899A72-214E-400A-9E15-6599A7297C3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"706dc1bd0a674d2529cf7888615cc60a3ec2ecd9","datavalue":{"value":{"entity-type":"item","numeric-id":1824381,"id":"Q1824381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$39E64EA0-2CE0-4BA2-8153-7BDEB4BE8E19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2ce7d0f1851c452c921612fdb804e4aabed6d9f","datavalue":{"value":{"entity-type":"item","numeric-id":3753472,"id":"Q3753472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$7783319C-5289-4CE1-867B-7C7B683FF561","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f87c691854819eec4f1d4808c08af46178b8c12f","datavalue":{"value":{"entity-type":"item","numeric-id":4168047,"id":"Q4168047"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$79BD9FCB-E47A-4EC9-B1D4-4FE2467A5F85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2b333869fe483ea43fd2b8640b2fdfa1360b3169","datavalue":{"value":{"entity-type":"item","numeric-id":1243118,"id":"Q1243118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$876DBF4D-E83A-44D0-B682-1DCDF4EEA3ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c3bc7f7b1ada9047dcaf5db1ffaa7831a76d111","datavalue":{"value":{"entity-type":"item","numeric-id":1332338,"id":"Q1332338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$E122EA33-B33E-4122-8CD4-378EE849F93C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fdeb57f4e5d37efa40bca3185df7185c3f2accb6","datavalue":{"value":{"entity-type":"item","numeric-id":789177,"id":"Q789177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$F5FC5E75-CDF8-465E-AD43-4A78F45E63B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1c5bfb17208f024589c23d81de3c137cadf1eb4","datavalue":{"value":{"entity-type":"item","numeric-id":1824382,"id":"Q1824382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$D530DEBB-B05A-48E7-9D0F-24C6F1466ECF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b13b7d31e58c7507203cbbccf857b418e8e5f66a","datavalue":{"value":{"entity-type":"item","numeric-id":1077161,"id":"Q1077161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$C568ABDD-35A5-4A42-9E73-5CBDA4570C1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"407daa1c47ad4e1b7bcdfae46df97a17606dddfa","datavalue":{"value":{"entity-type":"item","numeric-id":3338226,"id":"Q3338226"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$7B6EE6F3-2A2B-4E3D-A6E3-04E7BB6065B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbe37ba60d1d38231cb146c0ce87f7bab99a4d36","datavalue":{"value":{"entity-type":"item","numeric-id":3690200,"id":"Q3690200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$B94F03DF-078D-41DB-9A17-506C50A40156","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17f28bd12adf4f08b88e1bc9b70377dc99daeb17","datavalue":{"value":{"entity-type":"item","numeric-id":685352,"id":"Q685352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$C0723609-3901-40D8-A06F-FB716CEA3445","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7409adbeea4f06044f7b07a21aeeb141df7f0f2","datavalue":{"value":{"entity-type":"item","numeric-id":4712663,"id":"Q4712663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$E3D32428-92F8-4E44-B1EF-9E90F06CECB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"57cb7ce19da7a8c3d5223412ed1f311d14ff605c","datavalue":{"value":{"entity-type":"item","numeric-id":582891,"id":"Q582891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$792DD581-2D47-4A02-B1CA-A58E0A26E4EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d5b94812a0e7aa016cec7465e67fecf8fe8776a","datavalue":{"value":{"entity-type":"item","numeric-id":3034806,"id":"Q3034806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$842B9387-30CD-4E8B-9821-9C7936E9E70B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20b5bfa39edb1e5cd1ff35590d2c16f57053d8c3","datavalue":{"value":{"entity-type":"item","numeric-id":3345752,"id":"Q3345752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$D9652E42-4DF0-4DA3-A0FC-DDE77CC8CA7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de728b9d953b2c3c8ccc15e03a99271c3458b240","datavalue":{"value":{"entity-type":"item","numeric-id":1089794,"id":"Q1089794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$216F0435-F515-468B-A04A-7DD6732473DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c1c64aa77167c6580cd7c8c676f0c865faa32857","datavalue":{"value":{"entity-type":"item","numeric-id":4385539,"id":"Q4385539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$2B5E06E3-CF4F-4E48-B052-15A57243BCFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4c644393292b3f41469d648371f2669fdfbbd2a","datavalue":{"value":{"entity-type":"item","numeric-id":3805961,"id":"Q3805961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$6952C653-73AA-4A89-B0DB-5999A532E274","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8b4be2af9bc9dec67e639e18e42b9279d7a45c9","datavalue":{"value":{"entity-type":"item","numeric-id":6488578,"id":"Q6488578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$7D921F8D-9568-4D42-958D-81DB1D38E6E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4098701b77640969d6c5a6c2843a41c1bc5c5110","datavalue":{"value":{"entity-type":"item","numeric-id":6488529,"id":"Q6488529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q672051$07E30610-631F-490C-A964-BFCDCA0274A2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"32e87c7b7d10e5fc836a26638355ff86f7d1ce2f","datavalue":{"value":"https://doi.org/10.1016/s0304-3975(96)80708-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q672051$5B5D36B7-05DD-43D9-9D8E-101542F206D1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a30b6fe1ee608314807f0324911c59011ec9143d","datavalue":{"value":"W4246703498","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q672051$80ABE216-7F06-40FA-9CB5-51296FF9E83E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"976f6bfeefc2d3ac1125a9d7ceceac0920db7baf","datavalue":{"value":{"entity-type":"item","numeric-id":4537505,"id":"Q4537505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0fc7a8b56eb847268a61a6ee1dffa0c51fe05abd","datavalue":{"value":{"amount":"+0.8748124837875366","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":"Q672051$103D1085-2C2C-4AF2-AF67-B507DB62890D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec40261e8004852901d410e10c4f66c1792c328c","datavalue":{"value":{"entity-type":"item","numeric-id":4849648,"id":"Q4849648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f2e164baf0cff308238bef1f2eb34eb61e5f4952","datavalue":{"value":{"amount":"+0.7288933992385864","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":"Q672051$F41FECCB-23F7-4878-9F01-47E8C8B8DE42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1f284b16a2afee30940b5ef7c2361f8cb8e04521","datavalue":{"value":{"entity-type":"item","numeric-id":4551131,"id":"Q4551131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cf97e00257ce7539a09bcb00b7a44d2f404701c5","datavalue":{"value":{"amount":"+0.7244918942451477","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":"Q672051$41AD1E28-A784-4279-9649-7D70F7F131F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52b4a2fec8240cef8b3354cfe1bcecda862f0031","datavalue":{"value":{"entity-type":"item","numeric-id":1355757,"id":"Q1355757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5ef1fb159bf5a95a4828ae8339f6c853885dd29c","datavalue":{"value":{"amount":"+0.7160501480102539","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":"Q672051$11B92E5C-0666-431B-AAD3-21AAA2155438","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ec2537dcea7490ca8d09c48004d99af17f31f3f","datavalue":{"value":{"entity-type":"item","numeric-id":1607227,"id":"Q1607227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"740feba7652b783791b7218a1cf2286822d588e6","datavalue":{"value":{"amount":"+0.7148400545120239","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":"Q672051$3F9B8146-34FF-4F7C-B5A3-FAFB11155586","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Using induction and rewriting to verify and complete parameterized specifications","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Using_induction_and_rewriting_to_verify_and_complete_parameterized_specifications"}}}}}