Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrJj8../7071a..
PUfmP../b0638..
vout
PrJj8../42a66.. 24.98 bars
TMKrw../b591c.. ownership of 77bfd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYtq../f043b.. ownership of 2baef.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFk4../00d31.. ownership of 11ab3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHgm../e4a9e.. ownership of 0413f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHtA../03b33.. ownership of e88d1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPCo../3100d.. ownership of 13b0b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP5X../e8cee.. ownership of 0a953.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJB6../d7720.. ownership of b9b9c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVex../ea2d4.. ownership of 58929.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdqw../61585.. ownership of 801fe.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZve../596fa.. ownership of 0a4ae.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZD9../f8063.. ownership of 576bb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbLu../f5d56.. ownership of 3bc26.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYzH../2f593.. ownership of a64e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQuL../da4db.. ownership of d04af.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPfT../b8ad5.. ownership of 2d3e8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG6H../2724a.. ownership of 5549c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRJT../b41ae.. ownership of 26b8b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXU9../51371.. ownership of 2473b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNx2../b9391.. ownership of a9441.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMasJ../32664.. ownership of 293e1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGdK../655f6.. ownership of 7c8aa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFiC../491d8.. ownership of df2ad.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXUd../e12ac.. ownership of 36283.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXBH../3cb17.. ownership of e670a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRBM../80e0c.. ownership of 5622e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRGB../f6a4f.. ownership of 1e440.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTXq../110b7.. ownership of 53dad.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPKY../d7d9b.. ownership of cf832.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYBt../a69aa.. ownership of 07f0b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKGC../b6e78.. ownership of 99e8a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWrX../ff42b.. ownership of a5b77.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcQo../fe575.. ownership of cc896.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb1X../ffb46.. ownership of bd8cf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSbX../cdc24.. ownership of 08db2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUch../66d97.. ownership of b1cbd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLQr../bfbef.. ownership of 0c40e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPF2../67aa2.. ownership of 435ff.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaFb../91928.. ownership of f870f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ3V../1c899.. ownership of 90f68.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQH3../6607c.. ownership of a6148.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXZG../9483f.. ownership of eccef.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdib../d09b4.. ownership of 61077.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFFK../0d2c0.. ownership of 7953c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcyM../1c298.. ownership of 29f0c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLbR../8b1c3.. ownership of bbb55.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVaL../98584.. ownership of 7833c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU7z../1b7a2.. ownership of cc88b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUrs../f6f69.. ownership of eac13.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG8n../2374b.. ownership of 1dac6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF2n../89c80.. ownership of d989f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP37../50d62.. ownership of 3f900.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVmt../2d7ca.. ownership of e3dba.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLZS../47e7a.. ownership of 8550c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQEZ../77438.. ownership of 4eb22.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTLk../12b20.. ownership of 3f600.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdgr../efd8a.. ownership of 67806.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNZb../cd84d.. ownership of 2cc74.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNP7../a7314.. ownership of 46c2b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd2g../b0e7d.. ownership of c5e8a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaLp../a0c5f.. ownership of bd572.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbQj../28e09.. ownership of 17d4f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKod../0fb0a.. ownership of e5a18.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPmK../86f70.. ownership of 19657.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGkD../af5f8.. ownership of b7d3c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT99../fb6b3.. ownership of 8934c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdS8../a4d89.. ownership of 8892a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQLS../c5986.. ownership of 30c66.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaSu../409a8.. ownership of 9e7c7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMqa../ac273.. ownership of 0369d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVtJ../94b41.. ownership of af877.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcBX../3be9a.. ownership of 1a8f3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTiu../3a954.. ownership of b50ff.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRVr../ab505.. ownership of 59ac3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJkh../23d2b.. ownership of aa6de.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRnR../ae052.. ownership of c3fff.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGAd../b8c9a.. ownership of e5821.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHcy../853a8.. ownership of f7367.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKJH../65010.. ownership of e3820.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJMG../8fdaa.. ownership of 38181.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWfL../e897b.. ownership of 75de5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRMN../430da.. ownership of 639df.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdgh../5693a.. ownership of c310c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd7t../46e55.. ownership of 3d09d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLfq../f6960.. ownership of ddaaf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGpw../28b6b.. ownership of 7a527.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUqJ../541e1.. ownership of 03342.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQfc../912e8.. ownership of 83c69.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFHR../de319.. ownership of 6d0ba.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcc6../baf43.. ownership of 6f67e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcPb../a5e78.. ownership of af02e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSjz../2dcc3.. ownership of 4a59b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZTd../e037e.. ownership of ad831.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc9g../05756.. ownership of 161e1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMRh../c5bf6.. ownership of cea9c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb56../26e68.. ownership of e97a7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYAk../04cf2.. ownership of 6d178.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHUN../9a88c.. ownership of 63f2f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb2L../0a399.. ownership of d6e0e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUho../d03b7.. ownership of fc689.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZWM../a02b3.. ownership of 9794d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR25../1e0ee.. ownership of cf937.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVZS../38097.. ownership of 7da76.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPvU../bc4bd.. ownership of 9f43c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYpL../2929e.. ownership of b23c6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRR7../48e5d.. ownership of 17ea7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPWY../47fb3.. ownership of 6071f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSvt../4eb02.. ownership of ff6d5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYoJ../5772c.. ownership of 70120.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMgV../5a00a.. ownership of 10ad6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLS8../b49c4.. ownership of c9763.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKLf../440d2.. ownership of 6cbd7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWA2../3ff27.. ownership of 97885.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMStT../7f567.. ownership of 6c28b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQJ6../2c3bc.. ownership of b5643.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa8j../2d26b.. ownership of 2fded.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWDZ../f2818.. ownership of 1efa9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaZ4../be0a0.. ownership of 83266.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUQx../1c252.. ownership of 3efb3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRjs../502f0.. ownership of cbfe1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdXh../5eb10.. ownership of 86929.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdPq../a83b8.. ownership of 8db96.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJAm../16861.. ownership of d78b8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaxa../32e75.. ownership of c55d4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFLi../578d6.. ownership of 0a986.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPdc../2b29d.. ownership of 48f97.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXTh../4be71.. ownership of 730cb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMV13../53ec9.. ownership of dfd4f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRvs../79607.. ownership of 671d1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMJv../653b1.. ownership of d4148.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSxL../32b1e.. ownership of 5e2e5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUHc../73786.. ownership of 2ec40.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLji../7d17f.. ownership of 2a85a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEht../5e415.. ownership of a6d01.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYRg../5024c.. ownership of 7a9a7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVB7../4643e.. ownership of d0dab.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYxc../30af4.. ownership of 66d42.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPSW../d67a5.. ownership of 97d7c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHQN../75344.. ownership of e2c49.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMMf../843ac.. ownership of f7442.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF85../53f15.. ownership of 56c1e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMREJ../1442a.. ownership of 88e63.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNdh../ccc72.. ownership of 38231.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXAY../180e3.. ownership of 8c729.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH1r../6ee99.. ownership of 34d3b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPJ8../77226.. ownership of ac8d2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJyG../4f74c.. ownership of 5c6b7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbbw../80229.. ownership of e7448.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbxk../a9d70.. ownership of 6d899.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWGs../c56ba.. ownership of dd3d0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVEX../63a43.. ownership of 8d403.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEsY../586ef.. ownership of d8672.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPkL../1aaab.. ownership of a4680.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPAd../6dd33.. ownership of 72f47.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN4w../f4c99.. ownership of ae02b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSzk../c7768.. ownership of a27f1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKZF../47766.. ownership of 882cc.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG7s../32f14.. ownership of 6b9fc.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMqU../6ce86.. ownership of 3be00.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF82../58c98.. ownership of 55776.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKm6../d0837.. ownership of 14e81.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGqW../367f8.. ownership of 4ad7b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWWF../f22b4.. ownership of 264ee.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRGF../1d396.. ownership of 6fbf7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML2j../f8bbb.. ownership of 734b8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWcy../12f99.. ownership of 2cc57.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTNu../6d17c.. ownership of 311a4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaje../687ef.. ownership of a3d17.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMNd../6faf0.. ownership of 57517.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRxT../f2363.. ownership of 828bf.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbnK../a64cc.. ownership of 7e46e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYXd../7c3ba.. ownership of b799a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXYe../5d826.. ownership of d0331.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc1U../5bec4.. ownership of 179b9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQH8../dedd8.. ownership of d8d71.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPqu../3b8e2.. ownership of 8aa77.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXwe../bc947.. ownership of 7aeb9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJrJ../8262c.. ownership of a4019.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNig../6aa92.. ownership of ba600.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSiH../93842.. ownership of e597f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUTfE../ee81c.. doc published by PrGxv..
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Param 1216a.. : ι → (ι → ο) → ι
Definition ba600.. := λ x0 . λ x1 x2 : ι → ι . λ x3 x4 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (1216a.. x0 x3) (1216a.. x0 x4)))))
Param f482f.. : ι → ι → ι
Known 7d2e2.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) 4a7ef.. = x0
Theorem 5c6b7.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = ba600.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 34d3b.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . x0 = f482f.. (ba600.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Known 504a8.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. 4a7ef..) = x1
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem 38231.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = ba600.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x6 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 (proof)
Theorem 56c1e.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x1 x5 = f482f.. (f482f.. (ba600.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 (proof)
Known fb20c.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2
Theorem e2c49.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = ba600.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 (proof)
Theorem 66d42.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x2 x5 = f482f.. (f482f.. (ba600.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Param decode_p : ι → ι → ο
Known 431f3.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem 7a9a7.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = ba600.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem 2a85a.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x3 x5 = decode_p (f482f.. (ba600.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Known ffdcd.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = x4
Theorem 5e2e5.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = ba600.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x5 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 (proof)
Theorem 671d1.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x4 x5 = decode_p (f482f.. (ba600.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Theorem 730cb.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι . ∀ x6 x7 x8 x9 : ι → ο . ba600.. x0 x2 x4 x6 x8 = ba600.. x1 x3 x5 x7 x9 ⟶ and (and (and (and (x0 = x1) (∀ x10 . prim1 x10 x0 ⟶ x2 x10 = x3 x10)) (∀ x10 . prim1 x10 x0 ⟶ x4 x10 = x5 x10)) (∀ x10 . prim1 x10 x0 ⟶ x6 x10 = x7 x10)) (∀ x10 . prim1 x10 x0 ⟶ x8 x10 = x9 x10) (proof)
Param iff : ο → ο → ο
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
Known 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2
Theorem 0a986.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι . ∀ x5 x6 x7 x8 : ι → ο . (∀ x9 . prim1 x9 x0 ⟶ x1 x9 = x2 x9) ⟶ (∀ x9 . prim1 x9 x0 ⟶ x3 x9 = x4 x9) ⟶ (∀ x9 . prim1 x9 x0 ⟶ iff (x5 x9) (x6 x9)) ⟶ (∀ x9 . prim1 x9 x0 ⟶ iff (x7 x9) (x8 x9)) ⟶ ba600.. x0 x1 x3 x5 x7 = ba600.. x0 x2 x4 x6 x8 (proof)
Definition 7aeb9.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ prim1 (x4 x5) x2) ⟶ ∀ x5 x6 : ι → ο . x1 (ba600.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem d78b8.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x0) ⟶ ∀ x3 x4 : ι → ο . 7aeb9.. (ba600.. x0 x1 x2 x3 x4) (proof)
Theorem 86929.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . 7aeb9.. (ba600.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x1 x5) x0 (proof)
Theorem 3efb3.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . 7aeb9.. (ba600.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x2 x5) x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem 1efa9.. : ∀ x0 . 7aeb9.. x0 ⟶ x0 = ba600.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Definition d8d71.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι) → (ι → ο) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem b5643.. : ∀ x0 : ι → (ι → ι) → (ι → ι) → (ι → ο) → (ι → ο) → ι . ∀ x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ο . (∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ο . (∀ x9 . prim1 x9 x1 ⟶ iff (x4 x9) (x8 x9)) ⟶ ∀ x9 : ι → ο . (∀ x10 . prim1 x10 x1 ⟶ iff (x5 x10) (x9 x10)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ d8d71.. (ba600.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition d0331.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι) → (ι → ο) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem 97885.. : ∀ x0 : ι → (ι → ι) → (ι → ι) → (ι → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ο . (∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ο . (∀ x9 . prim1 x9 x1 ⟶ iff (x4 x9) (x8 x9)) ⟶ ∀ x9 : ι → ο . (∀ x10 . prim1 x10 x1 ⟶ iff (x5 x10) (x9 x10)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ d0331.. (ba600.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 7e46e.. := λ x0 . λ x1 x2 : ι → ι . λ x3 : ι → ο . λ x4 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (1216a.. x0 x3) x4))))
Theorem c9763.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = 7e46e.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 70120.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x0 = f482f.. (7e46e.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem 6071f.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = 7e46e.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x6 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 (proof)
Theorem b23c6.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ x1 x5 = f482f.. (f482f.. (7e46e.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 7da76.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = 7e46e.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 (proof)
Theorem 9794d.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ x2 x5 = f482f.. (f482f.. (7e46e.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem d6e0e.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = 7e46e.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem 6d178.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ x3 x5 = decode_p (f482f.. (7e46e.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem cea9c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = 7e46e.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem ad831.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x4 = f482f.. (7e46e.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem af02e.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι . ∀ x6 x7 : ι → ο . ∀ x8 x9 . 7e46e.. x0 x2 x4 x6 x8 = 7e46e.. x1 x3 x5 x7 x9 ⟶ and (and (and (and (x0 = x1) (∀ x10 . prim1 x10 x0 ⟶ x2 x10 = x3 x10)) (∀ x10 . prim1 x10 x0 ⟶ x4 x10 = x5 x10)) (∀ x10 . prim1 x10 x0 ⟶ x6 x10 = x7 x10)) (x8 = x9) (proof)
Theorem 6d0ba.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι . ∀ x5 x6 : ι → ο . ∀ x7 . (∀ x8 . prim1 x8 x0 ⟶ x1 x8 = x2 x8) ⟶ (∀ x8 . prim1 x8 x0 ⟶ x3 x8 = x4 x8) ⟶ (∀ x8 . prim1 x8 x0 ⟶ iff (x5 x8) (x6 x8)) ⟶ 7e46e.. x0 x1 x3 x5 x7 = 7e46e.. x0 x2 x4 x6 x7 (proof)
Definition 57517.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ prim1 (x4 x5) x2) ⟶ ∀ x5 : ι → ο . ∀ x6 . prim1 x6 x2 ⟶ x1 (7e46e.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 03342.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x0) ⟶ ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ 57517.. (7e46e.. x0 x1 x2 x3 x4) (proof)
Theorem ddaaf.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . 57517.. (7e46e.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x1 x5) x0 (proof)
Theorem c310c.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . 57517.. (7e46e.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x2 x5) x0 (proof)
Theorem 75de5.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . 57517.. (7e46e.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem e3820.. : ∀ x0 . 57517.. x0 ⟶ x0 = 7e46e.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 311a4.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι) → (ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem e5821.. : ∀ x0 : ι → (ι → ι) → (ι → ι) → (ι → ο) → ι → ι . ∀ x1 . ∀ x2 x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . (∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ο . (∀ x9 . prim1 x9 x1 ⟶ iff (x4 x9) (x8 x9)) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ 311a4.. (7e46e.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 734b8.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι) → (ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem aa6de.. : ∀ x0 : ι → (ι → ι) → (ι → ι) → (ι → ο) → ι → ο . ∀ x1 . ∀ x2 x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . (∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ο . (∀ x9 . prim1 x9 x1 ⟶ iff (x4 x9) (x8 x9)) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ 734b8.. (7e46e.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 264ee.. := λ x0 . λ x1 x2 : ι → ι . λ x3 x4 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))
Theorem b50ff.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 . x0 = 264ee.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem af877.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 . x0 = f482f.. (264ee.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem 9e7c7.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 . x0 = 264ee.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x6 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 (proof)
Theorem 8892a.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ x1 x5 = f482f.. (f482f.. (264ee.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 (proof)
Theorem b7d3c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 . x0 = 264ee.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 (proof)
Theorem e5a18.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ x2 x5 = f482f.. (f482f.. (264ee.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem bd572.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 . x0 = 264ee.. x1 x2 x3 x4 x5 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 46c2b.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 . x3 = f482f.. (264ee.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 67806.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 . x0 = 264ee.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 4eb22.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 . x4 = f482f.. (264ee.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem e3dba.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι . ∀ x6 x7 x8 x9 . 264ee.. x0 x2 x4 x6 x8 = 264ee.. x1 x3 x5 x7 x9 ⟶ and (and (and (and (x0 = x1) (∀ x10 . prim1 x10 x0 ⟶ x2 x10 = x3 x10)) (∀ x10 . prim1 x10 x0 ⟶ x4 x10 = x5 x10)) (x6 = x7)) (x8 = x9) (proof)
Theorem d989f.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι . ∀ x5 x6 . (∀ x7 . prim1 x7 x0 ⟶ x1 x7 = x2 x7) ⟶ (∀ x7 . prim1 x7 x0 ⟶ x3 x7 = x4 x7) ⟶ 264ee.. x0 x1 x3 x5 x6 = 264ee.. x0 x2 x4 x5 x6 (proof)
Definition 14e81.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ prim1 (x4 x5) x2) ⟶ ∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ x1 (264ee.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem eac13.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x0) ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ 14e81.. (264ee.. x0 x1 x2 x3 x4) (proof)
Theorem 7833c.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 . 14e81.. (264ee.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x1 x5) x0 (proof)
Theorem 29f0c.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 . 14e81.. (264ee.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x2 x5) x0 (proof)
Theorem 61077.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 . 14e81.. (264ee.. x0 x1 x2 x3 x4) ⟶ prim1 x3 x0 (proof)
Theorem a6148.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 . 14e81.. (264ee.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem f870f.. : ∀ x0 . 14e81.. x0 ⟶ x0 = 264ee.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 3be00.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι) → ι → ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 0c40e.. : ∀ x0 : ι → (ι → ι) → (ι → ι) → ι → ι → ι . ∀ x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 . (∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ 3be00.. (264ee.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 882cc.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι) → ι → ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 08db2.. : ∀ x0 : ι → (ι → ι) → (ι → ι) → ι → ι → ο . ∀ x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 . (∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ 882cc.. (264ee.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Param d2155.. : ι → (ι → ι → ο) → ι
Definition ae02b.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . λ x3 x4 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (1216a.. x0 x3) (1216a.. x0 x4)))))
Theorem cc896.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . x0 = ae02b.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 99e8a.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . x0 = f482f.. (ae02b.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem cf832.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . x0 = ae02b.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x6 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 (proof)
Theorem 1e440.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x1 x5 = f482f.. (f482f.. (ae02b.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 (proof)
Param 2b2e3.. : ι → ι → ι → ο
Known 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ 2b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3
Theorem e670a.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . x0 = ae02b.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 x7 (proof)
Theorem df2ad.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = 2b2e3.. (f482f.. (ae02b.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 293e1.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . x0 = ae02b.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem 2473b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x3 x5 = decode_p (f482f.. (ae02b.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem 5549c.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . x0 = ae02b.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x5 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 (proof)
Theorem d04af.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x4 x5 = decode_p (f482f.. (ae02b.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 (proof)
Theorem 3bc26.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ο . ∀ x6 x7 x8 x9 : ι → ο . ae02b.. x0 x2 x4 x6 x8 = ae02b.. x1 x3 x5 x7 x9 ⟶ and (and (and (and (x0 = x1) (∀ x10 . prim1 x10 x0 ⟶ x2 x10 = x3 x10)) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x4 x10 x11 = x5 x10 x11)) (∀ x10 . prim1 x10 x0 ⟶ x6 x10 = x7 x10)) (∀ x10 . prim1 x10 x0 ⟶ x8 x10 = x9 x10) (proof)
Known 62ef7.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ iff (x1 x3 x4) (x2 x3 x4)) ⟶ d2155.. x0 x1 = d2155.. x0 x2
Theorem 0a4ae.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 x6 x7 x8 : ι → ο . (∀ x9 . prim1 x9 x0 ⟶ x1 x9 = x2 x9) ⟶ (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ iff (x3 x9 x10) (x4 x9 x10)) ⟶ (∀ x9 . prim1 x9 x0 ⟶ iff (x5 x9) (x6 x9)) ⟶ (∀ x9 . prim1 x9 x0 ⟶ iff (x7 x9) (x8 x9)) ⟶ ae02b.. x0 x1 x3 x5 x7 = ae02b.. x0 x2 x4 x6 x8 (proof)
Definition a4680.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . x1 (ae02b.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 58929.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . a4680.. (ae02b.. x0 x1 x2 x3 x4) (proof)
Theorem 0a953.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . a4680.. (ae02b.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x1 x5) x0 (proof)
Theorem e88d1.. : ∀ x0 . a4680.. x0 ⟶ x0 = ae02b.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Definition 8d403.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι → ο) → (ι → ο) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem 11ab3.. : ∀ x0 : ι → (ι → ι) → (ι → ι → ο) → (ι → ο) → (ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . (∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x3 x8 x9) (x7 x8 x9)) ⟶ ∀ x8 : ι → ο . (∀ x9 . prim1 x9 x1 ⟶ iff (x4 x9) (x8 x9)) ⟶ ∀ x9 : ι → ο . (∀ x10 . prim1 x10 x1 ⟶ iff (x5 x10) (x9 x10)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ 8d403.. (ae02b.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 6d899.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι → ο) → (ι → ο) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem 77bfd.. : ∀ x0 : ι → (ι → ι) → (ι → ι → ο) → (ι → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . (∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x3 x8 x9) (x7 x8 x9)) ⟶ ∀ x8 : ι → ο . (∀ x9 . prim1 x9 x1 ⟶ iff (x4 x9) (x8 x9)) ⟶ ∀ x9 : ι → ο . (∀ x10 . prim1 x10 x1 ⟶ iff (x5 x10) (x9 x10)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ 6d899.. (ae02b.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)