Proofgold Address

Definition 236c6.. := prim1 (λ x0 . x0)
Known 9aea6.. : ∀ x0 x1 . ∀ x2 : ι → ι . prim0 x0 x1 = prim1 x2 ⟶ ∀ x3 : ο . x3
Theorem f558c.. : ∀ x0 x1 . 236c6.. = prim0 x0 x1 ⟶ ∀ x2 : ο . x2 (proof)
Known b4755.. : ∀ x0 x1 : ι → ι . prim1 x0 = prim1 x1 ⟶ x0 = x1
Theorem 148f8.. : ∀ x0 : ι → ι → ι . 236c6.. = prim1 (λ x2 . prim1 (x0 x2)) ⟶ ∀ x1 : ο . x1 (proof)
Theorem f2c23.. : ∀ x0 x1 : ι → ι . 236c6.. = prim1 (λ x3 . prim0 (x0 x3) (x1 x3)) ⟶ ∀ x2 : ο . x2 (proof)
Definition 57d6a.. := λ x0 x1 . prim0 236c6.. (prim0 x0 x1)
Definition 56103.. := λ x0 : ι → ι . prim0 236c6.. (prim1 x0)
Known 128d8.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ ∀ x4 : ο . (x0 = x2 ⟶ x1 = x3 ⟶ x4) ⟶ x4
Theorem 456ec.. : ∀ x0 x1 x2 x3 . 57d6a.. x0 x1 = 57d6a.. x2 x3 ⟶ ∀ x4 : ο . (x0 = x2 ⟶ x1 = x3 ⟶ x4) ⟶ x4 (proof)
Theorem c2c0d.. : ∀ x0 x1 : ι → ι . 56103.. x0 = 56103.. x1 ⟶ x0 = x1 (proof)
Theorem 59827.. : ∀ x0 x1 . ∀ x2 : ι → ι . 57d6a.. x0 x1 = 56103.. x2 ⟶ ∀ x3 : ο . x3 (proof)
Param de327.. : (ι → ο) → ι → ι → ο
Definition 707bb.. := λ x0 : ι → ο . λ x1 . ∀ x2 : (ι → ο) → ι → ο . (∀ x3 : ι → ο . ∀ x4 . x3 x4 ⟶ x2 x3 x4) ⟶ (∀ x3 : ι → ο . ∀ x4 : ι → ι . (∀ x5 . x2 (de327.. x3 x5) (x4 x5)) ⟶ x2 x3 (56103.. x4)) ⟶ (∀ x3 : ι → ο . ∀ x4 x5 . x2 x3 x4 ⟶ x2 x3 x5 ⟶ x2 x3 (57d6a.. x4 x5)) ⟶ x2 x0 x1
Theorem 05f2a.. : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ 707bb.. x0 x1 (proof)
Theorem 62e33.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . (∀ x2 . 707bb.. (de327.. x0 x2) (x1 x2)) ⟶ 707bb.. x0 (56103.. x1) (proof)
Theorem 2da01.. : ∀ x0 : ι → ο . ∀ x1 x2 . 707bb.. x0 x1 ⟶ 707bb.. x0 x2 ⟶ 707bb.. x0 (57d6a.. x1 x2) (proof)
Definition 4b3e1.. := λ x0 : ι → ο . λ x1 x2 . ∀ x3 : (ι → ο) → ι → ι → ο . (∀ x4 : ι → ο . ∀ x5 : ι → ι . ∀ x6 . (∀ x7 . 707bb.. (de327.. x4 x7) (x5 x7)) ⟶ 707bb.. x4 x6 ⟶ x3 x4 (57d6a.. (56103.. x5) x6) (x5 x6)) ⟶ (∀ x4 : ι → ο . ∀ x5 x6 : ι → ι . (∀ x7 . x3 (de327.. x4 x7) (x5 x7) (x6 x7)) ⟶ x3 x4 (56103.. x5) (56103.. x6)) ⟶ (∀ x4 : ι → ο . ∀ x5 x6 x7 . x3 x4 x5 x7 ⟶ 707bb.. x4 x6 ⟶ x3 x4 (57d6a.. x5 x6) (57d6a.. x7 x6)) ⟶ (∀ x4 : ι → ο . ∀ x5 x6 x7 . x3 x4 x6 x7 ⟶ 707bb.. x4 x5 ⟶ x3 x4 (57d6a.. x5 x6) (57d6a.. x5 x7)) ⟶ x3 x0 x1 x2
Theorem 45772.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . 707bb.. (de327.. x0 x3) (x1 x3)) ⟶ 707bb.. x0 x2 ⟶ 4b3e1.. x0 (57d6a.. (56103.. x1) x2) (x1 x2) (proof)
Theorem 9a3a3.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι . (∀ x3 . 4b3e1.. (de327.. x0 x3) (x1 x3) (x2 x3)) ⟶ 4b3e1.. x0 (56103.. x1) (56103.. x2) (proof)
Theorem b7449.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 . 4b3e1.. x0 x1 x3 ⟶ 707bb.. x0 x2 ⟶ 4b3e1.. x0 (57d6a.. x1 x2) (57d6a.. x3 x2) (proof)
Theorem c99f6.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 . 4b3e1.. x0 x2 x3 ⟶ 707bb.. x0 x1 ⟶ 4b3e1.. x0 (57d6a.. x1 x2) (57d6a.. x1 x3) (proof)
Definition 8e91b.. := λ x0 : ι → ι → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x0 x4 x5 ⟶ x3 x4 x5) ⟶ (∀ x4 x5 x6 . x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6) ⟶ x3 x1 x2
Theorem fed74.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x0 x1 x2 ⟶ 8e91b.. x0 x1 x2 (proof)
Theorem 8a0cb.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 x3 . 8e91b.. x0 x1 x2 ⟶ 8e91b.. x0 x2 x3 ⟶ 8e91b.. x0 x1 x3 (proof)
Definition 316b1.. := λ x0 : ι → ο . 8e91b.. (4b3e1.. x0)
Theorem f8636.. : ∀ x0 : ι → ο . ∀ x1 x2 . 4b3e1.. x0 x1 x2 ⟶ 316b1.. x0 x1 x2 (proof)
Theorem 0e197.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . 707bb.. (de327.. x0 x3) (x1 x3)) ⟶ 707bb.. x0 x2 ⟶ 316b1.. x0 (57d6a.. (56103.. x1) x2) (x1 x2) (proof)
Theorem c4cc0.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 . 316b1.. x0 x1 x2 ⟶ 316b1.. x0 x2 x3 ⟶ 316b1.. x0 x1 x3 (proof)
Definition df3ca.. := λ x0 : ι → ο . λ x1 : ι → ι → ο . λ x2 x3 . ∀ x4 : ι → ι → ο . (∀ x5 x6 . x1 x5 x6 ⟶ x4 x5 x6) ⟶ (∀ x5 . x0 x5 ⟶ x4 x5 x5) ⟶ (∀ x5 x6 . x4 x5 x6 ⟶ x4 x6 x5) ⟶ (∀ x5 x6 x7 . x4 x5 x6 ⟶ x4 x6 x7 ⟶ x4 x5 x7) ⟶ x4 x2 x3
Theorem 39a1f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . ∀ x2 x3 . x1 x2 x3 ⟶ df3ca.. x0 x1 x2 x3 (proof)
Theorem a286a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . ∀ x2 . x0 x2 ⟶ df3ca.. x0 x1 x2 x2 (proof)
Theorem 1868b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . ∀ x2 x3 . df3ca.. x0 x1 x2 x3 ⟶ df3ca.. x0 x1 x3 x2 (proof)
Theorem 8d17d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . ∀ x2 x3 x4 . df3ca.. x0 x1 x2 x3 ⟶ df3ca.. x0 x1 x3 x4 ⟶ df3ca.. x0 x1 x2 x4 (proof)
Definition d701e.. := λ x0 : ι → ο . df3ca.. (707bb.. x0) (4b3e1.. x0)
Theorem d6b7f.. : ∀ x0 : ι → ο . ∀ x1 x2 . 4b3e1.. x0 x1 x2 ⟶ d701e.. x0 x1 x2 (proof)
Theorem 03c76.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . 707bb.. (de327.. x0 x3) (x1 x3)) ⟶ 707bb.. x0 x2 ⟶ d701e.. x0 (57d6a.. (56103.. x1) x2) (x1 x2) (proof)
Theorem 3d3ad.. : ∀ x0 : ι → ο . ∀ x1 . 707bb.. x0 x1 ⟶ d701e.. x0 x1 x1 (proof)
Theorem a95d2.. : ∀ x0 : ι → ο . ∀ x1 x2 . d701e.. x0 x1 x2 ⟶ d701e.. x0 x2 x1 (proof)
Theorem 553b7.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 . d701e.. x0 x1 x2 ⟶ d701e.. x0 x2 x3 ⟶ d701e.. x0 x1 x3 (proof)
Param and : ο → ο → ο
Param 8ac9a.. : ι → ο
Conjecture 90489.. : ∀ x0 : ο . (∀ x1 . and (707bb.. 8ac9a.. x1) (∀ x2 . d701e.. (de327.. 8ac9a.. x2) (57d6a.. x1 x2) x2) ⟶ x0) ⟶ x0
Conjecture 1dd60.. : ∀ x0 : ο . (∀ x1 . and (707bb.. 8ac9a.. x1) (∀ x2 . d701e.. (de327.. 8ac9a.. x2) (57d6a.. x1 x2) (57d6a.. x2 (57d6a.. x1 x2))) ⟶ x0) ⟶ x0