Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrGgN../c07ce..
PULFk../3e829..
vout
PrGgN../ec455.. 9.99 bars
TMKTM../11f08.. ownership of 938bf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFyR../ed0f2.. ownership of bea85.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMDq../f605a.. ownership of 69516.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYYe../6d4dd.. ownership of 33d09.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbdC../c0426.. ownership of b3e73.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW5M../ca612.. ownership of 7712c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLAn../95738.. ownership of 5c3bc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHWP../9e526.. ownership of f4fce.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYWs../d0677.. ownership of 48a34.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN4W../fb7f3.. ownership of c91e3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGz7../79220.. ownership of b3c31.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbqT../e9ee2.. ownership of 89255.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUJK../e6b3b.. ownership of 2a51d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLLA../192c7.. ownership of 26941.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTx3../86b2b.. ownership of 76505.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUCn../81e48.. ownership of a619e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcpJ../15a16.. ownership of 78a8c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVoP../35376.. ownership of c24f7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGQU../cfd4e.. ownership of fd378.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMrC../dbb83.. ownership of b476b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRDr../1daf9.. ownership of 119c2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVrv../98db0.. ownership of fe832.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcYU../8bcfb.. ownership of e80db.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQux../802e5.. ownership of 1c403.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJBX../a3d53.. ownership of 89e73.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYCY../57187.. ownership of 2c8a6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP4w../0a82a.. ownership of 0d3cc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFBQ../eedcd.. ownership of d754e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ9P../060d8.. ownership of 61567.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdEF../0e4a5.. ownership of 9475f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPCV../4ff20.. ownership of 4755f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGk9../854f4.. ownership of 03874.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFmy../835e0.. ownership of 51deb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb5W../6d6be.. ownership of dd0e5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXHY../9a6d4.. ownership of 2f936.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYXa../edb35.. ownership of 5deaa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMckw../9f068.. ownership of b0689.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFKx../89dd8.. ownership of 03261.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbUt../705dd.. ownership of b69b2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH5u../11a23.. ownership of b6030.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGTB../aeeff.. ownership of eabbd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK66../17937.. ownership of 349b0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUbt../3cbb2.. ownership of 3fc2d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMMh../067b8.. ownership of 26c09.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSDA../94986.. ownership of 7b60c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJTs../30ac7.. ownership of 3d219.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPC1../95b21.. ownership of bd057.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMZW../64b36.. ownership of 580e8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNHU../4c145.. ownership of b818c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR94../0c50a.. ownership of 9c5d9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQZP../2f3c4.. ownership of 66eb4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWmY../7f8be.. ownership of 7708a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNZr../d2c1a.. ownership of 8da93.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM3e../bdfd7.. ownership of 63c45.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFGS../56a91.. ownership of a089c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGAJ../01152.. ownership of 53a14.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMctJ../2ba34.. ownership of 6d1ab.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJuP../543cd.. ownership of 25c4d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZs9../beb96.. ownership of 2b25e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd2x../bb601.. ownership of fddcf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc1K../051f8.. ownership of 9353f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVWZ../c628d.. ownership of dcaac.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb2A../44dfb.. ownership of 20b3f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdWf../bbecc.. ownership of 9f545.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRZb../befb1.. ownership of 5c7ca.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG5w../f20ba.. ownership of 10fd3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMddg../597a4.. ownership of c0e69.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaEZ../541a3.. ownership of 0e8be.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK4R../e5a53.. ownership of 6b633.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHqt../c4d47.. ownership of ef674.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKgE../f266f.. ownership of f600a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQMi../f02c0.. ownership of 2f9f1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMceE../bddcc.. ownership of 7b502.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQkT../876fd.. ownership of 66153.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRnX../65615.. ownership of dc48a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMans../87180.. ownership of 1524b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcbf../a3ec3.. ownership of dc4aa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJ8e../a8217.. ownership of f6946.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQBD../e02eb.. ownership of 923f0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPm7../312b2.. ownership of 4712b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSK1../3d774.. ownership of ae098.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWhJ../e21d3.. ownership of e27ee.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb9S../98fb8.. ownership of 0041c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQxr../99279.. ownership of 52bd6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXSN../3df18.. ownership of 9fde6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcu7../cfd03.. ownership of 458eb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcDW../3cae0.. ownership of 4b77a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFtW../c94a5.. ownership of 764ac.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFDA../aabab.. ownership of 17a28.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGpK../23e1b.. ownership of 1f733.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMawK../01455.. ownership of 8aa5c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbyn../77db4.. ownership of 978ca.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGmF../b5b68.. ownership of f43cf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGYb../821d8.. ownership of 4c550.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTKj../8ce95.. ownership of 12038.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJpu../1556e.. ownership of 4c0d5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMab8../83fb9.. ownership of d05db.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUVK../ab061.. ownership of 3faaf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaFE../f4810.. ownership of aa00f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWFZ../7f86a.. ownership of 1194c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFds../e4b62.. ownership of f4cca.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLFB../6ec56.. ownership of 971a2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMVR../a461e.. ownership of 9757d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF53../1450c.. ownership of e7798.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZXV../342eb.. ownership of 880ae.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYyc../0eaf0.. ownership of 3b475.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNLR../f68e8.. ownership of e5fea.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMVu../ab619.. ownership of c66e3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcLa../dddcd.. ownership of 1da29.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM7T../949b8.. ownership of 29ae1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML7E../dbf29.. ownership of 9867d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbAp../c2838.. ownership of 2b6e3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFvg../3b947.. ownership of 620b0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb9Z../593ea.. ownership of 98b44.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUkR../9eca7.. ownership of 47b2a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTnM../25a5c.. ownership of aca85.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXgV../7a87a.. ownership of 36fd9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVFn../36790.. ownership of 8ea88.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdew../3f224.. ownership of cec89.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXxp../75a4c.. ownership of 7bd5c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFG9../c4e6c.. ownership of d83ec.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVs4../cd255.. ownership of 3f236.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd7R../79699.. ownership of 9565e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQMB../17748.. ownership of 99bcd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP5P../11f1e.. ownership of dcb35.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPeN../be651.. ownership of 81d00.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXAw../11df4.. ownership of be260.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFzN../b84ab.. ownership of c7a7e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd7s../e0c72.. ownership of 8a21b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMLg../4b6a0.. ownership of e7d84.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLw1../7f108.. ownership of 44ab7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZVn../d05eb.. ownership of d86bb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLox../a726b.. ownership of 4c1a8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSF6../d0e0b.. ownership of a07b2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFDD../73deb.. ownership of e1cfe.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT1Q../cc0ad.. ownership of 8cc96.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH6p../831bf.. ownership of f28c1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTJj../05f05.. ownership of 5af65.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb2x../a0bf5.. ownership of b24dc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT7U../6f0fa.. ownership of ceb24.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbja../9c6fb.. ownership of bcc00.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZyS../a11bb.. ownership of 3b13d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHxx../078a6.. ownership of 155f9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTDo../2caf0.. ownership of d0c01.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS3S../79dd1.. ownership of 691ba.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH8j../294b0.. ownership of 56550.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP2L../0db44.. ownership of b56ab.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGJn../6edfc.. ownership of a6aee.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdci../a48f2.. ownership of 7492d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT2H../9a384.. ownership of 007f1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNvj../c3cb6.. ownership of 4cd9f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHWa../93007.. ownership of 0a543.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN6Y../b6ef6.. ownership of df6a8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZPQ../6e258.. ownership of a2dad.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFDP../3367c.. ownership of f593b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTdK../71475.. ownership of 8b8b7.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWh1../9b2b2.. ownership of d8d01.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdKP../63a54.. ownership of 76168.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJ4E../46fe6.. ownership of f9779.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbHt../ff814.. ownership of 951fb.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGtp../577cf.. ownership of 7811e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML5e../5ea9f.. ownership of ab52c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKna../c121e.. ownership of 014dd.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN6P../dfa2e.. ownership of b6d8e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGn6../97690.. ownership of 30bff.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMavv../29dab.. ownership of 6a9d2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQZN../6ab08.. ownership of 6c446.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ8o../c589f.. ownership of 6ad32.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbXp../57bba.. ownership of 26d87.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNvn../fde1c.. ownership of 9845d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTbL../8cb50.. ownership of b67a0.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW6Q../c4886.. ownership of f4445.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUpn../ef95e.. ownership of eb2d9.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKS2../ae2b3.. ownership of d6368.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKiq../456e8.. ownership of 2fe05.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKTU../f0e95.. ownership of c44f4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSug../6d2af.. ownership of 13026.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSEL../15228.. ownership of 705c2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcTV../1dd0d.. ownership of 49755.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTqU../cc3e0.. ownership of 7396b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGpp../45936.. ownership of c7ccc.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUrV../16571.. ownership of 068ee.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJwF../88b5c.. ownership of c1732.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMa1../34d93.. ownership of b3c3c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGTx../23ac9.. ownership of 1fdeb.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLmK../86922.. ownership of 94837.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaPq../db01c.. ownership of 9a300.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGA1../74e4f.. ownership of 9f8e3.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXQM../2c0fa.. ownership of 17e9f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFDZ../82704.. ownership of fa6c5.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUTqi../97867.. doc published by PrGxv..
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Param e0e40.. : ι → ((ι → ο) → ο) → ι
Param d2155.. : ι → (ι → ι → ο) → ι
Definition 17e9f.. := λ x0 . λ x1 : (ι → ο) → ο . λ x2 : ι → ι . λ x3 : ι → ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (e0e40.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. x0 x2) (d2155.. x0 x3))))
Param f482f.. : ι → ι → ι
Known 9f6be.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) 4a7ef.. = x0
Theorem 7492d.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . x0 = 17e9f.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem b56ab.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . x4 x0 (f482f.. (17e9f.. x0 x1 x2 x3) 4a7ef..) ⟶ x4 (f482f.. (17e9f.. x0 x1 x2 x3) 4a7ef..) x0 (proof)
Param decode_c : ι → (ι → ο) → ο
Known 8a328.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. 4a7ef..) = x1
Known 81500.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . (∀ x3 . x2 x3 ⟶ prim1 x3 x0) ⟶ decode_c (e0e40.. x0 x1) x2 = x1 x2
Theorem 691ba.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . x0 = 17e9f.. x1 x2 x3 x4 ⟶ ∀ x5 : ι → ο . (∀ x6 . x5 x6 ⟶ prim1 x6 x1) ⟶ x2 x5 = decode_c (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 155f9.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x0) ⟶ x1 x4 = decode_c (f482f.. (17e9f.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Known 142e6.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem bcc00.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . x0 = 17e9f.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x3 x5 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem b24dc.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . prim1 x4 x0 ⟶ x2 x4 = f482f.. (f482f.. (17e9f.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 (proof)
Param 2b2e3.. : ι → ι → ι → ο
Known 62a6b.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3
Known 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ 2b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3
Theorem f28c1.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . x0 = 17e9f.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 x6 (proof)
Theorem e1cfe.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x3 x4 x5 = 2b2e3.. (f482f.. (17e9f.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Theorem 4c1a8.. : ∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . ∀ x4 x5 : ι → ι . ∀ x6 x7 : ι → ι → ο . 17e9f.. x0 x2 x4 x6 = 17e9f.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 : ι → ο . (∀ x9 . x8 x9 ⟶ prim1 x9 x0) ⟶ x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0 ⟶ x4 x8 = x5 x8)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x6 x8 x9 = x7 x8 x9) (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
Known fe043.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . (∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ prim1 x4 x0) ⟶ iff (x1 x3) (x2 x3)) ⟶ e0e40.. x0 x1 = e0e40.. x0 x2
Theorem 44ab7.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . ∀ x3 x4 : ι → ι . ∀ x5 x6 : ι → ι → ο . (∀ x7 : ι → ο . (∀ x8 . x7 x8 ⟶ prim1 x8 x0) ⟶ iff (x1 x7) (x2 x7)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ x3 x7 = x4 x7) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x5 x7 x8) (x6 x7 x8)) ⟶ 17e9f.. x0 x1 x3 x5 = 17e9f.. x0 x2 x4 x6 (proof)
Definition 9a300.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : (ι → ο) → ο . ∀ x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ prim1 (x4 x5) x2) ⟶ ∀ x5 : ι → ι → ο . x1 (17e9f.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem 8a21b.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x0) ⟶ ∀ x3 : ι → ι → ο . 9a300.. (17e9f.. x0 x1 x2 x3) (proof)
Theorem be260.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . 9a300.. (17e9f.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x4) x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem dcb35.. : ∀ x0 . 9a300.. x0 ⟶ x0 = 17e9f.. (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 1fdeb.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ι) → (ι → ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 9565e.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ι) → (ι → ι → ο) → ι . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x3 x7 = x6 x7) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x4 x8 x9) (x7 x8 x9)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ 1fdeb.. (17e9f.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition c1732.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ι) → (ι → ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem d83ec.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ι) → (ι → ι → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x3 x7 = x6 x7) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x4 x8 x9) (x7 x8 x9)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ c1732.. (17e9f.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Param 1216a.. : ι → (ι → ο) → ι
Definition c7ccc.. := λ x0 . λ x1 : (ι → ο) → ο . λ x2 : ι → ι . λ x3 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (e0e40.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. x0 x2) (1216a.. x0 x3))))
Theorem cec89.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ο . x0 = c7ccc.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 36fd9.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ο . x0 = f482f.. (c7ccc.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 47b2a.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ο . x0 = c7ccc.. x1 x2 x3 x4 ⟶ ∀ x5 : ι → ο . (∀ x6 . x5 x6 ⟶ prim1 x6 x1) ⟶ x2 x5 = decode_c (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 620b0.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x0) ⟶ x1 x4 = decode_c (f482f.. (c7ccc.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Theorem 9867d.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ο . x0 = c7ccc.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x3 x5 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem 1da29.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ x2 x4 = f482f.. (f482f.. (c7ccc.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 (proof)
Param decode_p : ι → ι → ο
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem e5fea.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ο . x0 = c7ccc.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x4 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem 880ae.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ x3 x4 = decode_p (f482f.. (c7ccc.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (proof)
Theorem 9757d.. : ∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . ∀ x4 x5 : ι → ι . ∀ x6 x7 : ι → ο . c7ccc.. x0 x2 x4 x6 = c7ccc.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 : ι → ο . (∀ x9 . x8 x9 ⟶ prim1 x9 x0) ⟶ x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0 ⟶ x4 x8 = x5 x8)) (∀ x8 . prim1 x8 x0 ⟶ x6 x8 = x7 x8) (proof)
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
Theorem f4cca.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . ∀ x3 x4 : ι → ι . ∀ x5 x6 : ι → ο . (∀ x7 : ι → ο . (∀ x8 . x7 x8 ⟶ prim1 x8 x0) ⟶ iff (x1 x7) (x2 x7)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ x3 x7 = x4 x7) ⟶ (∀ x7 . prim1 x7 x0 ⟶ iff (x5 x7) (x6 x7)) ⟶ c7ccc.. x0 x1 x3 x5 = c7ccc.. x0 x2 x4 x6 (proof)
Definition 49755.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : (ι → ο) → ο . ∀ x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ prim1 (x4 x5) x2) ⟶ ∀ x5 : ι → ο . x1 (c7ccc.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem aa00f.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x0) ⟶ ∀ x3 : ι → ο . 49755.. (c7ccc.. x0 x1 x2 x3) (proof)
Theorem d05db.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ο . 49755.. (c7ccc.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x4) x0 (proof)
Theorem 12038.. : ∀ x0 . 49755.. x0 ⟶ x0 = c7ccc.. (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 13026.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ι) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem f43cf.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ι) → (ι → ο) → ι . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ο . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x3 x7 = x6 x7) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x4 x8) (x7 x8)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ 13026.. (c7ccc.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 2fe05.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ι) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 8aa5c.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ι) → (ι → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ο . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x3 x7 = x6 x7) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x4 x8) (x7 x8)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ 2fe05.. (c7ccc.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition eb2d9.. := λ x0 . λ x1 : (ι → ο) → ο . λ x2 : ι → ι . λ x3 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (e0e40.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (0fc90.. x0 x2) x3)))
Theorem 17a28.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 . x0 = eb2d9.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 4b77a.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 . x0 = f482f.. (eb2d9.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 9fde6.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 . x0 = eb2d9.. x1 x2 x3 x4 ⟶ ∀ x5 : ι → ο . (∀ x6 . x5 x6 ⟶ prim1 x6 x1) ⟶ x2 x5 = decode_c (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 0041c.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x0) ⟶ x1 x4 = decode_c (f482f.. (eb2d9.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Theorem ae098.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 . x0 = eb2d9.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x3 x5 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem 923f0.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 x4 . prim1 x4 x0 ⟶ x2 x4 = f482f.. (f482f.. (eb2d9.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 (proof)
Theorem dc4aa.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 . x0 = eb2d9.. x1 x2 x3 x4 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem dc48a.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 . x3 = f482f.. (eb2d9.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 7b502.. : ∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . ∀ x4 x5 : ι → ι . ∀ x6 x7 . eb2d9.. x0 x2 x4 x6 = eb2d9.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 : ι → ο . (∀ x9 . x8 x9 ⟶ prim1 x9 x0) ⟶ x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0 ⟶ x4 x8 = x5 x8)) (x6 = x7) (proof)
Theorem f600a.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . ∀ x3 x4 : ι → ι . ∀ x5 . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x0) ⟶ iff (x1 x6) (x2 x6)) ⟶ (∀ x6 . prim1 x6 x0 ⟶ x3 x6 = x4 x6) ⟶ eb2d9.. x0 x1 x3 x5 = eb2d9.. x0 x2 x4 x5 (proof)
Definition b67a0.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : (ι → ο) → ο . ∀ x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ prim1 (x4 x5) x2) ⟶ ∀ x5 . prim1 x5 x2 ⟶ x1 (eb2d9.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem 6b633.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x0) ⟶ ∀ x3 . prim1 x3 x0 ⟶ b67a0.. (eb2d9.. x0 x1 x2 x3) (proof)
Theorem c0e69.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 . b67a0.. (eb2d9.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x4) x0 (proof)
Theorem 5c7ca.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι . ∀ x3 . b67a0.. (eb2d9.. x0 x1 x2 x3) ⟶ prim1 x3 x0 (proof)
Theorem 20b3f.. : ∀ x0 . b67a0.. x0 ⟶ x0 = eb2d9.. (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition 26d87.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ι) → ι → ι . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 9353f.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ι) → ι → ι . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x3 x7 = x6 x7) ⟶ x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4) ⟶ 26d87.. (eb2d9.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 6c446.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ι) → ι → ο . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 2b25e.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ι) → ι → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι . ∀ x4 . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . prim1 x7 x1 ⟶ x3 x7 = x6 x7) ⟶ x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4) ⟶ 6c446.. (eb2d9.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 30bff.. := λ x0 . λ x1 : (ι → ο) → ο . λ x2 : ι → ι → ο . λ x3 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (e0e40.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) (1216a.. x0 x3))))
Theorem 6d1ab.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 30bff.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem a089c.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . x0 = f482f.. (30bff.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 8da93.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 30bff.. x1 x2 x3 x4 ⟶ ∀ x5 : ι → ο . (∀ x6 . x5 x6 ⟶ prim1 x6 x1) ⟶ x2 x5 = decode_c (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 66eb4.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x0) ⟶ x1 x4 = decode_c (f482f.. (30bff.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Theorem b818c.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 30bff.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem bd057.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = 2b2e3.. (f482f.. (30bff.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem 7b60c.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 30bff.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x4 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem 3fc2d.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ x3 x4 = decode_p (f482f.. (30bff.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (proof)
Theorem eabbd.. : ∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . ∀ x4 x5 : ι → ι → ο . ∀ x6 x7 : ι → ο . 30bff.. x0 x2 x4 x6 = 30bff.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 : ι → ο . (∀ x9 . x8 x9 ⟶ prim1 x9 x0) ⟶ x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ x6 x8 = x7 x8) (proof)
Theorem b69b2.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . ∀ x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . (∀ x7 : ι → ο . (∀ x8 . x7 x8 ⟶ prim1 x8 x0) ⟶ iff (x1 x7) (x2 x7)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x3 x7 x8) (x4 x7 x8)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ iff (x5 x7) (x6 x7)) ⟶ 30bff.. x0 x1 x3 x5 = 30bff.. x0 x2 x4 x6 (proof)
Definition 014dd.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : (ι → ο) → ο . ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x1 (30bff.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem b0689.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . 014dd.. (30bff.. x0 x1 x2 x3) (proof)
Theorem 2f936.. : ∀ x0 . 014dd.. x0 ⟶ x0 = 30bff.. (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 7811e.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ι → ο) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 51deb.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ι → ο) → (ι → ο) → ι . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x3 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x4 x8) (x7 x8)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ 7811e.. (30bff.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition f9779.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ι → ο) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 4755f.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ι → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x3 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x4 x8) (x7 x8)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ f9779.. (30bff.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition d8d01.. := λ x0 . λ x1 : (ι → ο) → ο . λ x2 : ι → ι → ο . λ x3 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (e0e40.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) x3)))
Theorem 61567.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = d8d01.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 0d3cc.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι → ο . ∀ x3 . x0 = f482f.. (d8d01.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 89e73.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = d8d01.. x1 x2 x3 x4 ⟶ ∀ x5 : ι → ο . (∀ x6 . x5 x6 ⟶ prim1 x6 x1) ⟶ x2 x5 = decode_c (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem e80db.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι → ο . ∀ x3 . ∀ x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x0) ⟶ x1 x4 = decode_c (f482f.. (d8d01.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Theorem 119c2.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = d8d01.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem fd378.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = 2b2e3.. (f482f.. (d8d01.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem 78a8c.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = d8d01.. x1 x2 x3 x4 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 76505.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι → ο . ∀ x3 . x3 = f482f.. (d8d01.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 2a51d.. : ∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . ∀ x4 x5 : ι → ι → ο . ∀ x6 x7 . d8d01.. x0 x2 x4 x6 = d8d01.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 : ι → ο . (∀ x9 . x8 x9 ⟶ prim1 x9 x0) ⟶ x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (x6 = x7) (proof)
Theorem b3c31.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . ∀ x3 x4 : ι → ι → ο . ∀ x5 . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x0) ⟶ iff (x1 x6) (x2 x6)) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ iff (x3 x6 x7) (x4 x6 x7)) ⟶ d8d01.. x0 x1 x3 x5 = d8d01.. x0 x2 x4 x5 (proof)
Definition f593b.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : (ι → ο) → ο . ∀ x4 : ι → ι → ο . ∀ x5 . prim1 x5 x2 ⟶ x1 (d8d01.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem 48a34.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ f593b.. (d8d01.. x0 x1 x2 x3) (proof)
Theorem 5c3bc.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ι → ο . ∀ x3 . f593b.. (d8d01.. x0 x1 x2 x3) ⟶ prim1 x3 x0 (proof)
Theorem b3e73.. : ∀ x0 . f593b.. x0 ⟶ x0 = d8d01.. (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition df6a8.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 69516.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ι → ο) → ι → ι . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x3 x7 x8) (x6 x7 x8)) ⟶ x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4) ⟶ df6a8.. (d8d01.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 4cd9f.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 938bf.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ι → ο . ∀ x4 . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x3 x7 x8) (x6 x7 x8)) ⟶ x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4) ⟶ 4cd9f.. (d8d01.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)