Proofgold Address

Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition If_Vo4 := λ x0 : ο . λ x1 x2 : (((ι → ο) → ο) → ο) → ο . λ x3 : ((ι → ο) → ο) → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Known prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem If_Vo4_1 : ∀ x0 : ο . ∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . x0 ⟶ If_Vo4 x0 x1 x2 = x1 (proof)
Known andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem If_Vo4_0 : ∀ x0 : ο . ∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . not x0 ⟶ If_Vo4 x0 x1 x2 = x2 (proof)
Definition Descr_Vo4 := λ x0 : ((((ι → ο) → ο) → ο) → ο) → ο . λ x1 : ((ι → ο) → ο) → ο . ∀ x2 : (((ι → ο) → ο) → ο) → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo4_prop : ∀ x0 : ((((ι → ο) → ο) → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : (((ι → ο) → ο) → ο) → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo4 x0) (proof)
Definition 9eb9b.. := λ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . λ x1 . λ x2 : (((ι → ο) → ο) → ο) → ο . ∀ x3 : ι → ((((ι → ο) → ο) → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_Vo4 := λ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . λ x1 . Descr_Vo4 (9eb9b.. x0 x1)
Theorem 71e94.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . ∀ x1 . ∀ x2 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x3 . prim1 x3 x1 ⟶ 9eb9b.. x0 x3 (x2 x3)) ⟶ 9eb9b.. x0 x1 (x0 x1 x2) (proof)
Theorem 1c22d.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . ∀ x1 . ∀ x2 : (((ι → ο) → ο) → ο) → ο . 9eb9b.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → (((ι → ο) → ο) → ο) → ο . and (∀ x5 . prim1 x5 x1 ⟶ 9eb9b.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Known In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Theorem 0f420.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : (((ι → ο) → ο) → ο) → ο . 9eb9b.. x0 x1 x2 ⟶ 9eb9b.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem f8b5f.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 9eb9b.. x0 x1 (In_rec_Vo4 x0 x1) (proof)
Theorem eb697.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 9eb9b.. x0 x1 (x0 x1 (In_rec_Vo4 x0)) (proof)
Theorem In_rec_Vo4_eq : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_Vo4 x0 x1 = x0 x1 (In_rec_Vo4 x0) (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm : ∀ x0 : ο . or x0 (not x0)
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Theorem not_and_or_demorgan : ∀ x0 x1 : ο . not (and x0 x1) ⟶ or (not x0) (not x1) (proof)
Theorem eq_imp_or : (λ x1 x2 : ο . x1 ⟶ x2) = λ x1 : ο . or (not x1) (proof)
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Theorem Subq_contra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ nIn x2 x1 ⟶ nIn x2 x0 (proof)
Param 4a7ef.. : ι
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known e8942.. : ∀ x0 . Subq 4a7ef.. x0
Theorem 3f849.. : ∀ x0 . Subq x0 4a7ef.. ⟶ x0 = 4a7ef.. (proof)
Theorem 3c674.. : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 4a7ef.. (proof)
Known UnionE : ∀ x0 x1 . prim1 x1 (prim3 x0) ⟶ ∀ x2 : ο . (∀ x3 . and (prim1 x1 x3) (prim1 x3 x0) ⟶ x2) ⟶ x2
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem b3f0d.. : prim3 4a7ef.. = 4a7ef.. (proof)
Param e5b72.. : ι → ι
Known b21da.. : ∀ x0 x1 . prim1 x1 (e5b72.. x0) ⟶ Subq x1 x0
Theorem 81acb.. : ∀ x0 . Subq (prim3 (e5b72.. x0)) x0 (proof)
Param 94f9e.. : ι → (ι → ι) → ι
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem d4dbc.. : ∀ x0 : ι → ι . 94f9e.. 4a7ef.. x0 = 4a7ef.. (proof)
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem 02c03.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ Subq (94f9e.. x0 x1) (94f9e.. x0 x2) (proof)
Theorem aff96.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 94f9e.. x0 x1 = 94f9e.. x0 x2 (proof)
Known 2532b.. : ∀ x0 x1 x2 . prim1 x0 (prim2 x1 x2) ⟶ or (x0 = x1) (x0 = x2)
Known 5a932.. : ∀ x0 x1 . prim1 x1 (prim2 x0 x1)
Known 67787.. : ∀ x0 x1 . prim1 x0 (prim2 x0 x1)
Theorem 38ffc.. : ∀ x0 x1 . Subq (prim2 x0 x1) (prim2 x1 x0) (proof)
Theorem 7cb28.. : ∀ x0 x1 . prim2 x0 x1 = prim2 x1 x0 (proof)
Param 0ac37.. : ι → ι → ι
Param 91630.. : ι → ι
Definition 15418.. := λ x0 x1 . 0ac37.. x0 (91630.. x1)
Known e7a4c.. : ∀ x0 . prim1 x0 (91630.. x0)
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0
Known c5d9a.. : ∀ x0 . prim1 4a7ef.. (e5b72.. x0)
Theorem 640be.. : e5b72.. 4a7ef.. = 91630.. 4a7ef.. (proof)
Theorem 2b8c2.. : ∀ x0 : ι → ι . ∀ x1 x2 . 94f9e.. (prim2 x1 x2) x0 = prim2 (x0 x1) (x0 x2) (proof)
Theorem 535ee.. : ∀ x0 : ι → ι . ∀ x1 . 94f9e.. (91630.. x1) x0 = 91630.. (x0 x1) (proof)
Known 6acac.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (x2 = x1 x4) ⟶ x3) ⟶ x3
Theorem 02c03.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ Subq (94f9e.. x0 x1) (94f9e.. x0 x2) (proof)
Theorem aff96.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 94f9e.. x0 x1 = 94f9e.. x0 x2 (proof)
Definition a842e.. := λ x0 . λ x1 : ι → ι . prim3 (94f9e.. x0 x1)
Known UnionI : ∀ x0 x1 x2 . prim1 x1 x2 ⟶ prim1 x2 x0 ⟶ prim1 x1 (prim3 x0)
Theorem 2236b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 x0 ⟶ prim1 x3 (x1 x2) ⟶ prim1 x3 (a842e.. x0 x1) (proof)
Known UnionE_impred : ∀ x0 x1 . prim1 x1 (prim3 x0) ⟶ ∀ x2 : ο . (∀ x3 . prim1 x1 x3 ⟶ prim1 x3 x0 ⟶ x2) ⟶ x2
Theorem 042d7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (a842e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (prim1 x2 (x1 x4)) ⟶ x3) ⟶ x3 (proof)
Theorem 9b5af.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (a842e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ prim1 x2 (x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem 0a29e.. : ∀ x0 . prim3 x0 = a842e.. x0 (λ x2 . x2) (proof)
Theorem 06b06.. : ∀ x0 . ∀ x1 : ι → ι . 94f9e.. x0 x1 = a842e.. x0 (λ x3 . 91630.. (x1 x3)) (proof)
Theorem f8e95.. : ∀ x0 . or (x0 = 4a7ef..) (∀ x1 : ο . (∀ x2 . prim1 x2 x0 ⟶ x1) ⟶ x1) (proof)
Known 62c05.. : ∀ x0 . prim1 x0 (e5b72.. x0)
Theorem 04a44.. : ∀ x0 . e5b72.. (91630.. x0) = prim2 4a7ef.. (91630.. x0) (proof)
Theorem e8b5a.. : e5b72.. (91630.. 4a7ef..) = prim2 4a7ef.. (91630.. 4a7ef..) (proof)
Param 1216a.. : ι → (ι → ο) → ι
Known d0a1f.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ prim1 x2 x0
Theorem 572ea.. : ∀ x0 . ∀ x1 : ι → ο . Subq (1216a.. x0 x1) x0 (proof)
Known 3daee.. : ∀ x0 x1 . Subq x1 x0 ⟶ prim1 x1 (e5b72.. x0)
Theorem d129e.. : ∀ x0 . ∀ x1 : ι → ο . prim1 (1216a.. x0 x1) (e5b72.. x0) (proof)
Known edd11.. : ∀ x0 x1 x2 . prim1 x2 (0ac37.. x0 x1) ⟶ or (prim1 x2 x0) (prim1 x2 x1)
Known da962.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 (0ac37.. x0 x1)
Known 287ca.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 x2 (0ac37.. x0 x1)
Theorem cf5a9.. : ∀ x0 x1 x2 . 0ac37.. x0 (0ac37.. x1 x2) = 0ac37.. (0ac37.. x0 x1) x2 (proof)
Theorem 64b03.. : ∀ x0 x1 . Subq (0ac37.. x0 x1) (0ac37.. x1 x0) (proof)
Theorem 47e6b.. : ∀ x0 x1 . 0ac37.. x0 x1 = 0ac37.. x1 x0 (proof)
Theorem 019ee.. : ∀ x0 . 0ac37.. 4a7ef.. x0 = x0 (proof)
Theorem 4d5c9.. : ∀ x0 . 0ac37.. x0 4a7ef.. = x0 (proof)
Theorem c20d9.. : ∀ x0 . 0ac37.. x0 x0 = x0 (proof)
Theorem 9c551.. : ∀ x0 x1 . Subq x0 (0ac37.. x0 x1) (proof)
Theorem cde9c.. : ∀ x0 x1 . Subq x1 (0ac37.. x0 x1) (proof)
Theorem 011e9.. : ∀ x0 x1 x2 . Subq x0 x2 ⟶ Subq x1 x2 ⟶ Subq (0ac37.. x0 x1) x2 (proof)
Known Subq_ref : ∀ x0 . Subq x0 x0
Theorem 02255.. : ∀ x0 x1 . Subq x0 x1 = (0ac37.. x0 x1 = x1) (proof)
Theorem 82f52.. : ∀ x0 x1 x2 . nIn x2 x0 ⟶ nIn x2 x1 ⟶ nIn x2 (0ac37.. x0 x1) (proof)
Theorem 7b5e9.. : ∀ x0 x1 x2 . nIn x2 (0ac37.. x0 x1) ⟶ and (nIn x2 x0) (nIn x2 x1) (proof)
Param d3786.. : ι → ι → ι
Known 695d8.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ prim1 x2 x0
Theorem fb39c.. : ∀ x0 x1 . Subq (d3786.. x0 x1) x0 (proof)
Known a5fe0.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ prim1 x2 x1
Theorem 93cc4.. : ∀ x0 x1 . Subq (d3786.. x0 x1) x1 (proof)
Known 2d07f.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 x1 ⟶ prim1 x2 (d3786.. x0 x1)
Theorem bd118.. : ∀ x0 x1 . Subq x0 x1 ⟶ d3786.. x0 x1 = x0 (proof)
Theorem fd472.. : ∀ x0 x1 x2 . Subq x2 x0 ⟶ Subq x2 x1 ⟶ Subq x2 (d3786.. x0 x1) (proof)
Known Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
Theorem 4ee26.. : ∀ x0 x1 x2 . d3786.. x0 (d3786.. x1 x2) = d3786.. (d3786.. x0 x1) x2 (proof)
Theorem ea6d0.. : ∀ x0 x1 . Subq (d3786.. x0 x1) (d3786.. x1 x0) (proof)
Theorem d7325.. : ∀ x0 x1 . d3786.. x0 x1 = d3786.. x1 x0 (proof)
Theorem c4edc.. : ∀ x0 . d3786.. 4a7ef.. x0 = 4a7ef.. (proof)
Theorem 5fecc.. : ∀ x0 . d3786.. x0 4a7ef.. = 4a7ef.. (proof)
Theorem 5cae2.. : ∀ x0 . d3786.. x0 x0 = x0 (proof)
Known 3eff2.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ and (prim1 x2 x0) (prim1 x2 x1)
Theorem 6deec.. : ∀ x0 x1 x2 . d3786.. x0 (0ac37.. x1 x2) = 0ac37.. (d3786.. x0 x1) (d3786.. x0 x2) (proof)
Theorem 62dce.. : ∀ x0 x1 x2 . 0ac37.. x0 (d3786.. x1 x2) = d3786.. (0ac37.. x0 x1) (0ac37.. x0 x2) (proof)
Theorem a7b4e.. : ∀ x0 x1 . Subq x0 x1 = (d3786.. x0 x1 = x0) (proof)
Theorem 87311.. : ∀ x0 x1 x2 . nIn x2 x0 ⟶ nIn x2 (d3786.. x0 x1) (proof)
Theorem ddd82.. : ∀ x0 x1 x2 . nIn x2 x1 ⟶ nIn x2 (d3786.. x0 x1) (proof)
Theorem e30c6.. : ∀ x0 x1 x2 . nIn x2 (d3786.. x0 x1) ⟶ or (nIn x2 x0) (nIn x2 x1) (proof)
Definition 1ad11.. := λ x0 x1 . 1216a.. x0 (λ x2 . nIn x2 x1)
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Theorem 753c4.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ nIn x2 x1 ⟶ prim1 x2 (1ad11.. x0 x1) (proof)
Known 6982e.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ and (prim1 x2 x0) (x1 x2)
Theorem 017d4.. : ∀ x0 x1 x2 . prim1 x2 (1ad11.. x0 x1) ⟶ and (prim1 x2 x0) (nIn x2 x1) (proof)
Theorem 26c23.. : ∀ x0 x1 x2 . prim1 x2 (1ad11.. x0 x1) ⟶ prim1 x2 x0 (proof)
Known ac5c1.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ x1 x2
Theorem 62370.. : ∀ x0 x1 x2 . prim1 x2 (1ad11.. x0 x1) ⟶ nIn x2 x1 (proof)
Theorem dcf34.. : ∀ x0 x1 . Subq (1ad11.. x0 x1) x0 (proof)
Theorem 7855c.. : ∀ x0 x1 x2 . Subq x2 x1 ⟶ Subq (1ad11.. x0 x1) (1ad11.. x0 x2) (proof)
Theorem c937b.. : ∀ x0 x1 x2 . nIn x2 x0 ⟶ nIn x2 (1ad11.. x0 x1) (proof)
Theorem 225c6.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ nIn x2 (1ad11.. x0 x1) (proof)
Known dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem fd21e.. : ∀ x0 x1 x2 . nIn x2 (1ad11.. x0 x1) ⟶ or (nIn x2 x0) (prim1 x2 x1) (proof)
Theorem 2c578.. : ∀ x0 . 1ad11.. x0 x0 = 4a7ef.. (proof)
Theorem 87924.. : ∀ x0 x1 x2 . 1ad11.. x0 (d3786.. x1 x2) = 0ac37.. (1ad11.. x0 x1) (1ad11.. x0 x2) (proof)
Theorem 4639d.. : ∀ x0 x1 x2 . 1ad11.. x0 (0ac37.. x1 x2) = 1ad11.. (1ad11.. x0 x1) x2 (proof)
Theorem c89f2.. : ∀ x0 x1 x2 . 1ad11.. (d3786.. x0 x1) x2 = d3786.. x0 (1ad11.. x1 x2) (proof)
Theorem f1c06.. : ∀ x0 x1 x2 . 1ad11.. (0ac37.. x0 x1) x2 = 0ac37.. (1ad11.. x0 x2) (1ad11.. x1 x2) (proof)
Theorem 60021.. : ∀ x0 x1 x2 . 1ad11.. x0 (1ad11.. x1 x2) = 0ac37.. (1ad11.. x0 x1) (d3786.. x0 x2) (proof)
Theorem 9a446.. : ∀ x0 . 1ad11.. 4a7ef.. x0 = 4a7ef.. (proof)
Theorem 25164.. : ∀ x0 . 1ad11.. x0 4a7ef.. = x0 (proof)