Proofgold Signed Transaction

vin
PrFfj../41a84.. PURxa../66ab7..

vout

PrFfj../015e9.. 25.00 bars
TMUua../b153e.. negprop ownership controlledby Pr4Ru.. upto 0
TMRpB../74677.. negprop ownership controlledby Pr4Ru.. upto 0
TMRj5../af26f.. negprop ownership controlledby Pr4Ru.. upto 0
TMRBW../d1091.. negprop ownership controlledby Pr4Ru.. upto 0
TMcck../e2c14.. ownership of d3bc2.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMcr4../c83e5.. ownership of 25981.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMTB2../8c986.. ownership of 1c497.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMNYN../d3566.. ownership of 936c9.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMLfB../1ddbc.. ownership of 2b6c7.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMcd4../fba31.. ownership of 565f1.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMajB../73f35.. ownership of 204a5.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMXm2../e35e4.. ownership of 23fac.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMUDs../0175b.. ownership of 025eb.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMcAq../4774a.. ownership of 03947.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMXTk../87574.. ownership of 7b5f8.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMPqa../8b709.. ownership of b42fc.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMcf7../b3661.. ownership of ae89b.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMYsc../e4687.. ownership of b8811.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMUen../f8abf.. ownership of 2d44a.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMU9G../15a49.. ownership of 9a40b.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMaXU../9901c.. ownership of 2901c.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMWqZ../a58a4.. ownership of 1cc88.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMXvD../68a2d.. ownership of 6696a.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMGBL../2cb2f.. ownership of d8898.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMMzE../1fda8.. ownership of 367e6.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMHAW../14a94.. ownership of cc8f6.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMHh2../d46b5.. ownership of b0dce.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMQCa../6b27b.. ownership of c3fe4.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMVNE../0db5b.. ownership of ad656.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMRdo../7cca9.. ownership of 8bd75.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMH77../28387.. ownership of 93720.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMNnh../d626c.. ownership of d5d9d.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMciG../e31d7.. ownership of 50594.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMPRP../8192d.. ownership of d4c6f.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMYdy../08cf1.. ownership of 9fc94.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMGn3../70fb9.. ownership of a8d0a.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMWGA../5767b.. ownership of eb789.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMTnL../73d4d.. ownership of 896cc.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMZiZ../14a86.. ownership of 39854.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMSo9../6f209.. ownership of c29e2.. as prop with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMGxd../86e0c.. ownership of c2ff2.. as obj with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
TMVcB../6eba2.. ownership of 1db70.. as obj with payaddr Pr4Ru.. rightscost 0.00 controlledby Pr4Ru.. upto 0
PUNKw../102d7.. doc published by Pr4Ru..

Definition False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ False
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 39854..^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0 (proof)
Theorem eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1 (proof)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 13bcd..^iff_def : iff = λ x1 x2 : ο . and (x1 ⟶ x2) (x2 ⟶ x1)
Theorem 9fc94.. : ∀ x0 x1 : ο . iff x0 x1 ⟶ and (x0 ⟶ x1) (x1 ⟶ x0) (proof)
Theorem 50594..^iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1 (proof)
Theorem 93720..^iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0 (proof)
Known 32c82..^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem ad656.. : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x2) ⟶ x2 (proof)
Known c1173..^Subq_def : Subq = λ x1 x2 . ∀ x3 . In x3 x1 ⟶ In x3 x2
Theorem b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1 (proof)
Theorem 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1 (proof)
Theorem 6696a..^Subq_ref : ∀ x0 . Subq x0 x0 (proof)
Known 7f305..^EmptyAx : not (∀ x0 : ο . (∀ x1 . In x1 0 ⟶ x0) ⟶ x0)
Theorem 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False (proof)
Known da6c8..^PowerEq : ∀ x0 x1 . iff (In x1 (Power x0)) (Subq x1 x0)
Theorem 2d44a..^PowerI : ∀ x0 x1 . Subq x1 x0 ⟶ In x1 (Power x0) (proof)
Theorem ae89b..^PowerE : ∀ x0 x1 . In x1 (Power x0) ⟶ Subq x1 x0 (proof)
Theorem 7b5f8..^{Self_In_Power} : ∀ x0 . In x0 (Power x0) (proof)
Theorem 025eb.. : 0 = Power 0 ⟶ False (proof)
Theorem 204a5.. : (∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 . and (x6 = x1 (x1 x5 (x1 x7 (x1 (x1 (x1 (x1 x6 (x1 (x1 x5 (x1 x5 (x1 (x1 x5 (x1 (x4 x5) (x1 (x1 x7 (x1 x6 (x1 x6 x6))) x5))) (x1 (x4 (x1 (x1 (x4 x7) x5) (x1 x5 x5))) (x1 x6 (x1 x6 (x1 (x1 (x1 x5 (x1 (x1 x5 (x1 (x4 x6) x7)) (x4 (x1 x7 x5)))) x6) (x4 (x1 (x1 x7 (x1 x5 (x1 (x4 (x1 x5 x7)) x5))) (x1 (x1 (x1 x6 (x1 (x4 x5) x6)) x6) (x4 (x4 (x1 (x1 (x1 (x1 x5 (x1 (x1 x6 (x1 (x1 x7 x5) x7)) x6)) x7) (x1 x7 (x1 x5 x5))) x6))))))))))))) (x1 (x1 (x1 (x1 (x1 x6 (x1 x5 x5)) (x4 (x4 (x1 x7 (x4 (x4 (x1 x7 x5))))))) x5) x6) (x1 x6 x7)))) x5) x5) (x4 x6)))) (x1 (x1 (x4 (x1 (x4 (x1 (x1 (x1 (x1 x7 (x1 (x4 (x4 (x1 (x1 x5 x6) x7))) (x4 (x1 x5 x5)))) x5) (x4 x5)) (x1 (x1 (x1 (x1 (x1 x5 x7) (x4 (x4 (x4 x7)))) x7) x6) x5))) (x1 (x1 (x1 x6 x5) (x4 x6)) x6))) x7) x6)) (∃ x8 . x3 (x4 x5))) ⟶ False (proof)
Theorem 2b6c7.. : (∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 x8 x9 . and (∀ x10 . x4 x9 = x10 ⟶ and (x2 x10) (x7 = x5 ⟶ and (∀ x11 . x9 = x8) (∃ x11 . x3 x10)) ⟶ ∃ x11 . x7 = x7) (not (x3 (x4 (x4 (x1 x7 x5))))) ⟶ x6 = x9) ⟶ False (proof)
Theorem 1c497.. : (∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 . x4 (x1 (x1 (x1 (x1 (x1 (x1 x6 x5) (x1 (x1 (x1 x6 x5) (x1 x7 (x1 (x1 (x1 x5 x5) (x1 (x1 (x1 (x1 x5 (x1 (x1 x6 (x1 x5 (x1 x5 x7))) x5)) x7) (x1 (x4 x6) x7)) (x1 (x1 (x1 (x1 x5 (x4 (x1 x7 x5))) (x1 x6 x6)) (x1 x6 (x1 x7 x5))) x5))) x7))) x5)) x6) (x1 x6 (x1 x5 (x1 (x1 (x4 x5) (x1 (x1 x6 x6) x6)) x5)))) (x4 (x4 x6))) x5) = x4 (x4 x7)) ⟶ False (proof)
Theorem d3bc2.. : (∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 . ∀ x8 : ο . (∀ x9 . and (x9 = x7) (x4 (x1 (x1 (x4 (x1 (x1 (x1 (x1 (x1 x5 x7) (x4 (x4 (x1 (x1 x7 x5) x7)))) (x1 (x1 x5 x5) (x1 (x4 x5) (x1 x7 (x1 (x4 x5) x9))))) x9) x9)) x5) (x4 x5)) = x6) ⟶ x8) ⟶ x8) ⟶ False (proof)