Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrMRX../794b7..
PUTzt../cb5cc..
vout
PrMRX../f99e3.. 24.98 bars
TMaic../c4aff.. ownership of 79059.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMjT../7903a.. ownership of d06ef.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPA6../b2019.. ownership of 9ad6c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcCC../af78e.. ownership of a991b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLKm../fded9.. ownership of d65e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK9V../de19a.. ownership of 21aac.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQfm../d4a58.. ownership of 67160.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZtb../aa562.. ownership of 05900.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJuh../b2a88.. ownership of e089c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN5w../bd4f2.. ownership of 0e25b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS3x../e4bdb.. ownership of 9b13b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdLQ../cb9ad.. ownership of 08d42.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcnK../4d44a.. ownership of eae4e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQKF../4ced6.. ownership of 1f4a1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKZk../a63c6.. ownership of 0ff82.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ6X../7e1d1.. ownership of 1f3d8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKKA../ca79a.. ownership of 15b36.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMpG../dea0e.. ownership of c1a9a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQTz../2126c.. ownership of 6afc8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcQm../d160e.. ownership of f9fc7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGsR../7d3d2.. ownership of 8dfed.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKfV../537a9.. ownership of 2fa88.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLJc../643be.. ownership of 41c5f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJMx../8f200.. ownership of 06b37.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdaY../b6c05.. ownership of 34be5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLt7../17b45.. ownership of f3e7e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWxT../b3817.. ownership of 7f647.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbmH../21a3d.. ownership of 4ad32.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVFv../c2bff.. ownership of e3ab5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQUQ../20d01.. ownership of e4576.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZmY../773e7.. ownership of 6599d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHcK../63193.. ownership of d2b3d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY4h../7d875.. ownership of 31265.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSJt../4278d.. ownership of 1a88e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdsr../27aab.. ownership of 186c4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF6Y../c2aa0.. ownership of c6595.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcs8../7e75d.. ownership of 6279e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWrY../beabf.. ownership of 229c6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRRt../ea227.. ownership of f8613.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSaz../bcba0.. ownership of c03c7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGjw../a24f7.. ownership of 25b04.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ2K../909ae.. ownership of 725a9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNQ6../bbc89.. ownership of d6079.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFzu../d705f.. ownership of 1e94f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ6H../4d67b.. ownership of e5c90.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbH4../09920.. ownership of b7d25.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFp2../a35e2.. ownership of 48f0e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ4G../dd071.. ownership of 15fd4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdjh../f79d0.. ownership of c3e6a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHaJ../2b869.. ownership of 4db2e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLpd../7c670.. ownership of 89ca8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMXs../ec46d.. ownership of af12a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKRS../88129.. ownership of ccfc9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWpa../25e51.. ownership of 9a81a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbYb../44b47.. ownership of 56e05.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW2E../160c9.. ownership of 1805d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMafQ../dc5a2.. ownership of cb282.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRrB../b7250.. ownership of 65e19.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ8r../83fbe.. ownership of 2e910.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbCh../0ecb8.. ownership of cbd33.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdRw../903e1.. ownership of 70d69.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMzg../458f6.. ownership of 604c0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYv7../86d11.. ownership of d7dfb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFGW../f8749.. ownership of 18b49.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRpE../246d8.. ownership of e27b3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaDg../4b0a6.. ownership of 8ced3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEsm../3838a.. ownership of 4d5a3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXTQ../1ceaf.. ownership of b300d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFiJ../205e1.. ownership of 2a955.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPYJ../22987.. ownership of faa9c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWqb../0d940.. ownership of 8c147.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbUH../15774.. ownership of 59cba.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJN8../28035.. ownership of 3d367.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTFV../496af.. ownership of d90e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF9T../856ac.. ownership of 859d3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWM8../eea82.. ownership of 78962.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRhi../ec035.. ownership of 3caf0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMahE../323da.. ownership of aa528.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFFZ../291f6.. ownership of 62ebe.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGeV../4e4e9.. ownership of c573c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY1v../f7658.. ownership of 6910c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMStJ../1968a.. ownership of 0317e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQpr../873ea.. ownership of 7dc73.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMve../19b9f.. ownership of db0b8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGA7../b1fef.. ownership of 8fb94.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTsM../e370b.. ownership of 804ed.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYRQ../fc644.. ownership of a5ddf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLBH../01d88.. ownership of 6bc04.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP4F../1d906.. ownership of 9932c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdzi../65afb.. ownership of 2412c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKre../43c20.. ownership of 3d606.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU57../dde6c.. ownership of a6ee9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdNd../eac1c.. ownership of 53091.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMot../e05e9.. ownership of 17176.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHF2../62b1b.. ownership of 3b2a8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWpH../7172e.. ownership of 65d55.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX6A../1a8fe.. ownership of bb0e1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKaK../c1aeb.. ownership of 5c8b2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM53../98d1d.. ownership of f4d0e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVma../db1ce.. ownership of 02a65.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaNp../2a90b.. ownership of 3bdd0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRKV../679ea.. ownership of 7e0a7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLwG../52c61.. ownership of 979e8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGcv../49d27.. ownership of d9be0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLdk../ae622.. ownership of b870e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLtj../981f2.. ownership of 9a574.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHpC../a6e0d.. ownership of 8c059.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLS5../82c3c.. ownership of 44675.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM1U../1d7bd.. ownership of a8821.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUHR../a8d2d.. ownership of 65b81.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdkh../7602e.. ownership of b9a9a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa7T../bdf5c.. ownership of 4ed17.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGVu../3aa42.. ownership of c60c1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHhK../67a28.. ownership of 23303.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKZD../88419.. ownership of 05b10.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRNR../108ea.. ownership of 4662e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHqW../95eea.. ownership of 0bf9e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZAF../ef194.. ownership of af1f8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH4C../be68c.. ownership of 79cfc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXNa../62e2c.. ownership of 865ea.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTfm../9f1dc.. ownership of dac0d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQtr../39227.. ownership of 01bc6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUhZ../e0447.. ownership of 1f288.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHBc../fff7d.. ownership of b7a69.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHQf../afd9b.. ownership of b3ae1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRfE../329eb.. ownership of ea347.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQyG../0e78a.. ownership of 6d916.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHGH../6b52c.. ownership of 10c58.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKHq../4b414.. ownership of 0702c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXyP../81853.. ownership of ce569.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdBQ../2b303.. ownership of efb24.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRzj../27636.. ownership of ba4f3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXes../bdd47.. ownership of c7688.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWyC../e0036.. ownership of 76da7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFp7../abcac.. ownership of 73318.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRVZ../fe9d6.. ownership of da4ae.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcwk../1d06c.. ownership of 4c7ff.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdZx../1efe5.. ownership of 0fe11.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWcz../c77d3.. ownership of be998.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUND../55b12.. ownership of 37f1a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdxh../ca435.. ownership of 3e80b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKSm../ab557.. ownership of 77127.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPtD../ea43d.. ownership of e10c2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWKe../a44f9.. ownership of 299f0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYms../61b5b.. ownership of 968d9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUyP../716f8.. ownership of c2c40.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNMy../2469d.. ownership of 52c69.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJJc../e003a.. ownership of 2fbc2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcmc../03651.. ownership of 4e949.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc95../9699d.. ownership of a58c6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNaW../94459.. ownership of dc25a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGQ4../545a1.. ownership of 2612b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWM2../c69d1.. ownership of 78340.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJJH../1fd32.. ownership of 8d3c0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN6N../896da.. ownership of ae96b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdvm../81e09.. ownership of 43cde.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc3z../85494.. ownership of 90bb8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPDk../5b6d8.. ownership of 0d241.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG6A../08cab.. ownership of 3c4da.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc5U../d0f8a.. ownership of cc053.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFbW../8ee5d.. ownership of 303f6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFkx../72145.. ownership of 9bcb6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVch../6ea6a.. ownership of 3da2d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbTP../917fd.. ownership of 13236.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXZe../b5e23.. ownership of a7b1c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRJt../5c94a.. ownership of 6553e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNz9../ccf06.. ownership of 02c31.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTJj../66720.. ownership of 03303.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSA3../c3c13.. ownership of 86731.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLQt../be9de.. ownership of e90b8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd6s../7b261.. ownership of 03f8d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVPu../3b524.. ownership of 8b288.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZQ2../8963a.. ownership of 1f33c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT9k../3e448.. ownership of adbf3.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZbr../7b5c6.. ownership of 86570.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGtc../742e7.. ownership of 1f551.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJJv../a9394.. ownership of 0ee3a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbPH../72d60.. ownership of cff3d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaB1../d5faf.. ownership of b3c00.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYAv../86e06.. ownership of 4e01d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUbdK../56c41.. doc published by PrGxv..
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Param eb53d.. : ι → CT2 ι
Param d2155.. : ι → (ι → ι → ο) → ι
Param 1216a.. : ι → (ι → ο) → ι
Definition b3c00.. := λ x0 . λ x1 : ι → ι → ι . λ x2 : ι → ι . λ x3 : ι → ι → ο . λ x4 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (d2155.. 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 52c69.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = b3c00.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 968d9.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = f482f.. (b3c00.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Param e3162.. : ι → ι → ι → ι
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 35054.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ e3162.. (eb53d.. x0 x1) x2 x3 = x1 x2 x3
Theorem e10c2.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = b3c00.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem 3e80b.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (b3c00.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (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
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem be998.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = b3c00.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 (proof)
Theorem 4c7ff.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x2 x5 = f482f.. (f482f.. (b3c00.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Param 2b2e3.. : ι → ι → ι → ο
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 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ 2b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3
Theorem 73318.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = b3c00.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x4 x6 x7 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 x7 (proof)
Theorem c7688.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 x6 = 2b2e3.. (f482f.. (b3c00.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 x6 (proof)
Param decode_p : ι → ι → ο
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
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem efb24.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = b3c00.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x5 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 (proof)
Theorem 0702c.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x4 x5 = decode_p (f482f.. (b3c00.. 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 6d916.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . ∀ x6 x7 : ι → ι → ο . ∀ x8 x9 : ι → ο . b3c00.. x0 x2 x4 x6 x8 = b3c00.. 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 ⟶ x4 x10 = x5 x10)) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x6 x10 x11 = x7 x10 x11)) (∀ 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 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
Known 8fdaf.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ eb53d.. x0 x1 = eb53d.. x0 x2
Theorem b3ae1.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 x6 : ι → ι → ο . ∀ x7 x8 : ι → ο . (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x1 x9 x10 = x2 x9 x10) ⟶ (∀ x9 . prim1 x9 x0 ⟶ x3 x9 = x4 x9) ⟶ (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ iff (x5 x9 x10) (x6 x9 x10)) ⟶ (∀ x9 . prim1 x9 x0 ⟶ iff (x7 x9) (x8 x9)) ⟶ b3c00.. x0 x1 x3 x5 x7 = b3c00.. x0 x2 x4 x6 x8 (proof)
Definition 0ee3a.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ prim1 (x4 x5) x2) ⟶ ∀ x5 : ι → ι → ο . ∀ x6 : ι → ο . x1 (b3c00.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 1f288.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x0) ⟶ ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . 0ee3a.. (b3c00.. x0 x1 x2 x3 x4) (proof)
Theorem dac0d.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . 0ee3a.. (b3c00.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem 79cfc.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . 0ee3a.. (b3c00.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x2 x5) x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem 0bf9e.. : ∀ x0 . 0ee3a.. x0 ⟶ x0 = b3c00.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Definition 86570.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem 05b10.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → (ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ι → ο . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ iff (x4 x9 x10) (x8 x9 x10)) ⟶ ∀ x9 : ι → ο . (∀ x10 . prim1 x10 x1 ⟶ iff (x5 x10) (x9 x10)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ 86570.. (b3c00.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 1f33c.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem c60c1.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ι → ο . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ iff (x4 x9 x10) (x8 x9 x10)) ⟶ ∀ x9 : ι → ο . (∀ x10 . prim1 x10 x1 ⟶ iff (x5 x10) (x9 x10)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ 1f33c.. (b3c00.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 03f8d.. := λ x0 . λ x1 : ι → ι → ι . λ x2 : ι → ι . λ x3 : ι → ι → ο . λ x4 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (d2155.. x0 x3) x4))))
Theorem b9a9a.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = 03f8d.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem a8821.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = f482f.. (03f8d.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem 8c059.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = 03f8d.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem b870e.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (03f8d.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 979e8.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = 03f8d.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 (proof)
Theorem 3bdd0.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ x2 x5 = f482f.. (f482f.. (03f8d.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem f4d0e.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = 03f8d.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x4 x6 x7 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 x7 (proof)
Theorem bb0e1.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 x6 = 2b2e3.. (f482f.. (03f8d.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 x6 (proof)
Theorem 3b2a8.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = 03f8d.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 53091.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x4 = f482f.. (03f8d.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 3d606.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . ∀ x6 x7 : ι → ι → ο . ∀ x8 x9 . 03f8d.. x0 x2 x4 x6 x8 = 03f8d.. 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 ⟶ x4 x10 = x5 x10)) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x6 x10 x11 = x7 x10 x11)) (x8 = x9) (proof)
Theorem 9932c.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 x6 : ι → ι → ο . ∀ x7 . (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x1 x8 x9 = x2 x8 x9) ⟶ (∀ x8 . prim1 x8 x0 ⟶ x3 x8 = x4 x8) ⟶ (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ iff (x5 x8 x9) (x6 x8 x9)) ⟶ 03f8d.. x0 x1 x3 x5 x7 = 03f8d.. x0 x2 x4 x6 x7 (proof)
Definition 86731.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ prim1 (x4 x5) x2) ⟶ ∀ x5 : ι → ι → ο . ∀ x6 . prim1 x6 x2 ⟶ x1 (03f8d.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem a5ddf.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x0) ⟶ ∀ x3 : ι → ι → ο . ∀ x4 . prim1 x4 x0 ⟶ 86731.. (03f8d.. x0 x1 x2 x3 x4) (proof)
Theorem 8fb94.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . 86731.. (03f8d.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem 7dc73.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . 86731.. (03f8d.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x2 x5) x0 (proof)
Theorem 6910c.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . 86731.. (03f8d.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem 62ebe.. : ∀ x0 . 86731.. x0 ⟶ x0 = 03f8d.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 02c31.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 3caf0.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ι → ο . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ iff (x4 x9 x10) (x8 x9 x10)) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ 02c31.. (03f8d.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition a7b1c.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 859d3.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x3 x8 = x7 x8) ⟶ ∀ x8 : ι → ι → ο . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ iff (x4 x9 x10) (x8 x9 x10)) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ a7b1c.. (03f8d.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 3da2d.. := λ x0 . λ x1 : ι → ι → ι . λ x2 : ι → ι . λ x3 x4 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (1216a.. x0 x3) (1216a.. x0 x4)))))
Theorem 3d367.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = 3da2d.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 8c147.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . x0 = f482f.. (3da2d.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem 2a955.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = 3da2d.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem 4d5a3.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (3da2d.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem e27b3.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = 3da2d.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 (proof)
Theorem d7dfb.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x2 x5 = f482f.. (f482f.. (3da2d.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem 70d69.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = 3da2d.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem 2e910.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x3 x5 = decode_p (f482f.. (3da2d.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem cb282.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . x0 = 3da2d.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x5 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 (proof)
Theorem 56e05.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x4 x5 = decode_p (f482f.. (3da2d.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 (proof)
Theorem ccfc9.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . ∀ x6 x7 x8 x9 : ι → ο . 3da2d.. x0 x2 x4 x6 x8 = 3da2d.. 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 ⟶ x4 x10 = x5 x10)) (∀ x10 . prim1 x10 x0 ⟶ x6 x10 = x7 x10)) (∀ x10 . prim1 x10 x0 ⟶ x8 x10 = x9 x10) (proof)
Theorem 89ca8.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 x6 x7 x8 : ι → ο . (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x1 x9 x10 = x2 x9 x10) ⟶ (∀ 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)) ⟶ 3da2d.. x0 x1 x3 x5 x7 = 3da2d.. x0 x2 x4 x6 x8 (proof)
Definition 303f6.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ prim1 (x4 x5) x2) ⟶ ∀ x5 x6 : ι → ο . x1 (3da2d.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem c3e6a.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x0) ⟶ ∀ x3 x4 : ι → ο . 303f6.. (3da2d.. x0 x1 x2 x3 x4) (proof)
Theorem 48f0e.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . 303f6.. (3da2d.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem e5c90.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . 303f6.. (3da2d.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x2 x5) x0 (proof)
Theorem d6079.. : ∀ x0 . 303f6.. x0 ⟶ x0 = 3da2d.. (f482f.. x0 4a7ef..) (e3162.. (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 3c4da.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι) → (ι → ο) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (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 25b04.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι) → (ι → ο) → (ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ 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) ⟶ 3c4da.. (3da2d.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 90bb8.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι) → (ι → ο) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (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 f8613.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι) → (ι → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ 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) ⟶ 90bb8.. (3da2d.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition ae96b.. := λ x0 . λ x1 : ι → ι → ι . λ x2 : ι → ι . λ x3 : ι → ο . λ x4 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (1216a.. x0 x3) x4))))
Theorem 6279e.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = ae96b.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 186c4.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x0 = f482f.. (ae96b.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem 31265.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = ae96b.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem 6599d.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (ae96b.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem e3ab5.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = ae96b.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 (proof)
Theorem 7f647.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ x2 x5 = f482f.. (f482f.. (ae96b.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem 34be5.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = ae96b.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem 41c5f.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ x3 x5 = decode_p (f482f.. (ae96b.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem 8dfed.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . x0 = ae96b.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 6afc8.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x4 = f482f.. (ae96b.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 15b36.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . ∀ x6 x7 : ι → ο . ∀ x8 x9 . ae96b.. x0 x2 x4 x6 x8 = ae96b.. 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 ⟶ x4 x10 = x5 x10)) (∀ x10 . prim1 x10 x0 ⟶ x6 x10 = x7 x10)) (x8 = x9) (proof)
Theorem 0ff82.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 x6 : ι → ο . ∀ x7 . (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x1 x8 x9 = x2 x8 x9) ⟶ (∀ x8 . prim1 x8 x0 ⟶ x3 x8 = x4 x8) ⟶ (∀ x8 . prim1 x8 x0 ⟶ iff (x5 x8) (x6 x8)) ⟶ ae96b.. x0 x1 x3 x5 x7 = ae96b.. x0 x2 x4 x6 x7 (proof)
Definition 78340.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ prim1 (x4 x5) x2) ⟶ ∀ x5 : ι → ο . ∀ x6 . prim1 x6 x2 ⟶ x1 (ae96b.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem eae4e.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x0) ⟶ ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ 78340.. (ae96b.. x0 x1 x2 x3 x4) (proof)
Theorem 9b13b.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . 78340.. (ae96b.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem e089c.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . 78340.. (ae96b.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x2 x5) x0 (proof)
Theorem 67160.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . 78340.. (ae96b.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem d65e3.. : ∀ x0 . 78340.. x0 ⟶ x0 = ae96b.. (f482f.. x0 4a7ef..) (e3162.. (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 dc25a.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι) → (ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (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 9ad6c.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι) → (ι → ο) → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ 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) ⟶ dc25a.. (ae96b.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 4e949.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι) → (ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (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 79059.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι) → (ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ 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) ⟶ 4e949.. (ae96b.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)