{"entities":{"Q2938044":{"pageid":2948764,"ns":120,"title":"Item:Q2938044","lastrevid":44749143,"modified":"2025-11-25T18:30:08Z","type":"item","id":"Q2938044","labels":{"en":{"language":"en","value":"Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6385861"}},"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":"Q2938044$FC537400-5B5E-4FDE-9349-1A74FEA58469","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2dcc303c3ee0324399860045740c43c9c1a4f828","datavalue":{"value":{"text":"Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2938044$A69ED684-7D42-419F-8300-3E1D02F3108F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8e1ae7b7beec9525a98d537b166754ff595af1eb","datavalue":{"value":"1426.68284","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2938044$7F0CA562-3D97-4066-B40B-27EAF21401F7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b0d69c95645a393b0defd7fa9f642278163bdcc5","datavalue":{"value":"10.1007/978-3-319-03545-1_9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2938044$DCA487E3-08C3-40BD-AE34-20615D0A33DD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ab2f745f26ee211bc2fd3f1017cfc1bf31e01f03","datavalue":{"value":{"entity-type":"item","numeric-id":832213,"id":"Q832213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$8A8F50B9-B630-417C-8A3A-2ECA397924BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb18cf0542c9d5785b9c3d13ac135abc8a7efb68","datavalue":{"value":{"entity-type":"item","numeric-id":1687532,"id":"Q1687532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$164D5ACC-B60B-4071-AFB7-C1A415CB52E7","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"19e7468504fbcb9c3a09d3a38cdd67d03e02eec6","datavalue":{"value":{"entity-type":"item","numeric-id":2938035,"id":"Q2938035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$5D446B05-950E-4318-8250-6D9192F41AED","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7326fd6e0963f01b5d05d75894cb7d24907c61f1","datavalue":{"value":{"time":"+2015-01-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2938044$648E797F-A1A0-493B-AA91-08CCECEA0232","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2938044$2DE7DCB1-8036-4F03-A3A5-E9D7EBD68CA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2938044$3483685C-B8E3-42C0-9273-AA24F579100C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9ac38ec6ff0bd9b3ac3965e8726cf52b67b9e05a","datavalue":{"value":"6385861","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2938044$6A44B934-1FB4-4791-B549-C4FD2C821E15","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":"Q2938044$1BC2D82D-E727-465C-A161-27AAE3509723","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":"Q2938044$F7B540F0-5B1B-4EE2-BC17-5EE169C3040F","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":"Q2938044$4682912E-2A75-4740-8027-36148BC053A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ed664df4807a1c1480dbcce90c73c0ac4e6b59b6","datavalue":{"value":{"entity-type":"item","numeric-id":24733,"id":"Q24733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$A71A255A-6346-4052-BFCC-5541F77B1F84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$EEEB11A5-EE39-45F2-AD9D-71C02784E357","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e9fd7dbff509abaee9c64d21afb19f85055bad01","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$8075B28F-258A-49C3-AA1D-03FC36AC68AA","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":"Q2938044$FAD799F9-425C-4498-B711-DC8ED0A88FDB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2583306edef8244bf58ceb543872f0f03f541380","datavalue":{"value":"https://doi.org/10.1007/978-3-319-03545-1_9","type":"string"},"datatype":"url"},"type":"statement","id":"Q2938044$FEB8EA8F-585C-4F4A-AD6B-C84BC9EB2A5F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"55f0d7480b60db261a8ef7b06acc448db5196611","datavalue":{"value":"W101424827","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2938044$B15C1590-4E3D-4028-9CE4-905ABF82D48E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d09d0d80888862919dac2ac00b2537e3464cf8cd","datavalue":{"value":{"entity-type":"item","numeric-id":5898175,"id":"Q5898175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$3F9E26CD-AADD-4D52-9D4F-6F5130066E15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da0d795517e293a55fbffeee6d84c637293c8bf8","datavalue":{"value":{"entity-type":"item","numeric-id":5327339,"id":"Q5327339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$B091F639-E591-467C-966D-3E9414A56FE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6496304f13783e82d12a275120aa4626825ea47b","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$2D2D5704-B5EB-4550-B540-33A3205CECA4","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":"Q2938044$2DB02F0E-CD90-4FEC-A91D-FA2340BE147E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50b0bfaa5604fbbf1607bb7e54efdd2fee887b49","datavalue":{"value":{"entity-type":"item","numeric-id":5327338,"id":"Q5327338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$2D6092CF-AA7B-4229-88BB-4AB800B2FB5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d60ce31f335bad429a6e1e462b560a699f61e298","datavalue":{"value":{"entity-type":"item","numeric-id":3559761,"id":"Q3559761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$76FAD663-4C36-46B3-A443-23C92102E028","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9f3d1ae30c91383ada80e5423ca9f4c05b9f2dc","datavalue":{"value":{"entity-type":"item","numeric-id":5277759,"id":"Q5277759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$23BBE74A-5A6E-43FF-93E0-68E1FF8D8009","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1fc734969332adab85b3154962e23089626b98e0","datavalue":{"value":{"entity-type":"item","numeric-id":3075239,"id":"Q3075239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2938044$BEC94F64-E75A-4345-8FDD-95B49BD9AFDB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6355fdcd09db84aad056c40c86e8fba6296f0644","datavalue":{"value":{"entity-type":"item","numeric-id":3582695,"id":"Q3582695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"df09a3e8e84f380d61a86c379180b959b1c0802d","datavalue":{"value":{"amount":"+0.86070484","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":"Q2938044$E91CDE1E-E0DD-4D86-871C-7EC96F2D8EC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7e4383c2ecd4e64a678e674cd670b84f21f373f","datavalue":{"value":{"entity-type":"item","numeric-id":4484345,"id":"Q4484345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8bc3d228cc85348845ad6d2cac5d3e651424b761","datavalue":{"value":{"amount":"+0.85093737","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":"Q2938044$C244B37A-75F2-4ADC-A3AB-83DC0F004592","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"98799b2eaa33c26b0299e74c57dd07d2ffe3836e","datavalue":{"value":{"entity-type":"item","numeric-id":5049005,"id":"Q5049005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2bdac0ecd9e4b23fde1f551fe24af46c63057419","datavalue":{"value":{"amount":"+0.84744924","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":"Q2938044$DA41F68A-8BBD-4869-8AF4-67EA7E1AE618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c21c4cd5d4993c28f29a090d2fcc426973edfae","datavalue":{"value":{"entity-type":"item","numeric-id":2280211,"id":"Q2280211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7105a75ee0138a70469018f50b67e7d44d6a0052","datavalue":{"value":{"amount":"+0.8474391","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":"Q2938044$67DFCE5B-CB7D-4203-ABF4-9E747AF60666","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a24a8ae0cfdf13ea75f0df7294b258b87d416140","datavalue":{"value":{"entity-type":"item","numeric-id":2879246,"id":"Q2879246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b20c3c2bbee386e2b727be92f9112a70753dc02","datavalue":{"value":{"amount":"+0.8401287","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":"Q2938044$B1C54876-9372-458D-A442-28A940C21F8E","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":"3d393e3e95fe616b4da3a0eb9835c5a1e2189f77","datavalue":{"value":{"amount":"+0.8396005","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":"Q2938044$3AF92574-D368-4877-87EF-6B20AD517B28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d5c10f469ebd8973e02cfaae23e4767153b3bb7","datavalue":{"value":{"entity-type":"item","numeric-id":2723411,"id":"Q2723411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b2101a492f849fafc011e04344f8fbab580fb938","datavalue":{"value":{"amount":"+0.8366391","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":"Q2938044$957AD2A0-3FD8-49ED-AB48-286B6E808C40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ca334c71b2f31093563b1df55327e8a824bfeca","datavalue":{"value":{"entity-type":"item","numeric-id":5415649,"id":"Q5415649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d8314ee78ab4f351a3c907e4c9e99067bda9d9d7","datavalue":{"value":{"amount":"+0.8355734","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":"Q2938044$43982976-9465-4D6E-91FF-B053EC3ABAF2","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":"30ba54fe46e83b101afe29660f1fd8441dc91650","datavalue":{"value":{"amount":"+0.8273744","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":"Q2938044$6D2F23A6-9C2C-409F-957F-F759B330CB3F","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":"30ba54fe46e83b101afe29660f1fd8441dc91650","datavalue":{"value":{"amount":"+0.8273744","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":"Q2938044$6837A2D2-AAA7-4A36-A050-234148E1D41B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2938044","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2938044"}}}}}