Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrJAV../ba798..
PUaYe../f81a6..
vout
PrJAV../d2852.. 6.58 bars
TMGWV../cfd4c.. negprop ownership controlledby Pr6Pc.. upto 0
TMXxC../f56fc.. negprop ownership controlledby Pr6Pc.. upto 0
TMPsB../72bc7.. negprop ownership controlledby Pr6Pc.. upto 0
TMQn8../e918d.. ownership of 44a08.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMV5Q../d80c3.. ownership of cd3b8.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMVN7../52b12.. ownership of 604a8.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLBa../c0003.. ownership of d756b.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMWAt../196cc.. ownership of 77f23.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMaJc../2f634.. ownership of 174b8.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMRAa../ffba8.. ownership of 229d2.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMTj2../984bf.. ownership of 56488.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMTE1../9706b.. ownership of a456b.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TManf../081ff.. ownership of c2db2.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMRv9../372cf.. ownership of d57b0.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMEg6../a7cf8.. ownership of 7758f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMK6Y../7a6a8.. ownership of 5d6ce.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMR99../46cf2.. ownership of 4525e.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMK29../75596.. ownership of 24e4e.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMPvh../47b0c.. ownership of 5cf7e.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMKee../9165b.. ownership of 6a2dd.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMat1../3d43e.. ownership of db8a3.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMHuR../df99e.. ownership of e910c.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMG1L../012ae.. ownership of d6343.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMWCj../98bfc.. ownership of 6dd6f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGeZ../7175f.. ownership of 37df5.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMYKP../6f545.. ownership of 1e5b2.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMb9V../ce9d8.. ownership of b2f56.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMTvQ../64b36.. ownership of 4ab17.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMUKh../f9343.. ownership of 40e95.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMHs3../cecd9.. ownership of e6efb.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMaAY../1437f.. ownership of 9c442.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMYQw../25112.. ownership of 84fbe.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLoq../3e7a7.. ownership of 8ceeb.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMJ8U../19927.. ownership of eec29.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMKhP../fe672.. ownership of c81c0.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFY4../fb77c.. ownership of 4c1d5.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMc24../7fe21.. ownership of a68ea.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZUD../1a2b4.. ownership of e61e1.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMTGv../437a2.. ownership of a5352.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXQW../472e9.. ownership of 23277.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMYQQ../1c009.. ownership of 402bc.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXGF../6fafb.. ownership of fe4c8.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMQkJ../bd95b.. ownership of 79718.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZ6o../c8c47.. ownership of be11a.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMVRM../7f087.. ownership of 416ea.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFCU../2a0f2.. ownership of 9ba88.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMdur../5468d.. ownership of 981f4.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMMVC../a1019.. ownership of aa9c6.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZYe../cd47f.. ownership of 02d55.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMHUz../dd26f.. ownership of 95d3e.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXsY../9984d.. ownership of 0c8dd.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMTGM../2a003.. ownership of dc3ff.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMWDN../4fb11.. ownership of f8aae.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMQXw../5323f.. ownership of 318ef.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMbbY../7627e.. ownership of caa1f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMSFu../71021.. ownership of fdadb.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMP2o../2f8f9.. ownership of 6e401.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMa3V../4ea6b.. ownership of afa2b.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGa1../8fa6b.. ownership of 330a4.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMSxq../b711f.. ownership of 02444.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLQm../569fe.. ownership of 0d30f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFXi../0a835.. ownership of 59222.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMPTV../83ac4.. ownership of 5cb21.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXfA../68760.. ownership of f12d8.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGFU../3439c.. ownership of cc598.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMEju../8a3e8.. ownership of 126ee.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGi4../c14f3.. ownership of 3c5f2.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMNL3../8090d.. ownership of bb5a7.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZyK../a19fb.. ownership of 5625e.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMHdg../49365.. ownership of d79eb.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMapc../006b6.. ownership of 219cc.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMKmz../f81f1.. ownership of 61791.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMN2S../efd96.. ownership of 9b36a.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMKDD../06c85.. ownership of 7ecda.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMbkn../e17d7.. ownership of a625d.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLXE../c93a9.. ownership of a07c8.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXL6../2d1bc.. ownership of 0d7bd.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXRw../9ca35.. ownership of fbef0.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMQfd../de7c3.. ownership of 7797f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMbVc../906ae.. ownership of 0f583.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMa39../19dc1.. ownership of fe9b5.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMMcW../b3083.. ownership of cb4ca.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZb8../5a7d4.. ownership of 81137.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMMku../6d733.. ownership of 685d8.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMPy9../61cd5.. ownership of 07ae6.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFfR../21340.. ownership of 2d470.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMPbK../ec835.. ownership of 38ad3.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZir../b0dc4.. ownership of e6779.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMUSm../1cbe0.. ownership of b47fb.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZoS../3bc2b.. ownership of b26cf.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMTHH../ea8ba.. ownership of 392ce.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMJSr../8eca9.. ownership of aa5cd.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMUvT../9ba2e.. ownership of 4cb36.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMdFj../dfa96.. ownership of a41b2.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMW8G../e4587.. ownership of 6d1dd.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMPEv../1fe09.. ownership of 2b492.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLPc../db365.. ownership of 5d38f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMMLy../42a82.. ownership of 1b41d.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMPdr../de6c9.. ownership of 9f463.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGXG../e9c1d.. ownership of a261e.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGRe../5b313.. ownership of a8f5a.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXd4../04413.. ownership of a8317.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMRoR../58b5a.. ownership of 32724.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMc8k../71eab.. ownership of 4c842.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMVHz../be311.. ownership of 9f78a.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLu5../2ecae.. ownership of 4b341.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMbts../6f633.. ownership of 03b9f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMM44../03679.. ownership of e72ad.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMEsH../30ce0.. ownership of df92f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFAt../80a5e.. ownership of eddd3.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMKyP../87eb0.. ownership of 7ed8e.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMckn../1bc0a.. ownership of ec68b.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMJSv../aa641.. ownership of 34c02.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXHZ../d5e4f.. ownership of be96a.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMK6c../1e20f.. ownership of 965bc.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMWXa../f65b7.. ownership of d496b.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMY5n../14a02.. ownership of 22a0a.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMHhd../29086.. ownership of f25e4.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZ4r../450ed.. ownership of 2cbb9.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMSmC../259db.. ownership of 33c2f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMb5w../c738f.. ownership of 1e2d5.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFSB../9be3a.. ownership of 5cabb.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMG6u../ffd0a.. ownership of 2d416.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMbWh../2ef04.. ownership of 0a266.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFx1../dac45.. ownership of ebdb5.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMPo1../910b3.. ownership of 4d67c.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZAi../0a72a.. ownership of 8f3ce.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGfU../e0e94.. ownership of 85201.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMU4C../aed45.. ownership of 313d9.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMYMG../3bfcf.. ownership of 5d5d5.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMUA9../4d971.. ownership of 0a1db.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMPuu../3dea5.. ownership of 7b90a.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMdVb../749dd.. ownership of 0a858.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMSu6../2e7cf.. ownership of 63bae.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMc22../5c650.. ownership of 3a751.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMapU../cbfd6.. ownership of 5810f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMYt6../32a8d.. ownership of eb945.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMKdW../4aa45.. ownership of 83e0b.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMcdz../c502d.. ownership of 786cb.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMVoM../5d431.. ownership of 6810b.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMJfL../89241.. ownership of f57d8.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMMWu../326e8.. ownership of cd48c.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMNVF../ecc37.. ownership of e5506.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMT9K../912ad.. ownership of 4147b.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMH3G../88ccd.. ownership of f75cd.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMbAb../233e2.. ownership of cad7c.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLxn../e682b.. ownership of 6e655.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLX5../141d7.. ownership of e9749.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TML9u../8049b.. ownership of 94398.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXFj../42e24.. ownership of 31c29.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMUrd../191cf.. ownership of 77740.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLzA../170ef.. ownership of e668f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZ7o../e1040.. ownership of 556f0.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXsB../4bd3f.. ownership of 135df.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMdqj../d77c9.. ownership of 2fd3e.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMavi../e422c.. ownership of b1976.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMSwD../52027.. ownership of 865a3.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMMk6../6d646.. ownership of 09a09.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMWMp../39b5e.. ownership of e5542.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGhp../ddf0c.. ownership of 1d088.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMYNJ../8bb3a.. ownership of 9c9a3.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZu4../ec976.. ownership of 05558.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMW8j../349bc.. ownership of 74867.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMby1../ca0cd.. ownership of 9630f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMSPd../182a9.. ownership of 80ccc.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMQ9V../5fda1.. ownership of 35a1e.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMQ7r../a6e8c.. ownership of 29768.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMQX4../fa8ee.. ownership of afa8a.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLxf../78a7c.. ownership of 1a64d.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMUnv../55cb3.. ownership of 1b322.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
PUfQZ../d7271.. doc published by Pr6Pc..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Definition nSubqnSubq := λ x0 x1 . not (x0x1)
Param ordsuccordsucc : ιι
Known neq_0_ordsuccneq_0_ordsucc : ∀ x0 . 0 = ordsucc x0∀ x1 : ο . x1
Theorem neq_0_1neq_0_1 : 0 = 1∀ x0 : ο . x0 (proof)
Theorem neq_0_2neq_0_2 : 0 = 2∀ x0 : ο . x0 (proof)
Known ordsucc_inj_contraordsucc_inj_contra : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)ordsucc x0 = ordsucc x1∀ x2 : ο . x2
Theorem neq_1_2neq_1_2 : 1 = 2∀ x0 : ο . x0 (proof)
Definition nInnIn := λ x0 x1 . not (x0x1)
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Theorem nIn_0_0nIn_0_0 : nIn 0 0 (proof)
Theorem nIn_1_0nIn_1_0 : nIn 1 0 (proof)
Theorem nIn_2_0nIn_2_0 : nIn 2 0 (proof)
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Theorem nIn_1_1nIn_1_1 : nIn 1 1 (proof)
Theorem nIn_2_2nIn_2_2 : nIn 2 2 (proof)
Known Subq_EmptySubq_Empty : ∀ x0 . 0x0
Theorem Subq_0_0Subq_0_0 : 00 (proof)
Theorem Subq_0_1Subq_0_1 : 01 (proof)
Theorem Subq_0_2Subq_0_2 : 02 (proof)
Known In_0_1In_0_1 : 01
Theorem nSubq_1_0nSubq_1_0 : nSubq 1 0 (proof)
Known Subq_refSubq_ref : ∀ x0 . x0x0
Theorem Subq_1_1Subq_1_1 : 11 (proof)
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Theorem Subq_1_2Subq_1_2 : 12 (proof)
Known In_0_2In_0_2 : 02
Theorem nSubq_2_0nSubq_2_0 : nSubq 2 0 (proof)
Known In_1_2In_1_2 : 12
Theorem nSubq_2_1nSubq_2_1 : nSubq 2 1 (proof)
Theorem Subq_2_2Subq_2_2 : 22 (proof)
Param nat_pnat_p : ιο
Known nat_complete_indnat_complete_ind : ∀ x0 : ι → ο . (∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . nat_p x1x0 x1
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known UnionE_impredUnionE_impred : ∀ x0 x1 . x1prim3 x0∀ x2 : ο . (∀ x3 . x1x3x3x0x2)x2
Known nat_ordsucc_transnat_ordsucc_trans : ∀ x0 . nat_p x0∀ x1 . x1ordsucc x0x1x0
Known UnionIUnionI : ∀ x0 x1 x2 . x1x2x2x0x1prim3 x0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Known Union_ordsucc_eqUnion_ordsucc_eq : ∀ x0 . nat_p x0prim3 (ordsucc x0) = x0
Theorem In_0_3In_0_3 : 03 (proof)
Theorem In_1_3In_1_3 : 13 (proof)
Theorem In_2_3In_2_3 : 23 (proof)
Theorem In_0_4In_0_4 : 04 (proof)
Theorem In_1_4In_1_4 : 14 (proof)
Theorem In_2_4In_2_4 : 24 (proof)
Theorem In_3_4In_3_4 : 34 (proof)
Theorem In_0_5In_0_5 : 05 (proof)
Theorem In_1_5In_1_5 : 15 (proof)
Theorem In_2_5In_2_5 : 25 (proof)
Theorem In_3_5In_3_5 : 35 (proof)
Theorem In_4_5In_4_5 : 45 (proof)
Theorem In_0_6In_0_6 : 06 (proof)
Theorem In_1_6In_1_6 : 16 (proof)
Theorem In_2_6In_2_6 : 26 (proof)
Theorem In_3_6In_3_6 : 36 (proof)
Theorem In_4_6In_4_6 : 46 (proof)
Theorem In_5_6In_5_6 : 56 (proof)
Theorem In_0_7In_0_7 : 07 (proof)
Theorem In_1_7In_1_7 : 17 (proof)
Theorem In_2_7In_2_7 : 27 (proof)
Theorem In_3_7In_3_7 : 37 (proof)
Theorem In_4_7In_4_7 : 47 (proof)
Theorem In_5_7In_5_7 : 57 (proof)
Theorem In_6_7In_6_7 : 67 (proof)
Theorem In_0_8In_0_8 : 08 (proof)
Theorem In_1_8In_1_8 : 18 (proof)
Theorem In_2_8In_2_8 : 28 (proof)
Theorem In_3_8In_3_8 : 38 (proof)
Theorem In_4_8In_4_8 : 48 (proof)
Theorem In_5_8In_5_8 : 58 (proof)
Theorem In_6_8In_6_8 : 68 (proof)
Theorem In_7_8In_7_8 : 78 (proof)
Theorem In_0_9In_0_9 : 09 (proof)
Theorem In_1_9In_1_9 : 19 (proof)
Theorem In_2_9In_2_9 : 29 (proof)
Theorem In_3_9In_3_9 : 39 (proof)
Theorem In_4_9In_4_9 : 49 (proof)
Theorem In_5_9In_5_9 : 59 (proof)
Theorem In_6_9In_6_9 : 69 (proof)
Theorem In_7_9In_7_9 : 79 (proof)
Theorem In_8_9In_8_9 : 89 (proof)
Param In_rec_iIn_rec_i : (ι(ιι) → ι) → ιι
Param If_iIf_i : οιιι
Definition nat_primrecnat_primrec := λ x0 . λ x1 : ι → ι → ι . In_rec_i (λ x2 . λ x3 : ι → ι . If_i (prim3 x2x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known If_i_0If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2
Theorem nat_primrec_rnat_primrec_r : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . ∀ x3 x4 : ι → ι . (∀ x5 . x5x2x3 x5 = x4 x5)If_i (prim3 x2x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0 = If_i (prim3 x2x2) (x1 (prim3 x2) (x4 (prim3 x2))) x0 (proof)
Known In_rec_i_eqIn_rec_i_eq : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_i x0 x1 = x0 x1 (In_rec_i x0)
Theorem nat_primrec_0nat_primrec_0 : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0 (proof)
Known If_i_1If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1
Theorem nat_primrec_Snat_primrec_S : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2) (proof)
Definition add_natadd_nat := λ x0 . nat_primrec x0 (λ x1 . ordsucc)
Theorem add_nat_0Radd_nat_0R : ∀ x0 . add_nat x0 0 = x0 (proof)
Theorem add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1) (proof)
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Theorem add_nat_padd_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (add_nat x0 x1) (proof)
Theorem add_nat_assoadd_nat_asso : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2add_nat (add_nat x0 x1) x2 = add_nat x0 (add_nat x1 x2) (proof)
Theorem add_nat_0Ladd_nat_0L : ∀ x0 . nat_p x0add_nat 0 x0 = x0 (proof)
Theorem add_nat_SLadd_nat_SL : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1) (proof)
Theorem add_nat_comadd_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat x0 x1 = add_nat x1 x0 (proof)
Definition mul_natmul_nat := λ x0 . nat_primrec 0 (λ x1 . add_nat x0)
Theorem mul_nat_0Rmul_nat_0R : ∀ x0 . mul_nat x0 0 = 0 (proof)
Theorem mul_nat_SRmul_nat_SR : ∀ x0 x1 . nat_p x1mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1) (proof)
Known nat_0nat_0 : nat_p 0
Theorem mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1) (proof)
Theorem mul_nat_0Lmul_nat_0L : ∀ x0 . nat_p x0mul_nat 0 x0 = 0 (proof)
Theorem mul_nat_SLmul_nat_SL : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat (ordsucc x0) x1 = add_nat (mul_nat x0 x1) x1 (proof)
Theorem mul_nat_commul_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat x0 x1 = mul_nat x1 x0 (proof)
Theorem mul_add_nat_distrLmul_add_nat_distrL : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2mul_nat x0 (add_nat x1 x2) = add_nat (mul_nat x0 x1) (mul_nat x0 x2) (proof)
Theorem mul_add_nat_distrRmul_add_nat_distrR : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2mul_nat (add_nat x0 x1) x2 = add_nat (mul_nat x0 x2) (mul_nat x1 x2) (proof)
Theorem mul_nat_assomul_nat_asso : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2mul_nat (mul_nat x0 x1) x2 = mul_nat x0 (mul_nat x1 x2) (proof)
Theorem add_nat_1_1_2add_nat_1_1_2 : add_nat 1 1 = 2 (proof)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known FalseEFalseE : False∀ x0 : ο . x0
Known nat_ordsucc_in_ordsuccnat_ordsucc_in_ordsucc : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known ordsucc_injordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1x0 = x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem PigeonHole_natPigeonHole_nat : ∀ x0 . nat_p x0∀ x1 : ι → ι . (∀ x2 . x2ordsucc x0x1 x2x0)not (∀ x2 . x2ordsucc x0∀ x3 . x3ordsucc x0x1 x2 = x1 x3x2 = x3) (proof)
Definition bijbij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Theorem PigeonHole_nat_bijPigeonHole_nat_bij : ∀ x0 . nat_p x0∀ x1 : ι → ι . (∀ x2 . x2x0x1 x2x0)(∀ x2 . x2x0∀ x3 . x3x0x1 x2 = x1 x3x2 = x3)bij x0 x0 x1 (proof)