Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrEvg../b4683..
PUKK9../0ed75..
vout
PrEvg../f4a78.. 0.30 bars
TMdZk../67db6.. negprop ownership controlledby PrGxv.. upto 0
TMdQv../1a78c.. negprop ownership controlledby PrGxv.. upto 0
TMbEw../cba5b.. negprop ownership controlledby PrGxv.. upto 0
TMEkd../98432.. ownership of aa4b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcL8../aba9a.. ownership of 350f8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQTD../05e53.. ownership of 893d8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRTe../c9353.. ownership of 7a5bc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRXX../fb798.. ownership of 1c51c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXZK../ac8a9.. ownership of ac9d3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbkt../ae873.. ownership of 7ecf1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY8P../3da7e.. ownership of fac77.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLS6../8445b.. ownership of 13c0f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRSd../84d21.. ownership of 58080.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPTY../6195c.. ownership of a5b99.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLdH../98f2c.. ownership of f3c9c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbME../12310.. ownership of 022d0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRoJ../6bd07.. ownership of d018b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaS7../d0dc7.. ownership of 7639b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcAU../d6ae5.. ownership of a1f78.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXBL../45078.. ownership of 7ae5f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNJ2../d1d3d.. ownership of 82fcf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGH1../b0c0a.. ownership of 97eb5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaUG../69dd7.. ownership of a6b90.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK4z../4fe42.. ownership of 5ddb9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVnY../61b5e.. ownership of df1b2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSsZ../87538.. ownership of 8940b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGH9../14860.. ownership of 63d5e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMasM../49c82.. ownership of 1ce6b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS73../745a1.. ownership of aa168.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGd3../6a15c.. ownership of 5cf31.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNiM../6ce2f.. ownership of e235f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdAp../88a86.. ownership of 140e5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSpr../9aa15.. ownership of 8c15e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLNo../e81c3.. ownership of 1319f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYSM../72ca7.. ownership of b792c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLJC../ed4a5.. ownership of 4183e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML5s../c296c.. ownership of 6ea59.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcmV../2096c.. ownership of 1c625.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX6Q../6a207.. ownership of 52ad2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK44../b72e3.. ownership of f30c5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWfa../b15e3.. ownership of 0d2e8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQh6../1ffac.. ownership of 239af.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXaZ../da784.. ownership of 46bb5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYRi../81cad.. ownership of 1f489.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZZg../3a0a0.. ownership of 1ee1e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcTv../72dd6.. ownership of e2782.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMV6d../e4ea2.. ownership of c955c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFpC../74613.. ownership of a1e1a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHNE../b2798.. ownership of 67f99.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVPU../bdca1.. ownership of 65954.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdmj../72af5.. ownership of f3681.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR5V../9a061.. ownership of 0d93c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLcA../19869.. ownership of bb62c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK5j../13206.. ownership of 9bb00.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNQi../9ed9a.. ownership of e29d7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRe6../64cc2.. ownership of 1ebb9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMU5../4ccf4.. ownership of 0e098.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbY1../53e76.. ownership of c8b62.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVf8../a1bac.. ownership of 7db9a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRxJ../fd35d.. ownership of 384d5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYKu../87652.. ownership of f6c18.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXm4../bb408.. ownership of 4e80f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMph../115ed.. ownership of a0a12.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN54../6059e.. ownership of 1cd68.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXNH../23aba.. ownership of e664f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLvs../f511f.. ownership of cbdee.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMawj../570d2.. ownership of 2aab7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd5T../61c1d.. ownership of 4b5d5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFL2../319b3.. ownership of 17ec0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG6v../46f8f.. ownership of 69e64.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXdd../bdc53.. ownership of 7a5ad.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM1s../7be5f.. ownership of d4e8e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKCV../b9413.. ownership of 4eb37.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKMj../2ae9a.. ownership of caeb5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWyp../c370c.. ownership of ccd18.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPDf../d6ad7.. ownership of 49aa4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNaj../6c526.. ownership of b4b12.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPi7../cbab4.. ownership of 71150.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLDJ../9bdca.. ownership of 0d106.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbb2../3cb7d.. ownership of 06ef3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXyB../f1286.. ownership of 2c6c2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdid../0ac96.. ownership of 57cc6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSW6../fbc91.. ownership of 58be5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMas9../2601a.. ownership of 1ceed.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXxS../921c3.. ownership of e8aa0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP2R../68490.. ownership of ea5d5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSQ7../36fc5.. ownership of bb4a2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd2D../dc439.. ownership of 57aad.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMZp../2e5e0.. ownership of f03b0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN1A../df665.. ownership of 28cca.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHV1../2d12b.. ownership of bcc68.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPp5../3c34e.. ownership of 102c8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXxV../75072.. ownership of a80b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdFN../2f0f1.. ownership of b9890.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLJh../77877.. ownership of 8690c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJom../4e683.. ownership of 98e34.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMrP../52e8c.. ownership of c2c69.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP6t../80e5e.. ownership of 15e7b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWU7../54b29.. ownership of 43f69.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUQt../4357a.. ownership of d88ba.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJPH../474d7.. ownership of 8e99f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSjJ../f5144.. ownership of 7f899.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNA3../2352e.. ownership of 4c533.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPp6../f3b53.. ownership of 71fcb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYpS../f7d61.. ownership of fe741.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbyj../ee50c.. ownership of 652a2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNjZ../7190e.. ownership of 5aff0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXKj../0a7cb.. ownership of 3b34e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJas../e3046.. ownership of a6f4d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSzu../47948.. ownership of 9044c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMco3../cc474.. ownership of 5f6bc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcm3../5aacb.. ownership of a7963.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTKY../f235c.. ownership of 78965.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXvh../77e8f.. ownership of ff451.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU7y../1d917.. ownership of a91ad.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNJi../89ce7.. ownership of 03651.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJe4../c3ac3.. ownership of 65971.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ3f../e3b56.. ownership of 778cc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFSa../372cc.. ownership of 24c97.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdMV../3f859.. ownership of 68d02.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRaB../f2bc1.. ownership of 1ee0c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHje../463c9.. ownership of 42824.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHFP../787aa.. ownership of 9ec65.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRz5../30874.. ownership of 77d87.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVZE../ede74.. ownership of a783e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLFy../d7598.. ownership of 2eaee.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHEu../eccb4.. ownership of 93bfa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNYi../5065e.. ownership of c60fe.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS41../d585d.. ownership of 1a950.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWfG../3fbe0.. ownership of 72f77.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJqZ../65794.. ownership of 90817.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN1v../95ec9.. ownership of 05ab8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHv3../74c26.. ownership of dbe42.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUQY../92261.. ownership of 8de7c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWM5../6ed48.. ownership of 10b06.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbiX../52b01.. ownership of 09622.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRyG../7f31a.. ownership of f3ff9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLVf../5facb.. ownership of 378c0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ1R../44f28.. ownership of 84b90.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKtZ../8ea1d.. ownership of cfb62.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHt1../471b1.. ownership of 75136.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWTX../6ff1b.. ownership of 25bc5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPC1../2db3f.. ownership of a7e8b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXiF../fb5b1.. ownership of 7a6f2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSaq../ae81a.. ownership of 1662d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMG3../b63f6.. ownership of f6c3d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKin../1515a.. ownership of 3390a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdhe../e07f4.. ownership of a90a3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJrY../6802f.. ownership of 0e82a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJvr../38a4c.. ownership of 67d30.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMom../45737.. ownership of 487b0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN6S../0b86c.. ownership of ef947.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYYn../85df5.. ownership of 65e83.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNJP../6fe5a.. ownership of 015b8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYLM../b9f05.. ownership of 55c75.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdRh../01820.. ownership of af2d6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcCi../07fb1.. ownership of a3bd7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP8h../d5898.. ownership of 2abd8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUVn../6da62.. ownership of 0641d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbfH../9c37c.. ownership of 1f5f7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJya../0ca5e.. ownership of fffc4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGJb../b2ca4.. ownership of 9ac87.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVy4../f72a9.. ownership of a40b1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF8S../adb7d.. ownership of 3bafe.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMcF../d33d7.. ownership of cda77.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWcg../5c22e.. ownership of c8c18.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFM3../51408.. ownership of 71b93.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUTH../e8e07.. ownership of 14149.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMQz../b1a07.. ownership of c723c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa8g../33472.. ownership of 616bf.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPSC../c0fd1.. ownership of d7158.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKwo../67234.. ownership of 94fee.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMru../11202.. ownership of 3be1c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTzF../90472.. ownership of 0e41b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZtJ../4f46c.. ownership of ea71e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUKrN../d9e20.. doc published by PrGxv..
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition nSubq := λ x0 x1 . not (Subq x0 x1)
Param 4a7ef.. : ι
Param 4ae4a.. : ι → ι
Known efbae.. : ∀ x0 . 4a7ef.. = 4ae4a.. x0 ⟶ ∀ x1 : ο . x1
Theorem c8c18.. : 4a7ef.. = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3bafe.. : 4a7ef.. = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Known 4b095.. : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ 4ae4a.. x0 = 4ae4a.. x1 ⟶ ∀ x2 : ο . x2
Theorem 9ac87.. : 4ae4a.. 4a7ef.. = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem 1f5f7.. : nIn 4a7ef.. 4a7ef.. (proof)
Theorem 2abd8.. : nIn (4ae4a.. 4a7ef..) 4a7ef.. (proof)
Theorem af2d6.. : nIn (4ae4a.. (4ae4a.. 4a7ef..)) 4a7ef.. (proof)
Known In_irref : ∀ x0 . nIn x0 x0
Theorem 015b8.. : nIn (4ae4a.. 4a7ef..) (4ae4a.. 4a7ef..) (proof)
Theorem ef947.. : nIn (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Known e8942.. : ∀ x0 . Subq 4a7ef.. x0
Theorem 67d30.. : Subq 4a7ef.. 4a7ef.. (proof)
Theorem a90a3.. : Subq 4a7ef.. (4ae4a.. 4a7ef..) (proof)
Theorem f6c3d.. : Subq 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Theorem 7a6f2.. : nSubq (4ae4a.. 4a7ef..) 4a7ef.. (proof)
Known Subq_ref : ∀ x0 . Subq x0 x0
Theorem 25bc5.. : Subq (4ae4a.. 4a7ef..) (4ae4a.. 4a7ef..) (proof)
Known c79db.. : ∀ x0 . Subq x0 (4ae4a.. x0)
Theorem cfb62.. : Subq (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 378c0.. : nSubq (4ae4a.. (4ae4a.. 4a7ef..)) 4a7ef.. (proof)
Known 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 09622.. : nSubq (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. 4a7ef..) (proof)
Theorem 8de7c.. : Subq (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Param ba9d8.. : ι → ο
Known 839f4.. : ∀ x0 : ι → ο . (∀ x1 . ba9d8.. x1 ⟶ (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ba9d8.. x1 ⟶ x0 x1
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known UnionE_impred : ∀ x0 x1 . prim1 x1 (prim3 x0) ⟶ ∀ x2 : ο . (∀ x3 . prim1 x1 x3 ⟶ prim1 x3 x0 ⟶ x2) ⟶ x2
Known 82e3b.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 (4ae4a.. x0) ⟶ Subq x1 x0
Known UnionI : ∀ x0 x1 x2 . prim1 x1 x2 ⟶ prim1 x2 x0 ⟶ prim1 x1 (prim3 x0)
Known 5faa3.. : ∀ x0 . prim1 x0 (4ae4a.. x0)
Theorem 05ab8.. : ∀ x0 . ba9d8.. x0 ⟶ prim3 (4ae4a.. x0) = x0 (proof)
Theorem 72f77.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem c60fe.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 2eaee.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 77d87.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 42824.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 68d02.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 778cc.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 03651.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem ff451.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem a7963.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem 9044c.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem 3b34e.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem 652a2.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem 71fcb.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem 7f899.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem d88ba.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem 15e7b.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem 98e34.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem b9890.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 102c8.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 28cca.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 57aad.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem ea5d5.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 1ceed.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 57cc6.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 06ef3.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem 71150.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem 49aa4.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem caeb5.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem d4e8e.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem 69e64.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem 4b5d5.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem cbdee.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem 1cd68.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 4e80f.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 384d5.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem c8b62.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 1ebb9.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 9bb00.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 0d93c.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 65954.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem a1e1a.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Param In_rec_i : (ι → (ι → ι) → ι) → ι → ι
Param If_i : ο → ι → ι → ι
Definition nat_primrec := λ x0 . λ x1 : ι → ι → ι . In_rec_i (λ x2 . λ x3 : ι → ι . If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm : ∀ x0 : ο . or x0 (not x0)
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Theorem nat_primrec_r : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . ∀ x3 x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ x3 x5 = x4 x5) ⟶ If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0 = If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x4 (prim3 x2))) x0 (proof)
Known 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)
Theorem 1f489.. : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 4a7ef.. = x0 (proof)
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem 239af.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . ba9d8.. x2 ⟶ nat_primrec x0 x1 (4ae4a.. x2) = x1 x2 (nat_primrec x0 x1 x2) (proof)
Definition 616bf.. := λ x0 . nat_primrec x0 (λ x1 . 4ae4a..)
Theorem f30c5.. : ∀ x0 . 616bf.. x0 4a7ef.. = x0 (proof)
Theorem 1c625.. : ∀ x0 x1 . ba9d8.. x1 ⟶ 616bf.. x0 (4ae4a.. x1) = 4ae4a.. (616bf.. x0 x1) (proof)
Known 5c211.. : ∀ x0 : ι → ο . x0 4a7ef.. ⟶ (∀ x1 . ba9d8.. x1 ⟶ x0 x1 ⟶ x0 (4ae4a.. x1)) ⟶ ∀ x1 . ba9d8.. x1 ⟶ x0 x1
Known 2fbbc.. : ∀ x0 . ba9d8.. x0 ⟶ ba9d8.. (4ae4a.. x0)
Theorem 4183e.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ba9d8.. (616bf.. x0 x1) (proof)
Theorem 1319f.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ∀ x2 . ba9d8.. x2 ⟶ 616bf.. (616bf.. x0 x1) x2 = 616bf.. x0 (616bf.. x1 x2) (proof)
Theorem 140e5.. : ∀ x0 . ba9d8.. x0 ⟶ 616bf.. 4a7ef.. x0 = x0 (proof)
Theorem 5cf31.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ 616bf.. (4ae4a.. x0) x1 = 4ae4a.. (616bf.. x0 x1) (proof)
Theorem 1ce6b.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ 616bf.. x0 x1 = 616bf.. x1 x0 (proof)
Definition 14149.. := λ x0 . nat_primrec 4a7ef.. (λ x1 . 616bf.. x0)
Theorem 8940b.. : ∀ x0 . 14149.. x0 4a7ef.. = 4a7ef.. (proof)
Theorem 5ddb9.. : ∀ x0 x1 . ba9d8.. x1 ⟶ 14149.. x0 (4ae4a.. x1) = 616bf.. x0 (14149.. x0 x1) (proof)
Known 4c9b8.. : ba9d8.. 4a7ef..
Theorem 97eb5.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ba9d8.. (14149.. x0 x1) (proof)
Theorem 7ae5f.. : ∀ x0 . ba9d8.. x0 ⟶ 14149.. 4a7ef.. x0 = 4a7ef.. (proof)
Theorem 7639b.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ 14149.. (4ae4a.. x0) x1 = 616bf.. (14149.. x0 x1) x1 (proof)
Theorem 022d0.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ 14149.. x0 x1 = 14149.. x1 x0 (proof)
Theorem a5b99.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ∀ x2 . ba9d8.. x2 ⟶ 14149.. x0 (616bf.. x1 x2) = 616bf.. (14149.. x0 x1) (14149.. x0 x2) (proof)
Theorem 13c0f.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ∀ x2 . ba9d8.. x2 ⟶ 14149.. (616bf.. x0 x1) x2 = 616bf.. (14149.. x0 x2) (14149.. x1 x2) (proof)
Theorem 7ecf1.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ∀ x2 . ba9d8.. x2 ⟶ 14149.. (14149.. x0 x1) x2 = 14149.. x0 (14149.. x1 x2) (proof)
Theorem 1c51c.. : 616bf.. (4ae4a.. 4a7ef..) (4ae4a.. 4a7ef..) = 4ae4a.. (4ae4a.. 4a7ef..) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0)
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known 3238a.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) (4ae4a.. x0)
Known 054cd.. : ∀ x0 x1 . 4ae4a.. x0 = 4ae4a.. x1 ⟶ x0 = x1
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 893d8.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . prim1 x2 (4ae4a.. x0) ⟶ prim1 (x1 x2) x0) ⟶ not (∀ x2 . prim1 x2 (4ae4a.. x0) ⟶ ∀ x3 . prim1 x3 (4ae4a.. x0) ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) (proof)
Definition bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem aa4b6.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ bij x0 x0 x1 (proof)