{"entities":{"Q7361319":{"pageid":31519496,"ns":120,"title":"Item:Q7361319","lastrevid":105364835,"modified":"2026-10-07T13:35:30Z","type":"item","id":"Q7361319","labels":{"en":{"language":"en","value":"Digit Expansions"}},"descriptions":{"en":{"language":"en","value":"AFP entry Digit_Expansions"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e6345a7a462b438d6319920ee08203f962a592fc","datavalue":{"value":"https://isa-afp.org/entries/Digit_Expansions.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361319$4BBF4462-48AB-492A-A381-6200237F6CB7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c21a91fa45947d63dbf4fb3cbc276ef8f54ca614","datavalue":{"value":{"time":"+2022-04-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361319$06112BF8-DDE3-4F4A-892C-99C11DF3A1E0","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"513ae4cf8772b3600f64ec8b3727a8b18d283806","datavalue":{"value":"Jonas Bayer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361319$3B8B103E-78FD-4480-823A-71997DA9E91A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"abb45793b00bbdb32cc9b9d2f6615590597dc328","datavalue":{"value":"Marco David","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361319$BA8F9E34-4080-4761-9368-D40A3A2D54CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"efb964987721d70357dea1ecc08781cff6b7678b","datavalue":{"value":"Abhik Pal","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361319$ADCCCEF7-ECB4-4860-8D8E-A912D46CBCCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"e4263d236ad6412ef29433243ce063338dd41980","datavalue":{"value":"Benedikt Stock","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361319$9FA282A2-4F51-403A-809D-4964532C9A99","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"649d0c3c51eb7d33470dab528f747fee072b64c7","datavalue":{"value":{"text":"Digit Expansions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361319$098BC5EC-B53F-4202-9566-FC8091EEC2B4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cf0eb8ea916ed4b26f6bb67aa658b6bfd81822dc","datavalue":{"value":"We formalize how a natural number can be expanded into its digits in some base and prove properties about functions that operate on digit expansions. This includes the formalization of concepts such as digit shifts and carries. For a base that is a power of 2 we formalize the binary AND, binary orthogonality and binary masking of two natural numbers. This library on digit expansions builds the basis for the formalization of the DPRM theorem.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361319$87654703-CAD8-4C89-804E-C6EB97D0E285","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361319$4DB30006-3288-4E9B-AEB2-442782423EEC","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"51467ee0a503af56d0e1903e0514853bd73fc1a9","datavalue":{"value":{"entity-type":"item","numeric-id":7360830,"id":"Q7360830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361319$9EE60490-4962-422F-9065-FE4B33F6A173","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361319$F7C4DECB-0FEB-4596-A318-2BFDF50CE6C1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Digit Expansions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Digit_Expansions"}}}}}