Proofgold Signed Transaction

vin
PrEvg../2bf91.. PUco4../59c11..

vout

PrEvg../4ed13.. 0.26 bars
TMTLj../865e2.. ownership of 0b20d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPmi../f1382.. ownership of c0874.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTGr../431e6.. ownership of 7210f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUV9../d8095.. ownership of bb77f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZP1../0f151.. ownership of 7efe5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRCF../45d15.. ownership of 32648.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaEJ../c9c3a.. ownership of 8f88b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaio../4fc1d.. ownership of 9eb2c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQLE../cf36a.. ownership of fc6d0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJLd../e9236.. ownership of c3ba5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRmA../79a85.. ownership of d08e9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcQE../0eac0.. ownership of 8baaa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVTE../8eab0.. ownership of b2596.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLzx../3d131.. ownership of a43e2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcLo../c06a8.. ownership of 1efa9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVnU../f156e.. ownership of c44bc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTxo../0fdc0.. ownership of f00b6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbVn../67e76.. ownership of 73cbf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN9Y../390fd.. ownership of 01155.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUHY../b9fe5.. ownership of 4418a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbwD../959b0.. ownership of 4f8ca.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWJU../6c2ea.. ownership of a80e0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVcn../f2f49.. ownership of 55955.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK88../d5d7e.. ownership of 1f3e0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYQs../2e0ec.. ownership of cf13a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQEg../d1b78.. ownership of 2d2f1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKJX../9f5dd.. ownership of 19215.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWxJ../02be5.. ownership of 4842c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdSR../8ff50.. ownership of e7504.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNko../12b1c.. ownership of 2887e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTUg../0b72e.. ownership of 33e65.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdy9../eab29.. ownership of 6ad54.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYGB../e5f9a.. ownership of 8e7c5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTqe../f78c9.. ownership of 86d03.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLkX../e9283.. ownership of d8839.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFPn../45772.. ownership of 89021.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRU9../8d402.. ownership of 7c7b1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLbi../aa2f9.. ownership of 97f80.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLw9../0042e.. ownership of d1955.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNqC../b5ad0.. ownership of 1fa9c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaE3../e08cf.. ownership of 8f348.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMReX../f2b56.. ownership of c687c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKZX../8720b.. ownership of 4b446.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHD8../ea4b2.. ownership of b361f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQs3../098b0.. ownership of b0c07.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJip../b45ed.. ownership of e15d6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHXe../e3d1a.. ownership of 0f4de.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbc4../5f5a1.. ownership of 6c0c8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMccH../a102b.. ownership of 6deec.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNJg../48e60.. ownership of b3166.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSvA../96bef.. ownership of 14896.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUnz../864e7.. ownership of f6032.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUeM../dd560.. ownership of 73cce.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML7S../ce9ed.. ownership of 12d3c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZrR../4e791.. ownership of d3d68.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPTo../886f0.. ownership of b5b40.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNGZ../e2ee6.. ownership of a4354.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUKb../bcb15.. ownership of 5ac7e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKaM../023ab.. ownership of 6ca5c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSxY../15802.. ownership of a2011.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb8c../73522.. ownership of 7dd3b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWhy../baa27.. ownership of 90e02.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJLT../8aaf8.. ownership of 0ccad.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVKH../a3929.. ownership of a723b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPg4../cee24.. ownership of 6eef1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRyU../0aedf.. ownership of 786fb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWig../564bd.. ownership of 4e11f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHas../47a30.. ownership of 25a4f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPZU../72a32.. ownership of b6770.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVm4../924c0.. ownership of 10272.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaqd../044a6.. ownership of a90ae.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFUC../a3a62.. ownership of d4587.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMURU../c4e62.. ownership of 31c9d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaqQ../c2f72.. ownership of 5cd05.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRbX../57cc9.. ownership of 88494.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM8p../1bf57.. ownership of a5915.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRja../0dbfa.. ownership of ad438.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNxL../75b36.. ownership of 70872.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW6P../94105.. ownership of f26a7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLHp../dc30a.. ownership of 86743.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFLU../de33c.. ownership of 2ce64.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWxv../e246e.. ownership of 7aec9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRuW../14eca.. ownership of 74d25.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLTC../bd434.. ownership of b0a3f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLg7../00787.. ownership of 27e2e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWsk../42d40.. ownership of 5234e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLCX../bba2e.. ownership of 9903d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRdh../29380.. ownership of 8b373.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYUW../7a46e.. ownership of 01ef5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJvy../29b54.. ownership of cfbb7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQaq../91bde.. ownership of 70745.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLYz../d263a.. ownership of d6374.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSSx../09fea.. ownership of 68a3f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLGi../3bfb0.. ownership of d27ca.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNMz../53b3f.. ownership of 1b8bb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM4v../f5e2a.. ownership of ca0a3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS5r../fb84a.. ownership of 6793f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHQs../4f175.. ownership of f58b9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRj2../0bc7c.. ownership of f9c17.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMceo../14bc5.. ownership of bc534.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWQC../cbf9c.. ownership of 03207.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXSJ../44907.. ownership of 64b30.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTiS../c3a14.. ownership of 2bd96.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYCD../0c76b.. ownership of 02278.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZFv../c03c2.. ownership of 42688.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGmV../714c6.. ownership of c5d71.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWz7../69cae.. ownership of 148e7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbAx../2d91b.. ownership of bd5a2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQG1../e8b24.. ownership of d26db.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKXi../ecb58.. ownership of 92898.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWVm../4d802.. ownership of f73e5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMLf../e3037.. ownership of fa854.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQuK../59096.. ownership of 9e478.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXwJ../dcc56.. ownership of f3ab9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWHT../ee7d5.. ownership of 54ffc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJ8X../79802.. ownership of e480f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW6i../edfc0.. ownership of 10197.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdUw../f0604.. ownership of c21db.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQyB../a52b1.. ownership of 1fa74.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcn1../96c0f.. ownership of fae42.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWaN../1a90a.. ownership of f25e9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZa3../c06d7.. ownership of 34f20.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWtg../e5584.. ownership of e7c20.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYZA../9fa46.. ownership of 161e8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZXC../80ee9.. ownership of a146d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ7r../0d29b.. ownership of e96ab.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdXx../60589.. ownership of 5e74a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXmc../51a8b.. ownership of 98247.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMag../92a0e.. ownership of 87ddc.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNLK../913d8.. ownership of 36891.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP2g../6ab2b.. ownership of 35104.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMatx../b88b3.. ownership of 4c3dd.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbGd../04d09.. ownership of e0700.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVGa../d26f3.. ownership of 85488.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUMb../8035b.. ownership of 56080.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPyF../b0c33.. ownership of dac7d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVuh../63eb9.. ownership of 36093.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQvX../d313c.. ownership of 6e011.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMd7../7a764.. ownership of 35983.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ4k../c4049.. ownership of f4216.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcKw../f8d16.. ownership of 23a1a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZvX../59c4c.. ownership of bdc98.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF8i../9744f.. ownership of 013da.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSCz../619b2.. ownership of 37fa5.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF1q../d09c6.. ownership of ec553.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc1w../40af1.. ownership of fc47a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEnj../a67c2.. ownership of 81bb1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMScR../9dc8e.. ownership of 4cbdd.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJCQ../0eba6.. ownership of 93c99.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRJi../0b283.. ownership of 6e1a8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbuJ../232b0.. ownership of 19c2c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYvb../a708b.. ownership of 9e4ea.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGyx../8e3ec.. ownership of 30750.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJE1../015bb.. ownership of 583be.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJ7F../0d324.. ownership of 987b2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMU2k../8282a.. ownership of 71348.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbbW../f7281.. ownership of 4de1f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPrD../303dd.. ownership of fa072.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVJN../88e0f.. ownership of 027cf.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLE7../3ea39.. ownership of 23253.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGr3../4065a.. ownership of f4ccf.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX39../204f8.. ownership of 4d32c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKeL../6257d.. ownership of c0301.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaLh../c737a.. ownership of 83536.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKq4../1f689.. ownership of 3aee2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMJ2../d85f8.. ownership of 1df85.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMa2r../e0dbe.. ownership of fcf68.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdaX../e2ed1.. ownership of 93bb6.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJBz../1618a.. ownership of c40a6.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMHT../e55e2.. ownership of 4cb76.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJ3W../7de1a.. ownership of 11e73.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTsM../d7b4b.. ownership of 63811.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUUUw../e4ab7.. doc published by PrGxv..

Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Definition 11e73.. := λ x0 x1 . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 x1)
Param f482f.. : ι → ι → ι
Known 6f2e8.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) 4a7ef.. = x0
Theorem e7c20.. : ∀ x0 x1 x2 . x0 = 11e73.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem f25e9.. : ∀ x0 x1 . x0 = f482f.. (11e73.. x0 x1) 4a7ef.. (proof)
Known 15d37.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) (4ae4a.. 4a7ef..) = x1
Theorem 1fa74.. : ∀ x0 x1 x2 . x0 = 11e73.. x1 x2 ⟶ x2 = f482f.. x0 (4ae4a.. 4a7ef..) (proof)
Theorem 10197.. : ∀ x0 x1 . x1 = f482f.. (11e73.. x0 x1) (4ae4a.. 4a7ef..) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 54ffc.. : ∀ x0 x1 x2 x3 . 11e73.. x0 x2 = 11e73.. x1 x3 ⟶ and (x0 = x1) (x2 = x3) (proof)
Definition c40a6.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 x3 . prim1 x3 x2 ⟶ x1 (11e73.. x2 x3)) ⟶ x1 x0
Theorem 9e478.. : ∀ x0 x1 . prim1 x1 x0 ⟶ c40a6.. (11e73.. x0 x1) (proof)
Theorem f73e5.. : ∀ x0 x1 . c40a6.. (11e73.. x0 x1) ⟶ prim1 x1 x0 (proof)
Theorem d26db.. : ∀ x0 . c40a6.. x0 ⟶ x0 = 11e73.. (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..)) (proof)
Definition fcf68.. := λ x0 . λ x1 : ι → ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..))
Theorem 148e7.. : ∀ x0 : ι → ι → ι . ∀ x1 x2 . fcf68.. (11e73.. x1 x2) x0 = x0 x1 x2 (proof)
Definition 3aee2.. := λ x0 . λ x1 : ι → ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..))
Theorem 42688.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . 3aee2.. (11e73.. x1 x2) x0 = x0 x1 x2 (proof)
Definition c0301.. := λ x0 . λ x1 : ι → ι . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 (0fc90.. x0 x1))
Theorem 2bd96.. : ∀ x0 x1 . ∀ x2 : ι → ι . x0 = c0301.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 03207.. : ∀ x0 . ∀ x1 : ι → ι . x0 = f482f.. (c0301.. x0 x1) 4a7ef.. (proof)
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem f9c17.. : ∀ x0 x1 . ∀ x2 : ι → ι . x0 = c0301.. x1 x2 ⟶ ∀ x3 . prim1 x3 x1 ⟶ x2 x3 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x3 (proof)
Theorem 6793f.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 = f482f.. (f482f.. (c0301.. x0 x1) (4ae4a.. 4a7ef..)) x2 (proof)
Theorem 1b8bb.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . c0301.. x0 x2 = c0301.. x1 x3 ⟶ and (x0 = x1) (∀ x4 . prim1 x4 x0 ⟶ x2 x4 = x3 x4) (proof)
Known 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2
Theorem 68a3f.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ c0301.. x0 x1 = c0301.. x0 x2 (proof)
Definition f4ccf.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ x1 (c0301.. x2 x3)) ⟶ x1 x0
Theorem 70745.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ f4ccf.. (c0301.. x0 x1) (proof)
Theorem 01ef5.. : ∀ x0 . ∀ x1 : ι → ι . f4ccf.. (c0301.. x0 x1) ⟶ ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0 (proof)
Theorem 9903d.. : ∀ x0 . f4ccf.. x0 ⟶ x0 = c0301.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (proof)
Definition 027cf.. := λ x0 . λ x1 : ι → (ι → ι) → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 27e2e.. : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 027cf.. (c0301.. x1 x2) x0 = x0 x1 x2 (proof)
Definition 4de1f.. := λ x0 . λ x1 : ι → (ι → ι) → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 74d25.. : ∀ x0 : ι → (ι → ι) → ο . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 4de1f.. (c0301.. x1 x2) x0 = x0 x1 x2 (proof)
Param eb53d.. : ι → CT2 ι
Definition 987b2.. := λ x0 . λ x1 : ι → ι → ι . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 (eb53d.. x0 x1))
Theorem 2ce64.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . x0 = 987b2.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem f26a7.. : ∀ x0 . ∀ x1 : ι → ι → ι . x0 = f482f.. (987b2.. x0 x1) 4a7ef.. (proof)
Param e3162.. : ι → ι → ι → ι
Known 35054.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ e3162.. (eb53d.. x0 x1) x2 x3 = x1 x2 x3
Theorem ad438.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . x0 = 987b2.. x1 x2 ⟶ ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x2 x3 x4 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x3 x4 (proof)
Theorem 88494.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 x3 = e3162.. (f482f.. (987b2.. x0 x1) (4ae4a.. 4a7ef..)) x2 x3 (proof)
Theorem 31c9d.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . 987b2.. x0 x2 = 987b2.. x1 x3 ⟶ and (x0 = x1) (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = x3 x4 x5) (proof)
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 a90ae.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ 987b2.. x0 x1 = 987b2.. x0 x2 (proof)
Definition 30750.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ x1 (987b2.. x2 x3)) ⟶ x1 x0
Theorem b6770.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ 30750.. (987b2.. x0 x1) (proof)
Theorem 4e11f.. : ∀ x0 . ∀ x1 : ι → ι → ι . 30750.. (987b2.. x0 x1) ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0 (proof)
Theorem 6eef1.. : ∀ x0 . 30750.. x0 ⟶ x0 = 987b2.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (proof)
Definition 19c2c.. := λ x0 . λ x1 : ι → (ι → ι → ι) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 0ccad.. : ∀ x0 : ι → (ι → ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 19c2c.. (987b2.. x1 x2) x0 = x0 x1 x2 (proof)
Definition 93c99.. := λ x0 . λ x1 : ι → (ι → ι → ι) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 7dd3b.. : ∀ x0 : ι → (ι → ι → ι) → ο . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 93c99.. (987b2.. x1 x2) x0 = x0 x1 x2 (proof)
Param 1216a.. : ι → (ι → ο) → ι
Definition 81bb1.. := λ x0 . λ x1 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 (1216a.. x0 x1))
Theorem 6ca5c.. : ∀ x0 x1 . ∀ x2 : ι → ο . x0 = 81bb1.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem a4354.. : ∀ x0 . ∀ x1 : ι → ο . x0 = f482f.. (81bb1.. x0 x1) 4a7ef.. (proof)
Param decode_p : ι → ι → ο
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem d3d68.. : ∀ x0 x1 . ∀ x2 : ι → ο . x0 = 81bb1.. x1 x2 ⟶ ∀ x3 . prim1 x3 x1 ⟶ x2 x3 = decode_p (f482f.. x0 (4ae4a.. 4a7ef..)) x3 (proof)
Theorem 73cce.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 = decode_p (f482f.. (81bb1.. x0 x1) (4ae4a.. 4a7ef..)) x2 (proof)
Theorem 14896.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . 81bb1.. x0 x2 = 81bb1.. x1 x3 ⟶ and (x0 = x1) (∀ x4 . prim1 x4 x0 ⟶ x2 x4 = x3 x4) (proof)
Param iff : ο → ο → ο
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
Theorem 6deec.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 81bb1.. x0 x1 = 81bb1.. x0 x2 (proof)
Definition ec553.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ο . x1 (81bb1.. x2 x3)) ⟶ x1 x0
Theorem 0f4de.. : ∀ x0 . ∀ x1 : ι → ο . ec553.. (81bb1.. x0 x1) (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem b0c07.. : ∀ x0 . ec553.. x0 ⟶ x0 = 81bb1.. (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..))) (proof)
Definition 013da.. := λ x0 . λ x1 : ι → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 4b446.. : ∀ x0 : ι → (ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ο . (∀ x3 : ι → ο . (∀ x4 . prim1 x4 x1 ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 013da.. (81bb1.. x1 x2) x0 = x0 x1 x2 (proof)
Definition 23a1a.. := λ x0 . λ x1 : ι → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 8f348.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ο . (∀ x3 : ι → ο . (∀ x4 . prim1 x4 x1 ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 23a1a.. (81bb1.. x1 x2) x0 = x0 x1 x2 (proof)
Param d2155.. : ι → (ι → ι → ο) → ι
Definition 35983.. := λ x0 . λ x1 : ι → ι → ο . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 (d2155.. x0 x1))
Theorem d1955.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . x0 = 35983.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 7c7b1.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . x2 x0 (f482f.. (35983.. x0 x1) 4a7ef..) ⟶ x2 (f482f.. (35983.. x0 x1) 4a7ef..) x0 (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 d8839.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . x0 = 35983.. x1 x2 ⟶ ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x2 x3 x4 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x3 x4 (proof)
Theorem 8e7c5.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 x3 = 2b2e3.. (f482f.. (35983.. x0 x1) (4ae4a.. 4a7ef..)) x2 x3 (proof)
Theorem 33e65.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . 35983.. x0 x2 = 35983.. x1 x3 ⟶ and (x0 = x1) (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = x3 x4 x5) (proof)
Known 62ef7.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ iff (x1 x3 x4) (x2 x3 x4)) ⟶ d2155.. x0 x1 = d2155.. x0 x2
Theorem e7504.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ iff (x1 x3 x4) (x2 x3 x4)) ⟶ 35983.. x0 x1 = 35983.. x0 x2 (proof)
Definition 36093.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . x1 (35983.. x2 x3)) ⟶ x1 x0
Theorem 19215.. : ∀ x0 . ∀ x1 : ι → ι → ο . 36093.. (35983.. x0 x1) (proof)
Theorem cf13a.. : ∀ x0 . 36093.. x0 ⟶ x0 = 35983.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (proof)
Definition 56080.. := λ x0 . λ x1 : ι → (ι → ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 55955.. : ∀ x0 : ι → (ι → ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 56080.. (35983.. x1 x2) x0 = x0 x1 x2 (proof)
Definition e0700.. := λ x0 . λ x1 : ι → (ι → ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 4f8ca.. : ∀ x0 : ι → (ι → ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ e0700.. (35983.. x1 x2) x0 = x0 x1 x2 (proof)
Param e0e40.. : ι → ((ι → ο) → ο) → ι
Definition 35104.. := λ x0 . λ x1 : (ι → ο) → ο . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 (e0e40.. x0 x1))
Theorem 01155.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . x0 = 35104.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem f00b6.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . x0 = f482f.. (35104.. x0 x1) 4a7ef.. (proof)
Param decode_c : ι → (ι → ο) → ο
Known 81500.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . (∀ x3 . x2 x3 ⟶ prim1 x3 x0) ⟶ decode_c (e0e40.. x0 x1) x2 = x1 x2
Theorem 1efa9.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . x0 = 35104.. x1 x2 ⟶ ∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ prim1 x4 x1) ⟶ x2 x3 = decode_c (f482f.. x0 (4ae4a.. 4a7ef..)) x3 (proof)
Theorem b2596.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . (∀ x3 . x2 x3 ⟶ prim1 x3 x0) ⟶ x1 x2 = decode_c (f482f.. (35104.. x0 x1) (4ae4a.. 4a7ef..)) x2 (proof)
Theorem d08e9.. : ∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . 35104.. x0 x2 = 35104.. x1 x3 ⟶ and (x0 = x1) (∀ x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x0) ⟶ x2 x4 = x3 x4) (proof)
Known fe043.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . (∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ prim1 x4 x0) ⟶ iff (x1 x3) (x2 x3)) ⟶ e0e40.. x0 x1 = e0e40.. x0 x2
Theorem fc6d0.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . (∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ prim1 x4 x0) ⟶ iff (x1 x3) (x2 x3)) ⟶ 35104.. x0 x1 = 35104.. x0 x2 (proof)
Definition 87ddc.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : (ι → ο) → ο . x1 (35104.. x2 x3)) ⟶ x1 x0
Theorem 8f88b.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . 87ddc.. (35104.. x0 x1) (proof)
Theorem 7efe5.. : ∀ x0 . 87ddc.. x0 ⟶ x0 = 35104.. (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (proof)
Definition 5e74a.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → ι . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 7210f.. : ∀ x0 : ι → ((ι → ο) → ο) → ι . ∀ x1 . ∀ x2 : (ι → ο) → ο . (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x1) ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 5e74a.. (35104.. x1 x2) x0 = x0 x1 x2 (proof)
Definition a146d.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → ο . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 0b20d.. : ∀ x0 : ι → ((ι → ο) → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x1) ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ a146d.. (35104.. x1 x2) x0 = x0 x1 x2 (proof)