Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrJAV../6c72b..
PUSzm../e871f..
vout
PrJAV../04eae.. 6.42 bars
TMGsD../0f92e.. ownership of d1fff.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMYf3../1b216.. ownership of e5cae.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMUGZ../eafa2.. ownership of b67a3.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMb5P../ff3a4.. ownership of e1594.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMUjL../a11b2.. ownership of ad6f9.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLLQ../8df2f.. ownership of 395b7.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMQhw../03f25.. ownership of f460f.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMd7F../18d32.. ownership of 7d1b5.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMGSK../f3e4a.. ownership of 4bf57.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMG6X../77e7a.. ownership of d9462.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMRrX../96cb5.. ownership of 8ea4a.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMRSZ../3d756.. ownership of 218e4.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMFCx../64c52.. ownership of acb62.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMXSQ../20483.. ownership of d9a12.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMWuS../ccd66.. ownership of c2320.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMLpp../8c62d.. ownership of 428b3.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMF8Q../3cf36.. ownership of d4afb.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
TMJyF../42ee8.. ownership of 9ecfc.. as prop with payaddr Pr6Pc.. rights free controlledby Pr6Pc.. upto 0
PUYBq../4f68a.. doc published by Pr6Pc..
Param add_SNoadd_SNo : ιιι
Param mul_SNomul_SNo : ιιι
Param minus_SNominus_SNo : ιι
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known mul_SNo_Subq_lemmul_SNo_Subq_lem : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . (∀ x8 . x8x6∀ x9 : ο . (∀ x10 . x10x2∀ x11 . x11x3x8 = add_SNo (mul_SNo x10 x1) (add_SNo (mul_SNo x0 x11) (minus_SNo (mul_SNo x10 x11)))x9)(∀ x10 . x10x4∀ x11 . x11x5x8 = add_SNo (mul_SNo x10 x1) (add_SNo (mul_SNo x0 x11) (minus_SNo (mul_SNo x10 x11)))x9)x9)(∀ x8 . x8x2∀ x9 . x9x3add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9)))x7)(∀ x8 . x8x4∀ x9 . x9x5add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9)))x7)x6x7
Param SNoSNo : ιο
Param SNoLtSNoLt : ιιο
Known add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0
Known add_SNo_Lt1_canceladd_SNo_Lt1_cancel : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt (add_SNo x0 x1) (add_SNo x2 x1)SNoLt x0 x2
Theorem add_SNo_Lt2_canceladd_SNo_Lt2_cancel : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt (add_SNo x0 x1) (add_SNo x0 x2)SNoLt x1 x2 (proof)
Param SNoLSNoL : ιι
Param SNoRSNoR : ιι
Known mul_SNo_prop_1mul_SNo_prop_1 : ∀ x0 . SNo x0∀ x1 . SNo x1∀ x2 : ο . (SNo (mul_SNo x0 x1)(∀ x3 . x3SNoL x0∀ x4 . x4SNoL x1SNoLt (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)))(∀ x3 . x3SNoR x0∀ x4 . x4SNoR x1SNoLt (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)))(∀ x3 . x3SNoL x0∀ x4 . x4SNoR x1SNoLt (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)) (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)))(∀ x3 . x3SNoR x0∀ x4 . x4SNoL x1SNoLt (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)) (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)))x2)x2
Param SNoLevSNoLev : ιι
Param binintersectbinintersect : ιιι
Param SNoEq_SNoEq_ : ιιιο
Param nInnIn : ιιο
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
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known binintersectEbinintersectE : ∀ x0 x1 x2 . x2binintersect x0 x1and (x2x0) (x2x1)
Known SNoLt_traSNoLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLt x1 x2SNoLt x0 x2
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Known add_SNo_com_4_inner_midadd_SNo_com_4_inner_mid : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3add_SNo (add_SNo x0 x1) (add_SNo x2 x3) = add_SNo (add_SNo x0 x2) (add_SNo x1 x3)
Known add_SNo_Lt3add_SNo_Lt3 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt x0 x2SNoLt x1 x3SNoLt (add_SNo x0 x1) (add_SNo x2 x3)
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Known SNoR_ISNoR_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x1SNoR x0
Known SNoL_ISNoL_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x1SNoL x0
Known add_SNo_com_3_0_1add_SNo_com_3_0_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo x1 (add_SNo x0 x2)
Known add_SNo_Lt2add_SNo_Lt2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x1 x2SNoLt (add_SNo x0 x1) (add_SNo x0 x2)
Known add_SNo_assocadd_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2
Known add_SNo_Lt1add_SNo_Lt1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x2SNoLt (add_SNo x0 x1) (add_SNo x2 x1)
Known add_SNo_rotate_3_1add_SNo_rotate_3_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo x2 (add_SNo x0 x1)
Theorem mul_SNo_Ltmul_SNo_Lt : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt x2 x0SNoLt x3 x1SNoLt (add_SNo (mul_SNo x2 x1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 x1) (mul_SNo x2 x3)) (proof)
Param SNoLeSNoLe : ιιο
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known SNoLeESNoLeE : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 x1or (SNoLt x0 x1) (x0 = x1)
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known SNoLe_refSNoLe_ref : ∀ x0 . SNoLe x0 x0
Theorem mul_SNo_Lemul_SNo_Le : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLe x2 x0SNoLe x3 x1SNoLe (add_SNo (mul_SNo x2 x1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 x1) (mul_SNo x2 x3)) (proof)
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Known add_SNo_minus_Lt1badd_SNo_minus_Lt1b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 (add_SNo x2 x1)SNoLt (add_SNo x0 (minus_SNo x1)) x2
Theorem add_SNo_minus_Lt1b3add_SNo_minus_Lt1b3 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt (add_SNo x0 x1) (add_SNo x3 x2)SNoLt (add_SNo x0 (add_SNo x1 (minus_SNo x2))) x3 (proof)
Known add_SNo_minus_Lt2badd_SNo_minus_Lt2b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt (add_SNo x2 x1) x0SNoLt x2 (add_SNo x0 (minus_SNo x1))
Theorem add_SNo_minus_Lt2b3add_SNo_minus_Lt2b3 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt (add_SNo x3 x2) (add_SNo x0 x1)SNoLt x3 (add_SNo x0 (add_SNo x1 (minus_SNo x2))) (proof)
Known SNoL_ESNoL_E : ∀ x0 . SNo x0∀ x1 . x1SNoL x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x2)x2
Param SNoS_SNoS_ : ιι
Known SNoLev_indSNoLev_ind : ∀ x0 : ι → ο . (∀ x1 . SNo x1(∀ x2 . x2SNoS_ (SNoLev x1)x0 x2)x0 x1)∀ x1 . SNo x1x0 x1
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known SNoLtLe_traSNoLtLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLe x1 x2SNoLt x0 x2
Param SNoCutPSNoCutP : ιιο
Param SNoCutSNoCut : ιιι
Known mul_SNo_eq_3mul_SNo_eq_3 : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (∀ x3 x4 . SNoCutP x3 x4(∀ x5 . x5x3∀ x6 : ο . (∀ x7 . x7SNoL x0∀ x8 . x8SNoL x1x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8)))x6)(∀ x7 . x7SNoR x0∀ x8 . x8SNoR x1x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8)))x6)x6)(∀ x5 . x5SNoL x0∀ x6 . x6SNoL x1add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x3)(∀ x5 . x5SNoR x0∀ x6 . x6SNoR x1add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x3)(∀ x5 . x5x4∀ x6 : ο . (∀ x7 . x7SNoL x0∀ x8 . x8SNoR x1x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8)))x6)(∀ x7 . x7SNoR x0∀ x8 . x8SNoL x1x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8)))x6)x6)(∀ x5 . x5SNoL x0∀ x6 . x6SNoR x1add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x4)(∀ x5 . x5SNoR x0∀ x6 . x6SNoL x1add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6)))x4)mul_SNo x0 x1 = SNoCut x3 x4x2)x2
Known SNo_etaSNo_eta : ∀ x0 . SNo x0x0 = SNoCut (SNoL x0) (SNoR x0)
Known SNoCut_LeSNoCut_Le : ∀ x0 x1 x2 x3 . SNoCutP x0 x1SNoCutP x2 x3(∀ x4 . x4x0SNoLt x4 (SNoCut x2 x3))(∀ x4 . x4x3SNoLt (SNoCut x0 x1) x4)SNoLe (SNoCut x0 x1) (SNoCut x2 x3)
Known SNoCutP_SNoL_SNoRSNoCutP_SNoL_SNoR : ∀ x0 . SNo x0SNoCutP (SNoL x0) (SNoR x0)
Known SNoR_ESNoR_E : ∀ x0 . SNo x0∀ x1 . x1SNoR x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x2)x2
Known SNoLt_trichotomy_or_impredSNoLt_trichotomy_or_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (SNoLt x0 x1x2)(x0 = x1x2)(SNoLt x1 x0x2)x2
Known SNoLeLt_traSNoLeLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 x2SNoLt x0 x2
Known SNoS_I2SNoS_I2 : ∀ x0 x1 . SNo x0SNo x1SNoLev x0SNoLev x1x0SNoS_ (SNoLev x1)
Param ordinalordinal : ιο
Definition TransSetTransSet := λ x0 . ∀ x1 . x1x0x1x0
Known ordinal_TransSetordinal_TransSet : ∀ x0 . ordinal x0TransSet x0
Known SNoLev_ordinalSNoLev_ordinal : ∀ x0 . SNo x0ordinal (SNoLev x0)
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 x0)
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Theorem mul_SNo_SNoL_interpolatemul_SNo_SNoL_interpolate : ∀ x0 x1 . SNo x0SNo x1∀ x2 . x2SNoL (mul_SNo x0 x1)or (∀ x3 : ο . (∀ x4 . and (x4SNoL x0) (∀ x5 : ο . (∀ x6 . and (x6SNoL x1) (SNoLe (add_SNo x2 (mul_SNo x4 x6)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x6)))x5)x5)x3)x3) (∀ x3 : ο . (∀ x4 . and (x4SNoR x0) (∀ x5 : ο . (∀ x6 . and (x6SNoR x1) (SNoLe (add_SNo x2 (mul_SNo x4 x6)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x6)))x5)x5)x3)x3) (proof)
Theorem mul_SNo_SNoL_interpolate_impredmul_SNo_SNoL_interpolate_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 . x2SNoL (mul_SNo x0 x1)∀ x3 : ο . (∀ x4 . x4SNoL x0∀ x5 . x5SNoL x1SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5))x3)(∀ x4 . x4SNoR x0∀ x5 . x5SNoR x1SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5))x3)x3 (proof)
Theorem mul_SNo_SNoR_interpolatemul_SNo_SNoR_interpolate : ∀ x0 x1 . SNo x0SNo x1∀ x2 . x2SNoR (mul_SNo x0 x1)or (∀ x3 : ο . (∀ x4 . and (x4SNoL x0) (∀ x5 : ο . (∀ x6 . and (x6SNoR x1) (SNoLe (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x6)) (add_SNo x2 (mul_SNo x4 x6)))x5)x5)x3)x3) (∀ x3 : ο . (∀ x4 . and (x4SNoR x0) (∀ x5 : ο . (∀ x6 . and (x6SNoL x1) (SNoLe (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x6)) (add_SNo x2 (mul_SNo x4 x6)))x5)x5)x3)x3) (proof)
Theorem mul_SNo_SNoR_interpolate_impredmul_SNo_SNoR_interpolate_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 . x2SNoR (mul_SNo x0 x1)∀ x3 : ο . (∀ x4 . x4SNoL x0∀ x5 . x5SNoR x1SNoLe (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) (add_SNo x2 (mul_SNo x4 x5))x3)(∀ x4 . x4SNoR x0∀ x5 . x5SNoL x1SNoLe (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) (add_SNo x2 (mul_SNo x4 x5))x3)x3 (proof)