Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrJGW../ef99f..
PUgU2../46113..
vout
PrJGW../c150f.. 1.99 bars
TMMeG../a3464.. ownership of 505b1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR4a../dd8ea.. ownership of 91554.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYCt../c006a.. ownership of aac29.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHJD../d3865.. ownership of d72a2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZB2../4f8b5.. ownership of 65146.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMDh../3db2a.. ownership of d3ec5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb7A../4afd3.. ownership of daa3d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJri../31a53.. ownership of 03f37.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbZY../0e0da.. ownership of 4f606.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZqf../f89d5.. ownership of 74cdd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXJi../1699d.. ownership of dee3e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRkF../1b136.. ownership of 429d2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU91../6b939.. ownership of 43682.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaYv../5c8be.. ownership of 5845b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc3R../a1408.. ownership of 476c5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK6i../25cea.. ownership of 6211e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSob../d82ed.. ownership of 6543a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVJd../30e35.. ownership of db0ab.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQhK../d251a.. ownership of ee03a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFby../df0bc.. ownership of f3d4c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS6A../58932.. ownership of a3364.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdac../0833d.. ownership of 0bc3c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTh1../adc9a.. ownership of ab95a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMkQ../150ef.. ownership of 316df.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVqf../fe7a5.. ownership of 7e03f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFiG../36aec.. ownership of 4618e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc2W../c3518.. ownership of b02dd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcYB../92a0a.. ownership of 55bdd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWhi../5b1b7.. ownership of 0ad46.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbTe../a999e.. ownership of 1b7d3.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML9a../f0505.. ownership of 9aa0b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdXY../47175.. ownership of b2a04.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJf9../85713.. ownership of 0ec24.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNA7../bbc67.. ownership of 6a088.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWaQ../bacd7.. ownership of 5f696.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN2R../6bdb6.. ownership of b8127.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRNP../4b1b7.. ownership of af10d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGuD../ea9b8.. ownership of a39a1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdWk../525e9.. ownership of 22293.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWoM../d90b2.. ownership of ae9dd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRcw../b8594.. ownership of 68791.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFik../1076e.. ownership of e3fba.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNTS../86880.. ownership of 9603b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUex../8aa8f.. ownership of 338b1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYXS../bec39.. ownership of 71c49.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLWu../818ff.. ownership of 159d1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbJa../e8533.. ownership of 54a4f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWF9../de25a.. ownership of 72b0f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLKp../7902a.. ownership of de906.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZXn../b6065.. ownership of d283c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc38../815a6.. ownership of f51da.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLeB../251db.. ownership of ab22b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLHm../aaaf6.. ownership of d3d9d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYkc../7ff80.. ownership of 253ff.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdFz../79f1d.. ownership of a70d1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHZR../7e4b9.. ownership of 265fb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUJT../125aa.. ownership of f52d3.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPHU../2d8d7.. ownership of ac5dc.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLKD../1c7f0.. ownership of 086a0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMau8../bba32.. ownership of c0ae8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGUa../c95fc.. ownership of f07f8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHQH../de5c5.. ownership of dc2ad.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHEp../966e4.. ownership of 436d2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY9e../334d5.. ownership of 26af7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRMo../cdb5a.. ownership of 0065e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNJP../2c75b.. ownership of be9f8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQpM../72a22.. ownership of 5030a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHjr../d7c35.. ownership of ae267.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEzy../d4f83.. ownership of cdbc5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGb3../50c05.. ownership of 2fb3a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZvn../40bc6.. ownership of f2960.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc89../8ecff.. ownership of 1e507.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX1W../7f664.. ownership of 8840c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVdd../e68a9.. ownership of c63ee.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZZF../3229a.. ownership of 14a50.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVvf../bec58.. ownership of b3d91.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUsM../c9f6e.. ownership of 9a13d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQm8../3e4eb.. ownership of afebd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWkY../f415f.. ownership of 74eba.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcGe../3c1b0.. ownership of 9c2bf.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbQF../8b869.. ownership of 4c37b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZRt../f1500.. ownership of b8b14.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLGv../89558.. ownership of 149e9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZhT../750e4.. ownership of d1c4d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPJo../1ac05.. ownership of 3d9f4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLUP../13c0a.. ownership of b8650.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ3j../11eb9.. ownership of 69fe6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSy9../d7631.. ownership of 585b2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNYi../730f2.. ownership of b759b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM9j../e2692.. ownership of 69e6a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYWm../48e12.. ownership of 176ea.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdH9../8bbe9.. ownership of 68bc3.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaSU../2e4b2.. ownership of 426f2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPxR../8496f.. ownership of 6a3f5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcyr../c5d6f.. ownership of b84f8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaYm../25dcb.. ownership of caa49.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMjC../848e0.. ownership of 88efa.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX3V../b9f16.. ownership of 70a67.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdz2../4a828.. ownership of a809c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLMA../9ebd3.. ownership of e09cd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXAz../a2d5f.. ownership of c5074.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSmK../49218.. ownership of 793d1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQHj../3ad81.. ownership of ece00.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNRp../a7912.. ownership of 5767a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSSW../05a4f.. ownership of fef4a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYJc../474ba.. ownership of fdeba.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTqP../3ed59.. ownership of 2f7dd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFWK../e8304.. ownership of 81564.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUNG../39526.. ownership of 57faf.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHWS../052be.. ownership of 79583.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGtB../2d154.. ownership of 541bd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPfT../14044.. ownership of 54ad2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGk1../66b72.. ownership of 24e94.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdS7../31336.. ownership of c3f1a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVpx../07b43.. ownership of 5da2d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKBT../7735d.. ownership of 2fb91.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYiN../647e9.. ownership of e09bd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTWX../2d59d.. ownership of 3a0bd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPT3../a57fa.. ownership of 2a8bd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTeN../e36ec.. ownership of f4a90.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS9S../dba93.. ownership of 99c12.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTtE../07f09.. ownership of 42a65.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc1G../cbc5a.. ownership of d4967.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP2d../7cf51.. ownership of bc6db.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGSP../21386.. ownership of fc59c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdp2../d34c1.. ownership of 9fac8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUfx../12d1e.. ownership of ba2b1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSq6../e158b.. ownership of babfe.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLtG../d8180.. ownership of 4fb85.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGDP../4ffc0.. ownership of 7b619.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcJb../1e47a.. ownership of 3228a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPDL../72796.. ownership of 91bcc.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP36../7022b.. ownership of 5c69a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJu6../20e9e.. ownership of d6948.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFkP../bff6e.. ownership of c7387.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ6M../097fa.. ownership of 4d6d4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTdp../bf9af.. ownership of fb467.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUBC../64c0b.. ownership of 24a8e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZoQ../534f7.. ownership of 8e134.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFwj../bda76.. ownership of c14e8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXAa../3a874.. ownership of 81b7d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWht../117b9.. ownership of ed125.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLZX../4c7c5.. ownership of e81b6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ33../9a5d7.. ownership of ae9b1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRED../ab93a.. ownership of 164ed.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbLW../667de.. ownership of 80564.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRkf../9750f.. ownership of c85c4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXHA../61d0d.. ownership of e65f5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRRx../e6eaa.. ownership of 30336.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJQN../19ee9.. ownership of d59ec.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWAT../02a57.. ownership of 0eacd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKrK../1b447.. ownership of d9072.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMBg../b37fb.. ownership of c4aab.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa9e../4f74a.. ownership of 65537.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUCo../4f496.. ownership of 65ce4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRKs../de986.. ownership of 9d7fd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUenj../6153d.. doc published by PrGxv..
Param and : ο → ο → ο
Param 244aa.. : (ι → ι → ο) → ο
Param 5d0c6.. : (ι → ι → ο) → ο
Param True : ο
Definition 65ce4.. := λ x0 : ι → ι → ο . and (and (244aa.. x0) (5d0c6.. x0)) True
Param 39ffe.. : (ι → ι → ο) → ο
Param 29aed.. : (ι → ι → ο) → ο
Definition c4aab.. := λ x0 : ι → ι → ο . and (and (39ffe.. x0) (29aed.. x0)) True
Definition 0eacd.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))
Param 57d6a.. : ι → ι → ι
Param 67ee8.. : ι
Param 27862.. : ι
Param bcddf.. : ι → (ι → ι) → ι
Param 1f2c4.. : ι
Param 25ca3.. : ι
Param 62f06.. : ι
Param 5b8fe.. : ι
Definition 472f9.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)))))
Definition 30336.. := λ x0 : ι → ι → ο . and (65ce4.. x0) (x0 0eacd.. 472f9..)
Param d478c.. : (ι → ι → ο) → (ι → ι → ο) → ι → ο
Conjecture 2d490.. : ∀ x0 x1 : ι → ι → ο . 65ce4.. x0 ⟶ c4aab.. x1 ⟶ d478c.. x0 x1 472f9..
Definition c85c4.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0)))))))))))
Param 3cd3c.. : ι
Param cb931.. : ι
Param 7a0ec.. : ι
Definition 164ed.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x1)))))
Definition e81b6.. := λ x0 : ι → ι → ο . and (30336.. x0) (x0 c85c4.. 164ed..)
Conjecture c05c7.. : ∀ x0 x1 : ι → ι → ο . 30336.. x0 ⟶ c4aab.. x1 ⟶ d478c.. x0 x1 164ed..
Definition 81b7d.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0)))))))))))))
Param f3baa.. : ι
Definition e09bd.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x2 x1)) (57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x3)) (57d6a.. x2 x3)))))))))))
Definition 8e134.. := λ x0 : ι → ι → ο . and (e81b6.. x0) (x0 81b7d.. e09bd..)
Conjecture d577a.. : ∀ x0 x1 : ι → ι → ο . e81b6.. x0 ⟶ c4aab.. x1 ⟶ d478c.. x0 x1 e09bd..
Definition fb467.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim1 (λ x0 . x0))))))))))))))))
Definition c7387.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x1)) (57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x3 x1)) (57d6a.. x3 x2)))))))))))
Definition 5c69a.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x1)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 81b7d.. x0) x2) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x4 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x4 x3)) (57d6a.. x4 x2)))))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x3 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. x3 x2)) (λ x4 . x4)))) x1)))))
Definition 3228a.. := λ x0 : ι → ι → ο . and (8e134.. x0) (x0 fb467.. c7387..)
Conjecture 56b32.. : ∀ x0 x1 : ι → ι → ο . 8e134.. x0 ⟶ c4aab.. x1 ⟶ d478c.. x0 x1 c7387..
Param 6fe8d.. : (ι → ι → ο) → (ι → ι → ο) → (ι → ι → ο) → ι → ι → ο
Param 5c39b.. : ι → ι → ο
Conjecture 9e9cb.. : ∀ x0 x1 : ι → ι → ο . 8e134.. x0 ⟶ c4aab.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 5c69a.. c7387..
Definition 4fb85.. := λ x0 : ι → ι → ο . and (c4aab.. x0) (x0 fb467.. 5c69a..)
Definition ba2b1.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim1 (λ x0 . x0)))))))))))))))
Definition 88efa.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x2 x1)) (57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x3) x1)) (57d6a.. x2 x3)))))))))))
Definition fc59c.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. x2 x1)) (λ x3 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x4) x1)) (λ x5 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. fb467.. x0) x1) x4) x5) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. x2))) x3))))))
Definition d4967.. := λ x0 : ι → ι → ο . and (3228a.. x0) (x0 ba2b1.. 88efa..)
Conjecture 7e7eb.. : ∀ x0 x1 : ι → ι → ο . 3228a.. x0 ⟶ 4fb85.. x1 ⟶ d478c.. x0 x1 88efa..
Conjecture 8014a.. : ∀ x0 x1 : ι → ι → ο . 3228a.. x0 ⟶ 4fb85.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. fc59c.. 88efa..
Definition 99c12.. := λ x0 : ι → ι → ο . and (4fb85.. x0) (x0 ba2b1.. fc59c..)
Definition 2a8bd.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0))))))))))))))))
Definition e09bd.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x2 x1)) (57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x3)) (57d6a.. x2 x3)))))))))))
Definition 5da2d.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. x2 x1)) (λ x3 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x4)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 81b7d.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. x2))) x3) x4)))))))
Definition 24e94.. := λ x0 : ι → ι → ο . and (d4967.. x0) (x0 2a8bd.. e09bd..)
Conjecture 23459.. : ∀ x0 x1 : ι → ι → ο . d4967.. x0 ⟶ 99c12.. x1 ⟶ d478c.. x0 x1 e09bd..
Conjecture ad066.. : ∀ x0 x1 : ι → ι → ο . d4967.. x0 ⟶ 99c12.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 5da2d.. e09bd..
Definition 541bd.. := λ x0 : ι → ι → ο . and (99c12.. x0) (x0 2a8bd.. 5da2d..)
Definition 57faf.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))
Definition 2f7dd.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x1))))))))
Definition fef4a.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2)) (λ x3 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x4) x1))) (57d6a.. (57d6a.. c85c4.. x0) x1)) x2) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1)))) (57d6a.. (57d6a.. c85c4.. x0) x1)) x2) x3)))))
Definition ece00.. := λ x0 : ι → ι → ο . and (24e94.. x0) (x0 57faf.. 2f7dd..)
Conjecture 1f6c7.. : ∀ x0 x1 : ι → ι → ο . 24e94.. x0 ⟶ 541bd.. x1 ⟶ d478c.. x0 x1 2f7dd..
Conjecture a71f4.. : ∀ x0 x1 : ι → ι → ο . 24e94.. x0 ⟶ 541bd.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. fef4a.. 2f7dd..
Definition c5074.. := λ x0 : ι → ι → ο . and (541bd.. x0) (x0 57faf.. fef4a..)
Definition a809c.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim1 (λ x0 . x0))))))))))))))))
Definition 88efa.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x2 x1)) (57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x3) x1)) (57d6a.. x2 x3)))))))))))
Definition b84f8.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. x2 x1)) (λ x3 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x4) x1)) (λ x5 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 81b7d.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. x2))) x3) x4) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 57faf.. x0) x4) x1) x5)))))))
Definition 426f2.. := λ x0 : ι → ι → ο . and (ece00.. x0) (x0 a809c.. 88efa..)
Conjecture 19fff.. : ∀ x0 x1 : ι → ι → ο . ece00.. x0 ⟶ c5074.. x1 ⟶ d478c.. x0 x1 88efa..
Conjecture f04b5.. : ∀ x0 x1 : ι → ι → ο . ece00.. x0 ⟶ c5074.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. b84f8.. 88efa..
Definition 176ea.. := λ x0 : ι → ι → ο . and (c5074.. x0) (x0 a809c.. b84f8..)
Definition b759b.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim1 (λ x0 . x0)))))))))))))))
Definition 69fe6.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. x0) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 5b8fe..) x0) x1)) x1))))))
Definition 3d9f4.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . bcddf.. (57d6a.. 3cd3c.. x0) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 5b8fe..) x0) x1)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 81b7d.. 5b8fe..) x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x3 . x3))) x2) x1)))))
Definition 149e9.. := λ x0 : ι → ι → ο . and (426f2.. x0) (x0 b759b.. 69fe6..)
Conjecture df7cd.. : ∀ x0 x1 : ι → ι → ο . 426f2.. x0 ⟶ 176ea.. x1 ⟶ d478c.. x0 x1 69fe6..
Conjecture 081ca.. : ∀ x0 x1 : ι → ι → ο . 426f2.. x0 ⟶ 176ea.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 3d9f4.. 69fe6..
Definition 4c37b.. := λ x0 : ι → ι → ο . and (176ea.. x0) (x0 b759b.. 3d9f4..)
Definition 74eba.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))))
Definition 9a13d.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2)) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x3)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x3)))))))))))
Definition 14a50.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x3)) (λ x5 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. ba2b1.. x0) x2) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x6) x3))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x6) x3))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1)))) (57d6a.. (57d6a.. c85c4.. x0) x1)) x3) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. a809c.. x0) x2) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x6) x3))) x5) x1) x4))) x2) x4)) x1) x4))))))
Definition 8840c.. := λ x0 : ι → ι → ο . and (149e9.. x0) (x0 74eba.. 9a13d..)
Conjecture cf051.. : ∀ x0 x1 : ι → ι → ο . 149e9.. x0 ⟶ 4c37b.. x1 ⟶ d478c.. x0 x1 9a13d..
Conjecture c6ef0.. : ∀ x0 x1 : ι → ι → ο . 149e9.. x0 ⟶ 4c37b.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 14a50.. 9a13d..
Definition f2960.. := λ x0 : ι → ι → ο . and (4c37b.. x0) (x0 74eba.. 14a50..)
Definition cdbc5.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim1 (λ x0 . x0)))))))))))
Definition 5030a.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x1 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) x1)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) x1))) (λ x2 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x3) x4)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) (57d6a.. x2 x3)) (57d6a.. x2 x4)))))))))))))
Definition 0065e.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. 1f2c4.. (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) x1))) (λ x2 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x3) x4)) (λ x5 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. ba2b1.. x0) x4) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) (57d6a.. x2 x6)) (57d6a.. x2 x4)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x3) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) (57d6a.. x2 x6)) (57d6a.. x2 x4)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x3) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) (57d6a.. x2 x3)) (57d6a.. x2 x6)))) (57d6a.. (57d6a.. c85c4.. x1) (57d6a.. x2 x3))) x4) x5)) x4) x5)) x3) x5))))))
Definition 436d2.. := λ x0 : ι → ι → ο . and (8840c.. x0) (x0 cdbc5.. 5030a..)
Conjecture 2c56b.. : ∀ x0 x1 : ι → ι → ο . 8840c.. x0 ⟶ f2960.. x1 ⟶ d478c.. x0 x1 5030a..
Conjecture 5c292.. : ∀ x0 x1 : ι → ι → ο . 8840c.. x0 ⟶ f2960.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 0065e.. 5030a..
Definition f07f8.. := λ x0 : ι → ι → ο . and (f2960.. x0) (x0 cdbc5.. 0065e..)
Definition 086a0.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x1) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim1 (λ x0 . x0))))))))))))
Definition f52d3.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x1 . 57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x2 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x1) x2))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x1) x2)))) (λ x3 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x5 . 57d6a.. (57d6a.. 7a0ec.. x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x6 . 57d6a.. (57d6a.. 7a0ec.. x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x7 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x4) x5)) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) x6) x7)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x4) x6)) (57d6a.. (57d6a.. x3 x5) x7))))))))))))))))))))
Definition a70d1.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. 1f2c4.. (λ x1 . bcddf.. 1f2c4.. (λ x2 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x1) x2)))) (λ x3 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x5 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x6 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x7 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x4) x5)) (λ x8 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) x6) x7)) (λ x9 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. ba2b1.. x0) x5) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x10) x6)) (57d6a.. (57d6a.. x3 x5) x7)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. ba2b1.. x1) x7) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x5) x10)) (57d6a.. (57d6a.. x3 x5) x7)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x4) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x10) x7)) (57d6a.. (57d6a.. x3 x5) x7)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x1) x6) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x4) x10)) (57d6a.. (57d6a.. x3 x5) x7)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x4) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x4) x6)) (57d6a.. (57d6a.. x3 x10) x7)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x1) x6) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x4) x6)) (57d6a.. (57d6a.. x3 x4) x10)))) (57d6a.. (57d6a.. c85c4.. x2) (57d6a.. (57d6a.. x3 x4) x6))) x7) x9)) x5) x8)) x7) x9)) x5) x8)) x6) x9)) x4) x8))))))))))
Definition d3d9d.. := λ x0 : ι → ι → ο . and (436d2.. x0) (x0 086a0.. f52d3..)
Conjecture 3b5f0.. : ∀ x0 x1 : ι → ι → ο . 436d2.. x0 ⟶ f07f8.. x1 ⟶ d478c.. x0 x1 f52d3..
Conjecture d0468.. : ∀ x0 x1 : ι → ι → ο . 436d2.. x0 ⟶ f07f8.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. a70d1.. f52d3..
Definition f51da.. := λ x0 : ι → ι → ο . and (f07f8.. x0) (x0 086a0.. a70d1..)
Definition de906.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))))
Param ae581.. : ι
Definition 54a4f.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (57d6a.. (57d6a.. f3baa.. ae581..))))
Definition 71c49.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . x1)))) (λ x1 . 57d6a.. x1 x0))
Definition 9603b.. := λ x0 : ι → ι → ο . and (d3d9d.. x0) (x0 de906.. 54a4f..)
Conjecture 0d946.. : ∀ x0 x1 : ι → ι → ο . d3d9d.. x0 ⟶ f51da.. x1 ⟶ d478c.. x0 x1 54a4f..
Conjecture 94b30.. : ∀ x0 x1 : ι → ι → ο . d3d9d.. x0 ⟶ f51da.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 71c49.. 54a4f..
Definition 68791.. := λ x0 : ι → ι → ο . and (f51da.. x0) (x0 de906.. 71c49..)
Definition 22293.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0))))))))))))))
Param c8911.. : ι
Definition af10d.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. f3baa.. x0) ae581..)) x1)) (57d6a.. (57d6a.. f3baa.. (57d6a.. c8911.. x0)) x1))))))
Definition 5f696.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. f3baa.. x0) ae581..)) x1)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. c8911.. x0)) (57d6a.. x2))))
Definition 0ec24.. := λ x0 : ι → ι → ο . and (9603b.. x0) (x0 22293.. af10d..)
Conjecture 56228.. : ∀ x0 x1 : ι → ι → ο . 9603b.. x0 ⟶ 68791.. x1 ⟶ d478c.. x0 x1 af10d..
Conjecture be1a5.. : ∀ x0 x1 : ι → ι → ο . 9603b.. x0 ⟶ 68791.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 5f696.. af10d..
Definition 9aa0b.. := λ x0 : ι → ι → ο . and (68791.. x0) (x0 22293.. 5f696..)
Definition 0ad46.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0)))))))))))))
Definition b02dd.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. f3baa.. x0) (57d6a.. (57d6a.. f3baa.. (57d6a.. c8911.. x0)) ae581..))))
Definition 7e03f.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 3cd3c.. x0) (λ x1 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. c8911.. x0)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 22293.. x0) ae581..) (bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. x0) ae581..)) (λ x2 . 57d6a.. x2 x1))))))
Definition ab95a.. := λ x0 : ι → ι → ο . and (0ec24.. x0) (x0 0ad46.. b02dd..)
Conjecture 18783.. : ∀ x0 x1 : ι → ι → ο . 0ec24.. x0 ⟶ 9aa0b.. x1 ⟶ d478c.. x0 x1 b02dd..
Conjecture bcfb2.. : ∀ x0 x1 : ι → ι → ο . 0ec24.. x0 ⟶ 9aa0b.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 7e03f.. b02dd..
Definition a3364.. := λ x0 : ι → ι → ο . and (9aa0b.. x0) (x0 0ad46.. 7e03f..)
Definition ee03a.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0)))))))))))))))))
Definition 6543a.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. f3baa.. x0) x1)) (57d6a.. (57d6a.. f3baa.. (57d6a.. c8911.. x1)) (57d6a.. c8911.. x0)))))))
Definition 476c5.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. x0) x1)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. c8911.. x1)) (λ x3 . bcddf.. (57d6a.. 3cd3c.. x0) (λ x4 . 57d6a.. (57d6a.. (57d6a.. 0ad46.. x1) (57d6a.. x2 x4)) x3)))))
Definition 43682.. := λ x0 : ι → ι → ο . and (ab95a.. x0) (x0 ee03a.. 6543a..)
Conjecture c2121.. : ∀ x0 x1 : ι → ι → ο . ab95a.. x0 ⟶ a3364.. x1 ⟶ d478c.. x0 x1 6543a..
Conjecture abebd.. : ∀ x0 x1 : ι → ι → ο . ab95a.. x0 ⟶ a3364.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 476c5.. 6543a..
Definition dee3e.. := λ x0 : ι → ι → ο . and (a3364.. x0) (x0 ee03a.. 476c5..)
Definition 4f606.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))))))
Definition daa3d.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. c8911.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2))) (57d6a.. c8911.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x1)))))))))
Definition 65146.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. c8911.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2))) (λ x3 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x1)) (λ x4 . 57d6a.. (57d6a.. (57d6a.. 0ad46.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. a809c.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1)))) (57d6a.. (57d6a.. c85c4.. x0) x1)) x2) x4)) x3)))))
Definition aac29.. := λ x0 : ι → ι → ο . and (43682.. x0) (x0 4f606.. daa3d..)
Conjecture 8816a.. : ∀ x0 x1 : ι → ι → ο . 43682.. x0 ⟶ dee3e.. x1 ⟶ d478c.. x0 x1 daa3d..
Conjecture 82e8c.. : ∀ x0 x1 : ι → ι → ο . 43682.. x0 ⟶ dee3e.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 65146.. daa3d..
Definition 505b1.. := λ x0 : ι → ι → ο . and (dee3e.. x0) (x0 4f606.. 65146..)