Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCSA../ba400..
PUci7../dd656..
vout
PrCSA../c7853.. 0.01 bars
TMZHy../ffb18.. ownership of 05733.. as prop with payaddr PrJJf.. rights free controlledby PrJJf.. upto 0
TMPVb../3fc70.. ownership of 9fcb2.. as prop with payaddr PrJJf.. rights free controlledby PrJJf.. upto 0
PUbkz../1adb2.. doc published by PrJJf..
Known 7c02f..andI : ∀ x0 x1 : ο . x0x1and x0 x1
Known c1173..Subq_def : Subq = λ x1 x2 . ∀ x3 . In x3 x1In x3 x2
Theorem 05733.. : ∀ x0 : ο . (∀ x1 . and (Subq x1 (Power (Power (Power (Power 0))))) (∀ x2 . (∀ x3 . Subq x3 x2∀ x4 x5 . and (not (tuple_p x4 x5)) (and (exactly5 x1) (not (atleast2 x3)))SNo_ (Sing (SNoLev x1)) x5)x2 = x2)x0)x0 (proof)