Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrEvg../5035e..
PUdXP../862bf..
vout
PrEvg../e4b45.. 0.29 bars
TMF85../a0794.. ownership of fe043.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbaH../101a6.. ownership of 35ee9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH89../89dc0.. ownership of 81500.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVh1../10237.. ownership of 886a0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFz5../4c6ea.. ownership of 62ef7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSbd../f1c78.. ownership of 75d5b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMaA../19200.. ownership of 67416.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZBr../6fafa.. ownership of 2f933.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNx6../1d9a8.. ownership of ee7ef.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUfc../8250c.. ownership of b3f05.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd1a../b8b4d.. ownership of 931fe.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFUa../7cd3a.. ownership of ffe6e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPw5../859d8.. ownership of 8fdaf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHNB../4c2d5.. ownership of dbb26.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc5d../238c5.. ownership of 35054.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSmr../3413d.. ownership of f02bb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHQw../af0e9.. ownership of 4402a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdSN../7dcec.. ownership of 075a7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTks../da88b.. ownership of f22ec.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXJD../0c6ab.. ownership of b4566.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMakL../1aa16.. ownership of ed27c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc4v../46e51.. ownership of 0c6a8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUZ3../b721c.. ownership of 1b91d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNbm../7972c.. ownership of e8283.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFjx../c74f8.. ownership of bcb22.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRLh../658b1.. ownership of 27feb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK5w../58549.. ownership of 7e4c2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZLD../0164a.. ownership of 0d475.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaqa../f9155.. ownership of a850e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHyz../bf115.. ownership of 08b94.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPbs../50adf.. ownership of 5af6c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNny../90bc7.. ownership of 92bea.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZEM../de09b.. ownership of f6f3f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGZf../679cd.. ownership of 127cc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMavJ../dde23.. ownership of 78561.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLuN../ba86a.. ownership of 30ac4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQQT../191d2.. ownership of 338b2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbqN../badb6.. ownership of 90f35.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRuG../6b08e.. ownership of 36b09.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWTz../58ae3.. ownership of 9eb26.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLhg../3f1dc.. ownership of 41662.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNeT../993a1.. ownership of 1016a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGhm../b2df5.. ownership of 0d9ad.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX8C../cf6b5.. ownership of 0d0b4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFS5../f7c89.. ownership of fbd31.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEk2../5ea3b.. ownership of d5163.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbhY../dab23.. ownership of 380ca.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMap4../e8c76.. ownership of f0ee0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYxH../6b7d8.. ownership of 15d37.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPd5../fa629.. ownership of 327f4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMa5a../4ddfa.. ownership of 6f2e8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXVa../c466b.. ownership of 67d8f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbv3../c7f49.. ownership of 2d4b0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWfu../b6e2a.. ownership of 1d98a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXjM../bcab7.. ownership of 8c3eb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZuU../cbc5d.. ownership of b7e2d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXjU../2ceca.. ownership of 1cc2a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc4a../fe703.. ownership of 19a14.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMco3../40ee3.. ownership of 204eb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcuo../94817.. ownership of 182c0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHKj../810b7.. ownership of 34894.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPaP../8f041.. ownership of 73713.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcmH../f8dad.. ownership of 6e275.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJwd../6288d.. ownership of 37fcf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNdy../df527.. ownership of cce19.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF16../122ec.. ownership of 5e17d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMVM../e5644.. ownership of d8d74.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSsz../fe35e.. ownership of c1643.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSVo../866e1.. ownership of 27474.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSgL../2aaf2.. ownership of 78f42.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVCN../aed2a.. ownership of 5795e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMMj../cae00.. ownership of d15af.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR5m../aaa65.. ownership of 85578.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK7s../87867.. ownership of e9180.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPk9../da7b0.. ownership of 8d403.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFvJ../72271.. ownership of e08a0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFNB../a4d45.. ownership of f71c6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZwi../13feb.. ownership of dc63f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRLj../6b065.. ownership of d9414.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR4m../7e8b4.. ownership of a47a6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMa3o../66802.. ownership of 7d7d0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZqy../c83c4.. ownership of c01e3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb7f../4ee53.. ownership of dfdb3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXtm../af2a9.. ownership of 296b6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP4Z../d8773.. ownership of dcd87.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMe1M../6da1c.. ownership of 5896c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaKt../a6d10.. ownership of 73bc9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS2N../30989.. ownership of 74e7c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQAF../725f8.. ownership of 35b50.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbFN../e3020.. ownership of e18ef.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ9W../1144d.. ownership of 33e74.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTR8../7e7f7.. ownership of a84e7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNqb../99c98.. ownership of a7149.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUcT../5023f.. ownership of 1f730.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKN8../fc3c8.. ownership of a283f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHBu../c9841.. ownership of 9dd94.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPhu../b3870.. ownership of 3f040.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKV5../9ea81.. ownership of faec3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMnQ../e0b49.. ownership of 0ba89.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYvk../b6dac.. ownership of fd8cf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFzV../9170f.. ownership of 76a87.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUxJ../7a894.. ownership of da2bd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRht../bdfde.. ownership of 9e5b2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJop../2c295.. ownership of 39bbb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYpA../2b1f1.. ownership of 69f30.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP2B../6985f.. ownership of be04e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPRc../a2925.. ownership of 2a2bc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH97../675c3.. ownership of 94a94.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR5o../39eb4.. ownership of aa929.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaPN../81544.. ownership of 5843a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZTE../486d3.. ownership of 9b331.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGM5../92b5d.. ownership of c6a1a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVUB../1732a.. ownership of 7d8a1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMGa../4800f.. ownership of d4dc7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQhb../8205a.. ownership of f5701.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQgA../a32ad.. ownership of 1f270.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK4E../ccde9.. ownership of 4949d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHHc../9b1e9.. ownership of 36957.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT4w../44fdf.. ownership of 713d5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZNm../5810c.. ownership of e2ceb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKgS../f5b05.. ownership of fd5b7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVWQ../c6ae5.. ownership of d2654.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZFy../d9986.. ownership of 8f68d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcnQ../4d3c2.. ownership of c9dc4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdbt../2ffd4.. ownership of c5caa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQTJ../78528.. ownership of eaf7c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSDf../5200f.. ownership of 2ad56.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRFL../8235b.. ownership of 723cd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPLU../993ce.. ownership of f42b8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWSR../e911d.. ownership of 6e18e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT5Z../37a32.. ownership of d3673.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY9y../8575e.. ownership of 84e80.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcoj../62fb3.. ownership of 690be.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdq2../de27e.. ownership of e852c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFtY../d4403.. ownership of e2bb7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUtV../07cea.. ownership of 71513.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK9J../ad7d6.. ownership of 5d5fc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHZ5../09442.. ownership of 65b69.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFFn../86273.. ownership of cbf3e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaLX../77183.. ownership of 39778.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGXi../d65c8.. ownership of a268e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVbt../c0c74.. ownership of 98f3c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTrV../19f85.. ownership of cdaf8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMe18../2967a.. ownership of c8b63.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPuM../a2862.. ownership of 016fc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPiN../867cc.. ownership of 4861f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQkp../5a7b2.. ownership of 33353.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGRA../07221.. ownership of 47a1e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW2Y../c903d.. ownership of e0e40.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFmT../a5ffc.. ownership of 879a5.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQjY../b1feb.. ownership of 2b2e3.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXYu../467c3.. ownership of 2cc21.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcQf../38c53.. ownership of d2155.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMU9q../d7079.. ownership of b4394.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM9p../5c42b.. ownership of 00287.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNmY../fb072.. ownership of 02231.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQPP../02bb9.. ownership of e3162.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPBx../ad41f.. ownership of 6571a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJGZ../39017.. ownership of eb53d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS9n../47505.. ownership of efd72.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVFE../a4e09.. ownership of f482f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdEk../a3ef7.. ownership of 03db1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJT4../4f1c2.. ownership of 0fc90.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFwH../45419.. ownership of f0179.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZpy../7f5e0.. ownership of 25755.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPxQ../e4831.. ownership of 2e184.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJJd../b3cee.. ownership of 76607.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaew../b77f1.. ownership of 74625.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZYh../57fac.. ownership of 38062.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJpZ../24bed.. ownership of ba4a2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJH4../f1ef4.. ownership of b5c9f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaER../440f9.. ownership of c045b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFA4../21ce7.. ownership of 3097a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbZa../572df.. ownership of eca70.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdjH../e4ba1.. ownership of 6b93f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSbD../f0024.. ownership of 937fe.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN1c../f61cb.. ownership of cad8f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM7V../e1ada.. ownership of ddd00.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQaJ../19b93.. ownership of ac767.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZBd../e6b36.. ownership of cd5eb.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUTo6../1811f.. doc published by PrGxv..
Param a842e.. : ι → (ι → ι) → ι
Param 94f9e.. : ι → (ι → ι) → ι
Param aae7a.. : ι → ι → ι
Definition 0fc90.. := λ x0 . λ x1 : ι → ι . a842e.. x0 (λ x2 . 94f9e.. (x1 x2) (aae7a.. x2))
Known 2236b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 x0 ⟶ prim1 x3 (x1 x2) ⟶ prim1 x3 (a842e.. x0 x1)
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem f5701.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 (x1 x2) ⟶ prim1 (aae7a.. x2 x3) (0fc90.. x0 x1) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param e76d4.. : ι → ι
Param 22ca9.. : ι → ι
Known exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known 5dd0a.. : ∀ x0 x1 . e76d4.. (aae7a.. x0 x1) = x0
Known 40190.. : ∀ x0 x1 . 22ca9.. (aae7a.. x0 x1) = x1
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known 042d7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (a842e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (prim1 x2 (x1 x4)) ⟶ x3) ⟶ x3
Theorem 016fc.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ and (and (aae7a.. (e76d4.. x2) (22ca9.. x2) = x2) (prim1 (e76d4.. x2) x0)) (prim1 (22ca9.. x2) (x1 (e76d4.. x2))) (proof)
Known and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem cdaf8.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ aae7a.. (e76d4.. x2) (22ca9.. x2) = x2 (proof)
Theorem a268e.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (e76d4.. x2) x0 (proof)
Theorem cbf3e.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (22ca9.. x2) (x1 (e76d4.. x2)) (proof)
Theorem 5d5fc.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 (aae7a.. x2 x3) (0fc90.. x0 x1) ⟶ prim1 x2 x0 (proof)
Theorem e2bb7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 (aae7a.. x2 x3) (0fc90.. x0 x1) ⟶ prim1 x3 (x1 x2) (proof)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 7d8a1.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (∀ x5 : ο . (∀ x6 . and (prim1 x6 (x1 x4)) (x2 = aae7a.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Definition iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem 9b331.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (prim1 x2 (0fc90.. x0 x1)) (∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (∀ x5 : ο . (∀ x6 . and (prim1 x6 (x1 x4)) (x2 = aae7a.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) (proof)
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Theorem 690be.. : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 x3 : ι → ι . (∀ x4 . prim1 x4 x0 ⟶ Subq (x2 x4) (x3 x4)) ⟶ Subq (0fc90.. x0 x2) (0fc90.. x1 x3) (proof)
Known Subq_ref : ∀ x0 . Subq x0 x0
Theorem d3673.. : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 : ι → ι . Subq (0fc90.. x0 x2) (0fc90.. x1 x2) (proof)
Theorem f42b8.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ Subq (x1 x3) (x2 x3)) ⟶ Subq (0fc90.. x0 x1) (0fc90.. x0 x2) (proof)
Param e5b72.. : ι → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Known 3daee.. : ∀ x0 x1 . Subq x1 x0 ⟶ prim1 x1 (e5b72.. x0)
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Known 7144c.. : aae7a.. 4a7ef.. 4a7ef.. = 4a7ef..
Param 91630.. : ι → ι
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0
Known 30652.. : Subq (4ae4a.. 4a7ef..) (91630.. 4a7ef..)
Known b21da.. : ∀ x0 x1 . prim1 x1 (e5b72.. x0) ⟶ Subq x1 x0
Theorem 2ad56.. : ∀ x0 . prim1 x0 (e5b72.. (4ae4a.. 4a7ef..)) ⟶ ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (e5b72.. (4ae4a.. 4a7ef..))) ⟶ prim1 (0fc90.. x0 x1) (e5b72.. (4ae4a.. 4a7ef..)) (proof)
Definition ac767.. := λ x0 x1 . 0fc90.. x0 (λ x2 . x1)
Theorem c5caa.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ prim1 (aae7a.. x2 x3) (ac767.. x0 x1) (proof)
Theorem 8f68d.. : ∀ x0 x1 x2 . prim1 x2 (ac767.. x0 x1) ⟶ prim1 (e76d4.. x2) x0 (proof)
Theorem fd5b7.. : ∀ x0 x1 x2 . prim1 x2 (ac767.. x0 x1) ⟶ prim1 (22ca9.. x2) x1 (proof)
Theorem 713d5.. : ∀ x0 x1 x2 x3 . prim1 (aae7a.. x2 x3) (ac767.. x0 x1) ⟶ prim1 x2 x0 (proof)
Theorem 4949d.. : ∀ x0 x1 x2 x3 . prim1 (aae7a.. x2 x3) (ac767.. x0 x1) ⟶ prim1 x3 x1 (proof)
Param a4c2a.. : ι → (ι → ο) → (ι → ι) → ι
Definition f482f.. := λ x0 x1 . a4c2a.. x0 (λ x2 . ∀ x3 : ο . (∀ x4 . x2 = aae7a.. x1 x4 ⟶ x3) ⟶ x3) 22ca9..
Theorem f5701.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 (x1 x2) ⟶ prim1 (aae7a.. x2 x3) (0fc90.. x0 x1) (proof)
Theorem 7d8a1.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (∀ x5 : ο . (∀ x6 . and (prim1 x6 (x1 x4)) (x2 = aae7a.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Theorem 9b331.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (prim1 x2 (0fc90.. x0 x1)) (∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (∀ x5 : ο . (∀ x6 . and (prim1 x6 (x1 x4)) (x2 = aae7a.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) (proof)
Known e951d.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 x0 ⟶ x1 x3 ⟶ prim1 (x2 x3) (a4c2a.. x0 x1 x2)
Theorem aa929.. : ∀ x0 x1 x2 . prim1 (aae7a.. x1 x2) x0 ⟶ prim1 x2 (f482f.. x0 x1) (proof)
Known 932b3.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 (a4c2a.. x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . prim1 x5 x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Theorem 2a2bc.. : ∀ x0 x1 x2 . prim1 x2 (f482f.. x0 x1) ⟶ prim1 (aae7a.. x1 x2) x0 (proof)
Theorem 69f30.. : ∀ x0 x1 x2 . iff (prim1 x2 (f482f.. x0 x1)) (prim1 (aae7a.. x1 x2) x0) (proof)
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Theorem f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2 (proof)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known 3c674.. : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 4a7ef..
Theorem 9e5b2.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nIn x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = 4a7ef.. (proof)
Known a6d0f.. : ∀ x0 x1 . prim1 x1 (e76d4.. x0) ⟶ prim1 (aae7a.. 4a7ef.. x1) x0
Known 2ef56.. : ∀ x0 x1 . prim1 (aae7a.. 4a7ef.. x1) x0 ⟶ prim1 x1 (e76d4.. x0)
Theorem 76a87.. : ∀ x0 . e76d4.. x0 = f482f.. x0 4a7ef.. (proof)
Known 98a9e.. : ∀ x0 x1 . prim1 x1 (22ca9.. x0) ⟶ prim1 (aae7a.. (4ae4a.. 4a7ef..) x1) x0
Known 36427.. : ∀ x0 x1 . prim1 (aae7a.. (4ae4a.. 4a7ef..) x1) x0 ⟶ prim1 x1 (22ca9.. x0)
Theorem 0ba89.. : ∀ x0 . 22ca9.. x0 = f482f.. x0 (4ae4a.. 4a7ef..) (proof)
Theorem 3f040.. : ∀ x0 x1 . f482f.. (aae7a.. x0 x1) 4a7ef.. = x0 (proof)
Theorem a283f.. : ∀ x0 x1 . f482f.. (aae7a.. x0 x1) (4ae4a.. 4a7ef..) = x1 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known 2f64c.. : ∀ x0 x1 x2 . prim1 x2 (aae7a.. x0 x1) ⟶ or (∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (x2 = aae7a.. 4a7ef.. x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (prim1 x4 x1) (x2 = aae7a.. (4ae4a.. 4a7ef..) x4) ⟶ x3) ⟶ x3)
Known cf31f.. : ∀ x0 x1 x2 x3 . aae7a.. x0 x1 = aae7a.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Known 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..))
Theorem a7149.. : ∀ x0 x1 x2 . nIn x2 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ f482f.. (aae7a.. x0 x1) x2 = 4a7ef.. (proof)
Theorem 33e74.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (f482f.. x2 4a7ef..) x0 (proof)
Theorem 35b50.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (f482f.. x2 (4ae4a.. 4a7ef..)) (x1 (f482f.. x2 4a7ef..)) (proof)
Definition cad8f.. := λ x0 . aae7a.. (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..)) = x0
Theorem 73bc9.. : ∀ x0 x1 . cad8f.. (aae7a.. x0 x1) (proof)
Known 2532b.. : ∀ x0 x1 x2 . prim1 x0 (prim2 x1 x2) ⟶ or (x0 = x1) (x0 = x2)
Known 4b3cb.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 (aae7a.. 4a7ef.. x2) (aae7a.. x0 x1)
Known 2391b.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 (aae7a.. (4ae4a.. 4a7ef..) x2) (aae7a.. x0 x1)
Known 2ea0c.. : Subq (4ae4a.. (4ae4a.. 4a7ef..)) (prim2 4a7ef.. (4ae4a.. 4a7ef..))
Theorem dcd87.. : ∀ x0 . (∀ x1 . prim1 x1 x0 ⟶ and (cad8f.. x1) (prim1 (f482f.. x1 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ cad8f.. x0 (proof)
Theorem dfdb3.. : ∀ x0 x1 . cad8f.. x0 ⟶ prim1 x0 x1 ⟶ prim1 (f482f.. x0 (4ae4a.. 4a7ef..)) (f482f.. x1 (f482f.. x0 4a7ef..)) (proof)
Definition 6b93f.. := λ x0 x1 . ∀ x2 . prim1 x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (∀ x5 : ο . (∀ x6 . x2 = aae7a.. x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Theorem 7d7d0.. : cad8f.. = 6b93f.. (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Param If_i : ο → ι → ι → ι
Theorem d9414.. : ∀ x0 x1 . 6b93f.. (4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 x1)) (proof)
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known 5c667.. : 4ae4a.. 4a7ef.. = 4a7ef.. ⟶ ∀ x0 : ο . x0
Theorem f71c6.. : ∀ x0 x1 . aae7a.. x0 x1 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1) (proof)
Param 1216a.. : ι → (ι → ο) → ι
Definition 3097a.. := λ x0 . λ x1 : ι → ι . 1216a.. (e5b72.. (0fc90.. x0 (λ x2 . prim3 (x1 x2)))) (λ x2 . ∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3))
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Known UnionI : ∀ x0 x1 x2 . prim1 x1 x2 ⟶ prim1 x2 x0 ⟶ prim1 x1 (prim3 x0)
Theorem 8d403.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . prim1 x3 x2 ⟶ and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0)) ⟶ (∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3)) ⟶ prim1 x2 (3097a.. x0 x1) (proof)
Known 6982e.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ and (prim1 x2 x0) (x1 x2)
Theorem 85578.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (3097a.. x0 x1) ⟶ and (∀ x3 . prim1 x3 x2 ⟶ and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0)) (∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3)) (proof)
Theorem 5795e.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (prim1 x2 (3097a.. x0 x1)) (and (∀ x3 . prim1 x3 x2 ⟶ and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0)) (∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3))) (proof)
Theorem 27474.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) (x1 x3)) ⟶ prim1 (0fc90.. x0 x2) (3097a.. x0 x1) (proof)
Known ac5c1.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ x1 x2
Theorem d8d74.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 (3097a.. x0 x1) ⟶ prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3) (proof)
Theorem cce19.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (3097a.. x0 x1) ⟶ ∀ x3 . prim1 x3 (3097a.. x0 x1) ⟶ (∀ x4 . prim1 x4 x0 ⟶ Subq (f482f.. x2 x4) (f482f.. x3 x4)) ⟶ Subq x2 x3 (proof)
Theorem 6e275.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (3097a.. x0 x1) ⟶ ∀ x3 . prim1 x3 (3097a.. x0 x1) ⟶ (∀ x4 . prim1 x4 x0 ⟶ f482f.. x2 x4 = f482f.. x3 x4) ⟶ x2 = x3 (proof)
Theorem 34894.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (3097a.. x0 x1) ⟶ 0fc90.. x0 (f482f.. x2) = x2 (proof)
Definition b5c9f.. := λ x0 x1 . 3097a.. x1 (λ x2 . x0)
Theorem 204eb.. : aae7a.. = λ x1 x2 . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x1 x2) (proof)
Theorem 1cc2a.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 (x1 x2) ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . If_i (x4 = 4a7ef..) x2 x3)) (0fc90.. x0 x1) (proof)
Theorem 8c3eb.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (∀ x5 : ο . (∀ x6 . and (prim1 x6 (x1 x4)) (x2 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x8 . If_i (x8 = 4a7ef..) x4 x6)) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Theorem 2d4b0.. : ∀ x0 x1 x2 x3 . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x0 x1) = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x2 x3) ⟶ and (x0 = x2) (x1 = x3) (proof)
Theorem 6f2e8.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) 4a7ef.. = x0 (proof)
Theorem 15d37.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) (4ae4a.. 4a7ef..) = x1 (proof)
Definition 38062.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . 1216a.. (0fc90.. x0 x1) (λ x3 . x2 (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..)))
Theorem 380ca.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 (x1 x3) ⟶ x2 x3 x4 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x3 x4)) (38062.. x0 x1 x2) (proof)
Theorem fbd31.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . prim1 x3 (38062.. x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (∀ x6 : ο . (∀ x7 . and (prim1 x7 (x1 x5)) (and (x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x9 . If_i (x9 = 4a7ef..) x5 x7)) (x2 x5 x7)) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4 (proof)
Theorem 0d9ad.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x3 x4)) (38062.. x0 x1 x2) ⟶ and (and (prim1 x3 x0) (prim1 x4 (x1 x3))) (x2 x3 x4) (proof)
Theorem 41662.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x3 x4)) (38062.. x0 x1 x2) ⟶ prim1 x3 x0 (proof)
Theorem 36b09.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x3 x4)) (38062.. x0 x1 x2) ⟶ prim1 x4 (x1 x3) (proof)
Theorem 338b2.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x3 x4)) (38062.. x0 x1 x2) ⟶ x2 x3 x4 (proof)
Definition 76607.. := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ ∀ x2 : ο . (∀ x3 . (∀ x4 : ο . (∀ x5 . x1 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x7 . If_i (x7 = 4a7ef..) x3 x5) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2
Theorem 78561.. : ∀ x0 x1 . 76607.. x0 ⟶ 76607.. x1 ⟶ (∀ x2 x3 . iff (prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . If_i (x4 = 4a7ef..) x2 x3)) x0) (prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . If_i (x4 = 4a7ef..) x2 x3)) x1)) ⟶ x0 = x1 (proof)
Theorem f6f3f.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . 76607.. (38062.. x0 x1 x2) (proof)
Theorem 5af6c.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ο . (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 (x1 x4) ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ 38062.. x0 x1 x2 = 38062.. x0 x1 x3 (proof)
Theorem a850e.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ Subq (0fc90.. x0 x1) (0fc90.. x0 x2) (proof)
Theorem 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2 (proof)
Theorem 7e4c2.. : ∀ x0 . ∀ x1 : ι → ι . 0fc90.. x0 (f482f.. (0fc90.. x0 x1)) = 0fc90.. x0 x1 (proof)
Theorem bcb22.. : ∀ x0 x1 . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1))) = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1) (proof)
Definition 25755.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι . 0fc90.. x0 (λ x3 . 0fc90.. (x1 x3) (x2 x3))
Theorem 1b91d.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 (x1 x3) ⟶ f482f.. (f482f.. (25755.. x0 x1 x2) x3) x4 = x2 x3 x4 (proof)
Theorem ed27c.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 (x1 x4) ⟶ x2 x4 x5 = x3 x4 x5) ⟶ 25755.. x0 x1 x2 = 25755.. x0 x1 x3 (proof)
Definition 0fc90.. := 0fc90..
Definition f482f.. := f482f..
Definition eb53d.. := λ x0 . 25755.. x0 (λ x1 . x0)
Definition e3162.. := λ x0 x1 . f482f.. (f482f.. x0 x1)
Definition 1216a.. := 1216a..
Definition decode_p := λ x0 x1 . prim1 x1 x0
Definition d2155.. := λ x0 . 38062.. x0 (λ x1 . x0)
Definition 2b2e3.. := λ x0 x1 x2 . prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x1 x2)) x0
Definition e0e40.. := λ x0 . λ x1 : (ι → ο) → ο . 1216a.. (e5b72.. x0) (λ x2 . x1 (λ x3 . prim1 x3 x2))
Definition decode_c := λ x0 . λ x1 : ι → ο . ∀ x2 : ο . (∀ x3 . and (∀ x4 . iff (x1 x4) (prim1 x4 x3)) (prim1 x3 x0) ⟶ x2) ⟶ x2
Theorem f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2 (proof)
Theorem 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2 (proof)
Theorem 35054.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ e3162.. (eb53d.. x0 x1) x2 x3 = x1 x2 x3 (proof)
Theorem 8fdaf.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ eb53d.. x0 x1 = eb53d.. x0 x2 (proof)
Known prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2 (proof)
Theorem ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2 (proof)
Theorem 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ 2b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3 (proof)
Theorem 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 (proof)
Known d129e.. : ∀ x0 . ∀ x1 : ι → ο . prim1 (1216a.. x0 x1) (e5b72.. x0)
Theorem 81500.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . (∀ x3 . x2 x3 ⟶ prim1 x3 x0) ⟶ decode_c (e0e40.. x0 x1) x2 = x1 x2 (proof)
Theorem fe043.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . (∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ prim1 x4 x0) ⟶ iff (x1 x3) (x2 x3)) ⟶ e0e40.. x0 x1 = e0e40.. x0 x2 (proof)