{"entities":{"Q2097420":{"pageid":2108163,"ns":120,"title":"Item:Q2097420","lastrevid":43511657,"modified":"2025-07-30T09:17:41Z","type":"item","id":"Q2097420","labels":{"en":{"language":"en","value":"Certifying algorithms and relevant properties of reversible primitive permutations with \\textsf{Lean}"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7615945"}},"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":"Q2097420$AE73FA41-27DD-4568-BE36-D6A43B2EF286","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ed36b2f2757d64fecf9c8d971c7e2778b439dff7","datavalue":{"value":{"text":"Certifying algorithms and relevant properties of reversible primitive permutations with \\textsf{Lean}","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2097420$31E46FF4-F7BB-474B-BC07-7B59DD17230C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"23b1f8cdee15fbb8dc01add39c7d90e440284fbb","datavalue":{"value":"10.1007/978-3-031-09005-9_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2097420$83722C74-F6D1-48CE-AA77-FD153E170FAB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c4329e2ea841404848d2ea4e6ba499ad648cd9ba","datavalue":{"value":{"entity-type":"item","numeric-id":2097419,"id":"Q2097419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$FE99B706-47FE-42CE-B58D-EE5E19610B93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e7fe2e34ceb1a5a0fc819d5b27ac5700ee0e0306","datavalue":{"value":{"entity-type":"item","numeric-id":737108,"id":"Q737108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$5A684B6D-7666-4BC5-9F74-F92B636439C9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d427d6e8557b276fa99b93deca64aa11553957f3","datavalue":{"value":{"time":"+2022-11-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":"Q2097420$985F28F6-49AD-46ED-A52F-46F0CBDF34CE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2dcd19816c1488ab55b8b2e38be241e5171cde82","datavalue":{"value":"https://arxiv.org/abs/2201.10443","type":"string"},"datatype":"url"},"type":"statement","id":"Q2097420$431619A5-FD27-44C2-A749-E8E41984B54D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"196916cd450165978c169d4fbf15975a01c78c72","datavalue":{"value":"68Q09","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2097420$62E18B50-A37D-4AED-B038-DD8FF676525E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35bbdcbda53152c249a7f99650e19b5ef62999f2","datavalue":{"value":"68Q10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2097420$9BBDDA9B-AEBD-4BEB-92AD-948ADCF392B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7af17f227fda8daecc6b4cd26e5d774fa965085f","datavalue":{"value":"81P68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2097420$CC1C0177-FF7F-4FFF-8D14-C889CDD7E39E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4e7ec8863943e071f32bdb9ad36c8ba69de2906d","datavalue":{"value":"7615945","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2097420$97B498BE-AF51-457E-9A1E-58D782BA81F1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"39d1d25ae8c00cfad058b188db36fd61dac09925","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$79D08309-10FA-4966-8180-A1A45DBF4135","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e262f47aa23786f0d5ca3c491b5060c53e80792f","datavalue":{"value":{"entity-type":"item","numeric-id":18274,"id":"Q18274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$82A2DD85-EF2B-4F8D-B863-FF6869E41FF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8bf42d0fd66acf369e3d5d44d7ebef6adc7ae452","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$0D4AB25A-9C51-4D34-A994-211B49B5A29C","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":"Q2097420$BA7107B3-4C2A-4EA2-9468-7285851F44FA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"80bf7965a3d303aee2d8335b70517c8c89e6e3ce","datavalue":{"value":"W4221143021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2097420$AF4F1FE7-9B35-4B51-89D6-F55AFA597EC2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c8847fc96bd6cc15667c599e80d53cc2bce3050","datavalue":{"value":{"entity-type":"item","numeric-id":2462635,"id":"Q2462635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$094ECAE7-7DE9-49F0-BCD6-C2EA89B78C46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"abc213f810e809eb3818c9e2bbad1ade805e212e","datavalue":{"value":{"entity-type":"item","numeric-id":5875420,"id":"Q5875420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$064BA030-AA60-4293-BEA1-E62535C1DA53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$AB1AC606-0D9F-4EB1-9022-8BAE94880CFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84574726939c563ff0c1d253534b262fc319b9f9","datavalue":{"value":{"entity-type":"item","numeric-id":3076735,"id":"Q3076735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$77430584-5EDE-4AC5-81C4-FA8EC9FB64B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98791e67835c414f0f96760868bb6411dc74eb22","datavalue":{"value":{"entity-type":"item","numeric-id":1123625,"id":"Q1123625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$1C7798FF-EEDC-4F56-8759-E84BE6F7CACC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a6a9a34084d4e9eef8d1389ed4cb5b4c36757fa","datavalue":{"value":{"entity-type":"item","numeric-id":1989327,"id":"Q1989327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$ADD82A6C-7660-4820-A3EA-15618D94B7FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9db4cf58426c9ea10d231a6a0aa9dd7c938708b8","datavalue":{"value":{"entity-type":"item","numeric-id":1401215,"id":"Q1401215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$B8011091-30C1-43B8-84AB-F26D3679F7E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b729a52ad4fc74104ed077cfa51390d6480c163","datavalue":{"value":{"entity-type":"item","numeric-id":2039893,"id":"Q2039893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$B418ABC3-0DE0-48F6-AB82-819B54850AE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36643d132f53e3cc2affee54b5315e94aed0558a","datavalue":{"value":{"entity-type":"item","numeric-id":1684627,"id":"Q1684627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$4DB471A2-B30E-4484-B6EE-50F45EA76F25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"432347ebf7758fa5347be4c601bf2d08f68cb652","datavalue":{"value":{"entity-type":"item","numeric-id":2055901,"id":"Q2055901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$F87B3000-AC60-4908-9B2E-E0A0B01D94C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a32a159641f6324f88615ff8cc2f78a5616d1c83","datavalue":{"value":{"entity-type":"item","numeric-id":4580228,"id":"Q4580228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$E19E2822-675F-4D72-BBE4-64BD965CB56B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d64348ad348372cadfbc43f64ea26ea379dcc05b","datavalue":{"value":{"entity-type":"item","numeric-id":1989331,"id":"Q1989331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$645B1BAB-B08E-405B-B8B0-B962695CC510","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9635365b0780328d7ae22bc69b462e7144999d03","datavalue":{"value":{"entity-type":"item","numeric-id":5573961,"id":"Q5573961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2097420$2E4D213A-3414-4054-ACBE-06BF0EDC6622","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36fc8216571e0cd6eae7b43915c498bf625d0fe1","datavalue":{"value":{"entity-type":"item","numeric-id":865624,"id":"Q865624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"242a8e4ac33a6155fbb45aa11b512a1a20f94a10","datavalue":{"value":{"amount":"+0.85196215","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2097420$94E7E741-44F6-4165-9040-69F1294DDB35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aff48e42a2319914c31cb01d2b0ba341dde70b0f","datavalue":{"value":{"entity-type":"item","numeric-id":3610928,"id":"Q3610928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e3abc192aa81953e72bff444ceaed422c87785b","datavalue":{"value":{"amount":"+0.8318928","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2097420$EC93C1C3-4DB8-4A48-B950-AF0CEC359B2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bfaf442647bbc6d798f065aeb9aa2824de10d495","datavalue":{"value":{"entity-type":"item","numeric-id":1629429,"id":"Q1629429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa5f308f124bd554ad5e14851414774e1d7b3e3b","datavalue":{"value":{"amount":"+0.8193827","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2097420$61AF367C-90F2-422E-9414-3DAE8C00A442","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb7c2e9637caecb5da32b36168ef13c8e571b32c","datavalue":{"value":{"entity-type":"item","numeric-id":6487931,"id":"Q6487931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6c9cb96cec13f43d7d73d72ae33e90d61d26a40c","datavalue":{"value":{"amount":"+0.816473","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2097420$FF99E545-1649-42DD-AA81-BA9DC4AB1952","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b15269f20229a851d891f711ea98b66954ed67d","datavalue":{"value":{"entity-type":"item","numeric-id":5384029,"id":"Q5384029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bef82a4770c3b68257f22913314d141611e077ef","datavalue":{"value":{"amount":"+0.8153943","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2097420$25DBB8BD-2237-422B-8A79-928782D4B8E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e6ef8aa847e42b7458d7e59b4635190c2f7a5fa","datavalue":{"value":{"entity-type":"item","numeric-id":392031,"id":"Q392031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c069734aea7657383bdda386c9190f3cf6ba902","datavalue":{"value":{"amount":"+0.81539166","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2097420$5BA5CAD1-92DA-4DE3-92C1-D02C0CA783EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2255b95106e517ad9da5eea4b1f3c50c9785e3a0","datavalue":{"value":{"entity-type":"item","numeric-id":1306396,"id":"Q1306396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a94650cb3e9a0b1386d169b6778e7155e9a08124","datavalue":{"value":{"amount":"+0.81432074","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2097420$E45627D1-8796-4304-9002-7C36EEBF7009","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"34ea6c39bc0c8ce6d7565d060dc8baeb38576aa4","datavalue":{"value":{"entity-type":"item","numeric-id":935473,"id":"Q935473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9e44075bb7834245a81706318cda45b004da90df","datavalue":{"value":{"amount":"+0.81366765","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2097420$D0475C79-3032-4190-A018-DA9280F4DA58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"86c7a267322cc0f05d0dee152997dd5b2d38fc2e","datavalue":{"value":{"entity-type":"item","numeric-id":3304150,"id":"Q3304150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec7a257d33f1c4c114ef6f68b51e65d895c3af24","datavalue":{"value":{"amount":"+0.8135344","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2097420$609A3623-2C01-409C-BA83-A3BD53A723E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4f3a783aee1c99214f2ccffb145084ad2c4cd9da","datavalue":{"value":{"entity-type":"item","numeric-id":5305642,"id":"Q5305642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"516bd79dee8803f470ba754958c7d2acd98565ef","datavalue":{"value":{"amount":"+0.8118576","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2097420$CBD14554-854C-4A0E-ABFB-C6FECEFC18FA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2097420","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2097420"}}}}}