Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrJAV../1874c..
PUUXL../08c12..
vout
PrJAV../55c95.. 6.47 bars
TMHiZ../580b9.. ownership of 9ff99.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMYt2../2f6cc.. ownership of ebe21.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMKV5../d7573.. ownership of e7d21.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMNv2../261b1.. ownership of e6fc1.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMMNC../7b15b.. ownership of 0165a.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMQmi../5e970.. ownership of d1d62.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMEgZ../1de15.. ownership of a1fba.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMF8n../78b25.. ownership of 8358f.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMTb2../34b43.. ownership of 70139.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGnP../d0cdb.. ownership of 75de2.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFrC../f5d82.. ownership of 787bf.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMc44../24d69.. ownership of 28f71.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMPrq../b70e1.. ownership of ea810.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMHss../d4ae5.. ownership of cc514.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXXH../01a77.. ownership of 76fc5.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMRPb../2be07.. ownership of 48ca7.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMWqX../06028.. ownership of a0bc4.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMHGh../d6c78.. ownership of aea71.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMT9K../e4123.. ownership of 5fa28.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMX9H../d4681.. ownership of af5f6.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGEQ../74e96.. ownership of 4f8b9.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMK4Z../db08a.. ownership of 9735b.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMTmT../e0db4.. ownership of 9ae2c.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMMdk../8179e.. ownership of 64174.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMVNC../01929.. ownership of aa403.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMHhg../df54f.. ownership of a2a94.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMYee../8c3a3.. ownership of 43798.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMZjH../708ce.. ownership of ff333.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMPkk../22874.. ownership of e1674.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGKN../a6b25.. ownership of 8358b.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMWJQ../2800a.. ownership of c28a3.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMJGQ../7b649.. ownership of 17250.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMEwK../6009e.. ownership of 8e35a.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMQba../fb7ff.. ownership of 37c53.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMTkK../eee23.. ownership of b3e62.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMbQx../26801.. ownership of 23f21.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMHvT../66213.. ownership of 5e7a6.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFmm../b84e5.. ownership of 73e63.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMPsb../f2dde.. ownership of a54ca.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMdvX../efdb7.. ownership of 729ee.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMc53../0c98e.. ownership of 35592.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFX8../7df78.. ownership of 1b17d.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFeY../b6197.. ownership of f9373.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMY2n../56253.. ownership of 5cef7.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMMYj../baca3.. ownership of e93bf.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMYaH../bf68b.. ownership of acdba.. as obj with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
PUfRN../b5eb2.. doc published by Pr6Pc..
Param andand : οοο
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Definition surjsurj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Param omegaomega : ι
Param ccad8.. : ιιο
Definition e93bf.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2omega) (ccad8.. x0 x2)x1)x1
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition f9373.. := λ x0 . not (e93bf.. x0)
Param mul_natmul_nat : ιιι
Definition divides_natdivides_nat := λ x0 x1 . and (and (x0omega) (x1omega)) (∀ x2 : ο . (∀ x3 . and (x3omega) (mul_nat x0 x3 = x1)x2)x2)
Param ordsuccordsucc : ιι
Param oror : οοο
Definition prime_natprime_nat := λ x0 . and (and (x0omega) (1x0)) (∀ x1 . x1omegadivides_nat x1 x0or (x1 = 1) (x1 = x0))
Param setminussetminus : ιιι
Definition coprime_natcoprime_nat := λ x0 x1 . and (and (x0omega) (x1omega)) (∀ x2 . x2setminus omega 1divides_nat x2 x0divides_nat x2 x1x2 = 1)
Param add_natadd_nat : ιιι
Definition b3e62..equiv_nat_mod := λ x0 x1 x2 . and (and (and (x0omega) (x1omega)) (x2omega)) (or (∀ x3 : ο . (∀ x4 . and (x4omega) (add_nat x0 (mul_nat x4 x2) = x1)x3)x3) (∀ x3 : ο . (∀ x4 . and (x4omega) (add_nat x1 (mul_nat x4 x2) = x0)x3)x3))
Param nat_primrecnat_primrec : ι(ιιι) → ιι
Definition exp_natexp_nat := λ x0 . nat_primrec 1 (λ x1 . mul_nat x0)
Definition even_nateven_nat := λ x0 . and (x0omega) (∀ x1 : ο . (∀ x2 . and (x2omega) (x0 = mul_nat 2 x2)x1)x1)
Definition odd_natodd_nat := λ x0 . and (x0omega) (∀ x1 . x1omegax0 = mul_nat 2 x1∀ x2 : ο . x2)
Definition nat_factorialnat_factorial := nat_primrec 1 (λ x0 . mul_nat (ordsucc x0))
Param apap : ιιι
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
Definition aa403.. := λ x0 . ap (nat_primrec (lam omega (λ x1 . If_i (x1 = 0) 1 0)) (λ x1 x2 . lam omega (λ x3 . If_i (x3 = 0) 1 (add_nat (ap x2 (prim3 x3)) (ap x2 x3)))) x0)
Param SepSep : ι(ιο) → ι
Definition 9ae2c.. := λ x0 . prim0 (λ x1 . and (x1omega) (ccad8.. x1 {x2 ∈ ordsucc x0|and (0x2) (coprime_nat x2 x0)}))
Param div_SNodiv_SNo : ιιι
Param mul_SNomul_SNo : ιιι
Param add_SNoadd_SNo : ιιι
Param minus_SNominus_SNo : ιι
Definition 4f8b9.. := λ x0 x1 . div_SNo (nat_factorial x0) (mul_SNo (nat_factorial (add_SNo x0 (minus_SNo x1))) (nat_factorial x1))
Param int_alt1int : ι
Definition divides_int_alt1divides_int := λ x0 x1 . and (and (x0int_alt1) (x1int_alt1)) (∀ x2 : ο . (∀ x3 . and (x3int_alt1) (mul_SNo x0 x3 = x1)x2)x2)
Definition a0bc4..equiv_int_mod := λ x0 x1 x2 . and (and (and (x0int_alt1) (x1int_alt1)) (x2setminus omega 1)) (divides_int_alt1 (add_SNo x0 (minus_SNo x1)) x2)
Definition 76fc5..coprime_int := λ x0 x1 . and (and (x0int_alt1) (x1int_alt1)) (∀ x2 . x2setminus omega 1divides_int_alt1 x2 x0divides_int_alt1 x2 x1x2 = 1)
Definition exp_SNo_natexp_SNo_nat := λ x0 . nat_primrec 1 (λ x1 . mul_SNo x0)
Param explicit_Natsexplicit_Nats : ιι(ιι) → ο
Param explicit_Nats_primrecexplicit_Nats_primrec : ιι(ιι) → ι(ιιι) → ιι
Param explicit_Nats_one_plusexplicit_Nats_one_plus : ιι(ιι) → ιιι
Param explicit_Nats_one_plusexplicit_Nats_one_plus : ιι(ιι) → ιιι
Definition explicit_Nats_one_mult_alt := λ x0 x1 . λ x2 : ι → ι . λ x3 . explicit_Nats_primrec x0 x1 x2 x3 (λ x4 . explicit_Nats_one_plus x0 x1 x2 x3)
Definition explicit_Nats_lt := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (x3x0) (x4x0)) (∀ x5 : ο . (∀ x6 . and (x6x0) (explicit_Nats_one_plus x0 x1 x2 x6 x3 = x4)x5)x5)
Definition 75de2.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (x3x0) (∀ x4 . x4x0explicit_Nats_lt x0 x1 x2 x4 x3or (x4 = x1) (x4 = x3))
Definition explicit_Nats_max_is_one := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (x3x0) (x4x0)) (∀ x5 . x5x0explicit_Nats_lt x0 x1 x2 x5 x3explicit_Nats_lt x0 x1 x2 x5 x4x5 = 1)
Definition a1fba.. := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 x5 . and (and (and (x3x0) (x4x0)) (x5x0)) (or (or (x3 = x4) (∀ x6 : ο . (∀ x7 . and (x7x0) (explicit_Nats_one_plus x0 x1 x2 x3 (explicit_Nats_one_plus x0 x1 x2 x7 x5) = x4)x6)x6)) (∀ x6 : ο . (∀ x7 . and (x7x0) (explicit_Nats_one_plus x0 x1 x2 x4 (explicit_Nats_one_plus x0 x1 x2 x7 x5) = x3)x6)x6))
Definition explicit_Nats_one_ltexplicit_Nats_one_lt := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (x3x0) (x4x0)) (∀ x5 : ο . (∀ x6 . and (x6x0) (explicit_Nats_one_plus x0 x1 x2 x3 x6 = x4)x5)x5)
Definition explicit_Nats_one_leexplicit_Nats_one_le := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (x3x0) (x4x0)) (or (x3 = x4) (∀ x5 : ο . (∀ x6 . and (x6x0) (explicit_Nats_one_plus x0 x1 x2 x3 x6 = x4)x5)x5))
Definition e6fc1.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (x3x0) (∀ x4 : ο . (∀ x5 . and (x5x0) (x3 = explicit_Nats_one_plus x0 x1 x2 (x2 x1) x5)x4)x4)
Definition e7d21.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . and (x3x0) (∀ x4 . x4x0x3 = explicit_Nats_one_plus x0 x1 x2 (x2 x1) x4∀ x5 : ο . x5)
Definition 9ff99.. := λ x0 x1 . λ x2 : ι → ι . explicit_Nats_primrec x0 x1 x2 x1 (λ x3 x4 . If_i (and (x3 = x1∀ x5 : ο . x5) (explicit_Nats_max_is_one x0 x1 x2 x3 x3)) (x2 x4) x4)