Proofgold Address

Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition TransSet := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Definition ordinal := λ x0 . and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1)
Param bc82c.. : ι → ι → ι
Param 80242.. : ι → ο
Known f3bd7.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ bc82c.. x0 x1 = bc82c.. x1 x0
Known cbcc4.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ prim1 (bc82c.. x2 x1) (bc82c.. x0 x1)
Known e3ccf.. : ∀ x0 . ordinal x0 ⟶ 80242.. x0
Known ordinal_Hered : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ordinal x1
Theorem c2a6e.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ ∀ x2 . prim1 x2 x1 ⟶ prim1 (bc82c.. x0 x2) (bc82c.. x0 x1) (proof)
Param 48ef8.. : ι
Param 616bf.. : ι → ι → ι
Param ba9d8.. : ι → ο
Known c2711.. : ∀ x0 . prim1 x0 48ef8.. ⟶ ba9d8.. x0
Param 4a7ef.. : ι
Param 4ae4a.. : ι → ι
Known 5c211.. : ∀ x0 : ι → ο . x0 4a7ef.. ⟶ (∀ x1 . ba9d8.. x1 ⟶ x0 x1 ⟶ x0 (4ae4a.. x1)) ⟶ ∀ x1 . ba9d8.. x1 ⟶ x0 x1
Known 97325.. : ∀ x0 . 80242.. x0 ⟶ bc82c.. x0 4a7ef.. = x0
Known f30c5.. : ∀ x0 . 616bf.. x0 4a7ef.. = x0
Known 9b91e.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ bc82c.. x0 (4ae4a.. x1) = 4ae4a.. (bc82c.. x0 x1)
Known f3fb5.. : ∀ x0 . ba9d8.. x0 ⟶ ordinal x0
Known 1c625.. : ∀ x0 x1 . ba9d8.. x1 ⟶ 616bf.. x0 (4ae4a.. x1) = 4ae4a.. (616bf.. x0 x1)
Theorem a1176.. : ∀ x0 . prim1 x0 48ef8.. ⟶ ∀ x1 . prim1 x1 48ef8.. ⟶ 616bf.. x0 x1 = bc82c.. x0 x1 (proof)
Known a3321.. : ∀ x0 . ba9d8.. x0 ⟶ prim1 x0 48ef8..
Known 4183e.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ba9d8.. (616bf.. x0 x1)
Theorem 2a532.. : ∀ x0 . prim1 x0 48ef8.. ⟶ ∀ x1 . prim1 x1 48ef8.. ⟶ prim1 (bc82c.. x0 x1) 48ef8.. (proof)
Known 47c39.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ bc82c.. x0 x1 = bc82c.. x0 x2 ⟶ x1 = x2
Theorem ef0df.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ bc82c.. x0 x1 = bc82c.. x2 x1 ⟶ x0 = x2 (proof)
Param e4431.. : ι → ι
Param 56ded.. : ι → ι
Known 9ec10.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . 80242.. x1 ⟶ 80242.. x2 ⟶ (∀ x3 . prim1 x3 (56ded.. (e4431.. x1)) ⟶ x0 x3 x2) ⟶ (∀ x3 . prim1 x3 (56ded.. (e4431.. x2)) ⟶ x0 x1 x3) ⟶ (∀ x3 . prim1 x3 (56ded.. (e4431.. x1)) ⟶ ∀ x4 . prim1 x4 (56ded.. (e4431.. x2)) ⟶ x0 x3 x4) ⟶ x0 x1 x2) ⟶ ∀ x1 x2 . 80242.. x1 ⟶ 80242.. x2 ⟶ x0 x1 x2
Param 02a50.. : ι → ι → ι
Param 0ac37.. : ι → ι → ι
Param 94f9e.. : ι → (ι → ι) → ι
Param 23e07.. : ι → ι
Param 5246e.. : ι → ι
Known 8a8cc.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ bc82c.. x0 x1 = 02a50.. (0ac37.. (94f9e.. (23e07.. x0) (λ x3 . bc82c.. x3 x1)) (94f9e.. (23e07.. x1) (bc82c.. x0))) (0ac37.. (94f9e.. (5246e.. x0) (λ x3 . bc82c.. x3 x1)) (94f9e.. (5246e.. x1) (bc82c.. x0)))
Param 02b90.. : ι → ι → ο
Param a842e.. : ι → (ι → ι) → ι
Param 099f3.. : ι → ι → ο
Param SNoEq_ : ι → ι → ι → ο
Known 9ecaa.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 : ο . (80242.. (02a50.. x0 x1) ⟶ prim1 (e4431.. (02a50.. x0 x1)) (4ae4a.. (0ac37.. (a842e.. x0 (λ x3 . 4ae4a.. (e4431.. x3))) (a842e.. x1 (λ x3 . 4ae4a.. (e4431.. x3))))) ⟶ (∀ x3 . prim1 x3 x0 ⟶ 099f3.. x3 (02a50.. x0 x1)) ⟶ (∀ x3 . prim1 x3 x1 ⟶ 099f3.. (02a50.. x0 x1) x3) ⟶ (∀ x3 . 80242.. x3 ⟶ (∀ x4 . prim1 x4 x0 ⟶ 099f3.. x4 x3) ⟶ (∀ x4 . prim1 x4 x1 ⟶ 099f3.. x3 x4) ⟶ and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. x3)) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) x3)) ⟶ x2) ⟶ x2
Known Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
Known 011e9.. : ∀ x0 x1 x2 . Subq x0 x2 ⟶ Subq x1 x2 ⟶ Subq (0ac37.. x0 x1) x2
Known 9b5af.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (a842e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ prim1 x2 (x1 x4) ⟶ x3) ⟶ x3
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 ordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (prim1 x0 x1) (Subq x1 x0)
Definition False := ∀ x0 : ο . x0
Known FalseE : False ⟶ ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known In_irref : ∀ x0 . nIn x0 x0
Known 4c9ee.. : ∀ x0 . 80242.. x0 ⟶ ordinal (e4431.. x0)
Known b71d0.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. (bc82c.. x0 x1)
Known 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0)
Known bba3d.. : ∀ x0 x1 . prim1 x0 x1 ⟶ nIn x1 x0
Known b72a3.. : ∀ x0 . ordinal x0 ⟶ ordinal (4ae4a.. x0)
Known 9aba9.. : ∀ x0 x1 . TransSet x1 ⟶ prim1 x0 (4ae4a.. x1) ⟶ Subq x0 x1
Known 45024.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (0ac37.. x0 x1)
Known d5fb2.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ordinal (x1 x2)) ⟶ ordinal (a842e.. x0 x1)
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known e76d1.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (5246e.. x0) ⟶ ∀ x2 : ο . (80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x0 x1 ⟶ x2) ⟶ x2
Known f4ff0.. : ∀ x0 . Subq (5246e.. x0) (56ded.. (e4431.. x0))
Known cbec9.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (23e07.. x0) ⟶ ∀ x2 : ο . (80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x1 x0 ⟶ x2) ⟶ x2
Known e1ffe.. : ∀ x0 . Subq (23e07.. x0) (56ded.. (e4431.. x0))
Known fe60b.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 02b90.. (0ac37.. (94f9e.. (23e07.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (23e07.. x1) (bc82c.. x0))) (0ac37.. (94f9e.. (5246e.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (5246e.. x1) (bc82c.. x0)))
Known c5221.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ ordinal (bc82c.. x0 x1)
Theorem da0a0.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ Subq (e4431.. (bc82c.. x0 x1)) (bc82c.. (e4431.. x0) (e4431.. x1)) (proof)
Param 1beb9.. : ι → ι → ο
Known bfaa9.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 (56ded.. x0) ⟶ ∀ x2 : ο . (prim1 (e4431.. x1) x0 ⟶ ordinal (e4431.. x1) ⟶ 80242.. x1 ⟶ 1beb9.. (e4431.. x1) x1 ⟶ x2) ⟶ x2
Known c8a5e.. : ordinal 48ef8..
Known ade9f.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 x2 . prim1 x2 x0 ⟶ 1beb9.. x2 x1 ⟶ prim1 x1 (56ded.. x0)
Known b0eab.. : ∀ x0 . 80242.. x0 ⟶ 1beb9.. (e4431.. x0) x0
Theorem 58e84.. : ∀ x0 . prim1 x0 (56ded.. 48ef8..) ⟶ ∀ x1 . prim1 x1 (56ded.. 48ef8..) ⟶ prim1 (bc82c.. x0 x1) (56ded.. 48ef8..) (proof)
Param 8428d.. : ι → ι
Definition a470d.. := 0ac37.. 48ef8.. (94f9e.. 48ef8.. 8428d..)
Param 3b429.. : ι → (ι → ι) → (ι → ι → ο) → CT2 ι
Param df931.. : ι → ι → ι
Definition efb37.. := 3b429.. a470d.. (λ x0 . 48ef8..) (λ x0 x1 . x1 = 4a7ef.. ⟶ ∀ x2 : ο . x2) df931..
Param nat_primrec : ι → (ι → ι → ι) → ι → ι
Param If_i : ο → ι → ι → ι
Param e37c0.. : ι → ι → ι
Definition 5fbd5.. := λ x0 x1 . λ x2 : ι → ι . nat_primrec 4a7ef.. (λ x3 x4 . If_i (prim1 x3 x0) 4a7ef.. (e37c0.. (x2 x3) x4)) (4ae4a.. x1)
Param 7ce1c.. : ι → ι → ι
Definition b4fd2.. := λ x0 x1 . λ x2 : ι → ι . nat_primrec (4ae4a.. 4a7ef..) (λ x3 x4 . If_i (prim1 x3 x0) (4ae4a.. 4a7ef..) (7ce1c.. (x2 x3) x4)) (4ae4a.. x1)