Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 1d20f.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ο . ∀ x4 . ∀ x5 x6 : ι → ο . ∀ x7 x8 x9 . ∀ x10 : ι → ι → ι → ι → ι . ∀ x11 : ι → ι → ι . ∀ x12 : ι → ο . ∀ x13 x14 . ∀ x15 x16 : ι → ι . ∀ x17 x18 : ι → ι → ι → ι . ∀ x19 : ι → ι → ι . ∀ x20 : ι → ι → ι → ι . ∀ x21 : ι → ι . ∀ x22 x23 : ι → ι → ι . ∀ x24 : ι → ι . ∀ x25 x26 x27 . ∀ x28 : ι → ο . ∀ x29 . ∀ x30 : ι → ο . ∀ x31 . ∀ x32 : ι → ο . ∀ x33 . ∀ x34 : ι → ο . (∀ x35 x36 . x34 x36 ⟶ (x36 = x35 ⟶ False) ⟶ x34 x35 ⟶ False) ⟶ (∀ x35 x36 . x0 x35 x36 ⟶ x34 x36 ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x35 = x33 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x0 x35 x36 ⟶ x2 x36 (x1 x37) ⟶ x34 x37 ⟶ False) ⟶ (∀ x35 x36 x37 . x0 x36 x37 ⟶ x2 x37 (x1 x35) ⟶ (x2 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x3 x36 x35 ⟶ (x2 x36 (x1 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x2 x36 (x1 x35) ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x2 x35 x36 ⟶ (x34 x36 ⟶ False) ⟶ (x0 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 x36 x35 ⟶ (x2 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x3 x35 x35 ⟶ False) ⟶ False) ⟶ (x32 x31 ⟶ False) ⟶ (x34 x4 ⟶ False) ⟶ ((x30 x29 ⟶ False) ⟶ False) ⟶ ((x5 x29 ⟶ False) ⟶ False) ⟶ ((x28 x27 ⟶ False) ⟶ False) ⟶ ((x6 x27 ⟶ False) ⟶ False) ⟶ ((x5 x27 ⟶ False) ⟶ False) ⟶ ((x32 x7 ⟶ False) ⟶ False) ⟶ (x34 x7 ⟶ False) ⟶ ((x34 x8 ⟶ False) ⟶ False) ⟶ ((x5 x26 ⟶ False) ⟶ False) ⟶ (x34 x26 ⟶ False) ⟶ ((x6 x25 ⟶ False) ⟶ False) ⟶ ((x5 x25 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x34 x35 ⟶ False) ⟶ x5 x35 ⟶ x34 (x24 x35) ⟶ False) ⟶ (∀ x35 . x32 x35 ⟶ x5 x35 ⟶ (x32 (x24 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x34 x36 ⟶ x5 x36 ⟶ (x34 (x23 x36 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x5 x36 ⟶ x34 x35 ⟶ (x34 (x23 x36 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x34 x36 ⟶ x5 x36 ⟶ (x34 (x22 x36 x35) ⟶ False) ⟶ False) ⟶ ((x34 x33 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x5 x36 ⟶ x34 x35 ⟶ (x34 (x22 x36 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x34 (x24 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 . (x2 (x21 x35) x35 ⟶ False) ⟶ False) ⟶ ((x34 x9 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x5 x37 ⟶ x6 x37 ⟶ (x0 (x19 x37 (x20 x35 x36 x37)) x36 ⟶ False) ⟶ (x0 (x20 x35 x36 x37) x35 ⟶ False) ⟶ (x35 = x23 x37 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x5 x37 ⟶ x6 x37 ⟶ (x0 (x20 x35 x36 x37) (x24 x37) ⟶ False) ⟶ (x0 (x20 x35 x36 x37) x35 ⟶ False) ⟶ (x35 = x23 x37 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x5 x37 ⟶ x6 x37 ⟶ x0 (x20 x35 x36 x37) x35 ⟶ x0 (x20 x35 x36 x37) (x24 x37) ⟶ x0 (x19 x37 (x20 x35 x36 x37)) x36 ⟶ (x35 = x23 x37 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x5 x38 ⟶ x6 x38 ⟶ x37 = x23 x38 x36 ⟶ x0 x35 (x24 x38) ⟶ x0 (x19 x38 x35) x36 ⟶ (x0 x35 x37 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x5 x38 ⟶ x6 x38 ⟶ x37 = x23 x38 x36 ⟶ x0 x35 x37 ⟶ (x0 (x19 x38 x35) x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x5 x38 ⟶ x6 x38 ⟶ x36 = x23 x38 x35 ⟶ x0 x37 x36 ⟶ (x0 x37 (x24 x38) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x5 x37 ⟶ x6 x37 ⟶ (x18 x35 x36 x37 = x19 x37 (x17 x35 x36 x37) ⟶ False) ⟶ (x0 (x18 x35 x36 x37) x35 ⟶ False) ⟶ (x35 = x22 x37 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x5 x37 ⟶ x6 x37 ⟶ (x0 (x17 x35 x36 x37) x36 ⟶ False) ⟶ (x0 (x18 x35 x36 x37) x35 ⟶ False) ⟶ (x35 = x22 x37 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x5 x37 ⟶ x6 x37 ⟶ (x0 (x17 x35 x36 x37) (x24 x37) ⟶ False) ⟶ (x0 (x18 x35 x36 x37) x35 ⟶ False) ⟶ (x35 = x22 x37 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x5 x38 ⟶ x6 x38 ⟶ x0 (x18 x37 x36 x38) x37 ⟶ x0 x35 (x24 x38) ⟶ x0 x35 x36 ⟶ x18 x37 x36 x38 = x19 x38 x35 ⟶ (x37 = x22 x38 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 x39 . x5 x39 ⟶ x6 x39 ⟶ x38 = x22 x39 x37 ⟶ x0 x35 (x24 x39) ⟶ x0 x35 x37 ⟶ x36 = x19 x39 x35 ⟶ (x0 x36 x38 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x5 x38 ⟶ x6 x38 ⟶ x37 = x22 x38 x36 ⟶ x0 x35 x37 ⟶ (x35 = x19 x38 (x10 x35 x37 x36 x38) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x5 x38 ⟶ x6 x38 ⟶ x37 = x22 x38 x36 ⟶ x0 x35 x37 ⟶ (x0 (x10 x35 x37 x36 x38) x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x5 x38 ⟶ x6 x38 ⟶ x37 = x22 x38 x36 ⟶ x0 x35 x37 ⟶ (x0 (x10 x35 x37 x36 x38) (x24 x38) ⟶ False) ⟶ False) ⟶ (∀ x35 . x5 x35 ⟶ x6 x35 ⟶ x16 x35 = x15 x35 ⟶ (x28 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x5 x35 ⟶ x6 x35 ⟶ (x19 x35 (x16 x35) = x19 x35 (x15 x35) ⟶ False) ⟶ (x28 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x5 x35 ⟶ x6 x35 ⟶ (x0 (x15 x35) (x24 x35) ⟶ False) ⟶ (x28 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x5 x35 ⟶ x6 x35 ⟶ (x0 (x16 x35) (x24 x35) ⟶ False) ⟶ (x28 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x5 x37 ⟶ x6 x37 ⟶ x28 x37 ⟶ x0 x35 (x24 x37) ⟶ x0 x36 (x24 x37) ⟶ x19 x37 x35 = x19 x37 x36 ⟶ (x35 = x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 (x11 x35 x36) x35 ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x0 (x11 x35 x36) x36 ⟶ False) ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x3 x36 x37 ⟶ x0 x35 x36 ⟶ (x0 x35 x37 ⟶ False) ⟶ False) ⟶ ((x33 = x9 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x5 x35 ⟶ (x30 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x5 x35 ⟶ (x5 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x5 x35 ⟶ (x12 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x5 x35 ⟶ (x5 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x32 x35 ⟶ False) ⟶ x34 x35 ⟶ False) ⟶ (∀ x35 x36 . x5 x36 ⟶ x2 x35 (x1 x36) ⟶ (x5 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x5 x35 ⟶ x6 x35 ⟶ (x28 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x5 x35 ⟶ x6 x35 ⟶ (x6 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ x5 x35 ⟶ x6 x35 ⟶ (x5 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x32 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x5 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x6 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 x35 x36 ⟶ x0 x36 x35 ⟶ False) ⟶ (x3 (x23 x14 (x22 x14 x13)) x13 ⟶ False) ⟶ ((x28 x14 ⟶ False) ⟶ False) ⟶ ((x6 x14 ⟶ False) ⟶ False) ⟶ ((x5 x14 ⟶ False) ⟶ False) ⟶ False (proof)

Proofgold Asset