{"entities":{"Q40261":{"pageid":40317,"ns":120,"title":"Item:Q40261","lastrevid":105427745,"modified":"2026-10-09T10:08:16Z","type":"item","id":"Q40261","labels":{"en":{"language":"en","value":"Myhill-Nerode"}},"descriptions":{"en":{"language":"en","value":"AFP entry Myhill-Nerode"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"ccfe75415b3a6de34156e0264b2293d0752f360e","datavalue":{"value":"28547","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40261$BA87B868-DCCA-444A-9F6C-A35946C4F136","rank":"normal"}],"P286":[{"mainsnak":{"snaktype":"value","property":"P286","hash":"b269a519fe0dd604812862be3fe433f9f80dd07c","datavalue":{"value":{"entity-type":"item","numeric-id":2351151,"id":"Q2351151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$3377DBBA-BBC5-402B-860E-2C248DE85BE3","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":"Q40261$C0DADFC5-D433-4F45-B947-15C0B85EA849","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"0d7b4b4adebf91e7a2c78882871e1a34c4e80b2e","datavalue":{"value":"https://www.isa-afp.org/entries/Myhill-Nerode.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40261$49A1C406-0D74-47CB-BE48-24073AA66E26","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40261$1CEEF46B-CF80-440D-987D-1FED53E5669B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d379e93a1cc3ab3df2a5b8d85c84eb0620f6469c","datavalue":{"value":"06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40261$23627250-4119-4B16-A002-59DB5491B5D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40261$7B4ABAAF-61CC-40F1-9B76-33AB661B79AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40261$EE9BB174-3412-41F5-8F60-73D67CA6BEBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2becadfb03f0a4ea19120ee675d7cd2fe8450d8c","datavalue":{"value":"6.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40261$FCBCC6F0-5BA9-4269-AD9C-DFB9D40C3825","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40261$2F1B6A72-F07B-495F-9853-4A32424FBD7B","rank":"normal"}],"P1458":[{"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":"Q40261$2A00DD12-08A9-4110-BF24-E40C173665DA","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":"Q40261$72DD70E1-AF95-43FA-AC19-94BA190F3279","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ea53781dc0a29ca150a09c3de99800e897e49297","datavalue":{"value":{"entity-type":"item","numeric-id":40507,"id":"Q40507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$CC9EE7BC-36B5-49EA-BB46-2B0D4F4DCAE3","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":"Q40261$3342FF87-8C9A-41C5-AC4B-B6BDF65F7275","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"feba23e7c41ba4aa38bf2dee9205344029ea237a","datavalue":{"value":{"entity-type":"item","numeric-id":40317,"id":"Q40317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$1DB78422-21E7-4CAC-B545-F2B79E13E20E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"81319f5b8664d8398f69fd7004689cf3156bb740","datavalue":{"value":{"entity-type":"item","numeric-id":40964,"id":"Q40964"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$785CB894-BC36-415F-AF4C-75424615FFFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"87ec2ca742c9eb10fbaa98b1820ddb7f4298bb25","datavalue":{"value":{"entity-type":"item","numeric-id":40963,"id":"Q40963"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$5E87B919-A6ED-43F5-A81D-01AC85CE297D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b49b6cd0d730920a3a4cd5d33a24263cc6515903","datavalue":{"value":{"entity-type":"item","numeric-id":43940,"id":"Q43940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$619080AB-D98D-40F6-8B46-DC2A6A57A900","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ab576408136da65ce68abf8488b4c4362524857b","datavalue":{"value":{"entity-type":"item","numeric-id":43941,"id":"Q43941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$BF5BA601-13E3-46E5-AF41-08CCB1957687","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"c1161e1e8de5a1bc9eb8260f27cf5114412c2b8a","datavalue":{"value":{"entity-type":"item","numeric-id":21343,"id":"Q21343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$287A244E-EE99-40F1-8073-ADFB5B6E19C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"27b35591f9a1d87570b3e9ffb19e51ff7cd09a28","datavalue":{"value":{"entity-type":"item","numeric-id":40544,"id":"Q40544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$ECF62C48-BC83-4D3E-BDA9-23D0BC5BA966","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":"Q40261$A0DEE525-3FDC-42D5-B9F5-82F06E58B39D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"61d0c0612cc30c9c51b93ddaf1f78ee1ae75f9fe","datavalue":{"value":{"entity-type":"item","numeric-id":18676,"id":"Q18676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$AB86D4A2-89A8-4A55-B15F-65A52E686DEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"85d5a2bfb7e5cd7e1dfb166523d6500a685410a1","datavalue":{"value":{"entity-type":"item","numeric-id":13377,"id":"Q13377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$07B855B5-1399-4336-B3F1-BD180F65D104","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":"Q40261$9B20E357-1A02-4F6F-9806-8983A0B8B243","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$48C20254-1FB8-4908-87FD-96D8B69DAB0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"c9b16366127050be336d5a6c8997cdced7a9e9ab","datavalue":{"value":{"entity-type":"item","numeric-id":30365,"id":"Q30365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$1133AD09-0719-4576-9895-D7504EB7FFAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ef8d4fcb901e471e97f6d315665a098aedf96b01","datavalue":{"value":{"entity-type":"item","numeric-id":53718,"id":"Q53718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$9138E191-920B-4DB4-A2A5-4CB780308050","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"d3a62eaf34da81f5e92b727b678d5beeaeb06686","datavalue":{"value":{"entity-type":"item","numeric-id":41247,"id":"Q41247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$8A6FD254-0A8D-43E9-986E-2D2033E4123A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fd28f0c44657bf57d829bfa7b12f5ac4c90727f3","datavalue":{"value":"https://isa-afp.org/entries/Myhill-Nerode.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40261$31120215-A175-4644-8555-0A2B492F9288","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"d403d6ed65503aa1a789b2126ea170e86ea1915a","datavalue":{"value":"Chunhan Wu","type":"string"},"datatype":"string"},"type":"statement","id":"Q40261$0BF45029-B5F2-4432-923C-E1FE1B38499B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"4af20a7c401b51ea85da2061c04ae0d4a083ab9c","datavalue":{"value":"Xingyuan Zhang","type":"string"},"datatype":"string"},"type":"statement","id":"Q40261$8B892A69-E3B9-4083-AAC7-3EEE9609DFED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"7538833d135040c28ea592b4b5e0506b7d8dd0b4","datavalue":{"value":"Christian Urban","type":"string"},"datatype":"string"},"type":"statement","id":"Q40261$AA303C65-7BF8-46C2-9BF0-46936F80A5B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"85859c7ab42dcb8b36208f2902b7ce0d86423a6f","datavalue":{"value":"Manuel Eberl","type":"string"},"datatype":"string"},"type":"statement","id":"Q40261$8A684763-EE75-436A-9DD7-7813B2788CD6","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e730b4047d98d1f3522e5c555aab2431e316299e","datavalue":{"value":"There are many proofs of the Myhill-Nerode theorem using automata. In this library we give a proof entirely based on regular expressions, since regularity of languages can be conveniently defined using regular expressions (it is more painful in HOL to define regularity in terms of automata). We prove the first direction of the Myhill-Nerode theorem by solving equational systems that involve regular expressions. For the second direction we give two proofs: one using tagging-functions and another using partial derivatives. We also establish various closure properties of regular languages. Most details of the theories are described in our ITP 2011 paper.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40261$0FF40DC4-D161-4F5F-B808-3D0948CD71CD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad1627b0ef0dc706a0d145ad59d2ccb2cc61cb36","datavalue":{"value":{"entity-type":"item","numeric-id":672142,"id":"Q672142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$C1AFF4EC-1918-49D6-A385-13580A197EA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dce670ec1d34ee6c61f1437c968abe3b27423157","datavalue":{"value":{"entity-type":"item","numeric-id":3088018,"id":"Q3088018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$54F3B3E3-AA64-44FE-8DE9-317C07A2D600","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"bb0293970cb12cb0c0b06315232bb60667277b31","datavalue":{"value":{"entity-type":"item","numeric-id":7361362,"id":"Q7361362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$1F3DB0A3-678E-4731-892D-77C51DD0028C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"890c0c4a61156b4e729dc9fcff8e39e1971a8f5e","datavalue":{"value":{"entity-type":"item","numeric-id":7361686,"id":"Q7361686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$C4413D57-50AF-41A9-A6E1-5D4DE49FB5B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"a0e462408f240420e2b3f4dd5e025dcac9e4a9cd","datavalue":{"value":{"entity-type":"item","numeric-id":7361044,"id":"Q7361044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$DDC88D58-59F6-40AA-BE78-977749785D59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"96097fd8ad0239121f217726b3d18b7636f6739e","datavalue":{"value":{"entity-type":"item","numeric-id":7361640,"id":"Q7361640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$039D25B0-1414-4CB7-A642-E78349F52EEC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b8f347fb3b92d10259e32e7ae3b68d43ebb98729","datavalue":{"value":{"time":"+2011-08-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40261$CB6DEB42-8857-4C1B-B44C-88830EA57E16","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"74fe8b2f03bbf6285d7b803a894dfb94ab629e1e","datavalue":{"value":{"text":"The Myhill-Nerode Theorem Based on Regular Expressions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40261$324D39A5-A2B8-41F8-9028-9BEB964A6B09","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":"Q40261$B5BD4209-B5F8-4449-825A-2BE943A884B3","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"73d93a21b0749f7f2c51d7daeb11b162660cd756","datavalue":{"value":{"entity-type":"item","numeric-id":7360784,"id":"Q7360784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40261$BE082FC2-D45D-4459-BB0F-8D0441F18903","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Myhill-Nerode","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Myhill-Nerode"}}}}}