Proofgold Asset

Param real^real : ι
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param SNoS_^SNoS_ : ι → ι
Param omega^omega : ι
Known SNoS_omega_real^{SNoS_omega_real} : SNoS_ omega ⊆ real
Known omega_SNoS_omega^{omega_SNoS_omega} : omega ⊆ SNoS_ omega
Param nat_p^nat_p : ι → ο
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known nat_0^nat_0 : nat_p 0
Theorem real_0^real_0 : 0 ∈ real (proof)
Param ordsucc^ordsucc : ι → ι
Known nat_1^nat_1 : nat_p 1
Theorem real_1^real_1 : 1 ∈ real (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param int_alt1^int : ι
Param mul_SNo^mul_SNo : ι → ι → ι
Param eps_^eps_ : ι → ι
Definition diadic_rational_alt1_p := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (∀ x3 : ο . (∀ x4 . and (x4 ∈ int_alt1) (x0 = mul_SNo (eps_ x2) x4) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Param minus_SNo^minus_SNo : ι → ι
Known a3283..^{int_SNo_cases} : ∀ x0 : ι → ο . (∀ x1 . x1 ∈ omega ⟶ x0 x1) ⟶ (∀ x1 . x1 ∈ omega ⟶ x0 (minus_SNo x1)) ⟶ ∀ x1 . x1 ∈ int_alt1 ⟶ x0 x1
Known nonneg_diadic_rational_p_SNoS_omega^{nonneg_diadic_rational_p_SNoS_omega} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . nat_p x1 ⟶ mul_SNo (eps_ x0) x1 ∈ SNoS_ omega
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Param SNo^SNo : ι → ο
Known mul_SNo_minus_distrR^{mul_minus_SNo_distrR} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1)
Known SNo_eps_^SNo_eps_ : ∀ x0 . x0 ∈ omega ⟶ SNo (eps_ x0)
Known omega_SNo^omega_SNo : ∀ x0 . x0 ∈ omega ⟶ SNo x0
Known minus_SNo_SNoS_omega^{minus_SNo_SNoS_omega} : ∀ x0 . x0 ∈ SNoS_ omega ⟶ minus_SNo x0 ∈ SNoS_ omega
Theorem f05cb.. : ∀ x0 . diadic_rational_alt1_p x0 ⟶ x0 ∈ SNoS_ omega (proof)
Param ordinal^ordinal : ι → ο
Param SNoLev^SNoLev : ι → ι
Param SNo_^SNo_ : ι → ι → ο
Known SNoS_E2^SNoS_E2 : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ SNoS_ x0 ⟶ ∀ x2 : ο . (SNoLev x1 ∈ x0 ⟶ ordinal (SNoLev x1) ⟶ SNo x1 ⟶ SNo_ (SNoLev x1) x1 ⟶ x2) ⟶ x2
Known omega_ordinal^{omega_ordinal} : ordinal omega
Theorem 455b5.. : ∀ x0 . diadic_rational_alt1_p x0 ⟶ SNo x0 (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known eps_0_1^eps_0_1 : eps_ 0 = 1
Known mul_SNo_oneL^mul_SNo_oneL : ∀ x0 . SNo x0 ⟶ mul_SNo 1 x0 = x0
Known 0c7a0.. : ∀ x0 . x0 ∈ int_alt1 ⟶ SNo x0
Theorem a08ea.. : ∀ x0 . x0 ∈ int_alt1 ⟶ diadic_rational_alt1_p x0 (proof)
Known c3d99..^{Subq_omega_int} : omega ⊆ int_alt1
Theorem a89df.. : ∀ x0 . x0 ∈ omega ⟶ diadic_rational_alt1_p x0 (proof)
Known mul_SNo_oneR^mul_SNo_oneR : ∀ x0 . SNo x0 ⟶ mul_SNo x0 1 = x0
Theorem 5042a.. : ∀ x0 . x0 ∈ omega ⟶ diadic_rational_alt1_p (eps_ x0) (proof)
Known daaad..^{int_minus_SNo} : ∀ x0 . x0 ∈ int_alt1 ⟶ minus_SNo x0 ∈ int_alt1
Theorem 3801d.. : ∀ x0 . diadic_rational_alt1_p x0 ⟶ diadic_rational_alt1_p (minus_SNo x0) (proof)
Param add_SNo^add_SNo : ι → ι → ι
Known add_SNo_In_omega^{add_SNo_In_omega} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_SNo x0 x1 ∈ omega
Known eefdf..^int_mul_SNo : ∀ x0 . x0 ∈ int_alt1 ⟶ ∀ x1 . x1 ∈ int_alt1 ⟶ mul_SNo x0 x1 ∈ int_alt1
Known mul_SNo_eps_eps_add_SNo^{mul_SNo_eps_eps_add_SNo} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_SNo (eps_ x0) (eps_ x1) = eps_ (add_SNo x0 x1)
Known mul_SNo_com_4_inner_mid^{mul_SNo_com_4_inner_mid} : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ mul_SNo (mul_SNo x0 x1) (mul_SNo x2 x3) = mul_SNo (mul_SNo x0 x2) (mul_SNo x1 x3)
Theorem 858c0.. : ∀ x0 x1 . diadic_rational_alt1_p x0 ⟶ diadic_rational_alt1_p x1 ⟶ diadic_rational_alt1_p (mul_SNo x0 x1) (proof)
Param exp_SNo_nat^exp_SNo_nat : ι → ι → ι
Known a0aa5..^int_add_SNo : ∀ x0 . x0 ∈ int_alt1 ⟶ ∀ x1 . x1 ∈ int_alt1 ⟶ add_SNo x0 x1 ∈ int_alt1
Known mul_SNo_distrL^{mul_SNo_distrL} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo x0 (add_SNo x1 x2) = add_SNo (mul_SNo x0 x1) (mul_SNo x0 x2)
Known SNo_mul_SNo^SNo_mul_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (mul_SNo x0 x1)
Known mul_SNo_assoc^{mul_SNo_assoc} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2
Known mul_SNo_eps_power_2^{mul_SNo_eps_power_2} : ∀ x0 . nat_p x0 ⟶ mul_SNo (eps_ x0) (exp_SNo_nat 2 x0) = 1
Known nat_exp_SNo_nat^{nat_exp_SNo_nat} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (exp_SNo_nat x0 x1)
Known nat_2^nat_2 : nat_p 2
Theorem 9e46f.. : ∀ x0 x1 . diadic_rational_alt1_p x0 ⟶ diadic_rational_alt1_p x1 ⟶ diadic_rational_alt1_p (add_SNo x0 x1) (proof)