vin

vout

PrRJn../9a59a.. 9.95 bars
TMcet../f8782.. ownership of 052e0.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMWeQ../3f8f1.. ownership of 4993d.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMS3y../4fcd2.. ownership of 256a7.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMYp3../be881.. ownership of 9c826.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMcpG../df59c.. ownership of 61bcd.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMX14../07dda.. ownership of 4cee5.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKAj../46f81.. ownership of 6cc17.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKkZ../e03ae.. ownership of 41522.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMTZi../0f1de.. ownership of c369e.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMcxv../b7396.. ownership of 28342.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMTva../17053.. ownership of 4b639.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMS8R../081e5.. ownership of f9887.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMdaH../402ba.. ownership of 5e04b.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMNy4../9ae46.. ownership of ba81f.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMdu9../c405c.. ownership of 33aee.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMPit../ea6c1.. ownership of bd598.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMY3f../4d9d4.. ownership of db996.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMMvh../cec85.. ownership of 5ec44.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMW6c../8b5dc.. ownership of b2ead.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMUhi../679dd.. ownership of a2891.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZw2../3b65b.. ownership of f16c1.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMRww../cae8b.. ownership of 6cb86.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMbJ6../d7c01.. ownership of d3315.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMaUs../ed1ad.. ownership of 7803f.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZ6v../a6b70.. ownership of 7d0dc.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMUHf../99f43.. ownership of 9b68e.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMTSb../667e7.. ownership of 1c92a.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMFo3../9de4f.. ownership of 83b1d.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMNef../53be7.. ownership of 6c4fc.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMY5Y../c7504.. ownership of 56a38.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMUWA../99a7f.. ownership of 0de29.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMadj../23de9.. ownership of 2a9fa.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMNnQ../b3375.. ownership of 416cf.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMTcS../7b3b6.. ownership of 8acfb.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZQw../372c1.. ownership of 76017.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKax../a408d.. ownership of 56bf4.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMV5J../fe5b5.. ownership of 9325f.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMbd3../b6c7f.. ownership of 4cf7e.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMNa9../845b7.. ownership of 5576f.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKSZ../b59bf.. ownership of 9d7a1.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMdJy../f739e.. ownership of d1304.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMScc../09325.. ownership of 2e291.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMX7j../a0f3b.. ownership of d3d48.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKn8../b7a69.. ownership of 40deb.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMb3Z../c888c.. ownership of 3e3aa.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMMRn../0e193.. ownership of 224fb.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMPFq../c85b3.. ownership of 371c6.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMH9s../a07e5.. ownership of 544f4.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMVfE../524ef.. ownership of 68e0b.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKNu../0b466.. ownership of 5b838.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMNb8../47d88.. ownership of eb0da.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMPbu../bcff8.. ownership of f3194.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMQUx../bf167.. ownership of 85533.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMaL9../42741.. ownership of 62ffb.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMQKj../20508.. ownership of 5b520.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMc7k../c8d5b.. ownership of a297e.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMUgf../b63f1.. ownership of 4aab3.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMXK5../f919f.. ownership of 8da13.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZq5../7ac72.. ownership of 1c01b.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMFLe../6da6e.. ownership of be33d.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMJan../60a91.. ownership of 95e88.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMWwp../2dd2c.. ownership of 9846a.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMbxf../40871.. ownership of 74066.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TML5y../52d0d.. ownership of d0de4.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMbzU../4f168.. ownership of 41fb9.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKEV../72865.. ownership of 5311e.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMQoo../76c7f.. ownership of 22598.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMbi6../c2745.. ownership of 28622.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMPck../00e33.. ownership of a0628.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMYjp../d1608.. ownership of 2d0b1.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMJ3N../45869.. ownership of b1848.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMSYV../6db41.. ownership of 1fb48.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMXTj../46a96.. ownership of d634d.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMaDF../1407e.. ownership of 1cbea.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMLVA../8ecdb.. ownership of 28f8d.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMU3B../d4775.. ownership of 32eb0.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMJi9../3b30d.. ownership of 8d0f8.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMb73../06e5e.. ownership of dae24.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
PUN7o../24fec.. doc published by PrQUS..

Param binunion^binunion : ι → ι → ι
Param SetAdjoin^SetAdjoin : ι → ι → ι
Param Sing^Sing : ι → ι
Definition e9c39.. := λ x0 x1 x2 . binunion x1 {SetAdjoin x3 (Sing x0)|x3 ∈ x2}
Param ordsucc^ordsucc : ι → ι
Definition ad280.. := e9c39.. 2
Known 43bcd.. : ∀ x0 . ad280.. x0 0 = x0
Param SNo^SNo : ι → ο
Known 8ae5d.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x2 ⟶ ad280.. x0 x1 = ad280.. x2 x3 ⟶ x0 = x2
Known 943f5.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ ad280.. x0 x1 = ad280.. x2 x3 ⟶ x1 = x3
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition c7ce4.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (x0 = ad280.. x2 x4) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Known e4080.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ c7ce4.. (ad280.. x0 x1)
Known 3577c.. : ∀ x0 . c7ce4.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 . SNo x2 ⟶ SNo x3 ⟶ x0 = ad280.. x2 x3 ⟶ x1 (ad280.. x2 x3)) ⟶ x1 x0
Definition 8d0f8.. := ad280.. 0 1
Definition 28f8d.. := λ x0 . prim0 (λ x1 . and (SNo x1) (∀ x2 : ο . (∀ x3 . and (SNo x3) (x0 = ad280.. x1 x3) ⟶ x2) ⟶ x2))
Definition d634d.. := λ x0 . prim0 (λ x1 . and (SNo x1) (x0 = ad280.. (28f8d.. x0) x1))
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem 95e88.. : ∀ x0 . c7ce4.. x0 ⟶ and (SNo (28f8d.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (x0 = ad280.. (28f8d.. x0) x2) ⟶ x1) ⟶ x1) (proof)
Theorem 1c01b.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ 28f8d.. (ad280.. x0 x1) = x0 (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 4aab3.. : ∀ x0 . c7ce4.. x0 ⟶ and (SNo (d634d.. x0)) (x0 = ad280.. (28f8d.. x0) (d634d.. x0)) (proof)
Theorem 5b520.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ d634d.. (ad280.. x0 x1) = x1 (proof)
Theorem 85533.. : ∀ x0 . c7ce4.. x0 ⟶ SNo (28f8d.. x0) (proof)
Theorem eb0da.. : ∀ x0 . c7ce4.. x0 ⟶ SNo (d634d.. x0) (proof)
Theorem 68e0b.. : ∀ x0 . c7ce4.. x0 ⟶ x0 = ad280.. (28f8d.. x0) (d634d.. x0) (proof)
Theorem 371c6.. : ∀ x0 x1 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ 28f8d.. x0 = 28f8d.. x1 ⟶ d634d.. x0 = d634d.. x1 ⟶ x0 = x1 (proof)
Param minus_SNo^minus_SNo : ι → ι
Definition b1848.. := λ x0 . ad280.. (minus_SNo (28f8d.. x0)) (minus_SNo (d634d.. x0))
Param add_SNo^add_SNo : ι → ι → ι
Definition a0628.. := λ x0 x1 . ad280.. (add_SNo (28f8d.. x0) (28f8d.. x1)) (add_SNo (d634d.. x0) (d634d.. x1))
Param mul_SNo^mul_SNo : ι → ι → ι
Definition 22598.. := λ x0 x1 . ad280.. (add_SNo (mul_SNo (28f8d.. x0) (28f8d.. x1)) (minus_SNo (mul_SNo (d634d.. x0) (d634d.. x1)))) (add_SNo (mul_SNo (28f8d.. x0) (d634d.. x1)) (mul_SNo (d634d.. x0) (28f8d.. x1)))
Param div_SNo^div_SNo : ι → ι → ι
Param exp_SNo_nat^exp_SNo_nat : ι → ι → ι
Definition 41fb9.. := λ x0 . ad280.. (div_SNo (28f8d.. x0) (add_SNo (exp_SNo_nat (28f8d.. x0) 2) (exp_SNo_nat (d634d.. x0) 2))) (minus_SNo (div_SNo (d634d.. x0) (add_SNo (exp_SNo_nat (28f8d.. x0) 2) (exp_SNo_nat (d634d.. x0) 2))))
Definition 74066.. := λ x0 x1 . 22598.. x0 (41fb9.. x1)
Known SNo_0^SNo_0 : SNo 0
Known SNo_1^SNo_1 : SNo 1
Theorem 3e3aa.. : c7ce4.. 8d0f8.. (proof)
Known SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Theorem d3d48.. : ∀ x0 . c7ce4.. x0 ⟶ 28f8d.. (b1848.. x0) = minus_SNo (28f8d.. x0) (proof)
Theorem d1304.. : ∀ x0 . c7ce4.. x0 ⟶ d634d.. (b1848.. x0) = minus_SNo (d634d.. x0) (proof)
Known SNo_add_SNo^SNo_add_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (add_SNo x0 x1)
Theorem 5576f.. : ∀ x0 x1 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ 28f8d.. (a0628.. x0 x1) = add_SNo (28f8d.. x0) (28f8d.. x1) (proof)
Theorem 9325f.. : ∀ x0 x1 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ d634d.. (a0628.. x0 x1) = add_SNo (d634d.. x0) (d634d.. x1) (proof)
Theorem 76017.. : ∀ x0 . c7ce4.. x0 ⟶ c7ce4.. (b1848.. x0) (proof)
Theorem 416cf.. : ∀ x0 . SNo x0 ⟶ 28f8d.. x0 = x0 (proof)
Theorem 0de29.. : ∀ x0 . SNo x0 ⟶ d634d.. x0 = 0 (proof)
Theorem 6c4fc.. : 28f8d.. 0 = 0 (proof)
Theorem 1c92a.. : d634d.. 0 = 0 (proof)
Theorem 7d0dc.. : 28f8d.. 1 = 1 (proof)
Theorem d3315.. : d634d.. 1 = 0 (proof)
Theorem f16c1.. : 28f8d.. 8d0f8.. = 0 (proof)
Theorem b2ead.. : d634d.. 8d0f8.. = 1 (proof)
Known add_SNo_0L^add_SNo_0L : ∀ x0 . SNo x0 ⟶ add_SNo 0 x0 = x0
Theorem db996.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 x1 = a0628.. x0 x1 (proof)
Theorem 33aee.. : ∀ x0 x1 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ c7ce4.. (a0628.. x0 x1) (proof)
Theorem 5e04b.. : ∀ x0 . c7ce4.. x0 ⟶ a0628.. 0 x0 = x0 (proof)
Known add_SNo_0R^add_SNo_0R : ∀ x0 . SNo x0 ⟶ add_SNo x0 0 = x0
Theorem 4b639.. : ∀ x0 . c7ce4.. x0 ⟶ a0628.. x0 0 = x0 (proof)
Known add_SNo_minus_SNo_linv^{add_SNo_minus_SNo_linv} : ∀ x0 . SNo x0 ⟶ add_SNo (minus_SNo x0) x0 = 0
Theorem c369e.. : ∀ x0 . c7ce4.. x0 ⟶ a0628.. (b1848.. x0) x0 = 0 (proof)
Known add_SNo_minus_SNo_rinv^{add_SNo_minus_SNo_rinv} : ∀ x0 . SNo x0 ⟶ add_SNo x0 (minus_SNo x0) = 0
Theorem 6cc17.. : ∀ x0 . c7ce4.. x0 ⟶ a0628.. x0 (b1848.. x0) = 0 (proof)
Known minus_SNo_0^minus_SNo_0 : minus_SNo 0 = 0
Theorem 61bcd.. : ∀ x0 . SNo x0 ⟶ minus_SNo x0 = b1848.. x0 (proof)
Known add_SNo_com^add_SNo_com : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 x1 = add_SNo x1 x0
Theorem 256a7.. : ∀ x0 x1 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ a0628.. x0 x1 = a0628.. x1 x0 (proof)
Known f_eq_i^f_eq_i : ∀ x0 : ι → ι . ∀ x1 x2 . x1 = x2 ⟶ x0 x1 = x0 x2
Known add_SNo_assoc^{add_SNo_assoc} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2
Theorem 052e0.. : ∀ x0 x1 x2 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ c7ce4.. x2 ⟶ a0628.. x0 (a0628.. x1 x2) = a0628.. (a0628.. x0 x1) x2 (proof)

Proofgold Signed Transaction