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

Proofgold Asset