Search for blocks/addresses/...

Proofgold Address

address
PUMGCash89FMSxHFVDu1BS3BHttu1vp34aK
total
0
mg
-
conjpub
-
current assets
04d20../13491.. bday: 27765 doc published by PrQUS..
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param SNoSNo : ιο
Param SNoLtSNoLt : ιιο
Definition SNoCutPSNoCutP := λ x0 x1 . and (and (∀ x2 . x2x0SNo x2) (∀ x2 . x2x1SNo x2)) (∀ x2 . x2x0∀ x3 . x3x1SNoLt x2 x3)
Param SNoCutSNoCut : ιιι
Param SNoLSNoL : ιι
Param mul_SNomul_SNo : ιιι
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Param SNoLeSNoLe : ιιο
Param add_SNoadd_SNo : ιιι
Param SNoLevSNoLev : ιι
Param ordsuccordsucc : ιι
Param binunionbinunion : ιιι
Param famunionfamunion : ι(ιι) → ι
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param SNoEq_SNoEq_ : ιιιο
Known SNoCutP_SNoCut_impredSNoCutP_SNoCut_impred : ∀ x0 x1 . SNoCutP x0 x1∀ x2 : ο . (SNo (SNoCut x0 x1)SNoLev (SNoCut x0 x1)ordsucc (binunion (famunion x0 (λ x3 . ordsucc (SNoLev x3))) (famunion x1 (λ x3 . ordsucc (SNoLev x3))))(∀ x3 . x3x0SNoLt x3 (SNoCut x0 x1))(∀ x3 . x3x1SNoLt (SNoCut x0 x1) x3)(∀ x3 . SNo x3(∀ x4 . x4x0SNoLt x4 x3)(∀ x4 . x4x1SNoLt x3 x4)and (SNoLev (SNoCut x0 x1)SNoLev x3) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x3))x2)x2
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 minus_SNominus_SNo : ιι
Known mul_SNoCut_absmul_SNoCut_abs : ∀ x0 x1 x2 x3 x4 x5 . SNoCutP x0 x1SNoCutP x2 x3x4 = SNoCut x0 x1x5 = SNoCut x2 x3∀ x6 : ο . (∀ x7 x8 x9 x10 . (∀ x11 . x11x7∀ x12 : ο . (∀ x13 . x13x0∀ x14 . x14x2SNo x13SNo x14SNoLt x13 x4SNoLt x14 x5x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14)))x12)x12)(∀ x11 . x11x0∀ x12 . x12x2add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12)))x7)(∀ x11 . x11x8∀ x12 : ο . (∀ x13 . x13x1∀ x14 . x14x3SNo x13SNo x14SNoLt x4 x13SNoLt x5 x14x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14)))x12)x12)(∀ x11 . x11x1∀ x12 . x12x3add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12)))x8)(∀ x11 . x11x9∀ x12 : ο . (∀ x13 . x13x0∀ x14 . x14x3SNo x13SNo x14SNoLt x13 x4SNoLt x5 x14x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14)))x12)x12)(∀ x11 . x11x0∀ x12 . x12x3add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12)))x9)(∀ x11 . x11x10∀ x12 : ο . (∀ x13 . x13x1∀ x14 . x14x2SNo x13SNo x14SNoLt x4 x13SNoLt x14 x5x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14)))x12)x12)(∀ x11 . x11x1∀ x12 . x12x2add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12)))x10)SNoCutP (binunion x7 x8) (binunion x9 x10)mul_SNo x4 x5 = SNoCut (binunion x7 x8) (binunion x9 x10)x6)x6
Param SNoRSNoR : ιι
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 binunionE'binunionE : ∀ x0 x1 x2 . ∀ x3 : ο . (x2x0x3)(x2x1x3)x2binunion x0 x1x3
Known 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
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 x0)
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
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 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 FalseEFalseE : False∀ x0 : ο . x0
Known SNoLt_traSNoLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLt x1 x2SNoLt x0 x2
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
Known SNoLeLt_traSNoLeLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 x2SNoLt x0 x2
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Theorem mul_SNo_SNoCut_SNoL_interpolatemul_SNo_SNoCut_SNoL_interpolate : ∀ x0 x1 x2 x3 . SNoCutP x0 x1SNoCutP x2 x3∀ x4 x5 . x4 = SNoCut x0 x1x5 = SNoCut x2 x3∀ x6 . x6SNoL (mul_SNo x4 x5)or (∀ x7 : ο . (∀ x8 . and (x8x0) (∀ x9 : ο . (∀ x10 . and (x10x2) (SNoLe (add_SNo x6 (mul_SNo x8 x10)) (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x10)))x9)x9)x7)x7) (∀ x7 : ο . (∀ x8 . and (x8x1) (∀ x9 : ο . (∀ x10 . and (x10x3) (SNoLe (add_SNo x6 (mul_SNo x8 x10)) (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x10)))x9)x9)x7)x7) (proof)
Theorem mul_SNo_SNoCut_SNoL_interpolate_impredmul_SNo_SNoCut_SNoL_interpolate_impred : ∀ x0 x1 x2 x3 . SNoCutP x0 x1SNoCutP x2 x3∀ x4 x5 . x4 = SNoCut x0 x1x5 = SNoCut x2 x3∀ x6 . x6SNoL (mul_SNo x4 x5)∀ x7 : ο . (∀ x8 . x8x0∀ x9 . x9x2SNoLe (add_SNo x6 (mul_SNo x8 x9)) (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x9))x7)(∀ x8 . x8x1∀ x9 . x9x3SNoLe (add_SNo x6 (mul_SNo x8 x9)) (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x9))x7)x7 (proof)
Known 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)))
Theorem mul_SNo_SNoCut_SNoR_interpolatemul_SNo_SNoCut_SNoR_interpolate : ∀ x0 x1 x2 x3 . SNoCutP x0 x1SNoCutP x2 x3∀ x4 x5 . x4 = SNoCut x0 x1x5 = SNoCut x2 x3∀ x6 . x6SNoR (mul_SNo x4 x5)or (∀ x7 : ο . (∀ x8 . and (x8x0) (∀ x9 : ο . (∀ x10 . and (x10x3) (SNoLe (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x10)) (add_SNo x6 (mul_SNo x8 x10)))x9)x9)x7)x7) (∀ x7 : ο . (∀ x8 . and (x8x1) (∀ x9 : ο . (∀ x10 . and (x10x2) (SNoLe (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x10)) (add_SNo x6 (mul_SNo x8 x10)))x9)x9)x7)x7) (proof)
Theorem mul_SNo_SNoCut_SNoR_interpolate_impredmul_SNo_SNoCut_SNoR_interpolate_impred : ∀ x0 x1 x2 x3 . SNoCutP x0 x1SNoCutP x2 x3∀ x4 x5 . x4 = SNoCut x0 x1x5 = SNoCut x2 x3∀ x6 . x6SNoR (mul_SNo x4 x5)∀ x7 : ο . (∀ x8 . x8x0∀ x9 . x9x3SNoLe (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x9)) (add_SNo x6 (mul_SNo x8 x9))x7)(∀ x8 . x8x1∀ x9 . x9x2SNoLe (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x9)) (add_SNo x6 (mul_SNo x8 x9))x7)x7 (proof)

previous assets