Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrRYw../5ee6e..
PUKBw../49c3f..
vout
PrRYw../4f929.. 24.98 bars
TMYoU../c8ece.. ownership of 19a2d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdwm../72403.. ownership of 6f0d1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHpF../9bdca.. ownership of 2ec61.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdNy../6d18b.. ownership of fcc48.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVjv../613a2.. ownership of 77020.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVSB../23756.. ownership of 35ef2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGqL../8678b.. ownership of a6584.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRne../11779.. ownership of 7ac04.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR4i../50982.. ownership of 55882.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd9F../3345e.. ownership of cd534.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTdH../26114.. ownership of 98f19.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZeY../134a6.. ownership of afd3e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUnh../9905f.. ownership of ad833.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbCM../41212.. ownership of 29343.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGB3../ef0c6.. ownership of 27c75.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNvG../6d8ac.. ownership of 0cdf8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQB2../6d45e.. ownership of 96786.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJfv../3678e.. ownership of 4891b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWmL../25574.. ownership of 5b026.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZvh../22a60.. ownership of ec415.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJRb../95e7b.. ownership of 8c63b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT9F../e8f4c.. ownership of 66405.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMU7../90d32.. ownership of 42853.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFr3../354ed.. ownership of 57fea.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPFt../ac49b.. ownership of 9c2c2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXYR../3043d.. ownership of cd749.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLFb../55752.. ownership of ad372.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLZr../71f26.. ownership of 0ebad.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcqx../09faf.. ownership of 0c8ea.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNkE../2b6ac.. ownership of e14f7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX8h../70699.. ownership of b2354.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRhM../5e5e9.. ownership of f5fe4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVRx../5b8cd.. ownership of de93d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYt3../36dfd.. ownership of e8406.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMDc../7109c.. ownership of 1f7f5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKGQ../96267.. ownership of ca80a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQBj../3e582.. ownership of fff31.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTEg../aaa02.. ownership of b06d1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTDK../f1d31.. ownership of 34ab5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG4n../873f1.. ownership of da8be.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYbE../527fb.. ownership of 6b740.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd6Y../15b69.. ownership of 7fcae.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ66../90aeb.. ownership of 4d8d1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGSP../90912.. ownership of be702.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRP3../fd7d2.. ownership of 5f7bc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYSc../bba3a.. ownership of 800b9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJDy../2bfd6.. ownership of 6bcf3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ4i../85fba.. ownership of c97de.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML2a../75361.. ownership of 9df7f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMky../23b3a.. ownership of 2fe36.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUkZ../3ffe4.. ownership of fa56b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUzX../e3628.. ownership of 2dcce.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT53../f4393.. ownership of 5c572.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMRZ../a5633.. ownership of 76655.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT1L../f63a3.. ownership of 1741e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaen../9a133.. ownership of dcbb4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGNP../8f7c3.. ownership of 30331.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEoj../7a44b.. ownership of b668c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTaJ../78900.. ownership of 62515.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMvb../e769a.. ownership of b6161.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcKG../e1718.. ownership of 54141.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUj7../ee5c2.. ownership of 22523.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKgt../1302c.. ownership of 44359.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQGt../5d7d9.. ownership of e85ab.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNZW../bef33.. ownership of 90bdf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS5S../ca119.. ownership of 574d0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUBQ../00efb.. ownership of e2946.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc9c../14aed.. ownership of f7651.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcmx../baed3.. ownership of 9205a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTTU../ecdc8.. ownership of 851fa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVg4../b443c.. ownership of 49059.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcX5../87c65.. ownership of 86667.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKXY../804e1.. ownership of 7b9b4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaEp../eb836.. ownership of 95991.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQhv../3f6d3.. ownership of c03b4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYe4../d3d51.. ownership of d5904.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMajt../99c66.. ownership of b4986.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUKT../7ae02.. ownership of 8077b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWsg../f6145.. ownership of 29640.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWU8../67616.. ownership of 6819b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMY9../f8304.. ownership of ea18c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNbH../8746e.. ownership of 86bcb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPqq../ecd0a.. ownership of a0b68.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJBX../2d279.. ownership of ed001.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLRH../bf5bd.. ownership of 1fd36.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcKH../9b90a.. ownership of d62dc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRkM../065df.. ownership of cdba3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUdg../b66a5.. ownership of 0dcb6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLLG../e1e45.. ownership of c5ea1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaNG../ab739.. ownership of 022e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQwT../02888.. ownership of 71b43.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYm4../ff96e.. ownership of d3a64.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS3L../12cb3.. ownership of 0f14e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFaw../1d9c3.. ownership of c38a1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSx3../01869.. ownership of 4c95d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb9h../54895.. ownership of 6cd6c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdRu../df5a9.. ownership of 71c9c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML7t../a4ba7.. ownership of c50e4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHbX../ba7a6.. ownership of 1348b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQf3../67649.. ownership of ba755.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVhd../71623.. ownership of 8cd35.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXSs../5f7b5.. ownership of eed20.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNXw../5305a.. ownership of c7fd3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRUu../5e397.. ownership of 8908b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUsW../9a200.. ownership of 77703.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLCt../0c9ad.. ownership of 0e447.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNGW../4b882.. ownership of 0b229.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWWt../f488b.. ownership of 6168c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML3A../0ac7e.. ownership of b2ef3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHmJ../65f8d.. ownership of 91a6b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLft../4fde6.. ownership of 2f87c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU3Z../93d01.. ownership of cafd8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdEy../2cbde.. ownership of 7c672.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZkd../9e46a.. ownership of 9c03b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ7h../03726.. ownership of cb18b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcGU../b6f0c.. ownership of 6104b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNQP../32de9.. ownership of c30a4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYxa../f86aa.. ownership of 76059.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbki../2164e.. ownership of f2018.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNed../cd7ac.. ownership of 28839.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKz2../5e257.. ownership of fe636.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLB9../96772.. ownership of 06b85.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNay../ba0ba.. ownership of 56b30.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJyY../20a78.. ownership of 33530.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFDG../0faf5.. ownership of 9cd02.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcQ4../90a31.. ownership of a35ed.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbY5../06f6a.. ownership of bd863.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUvc../34865.. ownership of 804e2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK4V../467cc.. ownership of 1f38c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQhy../e3acf.. ownership of a45ab.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMagQ../6181a.. ownership of 26d45.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRMw../47ddb.. ownership of 6826c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdmz../f6623.. ownership of c5a21.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcZS../f2bc5.. ownership of 12c6e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYFE../33cfb.. ownership of 73165.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbRK../25788.. ownership of 2d5b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMew../e0b0e.. ownership of be277.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPNR../a51a2.. ownership of 8482b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbvQ../51fa0.. ownership of 4a2a6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdDP../1b0b9.. ownership of 9331c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRoN../97bba.. ownership of e05f5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVAS../5756a.. ownership of 1b2e7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQGn../b9f33.. ownership of 1c95b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ3U../a1692.. ownership of 61cca.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY1o../75841.. ownership of 7f9b4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW8L../51533.. ownership of 67abb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUop../1d1bd.. ownership of abb35.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLNu../f8877.. ownership of c8763.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRg4../cce32.. ownership of 8617f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTMJ../84557.. ownership of 96066.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNVU../7bccf.. ownership of 918ae.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdZ4../30712.. ownership of 2aced.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcCd../d77ae.. ownership of da128.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFW9../94bf4.. ownership of 21187.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGWg../aa33f.. ownership of a6a86.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGpi../4c37a.. ownership of ab349.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFXU../882e3.. ownership of 45c1b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW9P../99f57.. ownership of c4c3f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFmq../7ff53.. ownership of 726e4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQhW../371c3.. ownership of 5c45e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLrj../fa53b.. ownership of 50937.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRLF../e9934.. ownership of 50544.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLF9../91c9b.. ownership of ce9f4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbox../a97c5.. ownership of 7151b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLiY../5fa82.. ownership of 4b311.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZH7../fda26.. ownership of 830d9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGUT../58f6d.. ownership of bd517.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVy5../fccd5.. ownership of 8e731.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK2h../216d7.. ownership of 32c7c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUzP../2eb57.. ownership of a42cd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMLN../01788.. ownership of ec111.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWDk../16f81.. ownership of f49c7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVrG../11cfd.. ownership of b610d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdzc../566c8.. ownership of 26ca5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN6c../081d2.. ownership of c7d1f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT5E../ba72f.. ownership of 7aedb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUNqw../7d949.. doc published by PrGxv..
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Param d2155.. : ι → (ι → ι → ο) → ι
Param 1216a.. : ι → (ι → ο) → ι
Definition c7d1f.. := λ 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) 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 1c95b.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x0 = c7d1f.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem e05f5.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . x0 = f482f.. (c7d1f.. 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 4a2a6.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x0 = c7d1f.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x6 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 (proof)
Theorem be277.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ x1 x5 = f482f.. (f482f.. (c7d1f.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 (proof)
Param 2b2e3.. : ι → ι → ι → ο
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
Known 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ 2b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3
Theorem 73165.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x0 = c7d1f.. 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 c5a21.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = 2b2e3.. (f482f.. (c7d1f.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (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 26d45.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x0 = c7d1f.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem 1f38c.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ x3 x5 = decode_p (f482f.. (c7d1f.. 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 bd863.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x0 = c7d1f.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 9cd02.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . x4 = f482f.. (c7d1f.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (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 56b30.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ο . ∀ x6 x7 : ι → ο . ∀ x8 x9 . c7d1f.. x0 x2 x4 x6 x8 = c7d1f.. 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)) (x8 = x9) (proof)
Param iff : ο → ο → ο
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
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
Known 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2
Theorem fe636.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . ∀ x7 . (∀ x8 . prim1 x8 x0 ⟶ x1 x8 = x2 x8) ⟶ (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ iff (x3 x8 x9) (x4 x8 x9)) ⟶ (∀ x8 . prim1 x8 x0 ⟶ iff (x5 x8) (x6 x8)) ⟶ c7d1f.. x0 x1 x3 x5 x7 = c7d1f.. x0 x2 x4 x6 x7 (proof)
Definition b610d.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . ∀ x6 . prim1 x6 x2 ⟶ x1 (c7d1f.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem f2018.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ b610d.. (c7d1f.. x0 x1 x2 x3 x4) (proof)
Theorem c30a4.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . b610d.. (c7d1f.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x1 x5) x0 (proof)
Theorem cb18b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . b610d.. (c7d1f.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem 7c672.. : ∀ x0 . b610d.. x0 ⟶ x0 = c7d1f.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition ec111.. := λ 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..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 2f87c.. : ∀ 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)) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ ec111.. (c7d1f.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 32c7c.. := λ 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..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem b2ef3.. : ∀ 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)) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ 32c7c.. (c7d1f.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition bd517.. := λ 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..))) x3 x4))))
Theorem 0b229.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x0 = bd517.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 77703.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . x0 = f482f.. (bd517.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem c7fd3.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x0 = bd517.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x6 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 (proof)
Theorem 8cd35.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ x1 x5 = f482f.. (f482f.. (bd517.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 1348b.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x0 = bd517.. 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 71c9c.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = 2b2e3.. (f482f.. (bd517.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 4c95d.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x0 = bd517.. x1 x2 x3 x4 x5 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 0f14e.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . x3 = f482f.. (bd517.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 71b43.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x0 = bd517.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem c5ea1.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . x4 = f482f.. (bd517.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem cdba3.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ο . ∀ x6 x7 x8 x9 . bd517.. x0 x2 x4 x6 x8 = bd517.. 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)) (x6 = x7)) (x8 = x9) (proof)
Theorem 1fd36.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 x6 . (∀ x7 . prim1 x7 x0 ⟶ x1 x7 = x2 x7) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x3 x7 x8) (x4 x7 x8)) ⟶ bd517.. x0 x1 x3 x5 x6 = bd517.. x0 x2 x4 x5 x6 (proof)
Definition 4b311.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ι → ο . ∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ x1 (bd517.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem a0b68.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ 4b311.. (bd517.. x0 x1 x2 x3 x4) (proof)
Theorem ea18c.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . 4b311.. (bd517.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x1 x5) x0 (proof)
Theorem 29640.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . 4b311.. (bd517.. x0 x1 x2 x3 x4) ⟶ prim1 x3 x0 (proof)
Theorem b4986.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . 4b311.. (bd517.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem c03b4.. : ∀ x0 . 4b311.. x0 ⟶ x0 = bd517.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition ce9f4.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι → ο) → ι → ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 7b9b4.. : ∀ 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)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ ce9f4.. (bd517.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 50937.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι → ο) → ι → ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 49059.. : ∀ 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)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ 50937.. (bd517.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 726e4.. := λ 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..)) (1216a.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))
Theorem 9205a.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . x0 = 726e4.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem e2946.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . x0 = f482f.. (726e4.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem 90bdf.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . x0 = 726e4.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x6 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 (proof)
Theorem 44359.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ x1 x5 = f482f.. (f482f.. (726e4.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 54141.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . x0 = 726e4.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 (proof)
Theorem 62515.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ x2 x5 = decode_p (f482f.. (726e4.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem 30331.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . x0 = 726e4.. x1 x2 x3 x4 x5 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 1741e.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . x3 = f482f.. (726e4.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 5c572.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . x0 = 726e4.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem fa56b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . x4 = f482f.. (726e4.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 9df7f.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ο . ∀ x6 x7 x8 x9 . 726e4.. x0 x2 x4 x6 x8 = 726e4.. 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 6bcf3.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 x6 . (∀ x7 . prim1 x7 x0 ⟶ x1 x7 = x2 x7) ⟶ (∀ x7 . prim1 x7 x0 ⟶ iff (x3 x7) (x4 x7)) ⟶ 726e4.. x0 x1 x3 x5 x6 = 726e4.. x0 x2 x4 x5 x6 (proof)
Definition 45c1b.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ x1 (726e4.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 5f7bc.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ 45c1b.. (726e4.. x0 x1 x2 x3 x4) (proof)
Theorem 4d8d1.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . 45c1b.. (726e4.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x1 x5) x0 (proof)
Theorem 6b740.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . 45c1b.. (726e4.. x0 x1 x2 x3 x4) ⟶ prim1 x3 x0 (proof)
Theorem 34ab5.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . 45c1b.. (726e4.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem fff31.. : ∀ x0 . 45c1b.. x0 ⟶ x0 = 726e4.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition a6a86.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ο) → ι → ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 1f7f5.. : ∀ x0 : ι → (ι → ι) → (ι → ο) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . (∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x3 x8) (x7 x8)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ a6a86.. (726e4.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition da128.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ο) → ι → ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem de93d.. : ∀ x0 : ι → (ι → ι) → (ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . (∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x2 x7 = x6 x7) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x3 x8) (x7 x8)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ da128.. (726e4.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 918ae.. := λ x0 . λ x1 x2 : ι → ι → ο . λ x3 x4 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (d2155.. 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 b2354.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . x0 = 918ae.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 0c8ea.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . x0 = f482f.. (918ae.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem ad372.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . x0 = 918ae.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem 9c2c2.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = 2b2e3.. (f482f.. (918ae.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 42853.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . x0 = 918ae.. 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 8c63b.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = 2b2e3.. (f482f.. (918ae.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 5b026.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . x0 = 918ae.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem 96786.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x3 x5 = decode_p (f482f.. (918ae.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem 27c75.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . x0 = 918ae.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x5 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 (proof)
Theorem ad833.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x4 x5 = decode_p (f482f.. (918ae.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 (proof)
Theorem 98f19.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ο . ∀ x6 x7 x8 x9 : ι → ο . 918ae.. x0 x2 x4 x6 x8 = 918ae.. x1 x3 x5 x7 x9 ⟶ and (and (and (and (x0 = x1) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x2 x10 x11 = x3 x10 x11)) (∀ 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)
Theorem 55882.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . ∀ x5 x6 x7 x8 : ι → ο . (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ iff (x1 x9 x10) (x2 x9 x10)) ⟶ (∀ 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)) ⟶ 918ae.. x0 x1 x3 x5 x7 = 918ae.. x0 x2 x4 x6 x8 (proof)
Definition 8617f.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . x1 (918ae.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem a6584.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . 8617f.. (918ae.. x0 x1 x2 x3 x4) (proof)
Theorem 77020.. : ∀ x0 . 8617f.. x0 ⟶ x0 = 918ae.. (f482f.. x0 4a7ef..) (2b2e3.. (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 abb35.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (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 2ec61.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → (ι → ο) → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . (∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x2 x7 x8) (x6 x7 x8)) ⟶ ∀ 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) ⟶ abb35.. (918ae.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 7f9b4.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (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 19a2d.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . (∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x2 x7 x8) (x6 x7 x8)) ⟶ ∀ 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) ⟶ 7f9b4.. (918ae.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)