Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr8bR../ccf6a..
PUYRB../083eb..
vout
Pr8bR../cd4c6.. 0.00 bars
TMXLS../60711.. ownership of 3f795.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUXq../dc041.. ownership of 6306c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVwQ../83646.. ownership of f7eb7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKX2../95a5a.. ownership of 0f17e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZXy../49847.. ownership of 04306.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZp3../a35ca.. ownership of ee14b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHmF../f52dc.. ownership of d4b7b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVzT../e999e.. ownership of e374f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFAC../f545b.. ownership of 570dd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc2z../eb475.. ownership of e5b95.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUULb../4d9d7.. doc published by PrGxv..
Param binunionbinunion : ιιι
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known binunionEbinunionE : ∀ x0 x1 x2 . x2binunion x0 x1or (x2x0) (x2x1)
Theorem binunionE'binunionE : ∀ x0 x1 x2 . ∀ x3 : ο . (x2x0x3)(x2x1x3)x2binunion x0 x1x3 (proof)
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Theorem ReplE'ReplE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . (∀ x3 . x3x0x2 (x1 x3))∀ x3 . x3prim5 x0 x1x2 x3 (proof)
Theorem 04306.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 : ι → ο . (∀ x5 . x5x0x4 (x2 x5))(∀ x5 . x5x1x4 (x3 x5))∀ x5 . x5binunion (prim5 x0 x2) (prim5 x1 x3)x4 x5 (proof)
Param SNoSNo : ιο
Param SNoLevSNoLev : ιι
Param ordsuccordsucc : ιι
Param SNoLtSNoLt : ιιο
Param SNo_extend0SNo_extend0 : ιι
Param SNoLeSNoLe : ιιο
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 x0)
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Param binintersectbinintersect : ιιι
Param SNoEq_SNoEq_ : ιιιο
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known SNoLtESNoLtE : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 x1∀ x2 : ο . (∀ x3 . SNo x3SNoLev x3binintersect (SNoLev x0) (SNoLev x1)SNoEq_ (SNoLev x3) x3 x0SNoEq_ (SNoLev x3) x3 x1SNoLt x0 x3SNoLt x3 x1nIn (SNoLev x3) x0SNoLev x3x1x2)(SNoLev x0SNoLev x1SNoEq_ (SNoLev x0) x0 x1SNoLev x0x1x2)(SNoLev x1SNoLev x0SNoEq_ (SNoLev x1) x0 x1nIn (SNoLev x1) x0x2)x2
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known SNoLt_traSNoLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLt x1 x2SNoLt x0 x2
Known SNo_extend0_SNoSNo_extend0_SNo : ∀ x0 . SNo x0SNo (SNo_extend0 x0)
Known SNoLtI2SNoLtI2 : ∀ x0 x1 . SNoLev x0SNoLev x1SNoEq_ (SNoLev x0) x0 x1SNoLev x0x1SNoLt x0 x1
Known SNo_extend0_SNoLevSNo_extend0_SNoLev : ∀ x0 . SNo x0SNoLev (SNo_extend0 x0) = ordsucc (SNoLev x0)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known SNoEq_tra_SNoEq_tra_ : ∀ x0 x1 x2 x3 . SNoEq_ x0 x1 x2SNoEq_ x0 x2 x3SNoEq_ x0 x1 x3
Param ordinalordinal : ιο
Known SNoEq_antimon_SNoEq_antimon_ : ∀ x0 . ordinal x0∀ x1 . x1x0∀ x2 x3 . SNoEq_ x0 x2 x3SNoEq_ x1 x2 x3
Known SNoLev_ordinalSNoLev_ordinal : ∀ x0 . SNo x0ordinal (SNoLev x0)
Known SNoEq_sym_SNoEq_sym_ : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2SNoEq_ x0 x2 x1
Known SNo_extend0_SNoEqSNo_extend0_SNoEq : ∀ x0 . SNo x0SNoEq_ (SNoLev x0) (SNo_extend0 x0) x0
Known SNoEq_E2SNoEq_E2 : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2∀ x3 . x3x0x3x2x3x1
Known binintersectE2binintersectE2 : ∀ x0 x1 x2 . x2binintersect x0 x1x2x1
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Theorem f7eb7.. : ∀ x0 x1 . SNo x0SNo x1SNoLev x1ordsucc (SNoLev x0)SNoLt (SNo_extend0 x0) x1SNoLe x0 x1 (proof)
Param SNo_extend1SNo_extend1 : ιι
Known SNo_extend1_SNoSNo_extend1_SNo : ∀ x0 . SNo x0SNo (SNo_extend1 x0)
Known SNoLtI3SNoLtI3 : ∀ x0 x1 . SNoLev x1SNoLev x0SNoEq_ (SNoLev x1) x0 x1nIn (SNoLev x1) x0SNoLt x0 x1
Known SNo_extend1_SNoLevSNo_extend1_SNoLev : ∀ x0 . SNo x0SNoLev (SNo_extend1 x0) = ordsucc (SNoLev x0)
Known SNo_extend1_SNoEqSNo_extend1_SNoEq : ∀ x0 . SNo x0SNoEq_ (SNoLev x0) (SNo_extend1 x0) x0
Known SNoEq_E1SNoEq_E1 : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2∀ x3 . x3x0x3x1x3x2
Known binintersectE1binintersectE1 : ∀ x0 x1 x2 . x2binintersect x0 x1x2x0
Theorem 3f795.. : ∀ x0 x1 . SNo x0SNo x1SNoLev x1ordsucc (SNoLev x0)SNoLt x1 (SNo_extend1 x0)SNoLe x1 x0 (proof)