Proofgold Address

Param 236c6.. : ι
Definition 07017.. := λ x0 . x0 = 236c6..
Definition 0b8ef.. := prim0 (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0)))
Definition 6c5f4.. := prim0 (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim1 (λ x0 . x0)))
Known 93754.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ x1 = x3
Theorem 3a245.. : ∀ x0 x1 . 0b8ef.. x0 = 0b8ef.. x1 ⟶ x0 = x1 (proof)
Theorem cc192.. : ∀ x0 x1 . 6c5f4.. x0 = 6c5f4.. x1 ⟶ x0 = x1 (proof)
Known 50787.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ x0 = x2
Definition False := ∀ x0 : ο . x0
Known 0286c.. : ∀ x0 x1 . prim0 x0 x1 = 236c6.. ⟶ False
Known db6fe.. : ∀ x0 x1 : ι → ι . ∀ x2 . prim1 x0 = prim1 x1 ⟶ x0 x2 = x1 x2
Theorem 88d35.. : ∀ x0 x1 . 0b8ef.. x0 = 6c5f4.. x1 ⟶ ∀ x2 : ο . x2 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition c0709.. := λ x0 x1 : ι → ο . λ x2 . or (∀ x3 : ο . (∀ x4 . and (x0 x4) (x2 = 0b8ef.. x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (x1 x4) (x2 = 6c5f4.. x4) ⟶ x3) ⟶ x3)
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 5c8d7.. : ∀ x0 x1 : ι → ο . ∀ x2 . x0 x2 ⟶ c0709.. x0 x1 (0b8ef.. x2) (proof)
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem f3d9f.. : ∀ x0 x1 : ι → ο . ∀ x2 . x1 x2 ⟶ c0709.. x0 x1 (6c5f4.. x2) (proof)
Theorem 8b44a.. : ∀ x0 x1 : ι → ο . ∀ x2 . c0709.. x0 x1 x2 ⟶ ∀ x3 : ι → ο . (∀ x4 . x0 x4 ⟶ x3 (0b8ef.. x4)) ⟶ (∀ x4 . x1 x4 ⟶ x3 (6c5f4.. x4)) ⟶ x3 x2 (proof)
Definition cfc98.. := λ x0 x1 . prim0 (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim1 (λ x2 . x2))) (prim0 x0 x1)
Known 128d8.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ ∀ x4 : ο . (x0 = x2 ⟶ x1 = x3 ⟶ x4) ⟶ x4
Theorem 3a4f6.. : ∀ x0 x1 x2 x3 . cfc98.. x0 x1 = cfc98.. x2 x3 ⟶ and (x0 = x2) (x1 = x3) (proof)
Definition 6e020.. := λ x0 x1 : ι → ο . λ x2 . ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . and (and (x0 x4) (x1 x6)) (x2 = cfc98.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 024d1.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 . x0 x2 ⟶ x1 x3 ⟶ 6e020.. x0 x1 (cfc98.. x2 x3) (proof)
Theorem 78238.. : ∀ x0 x1 : ι → ο . ∀ x2 . 6e020.. x0 x1 x2 ⟶ ∀ x3 : ι → ο . (∀ x4 x5 . x0 x4 ⟶ x1 x5 ⟶ x3 (cfc98.. x4 x5)) ⟶ x3 x2 (proof)
Param 5e331.. : ι
Param a3eb9.. : ι → ι → ι
Param bf68c.. : ι → ι → ι
Definition 858ff.. := λ x0 . λ x1 : ι → ο . ∀ x2 : ι → (ι → ο) → ο . x2 5e331.. 07017.. ⟶ (∀ x3 x4 . ∀ x5 x6 : ι → ο . x2 x3 x5 ⟶ x2 x4 x6 ⟶ x2 (a3eb9.. x3 x4) (c0709.. x5 x6)) ⟶ (∀ x3 x4 . ∀ x5 x6 : ι → ο . x2 x3 x5 ⟶ x2 x4 x6 ⟶ x2 (bf68c.. x3 x4) (6e020.. x5 x6)) ⟶ x2 x0 x1
Theorem fb7af.. : 858ff.. 5e331.. 07017.. (proof)
Theorem fc3cd.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . 858ff.. x0 x2 ⟶ 858ff.. x1 x3 ⟶ 858ff.. (a3eb9.. x0 x1) (c0709.. x2 x3) (proof)
Theorem 57d3c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . 858ff.. x0 x2 ⟶ 858ff.. x1 x3 ⟶ 858ff.. (bf68c.. x0 x1) (6e020.. x2 x3) (proof)
Param 74e69.. : ι → ο
Known facf7.. : ∀ x0 : ι → ο . x0 5e331.. ⟶ (∀ x1 x2 . 74e69.. x1 ⟶ x0 x1 ⟶ 74e69.. x2 ⟶ x0 x2 ⟶ x0 (a3eb9.. x1 x2)) ⟶ (∀ x1 x2 . 74e69.. x1 ⟶ x0 x1 ⟶ 74e69.. x2 ⟶ x0 x2 ⟶ x0 (bf68c.. x1 x2)) ⟶ ∀ x1 . 74e69.. x1 ⟶ x0 x1
Theorem 41bc1.. : ∀ x0 . 74e69.. x0 ⟶ ∀ x1 : ο . (∀ x2 : ι → ο . 858ff.. x0 x2 ⟶ x1) ⟶ x1 (proof)
Theorem 1aee4.. : ∀ x0 : ι → (ι → ο) → ο . x0 5e331.. 07017.. ⟶ (∀ x1 x2 . ∀ x3 x4 : ι → ο . 858ff.. x1 x3 ⟶ x0 x1 x3 ⟶ 858ff.. x2 x4 ⟶ x0 x2 x4 ⟶ x0 (a3eb9.. x1 x2) (c0709.. x3 x4)) ⟶ (∀ x1 x2 . ∀ x3 x4 : ι → ο . 858ff.. x1 x3 ⟶ x0 x1 x3 ⟶ 858ff.. x2 x4 ⟶ x0 x2 x4 ⟶ x0 (bf68c.. x1 x2) (6e020.. x3 x4)) ⟶ ∀ x1 . ∀ x2 : ι → ο . 858ff.. x1 x2 ⟶ x0 x1 x2 (proof)
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known 9ec26.. : ∀ x0 x1 . 5e331.. = a3eb9.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 59f91.. : ∀ x0 x1 . 5e331.. = bf68c.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 5e750.. : ∀ x0 x1 x2 x3 . a3eb9.. x0 x1 = a3eb9.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known a8e2e.. : ∀ x0 x1 x2 x3 . a3eb9.. x0 x1 = bf68c.. x2 x3 ⟶ ∀ x4 : ο . x4
Known 2f86f.. : ∀ x0 x1 x2 x3 . bf68c.. x0 x1 = bf68c.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Theorem 21067.. : ∀ x0 . ∀ x1 : ι → ο . 858ff.. x0 x1 ⟶ ∀ x2 . ∀ x3 : ι → ο . 858ff.. x2 x3 ⟶ x0 = x2 ⟶ x1 = x3 (proof)
Theorem e3e6f.. : ∀ x0 . ∀ x1 x2 : ι → ο . 858ff.. x0 x1 ⟶ 858ff.. x0 x2 ⟶ x1 = x2 (proof)
Theorem 98718.. : ∀ x0 . ∀ x1 : ι → ο . 858ff.. x0 x1 ⟶ ∀ x2 : ο . (x0 = 5e331.. ⟶ x1 = 07017.. ⟶ x2) ⟶ (∀ x3 x4 . ∀ x5 x6 : ι → ο . 858ff.. x3 x5 ⟶ 858ff.. x4 x6 ⟶ x0 = a3eb9.. x3 x4 ⟶ x1 = c0709.. x5 x6 ⟶ x2) ⟶ (∀ x3 x4 . ∀ x5 x6 : ι → ο . 858ff.. x3 x5 ⟶ 858ff.. x4 x6 ⟶ x0 = bf68c.. x3 x4 ⟶ x1 = 6e020.. x5 x6 ⟶ x2) ⟶ x2 (proof)
Theorem b4c82.. : ∀ x0 x1 . ∀ x2 : ι → ο . 858ff.. (a3eb9.. x0 x1) x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ο . (∀ x5 : ο . (∀ x6 : ι → ο . and (and (858ff.. x0 x4) (858ff.. x1 x6)) (x2 = c0709.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Theorem 2156c.. : ∀ x0 x1 . ∀ x2 : ι → ο . 858ff.. (bf68c.. x0 x1) x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ο . (∀ x5 : ο . (∀ x6 : ι → ο . and (and (858ff.. x0 x4) (858ff.. x1 x6)) (x2 = 6e020.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Param c4def.. : ι
Param 6b90c.. : ι → ι → ι
Param c9248.. : ι
Param a6e19.. : ι → ι
Param 2fe34.. : ι → ι
Param e05e6.. : ι → ο
Param 3e00e.. : ι → ι → ι
Param f9341.. : ι → ι → ι
Param 1fa6d.. : ι → ι
Param 3a365.. : ι → ι
Definition d7d78.. := λ x0 x1 x2 . ∀ x3 : ι → ι → ι → ο . (∀ x4 . x3 c4def.. x4 x4) ⟶ (∀ x4 x5 x6 x7 x8 . x3 x4 x6 x7 ⟶ x3 x5 x7 x8 ⟶ x3 (6b90c.. x4 x5) x6 x8) ⟶ (∀ x4 . x3 c9248.. x4 236c6..) ⟶ (∀ x4 x5 x6 . x3 x4 x5 x6 ⟶ x3 (a6e19.. x4) x5 (0b8ef.. x6)) ⟶ (∀ x4 x5 x6 . x3 x4 x5 x6 ⟶ x3 (2fe34.. x4) x5 (6c5f4.. x6)) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x5 ⟶ x3 x4 (cfc98.. x6 x7) x8 ⟶ x3 (3e00e.. x4 x5) (cfc98.. (0b8ef.. x6) x7) x8) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x4 ⟶ x3 x5 (cfc98.. x6 x7) x8 ⟶ x3 (3e00e.. x4 x5) (cfc98.. (6c5f4.. x6) x7) x8) ⟶ (∀ x4 x5 x6 x7 x8 . x3 x4 x6 x7 ⟶ x3 x5 x6 x8 ⟶ x3 (f9341.. x4 x5) x6 (cfc98.. x7 x8)) ⟶ (∀ x4 x5 x6 x7 . x3 x4 x5 x7 ⟶ x3 (1fa6d.. x4) (cfc98.. x5 x6) x7) ⟶ (∀ x4 x5 x6 x7 . x3 x4 x6 x7 ⟶ x3 (3a365.. x4) (cfc98.. x5 x6) x7) ⟶ x3 x0 x1 x2
Theorem 4a83c.. : ∀ x0 . d7d78.. c4def.. x0 x0 (proof)
Theorem 3e6f8.. : ∀ x0 x1 x2 x3 x4 . d7d78.. x0 x2 x3 ⟶ d7d78.. x1 x3 x4 ⟶ d7d78.. (6b90c.. x0 x1) x2 x4 (proof)
Theorem b6648.. : ∀ x0 . d7d78.. c9248.. x0 236c6.. (proof)
Theorem c8e20.. : ∀ x0 x1 x2 . d7d78.. x0 x1 x2 ⟶ d7d78.. (a6e19.. x0) x1 (0b8ef.. x2) (proof)
Theorem ca73c.. : ∀ x0 x1 x2 . d7d78.. x0 x1 x2 ⟶ d7d78.. (2fe34.. x0) x1 (6c5f4.. x2) (proof)
Theorem 547ca.. : ∀ x0 x1 x2 x3 x4 . e05e6.. x1 ⟶ d7d78.. x0 (cfc98.. x2 x3) x4 ⟶ d7d78.. (3e00e.. x0 x1) (cfc98.. (0b8ef.. x2) x3) x4 (proof)
Theorem 2011d.. : ∀ x0 x1 x2 x3 x4 . e05e6.. x0 ⟶ d7d78.. x1 (cfc98.. x2 x3) x4 ⟶ d7d78.. (3e00e.. x0 x1) (cfc98.. (6c5f4.. x2) x3) x4 (proof)
Theorem 092f4.. : ∀ x0 x1 x2 x3 x4 . d7d78.. x0 x2 x3 ⟶ d7d78.. x1 x2 x4 ⟶ d7d78.. (f9341.. x0 x1) x2 (cfc98.. x3 x4) (proof)
Theorem d0180.. : ∀ x0 x1 x2 x3 . d7d78.. x0 x1 x3 ⟶ d7d78.. (1fa6d.. x0) (cfc98.. x1 x2) x3 (proof)
Theorem 214ce.. : ∀ x0 x1 x2 x3 . d7d78.. x0 x2 x3 ⟶ d7d78.. (3a365.. x0) (cfc98.. x1 x2) x3 (proof)
Theorem 4bdfc.. : ∀ x0 : ι → ι → ι → ο . (∀ x1 . d7d78.. c4def.. x1 x1 ⟶ x0 c4def.. x1 x1) ⟶ (∀ x1 x2 x3 x4 x5 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ d7d78.. x2 x4 x5 ⟶ x0 x2 x4 x5 ⟶ x0 (6b90c.. x1 x2) x3 x5) ⟶ (∀ x1 . d7d78.. c9248.. x1 236c6.. ⟶ x0 c9248.. x1 236c6..) ⟶ (∀ x1 x2 x3 . d7d78.. x1 x2 x3 ⟶ x0 x1 x2 x3 ⟶ x0 (a6e19.. x1) x2 (0b8ef.. x3)) ⟶ (∀ x1 x2 x3 . d7d78.. x1 x2 x3 ⟶ x0 x1 x2 x3 ⟶ x0 (2fe34.. x1) x2 (6c5f4.. x3)) ⟶ (∀ x1 x2 x3 x4 x5 . e05e6.. x2 ⟶ d7d78.. x1 (cfc98.. x3 x4) x5 ⟶ x0 x1 (cfc98.. x3 x4) x5 ⟶ x0 (3e00e.. x1 x2) (cfc98.. (0b8ef.. x3) x4) x5) ⟶ (∀ x1 x2 x3 x4 x5 . e05e6.. x1 ⟶ d7d78.. x2 (cfc98.. x3 x4) x5 ⟶ x0 x2 (cfc98.. x3 x4) x5 ⟶ x0 (3e00e.. x1 x2) (cfc98.. (6c5f4.. x3) x4) x5) ⟶ (∀ x1 x2 x3 x4 x5 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ d7d78.. x2 x3 x5 ⟶ x0 x2 x3 x5 ⟶ x0 (f9341.. x1 x2) x3 (cfc98.. x4 x5)) ⟶ (∀ x1 x2 x3 x4 . d7d78.. x1 x2 x4 ⟶ x0 x1 x2 x4 ⟶ x0 (1fa6d.. x1) (cfc98.. x2 x3) x4) ⟶ (∀ x1 x2 x3 x4 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ x0 (3a365.. x1) (cfc98.. x2 x3) x4) ⟶ ∀ x1 x2 x3 . d7d78.. x1 x2 x3 ⟶ x0 x1 x2 x3 (proof)
Theorem 16c10.. : ∀ x0 x1 x2 . d7d78.. x0 x1 x2 ⟶ ∀ x3 : ο . (x0 = c4def.. ⟶ x1 = x2 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . d7d78.. x4 x6 x7 ⟶ d7d78.. x5 x7 x8 ⟶ x0 = 6b90c.. x4 x5 ⟶ x1 = x6 ⟶ x2 = x8 ⟶ x3) ⟶ (x0 = c9248.. ⟶ x2 = 236c6.. ⟶ x3) ⟶ (∀ x4 x5 x6 . d7d78.. x4 x5 x6 ⟶ x0 = a6e19.. x4 ⟶ x1 = x5 ⟶ x2 = 0b8ef.. x6 ⟶ x3) ⟶ (∀ x4 x5 x6 . d7d78.. x4 x5 x6 ⟶ x0 = 2fe34.. x4 ⟶ x1 = x5 ⟶ x2 = 6c5f4.. x6 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x5 ⟶ d7d78.. x4 (cfc98.. x6 x7) x8 ⟶ x0 = 3e00e.. x4 x5 ⟶ x1 = cfc98.. (0b8ef.. x6) x7 ⟶ x2 = x8 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x4 ⟶ d7d78.. x5 (cfc98.. x6 x7) x8 ⟶ x0 = 3e00e.. x4 x5 ⟶ x1 = cfc98.. (6c5f4.. x6) x7 ⟶ x2 = x8 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 x8 . d7d78.. x4 x6 x7 ⟶ d7d78.. x5 x6 x8 ⟶ x0 = f9341.. x4 x5 ⟶ x1 = x6 ⟶ x2 = cfc98.. x7 x8 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 . d7d78.. x4 x5 x7 ⟶ x0 = 1fa6d.. x4 ⟶ x1 = cfc98.. x5 x6 ⟶ x2 = x7 ⟶ x3) ⟶ (∀ x4 x5 x6 x7 . d7d78.. x4 x6 x7 ⟶ x0 = 3a365.. x4 ⟶ x1 = cfc98.. x5 x6 ⟶ x2 = x7 ⟶ x3) ⟶ x3 (proof)
Known a3634.. : ∀ x0 x1 . c4def.. = 6b90c.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 5e60e.. : c4def.. = c9248.. ⟶ ∀ x0 : ο . x0
Known 924dd.. : ∀ x0 . c4def.. = a6e19.. x0 ⟶ ∀ x1 : ο . x1
Known 0cc7e.. : ∀ x0 . c4def.. = 2fe34.. x0 ⟶ ∀ x1 : ο . x1
Known 91964.. : ∀ x0 x1 . c4def.. = 3e00e.. x0 x1 ⟶ ∀ x2 : ο . x2
Known a14cf.. : ∀ x0 x1 . c4def.. = f9341.. x0 x1 ⟶ ∀ x2 : ο . x2
Known b8b08.. : ∀ x0 . c4def.. = 1fa6d.. x0 ⟶ ∀ x1 : ο . x1
Known f9749.. : ∀ x0 . c4def.. = 3a365.. x0 ⟶ ∀ x1 : ο . x1
Theorem b316e.. : ∀ x0 x1 . d7d78.. c4def.. x0 x1 ⟶ x0 = x1 (proof)
Known ffc37.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 6b90c.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known dc5ae.. : ∀ x0 x1 . 6b90c.. x0 x1 = c9248.. ⟶ ∀ x2 : ο . x2
Known a9278.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = a6e19.. x2 ⟶ ∀ x3 : ο . x3
Known dabcf.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 2fe34.. x2 ⟶ ∀ x3 : ο . x3
Known 07fb9.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 3e00e.. x2 x3 ⟶ ∀ x4 : ο . x4
Known 72b8e.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = f9341.. x2 x3 ⟶ ∀ x4 : ο . x4
Known 0a32f.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 1fa6d.. x2 ⟶ ∀ x3 : ο . x3
Known ff84b.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 3a365.. x2 ⟶ ∀ x3 : ο . x3
Theorem 8b3a5.. : ∀ x0 x1 x2 x3 . d7d78.. (6b90c.. x0 x1) x2 x3 ⟶ ∀ x4 : ο . (∀ x5 . and (d7d78.. x0 x2 x5) (d7d78.. x1 x5 x3) ⟶ x4) ⟶ x4 (proof)
Known 84bad.. : ∀ x0 . c9248.. = a6e19.. x0 ⟶ ∀ x1 : ο . x1
Known 1832c.. : ∀ x0 . c9248.. = 2fe34.. x0 ⟶ ∀ x1 : ο . x1
Known 77b59.. : ∀ x0 x1 . c9248.. = 3e00e.. x0 x1 ⟶ ∀ x2 : ο . x2
Known b728e.. : ∀ x0 x1 . c9248.. = f9341.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 0482c.. : ∀ x0 . c9248.. = 1fa6d.. x0 ⟶ ∀ x1 : ο . x1
Known 36b24.. : ∀ x0 . c9248.. = 3a365.. x0 ⟶ ∀ x1 : ο . x1
Theorem 84f7f.. : ∀ x0 x1 . d7d78.. c9248.. x0 x1 ⟶ x1 = 236c6.. (proof)
Known 84af1.. : ∀ x0 x1 . a6e19.. x0 = a6e19.. x1 ⟶ x0 = x1
Known 7241c.. : ∀ x0 x1 . a6e19.. x0 = 2fe34.. x1 ⟶ ∀ x2 : ο . x2
Known 62a09.. : ∀ x0 x1 x2 . a6e19.. x0 = 3e00e.. x1 x2 ⟶ ∀ x3 : ο . x3
Known cec81.. : ∀ x0 x1 x2 . a6e19.. x0 = f9341.. x1 x2 ⟶ ∀ x3 : ο . x3
Known 4bdb9.. : ∀ x0 x1 . a6e19.. x0 = 1fa6d.. x1 ⟶ ∀ x2 : ο . x2
Known 62476.. : ∀ x0 x1 . a6e19.. x0 = 3a365.. x1 ⟶ ∀ x2 : ο . x2
Theorem aca1a.. : ∀ x0 x1 x2 . d7d78.. (a6e19.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . and (d7d78.. x0 x1 x4) (x2 = 0b8ef.. x4) ⟶ x3) ⟶ x3 (proof)
Known 2eb6f.. : ∀ x0 x1 . 2fe34.. x0 = 2fe34.. x1 ⟶ x0 = x1
Known a0ec1.. : ∀ x0 x1 x2 . 2fe34.. x0 = 3e00e.. x1 x2 ⟶ ∀ x3 : ο . x3
Known becdb.. : ∀ x0 x1 x2 . 2fe34.. x0 = f9341.. x1 x2 ⟶ ∀ x3 : ο . x3
Known a5def.. : ∀ x0 x1 . 2fe34.. x0 = 1fa6d.. x1 ⟶ ∀ x2 : ο . x2
Known cdd8a.. : ∀ x0 x1 . 2fe34.. x0 = 3a365.. x1 ⟶ ∀ x2 : ο . x2
Theorem 42fd0.. : ∀ x0 x1 x2 . d7d78.. (2fe34.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . and (d7d78.. x0 x1 x4) (x2 = 6c5f4.. x4) ⟶ x3) ⟶ x3 (proof)
Known 42e43.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = 3e00e.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known a1a1b.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = f9341.. x2 x3 ⟶ ∀ x4 : ο . x4
Known 54459.. : ∀ x0 x1 x2 . 3e00e.. x0 x1 = 1fa6d.. x2 ⟶ ∀ x3 : ο . x3
Known fb77a.. : ∀ x0 x1 x2 . 3e00e.. x0 x1 = 3a365.. x2 ⟶ ∀ x3 : ο . x3
Theorem b4261.. : ∀ x0 x1 x2 x3 . d7d78.. (3e00e.. x0 x1) x2 x3 ⟶ or (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . and (x2 = cfc98.. (0b8ef.. x5) x7) (d7d78.. x0 (cfc98.. x5 x7) x3) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . and (x2 = cfc98.. (6c5f4.. x5) x7) (d7d78.. x1 (cfc98.. x5 x7) x3) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) (proof)
Known 063ac.. : ∀ x0 x1 x2 x3 . f9341.. x0 x1 = f9341.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known 38968.. : ∀ x0 x1 x2 . f9341.. x0 x1 = 1fa6d.. x2 ⟶ ∀ x3 : ο . x3
Known 6774e.. : ∀ x0 x1 x2 . f9341.. x0 x1 = 3a365.. x2 ⟶ ∀ x3 : ο . x3
Theorem 3f6f9.. : ∀ x0 x1 x2 x3 . d7d78.. (f9341.. x0 x1) x2 x3 ⟶ ∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . and (and (d7d78.. x0 x2 x5) (d7d78.. x1 x2 x7)) (x3 = cfc98.. x5 x7) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4 (proof)
Known a1c68.. : ∀ x0 x1 . 1fa6d.. x0 = 1fa6d.. x1 ⟶ x0 = x1
Known 9f429.. : ∀ x0 x1 . 1fa6d.. x0 = 3a365.. x1 ⟶ ∀ x2 : ο . x2
Theorem 17be7.. : ∀ x0 x1 x2 . d7d78.. (1fa6d.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . and (x1 = cfc98.. x4 x6) (d7d78.. x0 x4 x2) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Known f684d.. : ∀ x0 x1 . 3a365.. x0 = 3a365.. x1 ⟶ x0 = x1
Theorem efdff.. : ∀ x0 x1 x2 . d7d78.. (3a365.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . and (x1 = cfc98.. x4 x6) (d7d78.. x0 x6 x2) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Param 762f0.. : ι → ι → ι → ο
Conjecture 085db.. : ∀ x0 x1 x2 . 762f0.. x0 x1 x2 ⟶ ∀ x3 x4 : ι → ο . 858ff.. x1 x3 ⟶ 858ff.. x2 x4 ⟶ ∀ x5 x6 . x3 x5 ⟶ d7d78.. x0 x5 x6 ⟶ x4 x6
Definition 5dc8b.. := λ x0 x1 . and (∀ x2 . x0 = 0b8ef.. x2 ⟶ x1 = 6c5f4.. x2) (∀ x2 . x0 = 6c5f4.. x2 ⟶ x1 = 0b8ef.. x2)
Conjecture 181f2.. : ∀ x0 . 74e69.. x0 ⟶ ∀ x1 : ο . (∀ x2 . and (762f0.. x2 (a3eb9.. x0 x0) (a3eb9.. x0 x0)) (∀ x3 : ι → ο . 858ff.. x0 x3 ⟶ ∀ x4 x5 . c0709.. x3 x3 x4 ⟶ 5dc8b.. x4 x5 ⟶ d7d78.. x2 x4 x5) ⟶ x1) ⟶ x1