Proofgold Address

Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Definition empty_p := λ x0 . ∀ x1 . nIn x1 x0
Definition e581a.. := λ x0 . not (empty_p x0)
Param 4a7ef.. : ι
Definition bd0b9.. := prim1 4a7ef..
Param If_i : ο → ι → ι → ι
Param 4ae4a.. : ι → ι
Definition 896e2.. := λ x0 : ο . If_i x0 (4ae4a.. 4a7ef..) 4a7ef..
Param 48ef8.. : ι
Known 8ee89.. : prim1 4a7ef.. 48ef8..
Theorem 0345c.. : e581a.. 48ef8.. (proof)
Param 3097a.. : ι → (ι → ι) → ι
Definition b5c9f.. := λ x0 x1 . 3097a.. x1 (λ x2 . x0)
Param f482f.. : ι → ι → ι
Known d8d74.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 (3097a.. x0 x1) ⟶ prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3)
Theorem f97a7.. : ∀ x0 x1 x2 . prim1 x2 (b5c9f.. x1 x0) ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) x1 (proof)
Theorem bb32b.. : ∀ x0 x1 x2 x3 . prim1 x3 (b5c9f.. (b5c9f.. x2 x1) x0) ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x1 ⟶ prim1 (f482f.. (f482f.. x3 x4) x5) x2 (proof)
Known dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem 62f13.. : ∀ x0 . e581a.. x0 ⟶ ∀ x1 : ο . (∀ x2 . prim1 x2 x0 ⟶ x1) ⟶ x1 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm : ∀ x0 : ο . or x0 (not x0)
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..))
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 9ca29.. : ∀ x0 : ο . prim1 (896e2.. x0) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Known 9f6cd.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 x0
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem c756b.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ bd0b9.. x0 ⟶ x0 = 4ae4a.. 4a7ef.. (proof)
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Theorem b588d.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ not (bd0b9.. x0) ⟶ x0 = 4a7ef.. (proof)
Theorem 0ae99.. : ∀ x0 : ο . x0 ⟶ bd0b9.. (896e2.. x0) (proof)
Theorem 109c3.. : ∀ x0 : ο . bd0b9.. (896e2.. x0) ⟶ x0 (proof)