Proofgold Asset

Param ordinal^ordinal : ι → ο
Param ordsucc^ordsucc : ι → ι
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Param nat_p^nat_p : ι → ο
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known nat_1^nat_1 : nat_p 1
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Known neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0
Known ordinal_Empty^{ordinal_Empty} : ordinal 0
Param SNo^SNo : ι → ο
Param SNoCut^SNoCut : ι → ι → ι
Param SNoLt^SNoLt : ι → ι → ο
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param Subq^Subq : ι → ι → ο
Param SNoLev^SNoLev : ι → ι
Param iff^iff : ο → ο → ο
Definition PNoEq_^PNoEq_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 . x3 ∈ x0 ⟶ iff (x1 x3) (x2 x3)
Definition SNoEq_^SNoEq_ := λ x0 x1 x2 . PNoEq_ x0 (λ x3 . x3 ∈ x1) (λ x3 . x3 ∈ x2)
Param minus_SNo^minus_SNo : ι → ι
Known SNoCut_0_0^SNoCut_0_0 : SNoCut 0 0 = 0
Known minus_SNo_Lt_contra1^{minus_SNo_Lt_contra1} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLt (minus_SNo x0) x1 ⟶ SNoLt (minus_SNo x1) x0
Known SNo_0^SNo_0 : SNo 0
Known SNo_1^SNo_1 : SNo 1
Known minus_SNo_0^minus_SNo_0 : minus_SNo 0 = 0
Known SNoLt_0_1^SNoLt_0_1 : SNoLt 0 1
Known SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Known SNoLev_0^SNoLev_0 : SNoLev 0 = 0
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known Subq_Empty^Subq_Empty : ∀ x0 . 0 ⊆ x0
Theorem 74d4d.. : (∀ x0 x1 x2 x3 x4 . (∀ x5 . x5 ∈ x1 ⟶ SNo x5) ⟶ SNo (SNoCut x0 x1) ⟶ (∀ x5 . x5 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x5) ⟶ (∀ x5 . SNo x5 ⟶ (∀ x6 . x6 ∈ x0 ⟶ SNoLt x6 x5) ⟶ (∀ x6 . x6 ∈ x1 ⟶ SNoLt x5 x6) ⟶ and (SNoLev (SNoCut x0 x1) ⊆ SNoLev x5) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x5)) ⟶ SNo x4 ⟶ SNoLt x4 (SNoCut x0 x1) ⟶ (∀ x5 . x5 ∈ x0 ⟶ SNoLt x5 x4) ⟶ not (∀ x5 . x5 ∈ x1 ⟶ SNoLt x4 x5)) ⟶ ∀ x0 : ο . x0 (proof)
Param eps_^eps_ : ι → ι
Known eps_0_1^eps_0_1 : eps_ 0 = 1
Known In_0_1^In_0_1 : 0 ∈ 1
Theorem 4edd6.. : (∀ x0 x1 x2 . SNoLt 0 x1 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLev x2 ∈ eps_ x0 ⟶ x2 = 0 ⟶ ∀ x3 : ο . x3) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4edd6.. : (∀ x0 x1 x2 . SNoLt 0 x1 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLev x2 ∈ eps_ x0 ⟶ x2 = 0 ⟶ ∀ x3 : ο . x3) ⟶ ∀ x0 : ο . x0 (proof)
Param SNo_^SNo_ : ι → ι → ο
Known minus_SNo_Lev^{minus_SNo_Lev} : ∀ x0 . SNo x0 ⟶ SNoLev (minus_SNo x0) = SNoLev x0
Known ordinal_SNoLev^{ordinal_SNoLev} : ∀ x0 . ordinal x0 ⟶ SNoLev x0 = x0
Known minus_SNo_SNo_^{minus_SNo_SNo_} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . SNo_ x0 x1 ⟶ SNo_ x0 (minus_SNo x1)
Known ordinal_SNo_^ordinal_SNo_ : ∀ x0 . ordinal x0 ⟶ SNo_ x0 x0
Theorem 90290.. : (∀ x0 x1 x2 . SNoLt x1 x0 ⟶ SNo_ x2 x1 ⟶ ordinal x2 ⟶ SNo x1 ⟶ SNoLev x1 = x2 ⟶ and (and (SNo x1) (SNoLev x1 ∈ SNoLev x0)) (SNoLt x1 x0)) ⟶ ∀ x0 : ο . x0 (proof)
Known SNoLt_irref^SNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known SNoLt_tra^SNoLt_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x0 x1 ⟶ SNoLt x1 x2 ⟶ SNoLt x0 x2
Theorem 7722e.. : (∀ x0 x1 x2 . x2 ∈ SNoLev x0 ⟶ SNo x1 ⟶ SNoLev x1 = x2 ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ and (and (SNo x1) (SNoLev x1 ∈ SNoLev x0)) (SNoLt x0 x1)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 66b65.. : (∀ x0 . ∀ x1 : ο . SNo x0 ⟶ ordinal (SNoLev x0) ⟶ x1) ⟶ ∀ x0 : ο . x0 (proof)
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Theorem e920e.. : (∀ x0 x1 x2 x3 . ordinal (SNoLev x0) ⟶ x1 ∈ ordsucc (SNoLev x2) ⟶ x2 = minus_SNo x3 ⟶ SNoLev (minus_SNo x3) ⊆ SNoLev x3 ⟶ ordinal (SNoLev (minus_SNo x3)) ⟶ ordinal (ordsucc (SNoLev x2)) ⟶ x1 ∈ SNoLev x0) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6c874.. : (∀ x0 x1 x2 x3 . ordinal (SNoLev x0) ⟶ x1 ∈ ordsucc (SNoLev x2) ⟶ x2 = minus_SNo x3 ⟶ SNo x3 ⟶ SNoLev (minus_SNo x3) ⊆ SNoLev x3 ⟶ ordinal (SNoLev x3) ⟶ x1 ∈ SNoLev x0) ⟶ ∀ x0 : ο . x0 (proof)
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Known In_1_2^In_1_2 : 1 ∈ 2
Known SNoLev_ordinal^{SNoLev_ordinal} : ∀ x0 . SNo x0 ⟶ ordinal (SNoLev x0)
Theorem 1bfb9.. : (∀ x0 x1 x2 x3 . ordinal (SNoLev x0) ⟶ x2 = minus_SNo x3 ⟶ SNoLev x3 ∈ SNoLev x0 ⟶ SNoLev (minus_SNo x3) ⊆ SNoLev x3 ⟶ ordinal (SNoLev (minus_SNo x3)) ⟶ ordinal (ordsucc (SNoLev x2)) ⟶ x1 ∈ SNoLev x0) ⟶ ∀ x0 : ο . x0 (proof)
Theorem e920e.. : (∀ x0 x1 x2 x3 . ordinal (SNoLev x0) ⟶ x1 ∈ ordsucc (SNoLev x2) ⟶ x2 = minus_SNo x3 ⟶ SNoLev (minus_SNo x3) ⊆ SNoLev x3 ⟶ ordinal (SNoLev (minus_SNo x3)) ⟶ ordinal (ordsucc (SNoLev x2)) ⟶ x1 ∈ SNoLev x0) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6c874.. : (∀ x0 x1 x2 x3 . ordinal (SNoLev x0) ⟶ x1 ∈ ordsucc (SNoLev x2) ⟶ x2 = minus_SNo x3 ⟶ SNo x3 ⟶ SNoLev (minus_SNo x3) ⊆ SNoLev x3 ⟶ ordinal (SNoLev x3) ⟶ x1 ∈ SNoLev x0) ⟶ ∀ x0 : ο . x0 (proof)
Param add_SNo^add_SNo : ι → ι → ι
Known add_SNo_0L^add_SNo_0L : ∀ x0 . SNo x0 ⟶ add_SNo 0 x0 = x0
Known ordinal_SNoLt_In^{ordinal_SNoLt_In} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ SNoLt x0 x1 ⟶ x0 ∈ x1
Theorem 45fa1.. : (∀ x0 x1 . ordinal x0 ⟶ SNo x0 ⟶ SNo x1 ⟶ ordinal (add_SNo x0 x1)) ⟶ ∀ x0 : ο . x0 (proof)
Known add_SNo_minus_SNo_linv^{add_SNo_minus_SNo_linv} : ∀ x0 . SNo x0 ⟶ add_SNo (minus_SNo x0) x0 = 0
Known add_SNo_0R^add_SNo_0R : ∀ x0 . SNo x0 ⟶ add_SNo x0 0 = x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem 048c4.. : (∀ x0 x1 . ordinal x1 ⟶ SNo x1 ⟶ add_SNo x0 (ordsucc x1) = ordsucc (add_SNo x0 x1)) ⟶ ∀ x0 : ο . x0 (proof)
Known add_SNo_minus_L2^{add_SNo_minus_L2} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1
Theorem 67c81.. : (∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo (minus_SNo x0) ⟶ add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1 ⟶ x1 = x2) ⟶ ∀ x0 : ο . x0 (proof)
Param omega^omega : ι
Known omega_ordinal^{omega_ordinal} : ordinal omega
Known SNo_omega^SNo_omega : SNo omega
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known nat_0^nat_0 : nat_p 0
Theorem 4d261.. : (∀ x0 x1 . SNoLev x0 ∈ omega ⟶ SNo x0 ⟶ SNo x1 ⟶ ordinal (SNoLev (add_SNo x0 x1)) ⟶ SNoLev (add_SNo x0 x1) ∈ omega) ⟶ ∀ x0 : ο . x0 (proof)
Known add_SNo_minus_SNo_rinv^{add_SNo_minus_SNo_rinv} : ∀ x0 . SNo x0 ⟶ add_SNo x0 (minus_SNo x0) = 0
Theorem 72f38.. : (∀ x0 x1 x2 x3 x4 x5 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo (minus_SNo x2) ⟶ SNo (minus_SNo x5) ⟶ SNo (add_SNo x0 x1) ⟶ SNoLt (add_SNo x0 (add_SNo x1 (minus_SNo x2))) (add_SNo x3 (add_SNo x4 (minus_SNo x5)))) ⟶ ∀ x0 : ο . x0 (proof)
Param int^int : ι
Known minus_SNo_invol^{minus_SNo_invol} : ∀ x0 . SNo x0 ⟶ minus_SNo (minus_SNo x0) = x0
Known int_SNo_cases^{int_SNo_cases} : ∀ x0 : ι → ο . (∀ x1 . x1 ∈ omega ⟶ x0 x1) ⟶ (∀ x1 . x1 ∈ omega ⟶ x0 (minus_SNo x1)) ⟶ ∀ x1 . x1 ∈ int ⟶ x0 x1
Param SNoLe^SNoLe : ι → ι → ο
Known SNoLtLe_tra^SNoLtLe_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x0 x1 ⟶ SNoLe x1 x2 ⟶ SNoLt x0 x2
Known ordinal_In_SNoLt^{ordinal_In_SNoLt} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ SNoLt x1 x0
Known minus_SNo_Le_contra^{minus_SNo_Le_contra} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe x0 x1 ⟶ SNoLe (minus_SNo x1) (minus_SNo x0)
Known omega_SNo^omega_SNo : ∀ x0 . x0 ∈ omega ⟶ SNo x0
Known ordinal_Subq_SNoLe^{ordinal_Subq_SNoLe} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ x0 ⊆ x1 ⟶ SNoLe x0 x1
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Theorem ef945.. : (∀ x0 x1 . x0 ∈ omega ⟶ SNo x0 ⟶ SNo x1 ⟶ add_SNo (minus_SNo x0) (minus_SNo x1) ∈ int) ⟶ ∀ x0 : ο . x0 (proof)
Param real^real : ι
Param mul_SNo^mul_SNo : ι → ι → ι
Known SNo_eps_1^SNo_eps_1 : SNo (eps_ 1)
Known mul_SNo_zeroL^{mul_SNo_zeroL} : ∀ x0 . SNo x0 ⟶ mul_SNo 0 x0 = 0
Known real_SNo^real_SNo : ∀ x0 . x0 ∈ real ⟶ SNo x0
Known real_0^real_0 : 0 ∈ real
Theorem 4a99f.. : (∀ x0 x1 x2 . SNo x0 ⟶ x1 ∈ omega ⟶ x2 ∈ real ⟶ SNo (eps_ x1) ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ real) (mul_SNo x0 x4 = 1) ⟶ x3) ⟶ x3) ⟶ ∀ x0 : ο . x0 (proof)
Param Sing^Sing : ι → ι
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Theorem b19ac.. : (∀ x0 x1 x2 . Sing 2 ∈ x1 ⟶ ordinal (SNoLev x0) ⟶ x2 ∈ SNoLev x0 ⟶ not (ordinal x2)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem c87ed.. : (∀ x0 x1 x2 . SNo x0 ⟶ x1 ∈ x0 ⟶ x2 ∈ Sing (Sing 2) ⟶ x2 = Sing 2 ⟶ ∀ x3 : ο . x3) ⟶ ∀ x0 : ο . x0 (proof)