Proofgold Address

Param and^and : ο → ο → ο
Definition 35624.. := λ x0 : (ι → ο) → ο . λ x1 : (ι → ι → ο) → ο . λ x2 . λ x3 x4 : ι → ι → ι . and (and (and (x0 (λ x5 . x3 x5 x2 = x5)) (x1 (λ x5 x6 . x3 x5 x6 = x3 x6 x5))) (x0 (λ x5 . x0 (λ x6 . x3 (x4 x5 x6) x6 = x5)))) (x0 (λ x5 . x0 (λ x6 . x4 (x3 x5 x6) x6 = x5)))
Param ap^ap : ι → ι → ι
Definition dc01f.. := λ x0 : (ι → ο) → ο . λ x1 : (ι → ι → ο) → ο . λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x13 . ap (ap (x12 (x12 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) (x12 x3 x7 x11 x4 x9 x8 x2 x5 x6 x10) (x12 x4 x11 x3 x7 x8 x10 x5 x6 x2 x9) (x12 x5 x4 x7 x3 x2 x9 x10 x11 x8 x6) (x12 x6 x9 x8 x2 x7 x4 x11 x10 x5 x3) (x12 x7 x8 x10 x9 x4 x6 x3 x2 x11 x5) (x12 x8 x2 x5 x10 x11 x3 x6 x4 x9 x7) (x12 x9 x5 x6 x11 x10 x2 x4 x7 x3 x8) (x12 x10 x6 x2 x8 x5 x11 x9 x3 x7 x4) (x12 x11 x10 x9 x6 x3 x5 x7 x8 x4 x2)) x13)
Definition 301ed.. := λ x0 : (ι → ο) → ο . λ x1 : (ι → ι → ο) → ο . λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x13 . ap (ap (x12 (x12 x2 x8 x10 x6 x5 x9 x3 x7 x4 x11) (x12 x3 x2 x4 x5 x11 x8 x7 x10 x9 x6) (x12 x4 x5 x2 x3 x7 x6 x9 x8 x11 x10) (x12 x5 x9 x8 x2 x10 x11 x4 x3 x6 x7) (x12 x6 x10 x9 x11 x2 x7 x8 x4 x3 x5) (x12 x7 x3 x5 x4 x6 x2 x11 x9 x10 x8) (x12 x8 x7 x6 x10 x4 x3 x2 x11 x5 x9) (x12 x9 x6 x11 x7 x3 x5 x10 x2 x8 x4) (x12 x10 x11 x7 x8 x9 x4 x5 x6 x2 x3) (x12 x11 x4 x3 x9 x8 x10 x6 x5 x7 x2)) x13)
Definition 5dfca.. := λ x0 : (ι → ο) → ο . λ x1 : (ι → ι → ο) → ο . λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x13 x14 : ι → ι → ι . λ x15 x16 x17 . x14 (x13 (x13 x17 x15) x16) (x13 x15 x16)
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem b7323.. : ∀ x0 : (ι → ο) → ο . ∀ x1 : (ι → ι → ο) → ο . ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . (∀ x12 : ι → ο . x12 x2 ⟶ x12 x3 ⟶ x12 x4 ⟶ x12 x5 ⟶ x12 x6 ⟶ x12 x7 ⟶ x12 x8 ⟶ x12 x9 ⟶ x12 x10 ⟶ x12 x11 ⟶ x0 x12) ⟶ (∀ x12 : ι → ι → ο . x12 x2 x2 ⟶ x12 x2 x3 ⟶ x12 x2 x4 ⟶ x12 x2 x5 ⟶ x12 x2 x6 ⟶ x12 x2 x7 ⟶ x12 x2 x8 ⟶ x12 x2 x9 ⟶ x12 x2 x10 ⟶ x12 x2 x11 ⟶ x12 x3 x2 ⟶ x12 x3 x3 ⟶ x12 x3 x4 ⟶ x12 x3 x5 ⟶ x12 x3 x6 ⟶ x12 x3 x7 ⟶ x12 x3 x8 ⟶ x12 x3 x9 ⟶ x12 x3 x10 ⟶ x12 x3 x11 ⟶ x12 x4 x2 ⟶ x12 x4 x3 ⟶ x12 x4 x4 ⟶ x12 x4 x5 ⟶ x12 x4 x6 ⟶ x12 x4 x7 ⟶ x12 x4 x8 ⟶ x12 x4 x9 ⟶ x12 x4 x10 ⟶ x12 x4 x11 ⟶ x12 x5 x2 ⟶ x12 x5 x3 ⟶ x12 x5 x4 ⟶ x12 x5 x5 ⟶ x12 x5 x6 ⟶ x12 x5 x7 ⟶ x12 x5 x8 ⟶ x12 x5 x9 ⟶ x12 x5 x10 ⟶ x12 x5 x11 ⟶ x12 x6 x2 ⟶ x12 x6 x3 ⟶ x12 x6 x4 ⟶ x12 x6 x5 ⟶ x12 x6 x6 ⟶ x12 x6 x7 ⟶ x12 x6 x8 ⟶ x12 x6 x9 ⟶ x12 x6 x10 ⟶ x12 x6 x11 ⟶ x12 x7 x2 ⟶ x12 x7 x3 ⟶ x12 x7 x4 ⟶ x12 x7 x5 ⟶ x12 x7 x6 ⟶ x12 x7 x7 ⟶ x12 x7 x8 ⟶ x12 x7 x9 ⟶ x12 x7 x10 ⟶ x12 x7 x11 ⟶ x12 x8 x2 ⟶ x12 x8 x3 ⟶ x12 x8 x4 ⟶ x12 x8 x5 ⟶ x12 x8 x6 ⟶ x12 x8 x7 ⟶ x12 x8 x8 ⟶ x12 x8 x9 ⟶ x12 x8 x10 ⟶ x12 x8 x11 ⟶ x12 x9 x2 ⟶ x12 x9 x3 ⟶ x12 x9 x4 ⟶ x12 x9 x5 ⟶ x12 x9 x6 ⟶ x12 x9 x7 ⟶ x12 x9 x8 ⟶ x12 x9 x9 ⟶ x12 x9 x10 ⟶ x12 x9 x11 ⟶ x12 x10 x2 ⟶ x12 x10 x3 ⟶ x12 x10 x4 ⟶ x12 x10 x5 ⟶ x12 x10 x6 ⟶ x12 x10 x7 ⟶ x12 x10 x8 ⟶ x12 x10 x9 ⟶ x12 x10 x10 ⟶ x12 x10 x11 ⟶ x12 x11 x2 ⟶ x12 x11 x3 ⟶ x12 x11 x4 ⟶ x12 x11 x5 ⟶ x12 x11 x6 ⟶ x12 x11 x7 ⟶ x12 x11 x8 ⟶ x12 x11 x9 ⟶ x12 x11 x10 ⟶ x12 x11 x11 ⟶ x0 (λ x13 . x0 (x12 x13))) ⟶ (∀ x12 : ι → ι → ο . x12 x2 x3 ⟶ x12 x2 x4 ⟶ x12 x3 x4 ⟶ x12 x2 x5 ⟶ x12 x3 x5 ⟶ x12 x4 x5 ⟶ x12 x2 x6 ⟶ x12 x3 x6 ⟶ x12 x4 x6 ⟶ x12 x5 x6 ⟶ x12 x2 x7 ⟶ x12 x3 x7 ⟶ x12 x4 x7 ⟶ x12 x5 x7 ⟶ x12 x6 x7 ⟶ x12 x2 x8 ⟶ x12 x3 x8 ⟶ x12 x4 x8 ⟶ x12 x5 x8 ⟶ x12 x6 x8 ⟶ x12 x7 x8 ⟶ x12 x2 x9 ⟶ x12 x3 x9 ⟶ x12 x4 x9 ⟶ x12 x5 x9 ⟶ x12 x6 x9 ⟶ x12 x7 x9 ⟶ x12 x8 x9 ⟶ x12 x2 x10 ⟶ x12 x3 x10 ⟶ x12 x4 x10 ⟶ x12 x5 x10 ⟶ x12 x6 x10 ⟶ x12 x7 x10 ⟶ x12 x8 x10 ⟶ x12 x9 x10 ⟶ x12 x2 x11 ⟶ x12 x3 x11 ⟶ x12 x4 x11 ⟶ x12 x5 x11 ⟶ x12 x6 x11 ⟶ x12 x7 x11 ⟶ x12 x8 x11 ⟶ x12 x9 x11 ⟶ x12 x10 x11 ⟶ x1 x12) ⟶ ∀ x12 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22) x2 = x13) ⟶ (∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22) x3 = x14) ⟶ (∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22) x4 = x15) ⟶ (∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22) x5 = x16) ⟶ (∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22) x6 = x17) ⟶ (∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22) x7 = x18) ⟶ (∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22) x8 = x19) ⟶ (∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22) x9 = x20) ⟶ (∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22) x10 = x21) ⟶ (∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . ap (x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22) x11 = x22) ⟶ ∀ x13 : ο . (∀ x14 : ι → ι → ι . (∀ x15 : ο . (∀ x16 : ι → ι → ι . and (and (35624.. x0 x1 x2 x14 x16) (5dfca.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x14 x16 x6 x4 (5dfca.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x14 x16 x7 x8 x7) = 5dfca.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x14 x16 x7 x8 (5dfca.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x14 x16 x6 x4 x7))) (∀ x17 : ο . (∀ x18 . (∀ x19 : ο . (∀ x20 . (∀ x21 : ο . (∀ x22 . (∀ x23 : ο . (∀ x24 . (∀ x25 : ο . (∀ x26 . and (x14 x24 (x14 (x14 (x16 x2 x22) (5dfca.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x14 x16 x18 x20 x22)) x26) = x3) (x14 (x14 x24 (x14 (x16 x2 x22) (5dfca.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x14 x16 x18 x20 x22))) x26 = x4) ⟶ x25) ⟶ x25) ⟶ x23) ⟶ x23) ⟶ x21) ⟶ x21) ⟶ x19) ⟶ x19) ⟶ x17) ⟶ x17) ⟶ x15) ⟶ x15) ⟶ x13) ⟶ x13 (proof)