Proofgold Signed Transaction

vin
PrEvg../7458c.. PUho7../c2c08..

vout

PrEvg../081b8.. 0.31 bars
TMXrm../fb8a1.. ownership of e5b9d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZt6../cc1f1.. ownership of 1386f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXMe../f8279.. ownership of a7ca6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZeF../71c6f.. ownership of dae3b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNdM../fbc61.. ownership of 4604c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ5f../07cd1.. ownership of a8c97.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHbc../b80d1.. ownership of ddf85.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXjR../1223e.. ownership of 57bc9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcDY../42f05.. ownership of 7f73e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXVt../fde5a.. ownership of d6c01.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaKB../16e4a.. ownership of c0fdc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGEQ../19f28.. ownership of 4827c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSKw../bdf92.. ownership of 9ba2e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKzE../82931.. ownership of fa315.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKwH../c6d88.. ownership of 24637.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVu5../4ee43.. ownership of 2de7a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUPj../9a9a8.. ownership of dd8c7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUEt../de573.. ownership of 90514.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXrx../45faf.. ownership of 27d99.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVvg../ca173.. ownership of 4a87b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFdG../78d7e.. ownership of 946ce.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT92../ae651.. ownership of 7aec4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRMW../642d5.. ownership of 8b22b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGGq../6178b.. ownership of 6b9d4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWEz../5c037.. ownership of 69fa6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG9A../40941.. ownership of a6bb8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNS1../d02b2.. ownership of a4174.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFAc../67d0a.. ownership of 09720.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKmN../5b7a6.. ownership of 39b30.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZL8../87842.. ownership of 4a2f5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMccc../108f4.. ownership of 0bcfd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMax5../d6cff.. ownership of 4eae4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPyS../d61d3.. ownership of 9f718.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdFR../ed4a6.. ownership of d9a7c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX2v../666e0.. ownership of bc67e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKCB../a99f8.. ownership of 29be8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXiX../92610.. ownership of 8c01c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLw5../15719.. ownership of 5f057.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXYb../979d2.. ownership of 76f37.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSzb../7ac43.. ownership of 60c6d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWnW../222d6.. ownership of 440fc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJya../fcb0d.. ownership of d8c3b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV96../95eb7.. ownership of a7d3d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTUV../c232f.. ownership of 574d7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEm7../14b6b.. ownership of ae479.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbus../2ba48.. ownership of 5f6e0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYGP../821ed.. ownership of 113f8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdqa../04406.. ownership of 4ea57.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMchN../a9b23.. ownership of b4867.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc1r../c6cc5.. ownership of f7aff.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHhH../c8ea8.. ownership of c4945.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSNt../ccf32.. ownership of 2ff1c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJxa../f6bc3.. ownership of 15e57.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN2W../148f9.. ownership of b2f81.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGKC../96b46.. ownership of e2910.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHqb../479eb.. ownership of 64b6e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZQP../334a5.. ownership of 27c9e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdmT../022f9.. ownership of 336cf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYMP../1df6c.. ownership of 1743f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHFG../0e6bd.. ownership of 38161.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcy8../1a39e.. ownership of 76e53.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS4n../0a593.. ownership of 11065.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNEb../69e5e.. ownership of 6f6b2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZmk../7e12f.. ownership of b480f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX18../e227d.. ownership of 6a8ef.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM51../e785d.. ownership of 09540.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJqv../88cf2.. ownership of 54858.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJ9T../2d59c.. ownership of 25f7f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGFm../017ff.. ownership of 15728.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZUw../5bc07.. ownership of ba177.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdwd../15d28.. ownership of 7cec7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGBC../77a83.. ownership of 4da59.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcL5../c8a8b.. ownership of 47fa3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFhC../cc5bc.. ownership of ba20c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQeo../59e4c.. ownership of ebfdf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLf5../14e33.. ownership of 0f655.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRnj../dbab1.. ownership of cd72e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLjB../dd3d0.. ownership of 9eab6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMhp../5304a.. ownership of ece62.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbdP../0bbda.. ownership of 6e5b2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKN8../3c26d.. ownership of 5c80a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWqG../dbf2f.. ownership of 59bda.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJxf../3c626.. ownership of e5851.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXYu../f809f.. ownership of bb101.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMduP../d3daa.. ownership of 22911.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMxC../e4750.. ownership of 9b77d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG3L../39fa7.. ownership of 52ec4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXoA../cbf46.. ownership of 2d62e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKZF../b50bb.. ownership of c0df0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNxH../fe016.. ownership of 6acab.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJuK../fdc0a.. ownership of 246a1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKos../a00a8.. ownership of 31521.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMchp../b31ac.. ownership of fec54.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWCs../3cc47.. ownership of b01fc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKyH../aa8e9.. ownership of 5ace0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT6c../a42ea.. ownership of 1a2f3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLms../b6e4b.. ownership of 815ee.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcph../3c921.. ownership of b364c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLJQ../522be.. ownership of bd6e2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSKF../40100.. ownership of eb591.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMU81../cd955.. ownership of 86782.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQf3../3fd0b.. ownership of 0186c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPCN../65a85.. ownership of 7807d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV5Y../fdc94.. ownership of 68779.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNuT../6ed69.. ownership of 028a8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRCr../9cbf1.. ownership of ad46e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRys../423c6.. ownership of c3e99.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKFs../9031c.. ownership of 0a410.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEsY../5c0fc.. ownership of c790e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEgk../381c2.. ownership of 046be.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVLU../78867.. ownership of 3e143.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV8X../607ea.. ownership of 391a1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG6G../258af.. ownership of b1aa3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUgY../16f57.. ownership of d98b9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS3v../29013.. ownership of fde1a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcAr../13c3f.. ownership of bf154.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYAP../82e89.. ownership of 2a17a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRLa../be77b.. ownership of ce2d2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFgh../50b9d.. ownership of b4f32.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdsN../7a12e.. ownership of 3dfc6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQbS../0ef94.. ownership of 410dc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFG2../9639f.. ownership of 0128f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKwk../c3b6c.. ownership of 12629.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQP2../8d474.. ownership of 2b95d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJV2../1ed67.. ownership of 8bc8d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWEU../b6898.. ownership of cdf76.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKPV../7db88.. ownership of d5e26.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFBJ../00c5b.. ownership of fbe49.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF7x../a1d9f.. ownership of e9c5f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcV5../f5b03.. ownership of 1d55d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTTu../7e8f2.. ownership of e791b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMLk../8d769.. ownership of 2b650.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKaa../af85a.. ownership of 84650.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXcS../0dda4.. ownership of 94aee.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSJQ../72bb9.. ownership of 8f242.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKx9../1a29c.. ownership of c1dd2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGS3../f5b6e.. ownership of 9b3a8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMctp../76433.. ownership of 60caf.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbSA../a7ad7.. ownership of 533cc.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRij../38daf.. ownership of 0cae5.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKaB../4bbfa.. ownership of f3c9a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdi3../8b4b3.. ownership of 018ce.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRoX../3904d.. ownership of 6edba.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMU3v../7bed0.. ownership of d4b05.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNdr../418f2.. ownership of fac41.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRQ4../4297f.. ownership of 350a1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWDM../818b5.. ownership of fde50.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMnE../4aea5.. ownership of 48e4c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH4o../66e62.. ownership of 6cf28.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQPp../4d657.. ownership of 62f23.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSVG../8e641.. ownership of bf2fb.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRZM../2816b.. ownership of 1d2e5.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJRu../9e592.. ownership of 2bb1d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFeU../84225.. ownership of f2c83.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMafE../6ef36.. ownership of 33147.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQgG../7469e.. ownership of 38165.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJ5C../193b2.. ownership of 17057.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNdx../dc969.. ownership of eb9e2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKvk../797aa.. ownership of 38783.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK3q../bcadb.. ownership of 00c30.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHB8../03674.. ownership of 88f2d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQSn../89d89.. ownership of 7bdba.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFXp../238fa.. ownership of b8ff5.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PULk4../df18f.. doc published by PrGxv..

Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Theorem In_irref : ∀ x0 . nIn x0 x0 (proof)
Theorem 3dfc6.. : ∀ x0 x1 x2 . prim1 x0 x1 ⟶ prim1 x1 x2 ⟶ nIn x2 x0 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem Eps_i_set_R : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ and (prim1 (prim0 (λ x3 . and (prim1 x3 x0) (x1 x3))) x0) (x1 (prim0 (λ x3 . and (prim1 x3 x0) (x1 x3)))) (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition If_i := λ x0 : ο . λ x1 x2 . prim0 (λ x3 . or (and x0 (x3 = x1)) (and (not x0) (x3 = x2)))
Known xm : ∀ x0 : ο . or x0 (not x0)
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem If_i_correct : ∀ x0 : ο . ∀ x1 x2 . or (and x0 (If_i x0 x1 x2 = x1)) (and (not x0) (If_i x0 x1 x2 = x2)) (proof)
Known andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2 (proof)
Theorem If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1 (proof)
Theorem If_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2) (proof)
Theorem If_i_eta : ∀ x0 : ο . ∀ x1 . If_i x0 x1 x1 = x1 (proof)
Theorem exandE_ii : ∀ x0 x1 : (ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Theorem exandE_iii : ∀ x0 x1 : (ι → ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Theorem exandE_iiii : ∀ x0 x1 : (ι → ι → ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Theorem exandE_iio : ∀ x0 x1 : (ι → ι → ο) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ο . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ο . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Theorem exandE_iiio : ∀ x0 x1 : (ι → ι → ι → ο) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ο . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι → ο . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Definition Descr_ii := λ x0 : (ι → ι) → ο . λ x1 . prim0 (λ x2 . ∀ x3 : ι → ι . x0 x3 ⟶ x3 x1 = x2)
Theorem Descr_ii_prop : ∀ x0 : (ι → ι) → ο . (∀ x1 : ο . (∀ x2 : ι → ι . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ι . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_ii x0) (proof)
Definition Descr_iii := λ x0 : (ι → ι → ι) → ο . λ x1 x2 . prim0 (λ x3 . ∀ x4 : ι → ι → ι . x0 x4 ⟶ x4 x1 x2 = x3)
Theorem Descr_iii_prop : ∀ x0 : (ι → ι → ι) → ο . (∀ x1 : ο . (∀ x2 : ι → ι → ι . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ι → ι . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_iii x0) (proof)
Definition Descr_iio := λ x0 : (ι → ι → ο) → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . x0 x3 ⟶ x3 x1 x2
Known prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem Descr_iio_prop : ∀ x0 : (ι → ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ι → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_iio x0) (proof)
Definition Descr_Vo1 := λ x0 : (ι → ο) → ο . λ x1 . ∀ x2 : ι → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo1_prop : ∀ x0 : (ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo1 x0) (proof)
Definition Descr_Vo2 := λ x0 : ((ι → ο) → ο) → ο . λ x1 : ι → ο . ∀ x2 : (ι → ο) → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo2_prop : ∀ x0 : ((ι → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : (ι → ο) → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : (ι → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo2 x0) (proof)
Definition If_ii := λ x0 : ο . λ x1 x2 : ι → ι . λ x3 . If_i x0 (x1 x3) (x2 x3)
Theorem If_ii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . x0 ⟶ If_ii x0 x1 x2 = x1 (proof)
Theorem If_ii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . not x0 ⟶ If_ii x0 x1 x2 = x2 (proof)
Definition If_iii := λ x0 : ο . λ x1 x2 : ι → ι → ι . λ x3 x4 . If_i x0 (x1 x3 x4) (x2 x3 x4)
Theorem If_iii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . x0 ⟶ If_iii x0 x1 x2 = x1 (proof)
Theorem If_iii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . not x0 ⟶ If_iii x0 x1 x2 = x2 (proof)
Definition If_Vo1 := λ x0 : ο . λ x1 x2 : ι → ο . λ x3 . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem If_Vo1_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . x0 ⟶ If_Vo1 x0 x1 x2 = x1 (proof)
Theorem If_Vo1_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . not x0 ⟶ If_Vo1 x0 x1 x2 = x2 (proof)
Definition If_iio := λ x0 : ο . λ x1 x2 : ι → ι → ο . λ x3 x4 . and (x0 ⟶ x1 x3 x4) (not x0 ⟶ x2 x3 x4)
Theorem If_iio_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . x0 ⟶ If_iio x0 x1 x2 = x1 (proof)
Theorem If_iio_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . not x0 ⟶ If_iio x0 x1 x2 = x2 (proof)
Definition If_Vo2 := λ x0 : ο . λ x1 x2 : (ι → ο) → ο . λ x3 : ι → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Theorem If_Vo2_1 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . x0 ⟶ If_Vo2 x0 x1 x2 = x1 (proof)
Theorem If_Vo2_0 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . not x0 ⟶ If_Vo2 x0 x1 x2 = x2 (proof)
Definition In_rec_i_G := λ x0 : ι → (ι → ι) → ι . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 . ∀ x5 : ι → ι . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_i := λ x0 : ι → (ι → ι) → ι . λ x1 . prim0 (In_rec_i_G x0 x1)
Theorem In_rec_i_G_c : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x1 ⟶ In_rec_i_G x0 x3 (x2 x3)) ⟶ In_rec_i_G x0 x1 (x0 x1 x2) (proof)
Theorem In_rec_i_G_inv : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 x2 . In_rec_i_G x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι . and (∀ x5 . prim1 x5 x1 ⟶ In_rec_i_G x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem In_rec_i_G_f : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 x2 x3 . In_rec_i_G x0 x1 x2 ⟶ In_rec_i_G x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem In_rec_i_G_In_rec_i : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_i_G x0 x1 (In_rec_i x0 x1) (proof)
Theorem In_rec_i_G_In_rec_i_d : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_i_G x0 x1 (x0 x1 (In_rec_i x0)) (proof)
Theorem In_rec_i_eq : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_i x0 x1 = x0 x1 (In_rec_i x0) (proof)
Definition In_rec_G_ii := λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . λ x2 : ι → ι . ∀ x3 : ι → (ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_ii := λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . Descr_ii (In_rec_G_ii x0 x1)
Theorem In_rec_G_ii_c : ∀ x0 : ι → (ι → ι → ι) → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 . prim1 x3 x1 ⟶ In_rec_G_ii x0 x3 (x2 x3)) ⟶ In_rec_G_ii x0 x1 (x0 x1 x2) (proof)
Theorem In_rec_G_ii_inv : ∀ x0 : ι → (ι → ι → ι) → ι → ι . ∀ x1 . ∀ x2 : ι → ι . In_rec_G_ii x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι . and (∀ x5 . prim1 x5 x1 ⟶ In_rec_G_ii x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem In_rec_G_ii_f : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι . In_rec_G_ii x0 x1 x2 ⟶ In_rec_G_ii x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem In_rec_G_ii_In_rec_ii : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_G_ii x0 x1 (In_rec_ii x0 x1) (proof)
Theorem In_rec_G_ii_In_rec_ii_d : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_G_ii x0 x1 (x0 x1 (In_rec_ii x0)) (proof)
Theorem In_rec_ii_eq : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_ii x0 x1 = x0 x1 (In_rec_ii x0) (proof)
Definition In_rec_G_iii := λ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . λ x1 . λ x2 : ι → ι → ι . ∀ x3 : ι → (ι → ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ι . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_iii := λ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . λ x1 . Descr_iii (In_rec_G_iii x0 x1)
Theorem In_rec_G_iii_c : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι → ι . (∀ x3 . prim1 x3 x1 ⟶ In_rec_G_iii x0 x3 (x2 x3)) ⟶ In_rec_G_iii x0 x1 (x0 x1 x2) (proof)
Theorem In_rec_G_iii_inv : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . In_rec_G_iii x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι → ι . and (∀ x5 . prim1 x5 x1 ⟶ In_rec_G_iii x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem In_rec_G_iii_f : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι → ι . In_rec_G_iii x0 x1 x2 ⟶ In_rec_G_iii x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem In_rec_G_iii_In_rec_iii : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_G_iii x0 x1 (In_rec_iii x0 x1) (proof)
Theorem In_rec_G_iii_In_rec_iii_d : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_G_iii x0 x1 (x0 x1 (In_rec_iii x0)) (proof)
Theorem In_rec_iii_eq : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_iii x0 x1 = x0 x1 (In_rec_iii x0) (proof)
Definition 94aee.. := λ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . λ x1 . λ x2 : ι → ι → ο . ∀ x3 : ι → (ι → ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ο . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_iio := λ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . λ x1 . Descr_iio (94aee.. x0 x1)
Theorem bc67e.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ι → ο . (∀ x3 . prim1 x3 x1 ⟶ 94aee.. x0 x3 (x2 x3)) ⟶ 94aee.. x0 x1 (x0 x1 x2) (proof)
Theorem 9f718.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . 94aee.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι → ο . and (∀ x5 . prim1 x5 x1 ⟶ 94aee.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem 0bcfd.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι → ο . 94aee.. x0 x1 x2 ⟶ 94aee.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem 39b30.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 94aee.. x0 x1 (In_rec_iio x0 x1) (proof)
Theorem a4174.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 94aee.. x0 x1 (x0 x1 (In_rec_iio x0)) (proof)
Theorem In_rec_iio_eq : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_iio x0 x1 = x0 x1 (In_rec_iio x0) (proof)
Definition 1d55d.. := λ x0 : ι → (ι → ι → ο) → ι → ο . λ x1 . λ x2 : ι → ο . ∀ x3 : ι → (ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_Vo1 := λ x0 : ι → (ι → ι → ο) → ι → ο . λ x1 . Descr_Vo1 (1d55d.. x0 x1)
Theorem 8b22b.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 . prim1 x3 x1 ⟶ 1d55d.. x0 x3 (x2 x3)) ⟶ 1d55d.. x0 x1 (x0 x1 x2) (proof)
Theorem 946ce.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ο . 1d55d.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ο . and (∀ x5 . prim1 x5 x1 ⟶ 1d55d.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem 27d99.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ο . 1d55d.. x0 x1 x2 ⟶ 1d55d.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem dd8c7.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 1d55d.. x0 x1 (In_rec_Vo1 x0 x1) (proof)
Theorem 24637.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 1d55d.. x0 x1 (x0 x1 (In_rec_Vo1 x0)) (proof)
Theorem In_rec_Vo1_eq : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_Vo1 x0 x1 = x0 x1 (In_rec_Vo1 x0) (proof)
Definition cdf76.. := λ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . λ x1 . λ x2 : (ι → ο) → ο . ∀ x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → (ι → ο) → ο . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_Vo2 := λ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . λ x1 . Descr_Vo2 (cdf76.. x0 x1)
Theorem c0fdc.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → (ι → ο) → ο . (∀ x3 . prim1 x3 x1 ⟶ cdf76.. x0 x3 (x2 x3)) ⟶ cdf76.. x0 x1 (x0 x1 x2) (proof)
Theorem 7f73e.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . cdf76.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → (ι → ο) → ο . and (∀ x5 . prim1 x5 x1 ⟶ cdf76.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem ddf85.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : (ι → ο) → ο . cdf76.. x0 x1 x2 ⟶ cdf76.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem 4604c.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . cdf76.. x0 x1 (In_rec_Vo2 x0 x1) (proof)
Theorem a7ca6.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . cdf76.. x0 x1 (x0 x1 (In_rec_Vo2 x0)) (proof)
Theorem In_rec_Vo2_eq : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_Vo2 x0 x1 = x0 x1 (In_rec_Vo2 x0) (proof)