Proofgold Signed Transaction

vin
Pr53g../118bc.. PUQ4v../9e7de..

vout

Pr53g../d4485.. 1.96 bars
TMHeJ../b8e03.. ownership of 53c70.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJDJ../651c3.. ownership of 8039b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMabh../54447.. ownership of 8088b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYWz../60fc0.. ownership of 4dd15.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRwU../1f672.. ownership of 014b6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNwQ../f2b06.. ownership of ad206.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHtV../cfb78.. ownership of 4b1e4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaCm../621ef.. ownership of 9fc28.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH56../27543.. ownership of e8e7c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLhi../d1872.. ownership of 56ae7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH9p../2b18c.. ownership of 2098a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUYm../4295d.. ownership of 0e45f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYdt../ed5df.. ownership of 9c7d4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUUa../d1a4d.. ownership of 6787a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaDZ../da048.. ownership of fd239.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNT6../3a4a9.. ownership of f1e63.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLPv../2c5a7.. ownership of 72fdb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLZz../72a5a.. ownership of 03ae4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd51../52da7.. ownership of 76e61.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMFM../82ab0.. ownership of 99ef3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGdi../46a9e.. ownership of 7c649.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR7e../d6522.. ownership of 842e3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYT1../62219.. ownership of e0b06.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRpw../345b3.. ownership of 80b97.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHmG../f9130.. ownership of c7e82.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZdc../1b1b7.. ownership of 6dcb0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZwU../98bf1.. ownership of b19dd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUoC../3be03.. ownership of a580b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKfc../795c9.. ownership of 5946d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXMf../d8d54.. ownership of add6d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbWx../4689a.. ownership of b127a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWe6../8aa2f.. ownership of 18466.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaE1../779d7.. ownership of cdeb8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF4N../a1cb2.. ownership of d1f4f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQUY../afee3.. ownership of 0b00c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFKg../f29b7.. ownership of 4529c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLqD../57893.. ownership of ea72b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPHZ../71ab5.. ownership of d5ae3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLAm../cf3fb.. ownership of 54b81.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJek../f0360.. ownership of ccbf6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQzM../0e348.. ownership of f4109.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaSo../1ec45.. ownership of 1f359.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM6a../385d3.. ownership of 4bd1d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcF5../1a6b5.. ownership of f9bb0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdbA../2bf4e.. ownership of 0ad5e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZy9../de56a.. ownership of afed1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYvv../2d899.. ownership of 3b2a9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQxZ../f6499.. ownership of 59ca0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJJj../69ee8.. ownership of a7210.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUqU../e721e.. ownership of a0c1c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKAQ../352f9.. ownership of 0c40b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUA3../269e9.. ownership of 3d9b7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWTx../75f58.. ownership of 451a8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUC7../4da9a.. ownership of 4b68e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMadG../6776e.. ownership of d1048.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFpE../cb736.. ownership of 4fae8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSEn../f5a9f.. ownership of b3521.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcsR../acffd.. ownership of fb834.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLjV../b2e14.. ownership of a26f3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN38../6adc3.. ownership of 40fe0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPs1../75253.. ownership of 7d9fd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFxW../e1ebe.. ownership of 90200.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMa7X../f08d4.. ownership of 592f1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR68../f1e9e.. ownership of a80b2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSah../7a654.. ownership of 6fb62.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNiQ../51eed.. ownership of 237b5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV2k../7b836.. ownership of 60aa8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQf1../f9758.. ownership of e73c4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWap../55520.. ownership of dad57.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLgq../0f61f.. ownership of 1507a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHXu../9a098.. ownership of f7f73.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZdE../96954.. ownership of ba850.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVQK../097af.. ownership of 7e1bc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGBr../1b4a5.. ownership of 7829c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdQB../481de.. ownership of 87465.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc4t../14a3b.. ownership of e5153.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPyY../e7a0e.. ownership of 8faf4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH4N../1d492.. ownership of ae455.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKM5../4ce7d.. ownership of b617b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXVD../20fd4.. ownership of 0c1a7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXfb../97075.. ownership of f77e0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTNp../bf254.. ownership of f09fe.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcBL../6327a.. ownership of c857f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaVJ../6043c.. ownership of dceb0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPDA../b9828.. ownership of 0cbda.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXzj../2e64d.. ownership of 9ae3c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNA6../2019d.. ownership of 5ab49.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN1G../c1f25.. ownership of 31e08.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHNs../a2c3a.. ownership of b6081.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVvS../ed18f.. ownership of 98aa8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY8E../d00d8.. ownership of a04cc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNK4../341f3.. ownership of e852d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFC2../9f263.. ownership of 1e3c2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHSS../e3f06.. ownership of ffab9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGa3../4fa37.. ownership of 1ddeb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFxt../f0da6.. ownership of 185df.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVS4../d6d07.. ownership of f1b26.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMoD../ca73a.. ownership of 2769d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLpJ../f4505.. ownership of 30e8e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYQv../6e9dc.. ownership of 12840.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMU8Q../4b085.. ownership of 97d26.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTLw../fb695.. ownership of 9f372.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHZ7../a0f26.. ownership of 16896.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNL2../5e270.. ownership of bf756.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUtb../be620.. ownership of b4c19.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMa2S../d33dd.. ownership of ade3d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFsi../4fc71.. ownership of c29f4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQxP../6ba84.. ownership of d6266.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFge../f63ed.. ownership of 9bb50.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWEg../4c139.. ownership of e78d5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGvP../eedb6.. ownership of 6227c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMQX../6fe10.. ownership of 32103.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdTN../d1ed8.. ownership of df1be.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFGv../7332f.. ownership of c8d12.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKaV../21b40.. ownership of 943ec.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdSH../237de.. ownership of cce38.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMUF../1e91b.. ownership of ba55d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMabv../72066.. ownership of aa3a1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYPp../d1d88.. ownership of 5bfd0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT3u../c907b.. ownership of 23bdc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFim../6822b.. ownership of 81d59.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGLs../9b084.. ownership of 4f3af.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbvj../50a2b.. ownership of 059c3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKZG../b8b24.. ownership of 2ba90.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXS4../f93fd.. ownership of 3b630.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUyg../35b89.. ownership of d5c66.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSqV../451ca.. ownership of ab466.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUrM../fa596.. ownership of 4b13a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY1b../2d2c7.. ownership of 6036d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHre../7df85.. ownership of 34caf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSVL../e8565.. ownership of 0ae8d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVd6../2b7a0.. ownership of 9d9f2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRyV../968f0.. ownership of 6f612.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQGg../3fd53.. ownership of 1d898.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFS5../bdbe9.. ownership of 05946.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXyh../3fda0.. ownership of 16a0a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQJx../30188.. ownership of a15d6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLhv../e1c2e.. ownership of bca97.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW3P../97bd9.. ownership of a6f1a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZw9../39e31.. ownership of 33f79.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTHf../34f90.. ownership of 0d55e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbyN../579b3.. ownership of dd02d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYeb../9913d.. ownership of 8a141.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLD8../a0042.. ownership of d3745.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYff../666a6.. ownership of 99d82.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEwx../3c37f.. ownership of 46c3e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRFr../441af.. ownership of 13bf1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLda../52c25.. ownership of 0eba4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUNj../eb7eb.. ownership of b5f96.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML7y../14926.. ownership of 8daea.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSWY../0ef06.. ownership of 0717a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbhD../c269b.. ownership of 56fff.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQn3../6d29f.. ownership of 5e270.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdyP../76b58.. ownership of ff14f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHLf../369bf.. ownership of a0dc3.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKaV../3c161.. ownership of 56896.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZXP../11da6.. ownership of 47d0a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN7h../050fa.. ownership of 0332d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLWj../69421.. ownership of f7c54.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP9n../16f19.. ownership of bbcc4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbdz../bc5f2.. ownership of dd3c8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKth../8684b.. ownership of f012c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX6L../e443f.. ownership of 24d60.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML5Q../9b3c5.. ownership of 62bb7.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPWx../3d019.. ownership of 8547b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPCw../6ef59.. ownership of c962d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPW2../da06f.. ownership of 7b9a8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFHW../a5ccb.. ownership of 80b9a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZUb../06f54.. ownership of 42836.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTfu../18080.. ownership of 9f5fe.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMxQ../65941.. ownership of b5e83.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSn6../b24e0.. ownership of 51209.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbqo../499ac.. ownership of 9663d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTTf../b8167.. ownership of 1134c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbMs../168b1.. ownership of 08eae.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMREc../176dc.. ownership of c0f94.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHHE../6ac9a.. ownership of 08354.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUaJ../6b0e3.. ownership of f48ce.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMri../e7d3b.. ownership of f1574.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS9M../d005b.. ownership of 31816.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYvM../11593.. ownership of a366a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRqm../3a9e9.. ownership of 918b8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFCx../8f929.. ownership of d7681.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFgH../7e98e.. ownership of 5fa8f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH3U../6a9d7.. ownership of 8eacd.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYSb../192a9.. ownership of fc788.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK2D../ceee5.. ownership of b4400.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY9j../fcf26.. ownership of cfdc4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT9D../ff967.. ownership of f614a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV7W../7c7a1.. ownership of 26d39.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMauZ../d8534.. ownership of 836b1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYjL../b8a39.. ownership of 120e8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSSL../42a0e.. ownership of da24e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFJc../2758a.. ownership of e45a4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM7U../faebc.. ownership of 54aad.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNpG../d6630.. ownership of 4e2ce.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJM7../29c27.. ownership of c7882.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNbu../0d124.. ownership of c0713.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR8K../b619e.. ownership of e5836.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM4k../f9405.. ownership of dfea4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKwf../19ee3.. ownership of 73737.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWT7../02de1.. ownership of a4e7e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUXdb../5aa77.. doc published by PrGxv..

Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Param d2155.. : ι → (ι → ι → ο) → ι
Definition 73737.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (d2155.. x0 x2)))
Param f482f.. : ι → ι → ι
Known 52da6.. : ∀ x0 x1 x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) 4a7ef.. = x0
Theorem 5e270.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . x0 = 73737.. x1 x2 x3 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 0717a.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ο . x3 x0 (f482f.. (73737.. x0 x1 x2) 4a7ef..) ⟶ x3 (f482f.. (73737.. x0 x1 x2) 4a7ef..) x0 (proof)
Known c2bca.. : ∀ x0 x1 x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (4ae4a.. 4a7ef..) = x1
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem b5f96.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . x0 = 73737.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x2 x4 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x4 (proof)
Theorem 13bf1.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ x1 x3 = f482f.. (f482f.. (73737.. x0 x1 x2) (4ae4a.. 4a7ef..)) x3 (proof)
Param 2b2e3.. : ι → ι → ι → ο
Known 11d6d.. : ∀ x0 x1 x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2
Known 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ 2b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3
Theorem 99d82.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . x0 = 73737.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x3 x4 x5 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem 8a141.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 x4 = 2b2e3.. (f482f.. (73737.. x0 x1 x2) (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 0d55e.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ο . 73737.. x0 x2 x4 = 73737.. x1 x3 x5 ⟶ and (and (x0 = x1) (∀ x6 . prim1 x6 x0 ⟶ x2 x6 = x3 x6)) (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x6 x7 = x5 x6 x7) (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
Known 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2
Theorem a6f1a.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . (∀ x5 . prim1 x5 x0 ⟶ x1 x5 = x2 x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ iff (x3 x5 x6) (x4 x5 x6)) ⟶ 73737.. x0 x1 x3 = 73737.. x0 x2 x4 (proof)
Definition e5836.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ι → ο . x1 (73737.. x2 x3 x4)) ⟶ x1 x0
Theorem a15d6.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ι → ο . e5836.. (73737.. x0 x1 x2) (proof)
Theorem 05946.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . e5836.. (73737.. x0 x1 x2) ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x3) x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem 6f612.. : ∀ x0 . e5836.. x0 ⟶ x0 = 73737.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition c7882.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 0ae8d.. : ∀ x0 : ι → (ι → ι) → (ι → ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . (∀ x4 : ι → ι . (∀ x5 . prim1 x5 x1 ⟶ x2 x5 = x4 x5) ⟶ ∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ iff (x3 x6 x7) (x5 x6 x7)) ⟶ x0 x1 x4 x5 = x0 x1 x2 x3) ⟶ c7882.. (73737.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition 54aad.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 6036d.. : ∀ x0 : ι → (ι → ι) → (ι → ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . (∀ x4 : ι → ι . (∀ x5 . prim1 x5 x1 ⟶ x2 x5 = x4 x5) ⟶ ∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ iff (x3 x6 x7) (x5 x6 x7)) ⟶ x0 x1 x4 x5 = x0 x1 x2 x3) ⟶ 54aad.. (73737.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Param 1216a.. : ι → (ι → ο) → ι
Definition da24e.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (1216a.. x0 x2)))
Theorem ab466.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . x0 = da24e.. x1 x2 x3 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 3b630.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . x0 = f482f.. (da24e.. x0 x1 x2) 4a7ef.. (proof)
Theorem 059c3.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . x0 = da24e.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x2 x4 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x4 (proof)
Theorem 81d59.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ x1 x3 = f482f.. (f482f.. (da24e.. x0 x1 x2) (4ae4a.. 4a7ef..)) x3 (proof)
Param decode_p : ι → ι → ο
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem 5bfd0.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . x0 = da24e.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x3 x4 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x4 (proof)
Theorem ba55d.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ x2 x3 = decode_p (f482f.. (da24e.. x0 x1 x2) (4ae4a.. (4ae4a.. 4a7ef..))) x3 (proof)
Theorem 943ec.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ο . da24e.. x0 x2 x4 = da24e.. x1 x3 x5 ⟶ and (and (x0 = x1) (∀ x6 . prim1 x6 x0 ⟶ x2 x6 = x3 x6)) (∀ x6 . prim1 x6 x0 ⟶ x4 x6 = x5 x6) (proof)
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
Theorem df1be.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . (∀ x5 . prim1 x5 x0 ⟶ x1 x5 = x2 x5) ⟶ (∀ x5 . prim1 x5 x0 ⟶ iff (x3 x5) (x4 x5)) ⟶ da24e.. x0 x1 x3 = da24e.. x0 x2 x4 (proof)
Definition 836b1.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ο . x1 (da24e.. x2 x3 x4)) ⟶ x1 x0
Theorem 6227c.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ο . 836b1.. (da24e.. x0 x1 x2) (proof)
Theorem 9bb50.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . 836b1.. (da24e.. x0 x1 x2) ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x3) x0 (proof)
Theorem c29f4.. : ∀ x0 . 836b1.. x0 ⟶ x0 = da24e.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition f614a.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem b4c19.. : ∀ x0 : ι → (ι → ι) → (ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . (∀ x4 : ι → ι . (∀ x5 . prim1 x5 x1 ⟶ x2 x5 = x4 x5) ⟶ ∀ x5 : ι → ο . (∀ x6 . prim1 x6 x1 ⟶ iff (x3 x6) (x5 x6)) ⟶ x0 x1 x4 x5 = x0 x1 x2 x3) ⟶ f614a.. (da24e.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition b4400.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 16896.. : ∀ x0 : ι → (ι → ι) → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . (∀ x4 : ι → ι . (∀ x5 . prim1 x5 x1 ⟶ x2 x5 = x4 x5) ⟶ ∀ x5 : ι → ο . (∀ x6 . prim1 x6 x1 ⟶ iff (x3 x6) (x5 x6)) ⟶ x0 x1 x4 x5 = x0 x1 x2 x3) ⟶ b4400.. (da24e.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition 8eacd.. := λ x0 . λ x1 : ι → ι . λ x2 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) x2))
Theorem 97d26.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . x0 = 8eacd.. x1 x2 x3 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 30e8e.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x0 = f482f.. (8eacd.. x0 x1 x2) 4a7ef.. (proof)
Theorem f1b26.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . x0 = 8eacd.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x2 x4 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x4 (proof)
Theorem 1ddeb.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x3 x0 ⟶ x1 x3 = f482f.. (f482f.. (8eacd.. x0 x1 x2) (4ae4a.. 4a7ef..)) x3 (proof)
Theorem 1e3c2.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . x0 = 8eacd.. x1 x2 x3 ⟶ x3 = f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem a04cc.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 = f482f.. (8eacd.. x0 x1 x2) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem b6081.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 . 8eacd.. x0 x2 x4 = 8eacd.. x1 x3 x5 ⟶ and (and (x0 = x1) (∀ x6 . prim1 x6 x0 ⟶ x2 x6 = x3 x6)) (x4 = x5) (proof)
Theorem 5ab49.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 . (∀ x4 . prim1 x4 x0 ⟶ x1 x4 = x2 x4) ⟶ 8eacd.. x0 x1 x3 = 8eacd.. x0 x2 x3 (proof)
Definition d7681.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 . prim1 x4 x2 ⟶ x1 (8eacd.. x2 x3 x4)) ⟶ x1 x0
Theorem 0cbda.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 . prim1 x2 x0 ⟶ d7681.. (8eacd.. x0 x1 x2) (proof)
Theorem c857f.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . d7681.. (8eacd.. x0 x1 x2) ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x3) x0 (proof)
Theorem f77e0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . d7681.. (8eacd.. x0 x1 x2) ⟶ prim1 x2 x0 (proof)
Theorem b617b.. : ∀ x0 . d7681.. x0 ⟶ x0 = 8eacd.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Definition a366a.. := λ x0 . λ x1 : ι → (ι → ι) → ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))
Theorem 8faf4.. : ∀ x0 : ι → (ι → ι) → ι → ι . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 . (∀ x4 : ι → ι . (∀ x5 . prim1 x5 x1 ⟶ x2 x5 = x4 x5) ⟶ x0 x1 x4 x3 = x0 x1 x2 x3) ⟶ a366a.. (8eacd.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition f1574.. := λ x0 . λ x1 : ι → (ι → ι) → ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))
Theorem 87465.. : ∀ x0 : ι → (ι → ι) → ι → ο . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 . (∀ x4 : ι → ι . (∀ x5 . prim1 x5 x1 ⟶ x2 x5 = x4 x5) ⟶ x0 x1 x4 x3 = x0 x1 x2 x3) ⟶ f1574.. (8eacd.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition 08354.. := λ x0 . λ x1 x2 : ι → ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (d2155.. x0 x2)))
Theorem 7e1bc.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . x0 = 08354.. x1 x2 x3 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem f7f73.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ο . x3 x0 (f482f.. (08354.. x0 x1 x2) 4a7ef..) ⟶ x3 (f482f.. (08354.. x0 x1 x2) 4a7ef..) x0 (proof)
Theorem dad57.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . x0 = 08354.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x4 x5 (proof)
Theorem 60aa8.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = 2b2e3.. (f482f.. (08354.. x0 x1 x2) (4ae4a.. 4a7ef..)) x3 x4 (proof)
Theorem 6fb62.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . x0 = 08354.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x3 x4 x5 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem 592f1.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 x4 = 2b2e3.. (f482f.. (08354.. x0 x1 x2) (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4 (proof)
Theorem 7d9fd.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ο . 08354.. x0 x2 x4 = 08354.. x1 x3 x5 ⟶ and (and (x0 = x1) (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x2 x6 x7 = x3 x6 x7)) (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x6 x7 = x5 x6 x7) (proof)
Theorem a26f3.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ iff (x1 x5 x6) (x2 x5 x6)) ⟶ (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ iff (x3 x5 x6) (x4 x5 x6)) ⟶ 08354.. x0 x1 x3 = 08354.. x0 x2 x4 (proof)
Definition 08eae.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 x4 : ι → ι → ο . x1 (08354.. x2 x3 x4)) ⟶ x1 x0
Theorem b3521.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . 08eae.. (08354.. x0 x1 x2) (proof)
Theorem d1048.. : ∀ x0 . 08eae.. x0 ⟶ x0 = 08354.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition 9663d.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 451a8.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 : ι → ι → ο . (∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ iff (x2 x5 x6) (x4 x5 x6)) ⟶ ∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ iff (x3 x6 x7) (x5 x6 x7)) ⟶ x0 x1 x4 x5 = x0 x1 x2 x3) ⟶ 9663d.. (08354.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition b5e83.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 0c40b.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 : ι → ι → ο . (∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ iff (x2 x5 x6) (x4 x5 x6)) ⟶ ∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ iff (x3 x6 x7) (x5 x6 x7)) ⟶ x0 x1 x4 x5 = x0 x1 x2 x3) ⟶ b5e83.. (08354.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition 42836.. := λ x0 . λ x1 : ι → ι → ο . λ x2 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (1216a.. x0 x2)))
Theorem a7210.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . x0 = 42836.. x1 x2 x3 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 3b2a9.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . x0 = f482f.. (42836.. x0 x1 x2) 4a7ef.. (proof)
Theorem 0ad5e.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . x0 = 42836.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x4 x5 (proof)
Theorem 4bd1d.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = 2b2e3.. (f482f.. (42836.. x0 x1 x2) (4ae4a.. 4a7ef..)) x3 x4 (proof)
Theorem f4109.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . x0 = 42836.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x3 x4 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x4 (proof)
Theorem 54b81.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ x2 x3 = decode_p (f482f.. (42836.. x0 x1 x2) (4ae4a.. (4ae4a.. 4a7ef..))) x3 (proof)
Theorem ea72b.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . 42836.. x0 x2 x4 = 42836.. x1 x3 x5 ⟶ and (and (x0 = x1) (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x2 x6 x7 = x3 x6 x7)) (∀ x6 . prim1 x6 x0 ⟶ x4 x6 = x5 x6) (proof)
Theorem 0b00c.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . (∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ iff (x1 x5 x6) (x2 x5 x6)) ⟶ (∀ x5 . prim1 x5 x0 ⟶ iff (x3 x5) (x4 x5)) ⟶ 42836.. x0 x1 x3 = 42836.. x0 x2 x4 (proof)
Definition 7b9a8.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x1 (42836.. x2 x3 x4)) ⟶ x1 x0
Theorem cdeb8.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . 7b9a8.. (42836.. x0 x1 x2) (proof)
Theorem b127a.. : ∀ x0 . 7b9a8.. x0 ⟶ x0 = 42836.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition 8547b.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 5946d.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . (∀ x4 : ι → ι → ο . (∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ iff (x2 x5 x6) (x4 x5 x6)) ⟶ ∀ x5 : ι → ο . (∀ x6 . prim1 x6 x1 ⟶ iff (x3 x6) (x5 x6)) ⟶ x0 x1 x4 x5 = x0 x1 x2 x3) ⟶ 8547b.. (42836.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition 24d60.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem b19dd.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . (∀ x4 : ι → ι → ο . (∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ iff (x2 x5 x6) (x4 x5 x6)) ⟶ ∀ x5 : ι → ο . (∀ x6 . prim1 x6 x1 ⟶ iff (x3 x6) (x5 x6)) ⟶ x0 x1 x4 x5 = x0 x1 x2 x3) ⟶ 24d60.. (42836.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition dd3c8.. := λ x0 . λ x1 : ι → ι → ο . λ x2 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) x2))
Theorem c7e82.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . ∀ x3 . x0 = dd3c8.. x1 x2 x3 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem e0b06.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . x0 = f482f.. (dd3c8.. x0 x1 x2) 4a7ef.. (proof)
Theorem 7c649.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . ∀ x3 . x0 = dd3c8.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x4 x5 (proof)
Theorem 76e61.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = 2b2e3.. (f482f.. (dd3c8.. x0 x1 x2) (4ae4a.. 4a7ef..)) x3 x4 (proof)
Theorem 72fdb.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . ∀ x3 . x0 = dd3c8.. x1 x2 x3 ⟶ x3 = f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem fd239.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . x2 = f482f.. (dd3c8.. x0 x1 x2) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem 9c7d4.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 . dd3c8.. x0 x2 x4 = dd3c8.. x1 x3 x5 ⟶ and (and (x0 = x1) (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x2 x6 x7 = x3 x6 x7)) (x4 = x5) (proof)
Theorem 2098a.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ iff (x1 x4 x5) (x2 x4 x5)) ⟶ dd3c8.. x0 x1 x3 = dd3c8.. x0 x2 x3 (proof)
Definition f7c54.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . ∀ x4 . prim1 x4 x2 ⟶ x1 (dd3c8.. x2 x3 x4)) ⟶ x1 x0
Theorem e8e7c.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ f7c54.. (dd3c8.. x0 x1 x2) (proof)
Theorem 4b1e4.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . f7c54.. (dd3c8.. x0 x1 x2) ⟶ prim1 x2 x0 (proof)
Theorem 014b6.. : ∀ x0 . f7c54.. x0 ⟶ x0 = dd3c8.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Definition 47d0a.. := λ x0 . λ x1 : ι → (ι → ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))
Theorem 8088b.. : ∀ x0 : ι → (ι → ι → ο) → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ο . ∀ x3 . (∀ x4 : ι → ι → ο . (∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ iff (x2 x5 x6) (x4 x5 x6)) ⟶ x0 x1 x4 x3 = x0 x1 x2 x3) ⟶ 47d0a.. (dd3c8.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition a0dc3.. := λ x0 . λ x1 : ι → (ι → ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))
Theorem 53c70.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . ∀ x3 . (∀ x4 : ι → ι → ο . (∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ iff (x2 x5 x6) (x4 x5 x6)) ⟶ x0 x1 x4 x3 = x0 x1 x2 x3) ⟶ a0dc3.. (dd3c8.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)