Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrJGW../d9dea..
PUdKP../8b566..
vout
PrJGW../39051.. 1.95 bars
TMM1C../1bae4.. negprop ownership controlledby PrGxv.. upto 0
TMX3A../f0d98.. negprop ownership controlledby PrGxv.. upto 0
TMW7M../4da8a.. negprop ownership controlledby PrGxv.. upto 0
TMMTh../c4781.. negprop ownership controlledby PrGxv.. upto 0
TMJnF../057d6.. negprop ownership controlledby PrGxv.. upto 0
TMJtn../a82d8.. negprop ownership controlledby PrGxv.. upto 0
TMEnc../fddf1.. negprop ownership controlledby PrGxv.. upto 0
TMdam../ca665.. negprop ownership controlledby PrGxv.. upto 0
TMHhG../c66ed.. negprop ownership controlledby PrGxv.. upto 0
TMSPv../80622.. negprop ownership controlledby PrGxv.. upto 0
TMZr9../2266a.. negprop ownership controlledby PrGxv.. upto 0
TMXVP../74768.. negprop ownership controlledby PrGxv.. upto 0
TMUcX../810d9.. negprop ownership controlledby PrGxv.. upto 0
TMa9h../b4e92.. negprop ownership controlledby PrGxv.. upto 0
TMF7a../a02dc.. negprop ownership controlledby PrGxv.. upto 0
TMcBz../16715.. negprop ownership controlledby PrGxv.. upto 0
TMagR../0d09c.. negprop ownership controlledby PrGxv.. upto 0
TMQCH../c642a.. negprop ownership controlledby PrGxv.. upto 0
TMN8k../0efc7.. negprop ownership controlledby PrGxv.. upto 0
TMXu7../e1f1b.. negprop ownership controlledby PrGxv.. upto 0
TMSdm../a0bb2.. negprop ownership controlledby PrGxv.. upto 0
TMVNt../4a9eb.. negprop ownership controlledby PrGxv.. upto 0
TMYL3../1fa67.. negprop ownership controlledby PrGxv.. upto 0
TMa8V../a7ed5.. negprop ownership controlledby PrGxv.. upto 0
TMJX3../3a29a.. negprop ownership controlledby PrGxv.. upto 0
TMFZX../4a539.. negprop ownership controlledby PrGxv.. upto 0
TMUH6../09666.. negprop ownership controlledby PrGxv.. upto 0
TMR24../1fe60.. negprop ownership controlledby PrGxv.. upto 0
TMPbR../cb1ab.. negprop ownership controlledby PrGxv.. upto 0
TMSm2../d9b2d.. negprop ownership controlledby PrGxv.. upto 0
TMMD9../463f9.. negprop ownership controlledby PrGxv.. upto 0
TMPDr../c5764.. negprop ownership controlledby PrGxv.. upto 0
TMWdT../cc99e.. negprop ownership controlledby PrGxv.. upto 0
TMFjx../62f77.. negprop ownership controlledby PrGxv.. upto 0
TMN2Y../40874.. negprop ownership controlledby PrGxv.. upto 0
TMaAF../17f98.. negprop ownership controlledby PrGxv.. upto 0
TMUPJ../c63fe.. negprop ownership controlledby PrGxv.. upto 0
TMM91../cda44.. negprop ownership controlledby PrGxv.. upto 0
TMQQF../c559d.. negprop ownership controlledby PrGxv.. upto 0
TMVsH../002b3.. negprop ownership controlledby PrGxv.. upto 0
TMYrk../6a3ef.. negprop ownership controlledby PrGxv.. upto 0
TMNXX../31663.. negprop ownership controlledby PrGxv.. upto 0
TMMbq../a7b87.. negprop ownership controlledby PrGxv.. upto 0
TMGkS../98346.. negprop ownership controlledby PrGxv.. upto 0
TMYsX../d079e.. negprop ownership controlledby PrGxv.. upto 0
TMWaM../d153a.. ownership of 4dd03.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYXh../c39a5.. ownership of 5d657.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS1L../47209.. ownership of b1f45.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX8Q../05c54.. ownership of 46d29.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ1J../e4310.. ownership of 7a9d0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ2C../c41c9.. ownership of 5cd7e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ27../88ee1.. ownership of db57a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMbC../a69c9.. ownership of f55a9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVHw../86c15.. ownership of bf8a0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRWw../b494f.. ownership of 6f68c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVAV../4c752.. ownership of 9be47.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFma../fa506.. ownership of 4fde4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPtG../6d472.. ownership of 754ab.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMEg../6cd21.. ownership of 3aac5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbEs../1288f.. ownership of aa4ec.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXxj../5785e.. ownership of 21217.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM5P../36f88.. ownership of 3babd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYSA../84bd8.. ownership of 8fbda.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdBu../b010d.. ownership of c4f4e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRx5../8f38b.. ownership of 1a5a5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJyL../cf5dc.. ownership of cc164.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPxv../5034a.. ownership of 03714.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFTJ../4f023.. ownership of 17be6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPLp../fe24b.. ownership of bf371.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXNU../e599a.. ownership of 622d4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSHT../6353b.. ownership of f36f9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcTh../ac920.. ownership of f5d01.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX1J../d9778.. ownership of 4f0c1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXp1../97c02.. ownership of 8fcc8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHjc../3bb74.. ownership of bce82.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTX6../63d2a.. ownership of 19797.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKMb../cd124.. ownership of bdd10.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTP2../5acb1.. ownership of 58716.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKzk../8cb71.. ownership of 3a325.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSZo../23d33.. ownership of 516c5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJsZ../16ae7.. ownership of cc080.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHaP../38e77.. ownership of ac13b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTSR../ee0c8.. ownership of fb62d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJwc../c16e4.. ownership of ee53e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRk2../dfbb3.. ownership of c196d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdbn../52c7e.. ownership of 16901.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVxK../9c0a3.. ownership of 175ee.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZGe../a42ce.. ownership of 58158.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHrU../18519.. ownership of 11b2d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX26../fa4ec.. ownership of c6805.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJQV../0aea1.. ownership of 30d77.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKaV../53d91.. ownership of ecc01.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcsH../e6833.. ownership of 67205.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc4c../4f077.. ownership of 2d896.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLcg../86c59.. ownership of 69a96.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMjY../9c1be.. ownership of d13e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGBn../34d32.. ownership of bd2b0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS8h../27d89.. ownership of 7357c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR4S../126c6.. ownership of fac87.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY2G../aaef1.. ownership of 5ccd2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWs5../e97e7.. ownership of d3c65.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQvc../7c1b0.. ownership of 31e4d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVvL../3c653.. ownership of 39a2f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSam../b4d02.. ownership of cdcd4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMtj../489e7.. ownership of 8901a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWq6../6dc9b.. ownership of e25a7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWkh../15560.. ownership of 1a1d3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPtv../3fa69.. ownership of 67cbd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH3d../c8a28.. ownership of c426a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcPu../1d6f0.. ownership of 7fa57.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMab6../c2777.. ownership of 9cfee.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYok../9c578.. ownership of a82a2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPno../840a8.. ownership of 277d6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK64../d158d.. ownership of 3dae7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ8V../a0ae3.. ownership of a2880.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMduc../5895f.. ownership of 2f510.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLEC../a4b91.. ownership of 37ab4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZek../03a33.. ownership of 05e02.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJhd../09600.. ownership of c8965.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMxT../eba26.. ownership of d1b49.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbJR../4be71.. ownership of ac927.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJEv../d2c39.. ownership of 37f0a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZmR../29d78.. ownership of ad3d8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRrG../7937b.. ownership of 0c325.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZxp../ba251.. ownership of 73033.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTP1../23c20.. ownership of daead.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLjs../e46b3.. ownership of 660d5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZKq../c52a1.. ownership of 57b7e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNNa../5cbc6.. ownership of 39c68.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUNj../18905.. ownership of 6afc6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMwp../8e1f4.. ownership of b2b67.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGG3../6f0e0.. ownership of f9d2f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHDQ../12b5e.. ownership of e0e60.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWaf../04424.. ownership of 3a2b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJse../bebae.. ownership of 38b5b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMDq../799a3.. ownership of 5c667.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRUZ../a1ce4.. ownership of 24ff2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSRA../b4b4f.. ownership of 0d7aa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUZ9../d0f8f.. ownership of 64b89.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS9x../695df.. ownership of 0a0af.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVoD../513ce.. ownership of d23f8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWde../0cd60.. ownership of e6eb7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUL2../024de.. ownership of 188fa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQGx../1e8ca.. ownership of f5104.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLqG../c8acb.. ownership of 765cd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKDL../3aa13.. ownership of 3cd21.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTrE../ca69b.. ownership of 6bcd8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFR4../69280.. ownership of aeaf9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP98../ef425.. ownership of 25845.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVjk../211b4.. ownership of b1d09.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG7U../5caed.. ownership of f0242.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGkr../addde.. ownership of 9f6cd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNQ5../6b20a.. ownership of 285d1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFBY../8b552.. ownership of 2911f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWmc../e0511.. ownership of 459e8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUJkX../a0044.. doc published by PrGxv..
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem 2911f.. : ∀ x0 . prim1 x0 (4ae4a.. 4a7ef..) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 x0 (proof)
Theorem 9f6cd.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 x0 (proof)
Theorem b1d09.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 x0 (proof)
Theorem aeaf9.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 x0 (proof)
Theorem 3cd21.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ x1 x0 (proof)
Theorem f5104.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ x1 x0 (proof)
Theorem e6eb7.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ x1 x0 (proof)
Theorem 0a0af.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) ⟶ x1 x0 (proof)
Theorem 0d7aa.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) ⟶ x1 x0 (proof)
Known 1b1d1.. : ∀ x0 . 4ae4a.. x0 = 4a7ef.. ⟶ ∀ x1 : ο . x1
Theorem 5c667.. : 4ae4a.. 4a7ef.. = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3a2b6.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Known 4b095.. : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ 4ae4a.. x0 = 4ae4a.. x1 ⟶ ∀ x2 : ο . x2
Theorem f9d2f.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6afc6.. : nIn (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. 4a7ef..) (proof)
Theorem 57b7e.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem daead.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 0c325.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 37f0a.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem d1b49.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 05e02.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 2f510.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3dae7.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem a82a2.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7fa57.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 67cbd.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem e25a7.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem cdcd4.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 31e4d.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 5ccd2.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7357c.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem d13e3.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 2d896.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem ecc01.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem c6805.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 58158.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 16901.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem ee53e.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem ac13b.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 516c5.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 58716.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 19797.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 8fcc8.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem f5d01.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 622d4.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 17be6.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem cc164.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem c4f4e.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3babd.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem aa4ec.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 754ab.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 9be47.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem bf8a0.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem db57a.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7a9d0.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem b1f45.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4dd03.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) ⟶ ∀ x0 : ο . x0 (proof)