Proofgold Asset

Param f4b0e.. : ι → ι → ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Definition 84b4d.. := f4b0e.. 0 1 0 0
Definition 439cb.. := f4b0e.. 0 0 1 0
Definition 11c0b.. := f4b0e.. 0 0 0 1
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param SNo^SNo : ι → ο
Definition 6b27d.. := λ x0 . prim0 (λ x1 . and (SNo x1) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (x0 = f4b0e.. x1 x3 x5 x7) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2))
Definition e5fe3.. := λ x0 . prim0 (λ x1 . and (SNo x1) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (x0 = f4b0e.. (6b27d.. x0) x1 x3 x5) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2))
Definition e47cc.. := λ x0 . prim0 (λ x1 . and (SNo x1) (∀ x2 : ο . (∀ x3 . and (SNo x3) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) x1 x3) ⟶ x2) ⟶ x2))
Definition 7cd66.. := λ x0 . prim0 (λ x1 . and (SNo x1) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) (e47cc.. x0) x1))
Definition 8c189.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (x0 = f4b0e.. x2 x4 x6 x8) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem 3f1df.. : ∀ x0 . 8c189.. x0 ⟶ and (SNo (6b27d.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (x0 = f4b0e.. (6b27d.. x0) x2 x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1) (proof)
Theorem 0dacf.. : ∀ x0 . 8c189.. x0 ⟶ and (SNo (e5fe3.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) x2 x4) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1) (proof)
Theorem 9c07c.. : ∀ x0 . 8c189.. x0 ⟶ and (SNo (e47cc.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) (e47cc.. x0) x2) ⟶ x1) ⟶ x1) (proof)
Theorem ef681.. : ∀ x0 . 8c189.. x0 ⟶ and (SNo (7cd66.. x0)) (x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) (e47cc.. x0) (7cd66.. x0)) (proof)
Theorem 7f221.. : ∀ x0 . 8c189.. x0 ⟶ SNo (6b27d.. x0) (proof)
Theorem 7b3f7.. : ∀ x0 . 8c189.. x0 ⟶ SNo (e5fe3.. x0) (proof)
Theorem 523de.. : ∀ x0 . 8c189.. x0 ⟶ SNo (e47cc.. x0) (proof)
Theorem 07fd4.. : ∀ x0 . 8c189.. x0 ⟶ SNo (7cd66.. x0) (proof)
Theorem f9f9c.. : ∀ x0 . 8c189.. x0 ⟶ x0 = f4b0e.. (6b27d.. x0) (e5fe3.. x0) (e47cc.. x0) (7cd66.. x0) (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 440f9.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ 8c189.. (f4b0e.. x0 x1 x2 x3) (proof)
Theorem 0869d.. : ∀ x0 . 8c189.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 x4 x5 . SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ x0 = f4b0e.. x2 x3 x4 x5 ⟶ x1 (f4b0e.. x2 x3 x4 x5)) ⟶ x1 x0 (proof)
Known SNo_0^SNo_0 : SNo 0
Known SNo_1^SNo_1 : SNo 1
Theorem a616f.. : 8c189.. 84b4d.. (proof)
Theorem c38f0.. : 8c189.. 439cb.. (proof)
Theorem 84934.. : 8c189.. 11c0b.. (proof)
Known 84fad.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x0 = x4
Theorem 7484f.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ 6b27d.. (f4b0e.. x0 x1 x2 x3) = x0 (proof)
Known aa1e8.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x1 = x5
Theorem d5450.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ e5fe3.. (f4b0e.. x0 x1 x2 x3) = x1 (proof)
Known 04ead.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x2 = x6
Theorem 097ec.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ e47cc.. (f4b0e.. x0 x1 x2 x3) = x2 (proof)
Known 57cf4.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ f4b0e.. x0 x1 x2 x3 = f4b0e.. x4 x5 x6 x7 ⟶ x3 = x7
Theorem 40e63.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ 7cd66.. (f4b0e.. x0 x1 x2 x3) = x3 (proof)
Param minus_SNo^minus_SNo : ι → ι
Definition 2b257.. := λ x0 . f4b0e.. (minus_SNo (6b27d.. x0)) (minus_SNo (e5fe3.. x0)) (minus_SNo (e47cc.. x0)) (minus_SNo (7cd66.. x0))
Param add_SNo^add_SNo : ι → ι → ι
Definition 989da.. := λ x0 x1 . f4b0e.. (add_SNo (6b27d.. x0) (6b27d.. x1)) (add_SNo (e5fe3.. x0) (e5fe3.. x1)) (add_SNo (e47cc.. x0) (e47cc.. x1)) (add_SNo (7cd66.. x0) (7cd66.. x1))
Param mul_SNo^mul_SNo : ι → ι → ι
Definition 1d79d.. := λ x0 x1 . f4b0e.. (add_SNo (mul_SNo (6b27d.. x0) (6b27d.. x1)) (add_SNo (minus_SNo (mul_SNo (e5fe3.. x0) (e5fe3.. x1))) (add_SNo (minus_SNo (mul_SNo (e47cc.. x0) (e47cc.. x1))) (minus_SNo (mul_SNo (7cd66.. x0) (7cd66.. x1)))))) (add_SNo (mul_SNo (6b27d.. x0) (e5fe3.. x1)) (add_SNo (mul_SNo (e5fe3.. x0) (6b27d.. x1)) (add_SNo (mul_SNo (e47cc.. x0) (7cd66.. x1)) (minus_SNo (mul_SNo (7cd66.. x0) (e47cc.. x1)))))) (add_SNo (mul_SNo (6b27d.. x0) (e47cc.. x1)) (add_SNo (minus_SNo (mul_SNo (e5fe3.. x0) (7cd66.. x1))) (add_SNo (mul_SNo (e47cc.. x0) (6b27d.. x1)) (mul_SNo (7cd66.. x0) (e5fe3.. x1))))) (add_SNo (mul_SNo (6b27d.. x0) (7cd66.. x1)) (add_SNo (mul_SNo (e5fe3.. x0) (e47cc.. x1)) (add_SNo (minus_SNo (mul_SNo (e47cc.. x0) (e5fe3.. x1))) (mul_SNo (7cd66.. x0) (6b27d.. x1)))))