Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrAAq../f62f6..
PUQHZ../9e047..
vout
PrAAq../3f7bf.. 0.00 bars
TMMje../1dfb9.. ownership of adedd.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXGd../ee931.. ownership of 8af84.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUab../50888.. ownership of eae4d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMSdx../a903f.. ownership of ff480.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMaCS../3234a.. ownership of df354.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHMR../1da9c.. ownership of d063c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJMi../4e493.. ownership of a039e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKXu../0248d.. ownership of 4755f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMW6a../e4dc8.. ownership of 6ab99.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHX7../c1306.. ownership of 872bd.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PURqB../dc015.. doc published by Pr4zB..
Param ordsuccordsucc : ι → ι
Param u19 : ι
Definition u20 := ordsucc u19
Param u1 : ι
Param u2 : ι
Param u3 : ι
Param u4 : ι
Param u5 : ι
Param u6 : ι
Param u7 : ι
Param u8 : ι
Param u9 : ι
Param u10 : ι
Param u11 : ι
Param u12 : ι
Param u13 : ι
Param u14 : ι
Param u15 : ι
Param u16 : ι
Param u17 : ι
Param u18 : ι
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known ordsuccEordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known 27a71.. : ∀ x0 . x0 ∈ u19 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 u17 ⟶ x1 u18 ⟶ x1 x0
Theorem 6ab99.. : ∀ x0 . x0 ∈ u20 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 u17 ⟶ x1 u18 ⟶ x1 u19 ⟶ x1 x0 (proof)
Definition u21 := ordsucc u20
Theorem a039e.. : ∀ x0 . x0 ∈ u21 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 u17 ⟶ x1 u18 ⟶ x1 u19 ⟶ x1 u20 ⟶ x1 x0 (proof)
Definition u22 := ordsucc u21
Theorem df354.. : ∀ x0 . x0 ∈ u22 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 u17 ⟶ x1 u18 ⟶ x1 u19 ⟶ x1 u20 ⟶ x1 u21 ⟶ x1 x0 (proof)
Definition u23 := ordsucc u22
Theorem eae4d.. : ∀ x0 . x0 ∈ u23 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 u17 ⟶ x1 u18 ⟶ x1 u19 ⟶ x1 u20 ⟶ x1 u21 ⟶ x1 u22 ⟶ x1 x0 (proof)
Definition u24 := ordsucc u23
Theorem adedd.. : ∀ x0 . x0 ∈ u24 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 u17 ⟶ x1 u18 ⟶ x1 u19 ⟶ x1 u20 ⟶ x1 u21 ⟶ x1 u22 ⟶ x1 u23 ⟶ x1 x0 (proof)