Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrEvg../1f042..
PUXi4../44a66..
vout
PrEvg../90f85.. 0.32 bars
TMbij../bc9ed.. negprop ownership controlledby PrGxv.. upto 0
TMZFi../a0836.. ownership of 48e77.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZDd../93b1b.. ownership of 04521.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVFK../aed29.. ownership of fb6d0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXYN../e50d4.. ownership of 3dcb8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaFe../fe1e9.. ownership of 96add.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFfP../738b6.. ownership of 2e5c3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaGz../1085c.. ownership of 45a0f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKXs../f96c6.. ownership of 7f087.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGb8../6630a.. ownership of 7fd4e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRJT../758ac.. ownership of 90122.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVy1../e252a.. ownership of 057f4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMceb../96c50.. ownership of 2e9d5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR47../8eaed.. ownership of 2cb0a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMkx../efb56.. ownership of d7038.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEo1../380c4.. ownership of 3e6f6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUV4../dd18e.. ownership of 90bcc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRdf../b34ca.. ownership of 0cbec.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFtU../6cee3.. ownership of 9c135.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNHz../6e968.. ownership of 8312b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdYq../3f854.. ownership of a89c5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG13../8fa5c.. ownership of f1d4d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZq9../7d560.. ownership of bebd8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSxZ../35c50.. ownership of a87f5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdzu../02497.. ownership of 6e6ce.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWmq../75723.. ownership of 5f7ef.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV5a../bd0eb.. ownership of 8e9af.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ6w../e6746.. ownership of ac124.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJ9u../5f2fe.. ownership of 1fe1f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY5a../d7815.. ownership of b5347.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQjX../a6303.. ownership of a538f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGb4../9f731.. ownership of 4a672.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTq3../ddde5.. ownership of f8eb3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPJW../bcdb4.. ownership of 98ac3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMk4../96774.. ownership of b917a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaRU../c9a50.. ownership of 8ee89.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHdA../7f51a.. ownership of f809b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXGW../c48a5.. ownership of a3321.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVFn../89325.. ownership of b67f6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQQd../eddf9.. ownership of c2711.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKxx../bbd68.. ownership of 03f5f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX6x../a045e.. ownership of 6c085.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGMC../9a149.. ownership of b57aa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXTh../0e321.. ownership of 4114a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK56../dce30.. ownership of 85e1b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK6V../c04c8.. ownership of f3fb5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTzL../80a4f.. ownership of 67a9b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPFP../f4711.. ownership of b72a3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKYU../c7624.. ownership of 1f03c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNGm../331cb.. ownership of a1a9f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYDe../746e8.. ownership of d3e80.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ7J../8e5d8.. ownership of 82e3b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLFx../547c6.. ownership of 45a16.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYph../6def6.. ownership of 8f913.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKvu../1a5e4.. ownership of 43b91.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWFu../01f62.. ownership of 10a0b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSb3../9b936.. ownership of e6223.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMBf../616b6.. ownership of 839f4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcFY../4c427.. ownership of f4ee1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJHY../f55a6.. ownership of be77e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUHR../ef2cf.. ownership of aca6b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM1n../e8f2a.. ownership of 5c211.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKuo../8086a.. ownership of 85336.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZCB../f3104.. ownership of 3238a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUMT../4660d.. ownership of ce785.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRkp../67520.. ownership of 26358.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ1e../2442d.. ownership of 7e0c9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMb58../c52d4.. ownership of d7fe6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK2y../54b28.. ownership of db15d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRta../d5af6.. ownership of 3db81.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUGa../02b81.. ownership of 70a91.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ6k../2005d.. ownership of 2fbbc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXft../661fe.. ownership of 11171.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd94../7bac6.. ownership of 4c9b8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdEf../f244e.. ownership of e5c15.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW8a../8dcd7.. ownership of c1ec7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYAT../b0cf6.. ownership of a7e78.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWQh../e2b13.. ownership of 40f7a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ2p../559bd.. ownership of d2696.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKsQ../c40b0.. ownership of 64059.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYKC../d16d4.. ownership of f4e77.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdck../78ddd.. ownership of 5a21d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdzY../01804.. ownership of 0dbaa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUSR../64211.. ownership of f336d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXtp../7cd50.. ownership of 94c43.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMU2x../3264e.. ownership of 0b783.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVnQ../061e6.. ownership of e256c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPDx../fd14b.. ownership of f1083.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdQj../335e4.. ownership of 375af.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQgn../0900e.. ownership of 4b095.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWg7../8a66a.. ownership of ce903.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMam4../bb77c.. ownership of 054cd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKz3../84653.. ownership of 684cb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNkU../07abb.. ownership of 1b1d1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWLR../7365a.. ownership of 2602c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQUe../e06e0.. ownership of efbae.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdhV../93b22.. ownership of e673f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ3D../67d9d.. ownership of bba3d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNLm../0ebff.. ownership of f1a52.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRtr../b91d4.. ownership of 958ef.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPdr../97786.. ownership of dec29.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMCB../1bf8f.. ownership of 5faa3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGps../22d81.. ownership of 38ce5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPNj../5d46c.. ownership of c79db.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNk4../e18e6.. ownership of 4c4b2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUCr../18eb6.. ownership of a5fe0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbMf../e35c6.. ownership of 0353a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHYF../4f93c.. ownership of 695d8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGWw../48431.. ownership of badc5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXew../50d25.. ownership of 3eff2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT98../f6d11.. ownership of 1ac99.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUfi../4cbe2.. ownership of 2d07f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbWK../7ecf8.. ownership of 0eb22.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVhW../e4d33.. ownership of ac5c1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJw7../d0c62.. ownership of e75b5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXxK../01925.. ownership of d0a1f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP3w../24e7b.. ownership of 78dd4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXmt../efe47.. ownership of edd11.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPmQ../a1933.. ownership of b4672.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNcw../b7664.. ownership of 287ca.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQxi../f1f5e.. ownership of e4d6e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY5S../0fa35.. ownership of da962.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPuf../12345.. ownership of 0b5b6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKgz../2df85.. ownership of 62c05.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRrG../7cfdf.. ownership of 1b39b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTPE../38de8.. ownership of c5d9a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNDB../ede94.. ownership of 21ecc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMW9../9e3c6.. ownership of 72294.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUF1../1fd79.. ownership of 0af09.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTTj../909f5.. ownership of 3daee.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTVS../16299.. ownership of 85c22.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVEc../b4a72.. ownership of b21da.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPK3../2afe1.. ownership of 4134b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUdk../0e0ae.. ownership of cf34a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGCx../194c7.. ownership of 34a9c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS6H../0be6c.. ownership of b0a2d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHTC../2239f.. ownership of 68109.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVa2../1d808.. ownership of e8942.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMajk../fbb74.. ownership of eb7b9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSBz../e4a79.. ownership of 2b26f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdui../6ae3e.. ownership of 73a09.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNtw../5adf8.. ownership of 1ffa0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHNY../9393b.. ownership of 852f3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPjQ../459f4.. ownership of 27172.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXhw../06980.. ownership of 79acc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWHH../f47b6.. ownership of 0d18f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWfj../cb3db.. ownership of 4c539.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR7M../f6e20.. ownership of ceda5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP6d../59cf4.. ownership of b3b69.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWKH../d722b.. ownership of 4ea1c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQwR../03ac2.. ownership of d05b3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZjr../93bcc.. ownership of 33d44.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVBH../cc531.. ownership of 7a200.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUEY../77679.. ownership of f9d06.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZiw../742a3.. ownership of 7500b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKzz../7d9a2.. ownership of 76d8b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMFm../f9757.. ownership of 17c76.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdQx../fb56e.. ownership of 46513.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNvs../b25fa.. ownership of d6130.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYqN../6d307.. ownership of d81ac.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTwt../38e47.. ownership of 7f6e6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLSf../9986d.. ownership of 80543.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdAo../d6a35.. ownership of ed32c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZmT../156fc.. ownership of ba6d2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML79../6d1cd.. ownership of 5d069.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPrM../3a9bf.. ownership of 96761.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMKV../8e4b6.. ownership of 017a0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaWK../d5a6c.. ownership of cfca3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcAN../e6e1e.. ownership of 8df6e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZMM../ec0ed.. ownership of 3e73f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY8t../f4676.. ownership of e44f3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHUP../79e87.. ownership of 8b103.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHw7../10526.. ownership of 445f7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNza../11f04.. ownership of 2b2c8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbFb../ff0ae.. ownership of 2f2ea.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPt1../f9521.. ownership of d42ef.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TML4p../67383.. ownership of aa8d2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUE7../ac454.. ownership of 802b4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZ2A../734bc.. ownership of 48ef8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFH5../86b4b.. ownership of 80d24.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSao../0540a.. ownership of ba9d8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJQH../7d9b0.. ownership of c4281.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRHA../d5280.. ownership of f4851.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMUu../c7008.. ownership of ee28d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNfn../8bcd4.. ownership of 2cbe2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFFk../886cc.. ownership of 538bb.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcMJ../d53e2.. ownership of 4ae4a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMau8../36459.. ownership of 19043.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZmd../74d21.. ownership of d3786.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPGW../d57c0.. ownership of dd6eb.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaoh../a5fba.. ownership of 0ac37.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTos../612b5.. ownership of 38283.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLPm../b7235.. ownership of e5b72.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHMK../7e95a.. ownership of 9018f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUUEj../f44cf.. doc published by PrGxv..
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2 (proof)
Theorem and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Theorem or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2 (proof)
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2 (proof)
Theorem or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2 (proof)
Theorem or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3 (proof)
Theorem and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3 (proof)
Theorem and4E : ∀ x0 x1 x2 x3 : ο . and (and (and x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4) ⟶ x4 (proof)
Theorem or4I1 : ∀ x0 x1 x2 x3 : ο . x0 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem or4I2 : ∀ x0 x1 x2 x3 : ο . x1 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem or4I3 : ∀ x0 x1 x2 x3 : ο . x2 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem or4I4 : ∀ x0 x1 x2 x3 : ο . x3 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem or4E : ∀ x0 x1 x2 x3 : ο . or (or (or x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x4) ⟶ (x1 ⟶ x4) ⟶ (x2 ⟶ x4) ⟶ (x3 ⟶ x4) ⟶ x4 (proof)
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known 0ddd1.. : ∀ x0 x1 . (∀ x2 . iff (prim1 x2 x0) (prim1 x2 x1)) ⟶ x0 = x1
Known iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1 (proof)
Theorem Subq_ref : ∀ x0 . Subq x0 x0 (proof)
Theorem Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2 (proof)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Known xm : ∀ x0 : ο . or x0 (not x0)
Known FalseE : False ⟶ ∀ x0 : ο . x0
Theorem dneg : ∀ x0 : ο . not (not x0) ⟶ x0 (proof)
Param 4a7ef.. : ι
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem 2b26f.. : not (∀ x0 : ο . (∀ x1 . prim1 x1 4a7ef.. ⟶ x0) ⟶ x0) (proof)
Theorem e8942.. : ∀ x0 . Subq 4a7ef.. x0 (proof)
Param c2e41.. : ι → ι → ο
Known adb47.. : ∀ x0 . ∀ x1 : ο . (∀ x2 . and (and (and (prim1 x0 x2) (∀ x3 x4 . prim1 x3 x2 ⟶ Subq x4 x3 ⟶ prim1 x4 x2)) (∀ x3 . prim1 x3 x2 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x2) (∀ x6 . Subq x6 x3 ⟶ prim1 x6 x5) ⟶ x4) ⟶ x4)) (∀ x3 . Subq x3 x2 ⟶ or (c2e41.. x3 x2) (prim1 x3 x2)) ⟶ x1) ⟶ x1
Param 1216a.. : ι → (ι → ο) → ι
Known 492ff.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ ∀ x3 : ο . (prim1 x2 x0 ⟶ x1 x2 ⟶ x3) ⟶ x3
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Theorem b0a2d.. : ∀ x0 . ∀ x1 : ο . (∀ x2 . (∀ x3 . iff (prim1 x3 x2) (Subq x3 x0)) ⟶ x1) ⟶ x1 (proof)
Definition e5b72.. := λ x0 . prim0 (λ x1 . ∀ x2 . iff (prim1 x2 x1) (Subq x2 x0))
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem cf34a.. : ∀ x0 x1 . iff (prim1 x1 (e5b72.. x0)) (Subq x1 x0) (proof)
Theorem b21da.. : ∀ x0 x1 . prim1 x1 (e5b72.. x0) ⟶ Subq x1 x0 (proof)
Theorem 3daee.. : ∀ x0 x1 . Subq x1 x0 ⟶ prim1 x1 (e5b72.. x0) (proof)
Theorem 72294.. : ∀ x0 x1 . Subq x0 x1 ⟶ Subq (e5b72.. x0) (e5b72.. x1) (proof)
Theorem c5d9a.. : ∀ x0 . prim1 4a7ef.. (e5b72.. x0) (proof)
Theorem 62c05.. : ∀ x0 . prim1 x0 (e5b72.. x0) (proof)
Definition 0ac37.. := λ x0 x1 . prim3 (prim2 x0 x1)
Known UnionI : ∀ x0 x1 x2 . prim1 x1 x2 ⟶ prim1 x2 x0 ⟶ prim1 x1 (prim3 x0)
Known 67787.. : ∀ x0 x1 . prim1 x0 (prim2 x0 x1)
Theorem da962.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 (0ac37.. x0 x1) (proof)
Known 5a932.. : ∀ x0 x1 . prim1 x1 (prim2 x0 x1)
Theorem 287ca.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 x2 (0ac37.. x0 x1) (proof)
Known UnionE_impred : ∀ x0 x1 . prim1 x1 (prim3 x0) ⟶ ∀ x2 : ο . (∀ x3 . prim1 x1 x3 ⟶ prim1 x3 x0 ⟶ x2) ⟶ x2
Known 2532b.. : ∀ x0 x1 x2 . prim1 x0 (prim2 x1 x2) ⟶ or (x0 = x1) (x0 = x2)
Theorem edd11.. : ∀ x0 x1 x2 . prim1 x2 (0ac37.. x0 x1) ⟶ or (prim1 x2 x0) (prim1 x2 x1) (proof)
Known 6982e.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ and (prim1 x2 x0) (x1 x2)
Theorem d0a1f.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ prim1 x2 x0 (proof)
Theorem ac5c1.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ x1 x2 (proof)
Definition d3786.. := λ x0 x1 . 1216a.. x0 (λ x2 . prim1 x2 x1)
Theorem 2d07f.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 x1 ⟶ prim1 x2 (d3786.. x0 x1) (proof)
Theorem 3eff2.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ and (prim1 x2 x0) (prim1 x2 x1) (proof)
Theorem 695d8.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ prim1 x2 x0 (proof)
Theorem a5fe0.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ prim1 x2 x1 (proof)
Param 91630.. : ι → ι
Definition 4ae4a.. := λ x0 . 0ac37.. x0 (91630.. x0)
Theorem c79db.. : ∀ x0 . Subq x0 (4ae4a.. x0) (proof)
Known e7a4c.. : ∀ x0 . prim1 x0 (91630.. x0)
Theorem 5faa3.. : ∀ x0 . prim1 x0 (4ae4a.. x0) (proof)
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0
Theorem 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0) (proof)
Known 113d7.. : ∀ x0 x1 . prim1 x1 x0 ⟶ ∀ x2 : ο . (∀ x3 . and (prim1 x3 x0) (not (∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (prim1 x5 x3) ⟶ x4) ⟶ x4)) ⟶ x2) ⟶ x2
Theorem bba3d.. : ∀ x0 x1 . prim1 x0 x1 ⟶ nIn x1 x0 (proof)
Theorem efbae.. : ∀ x0 . 4a7ef.. = 4ae4a.. x0 ⟶ ∀ x1 : ο . x1 (proof)
Theorem 1b1d1.. : ∀ x0 . 4ae4a.. x0 = 4a7ef.. ⟶ ∀ x1 : ο . x1 (proof)
Theorem 054cd.. : ∀ x0 x1 . 4ae4a.. x0 = 4ae4a.. x1 ⟶ x0 = x1 (proof)
Theorem 4b095.. : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ 4ae4a.. x0 = 4ae4a.. x1 ⟶ ∀ x2 : ο . x2 (proof)
Theorem f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..) (proof)
Theorem 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Definition TransSet := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Definition ordinal := λ x0 . and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1)
Known andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Theorem ordinal_TransSet : ∀ x0 . ordinal x0 ⟶ TransSet x0 (proof)
Known andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem ordinal_In_TransSet : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ TransSet x1 (proof)
Theorem 40f7a.. : ordinal 4a7ef.. (proof)
Theorem ordinal_Hered : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ordinal x1 (proof)
Definition ba9d8.. := λ x0 . ∀ x1 : ι → ο . x1 4a7ef.. ⟶ (∀ x2 . x1 x2 ⟶ x1 (4ae4a.. x2)) ⟶ x1 x0
Theorem 4c9b8.. : ba9d8.. 4a7ef.. (proof)
Theorem 2fbbc.. : ∀ x0 . ba9d8.. x0 ⟶ ba9d8.. (4ae4a.. x0) (proof)
Theorem 3db81.. : ba9d8.. (4ae4a.. 4a7ef..) (proof)
Theorem d7fe6.. : ba9d8.. (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem 26358.. : ∀ x0 . ba9d8.. x0 ⟶ prim1 4a7ef.. (4ae4a.. x0) (proof)
Theorem 3238a.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) (4ae4a.. x0) (proof)
Theorem 5c211.. : ∀ x0 : ι → ο . x0 4a7ef.. ⟶ (∀ x1 . ba9d8.. x1 ⟶ x0 x1 ⟶ x0 (4ae4a.. x1)) ⟶ ∀ x1 . ba9d8.. x1 ⟶ x0 x1 (proof)
Theorem be77e.. : ∀ x0 . ba9d8.. x0 ⟶ or (x0 = 4a7ef..) (∀ x1 : ο . (∀ x2 . and (ba9d8.. x2) (x0 = 4ae4a.. x2) ⟶ x1) ⟶ x1) (proof)
Theorem 839f4.. : ∀ x0 : ι → ο . (∀ x1 . ba9d8.. x1 ⟶ (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ba9d8.. x1 ⟶ x0 x1 (proof)
Theorem 10a0b.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ba9d8.. x1 (proof)
Theorem 8f913.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0 (proof)
Theorem 82e3b.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 (4ae4a.. x0) ⟶ Subq x1 x0 (proof)
Theorem a1a9f.. : ∀ x0 . TransSet x0 ⟶ TransSet (4ae4a.. x0) (proof)
Theorem b72a3.. : ∀ x0 . ordinal x0 ⟶ ordinal (4ae4a.. x0) (proof)
Theorem f3fb5.. : ∀ x0 . ba9d8.. x0 ⟶ ordinal x0 (proof)
Theorem 4114a.. : ∀ x0 : ο . (∀ x1 . (∀ x2 . iff (prim1 x2 x1) (ba9d8.. x2)) ⟶ x0) ⟶ x0 (proof)
Definition 48ef8.. := prim0 (λ x0 . ∀ x1 . iff (prim1 x1 x0) (ba9d8.. x1))
Theorem 6c085.. : ∀ x0 . iff (prim1 x0 48ef8..) (ba9d8.. x0) (proof)
Theorem c2711.. : ∀ x0 . prim1 x0 48ef8.. ⟶ ba9d8.. x0 (proof)
Theorem a3321.. : ∀ x0 . ba9d8.. x0 ⟶ prim1 x0 48ef8.. (proof)
Theorem 8ee89.. : prim1 4a7ef.. 48ef8.. (proof)
Theorem 98ac3.. : ∀ x0 . prim1 x0 48ef8.. ⟶ prim1 (4ae4a.. x0) 48ef8.. (proof)
Definition aa8d2.. := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . x3 4a7ef.. x1 ⟶ (∀ x4 . ba9d8.. x4 ⟶ ∀ x5 . x3 x4 x5 ⟶ x3 (4ae4a.. x4) (prim3 x5)) ⟶ x3 x0 x2
Theorem 4a672.. : ∀ x0 . aa8d2.. 4a7ef.. x0 x0 (proof)
Theorem b5347.. : ∀ x0 x1 . ba9d8.. x1 ⟶ ∀ x2 . aa8d2.. x1 x0 x2 ⟶ aa8d2.. (4ae4a.. x1) x0 (prim3 x2) (proof)
Theorem ac124.. : ∀ x0 . ∀ x1 : ι → ι → ο . x1 4a7ef.. x0 ⟶ (∀ x2 . ba9d8.. x2 ⟶ ∀ x3 . aa8d2.. x2 x0 x3 ⟶ x1 x2 x3 ⟶ x1 (4ae4a.. x2) (prim3 x3)) ⟶ ∀ x2 x3 . ba9d8.. x2 ⟶ aa8d2.. x2 x0 x3 ⟶ x1 x2 x3 (proof)
Theorem 5f7ef.. : ∀ x0 x1 x2 . ba9d8.. x1 ⟶ aa8d2.. x1 x0 x2 ⟶ or (and (x1 = 4a7ef..) (x2 = x0)) (∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . and (and (x1 = 4ae4a.. x4) (x2 = prim3 x6)) (aa8d2.. x4 x0 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) (proof)
Theorem a87f5.. : ∀ x0 x1 . aa8d2.. 4a7ef.. x0 x1 ⟶ x1 = x0 (proof)
Theorem f1d4d.. : ∀ x0 x1 x2 . ba9d8.. x0 ⟶ aa8d2.. (4ae4a.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . and (x2 = prim3 x4) (aa8d2.. x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem 8312b.. : ∀ x0 x1 . ba9d8.. x1 ⟶ ∀ x2 : ο . (∀ x3 . aa8d2.. x1 x0 x3 ⟶ x2) ⟶ x2 (proof)
Theorem 0cbec.. : ∀ x0 x1 . ba9d8.. x1 ⟶ ∀ x2 x3 . aa8d2.. x1 x0 x2 ⟶ aa8d2.. x1 x0 x3 ⟶ x2 = x3 (proof)
Theorem 3e6f6.. : ∀ x0 x1 . ba9d8.. x0 ⟶ aa8d2.. x0 x1 (prim0 (aa8d2.. x0 x1)) (proof)
Theorem 2cb0a.. : ∀ x0 . prim0 (aa8d2.. 4a7ef.. x0) = x0 (proof)
Theorem 057f4.. : ∀ x0 x1 . ba9d8.. x0 ⟶ prim0 (aa8d2.. (4ae4a.. x0) x1) = prim3 (prim0 (aa8d2.. x0 x1)) (proof)
Param 94f9e.. : ι → (ι → ι) → ι
Definition 2f2ea.. := λ x0 . prim3 (94f9e.. 48ef8.. (λ x1 . prim0 (aa8d2.. x1 x0)))
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem 7fd4e.. : ∀ x0 x1 x2 . ba9d8.. x2 ⟶ prim1 x1 (prim0 (aa8d2.. x2 x0)) ⟶ prim1 x1 (2f2ea.. x0) (proof)
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem 45a0f.. : ∀ x0 x1 . prim1 x1 (2f2ea.. x0) ⟶ ∀ x2 : ο . (∀ x3 . ba9d8.. x3 ⟶ prim1 x1 (prim0 (aa8d2.. x3 x0)) ⟶ x2) ⟶ x2 (proof)
Theorem 96add.. : ∀ x0 . Subq x0 (2f2ea.. x0) (proof)
Theorem fb6d0.. : ∀ x0 . TransSet (2f2ea.. x0) (proof)
Theorem In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1 (proof)