{"entities":{"Q7361305":{"pageid":31519454,"ns":120,"title":"Item:Q7361305","lastrevid":105364829,"modified":"2026-10-07T13:35:30Z","type":"item","id":"Q7361305","labels":{"en":{"language":"en","value":"Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals"}},"descriptions":{"en":{"language":"en","value":"AFP entry Nested_Multisets_Ordinals"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"475109c801697cee75d9c5744498a582639b6a55","datavalue":{"value":"https://isa-afp.org/entries/Nested_Multisets_Ordinals.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361305$92DDDD95-7C94-40C2-835E-4FF5B8767B65","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"41ff541fd86139b491ded56d8988e9c4cc3f5963","datavalue":{"value":{"time":"+2016-11-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361305$1C3648CF-6C1F-42DA-8BDE-CAF3D43C03D8","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"d593b6f197721b1ecf9f17d8e5bbb2bb5a1f7f8a","datavalue":{"value":"Jasmin Christian Blanchette","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361305$836BC234-FA2C-4D6A-A7F5-44DB4940101F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"945ab20dca3d165b4fc3dec98847d7b03a5dc77f","datavalue":{"value":"Mathias Fleury","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361305$58F9CD5F-DAD4-43B6-9B00-91C027325FF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2500aa80beaafa12dfa4ab6c7d8363674f762e6e","datavalue":{"value":"Dmitriy Traytel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361305$12A8B02C-2A39-45EA-9766-32426B1D7248","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"23ab623d440193756bc6a344c150accd134c92b8","datavalue":{"value":{"text":"Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361305$D6161C7D-D434-46B0-B13D-D70FC32AD41C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b3a75f42796b836b8d1963dc73b195050863b746","datavalue":{"value":"This Isabelle/HOL formalization introduces a nested multiset datatype and defines Dershowitz and Manna's nested multiset order. The order is proved well founded and linear. By removing one constructor, we transform the nested multisets into hereditary multisets. These are isomorphic to the syntactic ordinals\u2014the ordinals can be recursively expressed in Cantor normal form. Addition, subtraction, multiplication, and linear orders are provided on this type.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361305$3D050678-A046-4182-8178-ED06180EE57E","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":"Q7361305$D64A0D26-08EE-4C46-9C25-74F24612BFCF","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"e0b5465b6a0d9e05645cdb7168eee1aaf7eb2845","datavalue":{"value":{"entity-type":"item","numeric-id":7361518,"id":"Q7361518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361305$0DA8144B-011D-4245-83A8-A06E494ED572","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"9ae3577cc4d9f593cc896ccbab507cab0b1231f2","datavalue":{"value":{"entity-type":"item","numeric-id":7361485,"id":"Q7361485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361305$0D2A0616-C7FC-4AE8-AD0B-07C766500F79","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"edf8a8949edec3767dd80b6d3acecc92e5d25f1c","datavalue":{"value":{"entity-type":"item","numeric-id":7360818,"id":"Q7360818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361305$06748365-CF2C-4675-A644-EC54D92327E9","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":"Q7361305$F882938C-86D2-4A32-AE89-36346224D481","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_Nested_Multisets,_Hereditary_Multisets,_and_Syntactic_Ordinals"}}}}}