Proofgold Address

Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem 2911f.. : ∀ x0 . prim1 x0 (4ae4a.. 4a7ef..) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 x0 (proof)
Theorem 9f6cd.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 x0 (proof)
Theorem b1d09.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 x0 (proof)
Theorem aeaf9.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 x0 (proof)
Theorem 3cd21.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ x1 x0 (proof)
Theorem f5104.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ x1 x0 (proof)
Theorem e6eb7.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ x1 x0 (proof)
Theorem 0a0af.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) ⟶ x1 x0 (proof)
Theorem 0d7aa.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) ⟶ x1 x0 (proof)
Known 1b1d1.. : ∀ x0 . 4ae4a.. x0 = 4a7ef.. ⟶ ∀ x1 : ο . x1
Theorem 5c667.. : 4ae4a.. 4a7ef.. = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3a2b6.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Known 4b095.. : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ 4ae4a.. x0 = 4ae4a.. x1 ⟶ ∀ x2 : ο . x2
Theorem f9d2f.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 6afc6.. : nIn (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. 4a7ef..) (proof)
Theorem 57b7e.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem daead.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 0c325.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 37f0a.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem d1b49.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 05e02.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 2f510.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3dae7.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem a82a2.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7fa57.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 67cbd.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem e25a7.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem cdcd4.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 31e4d.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 5ccd2.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7357c.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem d13e3.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 2d896.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem ecc01.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem c6805.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 58158.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 16901.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem ee53e.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem ac13b.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 516c5.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 58716.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 19797.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 8fcc8.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem f5d01.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 622d4.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 17be6.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem cc164.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem c4f4e.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3babd.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem aa4ec.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 754ab.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 9be47.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0 (proof)
Theorem bf8a0.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem db57a.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 7a9d0.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem b1f45.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) ⟶ ∀ x0 : ο . x0 (proof)
Theorem 4dd03.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) ⟶ ∀ x0 : ο . x0 (proof)