vout |
---|
PrCit../cabea.. 5.60 bars TMbXT../f820e.. ownership of 9303b.. as prop with payaddr Pr4zB.. rightscost 800.00 controlledby Pr4zB.. upto 0 TMX8c../1df49.. ownership of 214df.. as prop with payaddr Pr4zB.. rightscost 800.00 controlledby Pr4zB.. upto 0 TMYoN../3fd79.. ownership of f60cd.. as prop with payaddr Pr4zB.. rightscost 800.00 controlledby Pr4zB.. upto 0 TMQWr../8ed45.. ownership of 181a8.. as prop with payaddr Pr4zB.. rightscost 800.00 controlledby Pr4zB.. upto 0 TMJ68../91e84.. ownership of e1672.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKS2../8a8ca.. ownership of 39d5d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMEyu../fbb37.. ownership of a5ec6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMWrb../682a7.. ownership of 83a1c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMUbH../7f7d6.. ownership of eed30.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMJJJ../9b583.. ownership of 4bce7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMPv5../eddef.. ownership of dac10.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMSHW../1e263.. ownership of 0eb34.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMYj9../31aa7.. ownership of eaaf4.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMWfF../b634c.. ownership of 7755d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMVy5../8739d.. ownership of c5de4.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMZ7Y../30137.. ownership of b8674.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMPE5../a7a1a.. ownership of 4ac5f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMMdK../ed52a.. ownership of 5ffaa.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMRqr../eb193.. ownership of e57bb.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMRjs../41661.. ownership of 315e2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMJRs../205f6.. ownership of 8922d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMNme../a141a.. ownership of 15211.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMGFk../d011a.. ownership of b1cc9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMUHJ../dcb0e.. ownership of 9d142.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMRtt../9a089.. ownership of 49e33.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMauJ../8bd36.. ownership of eed6a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQ4R../da551.. ownership of 28253.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKdk../e40b9.. ownership of f6f49.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKbn../c1e8f.. ownership of 53c9b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMLzR../4f42e.. ownership of 0cc15.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKHN../93810.. ownership of b782a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMcQS../fc59d.. ownership of 33e1c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMWeZ../6f878.. ownership of dfbcd.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMHX7../b34cb.. ownership of 20b77.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMS5J../4da60.. ownership of fa851.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMatR../3f6c0.. ownership of 2368c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMT7Q../15ec0.. ownership of a48ad.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMFET../4b661.. ownership of b5b7f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMGKw../f95f8.. ownership of ad374.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQaW../5d432.. ownership of 4c6be.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMWuZ../25a84.. ownership of 92519.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQrm../e9447.. ownership of 5fdff.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMVV1../45be2.. ownership of 0e9d3.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMPMT../606ef.. ownership of 36f23.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQd7../c4cc2.. ownership of c2824.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMRa6../dc829.. ownership of 3e50d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMHB5../808a0.. ownership of f8e90.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMHQj../b42bf.. ownership of 5a0d8.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMMww../a8389.. ownership of 6c736.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKmd../16532.. ownership of 97ae9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMTLV../b5b4a.. ownership of a776d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMa1e../b853c.. ownership of 5cf36.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMXFq../d5a80.. ownership of b68fb.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMcdN../aac2c.. ownership of 5c21f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMJ8m../e78cf.. ownership of f7f04.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQXx../c1fd7.. ownership of 41519.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TML17../792c2.. ownership of 1d5ae.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKpS../02f5d.. ownership of e6b7d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMGPd../85c74.. ownership of 0bfaf.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMJoN../ed14d.. ownership of 00381.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMNao../032eb.. ownership of 1aa1c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKWY../1136c.. ownership of 41071.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMJa5../2136c.. ownership of 2f553.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMS72../ed7e7.. ownership of 0d5b6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMFZf../6e874.. ownership of 7b754.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMPvS../eb1ce.. ownership of ba84a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMJL6../57992.. ownership of 24233.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQxk../dc2f1.. ownership of 2eb24.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMTQC../5dad1.. ownership of ec90a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMMfg../89ac7.. ownership of d2576.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMLda../9f923.. ownership of 16e4b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMM2H../8a92f.. ownership of 55d10.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQ8p../c14ef.. ownership of b0f0d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMUm7../4ae6a.. ownership of 4a2d5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMT9C../2f7eb.. ownership of d5994.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMYiC../22c93.. ownership of b1666.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMYXX../0e0be.. ownership of 081ec.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMPgf../96229.. ownership of 5881c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMPqs../246c6.. ownership of 7734d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMMQo../2d957.. ownership of 30cfc.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMYAB../bb07e.. ownership of 94187.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMPhM../e8792.. ownership of ec185.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMTq4../1c4bf.. ownership of 0ab9f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMXgz../bba26.. ownership of f0037.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKFM../136f0.. ownership of 3a83b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQg2../78397.. ownership of 77373.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMX9Z../76e4a.. ownership of 446d8.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKPC../f34e4.. ownership of a820e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMNv6../a81a9.. ownership of e5caa.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMXUv../ecefe.. ownership of d79e0.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMTAj../41edf.. ownership of ef1ab.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMT5r../61838.. ownership of f798c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMcjp../a615e.. ownership of 208f3.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMdPS../fc77d.. ownership of c81ed.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMTun../a6a36.. ownership of a5963.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMd3a../ea8a9.. ownership of f3fbe.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMTTu../c8cb3.. ownership of 18961.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMEht../788a4.. ownership of e6edc.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMNuW../58f47.. ownership of cef55.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMbHy../fa849.. ownership of b3205.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMb5q../5bad0.. ownership of 06461.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMN2k../d1827.. ownership of 805e6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMLwd../effd1.. ownership of abce4.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMRXm../0533a.. ownership of 650aa.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMJ2J../431d1.. ownership of 44285.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKzH../9bd28.. ownership of db37d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQrR../5c8fd.. ownership of 5a925.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMTp6../fc6ae.. ownership of 24a49.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMUHL../5dd4e.. ownership of d720a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMFVf../5554e.. ownership of 566a7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMW7W../71099.. ownership of 13c67.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMaJy../15d94.. ownership of 4e1ed.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMPH1../bd72c.. ownership of accc4.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMNEN../154dc.. ownership of fed3b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMLzp../27d46.. ownership of f6916.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMH65../4e8b1.. ownership of 489a1.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMbgn../84e6c.. ownership of 4cf1f.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMMoq../6f40b.. ownership of da520.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMJGZ../652bb.. ownership of 0b7fa.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMHAr../6ad49.. ownership of f1578.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKaM../f45c5.. ownership of 34e5c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQrT../78fbc.. ownership of a77ae.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMFQu../0a49f.. ownership of 64050.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMb48../29b42.. ownership of 7456b.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMb4A../7a43e.. ownership of c1186.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMFRL../057a4.. ownership of e4c40.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMUgP../23fa2.. ownership of 00ab7.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKLe../8eff7.. ownership of 448f5.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMa2o../ec710.. ownership of b8a3f.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMLR5../b00ee.. ownership of 89516.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMWj8../2c1f9.. ownership of f5fd5.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQLy../f88c8.. ownership of d2032.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMVS6../7ce1d.. ownership of c4d65.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMbJt../3485d.. ownership of d9df1.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMdin../5e6e0.. ownership of 8b623.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMNrP../7c590.. ownership of b555d.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMFL7../10246.. ownership of 59ee9.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMaup../5c97e.. ownership of ab347.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMSzb../b29ac.. ownership of 88da4.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQLf../ec279.. ownership of 344c0.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMG21../4784a.. ownership of 4c1cc.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMJ2F../dca76.. ownership of 953e3.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMZTX../16f33.. ownership of fe555.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMV7E../52f85.. ownership of 8df59.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMGEa../ade53.. ownership of 559a7.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMHhT../7b747.. ownership of 21043.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMNcd../2f534.. ownership of 31e8a.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMVs9../d100b.. ownership of fc696.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMcf6../b12e8.. ownership of bc88c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMTJt../c85d4.. ownership of 1b998.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMdt7../ed43c.. ownership of 373cc.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMd7V../b4d4d.. ownership of 6d417.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMb1Y../c4cca.. ownership of 7c377.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMQGJ../80855.. ownership of 72438.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMWXd../81c39.. ownership of 4a7c5.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMP3o../6080a.. ownership of 5393b.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMPA5../bbb57.. ownership of 04776.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMcZ2../aedc3.. ownership of c5e2a.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMKf3../70d95.. ownership of fd7f7.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMYQ6../51743.. ownership of 4ddf9.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMNPw../fdc79.. ownership of 69d89.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMGWw../34e15.. ownership of 5723e.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMLD4../dad39.. ownership of e2e24.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMc3L../e5fa3.. ownership of 47187.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMXDN../addb0.. ownership of 3c773.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMVvJ../0b198.. ownership of 23993.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMNaF../98b08.. ownership of a47d7.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMN6y../a477c.. ownership of 2976e.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMZY4../754c9.. ownership of 70a2b.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 TMPPr../d3949.. ownership of 12a33.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0 PUVpr../41b00.. doc published by Pr4zB..Param andand : ο → ο → οDefinition ChurchNums_3x8_eq := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . and (x0 = x2) (x1 = x3)Param notnot : ο → οDefinition ChurchNums_3x8_neq := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . not (ChurchNums_3x8_eq x0 x1 x2 x3)Known andIandI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1Theorem f6916.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x0 = x1 ⟶ x2 = x3 ⟶ ChurchNums_3x8_eq x0 x2 x1 x3...
Definition ChurchNums_8_perm_1_2_3_4_5_6_7_0 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x0 x2 x3 x4 x5 x6 x7 x8 x1Definition ChurchNums_8_perm_2_3_4_5_6_7_0_1 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x0 x3 x4 x5 x6 x7 x8 x1 x2Definition ChurchNums_8_perm_3_4_5_6_7_0_1_2 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x0 x4 x5 x6 x7 x8 x1 x2 x3Definition ChurchNums_8_perm_4_5_6_7_0_1_2_3 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x0 x5 x6 x7 x8 x1 x2 x3 x4Definition ChurchNums_8_perm_5_6_7_0_1_2_3_4 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x0 x6 x7 x8 x1 x2 x3 x4 x5Definition ChurchNums_8_perm_6_7_0_1_2_3_4_5 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x0 x7 x8 x1 x2 x3 x4 x5 x6Definition ChurchNums_8_perm_7_0_1_2_3_4_5_6 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x0 x8 x1 x2 x3 x4 x5 x6 x7Theorem accc4.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8_perm_1_2_3_4_5_6_7_0 (ChurchNums_8_perm_7_0_1_2_3_4_5_6 x0) = x0...
Theorem 13c67.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8_perm_2_3_4_5_6_7_0_1 (ChurchNums_8_perm_6_7_0_1_2_3_4_5 x0) = x0...
Theorem d720a.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8_perm_3_4_5_6_7_0_1_2 (ChurchNums_8_perm_5_6_7_0_1_2_3_4 x0) = x0...
Theorem 5a925.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8_perm_4_5_6_7_0_1_2_3 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x0) = x0...
Theorem 44285.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8_perm_5_6_7_0_1_2_3_4 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x0) = x0...
Theorem abce4.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8_perm_6_7_0_1_2_3_4_5 (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x0) = x0...
Theorem 06461.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8_perm_7_0_1_2_3_4_5_6 (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x0) = x0...
Definition ChurchNums_8x3_lt1_id_ge1_rot2 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2)Definition ChurchNums_8x3_lt2_id_ge2_rot2 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2)Definition ChurchNums_8x3_to_3_lt3_id_ge3_rot2 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2)Definition ChurchNums_8x3_to_3_lt4_id_ge4_rot2 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2)Definition ChurchNums_8x3_to_3_lt5_id_ge5_rot2 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2) (x1 x3 x4 x2)Definition ChurchNums_8x3_to_3_lt6_id_ge6_rot2 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2) (x1 x3 x4 x2)Definition ChurchNums_8x3_to_3_lt7_id_ge7_rot2 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x3 x4 x2)Definition ChurchNums_8x3_lt1_id_ge1_rot1 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3)Definition ChurchNums_8x3_lt2_id_ge2_rot1 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3)Definition ChurchNums_8x3_lt3_id_ge3_rot1 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3)Definition ChurchNums_8x3_lt4_id_ge4_rot1 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3)Definition ChurchNums_8x3_lt5_id_ge5_rot1 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3) (x1 x4 x2 x3)Definition ChurchNums_8x3_lt6_id_ge6_rot1 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3) (x1 x4 x2 x3)Definition ChurchNums_8x3_lt7_id_ge7_rot1 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 : (ι → ι) → ι → ι . x0 (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x2 x3 x4) (x1 x4 x2 x3)Definition ChurchNum_3ary_proj_p := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι) → ο . x1 (λ x2 x3 x4 : (ι → ι) → ι → ι . x2) ⟶ x1 (λ x2 x3 x4 : (ι → ι) → ι → ι . x3) ⟶ x1 (λ x2 x3 x4 : (ι → ι) → ι → ι . x4) ⟶ x1 x0Definition ChurchNum_8ary_proj_p := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x9) ⟶ x1 x0Theorem cef55.. : ChurchNum_3ary_proj_p (λ x0 x1 x2 : (ι → ι) → ι → ι . x0)...
Theorem 18961.. : ChurchNum_3ary_proj_p (λ x0 x1 x2 : (ι → ι) → ι → ι . x1)...
Theorem a5963.. : ChurchNum_3ary_proj_p (λ x0 x1 x2 : (ι → ι) → ι → ι . x2)...
Theorem 208f3.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x0)...
Theorem ef1ab.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x1)...
Theorem e5caa.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x2)...
Theorem 446d8.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x3)...
Theorem 3a83b.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x4)...
Theorem 0ab9f.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x5)...
Theorem 94187.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x6)...
Theorem 7734d.. : ChurchNum_8ary_proj_p (λ x0 x1 x2 x3 x4 x5 x6 x7 : (ι → ι) → ι → ι . x7)...
Theorem 081ec.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p (λ x1 x2 x3 : (ι → ι) → ι → ι . x0 x2 x3 x1)...
Theorem d5994.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p (λ x1 x2 x3 : (ι → ι) → ι → ι . x0 x3 x1 x2)...
Theorem b0f0d.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_lt1_id_ge1_rot2 x0 x1)...
Theorem 16e4b.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_lt2_id_ge2_rot2 x0 x1)...
Theorem ec90a.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 x0 x1)...
Theorem 24233.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x0 x1)...
Theorem 7b754.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x0 x1)...
Theorem 2f553.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x0 x1)...
Theorem 1aa1c.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x0 x1)...
Theorem 0bfaf.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_lt1_id_ge1_rot1 x0 x1)...
Theorem 1d5ae.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_lt2_id_ge2_rot1 x0 x1)...
Theorem f7f04.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_lt3_id_ge3_rot1 x0 x1)...
Theorem b68fb.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_lt4_id_ge4_rot1 x0 x1)...
Theorem a776d.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_lt5_id_ge5_rot1 x0 x1)...
Theorem 6c736.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_lt6_id_ge6_rot1 x0 x1)...
Theorem f8e90.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_lt7_id_ge7_rot1 x0 x1)...
Theorem c2824.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_lt1_id_ge1_rot2 x0 (ChurchNums_8x3_lt1_id_ge1_rot1 x0 x1) = x1...
Theorem 0e9d3.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_lt2_id_ge2_rot2 x0 (ChurchNums_8x3_lt2_id_ge2_rot1 x0 x1) = x1...
Theorem 92519.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt3_id_ge3_rot2 x0 (ChurchNums_8x3_lt3_id_ge3_rot1 x0 x1) = x1...
Theorem ad374.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x0 (ChurchNums_8x3_lt4_id_ge4_rot1 x0 x1) = x1...
Theorem a48ad.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x0 (ChurchNums_8x3_lt5_id_ge5_rot1 x0 x1) = x1...
Theorem fa851.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x0 (ChurchNums_8x3_lt6_id_ge6_rot1 x0 x1) = x1...
Theorem dfbcd.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x0 (ChurchNums_8x3_lt7_id_ge7_rot1 x0 x1) = x1...
Theorem b782a.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_lt1_id_ge1_rot1 x0 (ChurchNums_8x3_lt1_id_ge1_rot2 x0 x1) = x1...
Theorem 53c9b.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_lt2_id_ge2_rot1 x0 (ChurchNums_8x3_lt2_id_ge2_rot2 x0 x1) = x1...
Theorem 28253.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_lt3_id_ge3_rot1 x0 (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 x0 x1) = x1...
Theorem 49e33.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_lt4_id_ge4_rot1 x0 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x0 x1) = x1...
Theorem b1cc9.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_lt5_id_ge5_rot1 x0 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x0 x1) = x1...
Theorem 8922d.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_lt6_id_ge6_rot1 x0 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x0 x1) = x1...
Theorem e57bb.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ∀ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_lt7_id_ge7_rot1 x0 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x0 x1) = x1...
Theorem 4ac5f.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x0)...
Theorem c5de4.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x0)...
Theorem eaaf4.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x0)...
Theorem dac10.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x0)...
Theorem eed30.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_5_6_7_0_1_2_3_4 x0)...
Theorem a5ec6.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_6_7_0_1_2_3_4_5 x0)...
Theorem e1672.. : ∀ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p (ChurchNums_8_perm_7_0_1_2_3_4_5_6 x0)...
Definition TwoRamseyGraph_4_5_24_ChurchNums_3x8 := λ x0 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x4 . x0 (x1 (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)))) (x1 (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)))) (x1 (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6))) (x2 (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5))) (x2 (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)) (x3 (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . x5)))) (λ x5 . x4)Theorem f60cd.. : ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_8ary_proj_p x3 ⟶ TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x3 x0 x2...
Param ordsuccordsucc : ι → ιDefinition TwoRamseyGraph_4_5_24 := λ x0 x1 . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x3 ⟶ ChurchNum_8ary_proj_p x4 ⟶ ChurchNum_8ary_proj_p x5 ⟶ x0 = x2 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))))))))))) ordsucc (x4 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . x7) (λ x7 : ι → ι . λ x8 . x7 (x7 x8)) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 x8))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 x8)))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 x8))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 x8)))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 x8))))))) ordsucc 0) ⟶ x1 = x3 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))))))))))) ordsucc (x5 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . x7) (λ x7 : ι → ι . λ x8 . x7 (x7 x8)) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 x8))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 x8)))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 x8))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 x8)))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 x8))))))) ordsucc 0) ⟶ TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x4 x3 x5 = λ x7 x8 . x7Theorem 9303b.. : ∀ x0 x1 . TwoRamseyGraph_4_5_24 x0 x1 ⟶ TwoRamseyGraph_4_5_24 x1 x0...
|
|