Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 745b7.. : ∀ 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 x37 x38 x39 x40 x41 . ∀ x42 x43 : ι → ο . ∀ x44 x45 : ι → ι → ι . ∀ x46 : ι → ι → ο . ∀ x47 : ι → ι → ι . ∀ x48 : ι → ο . ∀ x49 . ∀ x50 : ι → ο . (∀ x51 x52 . x50 x52 ⟶ (x52 = x51 ⟶ False) ⟶ x50 x51 ⟶ False) ⟶ (∀ x51 x52 . x0 x51 x52 ⟶ x50 x52 ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ (x51 = x49 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x0 x51 x52 ⟶ x2 x52 (x1 x53) ⟶ x50 x53 ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x48 x52 ⟶ (x46 x53 x51 ⟶ False) ⟶ (x46 x52 x53 ⟶ False) ⟶ (x0 x53 (x47 x51 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x48 x52 ⟶ x0 x53 (x47 x51 x52) ⟶ x46 x52 x53 ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x48 x52 ⟶ x0 x53 (x47 x51 x52) ⟶ x46 x53 x51 ⟶ False) ⟶ (∀ x51 x52 x53 . x0 x52 x53 ⟶ x2 x53 (x1 x51) ⟶ (x2 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x48 x52 ⟶ x46 x51 x53 ⟶ (x46 x52 x53 ⟶ False) ⟶ (x0 x53 (x45 x51 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x48 x52 ⟶ x0 x53 (x45 x51 x52) ⟶ x46 x52 x53 ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x48 x52 ⟶ x0 x53 (x45 x51 x52) ⟶ (x46 x51 x53 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x3 x52 x51 ⟶ (x2 x52 (x1 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x2 x52 (x1 x51) ⟶ (x3 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x48 x52 ⟶ x46 x53 x51 ⟶ x46 x51 x52 ⟶ (x46 x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x0 x52 x53 ⟶ x0 x51 x53 ⟶ x0 x51 (x44 x53 x52) ⟶ False) ⟶ (∀ x51 x52 . x0 x52 x51 ⟶ (x0 (x44 x51 x52) x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x2 x51 x52 ⟶ (x50 x52 ⟶ False) ⟶ (x0 x51 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x48 x51 ⟶ (x46 x51 x52 ⟶ False) ⟶ x46 x51 (x4 x51 x52) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x48 x51 ⟶ (x46 x51 x52 ⟶ False) ⟶ x46 (x4 x51 x52) x52 ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x48 x51 ⟶ (x46 x51 x52 ⟶ False) ⟶ (x48 (x4 x51 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x0 x52 x51 ⟶ (x2 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x48 x51 ⟶ (x46 x52 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x3 x51 x51 ⟶ False) ⟶ False) ⟶ ((x48 x5 ⟶ False) ⟶ False) ⟶ ((x50 x5 ⟶ False) ⟶ False) ⟶ ((x6 x7 ⟶ False) ⟶ False) ⟶ ((x48 x7 ⟶ False) ⟶ False) ⟶ ((x8 x7 ⟶ False) ⟶ False) ⟶ ((x50 x7 ⟶ False) ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ ((x48 x10 ⟶ False) ⟶ False) ⟶ ((x6 x11 ⟶ False) ⟶ False) ⟶ ((x9 x11 ⟶ False) ⟶ False) ⟶ ((x48 x11 ⟶ False) ⟶ False) ⟶ ((x8 x11 ⟶ False) ⟶ False) ⟶ ((x12 x13 ⟶ False) ⟶ False) ⟶ ((x43 x13 ⟶ False) ⟶ False) ⟶ (x50 x13 ⟶ False) ⟶ ((x42 x41 ⟶ False) ⟶ False) ⟶ ((x48 x41 ⟶ False) ⟶ False) ⟶ ((x6 x40 ⟶ False) ⟶ False) ⟶ ((x42 x40 ⟶ False) ⟶ False) ⟶ ((x48 x40 ⟶ False) ⟶ False) ⟶ ((x8 x40 ⟶ False) ⟶ False) ⟶ (x50 x39 ⟶ False) ⟶ ((x43 x14 ⟶ False) ⟶ False) ⟶ (x50 x14 ⟶ False) ⟶ ((x48 x15 ⟶ False) ⟶ False) ⟶ ((x6 x38 ⟶ False) ⟶ False) ⟶ ((x50 x16 ⟶ False) ⟶ False) ⟶ ((x43 x37 ⟶ False) ⟶ False) ⟶ (x50 x37 ⟶ False) ⟶ (∀ x51 x52 x53 x54 . x48 x54 ⟶ x48 x51 ⟶ x2 x53 x36 ⟶ x52 = x53 ⟶ (x46 x53 x54 ⟶ False) ⟶ (x46 x51 x53 ⟶ False) ⟶ (x0 x52 (x35 x54 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x0 x52 (x35 x53 x51) ⟶ x46 x51 (x17 x51 x53 x52) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x0 x52 (x35 x53 x51) ⟶ x46 (x17 x51 x53 x52) x53 ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x0 x52 (x35 x53 x51) ⟶ (x52 = x17 x51 x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x0 x52 (x35 x53 x51) ⟶ (x2 (x17 x51 x53 x52) x36 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 x54 . x48 x54 ⟶ x48 x51 ⟶ x2 x53 x36 ⟶ x52 = x53 ⟶ x46 x54 x53 ⟶ (x46 x51 x53 ⟶ False) ⟶ (x0 x52 (x18 x54 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x0 x52 (x18 x53 x51) ⟶ x46 x51 (x34 x51 x53 x52) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x0 x52 (x18 x53 x51) ⟶ (x46 x53 (x34 x51 x53 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x0 x52 (x18 x53 x51) ⟶ (x52 = x34 x51 x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x48 x51 ⟶ x0 x52 (x18 x53 x51) ⟶ (x2 (x34 x51 x53 x52) x36 ⟶ False) ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ (x50 (x47 x51 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ (x50 (x45 x51 x51) ⟶ False) ⟶ False) ⟶ (x50 x36 ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x48 x51 ⟶ (x19 (x47 x52 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x48 x51 ⟶ (x19 (x45 x52 x51) ⟶ False) ⟶ False) ⟶ ((x19 x36 ⟶ False) ⟶ False) ⟶ ((x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x2 (x20 x51) x51 ⟶ False) ⟶ False) ⟶ ((x50 x33 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x19 x52 ⟶ x0 (x21 x51 x52) x51 ⟶ (x3 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x19 x52 ⟶ (x0 (x21 x51 x52) x52 ⟶ False) ⟶ (x3 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x19 x52 ⟶ (x48 (x21 x51 x52) ⟶ False) ⟶ (x3 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x19 x53 ⟶ x3 x53 x51 ⟶ x48 x52 ⟶ x0 x52 x53 ⟶ (x0 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x48 x51 ⟶ (x47 x52 x51 = x35 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x48 x51 ⟶ (x45 x52 x51 = x18 x52 x51 ⟶ False) ⟶ False) ⟶ ((x49 = x33 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x48 x51 ⟶ (x46 x52 x51 ⟶ False) ⟶ (x46 x51 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ (x42 x51 ⟶ False) ⟶ (x9 x51 ⟶ False) ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ (x42 x51 ⟶ False) ⟶ (x9 x51 ⟶ False) ⟶ (x50 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ x9 x51 ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ x42 x51 ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x2 x51 (x1 x36) ⟶ (x19 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ x48 x51 ⟶ (x42 x51 ⟶ False) ⟶ (x9 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ x48 x51 ⟶ (x42 x51 ⟶ False) ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ x9 x51 ⟶ x42 x51 ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ x9 x51 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ x9 x51 ⟶ x50 x51 ⟶ False) ⟶ (∀ x51 . x31 x51 ⟶ (x32 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ x48 x51 ⟶ (x9 x51 ⟶ False) ⟶ (x42 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ x48 x51 ⟶ (x9 x51 ⟶ False) ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x6 x51 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x31 x51 ⟶ (x19 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ x42 x51 ⟶ x9 x51 ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ x42 x51 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ x42 x51 ⟶ x50 x51 ⟶ False) ⟶ (∀ x51 . x6 x51 ⟶ (x8 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x22 x51 ⟶ (x31 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x30 x51 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x30 x51 ⟶ (x6 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x29 x51 ⟶ (x22 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ (x12 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x43 x52 ⟶ x2 x51 (x1 x52) ⟶ (x43 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x29 x52 ⟶ x2 x51 (x1 x52) ⟶ (x29 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x22 x52 ⟶ x2 x51 (x1 x52) ⟶ (x22 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x31 x52 ⟶ x2 x51 (x1 x52) ⟶ (x31 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x19 x52 ⟶ x2 x51 (x1 x52) ⟶ (x19 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x2 x51 x36 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x43 x51 ⟶ (x29 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x32 x52 ⟶ x2 x51 (x1 x52) ⟶ (x32 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ (x43 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x43 x52 ⟶ x2 x51 x52 ⟶ (x30 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x29 x52 ⟶ x2 x51 x52 ⟶ (x28 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x22 x52 ⟶ x2 x51 x52 ⟶ (x23 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x31 x52 ⟶ x2 x51 x52 ⟶ (x6 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x19 x52 ⟶ x2 x51 x52 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x32 x52 ⟶ x2 x51 x52 ⟶ (x8 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x0 x51 x52 ⟶ x0 x52 x51 ⟶ False) ⟶ ((x3 (x45 x27 x26) (x47 x25 x24) ⟶ False) ⟶ False) ⟶ (x46 x26 x27 ⟶ False) ⟶ (x46 x26 x24 ⟶ False) ⟶ ((x48 x25 ⟶ False) ⟶ False) ⟶ ((x48 x27 ⟶ False) ⟶ False) ⟶ ((x48 x26 ⟶ False) ⟶ False) ⟶ ((x48 x24 ⟶ False) ⟶ False) ⟶ False (proof)

Proofgold Asset