{"entities":{"Q7361253":{"pageid":31519298,"ns":120,"title":"Item:Q7361253","lastrevid":105364376,"modified":"2026-10-07T13:35:19Z","type":"item","id":"Q7361253","labels":{"en":{"language":"en","value":"Without Loss of Generality"}},"descriptions":{"en":{"language":"en","value":"AFP entry Wlog"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c3a6d3331461647f7579f091a272358e705fe96b","datavalue":{"value":"https://isa-afp.org/entries/Wlog.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361253$D28BEC9E-915A-4E04-AF6E-E1AA3E7C0D34","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0c8fa6bb43b78c1909fabd4abecf9fb01f680f46","datavalue":{"value":{"time":"+2024-08-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361253$6E91714F-5BED-45E7-A19F-97F36B5B84DD","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"0f726647cf47955102e00c4d9747edb7ccbe5fa2","datavalue":{"value":"Dominique Unruh","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361253$E53A123C-6AF4-49F6-855E-233C4B40C258","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"57958dd55c62d33f38adb482754afe73ef72a56b","datavalue":{"value":{"text":"Without Loss of Generality","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361253$0DB97734-6B8A-4F79-B914-7C98A00C5C6B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c769cb29e9c693e95c59cb561865161c0e3e66d4","datavalue":{"value":"We introduce a new command wlog in Isabelle/HOL that allows us to (soundly) assume facts without loss of generality inside a proof.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361253$5B117278-003B-4676-B6EB-871165D6B818","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8e615433d7c0da849d212b92d36df1a27bb8523","datavalue":{"value":{"entity-type":"item","numeric-id":3183516,"id":"Q3183516"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361253$F6766C76-4720-4C8D-93F0-D3A39AAD612C","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":"Q7361253$81ADC90E-065B-4660-88A7-828AADF60BA2","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"924412e4302451de51094e930f82bf07674a31aa","datavalue":{"value":{"entity-type":"item","numeric-id":7361105,"id":"Q7361105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361253$3B823D75-9DA5-46C3-98AB-6C16812E1265","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"7a918ca57cbef7417c708001c9499e7e295238c0","datavalue":{"value":{"entity-type":"item","numeric-id":7360836,"id":"Q7360836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361253$4DF84629-12D3-42C2-9377-DCDA93603FE2","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":"Q7361253$ABB1C7BB-5F74-4114-9843-F2108FA0C434","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Without Loss of Generality (AFP entry Wlog)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Without_Loss_of_Generality_(AFP_entry_Wlog)"}}}}}