Search for blocks/addresses/...

Proofgold Asset

asset id
6e2a3b1342f92f641c0f0fab781ac92bb00d73c0389235d016a9e758cf37797e
asset hash
560e5b30b51c90844683bafdd8d2551071ac14f39cfa4052332977d06ee9b2c6
bday / block
12306
tx
b890d..
preasset
doc published by PrGxv..
Param realreal : ι
Param minus_SNominus_SNo : ιι
Param SNoSNo : ιο
Param SNoLevSNoLev : ιι
Param ordsuccordsucc : ιι
Param omegaomega : ι
Param SNoS_SNoS_ : ιι
Param SNoLtSNoLt : ιιο
Param abs_SNoabs_SNo : ιι
Param add_SNoadd_SNo : ιιι
Param eps_eps_ : ιι
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known real_Ereal_E : ∀ x0 . x0real∀ x1 : ο . (SNo x0SNoLev x0ordsucc omegax0SNoS_ (ordsucc omega)SNoLt (minus_SNo omega) x0SNoLt x0 omega(∀ x2 . x2SNoS_ omega(∀ x3 . x3omegaSNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x3))x2 = x0)(∀ x2 . x2omega∀ x3 : ο . (∀ x4 . and (x4SNoS_ omega) (and (SNoLt x4 x0) (SNoLt x0 (add_SNo x4 (eps_ x2))))x3)x3)x1)x1
Known real_Ireal_I : ∀ x0 . x0SNoS_ (ordsucc omega)(x0 = omega∀ x1 : ο . x1)(x0 = minus_SNo omega∀ x1 : ο . x1)(∀ x1 . x1SNoS_ omega(∀ x2 . x2omegaSNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2))x1 = x0)x0real
Param ordinalordinal : ιο
Known minus_SNo_SNoS_minus_SNo_SNoS_ : ∀ x0 . ordinal x0∀ x1 . x1SNoS_ x0minus_SNo x1SNoS_ x0
Known ordsucc_omega_ordinalordsucc_omega_ordinal : ordinal (ordsucc omega)
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Known SNo_omegaSNo_omega : SNo omega
Known minus_SNo_prereal_1minus_SNo_prereal_1 : ∀ x0 . SNo x0(∀ x1 . x1SNoS_ omega(∀ x2 . x2omegaSNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2))x1 = x0)∀ x1 . x1SNoS_ omega(∀ x2 . x2omegaSNoLt (abs_SNo (add_SNo x1 (minus_SNo (minus_SNo x0)))) (eps_ x2))x1 = minus_SNo x0
Theorem real_minus_SNoreal_minus_SNo : ∀ x0 . x0realminus_SNo x0real (proof)
Param mul_SNomul_SNo : ιιι
Param SNo_SNo_ : ιιο
Known SNoS_E2SNoS_E2 : ∀ x0 . ordinal x0∀ x1 . x1SNoS_ x0∀ x2 : ο . (SNoLev x1x0ordinal (SNoLev x1)SNo x1SNo_ (SNoLev x1) x1x2)x2
Known SNoS_ordsucc_omega_bdd_aboveSNoS_ordsucc_omega_bdd_above : ∀ x0 . x0SNoS_ (ordsucc omega)SNoLt x0 omega∀ x1 : ο . (∀ x2 . and (x2omega) (SNoLt x0 x2)x1)x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known SNoLt_traSNoLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLt x1 x2SNoLt x0 x2
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Known SNo_eps_SNo_eps_ : ∀ x0 . x0omegaSNo (eps_ x0)
Known SNo_1SNo_1 : SNo 1
Known pos_mul_SNo_Ltpos_mul_SNo_Lt : ∀ x0 x1 x2 . SNo x0SNoLt 0 x0SNo x1SNo x2SNoLt x1 x2SNoLt (mul_SNo x0 x1) (mul_SNo x0 x2)
Known SNo_eps_posSNo_eps_pos : ∀ x0 . x0omegaSNoLt 0 (eps_ x0)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Param SNoLeSNoLe : ιιο
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 x0)
Known FalseEFalseE : False∀ x0 : ο . x0
Param exp_SNo_natexp_SNo_nat : ιιι
Known SNoLeLt_traSNoLeLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 x2SNoLt x0 x2
Known mul_SNo_oneLmul_SNo_oneL : ∀ x0 . SNo x0mul_SNo 1 x0 = x0
Param nat_pnat_p : ιο
Known mul_SNo_eps_power_2'mul_SNo_eps_power_2 : ∀ x0 . nat_p x0mul_SNo (exp_SNo_nat 2 x0) (eps_ x0) = 1
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Known mul_SNo_assocmul_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2
Known exp_SNo_2_bdexp_SNo_2_bd : ∀ x0 . nat_p x0SNoLt x0 (exp_SNo_nat 2 x0)
Known mul_SNo_oneRmul_SNo_oneR : ∀ x0 . SNo x0mul_SNo x0 1 = x0
Known nonneg_mul_SNo_Lenonneg_mul_SNo_Le : ∀ x0 x1 x2 . SNo x0SNoLe 0 x0SNo x1SNo x2SNoLe x1 x2SNoLe (mul_SNo x0 x1) (mul_SNo x0 x2)
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known exp_SNo_nat_posexp_SNo_nat_pos : ∀ x0 . SNo x0SNoLt 0 x0∀ x1 . nat_p x1SNoLt 0 (exp_SNo_nat x0 x1)
Known SNo_2SNo_2 : SNo 2
Known SNoLt_0_2SNoLt_0_2 : SNoLt 0 2
Known SNo_exp_SNo_natSNo_exp_SNo_nat : ∀ x0 . SNo x0∀ x1 . nat_p x1SNo (exp_SNo_nat x0 x1)
Known omega_SNoomega_SNo : ∀ x0 . x0omegaSNo x0
Theorem SNoS_ordsucc_omega_bdd_eps_posSNoS_ordsucc_omega_bdd_eps_pos : ∀ x0 . x0SNoS_ (ordsucc omega)SNoLt 0 x0SNoLt x0 omega∀ x1 : ο . (∀ x2 . and (x2omega) (SNoLt (mul_SNo (eps_ x2) x0) 1)x1)x1 (proof)
Known SNoLt_trichotomy_or_impredSNoLt_trichotomy_or_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (SNoLt x0 x1x2)(x0 = x1x2)(SNoLt x1 x0x2)x2
Known SNo_0SNo_0 : SNo 0
Known pos_abs_SNopos_abs_SNo : ∀ x0 . SNoLt 0 x0abs_SNo x0 = x0
Known mul_SNo_pos_posmul_SNo_pos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt 0 x1SNoLt 0 (mul_SNo x0 x1)
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known nat_0nat_0 : nat_p 0
Known mul_SNo_zeroRmul_SNo_zeroR : ∀ x0 . SNo x0mul_SNo x0 0 = 0
Known abs_SNo_0abs_SNo_0 : abs_SNo 0 = 0
Known SNoLt_0_1SNoLt_0_1 : SNoLt 0 1
Known mul_SNo_minus_distrRmul_minus_SNo_distrR : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1)
Known neg_abs_SNoneg_abs_SNo : ∀ x0 . SNo x0SNoLt x0 0abs_SNo x0 = minus_SNo x0
Known mul_SNo_pos_negmul_SNo_pos_neg : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt x1 0SNoLt (mul_SNo x0 x1) 0
Known minus_SNo_Lt_contra1minus_SNo_Lt_contra1 : ∀ x0 x1 . SNo x0SNo x1SNoLt (minus_SNo x0) x1SNoLt (minus_SNo x1) x0
Known minus_SNo_Lt_contra2minus_SNo_Lt_contra2 : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 (minus_SNo x1)SNoLt x1 (minus_SNo x0)
Known minus_SNo_0minus_SNo_0 : minus_SNo 0 = 0
Theorem a3f00.. : ∀ x0 . x0SNoS_ (ordsucc omega)SNoLt (minus_SNo omega) x0SNoLt x0 omega∀ x1 : ο . (∀ x2 . and (x2omega) (SNoLt (abs_SNo (mul_SNo (eps_ x2) x0)) 1)x1)x1 (proof)
Param mul_natmul_nat : ιιι
Known mul_nat_mul_SNomul_nat_mul_SNo : ∀ x0 . x0omega∀ x1 . x1omegamul_nat x0 x1 = mul_SNo x0 x1
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Known SNoLe_traSNoLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLe x1 x2SNoLe x0 x2
Known ordinal_SNoLev_max_2ordinal_SNoLev_max_2 : ∀ x0 . ordinal x0∀ x1 . SNo x1SNoLev x1ordsucc x0SNoLe x1 x0
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known SNoLev_0SNoLev_0 : SNoLev 0 = 0
Known nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0
Known nat_exp_SNo_natnat_exp_SNo_nat : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (exp_SNo_nat x0 x1)
Known nat_2nat_2 : nat_p 2
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known omega_SNoS_omegaomega_SNoS_omega : omegaSNoS_ omega
Known add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Known abs_SNo_minusabs_SNo_minus : ∀ x0 . SNo x0abs_SNo (minus_SNo x0) = abs_SNo x0
Theorem real_Archimedeanreal_Archimedean : ∀ x0 . x0real∀ x1 . x1realSNoLt 0 x0SNoLe 0 x1∀ x2 : ο . (∀ x3 . and (x3omega) (SNoLe x1 (mul_SNo x3 x0))x2)x2 (proof)