{"entities":{"Q4647561":{"pageid":6677142,"ns":120,"title":"Item:Q4647561","lastrevid":41758642,"modified":"2025-05-08T00:44:48Z","type":"item","id":"Q4647561","labels":{"en":{"language":"en","value":"More Church-Rosser proofs (in Isabelle/HOL)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7001949"}},"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":"Q4647561$3ED96FC4-BF78-4F11-8524-05B59D98FEE2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"94b6e586ee7f3171286b3a882c6d1e9edeb65234","datavalue":{"value":{"text":"More Church-Rosser proofs (in Isabelle/HOL)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647561$A98BF0EF-F7BD-47EB-8AA3-6FB06A68A50A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b91eb346a1f79526cfbc6b9ec30d88cbcc5285de","datavalue":{"value":"1412.68248","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647561$7E3A8138-9203-4D13-8AB6-F77A9FD7A78F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d9162cb8fbe275f54acb0e93bb5bd7efbd265cdc","datavalue":{"value":"10.1007/3-540-61511-3_125","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647561$52D90DB9-183F-4243-A09B-387CF38534AA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd39997decddd4925a8ef09cbbffc4f41d2b1f00","datavalue":{"value":{"entity-type":"item","numeric-id":670700,"id":"Q670700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$17D6BAA4-21FB-4FE9-843D-081E51F2797E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1c1c5ae1cd90ac8f2e7ae6528ac21a720bbd1fe8","datavalue":{"value":{"entity-type":"item","numeric-id":4647495,"id":"Q4647495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$23D904CE-3B9E-470C-AAC5-64B83DEFD311","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647561$CC307263-8BAA-4114-BA84-60AA890CA868","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647561$90DD62EE-8E76-4C65-9D41-BB0A63CF9E4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647561$D7CD5315-F4A8-4D4E-816E-A305D53B0138","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d10feeeed7ae9fddf912992e5b61e743b30a86aa","datavalue":{"value":"7001949","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647561$20DFEBC5-3EB9-445A-A146-B2E509D279C4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7125c0410429ee13b4d4209767f868cc1dc25212","datavalue":{"value":"standard proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647561$E490C12F-EFD2-477A-84CE-A67FE2924638","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48eea116bddf8a4aa136f21923c9bdf061e63c53","datavalue":{"value":"explicit substitution","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647561$35C793B7-BB38-42CF-9D01-64078F8A77B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1a6b59e788f1dba91ec9a6610b00bd47b74076b8","datavalue":{"value":"lambda-term","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647561$8040294E-9F11-4805-8B07-EB834219ECB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe403560b16acc6be8aae0480f4c9361f09c2f9c","datavalue":{"value":"typed lambda-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647561$5530938A-B691-455A-8FED-F9624A0AE7B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c9389ae12e01d8af4be45480dad1535b85784a6","datavalue":{"value":"substitution lemma","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647561$24C3ECDB-D0BF-4EDE-A261-1637006FB87E","rank":"normal"}],"P1463":[{"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":"Q4647561$41097D5D-A4B1-46BA-A76F-25FAD11F771B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$3EB66249-0CE2-4EC5-8F27-20FFC84A6C48","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":"Q4647561$656F50B0-E1F2-49D0-A698-7C279C09589D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$601ADF85-7331-4F55-B213-6063D82D4C78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$70B1BC3F-E560-4BA0-B8F7-4F55229F4579","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":"Q4647561$3B11FA1F-7674-46FE-98D6-04FBFBF07E93","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5bfe07cb8e0b8b5a12fb67449d9297d8d2874465","datavalue":{"value":"https://doi.org/10.1007/3-540-61511-3_125","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647561$2849B418-0EB4-482D-95C4-CB64E984C5A9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"258e64abfa3b45450d9c5cbd9763124adf9983f1","datavalue":{"value":"W2098856123","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647561$2BD8A88A-65DE-4FC6-9CDB-65677EAA2FB4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"787e8787fc0800d23d78fddfd9bf35254e758553","datavalue":{"value":{"entity-type":"item","numeric-id":801050,"id":"Q801050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$D7461FB0-6377-499E-A8B7-EC6E87ECF908","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9679f0826a8d3a4d0ec45661e84b0a0a87a61d3","datavalue":{"value":{"entity-type":"item","numeric-id":3024827,"id":"Q3024827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$8A65E8CE-2F5B-4D8D-9673-8183138186D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5dcacdf82491509f047ffa7adf630e71ade90","datavalue":{"value":{"entity-type":"item","numeric-id":5667469,"id":"Q5667469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$911ED084-0B7A-4BEE-9147-DFA0D46DB099","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$AFA81B79-D7DA-4B19-9BD8-78789537691B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e27c37d270f8213f21ee670514ffa6ee55602a3c","datavalue":{"value":{"entity-type":"item","numeric-id":4246726,"id":"Q4246726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$2B5332B5-3C67-46D4-A422-B732A9E39470","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a550204b4fc9eb077df82e95f8c42f6d0c6fa7c3","datavalue":{"value":{"entity-type":"item","numeric-id":4764621,"id":"Q4764621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$546DFCDA-5ADE-4022-BA8B-BAA62FA6DB29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"347ff5e243a44fe280b61636b43f4d0e72b66679","datavalue":{"value":{"entity-type":"item","numeric-id":4281480,"id":"Q4281480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$553CCD0F-6E13-4ADE-AF55-EE8CDE690C1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$79965E75-52B8-4639-BE62-CEE230D1AEE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5f1a85252a4c0a5bb2b7a3eae3c76b6088496bd","datavalue":{"value":{"entity-type":"item","numeric-id":4296962,"id":"Q4296962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647561$397732AB-1689-414C-BE33-9C74321677CA","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":"Q4647561$8E65C48F-4DC7-472D-BAEB-94644DC7E6C7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a81bce5a2e732ce4597f77ee4cd8a8ee5be58f7a","datavalue":{"value":{"entity-type":"item","numeric-id":1595924,"id":"Q1595924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1dc46660a5f61a39fe23b79fcf9ec8497afbe488","datavalue":{"value":{"amount":"+0.99999976","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":"Q4647561$88852B44-5FBE-4C6B-A961-D12754ACC93E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85ba6d27ac028dc305b8216dcfa65e5505b8e17d","datavalue":{"value":{"entity-type":"item","numeric-id":4415087,"id":"Q4415087"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb15181a6456bd97829a416299f3dfdafa8ed5a9","datavalue":{"value":{"amount":"+0.87740237","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":"Q4647561$02AAB107-3277-4913-86C5-7F695913756D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4b171dde0423d3f48718f03aab437cafacf114a3","datavalue":{"value":{"entity-type":"item","numeric-id":2537972,"id":"Q2537972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8695e94f7353b3788b0fa7bc4975f461a49db36","datavalue":{"value":{"amount":"+0.8580737","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":"Q4647561$260DAB5B-789C-4BEB-8D0D-6EA7D2677CE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ce93b36fbb93578ad5ecba2c0a0680a8f43e366","datavalue":{"value":{"entity-type":"item","numeric-id":5712322,"id":"Q5712322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"54473ff096621de5eefaeb98a702bee631f06493","datavalue":{"value":{"amount":"+0.8551224","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":"Q4647561$18311D44-72A6-4925-922A-0FD24042A24C","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":"0732f7acc8846827a359d3d9ecdae938304eb2f8","datavalue":{"value":{"amount":"+0.84907526","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":"Q4647561$4E207D32-B891-4077-A5ED-A4B28F8ECB85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"973595157d4a9c973debdd266ea66471d4416593","datavalue":{"value":{"entity-type":"item","numeric-id":5718674,"id":"Q5718674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"216b0e31c0bb4a2a3ade8a22705e64591fd21fed","datavalue":{"value":{"amount":"+0.8475937","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":"Q4647561$70E2D2D2-4F53-4019-8CCC-93384DF6BA4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"45d13ef8d6fb57ae2a72aea166ff2dfe0e46e35c","datavalue":{"value":{"entity-type":"item","numeric-id":4435474,"id":"Q4435474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9bfc12a7db1961b305229bdbb9e98ad7354420bd","datavalue":{"value":{"amount":"+0.8466599","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":"Q4647561$40F6BAFF-D4E0-48BF-8A0F-C020F5BCBFFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d8c676f8538b024eb2a80be0edde23296e2c1db","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"48c4be4364a6d6a67f768e729bfa9b06c6516c04","datavalue":{"value":{"amount":"+0.8445908","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":"Q4647561$4A495173-AF51-4CC6-902C-3034F1742B1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4261da25f1e5260ad9d60d7b88b40a714d3efcce","datavalue":{"value":{"entity-type":"item","numeric-id":6156630,"id":"Q6156630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ca79efc32e2122c009440e08804a3a28a6ed398","datavalue":{"value":{"amount":"+0.84303164","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":"Q4647561$88EE39F6-499A-496B-B5FD-7CBBBFEFB3D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bbb66796ebb5d6fd026e0d576e50220ff0462de6","datavalue":{"value":{"entity-type":"item","numeric-id":4457728,"id":"Q4457728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dcad55dd2ba981f268833f56f8b4c899edb7d9c7","datavalue":{"value":{"amount":"+0.8401785","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":"Q4647561$FB2C7B7B-4C79-4228-B4D8-A3031B1CF4B4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647561","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647561"}}}}}