{"entities":{"Q1092042":{"pageid":1102794,"ns":120,"title":"Item:Q1092042","lastrevid":66936321,"modified":"2026-04-12T13:50:17Z","type":"item","id":"Q1092042","labels":{"en":{"language":"en","value":"Strong normalization for typed terms with surjective pairing"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4012603"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1092042$267E1D4D-D059-4E34-A6F4-1A773713A1F7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9728a0fc8227579d731c57e5aad25a6a2a5c1f99","datavalue":{"value":{"text":"Strong normalization for typed terms with surjective pairing","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1092042$53F760E3-EB6A-4360-88B2-2ECDF17A897B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3a502e53899367e1f9343778b2f1d4111c102949","datavalue":{"value":"0624.03043","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1092042$C9229095-099A-4B79-9C72-531ACB7374D2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fd7bcd31c089eea43fd8677a5426b0c7b8e7e1a7","datavalue":{"value":{"entity-type":"item","numeric-id":792318,"id":"Q792318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1092042$77366EF6-254F-45E4-B8BC-B147065140F0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6325d9f59cde8ebbdb24a9f950cab3fcef3decf6","datavalue":{"value":{"entity-type":"item","numeric-id":190248,"id":"Q190248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1092042$280D8FD8-1150-4080-AB11-6B8978310F00","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1092042$A39A2BF0-4247-4958-BF6F-B20BC266FDE0","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"78f9a5f835f25188d6b2aa5dd1f4cdbe508c6bea","datavalue":{"value":"A simple method is described for reducing strong normalization for typed terms with surjective pairing to strong normalization for typed terms not involving product types. In essence the proof uses the well-known reduction of intuitionistic propositional formulas in \\(\\to\\), \\(\\wedge\\) to finite sequences of implicational formulas. The method is described in detail for intuitionistic finite-type arithmetic with Cartesian product types, but applies equally well to a number of other systems, such as the arithmetical first-order fragment of Martin-L\u00f6f's theory of types. Corrections: \\(548^{21}\\) read \\(\\succcurlyeq t\\prime''\\); \\(549^ 7\\), add \\(6\\to \\tau \\equiv (\\sigma)\\tau\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1092042$A6151DFF-99BD-4AC9-BC81-70E53BDD07BD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1092042$3C71F3E3-DA02-406A-8178-3E74196739F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1092042$9A137FE8-1268-48B8-A8B5-A2ECAD0AEA9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1092042$7E01D1C7-06C7-4247-BBE8-52DE818E8245","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a047adb87c6cccac036bdfcb43edb10b26fe6096","datavalue":{"value":"4012603","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1092042$B675B9B6-0BDC-46F8-8002-F28F65A559B2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af462e56ed2ce88a42c8df0ec7f2dc6a55ded212","datavalue":{"value":"strong normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1092042$71ACC99D-5D2E-44C0-A59C-44A6026BDA36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cdf9cf23f216ede957f818348198c0a32d9932bd","datavalue":{"value":"typed terms","type":"string"},"datatype":"string"},"type":"statement","id":"Q1092042$C721C12D-8E4B-4239-851A-F1A86B64FDA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f139f485bfbc0efef3240275c23790ec4be3d041","datavalue":{"value":"surjective pairing","type":"string"},"datatype":"string"},"type":"statement","id":"Q1092042$5B1FEFEF-BFAC-4E7F-AD75-3475397DF02B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"579c90d9461ff747e07ae89b6add2f2600155a03","datavalue":{"value":"intuitionistic finite-type arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1092042$FF2F1916-8821-4CA0-83CB-41D099B93AAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3050ea31bad2fddd7147f36c4d2f04a58abb42bd","datavalue":{"value":"Cartesian product types","type":"string"},"datatype":"string"},"type":"statement","id":"Q1092042$E33C1207-9BB7-470F-B0C7-2B6D886D299B","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1092042$749BEDCB-F5EF-4342-843C-447428AC6FC3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d84cc3c2884888eca6e280fafe5755b863291d7e","datavalue":{"value":"https://doi.org/10.1305/ndjfl/1093636767","type":"string"},"datatype":"url"},"type":"statement","id":"Q1092042$A5C15D4B-37BF-4091-9AF4-869B21B4620C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fab506e830d86f48f5a4a729ec8a65a437ca9806","datavalue":{"value":"W1981838174","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1092042$5CB3B554-C931-4CE6-9B0F-EFEDAECD3656","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6448fde09c91f03375164b6b3341b3fbb4798ad8","datavalue":{"value":"10.1305/NDJFL/1093636767","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1092042$76FFC65F-47A0-4F6C-9C45-22BC09F88FAA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3aa62e1435f440213482d06153bf378239060015","datavalue":{"value":{"entity-type":"item","numeric-id":2958549,"id":"Q2958549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"55a14f0f7b59a67d0b1abe842326f2dfe9e97329","datavalue":{"value":{"amount":"+0.91825044","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1092042$C775C4B3-1112-48DA-86A6-6A4095254C14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c79724a902ef851155de58df4436c9dc71307a9e","datavalue":{"value":{"entity-type":"item","numeric-id":5149155,"id":"Q5149155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"503e8046924b8a85cd01d46a5672ea11a34fbd00","datavalue":{"value":{"amount":"+0.9054706","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1092042$DFDC122A-85D3-4020-95E2-AF7801C72631","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7deb4069a633156022e294596d3e1e23591d21f2","datavalue":{"value":{"entity-type":"item","numeric-id":4862765,"id":"Q4862765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dab9b2697a5ddea8b838140b248b85926c591e99","datavalue":{"value":{"amount":"+0.8986989","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1092042$BB8B8B75-D2ED-487D-9914-26411958148B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9e0fc5f0014bdd6c8e8417e372280fe791b4099","datavalue":{"value":{"entity-type":"item","numeric-id":1891251,"id":"Q1891251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5acc4555207b5af25648b1dfb25bed808eaf761e","datavalue":{"value":{"amount":"+0.89596975","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1092042$378607F8-87AE-4D8D-8054-5A14C2E60917","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a566b1d6a70d6aeb478a7fbe2b2db3c381d5fcb","datavalue":{"value":{"entity-type":"item","numeric-id":1924327,"id":"Q1924327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8739d6bf318d4325e36d224d35625fee8ca8aa0f","datavalue":{"value":{"amount":"+0.89288604","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1092042$A3D1159E-60F7-48B1-B712-66FD3FF11666","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b880e15382c3f4ed44af04a3258cd89112c976c9","datavalue":{"value":{"entity-type":"item","numeric-id":3612619,"id":"Q3612619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"77ab485b0a1f74fd03cc44653ed5561fa0a7e1f8","datavalue":{"value":{"amount":"+0.8894687","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1092042$ED50F093-D2DA-4397-9FDF-0AECDEB721BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"db2342ed2c626049bdf31040ee77033b181e8e71","datavalue":{"value":{"entity-type":"item","numeric-id":4457448,"id":"Q4457448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e6bb132dc20c2f742d4a28e62ec984352dd104d","datavalue":{"value":{"amount":"+0.88632256","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1092042$374EE130-0EB4-4655-A8A3-720D5CDCE5E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3731b13ffcfcd2791dd812dcf159bf727e2a0f06","datavalue":{"value":{"entity-type":"item","numeric-id":4501146,"id":"Q4501146"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71bd4223f9a10eb1025d6ca1d3c3e9e18a6b1ab5","datavalue":{"value":{"amount":"+0.8831049","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1092042$7EE8A965-8A46-4360-886A-F500DDA8065A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ebed28782f7de1c5df341ee5cee3d512cd956178","datavalue":{"value":{"entity-type":"item","numeric-id":1351999,"id":"Q1351999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"00f72db126a3674561b84db6f964487368c0491a","datavalue":{"value":{"amount":"+0.88259983","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1092042$98A98CC2-434A-44A5-9A8C-18239B9FC718","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"32ca232539b3919fae74a91eac485d7d5c56544e","datavalue":{"value":{"entity-type":"item","numeric-id":3520143,"id":"Q3520143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cead8308fa82cc341f92e74292d2b1996e6c7c88","datavalue":{"value":{"amount":"+0.8825829","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1092042$64A391D0-4BB7-451E-8FB2-5D57F48EA3DC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Strong normalization for typed terms with surjective pairing","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Strong_normalization_for_typed_terms_with_surjective_pairing"}}}}}