Proofgold Address

Param de327.. : (ι → ο) → ι → ι → ο
Param 56103.. : (ι → ι) → ι
Param 57d6a.. : ι → ι → ι
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
Known 62e33.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . (∀ x2 . 707bb.. (de327.. x0 x2) (x1 x2)) ⟶ 707bb.. x0 (56103.. x1)
Known 05f2a.. : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ 707bb.. x0 x1
Known f147c.. : ∀ x0 : ι → ο . ∀ x1 . de327.. x0 x1 x1
Theorem 76e10.. : ∀ x0 : ι → ο . 707bb.. x0 (56103.. (λ x1 . x1)) (proof)
Param and : ο → ο → ο
Param 8ac9a.. : ι → ο
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
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
Definition d701e.. := λ x0 : ι → ο . df3ca.. (707bb.. x0) (4b3e1.. x0)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 03c76.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . 707bb.. (de327.. x0 x3) (x1 x3)) ⟶ 707bb.. x0 x2 ⟶ d701e.. x0 (57d6a.. (56103.. x1) x2) (x1 x2)
Theorem 90489.. : ∀ x0 : ο . (∀ x1 . and (707bb.. 8ac9a.. x1) (∀ x2 . d701e.. (de327.. 8ac9a.. x2) (57d6a.. x1 x2) x2) ⟶ x0) ⟶ x0 (proof)
Known 2da01.. : ∀ x0 : ι → ο . ∀ x1 x2 . 707bb.. x0 x1 ⟶ 707bb.. x0 x2 ⟶ 707bb.. x0 (57d6a.. x1 x2)
Known 553b7.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 . d701e.. x0 x1 x2 ⟶ d701e.. x0 x2 x3 ⟶ d701e.. x0 x1 x3
Known a95d2.. : ∀ x0 : ι → ο . ∀ x1 x2 . d701e.. x0 x1 x2 ⟶ d701e.. x0 x2 x1
Known d6b7f.. : ∀ x0 : ι → ο . ∀ x1 x2 . 4b3e1.. x0 x1 x2 ⟶ d701e.. x0 x1 x2
Known c99f6.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 . 4b3e1.. x0 x2 x3 ⟶ 707bb.. x0 x1 ⟶ 4b3e1.. x0 (57d6a.. x1 x2) (57d6a.. x1 x3)
Known 45772.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . 707bb.. (de327.. x0 x3) (x1 x3)) ⟶ 707bb.. x0 x2 ⟶ 4b3e1.. x0 (57d6a.. (56103.. x1) x2) (x1 x2)
Known 0998e.. : ∀ x0 : ι → ο . ∀ x1 x2 . x0 x2 ⟶ de327.. x0 x1 x2
Theorem 1dd60.. : ∀ x0 : ο . (∀ x1 . and (707bb.. 8ac9a.. x1) (∀ x2 . d701e.. (de327.. 8ac9a.. x2) (57d6a.. x1 x2) (57d6a.. x2 (57d6a.. x1 x2))) ⟶ x0) ⟶ x0 (proof)