{"entities":{"Q2358702":{"pageid":2369445,"ns":120,"title":"Item:Q2358702","lastrevid":73997076,"modified":"2026-04-14T17:59:55Z","type":"item","id":"Q2358702","labels":{"en":{"language":"en","value":"Formal metatheory of the lambda calculus using Stoughton's substitution"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6731776"}},"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":"Q2358702$F0DB878F-23A2-48EA-B90D-5BBCE54E8BFB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5b57e1c2310327a2d3c8503e0950d873b86006ab","datavalue":{"value":{"text":"Formal metatheory of the lambda calculus using Stoughton's substitution","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2358702$89D99B08-A34D-4C52-8199-F06B35C45679","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5e4f3298d81ca835ca0df743fee1f8b36aa7bf8f","datavalue":{"value":"1383.03021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2358702$EFCA2867-489F-40B3-AD23-E97D79E1FD1C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ef5f2fcbe4affe3a081b63bc32cd9f9b1ef1904f","datavalue":{"value":{"entity-type":"item","numeric-id":530863,"id":"Q530863"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$2D625E28-8352-4FAB-8F74-DCB7286978AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"402a48fb715d415da55853e3651509e9510c9149","datavalue":{"value":{"entity-type":"item","numeric-id":220715,"id":"Q220715"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$CF769DBF-C753-49C5-B7A1-9CC54CF6FFE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"746409b166da6b3324f8a076651b3e33b41a949f","datavalue":{"value":{"entity-type":"item","numeric-id":530862,"id":"Q530862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$AEFC793D-9928-45FE-B7A9-20FE3E3D7D92","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$EDB265FB-A50D-44B8-898F-903FAC669FFF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"92d82bc79e45dbea4d44c115656eba4b7d7ac07a","datavalue":{"value":{"time":"+2017-06-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2358702$54F2B5E3-925B-419B-97E5-F027ED810071","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d583d597e7b3c2b34495199538eeb63851f1e674","datavalue":{"value":"When he formulated the lambda calculus \\textit{A. Church} [Ann. Math. (2) 33, 346--366 (1932; Zbl 0004.14507; JFM 58.0997.06)] left substitution, which is essential for \\(\\alpha\\)- and \\(\\beta\\)-reduction, undefined. \\textit{H. B. Curry} and \\textit{R. Feys} [Combinatory logic. Amsterdam: North-Holland Publishing Company (1958; Zbl 0081.24104)] did define this, but the substitution \\((\\lambda x.M)[y:=P]\\), in the case where \\(y\\) is free in \\(M\\) and \\(x\\) is free in \\(P\\), is complex. One way around, this is to have separate sorts of free and bound variables. The authors develop a new meta theory, for the \\(\\lambda\\)-calculus, in constructive type theory, where, as for Church and Curry, only one sort of names of variables is used. In order to overcome the complexity of substitution, they define, inductively, notions such as \\(x\\) is free in \\(M\\), \\(x\\) is fresh in \\(M\\) and a variant of the substitution first defined by \\textit{A. Stoughton} [Theor. Comput. Sci. 59, No. 3, 317--325 (1988; Zbl 0651.03008)]. New formulations of \\(\\alpha\\)- and \\(\\beta\\)-reduction are given. Importantly, the identification of \\(\\alpha\\)-equal terms is not needed. All the usual properties such as Church-Rosser and subject reduction are proved using detailed but elementary proofs. They have machine checked the whole development using the system Agda.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2358702$34141A70-3AC2-46E3-99B7-929A86B47DE9","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"376f136d3715d0668145bfef82b652dbeb24818d","datavalue":{"value":{"entity-type":"item","numeric-id":591019,"id":"Q591019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$086F3A2A-8C24-49B7-86BC-50E9B2C6C2CF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2358702$BE98D007-C069-4CD6-8775-28779433651F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2de267ce7071e755d603a1690a3f2c781f58931a","datavalue":{"value":"6731776","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2358702$582EE285-E0BE-45F6-ACF5-62E2341DCC50","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"34ae3a8d9f3401a083509ec6ab2b6f0f2deb2a29","datavalue":{"value":"formal metatheory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2358702$ED3F3EF8-0625-46E2-BDC2-C18249E414C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b876698d821b50cd7ba02ddb5424ed80f1905d8","datavalue":{"value":"lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2358702$7C49F40B-1FA6-424D-943E-9A39815E8F8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2358702$95DF47DE-28C1-4308-91F4-5114B6DFA7D8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d40b61763c81cd80c5c82e03c39b2fdb5cbb80a2","datavalue":{"value":{"entity-type":"item","numeric-id":23989,"id":"Q23989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$93C84E15-1633-4971-9DDB-EB28A80DE6B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$226A42E1-621D-408C-85B1-3188FA96A95A","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":"Q2358702$058C802A-59CC-4F8E-A25E-2A3C513C2789","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6df5b4cd73230ed3071900354eec4a11747d6390","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2016.08.025","type":"string"},"datatype":"url"},"type":"statement","id":"Q2358702$ECAADBFB-73B9-43A4-9843-F54C251DC3A9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"237dacf680d2924ec5abc38db4adc3852e012e0a","datavalue":{"value":"W2521607330","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2358702$73B50668-C96B-4662-B5F0-76642A197C70","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f3a7c1faf671a42f888a143ca6d231a4f3b4f0a","datavalue":{"value":{"entity-type":"item","numeric-id":2871861,"id":"Q2871861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$A407DE22-D013-4AAF-8244-36BD3F08EE4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c50237c8bde09d6668086722c62e1080ba158cf","datavalue":{"value":{"entity-type":"item","numeric-id":3189820,"id":"Q3189820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$2EA13491-19CF-4DC6-8B76-5BE3520B2DCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"787e8787fc0800d23d78fddfd9bf35254e758553","datavalue":{"value":{"entity-type":"item","numeric-id":801050,"id":"Q801050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$3F9438D6-A06C-4700-A1A7-9B7B9C556996","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fac7c6d05f114a4ae2738237ef25b8c9ead77ff","datavalue":{"value":{"entity-type":"item","numeric-id":1945914,"id":"Q1945914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$CE162191-ACDE-4002-A214-3473A8C001C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fcfdc5d6158991f32af2cf5057f70743de7ebb00","datavalue":{"value":{"entity-type":"item","numeric-id":1744410,"id":"Q1744410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$87CA15D7-6413-4C1D-B1E7-A27A3F070A30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27e31b151b8d22be2aa79bf2dfac73aa834ed045","datavalue":{"value":{"entity-type":"item","numeric-id":4012882,"id":"Q4012882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$730FABA1-5845-4063-8503-717A646C2AA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ccc272df6e3f638456d722d8f630056eceb056f","datavalue":{"value":{"entity-type":"item","numeric-id":5565113,"id":"Q5565113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$E7266B9D-C1BC-4A4B-9EE9-BBDDFD5CD499","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5dcacdf82491509f047ffa7adf630e71ade90","datavalue":{"value":{"entity-type":"item","numeric-id":5667469,"id":"Q5667469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$721D55F2-5A43-4A3E-976A-4B44E9C2D6D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4c1fc4571c1bcfa1a269c86e271e994d399bdd3","datavalue":{"value":{"entity-type":"item","numeric-id":5422334,"id":"Q5422334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$48FB9E4C-441A-45F9-8DE1-0EE0ACD239B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c89d163ec2cfe20cdcef09243a785a3cf35ab8f","datavalue":{"value":{"entity-type":"item","numeric-id":5573940,"id":"Q5573940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$73A3187F-B1AE-4106-9204-C36EBA3E7FE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e142ea160b3f096a8d7d9cd92f9c9ab65760eccf","datavalue":{"value":{"entity-type":"item","numeric-id":3011103,"id":"Q3011103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$99DB2297-F22C-42E0-9185-58A43DDE292D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"882e318ac9b6bbd79e82dcc1ce3fe340042f5778","datavalue":{"value":{"entity-type":"item","numeric-id":699761,"id":"Q699761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$6FA4AA27-1504-4E00-9B5E-1CB2062D1E02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff1c9576a9af1e44009a9ef9a0f7f22e091829d5","datavalue":{"value":{"entity-type":"item","numeric-id":5610986,"id":"Q5610986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$1E1A75F6-FBCA-4094-A9E5-9C566817667E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f23417d0146cdc8808662ea4f0b0496e878f3547","datavalue":{"value":{"entity-type":"item","numeric-id":4722037,"id":"Q4722037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$43B69939-D3E5-4DB1-9622-6A1F6D15D272","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$0E55AB80-B570-4952-8D77-9986C3DA8B12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"486b3db15310f7b4419a518b9731479317d56d77","datavalue":{"value":{"entity-type":"item","numeric-id":1961921,"id":"Q1961921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$E6E2C031-0ADA-4442-B445-7E38BA169A33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b8c3a63f5113f0209622b58f18640a08a06fa7","datavalue":{"value":{"entity-type":"item","numeric-id":1887151,"id":"Q1887151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$AD362576-071B-4E21-8ABA-32C8ACBC3815","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1851616a00610aaeabd4291b4d22573878184fd4","datavalue":{"value":{"entity-type":"item","numeric-id":3546313,"id":"Q3546313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$963D6DF0-5260-470A-9A89-C21F133D5F3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$40836734-594D-40DA-A128-C299D74E9FF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0e6d9e849bd790f8e9802155d975aaec967d07c","datavalue":{"value":{"entity-type":"item","numeric-id":4039770,"id":"Q4039770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$33D02FA0-02F9-4E1A-98C5-623EC21B2BEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5f149ec444851c81f8f28cc669b90ac06bcf6ea","datavalue":{"value":{"entity-type":"item","numeric-id":1106190,"id":"Q1106190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$78FA8A11-66AD-4B3C-A6DE-3C064B52709C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c382f571059f65c71d7c5267e06c23fa2d98eb72","datavalue":{"value":{"entity-type":"item","numeric-id":5917605,"id":"Q5917605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$1A4C8B5B-547F-4890-87F6-E24988A518E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46a6fdc5d1c9fc3a5278a9651165a74b6d670aa9","datavalue":{"value":{"entity-type":"item","numeric-id":530864,"id":"Q530864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$92A50081-1F4B-4F67-A8B9-E6ADF3C4EB8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4feea37c535bd22cbdd726fd39655db123c9a3f5","datavalue":{"value":{"entity-type":"item","numeric-id":928672,"id":"Q928672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$671CEE8D-5E78-421F-8BD1-E454DBB884B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9d1210df4ca2f7a9d1c0e50c280e46b223a4f48","datavalue":{"value":{"entity-type":"item","numeric-id":1401936,"id":"Q1401936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2358702$5578232C-732C-41DC-A204-97850957039C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4ab9a24f96308633f132df5d486d94c31ed35045","datavalue":{"value":"10.1016/J.TCS.2016.08.025","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2358702$00A0CCF5-076D-4C2A-B0A0-BCCE8CD4D4CC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"84552983a22f6f68b1aaacfe13c4e7ca7480ba50","datavalue":{"value":{"entity-type":"item","numeric-id":530864,"id":"Q530864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0dcb36445e1f281bddbfde97d2c357d444c25efd","datavalue":{"value":{"amount":"+0.9428966","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":"Q2358702$F11ADB1C-0412-47DB-8EA2-7737C51B3DE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b361ca1aa5526764549f3d95137afb2aca29dcf6","datavalue":{"value":{"entity-type":"item","numeric-id":6061881,"id":"Q6061881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea86b525db5dd89dcfab60fd2d49ef710ce1a3bf","datavalue":{"value":{"amount":"+0.89998686","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":"Q2358702$0A6FEB39-B48F-4636-B66B-5547DD0AF641","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0234589f2ebd950feb0efa0de76dafdbbee659d1","datavalue":{"value":{"entity-type":"item","numeric-id":4506397,"id":"Q4506397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae94abc71537e747e465bdc91482fe701fc26c4e","datavalue":{"value":{"amount":"+0.8969375","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":"Q2358702$EFF050A9-7299-47E8-8BCC-23834AB62018","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"834ee936acd9e48cc35c692020e0f19867471065","datavalue":{"value":{"entity-type":"item","numeric-id":5022932,"id":"Q5022932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"76e8387118bfab7e4151fb59e52b3232c418decd","datavalue":{"value":{"amount":"+0.89408314","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":"Q2358702$4AB44CF7-B398-4F7A-A7CD-8B36A8DC5183","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"42797fc209eaaddb74c3306a25952bf259efdce8","datavalue":{"value":{"entity-type":"item","numeric-id":1850959,"id":"Q1850959"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f687621b9f48d13ee5067ab57615d286f7fb2a58","datavalue":{"value":{"amount":"+0.89305294","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":"Q2358702$97E69F08-BC97-4C05-933C-4CCEC5FF8B17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"37922e77ad3c1ec200f259057289706cbb3dd3b0","datavalue":{"value":{"entity-type":"item","numeric-id":1744443,"id":"Q1744443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e597cb15528439391b48abad09f068e74d8a1b6","datavalue":{"value":{"amount":"+0.879949","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":"Q2358702$933BD5DD-BDC7-41D2-B869-A769D9654C5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae33ec0cec722ae39db812bfd7fd70874e418f99","datavalue":{"value":{"entity-type":"item","numeric-id":2713357,"id":"Q2713357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"271c2eb1785ee76676b44a3a886b3da199b6347a","datavalue":{"value":{"amount":"+0.8720609","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":"Q2358702$E8436F47-C3DE-476E-A86C-A7454E412F44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2c3b51f8a0d80d67354e45b2e72b0c69c6d1b718","datavalue":{"value":{"entity-type":"item","numeric-id":2871868,"id":"Q2871868"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c28ada2ae4eac729b80ca27f90117c536d7596f4","datavalue":{"value":{"amount":"+0.8705524","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":"Q2358702$BCABF009-5849-47BD-B737-20FCB64E0534","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"71d114b68c8bdca87f93fe5ac469a6d3a03827b2","datavalue":{"value":{"entity-type":"item","numeric-id":687575,"id":"Q687575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a51f23c3abc1f85e484c4933e5cf4575acb4c75b","datavalue":{"value":{"amount":"+0.86998546","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":"Q2358702$E749EA52-D08C-48FF-B0C7-9D10F10A07A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4710ab823047963dca88071ab76a8a2caaf6530","datavalue":{"value":{"entity-type":"item","numeric-id":3553919,"id":"Q3553919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82c5671a2daa7ec8019b4748a6876c348525595c","datavalue":{"value":{"amount":"+0.86993235","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":"Q2358702$9B7ADD99-406A-4067-BF83-B189DC039FD3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal metatheory of the lambda calculus using Stoughton's substitution","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formal_metatheory_of_the_lambda_calculus_using_Stoughton%27s_substitution"}}}}}