Proofgold Signed Transaction

vin
PrEvg../3ef38.. PUhTZ../193cb..

vout

PrEvg../fa49f.. 3.38 bars
TMcEL../5448a.. negprop ownership controlledby PrGxv.. upto 0
TMXVB../34d6d.. ownership of e5856.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZim../eb582.. ownership of c4ac7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWob../10257.. ownership of ea617.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZNK../72607.. ownership of d5674.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXVP../43a99.. ownership of 500f6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRoV../1af9e.. ownership of 30b06.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN52../b7ee7.. ownership of 43dff.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPrq../92697.. ownership of 158d0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdeL../6c894.. ownership of b8753.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT6T../7223a.. ownership of 30e05.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV15../7a137.. ownership of 3c94a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK8t../661c4.. ownership of 13ab5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb8F../298e5.. ownership of 5bcd7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNud../4f471.. ownership of ea373.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaZ9../cb02b.. ownership of a4074.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEnk../27121.. ownership of 410ce.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWYv../d12fa.. ownership of 0f560.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd86../3f687.. ownership of 00aa3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML2d../7be31.. ownership of 674bb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYgt../e3e29.. ownership of 35963.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQvc../63029.. ownership of fb4aa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbAk../e8314.. ownership of 1f91c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQw6../46917.. ownership of 48be8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGEB../3cb5e.. ownership of db10f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF6N../d14ac.. ownership of 79851.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZZt../e5503.. ownership of 6381d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLWh../ede89.. ownership of 2ffba.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTbL../d42d2.. ownership of 535e5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWwo../c4e71.. ownership of 8029f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTKt../ca67d.. ownership of 8ed5e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUrc../04d51.. ownership of 803ff.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKKZ../19160.. ownership of a321e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZY8../a6823.. ownership of 2e748.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMDa../cc7fd.. ownership of b9b57.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXDM../8e5cf.. ownership of 7f213.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVEn../ecb23.. ownership of d894a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQpt../f8178.. ownership of d73e9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR5u../25e10.. ownership of 49096.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMwS../d1496.. ownership of 5a2be.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd1d../b50ef.. ownership of 5ea2b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMZf../727b2.. ownership of fd818.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHKn../f92a7.. ownership of 770b8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXLk../f789b.. ownership of 05e93.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNH6../914ae.. ownership of b68ba.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLjn../befab.. ownership of 7d382.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXid../36435.. ownership of 2f1b9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLY9../d8494.. ownership of 9b3dc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTRU../47f2d.. ownership of 81f42.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdhr../10d1d.. ownership of abff8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTww../a7738.. ownership of b4e26.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMZP../5481b.. ownership of c4419.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR6u../568f0.. ownership of af17c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSqh../ff148.. ownership of 0cbcb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKHn../80f5e.. ownership of 0ed8a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQWm../c5e4a.. ownership of 81c0c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK7y../f9a99.. ownership of ad940.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKbU../72f45.. ownership of 932b3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYbA../e26f0.. ownership of e546e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJhn../df2f7.. ownership of ca584.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT2r../34d22.. ownership of de6cf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSAp../f38b7.. ownership of e951d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNjc../7bad0.. ownership of 9c424.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQDt../d7c31.. ownership of 492ff.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZDT../8069d.. ownership of 1a735.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYYz../b44d7.. ownership of 6982e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPYT../51530.. ownership of e4362.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMGG../257a6.. ownership of b2421.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM8A../bfd0a.. ownership of 1dada.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdSw../bb538.. ownership of 92823.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYUY../c8ac9.. ownership of 7ba3c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKCT../0186c.. ownership of 15fbb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFoC../69052.. ownership of 73dbb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV8P../75499.. ownership of 8c6f6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXbc../17dff.. ownership of d908b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMasw../c8088.. ownership of 6acac.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcyE../8a3c1.. ownership of 04b90.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRUR../03658.. ownership of 696c0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLuF../4afae.. ownership of 4785a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVGT../d31d4.. ownership of b81d7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUog../4debc.. ownership of 0e196.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcjT../069a4.. ownership of f336f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdGy../e0536.. ownership of 16786.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGLA../feb23.. ownership of 71e64.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTiF../fbcc0.. ownership of e8090.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcB2../1e1eb.. ownership of b2728.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML7c../4d2bf.. ownership of e4705.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVXR../fa2c3.. ownership of 477e8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHjC../90317.. ownership of 38104.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTgJ../2cbd7.. ownership of bbc77.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMqD../c79fd.. ownership of ef71c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV6R../fa68d.. ownership of 8098c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFUC../c15a8.. ownership of 6ac60.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTRs../6c7f6.. ownership of b6cac.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH5n../29c3c.. ownership of 8efd5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHyh../59fa5.. ownership of 5d2da.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF2P../f1542.. ownership of db4bc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMi5../924c2.. ownership of 9dd94.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQCY../2ac13.. ownership of 51b54.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdQL../7d1ee.. ownership of a0687.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKtB../bc7d5.. ownership of 62e4c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK34../bac1d.. ownership of dcd83.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZZq../21a8c.. ownership of da336.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH1T../4e91a.. ownership of 0117f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdVp../b68d5.. ownership of aa086.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRMU../bb1e2.. ownership of fead7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSME../4ff1b.. ownership of 30833.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM6J../7f3a9.. ownership of e7a4c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPsg../8517a.. ownership of c6d72.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFJW../9ccae.. ownership of 5a932.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWv6../10352.. ownership of 70f06.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML7b../5b7d6.. ownership of 67787.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPe1../0413c.. ownership of 89387.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMa8h../7e828.. ownership of 2532b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMds7../27376.. ownership of 44132.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLwm../9aee2.. ownership of f14df.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFZQ../f3f13.. ownership of d4e4f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTJr../b0086.. ownership of 1e4c0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYnq../40adb.. ownership of e9e64.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSLg../f7e1a.. ownership of 77290.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJM2../2fea2.. ownership of 168b6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSKz../35c3a.. ownership of 01338.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHEt../245bf.. ownership of 0a455.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMju../83ad9.. ownership of 7516b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZkF../92a59.. ownership of 44b25.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLxQ../95e05.. ownership of 54702.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJsa../8298a.. ownership of 97cb1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPAK../89d44.. ownership of 0e94c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVwV../1e33b.. ownership of 2bae9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRxb../063c8.. ownership of 5af08.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWu6../43880.. ownership of 54d21.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTfY../b47e4.. ownership of 3c63f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdTj../886c1.. ownership of b0842.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcR7../5b43c.. ownership of 55be8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZBR../510e3.. ownership of 30f47.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML2f../8b481.. ownership of f66b8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX43../5c235.. ownership of 8bdad.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNrP../9e364.. ownership of c2f00.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKJB../b9739.. ownership of 1e512.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdtg../629fc.. ownership of 3c4f5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSLJ../68bca.. ownership of 4495a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVPd../1d5f8.. ownership of 23bb7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcEd../0efb3.. ownership of a6a13.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMfB../52d57.. ownership of 67ebf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHJE../86b2e.. ownership of fa082.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXh1../e2c16.. ownership of f81b3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQVM../f892c.. ownership of be2e3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKsm../0e50e.. ownership of 0dcfe.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHEp../15927.. ownership of 17176.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP9N../f3152.. ownership of f6970.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRxy../8b06f.. ownership of 6ce64.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPFt../1316f.. ownership of 28d46.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcGp../6e8bd.. ownership of 3c39d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdGm../d23e6.. ownership of f0140.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVzz../7e3fa.. ownership of fa71f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPPX../97ef8.. ownership of ceeb0.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGiG../02dca.. ownership of 1ba2d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVHe../bb53d.. ownership of 31a8b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXMA../98cdd.. ownership of 9a7b4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNEA../77437.. ownership of 6a284.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYm4../293e4.. ownership of 52b09.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFMx../f3d10.. ownership of 127a8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH1q../3db12.. ownership of cde91.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS69../7a149.. ownership of 4dee0.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUEC../8da4f.. ownership of 5eb06.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVWy../bcc99.. ownership of 1eee5.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPtY../3aad9.. ownership of 7bebd.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZSk../5fc85.. ownership of d6c7f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFJR../b1bd8.. ownership of cdba9.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLA6../2a3ba.. ownership of b6e4d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ12../5e3c1.. ownership of e8533.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUKT../3902a.. ownership of 9f485.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMwq../2eb03.. ownership of fa4ab.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH2J../ed8fb.. ownership of 8c205.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGcF../d25fb.. ownership of f8922.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYTk../af35d.. ownership of 103e3.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSz8../b6a92.. ownership of e5d4c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZUj../33a93.. ownership of bc6cf.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVWA../8bd22.. ownership of 6cd44.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEx4../5e3fa.. ownership of 851df.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQQd../ad7fd.. ownership of 2aab0.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaqz../f1a5d.. ownership of d8e4a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMczE../ecaec.. ownership of f6efa.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRyc../70477.. ownership of 58681.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMawp../d5496.. ownership of 85402.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT4s../ecb57.. ownership of f15a6.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGDM../4c977.. ownership of 3b429.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGDF../a05a4.. ownership of 868ec.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZmW../e8a35.. ownership of a4c2a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTUZ../f7eba.. ownership of bf4f6.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGyr../a3e56.. ownership of 1216a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNN8../1607e.. ownership of da98b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRs6../dd729.. ownership of 94f9e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPQG../5698a.. ownership of 3041a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVAZ../56555.. ownership of 707e2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT2f../123c7.. ownership of 35f96.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF11../e810b.. ownership of c2f57.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNTV../cf34d.. ownership of f58a8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMyY../7b079.. ownership of 4a7ef.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd2k../751b7.. ownership of 2ef0d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWCk../0ea0c.. ownership of c2e41.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ55../f047c.. ownership of bbda1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMqH../0e771.. ownership of 7ee77.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY8M../2595e.. ownership of 7a075.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLj9../24079.. ownership of 91630.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMBx../475f5.. ownership of ec939.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXNS../45b14.. ownership of c4255.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbQv../c2e23.. ownership of 81c0e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFzx../57bdf.. ownership of 3b018.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSqg../56694.. ownership of 36808.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMWH../2d539.. ownership of 5fba2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNPk../f4d85.. ownership of 98aaa.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHzp../8a7e2.. ownership of 5cc77.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRrS../3061f.. ownership of 95774.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdDk../bd616.. ownership of 37d7b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHVP../4ae3c.. ownership of 2ba7d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd6Q../7d67b.. ownership of c156d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWAv../b432b.. ownership of f3043.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLox../352e6.. ownership of d3e93.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXh1../e5815.. ownership of f81b3.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSx6../d958e.. ownership of 2c067.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUdeW../80715.. doc published by PrGxv..

Definition False := ∀ x0 : ο . x0
Definition True := ∀ x0 : ο . x0 ⟶ x0
Definition not := λ x0 : ο . x0 ⟶ False
Theorem FalseE : False ⟶ ∀ x0 : ο . x0 (proof)
Theorem TrueI : True (proof)
Theorem notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0 (proof)
Theorem notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1 (proof)
Theorem andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0 (proof)
Theorem andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1 (proof)
Theorem orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1 (proof)
Theorem orE : ∀ x0 x1 x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ or x0 x1 ⟶ x2 (proof)
Definition iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Theorem iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1 (proof)
Theorem iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0 (proof)
Theorem iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1 (proof)
Theorem iff_refl : ∀ x0 : ο . iff x0 x0 (proof)
Known prop_ext : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 = x1
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition 91630.. := λ x0 . prim2 x0 x0
Definition 7ee77.. := λ x0 x1 . prim2 (prim2 x0 x1) (91630.. x0)
Definition c2e41.. := λ x0 x1 . ∀ x2 : ο . (∀ x3 . and (and (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 : ο . (∀ x6 . and (prim1 x6 x1) (prim1 (7ee77.. x4 x6) x3) ⟶ x5) ⟶ x5) (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (prim1 (7ee77.. x6 x4) x3) ⟶ x5) ⟶ x5)) (∀ x4 x5 x6 x7 . prim1 (7ee77.. x4 x5) x3 ⟶ prim1 (7ee77.. x6 x7) x3 ⟶ iff (x4 = x6) (x5 = x7)) ⟶ x2) ⟶ x2
Known Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Known 0ddd1.. : ∀ x0 x1 . (∀ x2 . iff (prim1 x2 x0) (prim1 x2 x1)) ⟶ x0 = x1
Known 53c21.. : ∀ x0 x1 x2 . iff (prim1 x0 (prim2 x1 x2)) (or (x0 = x1) (x0 = x2))
Known UnionEq : ∀ x0 x1 . iff (prim1 x1 (prim3 x0)) (∀ x2 : ο . (∀ x3 . and (prim1 x1 x3) (prim1 x3 x0) ⟶ x2) ⟶ x2)
Known e8b3c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 x4 . x1 x2 x3 ⟶ x1 x2 x4 ⟶ x3 = x4) ⟶ ∀ x2 : ο . (∀ x3 . (∀ x4 . iff (prim1 x4 x3) (∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (x1 x6 x4) ⟶ x5) ⟶ x5)) ⟶ x2) ⟶ x2
Theorem Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0) (proof)
Theorem pred_ext : ∀ x0 x1 : ι → ο . (∀ x2 . iff (x0 x2) (x1 x2)) ⟶ x0 = x1 (proof)
Theorem prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1 (proof)
Theorem pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1 (proof)
Theorem 2532b.. : ∀ x0 x1 x2 . prim1 x0 (prim2 x1 x2) ⟶ or (x0 = x1) (x0 = x2) (proof)
Theorem 67787.. : ∀ x0 x1 . prim1 x0 (prim2 x0 x1) (proof)
Theorem 5a932.. : ∀ x0 x1 . prim1 x1 (prim2 x0 x1) (proof)
Theorem e7a4c.. : ∀ x0 . prim1 x0 (91630.. x0) (proof)
Theorem fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0 (proof)
Theorem 0117f.. : ∀ x0 : ο . (∀ x1 . (∀ x2 . nIn x2 x1) ⟶ x0) ⟶ x0 (proof)
Definition 4a7ef.. := prim0 (λ x0 . ∀ x1 . nIn x1 x0)
Theorem dcd83.. : ∀ x0 . nIn x0 4a7ef.. (proof)
Theorem xm : ∀ x0 : ο . or x0 (not x0) (proof)
Theorem UnionI : ∀ x0 x1 x2 . prim1 x1 x2 ⟶ prim1 x2 x0 ⟶ prim1 x1 (prim3 x0) (proof)
Theorem UnionE : ∀ x0 x1 . prim1 x1 (prim3 x0) ⟶ ∀ x2 : ο . (∀ x3 . and (prim1 x1 x3) (prim1 x3 x0) ⟶ x2) ⟶ x2 (proof)
Theorem UnionE_impred : ∀ x0 x1 . prim1 x1 (prim3 x0) ⟶ ∀ x2 : ο . (∀ x3 . prim1 x1 x3 ⟶ prim1 x3 x0 ⟶ x2) ⟶ x2 (proof)
Definition c2f57.. := λ x0 : ι → ο . ∀ x1 : ο . (∀ x2 . (∀ x3 . iff (prim1 x3 x2) (x0 x3)) ⟶ x1) ⟶ x1
Definition 707e2.. := λ x0 : ι → ο . prim0 (λ x1 . ∀ x2 . iff (prim1 x2 x1) (x0 x2))
Theorem 8098c.. : ∀ x0 : ι → ο . c2f57.. x0 ⟶ ∀ x1 . iff (prim1 x1 (707e2.. x0)) (x0 x1) (proof)
Theorem bbc77.. : ∀ x0 : ι → ο . c2f57.. x0 ⟶ ∀ x1 . x0 x1 ⟶ prim1 x1 (707e2.. x0) (proof)
Theorem 477e8.. : ∀ x0 : ι → ο . c2f57.. x0 ⟶ ∀ x1 . prim1 x1 (707e2.. x0) ⟶ x0 x1 (proof)
Theorem b2728.. : ∀ x0 . c2f57.. (λ x1 . prim1 x1 x0) (proof)
Theorem 71e64.. : ∀ x0 . 707e2.. (λ x2 . prim1 x2 x0) = x0 (proof)
Theorem f336f.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ο . (∀ x3 . (∀ x4 . iff (prim1 x4 x3) (∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (x4 = x1 x6) ⟶ x5) ⟶ x5)) ⟶ x2) ⟶ x2 (proof)
Definition 94f9e.. := λ x0 . λ x1 : ι → ι . prim0 (λ x2 . ∀ x3 . iff (prim1 x3 x2) (∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x3 = x1 x5) ⟶ x4) ⟶ x4))
Theorem b81d7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (prim1 x2 (94f9e.. x0 x1)) (∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (x2 = x1 x4) ⟶ x3) ⟶ x3) (proof)
Theorem 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1) (proof)
Theorem 6acac.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (x2 = x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3 (proof)
Theorem 15fbb.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ο . (∀ x3 . (∀ x4 . iff (prim1 x4 x3) (and (prim1 x4 x0) (x1 x4))) ⟶ x2) ⟶ x2 (proof)
Definition 1216a.. := λ x0 . λ x1 : ι → ο . prim0 (λ x2 . ∀ x3 . iff (prim1 x3 x2) (and (prim1 x3 x0) (x1 x3)))
Theorem 92823.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . iff (prim1 x2 (1216a.. x0 x1)) (and (prim1 x2 x0) (x1 x2)) (proof)
Theorem b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1) (proof)
Theorem 6982e.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ and (prim1 x2 x0) (x1 x2) (proof)
Theorem 492ff.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ ∀ x3 : ο . (prim1 x2 x0 ⟶ x1 x2 ⟶ x3) ⟶ x3 (proof)
Definition a4c2a.. := λ x0 . λ x1 : ι → ο . 94f9e.. (1216a.. x0 x1)
Theorem e951d.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 x0 ⟶ x1 x3 ⟶ prim1 (x2 x3) (a4c2a.. x0 x1 x2) (proof)
Theorem ca584.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 (a4c2a.. x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (and (x1 x5) (x3 = x2 x5)) ⟶ x4) ⟶ x4 (proof)
Theorem 932b3.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 (a4c2a.. x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . prim1 x5 x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4 (proof)
Definition 3b429.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . λ x3 : ι → ι → ι . prim3 (94f9e.. x0 (λ x4 . a4c2a.. (x1 x4) (x2 x4) (x3 x4)))
Theorem 81c0c.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 (x1 x4) ⟶ x2 x4 x5 ⟶ prim1 (x3 x4 x5) (3b429.. x0 x1 x2 x3) (proof)
Theorem 0cbcb.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . prim1 x4 (3b429.. x0 x1 x2 x3) ⟶ ∀ x5 : ο . (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 (x1 x6) ⟶ x2 x6 x7 ⟶ x4 = x3 x6 x7 ⟶ x5) ⟶ x5 (proof)
Theorem c4419.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . prim1 x4 (3b429.. x0 x1 x2 x3) ⟶ ∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (∀ x7 : ο . (∀ x8 . and (prim1 x8 (x1 x6)) (and (x2 x6 x8) (x4 = x3 x6 x8)) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5 (proof)
Definition 85402.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι . λ x3 : ι → ι → ι → ο . λ x4 : ι → ι → ι → ι . prim3 (94f9e.. x0 (λ x5 . 3b429.. (x1 x5) (x2 x5) (x3 x5) (x4 x5)))
Theorem abff8.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ο . ∀ x4 : ι → ι → ι → ι . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 (x1 x5) ⟶ ∀ x7 . prim1 x7 (x2 x5 x6) ⟶ x3 x5 x6 x7 ⟶ prim1 (x4 x5 x6 x7) (85402.. x0 x1 x2 x3 x4) (proof)
Theorem 9b3dc.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ο . ∀ x4 : ι → ι → ι → ι . ∀ x5 . prim1 x5 (85402.. x0 x1 x2 x3 x4) ⟶ ∀ x6 : ο . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 (x1 x7) ⟶ ∀ x9 . prim1 x9 (x2 x7 x8) ⟶ x3 x7 x8 x9 ⟶ x5 = x4 x7 x8 x9 ⟶ x6) ⟶ x6 (proof)
Theorem 7d382.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ο . ∀ x4 : ι → ι → ι → ι . ∀ x5 . prim1 x5 (85402.. x0 x1 x2 x3 x4) ⟶ ∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (∀ x8 : ο . (∀ x9 . and (prim1 x9 (x1 x7)) (∀ x10 : ο . (∀ x11 . and (prim1 x11 (x2 x7 x9)) (and (x3 x7 x9 x11) (x5 = x4 x7 x9 x11)) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6 (proof)
Definition f6efa.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι . λ x3 : ι → ι → ι → ι . λ x4 : ι → ι → ι → ι → ο . λ x5 : ι → ι → ι → ι → ι . prim3 (94f9e.. x0 (λ x6 . 85402.. (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6)))
Theorem 05e93.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ο . ∀ x5 : ι → ι → ι → ι → ι . ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 (x1 x6) ⟶ ∀ x8 . prim1 x8 (x2 x6 x7) ⟶ ∀ x9 . prim1 x9 (x3 x6 x7 x8) ⟶ x4 x6 x7 x8 x9 ⟶ prim1 (x5 x6 x7 x8 x9) (f6efa.. x0 x1 x2 x3 x4 x5) (proof)
Theorem fd818.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ο . ∀ x5 : ι → ι → ι → ι → ι . ∀ x6 . prim1 x6 (f6efa.. x0 x1 x2 x3 x4 x5) ⟶ ∀ x7 : ο . (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 (x1 x8) ⟶ ∀ x10 . prim1 x10 (x2 x8 x9) ⟶ ∀ x11 . prim1 x11 (x3 x8 x9 x10) ⟶ x4 x8 x9 x10 x11 ⟶ x6 = x5 x8 x9 x10 x11 ⟶ x7) ⟶ x7 (proof)
Theorem 5a2be.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ο . ∀ x5 : ι → ι → ι → ι → ι . ∀ x6 . prim1 x6 (f6efa.. x0 x1 x2 x3 x4 x5) ⟶ ∀ x7 : ο . (∀ x8 . and (prim1 x8 x0) (∀ x9 : ο . (∀ x10 . and (prim1 x10 (x1 x8)) (∀ x11 : ο . (∀ x12 . and (prim1 x12 (x2 x8 x10)) (∀ x13 : ο . (∀ x14 . and (prim1 x14 (x3 x8 x10 x12)) (and (x4 x8 x10 x12 x14) (x6 = x5 x8 x10 x12 x14)) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7 (proof)
Definition 2aab0.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι . λ x3 : ι → ι → ι → ι . λ x4 : ι → ι → ι → ι → ι . λ x5 : ι → ι → ι → ι → ι → ο . λ x6 : ι → ι → ι → ι → ι → ι . prim3 (94f9e.. x0 (λ x7 . f6efa.. (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7)))
Theorem d73e9.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ο . ∀ x6 : ι → ι → ι → ι → ι → ι . ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 (x1 x7) ⟶ ∀ x9 . prim1 x9 (x2 x7 x8) ⟶ ∀ x10 . prim1 x10 (x3 x7 x8 x9) ⟶ ∀ x11 . prim1 x11 (x4 x7 x8 x9 x10) ⟶ x5 x7 x8 x9 x10 x11 ⟶ prim1 (x6 x7 x8 x9 x10 x11) (2aab0.. x0 x1 x2 x3 x4 x5 x6) (proof)
Theorem 7f213.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ο . ∀ x6 : ι → ι → ι → ι → ι → ι . ∀ x7 . prim1 x7 (2aab0.. x0 x1 x2 x3 x4 x5 x6) ⟶ ∀ x8 : ο . (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 (x1 x9) ⟶ ∀ x11 . prim1 x11 (x2 x9 x10) ⟶ ∀ x12 . prim1 x12 (x3 x9 x10 x11) ⟶ ∀ x13 . prim1 x13 (x4 x9 x10 x11 x12) ⟶ x5 x9 x10 x11 x12 x13 ⟶ x7 = x6 x9 x10 x11 x12 x13 ⟶ x8) ⟶ x8 (proof)
Theorem 2e748.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ο . ∀ x6 : ι → ι → ι → ι → ι → ι . ∀ x7 . prim1 x7 (2aab0.. x0 x1 x2 x3 x4 x5 x6) ⟶ ∀ x8 : ο . (∀ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 (x1 x9)) (∀ x12 : ο . (∀ x13 . and (prim1 x13 (x2 x9 x11)) (∀ x14 : ο . (∀ x15 . and (prim1 x15 (x3 x9 x11 x13)) (∀ x16 : ο . (∀ x17 . and (prim1 x17 (x4 x9 x11 x13 x15)) (and (x5 x9 x11 x13 x15 x17) (x7 = x6 x9 x11 x13 x15 x17)) ⟶ x16) ⟶ x16) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8 (proof)
Definition 6cd44.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι . λ x3 : ι → ι → ι → ι . λ x4 : ι → ι → ι → ι → ι . λ x5 : ι → ι → ι → ι → ι → ι . λ x6 : ι → ι → ι → ι → ι → ι → ο . λ x7 : ι → ι → ι → ι → ι → ι → ι . prim3 (94f9e.. x0 (λ x8 . 2aab0.. (x1 x8) (x2 x8) (x3 x8) (x4 x8) (x5 x8) (x6 x8) (x7 x8)))
Theorem 803ff.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ο . ∀ x7 : ι → ι → ι → ι → ι → ι → ι . ∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 (x1 x8) ⟶ ∀ x10 . prim1 x10 (x2 x8 x9) ⟶ ∀ x11 . prim1 x11 (x3 x8 x9 x10) ⟶ ∀ x12 . prim1 x12 (x4 x8 x9 x10 x11) ⟶ ∀ x13 . prim1 x13 (x5 x8 x9 x10 x11 x12) ⟶ x6 x8 x9 x10 x11 x12 x13 ⟶ prim1 (x7 x8 x9 x10 x11 x12 x13) (6cd44.. x0 x1 x2 x3 x4 x5 x6 x7) (proof)
Theorem 8029f.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ο . ∀ x7 : ι → ι → ι → ι → ι → ι → ι . ∀ x8 . prim1 x8 (6cd44.. x0 x1 x2 x3 x4 x5 x6 x7) ⟶ ∀ x9 : ο . (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 (x1 x10) ⟶ ∀ x12 . prim1 x12 (x2 x10 x11) ⟶ ∀ x13 . prim1 x13 (x3 x10 x11 x12) ⟶ ∀ x14 . prim1 x14 (x4 x10 x11 x12 x13) ⟶ ∀ x15 . prim1 x15 (x5 x10 x11 x12 x13 x14) ⟶ x6 x10 x11 x12 x13 x14 x15 ⟶ x8 = x7 x10 x11 x12 x13 x14 x15 ⟶ x9) ⟶ x9 (proof)
Theorem 2ffba.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ο . ∀ x7 : ι → ι → ι → ι → ι → ι → ι . ∀ x8 . prim1 x8 (6cd44.. x0 x1 x2 x3 x4 x5 x6 x7) ⟶ ∀ x9 : ο . (∀ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 (x1 x10)) (∀ x13 : ο . (∀ x14 . and (prim1 x14 (x2 x10 x12)) (∀ x15 : ο . (∀ x16 . and (prim1 x16 (x3 x10 x12 x14)) (∀ x17 : ο . (∀ x18 . and (prim1 x18 (x4 x10 x12 x14 x16)) (∀ x19 : ο . (∀ x20 . and (prim1 x20 (x5 x10 x12 x14 x16 x18)) (and (x6 x10 x12 x14 x16 x18 x20) (x8 = x7 x10 x12 x14 x16 x18 x20)) ⟶ x19) ⟶ x19) ⟶ x17) ⟶ x17) ⟶ x15) ⟶ x15) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9 (proof)
Definition e5d4c.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι . λ x3 : ι → ι → ι → ι . λ x4 : ι → ι → ι → ι → ι . λ x5 : ι → ι → ι → ι → ι → ι . λ x6 : ι → ι → ι → ι → ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι → ι → ο . λ x8 : ι → ι → ι → ι → ι → ι → ι → ι . prim3 (94f9e.. x0 (λ x9 . 6cd44.. (x1 x9) (x2 x9) (x3 x9) (x4 x9) (x5 x9) (x6 x9) (x7 x9) (x8 x9)))
Theorem 79851.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι → ι → ο . ∀ x8 : ι → ι → ι → ι → ι → ι → ι → ι . ∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 (x1 x9) ⟶ ∀ x11 . prim1 x11 (x2 x9 x10) ⟶ ∀ x12 . prim1 x12 (x3 x9 x10 x11) ⟶ ∀ x13 . prim1 x13 (x4 x9 x10 x11 x12) ⟶ ∀ x14 . prim1 x14 (x5 x9 x10 x11 x12 x13) ⟶ ∀ x15 . prim1 x15 (x6 x9 x10 x11 x12 x13 x14) ⟶ x7 x9 x10 x11 x12 x13 x14 x15 ⟶ prim1 (x8 x9 x10 x11 x12 x13 x14 x15) (e5d4c.. x0 x1 x2 x3 x4 x5 x6 x7 x8) (proof)
Theorem 48be8.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι → ι → ο . ∀ x8 : ι → ι → ι → ι → ι → ι → ι → ι . ∀ x9 . prim1 x9 (e5d4c.. x0 x1 x2 x3 x4 x5 x6 x7 x8) ⟶ ∀ x10 : ο . (∀ x11 . prim1 x11 x0 ⟶ ∀ x12 . prim1 x12 (x1 x11) ⟶ ∀ x13 . prim1 x13 (x2 x11 x12) ⟶ ∀ x14 . prim1 x14 (x3 x11 x12 x13) ⟶ ∀ x15 . prim1 x15 (x4 x11 x12 x13 x14) ⟶ ∀ x16 . prim1 x16 (x5 x11 x12 x13 x14 x15) ⟶ ∀ x17 . prim1 x17 (x6 x11 x12 x13 x14 x15 x16) ⟶ x7 x11 x12 x13 x14 x15 x16 x17 ⟶ x9 = x8 x11 x12 x13 x14 x15 x16 x17 ⟶ x10) ⟶ x10 (proof)
Theorem fb4aa.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι → ι → ο . ∀ x8 : ι → ι → ι → ι → ι → ι → ι → ι . ∀ x9 . prim1 x9 (e5d4c.. x0 x1 x2 x3 x4 x5 x6 x7 x8) ⟶ ∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 (x1 x11)) (∀ x14 : ο . (∀ x15 . and (prim1 x15 (x2 x11 x13)) (∀ x16 : ο . (∀ x17 . and (prim1 x17 (x3 x11 x13 x15)) (∀ x18 : ο . (∀ x19 . and (prim1 x19 (x4 x11 x13 x15 x17)) (∀ x20 : ο . (∀ x21 . and (prim1 x21 (x5 x11 x13 x15 x17 x19)) (∀ x22 : ο . (∀ x23 . and (prim1 x23 (x6 x11 x13 x15 x17 x19 x21)) (and (x7 x11 x13 x15 x17 x19 x21 x23) (x9 = x8 x11 x13 x15 x17 x19 x21 x23)) ⟶ x22) ⟶ x22) ⟶ x20) ⟶ x20) ⟶ x18) ⟶ x18) ⟶ x16) ⟶ x16) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10 (proof)
Definition f8922.. := λ x0 : (ι → ι) → ο . ∀ x1 : (ι → ι) → ι . ∀ x2 : ο . (∀ x3 . (∀ x4 : ι → ι . x0 x4 ⟶ x4 x3 = x1 x4) ⟶ x2) ⟶ x2
Theorem 674bb.. : ∀ x0 x1 : (ι → ι) → ο . f8922.. x1 ⟶ (∀ x2 : ι → ι . x0 x2 ⟶ x1 x2) ⟶ f8922.. x0 (proof)
Definition fa4ab.. := λ x0 : (ι → ι) → ο . λ x1 : (ι → ι) → ι . prim0 (λ x2 . ∀ x3 : ι → ι . x0 x3 ⟶ x3 x2 = x1 x3)
Theorem 0f560.. : ∀ x0 : (ι → ι) → ο . f8922.. x0 ⟶ ∀ x1 : ι → ι . x0 x1 ⟶ ∀ x2 : (ι → ι) → ι . x1 (fa4ab.. x0 x2) = x2 x1 (proof)
Definition e8533.. := λ x0 : (ι → ι) → ο . λ x1 . x1 = fa4ab.. x0 (λ x3 : ι → ι . x3 x1)
Theorem a4074.. : ∀ x0 : (ι → ι) → ο . f8922.. x0 ⟶ ∀ x1 . fa4ab.. x0 (λ x3 : ι → ι . x3 x1) = fa4ab.. x0 (λ x3 : ι → ι . x3 (fa4ab.. x0 (λ x4 : ι → ι . x4 x1))) (proof)
Theorem 5bcd7.. : ∀ x0 : (ι → ι) → ο . f8922.. x0 ⟶ ∀ x1 . e8533.. x0 (fa4ab.. x0 (λ x2 : ι → ι . x2 x1)) (proof)
Definition cdba9.. := λ x0 : (ι → ι) → ο . λ x1 x2 . ∀ x3 : ι → ι . x0 x3 ⟶ x3 x1 = x3 x2
Theorem 3c94a.. : ∀ x0 : (ι → ι) → ο . ∀ x1 . cdba9.. x0 x1 x1 (proof)
Theorem b8753.. : ∀ x0 : (ι → ι) → ο . ∀ x1 x2 . cdba9.. x0 x1 x2 ⟶ cdba9.. x0 x2 x1 (proof)
Theorem 43dff.. : ∀ x0 : (ι → ι) → ο . ∀ x1 x2 x3 . cdba9.. x0 x1 x2 ⟶ cdba9.. x0 x2 x3 ⟶ cdba9.. x0 x1 x3 (proof)
Definition 7bebd.. := λ x0 : ι → ι . λ x1 . True
Definition 5eb06.. := λ x0 : ι → ι . λ x1 . and (7bebd.. x0 x1) (e8533.. (λ x2 : ι → ι . x2 = x0) x1)
Definition cde91.. := λ x0 : ι → ι . λ x1 . ∀ x2 . nIn x2 (x0 x1)
Definition 52b09.. := λ x0 : ι → ι . λ x1 . not (cde91.. x0 x1)
Definition 9a7b4.. := λ x0 x1 : ι → ι . λ x2 . prim1 (x1 x2) (x0 x2)
Definition 1ba2d.. := λ x0 x1 : ι → ι . λ x2 . and (9a7b4.. x0 x1 x2) (e8533.. (λ x3 : ι → ι . or (x3 = x0) (x3 = x1)) x2)
Definition fa71f.. := λ x0 x1 x2 : ι → ι . λ x3 . and (9a7b4.. x0 x1 x3) (9a7b4.. x0 x2 x3)
Definition 3c39d.. := λ x0 x1 x2 : ι → ι . λ x3 . and (fa71f.. x0 x1 x2 x3) (e8533.. (λ x4 : ι → ι . or (or (x4 = x0) (x4 = x1)) (x4 = x2)) x3)
Theorem 500f6.. : ∀ x0 x1 : ι → ι . not (x0 = x1) ⟶ f8922.. (λ x2 : ι → ι . or (x2 = x0) (x2 = x1)) ⟶ ∀ x2 . 9a7b4.. x0 x1 x2 ⟶ 7bebd.. x0 x2 (proof)
Theorem 500f6.. : ∀ x0 x1 : ι → ι . not (x0 = x1) ⟶ f8922.. (λ x2 : ι → ι . or (x2 = x0) (x2 = x1)) ⟶ ∀ x2 . 9a7b4.. x0 x1 x2 ⟶ 7bebd.. x0 x2 (proof)
Theorem ea617.. : ∀ x0 x1 x2 : ι → ι . not (x0 = x1) ⟶ not (x0 = x2) ⟶ not (x1 = x2) ⟶ f8922.. (λ x3 : ι → ι . or (or (x3 = x0) (x3 = x1)) (x3 = x2)) ⟶ ∀ x3 . fa71f.. x0 x1 x2 x3 ⟶ 9a7b4.. x0 x1 x3 (proof)
Theorem e5856.. : ∀ x0 x1 x2 : ι → ι . not (x0 = x1) ⟶ not (x0 = x2) ⟶ not (x1 = x2) ⟶ f8922.. (λ x3 : ι → ι . or (or (x3 = x0) (x3 = x1)) (x3 = x2)) ⟶ ∀ x3 . fa71f.. x0 x1 x2 x3 ⟶ 9a7b4.. x0 x2 x3 (proof)
Definition 6ce64.. := λ x0 x1 : ι → ι . λ x2 . True
Definition 17176.. := λ x0 x1 : ι → ι . λ x2 . and (6ce64.. x0 x1 x2) (e8533.. (λ x3 : ι → ι . or (x3 = x0) (x3 = x1)) x2)