Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../bad4c..
PUJwo../8a592..
vout
PrCit../d2739.. 3.80 bars
TMUrt../307a3.. ownership of 667cd.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMY4A../64ba0.. ownership of 58d7e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSrn../2765d.. ownership of 54789.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVBi../07aa1.. ownership of cef52.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUXj../8c5ac.. ownership of 1435b.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKYC../f59c6.. ownership of 9ef01.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdR8../e9bda.. ownership of 34154.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQq3../10172.. ownership of ba361.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZ2M../83199.. ownership of 67f22.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLLo../d2d37.. ownership of 06570.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFmi../4b525.. ownership of d568c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMS3v../986fc.. ownership of ff929.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTJz../2f9ea.. ownership of 01ee3.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMX3E../ccb05.. ownership of 8ce01.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLsL../c491a.. ownership of 5e08e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJvc../7c2fd.. ownership of f0704.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZ7o../ee53d.. ownership of 91e6c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMbwH../c266a.. ownership of 84f2e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJkV../a33a4.. ownership of 7ba92.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQdE../21f7d.. ownership of ab150.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZko../24fe8.. ownership of 96b76.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFRR../40719.. ownership of 73689.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTY7../c2023.. ownership of d63b1.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQAc../e2a63.. ownership of 2ed7a.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUMc../f9642.. ownership of 9c9ec.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMHD9../dcf13.. ownership of d6cba.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJWv../13bec.. ownership of caae0.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTmH../e4a5a.. ownership of ad9ef.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRkV../ae612.. ownership of 49a59.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQcN../a9b4d.. ownership of bd203.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQiF../b0351.. ownership of 126ca.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMa6H../b8f70.. ownership of a2c7b.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMYaa../870d3.. ownership of 0158f.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJUm../81604.. ownership of 2418e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZAJ../c893a.. ownership of abaf6.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMXU7../b972b.. ownership of 2f2ff.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMcZM../85c61.. ownership of 8413f.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMcQz../51661.. ownership of 44523.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMbYz../6665d.. ownership of e5453.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJTH../73498.. ownership of 046cd.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSBu../c4fea.. ownership of 3224f.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMPTW../a656a.. ownership of 1f0d4.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQYY../f6a4d.. ownership of 8f513.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMN43../09d93.. ownership of ef54e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMV9H../e635e.. ownership of 8a085.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUnW../bf993.. ownership of 38828.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PUMSU../888b0.. doc published by Pr4zB..
Param ordsuccordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known 179f3.. : 0 ∈ u21
Theorem c34a2.. : 0 ∈ u22 (proof)
Known 07fdb.. : u1 ∈ u21
Theorem 617e2.. : u1 ∈ u22 (proof)
Known c25ea.. : u2 ∈ u21
Theorem a7839.. : u2 ∈ u22 (proof)
Known 0750b.. : u3 ∈ u21
Theorem 9018e.. : u3 ∈ u22 (proof)
Known 701a9.. : u4 ∈ u21
Theorem 540e6.. : u4 ∈ u22 (proof)
Known 0dc69.. : u5 ∈ u21
Theorem 8a085.. : u5 ∈ u22 (proof)
Known 1d1d3.. : u6 ∈ u21
Theorem 8f513.. : u6 ∈ u22 (proof)
Known 0b77c.. : u7 ∈ u21
Theorem 3224f.. : u7 ∈ u22 (proof)
Known 5fc29.. : u8 ∈ u21
Theorem e5453.. : u8 ∈ u22 (proof)
Known 4b046.. : u9 ∈ u21
Theorem 8413f.. : u9 ∈ u22 (proof)
Known 46da3.. : u10 ∈ u21
Theorem abaf6.. : u10 ∈ u22 (proof)
Known 3ad1f.. : u11 ∈ u21
Theorem 0158f.. : u11 ∈ u22 (proof)
Known 07061.. : u12 ∈ u21
Theorem 126ca.. : u12 ∈ u22 (proof)
Known d16a4.. : u13 ∈ u21
Theorem 49a59.. : u13 ∈ u22 (proof)
Known a6788.. : u14 ∈ u21
Theorem caae0.. : u14 ∈ u22 (proof)
Known ce294.. : u15 ∈ u21
Theorem 9c9ec.. : u15 ∈ u22 (proof)
Known 20f4b.. : u16 ∈ u21
Theorem d63b1.. : u16 ∈ u22 (proof)
Known d5f90.. : u17 ∈ u21
Theorem 96b76.. : u17 ∈ u22 (proof)
Known 08993.. : u18 ∈ u21
Theorem 7ba92.. : u18 ∈ u22 (proof)
Known b8dfd.. : u19 ∈ u21
Theorem 91e6c.. : u19 ∈ u22 (proof)
Known c955e.. : u20 ∈ u21
Theorem 5e08e.. : u20 ∈ u22 (proof)
Known ordsuccI2ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem 01ee3.. : u21 ∈ u22 (proof)
Param apap : ι → ι → ι
Param lamSigma : ι → (ι → ι) → ι
Param If_iIf_i : ο → ι → ι → ι
Known d21a1.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 x4 . (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ ap (lam x1 (λ x6 . If_i (x6 = x3) x0 (x2 (ordsucc x3) x6))) x4 = ap (lam x1 (x2 (ordsucc x3))) x4
Known fd18a.. : u19 = 0 ⟶ ∀ x0 : ο . x0
Known 70279.. : u19 = u1 ⟶ ∀ x0 : ο . x0
Known 81672.. : u19 = u2 ⟶ ∀ x0 : ο . x0
Known 2e7b7.. : u19 = u3 ⟶ ∀ x0 : ο . x0
Known 26e28.. : u19 = u4 ⟶ ∀ x0 : ο . x0
Known dcd9d.. : u19 = u5 ⟶ ∀ x0 : ο . x0
Known b1809.. : u19 = u6 ⟶ ∀ x0 : ο . x0
Known 36989.. : u19 = u7 ⟶ ∀ x0 : ο . x0
Known 9b462.. : u19 = u8 ⟶ ∀ x0 : ο . x0
Known 4545d.. : u19 = u9 ⟶ ∀ x0 : ο . x0
Known 7d160.. : u19 = u10 ⟶ ∀ x0 : ο . x0
Known 8109a.. : u19 = u11 ⟶ ∀ x0 : ο . x0
Known a5243.. : u19 = u12 ⟶ ∀ x0 : ο . x0
Known 8c598.. : u19 = u13 ⟶ ∀ x0 : ο . x0
Known 35149.. : u19 = u14 ⟶ ∀ x0 : ο . x0
Known 38ccc.. : u19 = u15 ⟶ ∀ x0 : ο . x0
Known 0384c.. : u19 = u16 ⟶ ∀ x0 : ο . x0
Known 3c054.. : u19 = u17 ⟶ ∀ x0 : ο . x0
Known 97eb4.. : u19 = u18 ⟶ ∀ x0 : ο . x0
Known 48efb.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0
Theorem d568c.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u19 = x19 (proof)
Known 4552b.. : u20 = 0 ⟶ ∀ x0 : ο . x0
Known d8b53.. : u20 = u1 ⟶ ∀ x0 : ο . x0
Known c9329.. : u20 = u2 ⟶ ∀ x0 : ο . x0
Known 0af1b.. : u20 = u3 ⟶ ∀ x0 : ο . x0
Known f2a22.. : u20 = u4 ⟶ ∀ x0 : ο . x0
Known 98620.. : u20 = u5 ⟶ ∀ x0 : ο . x0
Known fd91d.. : u20 = u6 ⟶ ∀ x0 : ο . x0
Known ae219.. : u20 = u7 ⟶ ∀ x0 : ο . x0
Known 54bdc.. : u20 = u8 ⟶ ∀ x0 : ο . x0
Known 6bb84.. : u20 = u9 ⟶ ∀ x0 : ο . x0
Known 8b01c.. : u20 = u10 ⟶ ∀ x0 : ο . x0
Known 66622.. : u20 = u11 ⟶ ∀ x0 : ο . x0
Known 01bb6.. : u20 = u12 ⟶ ∀ x0 : ο . x0
Known 551bd.. : u20 = u13 ⟶ ∀ x0 : ο . x0
Known 28d21.. : u20 = u14 ⟶ ∀ x0 : ο . x0
Known bf7ce.. : u20 = u15 ⟶ ∀ x0 : ο . x0
Known 996e8.. : u20 = u16 ⟶ ∀ x0 : ο . x0
Known 9ce5b.. : u20 = u17 ⟶ ∀ x0 : ο . x0
Known 75fad.. : u20 = u18 ⟶ ∀ x0 : ο . x0
Known 2615b.. : u20 = u19 ⟶ ∀ x0 : ο . x0
Theorem 67f22.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u20 = x20 (proof)
Known 1158c.. : u21 = 0 ⟶ ∀ x0 : ο . x0
Known db0cd.. : u21 = u1 ⟶ ∀ x0 : ο . x0
Known ebee4.. : u21 = u2 ⟶ ∀ x0 : ο . x0
Known 272ed.. : u21 = u3 ⟶ ∀ x0 : ο . x0
Known ac7ac.. : u21 = u4 ⟶ ∀ x0 : ο . x0
Known 18fbb.. : u21 = u5 ⟶ ∀ x0 : ο . x0
Known 2ec13.. : u21 = u6 ⟶ ∀ x0 : ο . x0
Known 471c9.. : u21 = u7 ⟶ ∀ x0 : ο . x0
Known ada11.. : u21 = u8 ⟶ ∀ x0 : ο . x0
Known f159f.. : u21 = u9 ⟶ ∀ x0 : ο . x0
Known b1234.. : u21 = u10 ⟶ ∀ x0 : ο . x0
Known 4c4e0.. : u21 = u11 ⟶ ∀ x0 : ο . x0
Known 6371d.. : u21 = u12 ⟶ ∀ x0 : ο . x0
Known 87a9a.. : u21 = u13 ⟶ ∀ x0 : ο . x0
Known 25d09.. : u21 = u14 ⟶ ∀ x0 : ο . x0
Known 17bc6.. : u21 = u15 ⟶ ∀ x0 : ο . x0
Known 39009.. : u21 = u16 ⟶ ∀ x0 : ο . x0
Known b821e.. : u21 = u17 ⟶ ∀ x0 : ο . x0
Known 80a82.. : u21 = u18 ⟶ ∀ x0 : ο . x0
Known 44711.. : u21 = u19 ⟶ ∀ x0 : ο . x0
Known 32e25.. : u21 = u20 ⟶ ∀ x0 : ο . x0
Known betabeta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Theorem 34154.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . ap (lam 22 (λ x23 . If_i (x23 = 0) x0 (If_i (x23 = 1) x1 (If_i (x23 = 2) x2 (If_i (x23 = 3) x3 (If_i (x23 = 4) x4 (If_i (x23 = 5) x5 (If_i (x23 = 6) x6 (If_i (x23 = 7) x7 (If_i (x23 = 8) x8 (If_i (x23 = 9) x9 (If_i (x23 = 10) x10 (If_i (x23 = 11) x11 (If_i (x23 = 12) x12 (If_i (x23 = 13) x13 (If_i (x23 = 14) x14 (If_i (x23 = 15) x15 (If_i (x23 = 16) x16 (If_i (x23 = 17) x17 (If_i (x23 = 18) x18 (If_i (x23 = 19) x19 (If_i (x23 = 20) x20 x21)))))))))))))))))))))) u21 = x21 (proof)
Definition 55574.. := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (lam 22 (λ x23 . If_i (x23 = 0) x1 (If_i (x23 = 1) x2 (If_i (x23 = 2) x3 (If_i (x23 = 3) x4 (If_i (x23 = 4) x5 (If_i (x23 = 5) x6 (If_i (x23 = 6) x7 (If_i (x23 = 7) x8 (If_i (x23 = 8) x9 (If_i (x23 = 9) x10 (If_i (x23 = 10) x11 (If_i (x23 = 11) x12 (If_i (x23 = 12) x13 (If_i (x23 = 13) x14 (If_i (x23 = 14) x15 (If_i (x23 = 15) x16 (If_i (x23 = 16) x17 (If_i (x23 = 17) x18 (If_i (x23 = 18) x19 (If_i (x23 = 19) x20 (If_i (x23 = 20) x21 x22)))))))))))))))))))))) x0
Theorem 1435b.. : 55574.. u19 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x20 (proof)
Theorem 54789.. : 55574.. u20 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x21 (proof)
Theorem 667cd.. : 55574.. u21 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x22 (proof)