Proofgold Address

Param a842e.. : ι → (ι → ι) → ι
Param 4a7ef.. : ι
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Known 3f849.. : ∀ x0 . Subq x0 4a7ef.. ⟶ x0 = 4a7ef..
Known 9b5af.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (a842e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ prim1 x2 (x1 x4) ⟶ x3) ⟶ x3
Definition False := ∀ x0 : ο . x0
Known FalseE : False ⟶ ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem 5dcf0.. : ∀ x0 : ι → ι . a842e.. 4a7ef.. x0 = 4a7ef.. (proof)
Param 80242.. : ι → ο
Param and : ο → ο → ο
Param 099f3.. : ι → ι → ο
Definition 02b90.. := λ x0 x1 . and (and (∀ x2 . prim1 x2 x0 ⟶ 80242.. x2) (∀ x2 . prim1 x2 x1 ⟶ 80242.. x2)) (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3)
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem c0b78.. : ∀ x0 . (∀ x1 . prim1 x1 x0 ⟶ 80242.. x1) ⟶ 02b90.. x0 4a7ef.. (proof)
Theorem 80b57.. : ∀ x0 . (∀ x1 . prim1 x1 x0 ⟶ 80242.. x1) ⟶ 02b90.. 4a7ef.. x0 (proof)
Theorem 64de1.. : 02b90.. 4a7ef.. 4a7ef.. (proof)
Param 02a50.. : ι → ι → ι
Param e4431.. : ι → ι
Param 4ae4a.. : ι → ι
Param 0ac37.. : ι → ι → ι
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 019ee.. : ∀ x0 . 0ac37.. 4a7ef.. x0 = x0
Known 2b8be.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ e4431.. x0 = e4431.. x1 ⟶ SNoEq_ (e4431.. x0) x0 x1 ⟶ x0 = x1
Known ebb60.. : 80242.. 4a7ef..
Known ab02c.. : e4431.. 4a7ef.. = 4a7ef..
Param iff : ο → ο → ο
Known SNoEq_I : ∀ x0 x1 x2 . (∀ x3 . prim1 x3 x0 ⟶ iff (prim1 x3 x1) (prim1 x3 x2)) ⟶ SNoEq_ x0 x1 x2
Known 2911f.. : ∀ x0 . prim1 x0 (4ae4a.. 4a7ef..) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 x0
Theorem 4e105.. : 02a50.. 4a7ef.. 4a7ef.. = 4a7ef.. (proof)
Param 23e07.. : ι → ι
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known cbec9.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (23e07.. x0) ⟶ ∀ x2 : ο . (80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x1 x0 ⟶ x2) ⟶ x2
Known c8ed0.. : 80242.. (4ae4a.. 4a7ef..)
Param ordinal : ι → ο
Known aab4f.. : ∀ x0 . ordinal x0 ⟶ e4431.. x0 = x0
Param ba9d8.. : ι → ο
Known f3fb5.. : ∀ x0 . ba9d8.. x0 ⟶ ordinal x0
Known 3db81.. : ba9d8.. (4ae4a.. 4a7ef..)
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Known f5194.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x1 x0 ⟶ prim1 x1 (23e07.. x0)
Known 44eea.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ 099f3.. x1 x0
Theorem 47397.. : 23e07.. (4ae4a.. 4a7ef..) = 4ae4a.. 4a7ef.. (proof)
Param 5246e.. : ι → ι
Known 44ec0.. : ∀ x0 . ordinal x0 ⟶ 5246e.. x0 = 4a7ef..
Theorem f5a07.. : 5246e.. (4ae4a.. 4a7ef..) = 4a7ef.. (proof)
Param bc82c.. : ι → ι → ι
Known b71d0.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. (bc82c.. x0 x1)
Theorem 18470.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. (bc82c.. x0 (bc82c.. x1 x2)) (proof)
Param f4dc0.. : ι → ι
Known 706f7.. : ∀ x0 . 80242.. x0 ⟶ 80242.. (f4dc0.. x0)
Theorem 9cb52.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. (bc82c.. x0 (bc82c.. x1 (f4dc0.. x2))) (proof)
Known 58c5d.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ f4dc0.. (bc82c.. x0 x1) = bc82c.. (f4dc0.. x0) (f4dc0.. x1)
Theorem c8dd9.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ f4dc0.. (bc82c.. x0 (bc82c.. x1 x2)) = bc82c.. (f4dc0.. x0) (bc82c.. (f4dc0.. x1) (f4dc0.. x2)) (proof)
Known 368c5.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ bc82c.. x0 (bc82c.. x1 x2) = bc82c.. (bc82c.. x0 x1) x2
Known 8782d.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 x2 ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x1)
Theorem e1455.. : ∀ x0 x1 x2 x3 x4 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 80242.. x4 ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x3) ⟶ 099f3.. (bc82c.. x0 (bc82c.. x1 x4)) (bc82c.. x2 (bc82c.. x3 x4)) (proof)
Known 5144e.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ bc82c.. x0 (bc82c.. x1 x2) = bc82c.. x2 (bc82c.. x0 x1)
Theorem db322.. : ∀ x0 x1 x2 x3 x4 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 80242.. x4 ⟶ 099f3.. (bc82c.. x1 x0) (bc82c.. x2 x3) ⟶ 099f3.. (bc82c.. x0 (bc82c.. x4 x1)) (bc82c.. x2 (bc82c.. x3 x4)) (proof)
Known 08d14.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x1) ⟶ 099f3.. x0 x2
Known 5c481.. : ∀ x0 . 80242.. x0 ⟶ bc82c.. (f4dc0.. x0) x0 = 4a7ef..
Known 97325.. : ∀ x0 . 80242.. x0 ⟶ bc82c.. x0 4a7ef.. = x0
Theorem b9ca8.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 (bc82c.. x2 x1) ⟶ 099f3.. (bc82c.. x0 (f4dc0.. x1)) x2 (proof)
Theorem 1dc86.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. (bc82c.. x2 x1) x0 ⟶ 099f3.. x2 (bc82c.. x0 (f4dc0.. x1)) (proof)
Known f3bd7.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ bc82c.. x0 x1 = bc82c.. x1 x0
Theorem 98ce3.. : ∀ x0 x1 x2 x3 x4 x5 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 80242.. x4 ⟶ 80242.. x5 ⟶ 099f3.. (bc82c.. x0 (bc82c.. x1 x5)) (bc82c.. x3 (bc82c.. x4 x2)) ⟶ 099f3.. (bc82c.. x0 (bc82c.. x1 (f4dc0.. x2))) (bc82c.. x3 (bc82c.. x4 (f4dc0.. x5))) (proof)
Param e6316.. : ι → ι → ι
Known ed5b9.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ ∀ x2 : ο . (80242.. (e6316.. x0 x1) ⟶ (∀ x3 . prim1 x3 (23e07.. x0) ⟶ ∀ x4 . prim1 x4 (23e07.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x3 x1) (e6316.. x0 x4)) (bc82c.. (e6316.. x0 x1) (e6316.. x3 x4))) ⟶ (∀ x3 . prim1 x3 (5246e.. x0) ⟶ ∀ x4 . prim1 x4 (5246e.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x3 x1) (e6316.. x0 x4)) (bc82c.. (e6316.. x0 x1) (e6316.. x3 x4))) ⟶ (∀ x3 . prim1 x3 (23e07.. x0) ⟶ ∀ x4 . prim1 x4 (5246e.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x0 x1) (e6316.. x3 x4)) (bc82c.. (e6316.. x3 x1) (e6316.. x0 x4))) ⟶ (∀ x3 . prim1 x3 (5246e.. x0) ⟶ ∀ x4 . prim1 x4 (23e07.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x0 x1) (e6316.. x3 x4)) (bc82c.. (e6316.. x3 x1) (e6316.. x0 x4))) ⟶ x2) ⟶ x2
Theorem 278ed.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. (e6316.. x0 x1) (proof)
Theorem fa87a.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 80242.. (bc82c.. (e6316.. x2 x1) (bc82c.. (e6316.. x0 x3) (f4dc0.. (e6316.. x2 x3)))) (proof)
Known ca858.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 : ο . (∀ x3 x4 . (∀ x5 . prim1 x5 x3 ⟶ ∀ x6 : ο . (∀ x7 . prim1 x7 (23e07.. x0) ⟶ ∀ x8 . prim1 x8 (23e07.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ (∀ x7 . prim1 x7 (5246e.. x0) ⟶ ∀ x8 . prim1 x8 (5246e.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . prim1 x5 (23e07.. x0) ⟶ ∀ x6 . prim1 x6 (23e07.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x3) ⟶ (∀ x5 . prim1 x5 (5246e.. x0) ⟶ ∀ x6 . prim1 x6 (5246e.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x3) ⟶ (∀ x5 . prim1 x5 x4 ⟶ ∀ x6 : ο . (∀ x7 . prim1 x7 (23e07.. x0) ⟶ ∀ x8 . prim1 x8 (5246e.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ (∀ x7 . prim1 x7 (5246e.. x0) ⟶ ∀ x8 . prim1 x8 (23e07.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . prim1 x5 (23e07.. x0) ⟶ ∀ x6 . prim1 x6 (5246e.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x4) ⟶ (∀ x5 . prim1 x5 (5246e.. x0) ⟶ ∀ x6 . prim1 x6 (23e07.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x4) ⟶ e6316.. x0 x1 = 02a50.. x3 x4 ⟶ x2) ⟶ x2
Known e76d1.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (5246e.. x0) ⟶ ∀ x2 : ο . (80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x0 x1 ⟶ x2) ⟶ x2
Known c7cc7.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 x1 ⟶ 099f3.. x1 x2 ⟶ 099f3.. x0 x2
Theorem eb06e.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 : ο . (∀ x3 x4 . 02b90.. x3 x4 ⟶ (∀ x5 . prim1 x5 x3 ⟶ ∀ x6 : ο . (∀ x7 . prim1 x7 (23e07.. x0) ⟶ ∀ x8 . prim1 x8 (23e07.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ (∀ x7 . prim1 x7 (5246e.. x0) ⟶ ∀ x8 . prim1 x8 (5246e.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . prim1 x5 (23e07.. x0) ⟶ ∀ x6 . prim1 x6 (23e07.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x3) ⟶ (∀ x5 . prim1 x5 (5246e.. x0) ⟶ ∀ x6 . prim1 x6 (5246e.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x3) ⟶ (∀ x5 . prim1 x5 x4 ⟶ ∀ x6 : ο . (∀ x7 . prim1 x7 (23e07.. x0) ⟶ ∀ x8 . prim1 x8 (5246e.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ (∀ x7 . prim1 x7 (5246e.. x0) ⟶ ∀ x8 . prim1 x8 (23e07.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . prim1 x5 (23e07.. x0) ⟶ ∀ x6 . prim1 x6 (5246e.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x4) ⟶ (∀ x5 . prim1 x5 (5246e.. x0) ⟶ ∀ x6 . prim1 x6 (23e07.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x4) ⟶ e6316.. x0 x1 = 02a50.. x3 x4 ⟶ x2) ⟶ x2 (proof)
Theorem b4f65.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . (∀ x8 . prim1 x8 x6 ⟶ ∀ x9 : ο . (∀ x10 . prim1 x10 x2 ⟶ ∀ x11 . prim1 x11 x3 ⟶ x8 = bc82c.. (e6316.. x10 x1) (bc82c.. (e6316.. x0 x11) (f4dc0.. (e6316.. x10 x11))) ⟶ x9) ⟶ (∀ x10 . prim1 x10 x4 ⟶ ∀ x11 . prim1 x11 x5 ⟶ x8 = bc82c.. (e6316.. x10 x1) (bc82c.. (e6316.. x0 x11) (f4dc0.. (e6316.. x10 x11))) ⟶ x9) ⟶ x9) ⟶ (∀ x8 . prim1 x8 x2 ⟶ ∀ x9 . prim1 x9 x3 ⟶ prim1 (bc82c.. (e6316.. x8 x1) (bc82c.. (e6316.. x0 x9) (f4dc0.. (e6316.. x8 x9)))) x7) ⟶ (∀ x8 . prim1 x8 x4 ⟶ ∀ x9 . prim1 x9 x5 ⟶ prim1 (bc82c.. (e6316.. x8 x1) (bc82c.. (e6316.. x0 x9) (f4dc0.. (e6316.. x8 x9)))) x7) ⟶ Subq x6 x7 (proof)
Known bf919.. : 5246e.. 4a7ef.. = 4a7ef..
Known 3e9e2.. : 23e07.. 4a7ef.. = 4a7ef..
Theorem b92db.. : ∀ x0 . 80242.. x0 ⟶ e6316.. x0 4a7ef.. = 4a7ef.. (proof)
Param 56ded.. : ι → ι
Known 5ccff.. : ∀ x0 : ι → ο . (∀ x1 . 80242.. x1 ⟶ (∀ x2 . prim1 x2 (56ded.. (e4431.. x1)) ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . 80242.. x1 ⟶ x0 x1
Known f6a2d.. : ∀ x0 . 80242.. x0 ⟶ x0 = 02a50.. (23e07.. x0) (5246e.. x0)
Known 22361.. : ∀ x0 x1 x2 x3 . 02b90.. x0 x1 ⟶ 02b90.. x2 x3 ⟶ (∀ x4 . prim1 x4 x0 ⟶ 099f3.. x4 (02a50.. x2 x3)) ⟶ (∀ x4 . prim1 x4 x1 ⟶ 099f3.. (02a50.. x2 x3) x4) ⟶ (∀ x4 . prim1 x4 x2 ⟶ 099f3.. x4 (02a50.. x0 x1)) ⟶ (∀ x4 . prim1 x4 x3 ⟶ 099f3.. (02a50.. x0 x1) x4) ⟶ 02a50.. x0 x1 = 02a50.. x2 x3
Known 23b01.. : ∀ x0 . 80242.. x0 ⟶ 02b90.. (23e07.. x0) (5246e.. x0)
Known 0888b.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1)
Known b6795.. : f4dc0.. 4a7ef.. = 4a7ef..
Known 63df9.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (23e07.. x0) ⟶ prim1 x1 (56ded.. (e4431.. x0))
Known 9c8cc.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 . prim1 x2 x1 ⟶ 099f3.. (02a50.. x0 x1) x2
Known 54843.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (5246e.. x0) ⟶ prim1 x1 (56ded.. (e4431.. x0))
Theorem 0d1f9.. : ∀ x0 . 80242.. x0 ⟶ e6316.. x0 (4ae4a.. 4a7ef..) = x0 (proof)
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
Known eb5ba.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ bc82c.. x0 (bc82c.. x1 x2) = bc82c.. x1 (bc82c.. x0 x2)
Theorem 97a13.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ e6316.. x0 x1 = e6316.. x1 x0 (proof)
Param 94f9e.. : ι → (ι → ι) → ι
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Known 8948a.. : ∀ x0 . 80242.. x0 ⟶ f4dc0.. (f4dc0.. x0) = x0
Known 18a76.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x0 x1 ⟶ prim1 x1 (5246e.. x0)
Known 15454.. : ∀ x0 . 80242.. x0 ⟶ e4431.. (f4dc0.. x0) = e4431.. x0
Known 26c90.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 099f3.. x0 (f4dc0.. x1) ⟶ 099f3.. x1 (f4dc0.. x0)
Known d4781.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 099f3.. (f4dc0.. x0) x1 ⟶ 099f3.. (f4dc0.. x1) x0
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known 4d4af.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 099f3.. x0 x1 ⟶ 099f3.. (f4dc0.. x1) (f4dc0.. x0)
Known 3cd4e.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ f4dc0.. (02a50.. x0 x1) = 02a50.. (94f9e.. x1 f4dc0..) (94f9e.. x0 f4dc0..)
Theorem 5fabd.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ e6316.. (f4dc0.. x0) x1 = f4dc0.. (e6316.. x0 x1) (proof)