Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrQyi../cbb83..
PUUqX../8cc55..
vout
PrQyi../f6724.. 6.22 bars
TMcDn../bf43a.. ownership of db1de.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMa8J../1ec2b.. ownership of 18dab.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXwz../f6626.. ownership of adab1.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbHb../012a8.. ownership of dce43.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbXY../88109.. ownership of d9442.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKcV../4a0be.. ownership of 441f5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRyR../79eed.. ownership of 95d11.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMckG../5a3bb.. ownership of 98467.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFQv../96764.. ownership of a8f07.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMc6T../f38d0.. ownership of c2aa6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNTk../0e2fc.. ownership of 3e9f7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNVd../e5caf.. ownership of 5858d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRkD../53a77.. ownership of 22701.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMSgC../164f1.. ownership of b985b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUwq../d2886.. ownership of fbe6e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMX6../9ac8c.. ownership of 0e26a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMURJ../31c99.. ownership of fa3b7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYiG../a92a0.. ownership of d9a10.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMcx../b2aa1.. ownership of d085c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPnf../f0dd5.. ownership of 01294.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTfR../6c6c3.. ownership of a3f6a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMY51../f2caf.. ownership of bbeab.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMT3j../97557.. ownership of 816bd.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMea../7ff22.. ownership of 4da5f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWGH../fd11f.. ownership of 07f4e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdah../a35d7.. ownership of bf2b8.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbE9../56046.. ownership of f5339.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMF14../9a335.. ownership of dd393.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZkW../90884.. ownership of ba5ba.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMGhb../dea1f.. ownership of 5e518.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLXk../edaad.. ownership of f956d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMb3d../b0dd7.. ownership of 869ea.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbvZ../0ff8f.. ownership of dc79e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMN67../c1085.. ownership of 6dfb8.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMVzX../fb50c.. ownership of 019e3.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTPv../b10a5.. ownership of 26fac.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKHM../02f69.. ownership of 3df8e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXfK../aa3a0.. ownership of 4b443.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZ4W../1861f.. ownership of 2cf95.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMSrZ../6ed1f.. ownership of bb0cc.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMc5G../81eda.. ownership of c3434.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNvo../f1c5e.. ownership of fe077.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdwF../f2907.. ownership of a16a6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHBW../da2ea.. ownership of 322d6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMSVQ../c7b67.. ownership of a9609.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPye../44a8e.. ownership of e9366.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMS5Y../2c53a.. ownership of af7b1.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJCB../0ada1.. ownership of 36374.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFrk../edfde.. ownership of 5712d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKuy../fa216.. ownership of 82b4c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXwa../d5752.. ownership of c3da7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdKu../00be1.. ownership of 74ac8.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYRz../51845.. ownership of 90194.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRoj../b3132.. ownership of b1cbd.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMY1K../2c138.. ownership of d5f37.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcTP../f3472.. ownership of 70a8e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMG29../5b123.. ownership of 2e174.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHL2../e9583.. ownership of 74cdc.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYeH../f9f93.. ownership of 45540.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYgZ../f68e4.. ownership of 7a066.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNVT../d0a56.. ownership of 50bed.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPmT../4cdae.. ownership of c47a2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMr2../cf3c6.. ownership of a918d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMaFk../a83b4.. ownership of c92fe.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRiJ../4bafc.. ownership of 91a85.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdDn../b5ff3.. ownership of df15f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUVz../a642c.. ownership of 525d1.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFkS../268b7.. ownership of 7cd03.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUb6../7cef4.. ownership of 62dd3.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMpW../1f839.. ownership of 09fb1.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMK2G../4da79.. ownership of 336f0.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMGk4../99fd4.. ownership of 2abea.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYaj../ca75c.. ownership of cef3c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMEpw../64ca7.. ownership of 86401.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFTs../08de3.. ownership of 4ff4f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdgD../883b7.. ownership of e8b8c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMccK../e11b2.. ownership of 1521b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdTv../ca462.. ownership of 344c7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMU9e../c9496.. ownership of e1175.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTR8../ddf97.. ownership of e9e46.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMX5S../121c9.. ownership of 70d6d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFY6../4a604.. ownership of 3c436.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMEtV../eb2f1.. ownership of 5f9b2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWVD../584f4.. ownership of be387.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRUX../3dde4.. ownership of 69b67.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMGK3../f2cde.. ownership of 6cbf2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNRR../91a23.. ownership of cd2cb.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcXb../17dc0.. ownership of c5746.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPGD../9b064.. ownership of 118d3.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTtq../f2873.. ownership of d7dee.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTj9../f30d2.. ownership of 9dea5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPb4../c65b2.. ownership of 33843.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLoV../96f84.. ownership of 36602.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTPX../93cfe.. ownership of 58ff2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUs7../bb7e2.. ownership of 54790.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWUQ../370bf.. ownership of 909bc.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJPF../41922.. ownership of f3bb6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbnq../11075.. ownership of c7ff2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMG8f../9855c.. ownership of 893fe.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMQog../77624.. ownership of 150e3.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PUYq4../d16e1.. doc published by Pr4zB..
Param add_natadd_nat : ιιι
Param ordsuccordsucc : ιι
Param nat_pnat_p : ιο
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_0nat_0 : nat_p 0
Known add_nat_0Radd_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem 893fe.. : add_nat 4 1 = 5 (proof)
Known nat_1nat_1 : nat_p 1
Theorem f3bb6.. : add_nat 4 2 = 6 (proof)
Known nat_2nat_2 : nat_p 2
Theorem 54790.. : add_nat 4 3 = 7 (proof)
Known nat_3nat_3 : nat_p 3
Theorem 36602.. : add_nat 4 4 = 8 (proof)
Theorem 9dea5.. : add_nat 8 1 = 9 (proof)
Theorem 118d3.. : add_nat 8 2 = 10 (proof)
Theorem cd2cb.. : add_nat 8 3 = 11 (proof)
Theorem 69b67..add_nat_8_4 : add_nat 8 4 = 12 (proof)
Known nat_4nat_4 : nat_p 4
Theorem 5f9b2.. : add_nat 8 5 = 13 (proof)
Known nat_5nat_5 : nat_p 5
Theorem 70d6d.. : add_nat 8 6 = 14 (proof)
Known nat_6nat_6 : nat_p 6
Theorem e1175.. : add_nat 8 7 = 15 (proof)
Known nat_7nat_7 : nat_p 7
Theorem 1521b.. : add_nat 8 8 = 16 (proof)
Theorem 4ff4f.. : add_nat 11 1 = 12 (proof)
Theorem cef3c.. : add_nat 11 2 = 13 (proof)
Theorem 336f0.. : add_nat 11 3 = 14 (proof)
Theorem 62dd3.. : add_nat 11 4 = 15 (proof)
Theorem 525d1.. : add_nat 11 5 = 16 (proof)
Theorem 91a85.. : add_nat 11 6 = 17 (proof)
Theorem a918d.. : add_nat 11 7 = 18 (proof)
Theorem 50bed.. : add_nat 11 8 = 19 (proof)
Known nat_8nat_8 : nat_p 8
Theorem 45540.. : add_nat 11 9 = 20 (proof)
Known nat_9nat_9 : nat_p 9
Theorem 2e174.. : add_nat 11 10 = 21 (proof)
Known nat_10nat_10 : nat_p 10
Theorem d5f37.. : add_nat 11 11 = 22 (proof)
Known nat_11nat_11 : nat_p 11
Theorem 90194.. : add_nat 11 12 = 23 (proof)
Param mul_natmul_nat : ιιι
Known add_nat_1_1_2add_nat_1_1_2 : add_nat 1 1 = 2
Known 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)
Known mul_nat_1Rmul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Known 256ca.. : add_nat 2 2 = 4
Theorem c3da7.. : mul_nat 2 2 = 4 (proof)
Theorem 5712d.. : mul_nat 2 4 = 8 (proof)
Theorem af7b1.. : mul_nat 2 8 = 16 (proof)
Theorem a9609.. : add_nat 6 1 = 7 (proof)
Theorem a16a6.. : add_nat 6 2 = 8 (proof)
Theorem c3434.. : add_nat 6 3 = 9 (proof)
Theorem 2cf95.. : add_nat 6 4 = 10 (proof)
Theorem 3df8e.. : add_nat 16 1 = 17 (proof)
Theorem 019e3.. : add_nat 16 2 = 18 (proof)
Theorem dc79e.. : add_nat 16 3 = 19 (proof)
Theorem f956d.. : add_nat 16 4 = 20 (proof)
Theorem ba5ba.. : add_nat 16 5 = 21 (proof)
Theorem f5339.. : add_nat 16 6 = 22 (proof)
Theorem 07f4e.. : add_nat 16 7 = 23 (proof)
Theorem 816bd.. : add_nat 16 8 = 24 (proof)
Theorem a3f6a.. : add_nat 16 9 = 25 (proof)
Theorem d085c.. : add_nat 16 10 = 26 (proof)
Theorem fa3b7.. : add_nat 16 11 = 27 (proof)
Theorem fbe6e.. : add_nat 16 12 = 28 (proof)
Known nat_12nat_12 : nat_p 12
Theorem 22701.. : add_nat 16 13 = 29 (proof)
Param nat_primrecnat_primrec : ι(ιιι) → ιι
Definition exp_natexp_nat := λ x0 . nat_primrec 1 (λ x1 . mul_nat x0)
Known nat_primrec_Snat_primrec_S : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Known nat_primrec_0nat_primrec_0 : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem 3e9f7..exp_nat_1 : ∀ x0 . exp_nat x0 1 = x0 (proof)
Theorem a8f07.. : exp_nat 2 2 = 4 (proof)
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known mul_nat_SRmul_nat_SR : ∀ x0 x1 . nat_p x1mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Known add_nat_SLadd_nat_SL : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Known add_nat_0Ladd_nat_0L : ∀ x0 . nat_p x0add_nat 0 x0 = x0
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Theorem 95d11.. : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc (mul_nat 2 x1)mul_nat 2 x0 (proof)
Known In_3_4In_3_4 : 34
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Known nat_transnat_trans : ∀ x0 . nat_p x0∀ x1 . x1x0x1x0
Known 4f402..exp_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (exp_nat x0 x1)
Theorem d9442.. : ∀ x0 . nat_p x0ordsucc (exp_nat 2 (ordsucc x0))exp_nat 2 (ordsucc (ordsucc x0)) (proof)
Theorem adab1.. : exp_nat 2 3 = 8 (proof)
Theorem db1de.. : exp_nat 2 4 = 16 (proof)