Proofgold Address

Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition TransSet := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Param 91630.. : ι → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Known 3bafe.. : 4a7ef.. = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0
Known e7a4c.. : ∀ x0 . prim1 x0 (91630.. x0)
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 6351a.. : not (TransSet (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition ordinal := λ x0 . and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1)
Theorem 39b19.. : not (ordinal (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Param 0ac37.. : ι → ι → ι
Definition 15418.. := λ x0 x1 . 0ac37.. x0 (91630.. x1)
Known ordinal_Hered : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ordinal x1
Known 287ca.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 x2 (0ac37.. x0 x1)
Theorem aef25.. : ∀ x0 . not (ordinal (15418.. x0 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Theorem ada38.. : ∀ x0 x1 . ordinal x0 ⟶ nIn (15418.. x1 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x0 (proof)
Known 9ac87.. : 4ae4a.. 4a7ef.. = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Theorem b3b5f.. : nIn (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) (91630.. (91630.. (4ae4a.. 4a7ef..))) (proof)
Param 94f9e.. : ι → (ι → ι) → ι
Definition 472ec.. := λ x0 . 0ac37.. x0 (94f9e.. x0 (λ x1 . 15418.. x1 (91630.. (4ae4a.. 4a7ef..))))
Param exactly1of2 : ο → ο → ο
Definition 1beb9.. := λ x0 x1 . and (Subq x1 (472ec.. x0)) (∀ x2 . prim1 x2 x0 ⟶ exactly1of2 (prim1 (15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1) (prim1 x2 x1))
Definition 80242.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (ordinal x2) (1beb9.. x2 x0) ⟶ x1) ⟶ x1
Known FalseE : False ⟶ ∀ x0 : ο . x0
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known edd11.. : ∀ x0 x1 x2 . prim1 x2 (0ac37.. x0 x1) ⟶ or (prim1 x2 x0) (prim1 x2 x1)
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem dd5e7.. : ∀ x0 x1 . 80242.. x0 ⟶ nIn (15418.. x1 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x0 (proof)
Definition 236dc.. := λ x0 x1 . 0ac37.. x0 (94f9e.. x1 (λ x2 . 15418.. x2 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Known da962.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 (0ac37.. x0 x1)
Theorem cd385.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 236dc.. x0 x1 = 236dc.. x2 x3 ⟶ Subq x0 x2 (proof)
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Theorem 513aa.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x2 ⟶ 236dc.. x0 x1 = 236dc.. x2 x3 ⟶ x0 = x2 (proof)
Theorem de4dc.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ 15418.. x2 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) = 15418.. x3 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ Subq x2 x3 (proof)
Theorem 5a16f.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ 15418.. x2 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) = 15418.. x3 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x2 = x3 (proof)
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem 4999f.. : ∀ x0 x1 x2 x3 . 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 236dc.. x0 x1 = 236dc.. x2 x3 ⟶ Subq x1 x3 (proof)
Theorem 21331.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 236dc.. x0 x1 = 236dc.. x2 x3 ⟶ x1 = x3 (proof)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem d3c08.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 236dc.. x0 x1 = 236dc.. x2 x3 ⟶ and (x0 = x2) (x1 = x3) (proof)
Known d4dbc.. : ∀ x0 : ι → ι . 94f9e.. 4a7ef.. x0 = 4a7ef..
Known 4d5c9.. : ∀ x0 . 0ac37.. x0 4a7ef.. = x0
Theorem a0d36.. : ∀ x0 . 236dc.. x0 4a7ef.. = x0 (proof)
Definition 1013b.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (80242.. x2) (∀ x3 : ο . (∀ x4 . and (80242.. x4) (x0 = 236dc.. x2 x4) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Theorem 746bb.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 1013b.. (236dc.. x0 x1) (proof)
Theorem d7ca5.. : ∀ x0 . 1013b.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 . 80242.. x2 ⟶ 80242.. x3 ⟶ x0 = 236dc.. x2 x3 ⟶ x1 (236dc.. x2 x3)) ⟶ x1 x0 (proof)
Known ebb60.. : 80242.. 4a7ef..
Theorem 6cab0.. : ∀ x0 . 80242.. x0 ⟶ 1013b.. x0 (proof)
Definition f8050.. := 236dc.. 4a7ef.. (4ae4a.. 4a7ef..)
Known c8ed0.. : 80242.. (4ae4a.. 4a7ef..)
Theorem b4a76.. : 1013b.. f8050.. (proof)
Definition ce322.. := λ x0 . prim0 (λ x1 . and (80242.. x1) (∀ x2 : ο . (∀ x3 . and (80242.. x3) (x0 = 236dc.. x1 x3) ⟶ x2) ⟶ x2))
Definition f6a32.. := λ x0 . prim0 (λ x1 . and (80242.. x1) (x0 = 236dc.. (ce322.. x0) x1))
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem a5a32.. : ∀ x0 . 1013b.. x0 ⟶ and (80242.. (ce322.. x0)) (∀ x1 : ο . (∀ x2 . and (80242.. x2) (x0 = 236dc.. (ce322.. x0) x2) ⟶ x1) ⟶ x1) (proof)
Theorem 55f9f.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ce322.. (236dc.. x0 x1) = x0 (proof)
Theorem d89f9.. : ∀ x0 . 1013b.. x0 ⟶ and (80242.. (f6a32.. x0)) (x0 = 236dc.. (ce322.. x0) (f6a32.. x0)) (proof)
Theorem 41b27.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ f6a32.. (236dc.. x0 x1) = x1 (proof)
Theorem 3a25a.. : ∀ x0 . 1013b.. x0 ⟶ 80242.. (ce322.. x0) (proof)
Theorem 43fc2.. : ∀ x0 . 1013b.. x0 ⟶ 80242.. (f6a32.. x0) (proof)
Theorem 501e2.. : ∀ x0 . 1013b.. x0 ⟶ x0 = 236dc.. (ce322.. x0) (f6a32.. x0) (proof)
Theorem facc5.. : ∀ x0 x1 . 1013b.. x0 ⟶ 1013b.. x1 ⟶ ce322.. x0 = ce322.. x1 ⟶ f6a32.. x0 = f6a32.. x1 ⟶ x0 = x1 (proof)
Param bc82c.. : ι → ι → ι
Definition e37c0.. := λ x0 x1 . 236dc.. (bc82c.. (ce322.. x0) (ce322.. x1)) (bc82c.. (f6a32.. x0) (f6a32.. x1))
Param e6316.. : ι → ι → ι
Param f4dc0.. : ι → ι
Definition 7ce1c.. := λ x0 x1 . 236dc.. (bc82c.. (e6316.. (ce322.. x0) (ce322.. x1)) (f4dc0.. (e6316.. (f6a32.. x0) (f6a32.. x1)))) (bc82c.. (e6316.. (ce322.. x0) (f6a32.. x1)) (e6316.. (f6a32.. x0) (ce322.. x1)))
Param 3b429.. : ι → (ι → ι) → (ι → ι → ο) → CT2 ι
Param f74bd.. : ι
Param True : ο
Definition aee35.. := 3b429.. f74bd.. (λ x0 . f74bd..) (λ x0 x1 . True) 236dc..