Proofgold Signed Transaction

vin
Pr314../20380.. PULZn../c9a24..

vout

Pr314../99fc7.. 44.14 bars
TMNJL../922c0.. ownership of 40e63.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMMLP../df921.. ownership of f844e.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMJ2h../b15ae.. ownership of 097ec.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMYyj../e8f4f.. ownership of c802f.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMHvn../005c0.. ownership of d5450.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMWvb../f30b4.. ownership of af5c9.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMdFS../6024f.. ownership of 7484f.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMHsc../67431.. ownership of 5b2d2.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMViY../5090f.. ownership of 84934.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMVPZ../45fca.. ownership of c5fc1.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZnZ../0841c.. ownership of c38f0.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMMuX../2e447.. ownership of 45a71.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMaAs../7d7f8.. ownership of a616f.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMTgt../fce5a.. ownership of 6f139.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMFEF../078e1.. ownership of 0869d.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMJTE../5ddfa.. ownership of c7c4a.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMdvs../b9917.. ownership of 440f9.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMRpi../a45df.. ownership of 1c4b7.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMXZB../a0a5e.. ownership of f9f9c.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMR1e../79500.. ownership of fab35.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMWqR../7dce1.. ownership of 07fd4.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMHB4../627b8.. ownership of 072d8.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMQ4T../94087.. ownership of 523de.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMQ2k../2a8f0.. ownership of 8c3e9.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMc3U../e3bd9.. ownership of 7b3f7.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKAU../3b661.. ownership of 221fd.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMH8E../34bfb.. ownership of 7f221.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMWk1../2d804.. ownership of d490e.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMRNE../82647.. ownership of ef681.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMPeo../3a20d.. ownership of 1df4b.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZ8v../aa669.. ownership of 9c07c.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKTQ../54a2e.. ownership of e1da7.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMRvc../c1c89.. ownership of 0dacf.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMc1a../0cd77.. ownership of cc980.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMaVj../57479.. ownership of 3f1df.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMP3v../83767.. ownership of 431ff.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMboF../6f65a.. ownership of 1d79d.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMNLd../2b9df.. ownership of dd2a3.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZfH../d1ef6.. ownership of 989da.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMcRv../e8b06.. ownership of c8482.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKTg../d0402.. ownership of 2b257.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMbr9../5952b.. ownership of d768d.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMctT../00771.. ownership of 7cd66.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMSu7../37230.. ownership of 3115e.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZcV../cf15a.. ownership of e47cc.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMYL2../fe2d9.. ownership of 040f1.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMcBv../fd03e.. ownership of e5fe3.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMNYz../1f128.. ownership of 2c274.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMLDG../4a624.. ownership of 6b27d.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMEpg../7e2db.. ownership of a833c.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMdXf../4bcdc.. ownership of 11c0b.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMbQX../50f23.. ownership of b0639.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMXqX../5f64e.. ownership of 439cb.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMd9n../4aa35.. ownership of 486f6.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMU2Y../b1663.. ownership of 84b4d.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKDx../ba7a9.. ownership of 11a78.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
PUVHe../62545.. doc published by PrQUS..

Param f4b0e.. : ι → ι → ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Definition 84b4d.. := f4b0e.. 0 1 0 0
Definition 439cb.. := f4b0e.. 0 0 1 0
Definition 11c0b.. := f4b0e.. 0 0 0 1
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param SNo^SNo : ι → ο
Definition 6b27d.. := λ x0 . prim0 (λ x1 . and (SNo x1) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (x0 = f4b0e.. x1 x3 x5 x7) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2))
Definition e5fe3.. := λ x0 . prim0 (λ x1 . and (SNo x1) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (x0 = f4b0e.. (6b27d.. x0) x1 x3 x5) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2))
Definition e47cc.. := λ x0 . prim0 (λ x1 . and (SNo x1) (∀ x2 : ο . (∀ x3 . and (SNo x3) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) x1 x3) ⟶ x2) ⟶ x2))
Definition 7cd66.. := λ x0 . prim0 (λ x1 . and (SNo x1) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) (e47cc.. x0) x1))
Definition 8c189.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (x0 = f4b0e.. x2 x4 x6 x8) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem 3f1df.. : ∀ x0 . 8c189.. x0 ⟶ and (SNo (6b27d.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (x0 = f4b0e.. (6b27d.. x0) x2 x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1) (proof)
Theorem 0dacf.. : ∀ x0 . 8c189.. x0 ⟶ and (SNo (e5fe3.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) x2 x4) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1) (proof)
Theorem 9c07c.. : ∀ x0 . 8c189.. x0 ⟶ and (SNo (e47cc.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) (e47cc.. x0) x2) ⟶ x1) ⟶ x1) (proof)
Theorem ef681.. : ∀ x0 . 8c189.. x0 ⟶ and (SNo (7cd66.. x0)) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) (e47cc.. x0) (7cd66.. x0)) (proof)
Theorem 7f221.. : ∀ x0 . 8c189.. x0 ⟶ SNo (6b27d.. x0) (proof)
Theorem 7b3f7.. : ∀ x0 . 8c189.. x0 ⟶ SNo (e5fe3.. x0) (proof)
Theorem 523de.. : ∀ x0 . 8c189.. x0 ⟶ SNo (e47cc.. x0) (proof)
Theorem 07fd4.. : ∀ x0 . 8c189.. x0 ⟶ SNo (7cd66.. x0) (proof)
Theorem f9f9c.. : ∀ x0 . 8c189.. x0 ⟶ x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) (e47cc.. x0) (7cd66.. x0) (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 440f9.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ 8c189.. (f4b0e.. x0 x1 x2 x3) (proof)
Theorem 0869d.. : ∀ x0 . 8c189.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 x4 x5 . SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ x0 = f4b0e.. x2 x3 x4 x5 ⟶ x1 (f4b0e.. x2 x3 x4 x5)) ⟶ x1 x0 (proof)
Known SNo_0^SNo_0 : SNo 0
Known SNo_1^SNo_1 : SNo 1
Theorem a616f.. : 8c189.. 84b4d.. (proof)
Theorem c38f0.. : 8c189.. 439cb.. (proof)
Theorem 84934.. : 8c189.. 11c0b.. (proof)
Known 84fad.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x0 = x4
Theorem 7484f.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ 6b27d.. (f4b0e.. x0 x1 x2 x3) = x0 (proof)
Known aa1e8.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x1 = x5
Theorem d5450.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ e5fe3.. (f4b0e.. x0 x1 x2 x3) = x1 (proof)
Known 04ead.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x2 = x6
Theorem 097ec.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ e47cc.. (f4b0e.. x0 x1 x2 x3) = x2 (proof)
Known 57cf4.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x3 = x7
Theorem 40e63.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ 7cd66.. (f4b0e.. x0 x1 x2 x3) = x3 (proof)
Param minus_SNo^minus_SNo : ι → ι
Definition 2b257.. := λ x0 . f4b0e.. (minus_SNo (6b27d.. x0)) (minus_SNo (e5fe3.. x0)) (minus_SNo (e47cc.. x0)) (minus_SNo (7cd66.. x0))
Param add_SNo^add_SNo : ι → ι → ι
Definition 989da.. := λ x0 x1 . f4b0e.. (add_SNo (6b27d.. x0) (6b27d.. x1)) (add_SNo (e5fe3.. x0) (e5fe3.. x1)) (add_SNo (e47cc.. x0) (e47cc.. x1)) (add_SNo (7cd66.. x0) (7cd66.. x1))
Param mul_SNo^mul_SNo : ι → ι → ι
Definition 1d79d.. := λ x0 x1 . f4b0e.. (add_SNo (mul_SNo (6b27d.. x0) (6b27d.. x1)) (add_SNo (minus_SNo (mul_SNo (e5fe3.. x0) (e5fe3.. x1))) (add_SNo (minus_SNo (mul_SNo (e47cc.. x0) (e47cc.. x1))) (minus_SNo (mul_SNo (7cd66.. x0) (7cd66.. x1)))))) (add_SNo (mul_SNo (6b27d.. x0) (e5fe3.. x1)) (add_SNo (mul_SNo (e5fe3.. x0) (6b27d.. x1)) (add_SNo (mul_SNo (e47cc.. x0) (7cd66.. x1)) (minus_SNo (mul_SNo (7cd66.. x0) (e47cc.. x1)))))) (add_SNo (mul_SNo (6b27d.. x0) (e47cc.. x1)) (add_SNo (minus_SNo (mul_SNo (e5fe3.. x0) (7cd66.. x1))) (add_SNo (mul_SNo (e47cc.. x0) (6b27d.. x1)) (mul_SNo (7cd66.. x0) (e5fe3.. x1))))) (add_SNo (mul_SNo (6b27d.. x0) (7cd66.. x1)) (add_SNo (mul_SNo (e5fe3.. x0) (e47cc.. x1)) (add_SNo (minus_SNo (mul_SNo (e47cc.. x0) (e5fe3.. x1))) (mul_SNo (7cd66.. x0) (6b27d.. x1)))))