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

Proofgold Asset