Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrLUy../596c6..
PULx7../3f834..
vout
PrLUy../d9bed.. 24.98 bars
TMYag../e38a1.. ownership of 4d242.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTNe../58e3c.. ownership of e788d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPGN../c55d8.. ownership of b7c2b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcGH../853b8.. ownership of 3caff.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGrU../c9211.. ownership of 84780.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRwz../1fcde.. ownership of 04518.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVZo../14524.. ownership of b737f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbJx../86426.. ownership of 9a883.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMazn../e3f49.. ownership of 6fd41.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFWg../67d3a.. ownership of 7cc5f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbXU../21d01.. ownership of a923f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdDZ../36d01.. ownership of c7971.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEhd../24693.. ownership of 1905b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLWs../a2fe6.. ownership of 63430.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSyW../0d79d.. ownership of 77b5c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdLr../94668.. ownership of e8cee.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQxJ../dfca5.. ownership of 81909.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHZu../cd43d.. ownership of 70d18.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQxC../9c8ee.. ownership of 33194.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQYt../5174f.. ownership of f61d3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF2j../c879c.. ownership of 32da5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN5U../b2581.. ownership of 533f7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXwa../a2489.. ownership of 9593f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPLo../eb11a.. ownership of 717c3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRFp../23d06.. ownership of d50a8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVAX../0fbd4.. ownership of 96f5d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSY8../08ee7.. ownership of a8a71.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGHm../d0b54.. ownership of 02057.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSo7../35522.. ownership of cd879.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPi8../f3932.. ownership of 67d30.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSkN../2893b.. ownership of 55b3b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGXv../f9ea3.. ownership of b5795.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbAe../59ad6.. ownership of 5b912.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdjU../d2278.. ownership of 21a5e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYdc../c18a9.. ownership of 9e865.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNU5../d4a2d.. ownership of eabed.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSrD../cdc35.. ownership of 4f172.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJVk../51df0.. ownership of 7e054.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX9M../eacb7.. ownership of cf9f4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaUj../cbdc3.. ownership of 77628.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHD6../23aa5.. ownership of e3d85.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHy9../ab913.. ownership of d94c6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaSc../6f323.. ownership of f6d57.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaYE../b6152.. ownership of a33f1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGWR../50d46.. ownership of 9407e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS5C../7c5e0.. ownership of b5968.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGey../fa3cb.. ownership of 81905.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWGD../d8825.. ownership of bdc8b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWZw../e3076.. ownership of e4e04.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNFR../d9a37.. ownership of ad799.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT9x../2e46b.. ownership of 813a6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQnc../d535c.. ownership of 2bf73.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXL1../a9ace.. ownership of 3d485.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaqs../2f39d.. ownership of 65083.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPWd../db6eb.. ownership of cdfe8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRF2../6bd8e.. ownership of 820bb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPzN../6c741.. ownership of a65e1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd6h../7e602.. ownership of 8ce88.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMawX../6225c.. ownership of fb2a2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNfz../bb6ed.. ownership of c1ac9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ8e../7e3f0.. ownership of 5546a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPyg../198f1.. ownership of dfd52.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFsU../4efdd.. ownership of 08625.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYXs../59fba.. ownership of f9ab7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY8M../614c9.. ownership of 9b51e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVZa../e1621.. ownership of c7158.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYqE../5886b.. ownership of e7638.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPkp../28609.. ownership of d3016.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZYB../1203f.. ownership of 3f319.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKv9../c2f46.. ownership of 0a87a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWvz../3e053.. ownership of 40dbf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYqg../f24f3.. ownership of 9cdbb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQN1../67a92.. ownership of 1cc79.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZuL../e33eb.. ownership of e1dc6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGLJ../44d9e.. ownership of e7406.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaJJ../7ae7e.. ownership of 99c4e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR13../57ebd.. ownership of 930cc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTPS../3ca34.. ownership of 736fc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXof../62257.. ownership of 7edfd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRXY../360af.. ownership of 439d3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMavo../5daab.. ownership of 55142.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY7Z../d3b34.. ownership of 04d1f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGua../6c060.. ownership of 84da4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKiw../7452f.. ownership of cfcea.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML5s../2fcce.. ownership of 1058f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKYL../168e3.. ownership of 1ce5f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPm1../12909.. ownership of 2fe9f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKeq../80a22.. ownership of 984bf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXor../12db1.. ownership of e6222.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYGD../2ac5a.. ownership of c63c6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMMc../f1340.. ownership of ea292.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKMc../2dfc9.. ownership of 2ef8d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWdM../d9622.. ownership of abcfe.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKDR../68bb2.. ownership of 219e2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYMb../e5fa9.. ownership of 1cb3e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJto../f9173.. ownership of 41bee.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMViQ../61eb0.. ownership of 91c59.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY4y../40e15.. ownership of aaaa9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc7H../7b722.. ownership of 85124.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcrs../871e5.. ownership of 64e46.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML3V../b6305.. ownership of ab871.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSVZ../2998b.. ownership of 81bf0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMStd../38362.. ownership of 61575.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRD6../c701d.. ownership of e5de0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcDW../b97e7.. ownership of ca791.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRpn../709ba.. ownership of c3e0f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdwB../a8bd3.. ownership of 73df7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXj2../fe897.. ownership of 96e32.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRME../25518.. ownership of a2508.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXGw../3a17e.. ownership of fd2f7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS8X../3809d.. ownership of cfdeb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbg2../c1646.. ownership of 0a760.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYAX../4356b.. ownership of ba422.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSu5../32ffa.. ownership of 31b18.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMRD../fb895.. ownership of 2ed2d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZRD../2f3e7.. ownership of 8d38a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMov../5d094.. ownership of 6c21e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVoc../9f4a2.. ownership of 7f09f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT4o../fa401.. ownership of aca4e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSvs../ede5a.. ownership of 4f96a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYBe../31613.. ownership of e3173.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb9a../51608.. ownership of ab45b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb6Z../ecc30.. ownership of 313db.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXTX../e5f5c.. ownership of 3f2cb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRne../19994.. ownership of 81c5c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPu4../9d3d0.. ownership of f380b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRjL../933f6.. ownership of 983e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMhZ../ffc67.. ownership of 7a35e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbnr../db9f3.. ownership of 9942f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRDz../20d7f.. ownership of a7e7d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNmR../7d622.. ownership of 82755.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKc3../af60d.. ownership of 332b8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNV6../f4cb9.. ownership of 39ea5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGxK../d02f9.. ownership of a80a4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJh6../80272.. ownership of 951c5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFRt../5ccb5.. ownership of d7fd6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFFR../093ca.. ownership of 0dd1a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNzw../65869.. ownership of 78c0a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZfG../8a090.. ownership of d358e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUZ4../944cb.. ownership of 296e2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFmX../3de5e.. ownership of 6257c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa7w../bc35e.. ownership of 63b4d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH6A../c4cf8.. ownership of 78c97.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb1Y../620a5.. ownership of a2571.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKHH../d0e0d.. ownership of 81ecf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXrs../86f1e.. ownership of ac290.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK9p../880f9.. ownership of 12fdb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKRi../c19b8.. ownership of 991b7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc3v../772cc.. ownership of 16c83.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMddG../e0137.. ownership of 17625.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHL2../9500b.. ownership of e925d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPWm../2a23d.. ownership of 3202d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKYQ../6d38a.. ownership of c1934.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcaK../bef71.. ownership of 2501e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPPj../da158.. ownership of b089b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQQr../e7f96.. ownership of 3ca5d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQD3../c588f.. ownership of a599b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbDc../7dc82.. ownership of 7fa6c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHdc../d6843.. ownership of fc4dd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHWa../57882.. ownership of 7da8a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVnz../3ad41.. ownership of 87e55.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFJY../d7dca.. ownership of 9b00b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWTh../8cb3c.. ownership of 430d6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb4G../624bf.. ownership of 698ce.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUnd../56faf.. ownership of 9f84a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaEN../e9c1e.. ownership of fe64d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPZ6../9ce60.. ownership of 3b083.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJxU../e0e39.. ownership of df434.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaF2../9aa35.. ownership of 9d885.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMBj../f2968.. ownership of 73cfe.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbJV../b2f32.. ownership of 74b16.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUkv../d5f63.. ownership of cb43b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLGp../11dda.. ownership of 8e582.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYQJ../2a81d.. ownership of 58bb1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJDV../bb82a.. ownership of 352ba.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT8n../ae1f9.. ownership of 3759d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRz6../631f4.. ownership of 3e570.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUzA../68fa4.. ownership of a2f61.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMam2../65520.. ownership of 7e4ad.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaUy../00293.. ownership of fc3f0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdB8../748d8.. ownership of 6640c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSQS../54ab8.. ownership of cbf25.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUctR../c0915.. doc published by PrGxv..
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Param eb53d.. : ι → CT2 ι
Definition 6640c.. := λ 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..)) (eb53d.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (0fc90.. 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 16c83.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 . x0 = 6640c.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 12fdb.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 . x0 = f482f.. (6640c.. 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 81ecf.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 . x0 = 6640c.. 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 78c97.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (6640c.. 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
Theorem 6257c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 . x0 = 6640c.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 x7 (proof)
Theorem d358e.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = e3162.. (f482f.. (6640c.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
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 f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem 0dd1a.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 . x0 = 6640c.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem 951c5.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 . prim1 x5 x0 ⟶ x3 x5 = f482f.. (f482f.. (6640c.. 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 39ea5.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 . x0 = 6640c.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 82755.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 . x4 = f482f.. (6640c.. 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 9942f.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 : ι → ι . ∀ x8 x9 . 6640c.. x0 x2 x4 x6 x8 = 6640c.. 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)) (x8 = x9) (proof)
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 983e3.. : ∀ 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 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x3 x8 x9 = x4 x8 x9) ⟶ (∀ x8 . prim1 x8 x0 ⟶ x5 x8 = x6 x8) ⟶ 6640c.. x0 x1 x3 x5 x7 = 6640c.. x0 x2 x4 x6 x7 (proof)
Definition 7e4ad.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ prim1 (x4 x5 x6) x2) ⟶ ∀ x5 : ι → ι . (∀ x6 . prim1 x6 x2 ⟶ prim1 (x5 x6) x2) ⟶ ∀ x6 . prim1 x6 x2 ⟶ x1 (6640c.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 81c5c.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x3 x4) x0) ⟶ ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x0 ⟶ prim1 (x3 x4) x0) ⟶ ∀ x4 . prim1 x4 x0 ⟶ 7e4ad.. (6640c.. x0 x1 x2 x3 x4) (proof)
Theorem 313db.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 . 7e4ad.. (6640c.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem e3173.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 . 7e4ad.. (6640c.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x2 x5 x6) x0 (proof)
Theorem aca4e.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 . 7e4ad.. (6640c.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x3 x5) x0 (proof)
Theorem 6c21e.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 . 7e4ad.. (6640c.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem 2ed2d.. : ∀ x0 . 7e4ad.. x0 ⟶ x0 = 6640c.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 3e570.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → ι → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem ba422.. : ∀ 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 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι . (∀ x9 . prim1 x9 x1 ⟶ x4 x9 = x8 x9) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ 3e570.. (6640c.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 352ba.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → ι → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem cfdeb.. : ∀ 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 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι . (∀ x9 . prim1 x9 x1 ⟶ x4 x9 = x8 x9) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ 352ba.. (6640c.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Param d2155.. : ι → (ι → ι → ο) → ι
Definition 8e582.. := λ 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..)) (eb53d.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (d2155.. x0 x3) (d2155.. x0 x4)))))
Theorem a2508.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι → ο . x0 = 8e582.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 73df7.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 x5 : ι → ι → ο . x5 x0 (f482f.. (8e582.. x0 x1 x2 x3 x4) 4a7ef..) ⟶ x5 (f482f.. (8e582.. x0 x1 x2 x3 x4) 4a7ef..) x0 (proof)
Theorem ca791.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι → ο . x0 = 8e582.. 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 61575.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (8e582.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem ab871.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι → ο . x0 = 8e582.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 x7 (proof)
Theorem 85124.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = e3162.. (f482f.. (8e582.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (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 91c59.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι → ο . x0 = 8e582.. 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 1cb3e.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 x6 = 2b2e3.. (f482f.. (8e582.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 x6 (proof)
Theorem abcfe.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι → ο . x0 = 8e582.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x5 x6 x7 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 x7 (proof)
Theorem ea292.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x4 x5 x6 = 2b2e3.. (f482f.. (8e582.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6 (proof)
Theorem e6222.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 x8 x9 : ι → ι → ο . 8e582.. x0 x2 x4 x6 x8 = 8e582.. 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 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x6 x10 x11 = x7 x10 x11)) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x8 x10 x11 = x9 x10 x11) (proof)
Param iff : ο → ο → ο
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 2fe9f.. : ∀ 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 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x3 x9 x10 = x4 x9 x10) ⟶ (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ iff (x5 x9 x10) (x6 x9 x10)) ⟶ (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ iff (x7 x9 x10) (x8 x9 x10)) ⟶ 8e582.. x0 x1 x3 x5 x7 = 8e582.. x0 x2 x4 x6 x8 (proof)
Definition 74b16.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ prim1 (x4 x5 x6) x2) ⟶ ∀ x5 x6 : ι → ι → ο . x1 (8e582.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 1058f.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x3 x4) x0) ⟶ ∀ x3 x4 : ι → ι → ο . 74b16.. (8e582.. x0 x1 x2 x3 x4) (proof)
Theorem 84da4.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι → ο . 74b16.. (8e582.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem 55142.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι → ο . 74b16.. (8e582.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x2 x5 x6) x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem 7edfd.. : ∀ x0 . 74b16.. x0 ⟶ x0 = 8e582.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Definition 9d885.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → (ι → ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem 930cc.. : ∀ 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 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι → ο . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ iff (x4 x9 x10) (x8 x9 x10)) ⟶ ∀ x9 : ι → ι → ο . (∀ x10 . prim1 x10 x1 ⟶ ∀ x11 . prim1 x11 x1 ⟶ iff (x5 x10 x11) (x9 x10 x11)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ 9d885.. (8e582.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 3b083.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → (ι → ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem e7406.. : ∀ 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 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι → ο . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ iff (x4 x9 x10) (x8 x9 x10)) ⟶ ∀ x9 : ι → ι → ο . (∀ x10 . prim1 x10 x1 ⟶ ∀ x11 . prim1 x11 x1 ⟶ iff (x5 x10 x11) (x9 x10 x11)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ 3b083.. (8e582.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Param 1216a.. : ι → (ι → ο) → ι
Definition 9f84a.. := λ 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..)) (eb53d.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (d2155.. x0 x3) (1216a.. x0 x4)))))
Theorem 1cc79.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = 9f84a.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 40dbf.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = f482f.. (9f84a.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem 3f319.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = 9f84a.. 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 e7638.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (9f84a.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 9b51e.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = 9f84a.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 x7 (proof)
Theorem 08625.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = e3162.. (f482f.. (9f84a.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 5546a.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = 9f84a.. 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 fb2a2.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 x6 = 2b2e3.. (f482f.. (9f84a.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 x6 (proof)
Param decode_p : ι → ι → ο
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem a65e1.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x0 = 9f84a.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x5 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 (proof)
Theorem cdfe8.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x4 x5 = decode_p (f482f.. (9f84a.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 (proof)
Theorem 3d485.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 : ι → ι → ο . ∀ x8 x9 : ι → ο . 9f84a.. x0 x2 x4 x6 x8 = 9f84a.. 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 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x6 x10 x11 = x7 x10 x11)) (∀ x10 . prim1 x10 x0 ⟶ x8 x10 = x9 x10) (proof)
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
Theorem 813a6.. : ∀ 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 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x3 x9 x10 = x4 x9 x10) ⟶ (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ iff (x5 x9 x10) (x6 x9 x10)) ⟶ (∀ x9 . prim1 x9 x0 ⟶ iff (x7 x9) (x8 x9)) ⟶ 9f84a.. x0 x1 x3 x5 x7 = 9f84a.. x0 x2 x4 x6 x8 (proof)
Definition 430d6.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ prim1 (x4 x5 x6) x2) ⟶ ∀ x5 : ι → ι → ο . ∀ x6 : ι → ο . x1 (9f84a.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem e4e04.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x3 x4) x0) ⟶ ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . 430d6.. (9f84a.. x0 x1 x2 x3 x4) (proof)
Theorem 81905.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . 430d6.. (9f84a.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem 9407e.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . 430d6.. (9f84a.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x2 x5 x6) x0 (proof)
Theorem f6d57.. : ∀ x0 . 430d6.. x0 ⟶ x0 = 9f84a.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Definition 87e55.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem e3d85.. : ∀ 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 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ 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) ⟶ 87e55.. (9f84a.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition fc4dd.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem cf9f4.. : ∀ 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 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ 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) ⟶ fc4dd.. (9f84a.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition a599b.. := λ 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..)) (eb53d.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (d2155.. x0 x3) x4))))
Theorem 4f172.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = a599b.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 9e865.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = f482f.. (a599b.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem 5b912.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = a599b.. 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 55b3b.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (a599b.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem cd879.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = a599b.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 x7 (proof)
Theorem a8a71.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = e3162.. (f482f.. (a599b.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem d50a8.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = a599b.. 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 9593f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 x6 = 2b2e3.. (f482f.. (a599b.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 x6 (proof)
Theorem 32da5.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . x0 = a599b.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 33194.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x4 = f482f.. (a599b.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 81909.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 : ι → ι → ο . ∀ x8 x9 . a599b.. x0 x2 x4 x6 x8 = a599b.. 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 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x6 x10 x11 = x7 x10 x11)) (x8 = x9) (proof)
Theorem 77b5c.. : ∀ 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 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x3 x8 x9 = x4 x8 x9) ⟶ (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ iff (x5 x8 x9) (x6 x8 x9)) ⟶ a599b.. x0 x1 x3 x5 x7 = a599b.. x0 x2 x4 x6 x7 (proof)
Definition b089b.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ prim1 (x4 x5 x6) x2) ⟶ ∀ x5 : ι → ι → ο . ∀ x6 . prim1 x6 x2 ⟶ x1 (a599b.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 1905b.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x3 x4) x0) ⟶ ∀ x3 : ι → ι → ο . ∀ x4 . prim1 x4 x0 ⟶ b089b.. (a599b.. x0 x1 x2 x3 x4) (proof)
Theorem a923f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . b089b.. (a599b.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem 6fd41.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . b089b.. (a599b.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x2 x5 x6) x0 (proof)
Theorem b737f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . b089b.. (a599b.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem 84780.. : ∀ x0 . b089b.. x0 ⟶ x0 = a599b.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition c1934.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem b7c2b.. : ∀ 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 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ 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) ⟶ c1934.. (a599b.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition e925d.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 4d242.. : ∀ 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 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ 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) ⟶ e925d.. (a599b.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)