Proofgold Address

Param binunion^binunion : ι → ι → ι
Param SetAdjoin^SetAdjoin : ι → ι → ι
Param Sing^Sing : ι → ι
Definition e9c39.. := λ x0 x1 x2 . binunion x1 {SetAdjoin x3 (Sing x0)|x3 ∈ x2}
Param ordsucc^ordsucc : ι → ι
Definition ad280.. := e9c39.. 2
Known 43bcd.. : ∀ x0 . ad280.. x0 0 = x0
Param SNo^SNo : ι → ο
Known 8ae5d.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x2 ⟶ ad280.. x0 x1 = ad280.. x2 x3 ⟶ x0 = x2
Known 943f5.. : ∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ ad280.. x0 x1 = ad280.. x2 x3 ⟶ x1 = x3
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition c7ce4.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (x0 = ad280.. x2 x4) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Known e4080.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ c7ce4.. (ad280.. x0 x1)
Known 3577c.. : ∀ x0 . c7ce4.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 . SNo x2 ⟶ SNo x3 ⟶ x0 = ad280.. x2 x3 ⟶ x1 (ad280.. x2 x3)) ⟶ x1 x0
Definition 8d0f8.. := ad280.. 0 1
Definition 28f8d.. := λ x0 . prim0 (λ x1 . and (SNo x1) (∀ x2 : ο . (∀ x3 . and (SNo x3) (x0 = ad280.. x1 x3) ⟶ x2) ⟶ x2))
Definition d634d.. := λ x0 . prim0 (λ x1 . and (SNo x1) (x0 = ad280.. (28f8d.. x0) x1))
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem 95e88.. : ∀ x0 . c7ce4.. x0 ⟶ and (SNo (28f8d.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (x0 = ad280.. (28f8d.. x0) x2) ⟶ x1) ⟶ x1) (proof)
Theorem 1c01b.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ 28f8d.. (ad280.. x0 x1) = x0 (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 4aab3.. : ∀ x0 . c7ce4.. x0 ⟶ and (SNo (d634d.. x0)) (x0 = ad280.. (28f8d.. x0) (d634d.. x0)) (proof)
Theorem 5b520.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ d634d.. (ad280.. x0 x1) = x1 (proof)
Theorem 85533.. : ∀ x0 . c7ce4.. x0 ⟶ SNo (28f8d.. x0) (proof)
Theorem eb0da.. : ∀ x0 . c7ce4.. x0 ⟶ SNo (d634d.. x0) (proof)
Theorem 68e0b.. : ∀ x0 . c7ce4.. x0 ⟶ x0 = ad280.. (28f8d.. x0) (d634d.. x0) (proof)
Theorem 371c6.. : ∀ x0 x1 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ 28f8d.. x0 = 28f8d.. x1 ⟶ d634d.. x0 = d634d.. x1 ⟶ x0 = x1 (proof)
Param minus_SNo^minus_SNo : ι → ι
Definition b1848.. := λ x0 . ad280.. (minus_SNo (28f8d.. x0)) (minus_SNo (d634d.. x0))
Param add_SNo^add_SNo : ι → ι → ι
Definition a0628.. := λ x0 x1 . ad280.. (add_SNo (28f8d.. x0) (28f8d.. x1)) (add_SNo (d634d.. x0) (d634d.. x1))
Param mul_SNo^mul_SNo : ι → ι → ι
Definition 22598.. := λ x0 x1 . ad280.. (add_SNo (mul_SNo (28f8d.. x0) (28f8d.. x1)) (minus_SNo (mul_SNo (d634d.. x0) (d634d.. x1)))) (add_SNo (mul_SNo (28f8d.. x0) (d634d.. x1)) (mul_SNo (d634d.. x0) (28f8d.. x1)))
Param div_SNo^div_SNo : ι → ι → ι
Param exp_SNo_nat^exp_SNo_nat : ι → ι → ι
Definition 41fb9.. := λ x0 . ad280.. (div_SNo (28f8d.. x0) (add_SNo (exp_SNo_nat (28f8d.. x0) 2) (exp_SNo_nat (d634d.. x0) 2))) (minus_SNo (div_SNo (d634d.. x0) (add_SNo (exp_SNo_nat (28f8d.. x0) 2) (exp_SNo_nat (d634d.. x0) 2))))
Definition 74066.. := λ x0 x1 . 22598.. x0 (41fb9.. x1)
Known SNo_0^SNo_0 : SNo 0
Known SNo_1^SNo_1 : SNo 1
Theorem 3e3aa.. : c7ce4.. 8d0f8.. (proof)
Known SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Theorem d3d48.. : ∀ x0 . c7ce4.. x0 ⟶ 28f8d.. (b1848.. x0) = minus_SNo (28f8d.. x0) (proof)
Theorem d1304.. : ∀ x0 . c7ce4.. x0 ⟶ d634d.. (b1848.. x0) = minus_SNo (d634d.. x0) (proof)
Known SNo_add_SNo^SNo_add_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (add_SNo x0 x1)
Theorem 5576f.. : ∀ x0 x1 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ 28f8d.. (a0628.. x0 x1) = add_SNo (28f8d.. x0) (28f8d.. x1) (proof)
Theorem 9325f.. : ∀ x0 x1 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ d634d.. (a0628.. x0 x1) = add_SNo (d634d.. x0) (d634d.. x1) (proof)
Theorem 76017.. : ∀ x0 . c7ce4.. x0 ⟶ c7ce4.. (b1848.. x0) (proof)
Theorem 416cf.. : ∀ x0 . SNo x0 ⟶ 28f8d.. x0 = x0 (proof)
Theorem 0de29.. : ∀ x0 . SNo x0 ⟶ d634d.. x0 = 0 (proof)
Theorem 6c4fc.. : 28f8d.. 0 = 0 (proof)
Theorem 1c92a.. : d634d.. 0 = 0 (proof)
Theorem 7d0dc.. : 28f8d.. 1 = 1 (proof)
Theorem d3315.. : d634d.. 1 = 0 (proof)
Theorem f16c1.. : 28f8d.. 8d0f8.. = 0 (proof)
Theorem b2ead.. : d634d.. 8d0f8.. = 1 (proof)
Known add_SNo_0L^add_SNo_0L : ∀ x0 . SNo x0 ⟶ add_SNo 0 x0 = x0
Theorem db996.. : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 x1 = a0628.. x0 x1 (proof)
Theorem 33aee.. : ∀ x0 x1 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ c7ce4.. (a0628.. x0 x1) (proof)
Theorem 5e04b.. : ∀ x0 . c7ce4.. x0 ⟶ a0628.. 0 x0 = x0 (proof)
Known add_SNo_0R^add_SNo_0R : ∀ x0 . SNo x0 ⟶ add_SNo x0 0 = x0
Theorem 4b639.. : ∀ x0 . c7ce4.. x0 ⟶ a0628.. x0 0 = x0 (proof)
Known add_SNo_minus_SNo_linv^{add_SNo_minus_SNo_linv} : ∀ x0 . SNo x0 ⟶ add_SNo (minus_SNo x0) x0 = 0
Theorem c369e.. : ∀ x0 . c7ce4.. x0 ⟶ a0628.. (b1848.. x0) x0 = 0 (proof)
Known add_SNo_minus_SNo_rinv^{add_SNo_minus_SNo_rinv} : ∀ x0 . SNo x0 ⟶ add_SNo x0 (minus_SNo x0) = 0
Theorem 6cc17.. : ∀ x0 . c7ce4.. x0 ⟶ a0628.. x0 (b1848.. x0) = 0 (proof)
Known minus_SNo_0^minus_SNo_0 : minus_SNo 0 = 0
Theorem 61bcd.. : ∀ x0 . SNo x0 ⟶ minus_SNo x0 = b1848.. x0 (proof)
Known add_SNo_com^add_SNo_com : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 x1 = add_SNo x1 x0
Theorem 256a7.. : ∀ x0 x1 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ a0628.. x0 x1 = a0628.. x1 x0 (proof)
Known f_eq_i^f_eq_i : ∀ x0 : ι → ι . ∀ x1 x2 . x1 = x2 ⟶ x0 x1 = x0 x2
Known add_SNo_assoc^{add_SNo_assoc} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2
Theorem 052e0.. : ∀ x0 x1 x2 . c7ce4.. x0 ⟶ c7ce4.. x1 ⟶ c7ce4.. x2 ⟶ a0628.. x0 (a0628.. x1 x2) = a0628.. (a0628.. x0 x1) x2 (proof)