{"entities":{"Q51731":{"pageid":51787,"ns":120,"title":"Item:Q51731","lastrevid":105426686,"modified":"2026-10-09T10:05:58Z","type":"item","id":"Q51731","labels":{"en":{"language":"en","value":"Nominal2"}},"descriptions":{"en":{"language":"en","value":"AFP entry Nominal2"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"99c274298dbe2cc34d37ec192d5c96b89abedb99","datavalue":{"value":"36029","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q51731$75D5AB79-24F8-4026-9BC7-2888942C63CD","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":"Q51731$AA493A1F-6E24-4298-B77D-3E168A99BA35","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"bfbabf10749dcfc64bbb6d6e054252f42368cf15","datavalue":{"value":"https://www.isa-afp.org/entries/Nominal2.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q51731$7B7D8442-8787-4D10-BC45-A9E3FE6D2961","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q51731$6E066398-6B5F-46E3-B1CA-FD24676D11FB","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"47548059e3416b4b47c737ba6e24ccdeda7d9657","datavalue":{"value":{"entity-type":"item","numeric-id":40548,"id":"Q40548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51731$1B3A9E80-C878-4359-A2AE-7698BC229211","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51731$A01679FD-C299-4B1D-AE3C-A10779836F9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51731$7D0ABC41-811C-4447-AFCE-7539EF30B829","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"20f9bbd727bc5cdb284bf24bdb16fda7e6410101","datavalue":{"value":{"entity-type":"item","numeric-id":51730,"id":"Q51730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51731$21592C25-EC6E-43E7-9E4C-908A10CACD3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4a5d7cc7c93c22bf9c8fa550419d7f2b201a4c87","datavalue":{"value":{"entity-type":"item","numeric-id":31827,"id":"Q31827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51731$EB1B80AF-D883-49A6-9A49-FE2DDFB3B00F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7343f563fd02ee3f7d39ccb038f5c1c6c726769a","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51731$83A167AF-7BC6-4AAB-A88B-09C7313E55AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51731$F73DA0EE-CDD3-4ED9-AB1C-45D48FF620DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51731$6F7A14E0-0807-4D93-84DD-5540714D80B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51731$6B5D12A2-8503-48BD-9822-3B8D2E9EB878","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"139c69b2a23f419923a7989e28183ef8179b6836","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51731$32654B36-CA46-4193-B42B-94A1E0B37AF2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"504cbbf3ad90cbc75a76258e0e07eba664f8cfdc","datavalue":{"value":"https://isa-afp.org/entries/Nominal2.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q51731$E41D8F46-1228-446E-AD7A-F364E1D8618F","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7538833d135040c28ea592b4b5e0506b7d8dd0b4","datavalue":{"value":"Christian Urban","type":"string"},"datatype":"string"},"type":"statement","id":"Q51731$33E1859D-7FCA-42D6-B0BD-25ACA5BAEDDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"42cc17b6ebd1e6b2e2779d5c2e7eb07525a54975","datavalue":{"value":"Stefan Berghofer","type":"string"},"datatype":"string"},"type":"statement","id":"Q51731$9CEFDBEC-FF77-43F5-AF16-D87F4C253A64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"24ecedfcd986881afa2237d024b26ac8d56865f3","datavalue":{"value":"Cezary Kaliszyk","type":"string"},"datatype":"string"},"type":"statement","id":"Q51731$2B6B3F8F-258F-49EA-B4C7-77059C20BA32","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a76684a4c743ec184eece599fd9ca9e969841515","datavalue":{"value":"Dealing with binders, renaming of bound variables, capture-avoiding substitution, etc., is very often a major problem in formal proofs, especially in proofs by structural and rule induction. Nominal Isabelle is designed to make such proofs easy to formalise: it provides an infrastructure for declaring nominal datatypes (that is alpha-equivalence classes) and for defining functions over them by structural recursion. It also provides induction principles that have Barendregt\u2019s variable convention already built in. This entry can be used as a more advanced replacement for HOL/Nominal in the Isabelle distribution.","type":"string"},"datatype":"string"},"type":"statement","id":"Q51731$4D5E3506-DEF8-44B9-814C-023344619E7E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4ec88787b088b88fbcbfef6eb4534917e7df1ffe","datavalue":{"value":{"time":"+2013-02-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q51731$C5F6E8CD-B7CA-4FE1-B60B-212D5E8A0702","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b01acc03bb891c0600546d4a9154769346587c80","datavalue":{"value":{"text":"Nominal 2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q51731$22F4A569-8903-4E92-8866-A7B1A69E3023","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":"Q51731$48BFBE39-1592-47E8-9452-4D248BF7FA53","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"c6381c3139ee5dae1881d28867a7925513419337","datavalue":{"value":{"entity-type":"item","numeric-id":7361667,"id":"Q7361667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51731$67A98882-6158-4D16-834D-3B7BB3AD9D5B","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":"Q51731$91A8FF0F-04BC-45E7-ABB0-DB21FEF816EF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Nominal2","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Nominal2"}}}}}