Search for blocks/addresses/...

Proofgold Asset

asset id
c7781238cd4c097838de0f1cddf4a733c3d35d1df437d519b3a6aef0cb10549a
asset hash
7bd7130594fab2b56e2532f20c47e697a3ecc9ede59978d5967911b26cf3283d
bday / block
12463
tx
ba872..
preasset
doc published by PrGxv..
Param nat_pnat_p : ιο
Param SNoSNo : ιο
Param SNoLevSNoLev : ιι
Param diadic_rational_alt1_p : ιο
Known nat_complete_indnat_complete_ind : ∀ x0 : ι → ο . (∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . nat_p x1x0 x1
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Param SNoS_SNoS_ : ιι
Param omegaomega : ι
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param SNoLeSNoLe : ιιο
Definition SNo_max_ofSNo_max_of := λ x0 x1 . and (and (x1x0) (SNo x1)) (∀ x2 . x2x0SNo x2SNoLe x2 x1)
Param SNoLSNoL : ιι
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known SNoS_omega_SNoL_max_existsSNoS_omega_SNoL_max_exists : ∀ x0 . x0SNoS_ omegaor (SNoL x0 = 0) (∀ x1 : ο . (∀ x2 . SNo_max_of (SNoL x0) x2x1)x1)
Known FalseEFalseE : False∀ x0 : ο . x0
Param minus_SNominus_SNo : ιι
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Known 3801d.. : ∀ x0 . diadic_rational_alt1_p x0diadic_rational_alt1_p (minus_SNo x0)
Known minus_SNo_Levminus_SNo_Lev : ∀ x0 . SNo x0SNoLev (minus_SNo x0) = SNoLev x0
Param ordinalordinal : ιο
Known ordinal_SNoLevordinal_SNoLev : ∀ x0 . ordinal x0SNoLev x0 = x0
Param SNoLtSNoLt : ιιο
Known SNo_max_ordinalSNo_max_ordinal : ∀ x0 . SNo x0(∀ x1 . x1SNoS_ (SNoLev x0)SNoLt x1 x0)ordinal x0
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
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 SNoLev_ordinalSNoLev_ordinal : ∀ x0 . SNo x0ordinal (SNoLev x0)
Known SNoLt_trichotomy_or_impredSNoLt_trichotomy_or_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (SNoLt x0 x1x2)(x0 = x1x2)(SNoLt x1 x0x2)x2
Definition nInnIn := λ x0 x1 . not (x0x1)
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known SNoL_ISNoL_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x1SNoL x0
Known minus_SNo_Lt_contra1minus_SNo_Lt_contra1 : ∀ x0 x1 . SNo x0SNo x1SNoLt (minus_SNo x0) x1SNoLt (minus_SNo x1) x0
Known a89df.. : ∀ x0 . x0omegadiadic_rational_alt1_p x0
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known SNoL_ESNoL_E : ∀ x0 . SNo x0∀ x1 . x1SNoL x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x2)x2
Definition SNo_min_ofSNo_min_of := λ x0 x1 . and (and (x1x0) (SNo x1)) (∀ x2 . x2x0SNo x2SNoLe x1 x2)
Param SNoRSNoR : ιι
Known SNoS_omega_SNoR_min_existsSNoS_omega_SNoR_min_exists : ∀ x0 . x0SNoS_ omegaor (SNoR x0 = 0) (∀ x1 : ο . (∀ x2 . SNo_min_of (SNoR x0) x2x1)x1)
Known SNoR_ISNoR_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x1SNoR x0
Known SNoR_ESNoR_E : ∀ x0 . SNo x0∀ x1 . x1SNoR x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x2)x2
Param add_SNoadd_SNo : ιιι
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Known add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0
Known double_SNo_min_1double_SNo_min_1 : ∀ x0 x1 . SNo x0SNo_min_of (SNoR x0) x1∀ x2 . SNo x2SNoLt x2 x0SNoLt (add_SNo x0 x0) (add_SNo x1 x2)∀ x3 : ο . (∀ x4 . and (x4SNoL x2) (add_SNo x1 x4 = add_SNo x0 x0)x3)x3
Param mul_SNomul_SNo : ιιι
Param eps_eps_ : ιι
Param ordsuccordsucc : ιι
Known double_eps_1double_eps_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 x0 = add_SNo x1 x2x0 = mul_SNo (eps_ 1) (add_SNo x1 x2)
Known 858c0.. : ∀ x0 x1 . diadic_rational_alt1_p x0diadic_rational_alt1_p x1diadic_rational_alt1_p (mul_SNo x0 x1)
Known 5042a.. : ∀ x0 . x0omegadiadic_rational_alt1_p (eps_ x0)
Known nat_1nat_1 : nat_p 1
Known 9e46f.. : ∀ x0 x1 . diadic_rational_alt1_p x0diadic_rational_alt1_p x1diadic_rational_alt1_p (add_SNo x0 x1)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Definition TransSetTransSet := λ x0 . ∀ x1 . x1x0x1x0
Known ordinal_TransSetordinal_TransSet : ∀ x0 . ordinal x0TransSet x0
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known double_SNo_max_1double_SNo_max_1 : ∀ x0 x1 . SNo x0SNo_max_of (SNoL x0) x1∀ x2 . SNo x2SNoLt x0 x2SNoLt (add_SNo x1 x2) (add_SNo x0 x0)∀ x3 : ο . (∀ x4 . and (x4SNoR x2) (add_SNo x1 x4 = add_SNo x0 x0)x3)x3
Known SNoS_ISNoS_I : ∀ x0 . ordinal x0∀ x1 x2 . x2x0SNo_ x2 x1x1SNoS_ x0
Known omega_ordinalomega_ordinal : ordinal omega
Known SNoLev_SNoLev_ : ∀ x0 . SNo x0SNo_ (SNoLev x0) x0
Theorem b9dc3.. : ∀ x0 . nat_p x0∀ x1 . SNo x1SNoLev x1 = x0diadic_rational_alt1_p x1 (proof)
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Theorem 5c296.. : ∀ x0 . x0SNoS_ omegadiadic_rational_alt1_p x0 (proof)
Known f05cb.. : ∀ x0 . diadic_rational_alt1_p x0x0SNoS_ omega
Theorem mul_SNo_SNoS_omegamul_SNo_SNoS_omega : ∀ x0 . x0SNoS_ omega∀ x1 . x1SNoS_ omegamul_SNo x0 x1SNoS_ omega (proof)
Known SNo_foilSNo_foil : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3mul_SNo (add_SNo x0 x1) (add_SNo x2 x3) = add_SNo (mul_SNo x0 x2) (add_SNo (mul_SNo x0 x3) (add_SNo (mul_SNo x1 x2) (mul_SNo x1 x3)))
Known mul_SNo_minus_minusmul_SNo_minus_minus : ∀ x0 x1 . SNo x0SNo x1mul_SNo (minus_SNo x0) (minus_SNo x1) = mul_SNo x0 x1
Known mul_SNo_minus_distrLmul_SNo_minus_distrL : ∀ x0 x1 . SNo x0SNo x1mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_SNo x0 x1)
Known mul_SNo_minus_distrRmul_minus_SNo_distrR : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1)
Theorem SNo_foil_mmSNo_foil_mm : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3mul_SNo (add_SNo x0 (minus_SNo x1)) (add_SNo x2 (minus_SNo x3)) = add_SNo (mul_SNo x0 x2) (add_SNo (minus_SNo (mul_SNo x0 x3)) (add_SNo (minus_SNo (mul_SNo x1 x2)) (mul_SNo x1 x3))) (proof)
Known SNo_add_SNo_3SNo_add_SNo_3 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNo (add_SNo x0 (add_SNo x1 x2))
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)
Theorem add_SNo_3a_2badd_SNo_3a_2b : ∀ x0 x1 x2 x3 x4 . SNo x0SNo x1SNo x2SNo x3SNo x4add_SNo (add_SNo x0 (add_SNo x1 x2)) (add_SNo x3 x4) = add_SNo (add_SNo x4 (add_SNo x1 x2)) (add_SNo x3 x0) (proof)
Param realreal : ι
Param abs_SNoabs_SNo : ιι
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
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 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
Known ordinal_trichotomy_or_impredordinal_trichotomy_or_impred : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 : ο . (x0x1x2)(x0 = x1x2)(x1x0x2)x2
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_Lt'pos_mul_SNo_Lt : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt 0 x2SNoLt x0 x1SNoLt (mul_SNo x0 x2) (mul_SNo x1 x2)
Known SNo_eps_decrSNo_eps_decr : ∀ x0 . x0omega∀ x1 . x1x0SNoLt (eps_ x0) (eps_ x1)
Param PiPi : ι(ιι) → ι
Definition setexpsetexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Param apap : ιιι
Known SNo_prereal_incr_lower_approxSNo_prereal_incr_lower_approx : ∀ x0 . SNo x0(∀ x1 . x1SNoS_ omega(∀ x2 . x2omegaSNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2))x1 = x0)(∀ x1 . x1omega∀ x2 : ο . (∀ x3 . and (x3SNoS_ omega) (and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 (eps_ x1))))x2)x2)∀ x1 : ο . (∀ x2 . and (x2setexp (SNoS_ omega) omega) (∀ x3 . x3omegaand (and (SNoLt (ap x2 x3) x0) (SNoLt x0 (add_SNo (ap x2 x3) (eps_ x3)))) (∀ x4 . x4x3SNoLt (ap x2 x4) (ap x2 x3)))x1)x1
Known SNo_prereal_decr_upper_approxSNo_prereal_decr_upper_approx : ∀ x0 . SNo x0(∀ x1 . x1SNoS_ omega(∀ x2 . x2omegaSNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2))x1 = x0)(∀ x1 . x1omega∀ x2 : ο . (∀ x3 . and (x3SNoS_ omega) (and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 (eps_ x1))))x2)x2)∀ x1 : ο . (∀ x2 . and (x2setexp (SNoS_ omega) omega) (∀ x3 . x3omegaand (and (SNoLt (add_SNo (ap x2 x3) (minus_SNo (eps_ x3))) x0) (SNoLt x0 (ap x2 x3))) (∀ x4 . x4x3SNoLt (ap x2 x3) (ap x2 x4)))x1)x1
Known SNo_approx_real_lemSNo_approx_real_lem : ∀ x0 . x0setexp (SNoS_ omega) omega∀ x1 . x1setexp (SNoS_ omega) omega(∀ x2 . x2omega∀ x3 . x3omegaSNoLt (ap x0 x2) (ap x1 x3))∀ x2 : ο . (SNoCutP (prim5 omega (ap x0)) (prim5 omega (ap x1))SNo (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1)))SNoLev (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1)))ordsucc omegaSNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1))SNoS_ (ordsucc omega)(∀ x3 . x3omegaSNoLt (ap x0 x3) (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1))))(∀ x3 . x3omegaSNoLt (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1))) (ap x1 x3))x2)x2
Known SNo_approx_realSNo_approx_real : ∀ x0 . SNo x0∀ x1 . x1setexp (SNoS_ omega) omega∀ x2 . x2setexp (SNoS_ omega) omega(∀ x3 . x3omegaSNoLt (ap x1 x3) x0)(∀ x3 . x3omegaSNoLt x0 (add_SNo (ap x1 x3) (eps_ x3)))(∀ x3 . x3omega∀ x4 . x4x3SNoLt (ap x1 x4) (ap x1 x3))(∀ x3 . x3omegaSNoLt x0 (ap x2 x3))(∀ x3 . x3omega∀ x4 . x4x3SNoLt (ap x2 x3) (ap x2 x4))x0 = SNoCut (prim5 omega (ap x1)) (prim5 omega (ap x2))x0real
Known SNoCut_extSNoCut_ext : ∀ x0 x1 x2 x3 . SNoCutP x0 x1SNoCutP x2 x3(∀ x4 . x4x0SNoLt x4 (SNoCut x2 x3))(∀ x4 . x4x1SNoLt (SNoCut x2 x3) x4)(∀ x4 . x4x2SNoLt x4 (SNoCut x0 x1))(∀ x4 . x4x3SNoLt (SNoCut x0 x1) x4)SNoCut x0 x1 = SNoCut x2 x3
Known SNoLeLt_traSNoLeLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 x2SNoLt x0 x2
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 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
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_minus_Le2add_SNo_minus_Le2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x2 (add_SNo x0 (minus_SNo x1))SNoLe (add_SNo x2 x1) 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 minus_add_SNo_distr_3minus_add_SNo_distr_3 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2minus_SNo (add_SNo x0 (add_SNo x1 x2)) = add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (minus_SNo x2))
Known mul_SNo_eps_eps_add_SNomul_SNo_eps_eps_add_SNo : ∀ x0 . x0omega∀ x1 . x1omegamul_SNo (eps_ x0) (eps_ x1) = eps_ (add_SNo x0 x1)
Known nonneg_mul_SNo_Le2nonneg_mul_SNo_Le2 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLe 0 x0SNoLe 0 x1SNoLe x0 x2SNoLe x1 x3SNoLe (mul_SNo x0 x1) (mul_SNo x2 x3)
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known SNo_eps_posSNo_eps_pos : ∀ x0 . x0omegaSNoLt 0 (eps_ x0)
Known add_SNo_In_omegaadd_SNo_In_omega : ∀ x0 . x0omega∀ x1 . x1omegaadd_SNo x0 x1omega
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)
Known add_SNo_assoc_4add_SNo_assoc_4 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3add_SNo x0 (add_SNo x1 (add_SNo x2 x3)) = add_SNo (add_SNo x0 (add_SNo x1 x2)) x3
Known add_SNo_minus_Le2badd_SNo_minus_Le2b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe (add_SNo x2 x1) x0SNoLe x2 (add_SNo x0 (minus_SNo x1))
Known add_SNo_rotate_4_1add_SNo_rotate_4_1 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3add_SNo x0 (add_SNo x1 (add_SNo x2 x3)) = add_SNo x3 (add_SNo x0 (add_SNo x1 x2))
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Known ap_Piap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2Pi x0 x1x3x0ap x2 x3x1 x3
Known SNo_prereal_incr_lower_posSNo_prereal_incr_lower_pos : ∀ x0 . SNo x0SNoLt 0 x0(∀ x1 . x1SNoS_ omega(∀ x2 . x2omegaSNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2))x1 = x0)(∀ x1 . x1omega∀ x2 : ο . (∀ x3 . and (x3SNoS_ omega) (and (SNoLt x3 x0) (SNoLt x0 (add_SNo x3 (eps_ x1))))x2)x2)∀ x1 . x1omega∀ x2 : ο . (∀ x3 . x3SNoS_ omegaSNoLt 0 x3SNoLt x3 x0SNoLt x0 (add_SNo x3 (eps_ x1))x2)x2
Known pos_mul_SNo_Lt2pos_mul_SNo_Lt2 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt 0 x0SNoLt 0 x1SNoLt x0 x2SNoLt x1 x3SNoLt (mul_SNo x0 x1) (mul_SNo x2 x3)
Known add_SNo_Lt2add_SNo_Lt2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x1 x2SNoLt (add_SNo x0 x1) (add_SNo x0 x2)
Known eps_ordsucc_half_addeps_ordsucc_half_add : ∀ x0 . nat_p x0add_SNo (eps_ (ordsucc x0)) (eps_ (ordsucc x0)) = eps_ x0
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Known add_SNo_1_ordsuccadd_SNo_1_ordsucc : ∀ x0 . x0omegaadd_SNo x0 1 = ordsucc x0
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 omega_SNoomega_SNo : ∀ x0 . x0omegaSNo x0
Known add_SNo_1_1_2add_SNo_1_1_2 : add_SNo 1 1 = 2
Known add_SNo_Lt4add_SNo_Lt4 : ∀ x0 x1 x2 x3 x4 x5 . SNo x0SNo x1SNo x2SNo x3SNo x4SNo x5SNoLt x0 x3SNoLt x1 x4SNoLt x2 x5SNoLt (add_SNo x0 (add_SNo x1 x2)) (add_SNo x3 (add_SNo x4 x5))
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 mul_SNo_Lt1_pos_Ltmul_SNo_Lt1_pos_Lt : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 1SNoLt 0 x1SNoLt (mul_SNo x0 x1) x1
Known mul_SNo_commul_SNo_com : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_SNo x1 x0
Known SNoLe_traSNoLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLe x1 x2SNoLe x0 x2
Known mul_SNo_Le1_nonneg_Lemul_SNo_Le1_nonneg_Le : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 1SNoLe 0 x1SNoLe (mul_SNo x0 x1) x1
Known mul_SNo_oneLmul_SNo_oneL : ∀ x0 . SNo x0mul_SNo 1 x0 = x0
Known eps_bd_1eps_bd_1 : ∀ x0 . x0omegaSNoLe (eps_ x0) 1
Known mul_SNo_pos_posmul_SNo_pos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt 0 x1SNoLt 0 (mul_SNo x0 x1)
Known ordinal_SNoLt_Inordinal_SNoLt_In : ∀ x0 x1 . ordinal x0ordinal x1SNoLt x0 x1x0x1
Known SNo_2SNo_2 : SNo 2
Known SNoLt_1_2SNoLt_1_2 : SNoLt 1 2
Known nat_2nat_2 : nat_p 2
Known 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
Known SNo_abs_SNoSNo_abs_SNo : ∀ x0 . SNo x0SNo (abs_SNo x0)
Known abs_SNo_dist_swapabs_SNo_dist_swap : ∀ x0 x1 . SNo x0SNo x1abs_SNo (add_SNo x0 (minus_SNo x1)) = abs_SNo (add_SNo x1 (minus_SNo x0))
Known pos_abs_SNopos_abs_SNo : ∀ x0 . SNoLt 0 x0abs_SNo x0 = x0
Known SNoLt_minus_posSNoLt_minus_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 x1SNoLt 0 (add_SNo x1 (minus_SNo x0))
Known add_SNo_Le1add_SNo_Le1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x2SNoLe (add_SNo x0 x1) (add_SNo x2 x1)
Known add_SNo_Le2add_SNo_Le2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x1 x2SNoLe (add_SNo x0 x1) (add_SNo x0 x2)
Known add_SNo_minus_SNo_prop5add_SNo_minus_SNo_prop5 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3add_SNo (add_SNo x0 (add_SNo x1 (minus_SNo x2))) (add_SNo x2 x3) = add_SNo x0 (add_SNo x1 x3)
Known add_SNo_minus_SNo_linvadd_SNo_minus_SNo_linv : ∀ x0 . SNo x0add_SNo (minus_SNo x0) x0 = 0
Known add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = x0
Known SNoLe_refSNoLe_ref : ∀ x0 . SNoLe x0 x0
Known 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
Known SNo_add_SNo_4SNo_add_SNo_4 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 x3)))
Known add_SNo_minus_SNo_prop2add_SNo_minus_SNo_prop2 : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 (add_SNo (minus_SNo x0) x1) = x1
Known add_SNo_minus_L2add_SNo_minus_L2 : ∀ x0 x1 . SNo x0SNo x1add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known omega_TransSetomega_TransSet : TransSet omega
Known nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1
Known SNoS_omega_realSNoS_omega_real : SNoS_ omegareal
Theorem real_mul_SNo_posreal_mul_SNo_pos : ∀ x0 . x0real∀ x1 . x1realSNoLt 0 x0SNoLt 0 x1mul_SNo x0 x1real (proof)
Known SNo_0SNo_0 : SNo 0
Known real_minus_SNoreal_minus_SNo : ∀ x0 . x0realminus_SNo x0real
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
Known mul_SNo_zeroRmul_SNo_zeroR : ∀ x0 . SNo x0mul_SNo x0 0 = 0
Known real_0real_0 : 0real
Known mul_SNo_zeroLmul_SNo_zeroL : ∀ x0 . SNo x0mul_SNo 0 x0 = 0
Known real_SNoreal_SNo : ∀ x0 . x0realSNo x0
Theorem real_mul_SNoreal_mul_SNo : ∀ x0 . x0real∀ x1 . x1realmul_SNo x0 x1real (proof)
Known nonneg_abs_SNononneg_abs_SNo : ∀ x0 . SNoLe 0 x0abs_SNo x0 = x0
Known add_SNo_minus_SNo_rinvadd_SNo_minus_SNo_rinv : ∀ x0 . SNo x0add_SNo x0 (minus_SNo x0) = 0
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 abs_SNo_intvl_bdabs_SNo_intvl_bd : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 (add_SNo x0 x2)SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) x2 (proof)
Known real_SNoS_omega_propreal_SNoS_omega_prop : ∀ x0 . x0real∀ x1 . x1SNoS_ omega(∀ x2 . x2omegaSNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2))x1 = x0
Theorem 73c92.. : ∀ x0 . x0SNoS_ omega(∀ x1 . x1omegaSNoLt (abs_SNo x0) (eps_ x1))x0 = 0 (proof)
Known real_1real_1 : 1real
Theorem 569c3.. : ∀ x0 . x0SNoS_ omega(∀ x1 . x1omegaSNoLt (abs_SNo (add_SNo x0 (minus_SNo 1))) (eps_ x1))x0 = 1 (proof)