Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr88V../c88b0..
PUVvu../14e52..
vout
Pr88V../f73a5.. 24.99 bars
TMGE5../a355e.. ownership of 6f4cb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZaw../5ba8c.. ownership of ea884.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWLJ../f9e09.. ownership of 46416.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHgL../0f5b8.. ownership of 0c122.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFWP../840db.. ownership of 75acf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb1C../54209.. ownership of d59a4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbZn../68262.. ownership of 2b61f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ5a../9b5b9.. ownership of f41cd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNHK../233cb.. ownership of a0ca8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaP5../ed155.. ownership of d06d1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb9U../5bf15.. ownership of ca557.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYyz../587e5.. ownership of 43eea.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc2g../16ee2.. ownership of 1d1cc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLgm../9e452.. ownership of eaccd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVKH../c4338.. ownership of d2b0c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWzs../132a6.. ownership of b3efa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML9R../c5601.. ownership of c3fd7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNMX../939e7.. ownership of 486b4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSb6../87654.. ownership of b362f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMtL../98e9c.. ownership of 3ca25.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdnz../62bc5.. ownership of 39d3e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFbX../47df7.. ownership of b4bc5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQXJ../9ddf8.. ownership of 45188.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF5z../d08f2.. ownership of 3f148.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLc5../98fd4.. ownership of a72d5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGJx../9b285.. ownership of 3ad63.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJ77../6d6e0.. ownership of d8aec.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJa3../96eee.. ownership of 8056a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbzG../3ca7d.. ownership of 56e41.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbEh../f71d3.. ownership of 3daee.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFSJ../12685.. ownership of 53bce.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHZX../f22f4.. ownership of 8ad76.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRHL../3b858.. ownership of 33736.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJ33../f2818.. ownership of 710bc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT4f../bb437.. ownership of dc474.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEko../665cb.. ownership of aa6f2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWqZ../5aa06.. ownership of e65f7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd3v../88cfa.. ownership of 13a89.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdqf../0b128.. ownership of 827c4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWCo../31cb5.. ownership of c7168.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbma../f723a.. ownership of 6adab.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXKf../71a27.. ownership of 07077.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXU9../9ffbc.. ownership of 0b18c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVf2../edf62.. ownership of 96bdc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJsL../1a806.. ownership of aacc9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHHj../abe05.. ownership of ea4c2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP6j../9ba5e.. ownership of 9bb3e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdtR../54486.. ownership of dc4e7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNBC../2f7e7.. ownership of 2ef07.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcJN../82081.. ownership of 2f702.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMDg../fd8ce.. ownership of f2271.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXiD../9a707.. ownership of 6f772.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdra../9c757.. ownership of 42b73.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKaq../414ec.. ownership of 98eef.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcvZ../a062f.. ownership of 3a341.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLfY../2897e.. ownership of 02c53.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUmB../11e1a.. ownership of 04e59.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVTd../7a426.. ownership of cab7d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW3x../f11f9.. ownership of 36171.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZVb../238db.. ownership of 74380.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMgm../13807.. ownership of b8cba.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTBr../44570.. ownership of b655a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJCg../9deca.. ownership of da228.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNEP../1593c.. ownership of bcd26.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT1s../757a9.. ownership of c70df.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMar2../afea2.. ownership of 626c0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbEj../10c05.. ownership of 42fa4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLem../a0de3.. ownership of da2df.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMamT../48496.. ownership of b756b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbbq../2814f.. ownership of d8462.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcyG../649aa.. ownership of 6a79a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWbS../a62cb.. ownership of 24a53.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSur../19df2.. ownership of c9420.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSiX../9f591.. ownership of accd9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFZX../6e9a0.. ownership of 42ff4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLcf../73fb5.. ownership of 830bd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWaF../d6caf.. ownership of 72e88.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFwT../cc848.. ownership of 71117.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJYR../21bb9.. ownership of 13aa7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRsU../73bb9.. ownership of 2f1af.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMco4../6cd6d.. ownership of dadc3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTBA../d7449.. ownership of 05a6e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaTP../732ef.. ownership of 02a4b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWU3../1c015.. ownership of 602da.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbSJ../7ff61.. ownership of 59148.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNeN../1550c.. ownership of dd69a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZqM../d0133.. ownership of 9db4b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMadw../de91f.. ownership of cd69b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFa6../7c591.. ownership of 47259.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMqZ../06d00.. ownership of 22726.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJny../cf4f3.. ownership of 3e25e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSKr../43940.. ownership of bf5cc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRuc../a1e88.. ownership of 33e73.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMJ5../2c32f.. ownership of ea216.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZL7../7d528.. ownership of 6f356.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdoc../5e5b1.. ownership of 7e8ef.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbgw../5df3e.. ownership of 5041b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFyj../c6f26.. ownership of 485ea.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQgH../a858e.. ownership of f7341.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXS4../b6c8e.. ownership of afcf3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ9z../a470c.. ownership of 39190.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXhp../10d77.. ownership of 6c71e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMctL../f899a.. ownership of e4331.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVfm../b3595.. ownership of 8a57d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPbV../e19d6.. ownership of 1b17b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLND../5ea8b.. ownership of b851e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ2H../8207c.. ownership of 915b7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMa1X../08204.. ownership of e736d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM43../a14ed.. ownership of 1502a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGCd../66dad.. ownership of 000b6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFvk../a91c2.. ownership of fe79a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRoA../df373.. ownership of 02221.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLY2../4f661.. ownership of 13468.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQo9../e8cc0.. ownership of 6ec24.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJQ2../f0fe2.. ownership of b995b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQQt../b1b48.. ownership of 0fd91.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXtq../bfdcd.. ownership of 72790.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRv7../01926.. ownership of 388fd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWsb../a0602.. ownership of f7360.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcCZ../a7070.. ownership of 0cc92.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWQK../ca606.. ownership of 12274.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFNW../2db01.. ownership of 69363.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGFo../9e235.. ownership of 90754.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdY2../ddf46.. ownership of 979cb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWq9../cf766.. ownership of dff40.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY4S../9770c.. ownership of 49cc1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcpY../218a5.. ownership of 81349.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLhE../9e5ce.. ownership of d3deb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSjr../4f252.. ownership of cd0a3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW1E../2fb70.. ownership of c7d21.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLKW../5e971.. ownership of d85c0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFSD../808cb.. ownership of 48667.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJHn../893bb.. ownership of f9c4e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ2M../495fc.. ownership of f15cb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPbk../db419.. ownership of c5aab.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSJ8../9c1b3.. ownership of 6a4e4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQqs../8eed6.. ownership of f5ffc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKTB../91732.. ownership of 29ad1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdEY../3f057.. ownership of 32c95.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR5J../f433d.. ownership of 05025.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLFx../6d4de.. ownership of 9fe37.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMa7y../ed9e4.. ownership of 2e831.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcWi../0d1e4.. ownership of 65b5f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXDY../e7b0e.. ownership of 46c6f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMX8../49b1f.. ownership of 2e323.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWdd../d7dd0.. ownership of 8adc6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ4D../24a2f.. ownership of 1a110.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRWM../12deb.. ownership of 0bae4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaGS../e2e78.. ownership of 3a064.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGAE../9a7fc.. ownership of b420e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd7g../7d897.. ownership of c51b5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSki../5ae7e.. ownership of 2f767.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLEc../47da7.. ownership of 16053.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQPM../6b948.. ownership of bbd9a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQNh../95766.. ownership of 85b48.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYzg../e45ff.. ownership of bd09f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRVt../6c9d6.. ownership of d97ab.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMa1r../ca50f.. ownership of 7759b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH7A../64107.. ownership of 1f7e2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWtw../85772.. ownership of 51ab0.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbgm../793dc.. ownership of 29e37.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW7T../c18b2.. ownership of d1eb0.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcw4../f8495.. ownership of ed32f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ1d../47d18.. ownership of 37d2e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML81../207e0.. ownership of 0b60a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHZQ../fdb15.. ownership of 9497f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFaL../368b9.. ownership of 3bbe6.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKX6../16fd3.. ownership of aee22.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJby../a6989.. ownership of 4ea01.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF3k../dab13.. ownership of d009f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHfk../154be.. ownership of 68d20.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLcb../63f77.. ownership of 2f75d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSEk../69da7.. ownership of 49e31.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG5P../c7b0f.. ownership of 237b7.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYjF../fac04.. ownership of 1cd8e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMSG../72bf8.. ownership of 9bf02.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPcw../3c795.. ownership of 7557e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM6F../22be9.. ownership of 581ec.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWHi../916e3.. ownership of 79719.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEo3../2631f.. ownership of fd428.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXVP../0a706.. ownership of 6100b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQGk../a6a4f.. ownership of 4bc77.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPMv../260c7.. ownership of 1bcc7.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdZF../88130.. ownership of 4bb22.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG5n../63822.. ownership of 7d7bf.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaHw../dbd71.. ownership of 71c09.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGW3../66f69.. ownership of 3e28b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb9r../b2f68.. ownership of 94011.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGsZ../35769.. ownership of 86f84.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMqt../8c5db.. ownership of 86f21.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJgP../a76fd.. ownership of 81367.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdA7../bf90f.. ownership of 74dd1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUVEY../bf7c8.. doc published by PrGxv..
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Param d2155.. : ι → (ι → ι → ο) → ι
Param 1216a.. : ι → (ι → ο) → ι
Definition 81367.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . λ x3 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) (1216a.. 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 c51b5.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 81367.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 3a064.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . x0 = f482f.. (81367.. x0 x1 x2 x3) 4a7ef.. (proof)
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 f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem 1a110.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 81367.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x5 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 2e323.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ x1 x4 = f482f.. (f482f.. (81367.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Param 2b2e3.. : ι → ι → ι → ο
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 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ 2b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3
Theorem 65b5f.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 81367.. 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 9fe37.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = 2b2e3.. (f482f.. (81367.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Param decode_p : ι → ι → ο
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 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem 32c95.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 81367.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x4 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem f5ffc.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ x3 x4 = decode_p (f482f.. (81367.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (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 c5aab.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ο . ∀ x6 x7 : ι → ο . 81367.. x0 x2 x4 x6 = 81367.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 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)
Param iff : ο → ο → ο
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
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 f9c4e.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . (∀ x7 . prim1 x7 x0 ⟶ 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)) ⟶ 81367.. x0 x1 x3 x5 = 81367.. x0 x2 x4 x6 (proof)
Definition 86f84.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x1 (81367.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem d85c0.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . 86f84.. (81367.. x0 x1 x2 x3) (proof)
Theorem cd0a3.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . 86f84.. (81367.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x1 x4) x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem 81349.. : ∀ x0 . 86f84.. x0 ⟶ x0 = 81367.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 3e28b.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι → ο) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem dff40.. : ∀ x0 : ι → (ι → ι) → (ι → ι → ο) → (ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1 ⟶ 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) ⟶ 3e28b.. (81367.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 7d7bf.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι → ο) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 90754.. : ∀ x0 : ι → (ι → ι) → (ι → ι → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1 ⟶ 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) ⟶ 7d7bf.. (81367.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 1bcc7.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . λ x3 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) x3)))
Theorem 12274.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = 1bcc7.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem f7360.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . x0 = f482f.. (1bcc7.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 72790.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = 1bcc7.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x5 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem b995b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ x1 x4 = f482f.. (f482f.. (1bcc7.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Theorem 13468.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = 1bcc7.. 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 fe79a.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = 2b2e3.. (f482f.. (1bcc7.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem 1502a.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = 1bcc7.. x1 x2 x3 x4 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 915b7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . x3 = f482f.. (1bcc7.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 1b17b.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ο . ∀ x6 x7 . 1bcc7.. x0 x2 x4 x6 = 1bcc7.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (x6 = x7) (proof)
Theorem e4331.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 . (∀ x6 . prim1 x6 x0 ⟶ x1 x6 = x2 x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ iff (x3 x6 x7) (x4 x6 x7)) ⟶ 1bcc7.. x0 x1 x3 x5 = 1bcc7.. x0 x2 x4 x5 (proof)
Definition 6100b.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ι → ο . ∀ x5 . prim1 x5 x2 ⟶ x1 (1bcc7.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem 39190.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ 6100b.. (1bcc7.. x0 x1 x2 x3) (proof)
Theorem f7341.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . 6100b.. (1bcc7.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x1 x4) x0 (proof)
Theorem 5041b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . 6100b.. (1bcc7.. x0 x1 x2 x3) ⟶ prim1 x3 x0 (proof)
Theorem 6f356.. : ∀ x0 . 6100b.. x0 ⟶ x0 = 1bcc7.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition 79719.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 33e73.. : ∀ x0 : ι → (ι → ι) → (ι → ι → ο) → ι → ι . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1 ⟶ 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) ⟶ 79719.. (1bcc7.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 7557e.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 3e25e.. : ∀ x0 : ι → (ι → ι) → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1 ⟶ 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) ⟶ 7557e.. (1bcc7.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 1cd8e.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ο . λ x3 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (1216a.. x0 x2) x3)))
Theorem 47259.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x0 = 1cd8e.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 9db4b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . x0 = f482f.. (1cd8e.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 59148.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x0 = 1cd8e.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x5 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 02a4b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ x1 x4 = f482f.. (f482f.. (1cd8e.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Theorem dadc3.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x0 = 1cd8e.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x3 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem 13aa7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ x2 x4 = decode_p (f482f.. (1cd8e.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 (proof)
Theorem 72e88.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x0 = 1cd8e.. x1 x2 x3 x4 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 42ff4.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . x3 = f482f.. (1cd8e.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem c9420.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ο . ∀ x6 x7 . 1cd8e.. x0 x2 x4 x6 = 1cd8e.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0 ⟶ x4 x8 = x5 x8)) (x6 = x7) (proof)
Theorem 6a79a.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . (∀ x6 . prim1 x6 x0 ⟶ x1 x6 = x2 x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ iff (x3 x6) (x4 x6)) ⟶ 1cd8e.. x0 x1 x3 x5 = 1cd8e.. x0 x2 x4 x5 (proof)
Definition 49e31.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x2 ⟶ x1 (1cd8e.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem b756b.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ 49e31.. (1cd8e.. x0 x1 x2 x3) (proof)
Theorem 42fa4.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . 49e31.. (1cd8e.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x1 x4) x0 (proof)
Theorem c70df.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . 49e31.. (1cd8e.. x0 x1 x2 x3) ⟶ prim1 x3 x0 (proof)
Theorem da228.. : ∀ x0 . 49e31.. x0 ⟶ x0 = 1cd8e.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition 68d20.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem b8cba.. : ∀ x0 : ι → (ι → ι) → (ι → ο) → ι → ι . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1 ⟶ x2 x6 = x5 x6) ⟶ ∀ x6 : ι → ο . (∀ x7 . prim1 x7 x1 ⟶ iff (x3 x7) (x6 x7)) ⟶ x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4) ⟶ 68d20.. (1cd8e.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 4ea01.. := λ x0 . λ x1 : ι → (ι → ι) → (ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 36171.. : ∀ x0 : ι → (ι → ι) → (ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1 ⟶ x2 x6 = x5 x6) ⟶ ∀ x6 : ι → ο . (∀ x7 . prim1 x7 x1 ⟶ iff (x3 x7) (x6 x7)) ⟶ x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4) ⟶ 4ea01.. (1cd8e.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 3bbe6.. := λ x0 . λ x1 x2 : ι → ι → ο . λ x3 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) (1216a.. x0 x3))))
Theorem 04e59.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 3bbe6.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 3a341.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . x0 = f482f.. (3bbe6.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 42b73.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 3bbe6.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem f2271.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 x4 x5 = 2b2e3.. (f482f.. (3bbe6.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 x5 (proof)
Theorem 2ef07.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 3bbe6.. 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 9bb3e.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = 2b2e3.. (f482f.. (3bbe6.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem aacc9.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 3bbe6.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x4 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem 0b18c.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ x3 x4 = decode_p (f482f.. (3bbe6.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (proof)
Theorem 6adab.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ο . ∀ x6 x7 : ι → ο . 3bbe6.. x0 x2 x4 x6 = 3bbe6.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x2 x8 x9 = x3 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ x6 x8 = x7 x8) (proof)
Theorem 827c4.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x1 x7 x8) (x2 x7 x8)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x3 x7 x8) (x4 x7 x8)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ iff (x5 x7) (x6 x7)) ⟶ 3bbe6.. x0 x1 x3 x5 = 3bbe6.. x0 x2 x4 x6 (proof)
Definition 0b60a.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 x4 : ι → ι → ο . ∀ x5 : ι → ο . x1 (3bbe6.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem e65f7.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . 0b60a.. (3bbe6.. x0 x1 x2 x3) (proof)
Theorem dc474.. : ∀ x0 . 0b60a.. x0 ⟶ x0 = 3bbe6.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition ed32f.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 33736.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . (∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ iff (x2 x6 x7) (x5 x6 x7)) ⟶ ∀ 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) ⟶ ed32f.. (3bbe6.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 29e37.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 53bce.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . (∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ iff (x2 x6 x7) (x5 x6 x7)) ⟶ ∀ 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) ⟶ 29e37.. (3bbe6.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 1f7e2.. := λ x0 . λ x1 x2 : ι → ι → ο . λ x3 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) x3)))
Theorem 56e41.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . x0 = 1f7e2.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem d8aec.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . x0 = f482f.. (1f7e2.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem a72d5.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . x0 = 1f7e2.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 45188.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 x4 x5 = 2b2e3.. (f482f.. (1f7e2.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 x5 (proof)
Theorem 39d3e.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . x0 = 1f7e2.. 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 b362f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = 2b2e3.. (f482f.. (1f7e2.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem c3fd7.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . x0 = 1f7e2.. x1 x2 x3 x4 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem d2b0c.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . x3 = f482f.. (1f7e2.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 1d1cc.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ο . ∀ x6 x7 . 1f7e2.. x0 x2 x4 x6 = 1f7e2.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x2 x8 x9 = x3 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (x6 = x7) (proof)
Theorem ca557.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . ∀ x5 . (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ iff (x1 x6 x7) (x2 x6 x7)) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ iff (x3 x6 x7) (x4 x6 x7)) ⟶ 1f7e2.. x0 x1 x3 x5 = 1f7e2.. x0 x2 x4 x5 (proof)
Definition d97ab.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 x4 : ι → ι → ο . ∀ x5 . prim1 x5 x2 ⟶ x1 (1f7e2.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem a0ca8.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ d97ab.. (1f7e2.. x0 x1 x2 x3) (proof)
Theorem 2b61f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . d97ab.. (1f7e2.. x0 x1 x2 x3) ⟶ prim1 x3 x0 (proof)
Theorem 75acf.. : ∀ x0 . d97ab.. x0 ⟶ x0 = 1f7e2.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition 85b48.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 46416.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → ι → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . (∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ iff (x2 x6 x7) (x5 x6 x7)) ⟶ ∀ 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) ⟶ 85b48.. (1f7e2.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 16053.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 6f4cb.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . (∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ iff (x2 x6 x7) (x5 x6 x7)) ⟶ ∀ 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) ⟶ 16053.. (1f7e2.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)