Search for blocks/addresses/...

Proofgold Asset

asset id
74318905032c7fa78610694aa24790736047d003950be2c32c25aa06d5b7e470
asset hash
648f05303c8e3813fe183710b47d38c7885a317a588b053f90849dcdd7ad8a35
bday / block
35160
tx
77d26..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 1de24.. : ∀ 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 . x45 x47 ⟶ (x47 = x46 ⟶ False) ⟶ x45 x46 ⟶ False) ⟶ (∀ x46 x47 . x0 x46 x47 ⟶ x45 x47 ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x46 = x44 ⟶ False) ⟶ False) ⟶ (∀ x46 . x1 x46 ⟶ (x2 x46 x3 = x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x0 x46 x47 ⟶ x42 x47 (x43 x48) ⟶ x45 x48 ⟶ False) ⟶ (∀ x46 . x1 x46 ⟶ (x2 x4 x46 = x4 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x0 x47 x48 ⟶ x42 x48 (x43 x46) ⟶ (x42 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x5 x47 x46 ⟶ (x42 x47 (x43 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x42 x47 (x43 x46) ⟶ (x5 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x1 x46 ⟶ (x6 x3 x46 = x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x42 x46 x47 ⟶ (x45 x47 ⟶ False) ⟶ (x0 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 . x1 x46 ⟶ (x6 x46 x4 = x4 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x0 x47 x46 ⟶ (x42 x47 x46 ⟶ False) ⟶ False) ⟶ ((x42 x44 x7 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x1 x48 ⟶ x1 x46 ⟶ x1 x47 ⟶ (x6 (x6 x48 x46) x47 = x6 x48 (x6 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x1 x48 ⟶ x1 x46 ⟶ x1 x47 ⟶ (x6 x48 (x2 x46 x47) = x2 (x6 x48 x46) x47 ⟶ False) ⟶ False) ⟶ (∀ x46 . x1 x46 ⟶ (x2 x3 x46 = x41 x46 ⟶ False) ⟶ False) ⟶ ((x42 x3 x8 ⟶ False) ⟶ False) ⟶ ((x42 x3 x40 ⟶ False) ⟶ False) ⟶ ((x9 x3 x8 x40 ⟶ False) ⟶ False) ⟶ ((x39 x3 ⟶ False) ⟶ False) ⟶ (x45 x3 ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x6 x47 (x41 x46) = x2 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x2 (x41 x47) (x41 x46) = x2 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x6 (x41 x47) (x41 x46) = x41 (x6 x47 x46) ⟶ False) ⟶ False) ⟶ ((x6 x3 x3 = x3 ⟶ False) ⟶ False) ⟶ ((x2 x3 x3 = x3 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x5 x46 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x45 x48 ⟶ False) ⟶ (x45 x46 ⟶ False) ⟶ x42 x46 (x43 x48) ⟶ x42 x47 x46 ⟶ (x9 x47 x48 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x45 x48 ⟶ False) ⟶ (x45 x46 ⟶ False) ⟶ x42 x46 (x43 x48) ⟶ x9 x47 x48 x46 ⟶ (x42 x47 x46 ⟶ False) ⟶ False) ⟶ ((x4 = x44 ⟶ False) ⟶ False) ⟶ ((x40 = x7 ⟶ False) ⟶ False) ⟶ ((x38 x37 ⟶ False) ⟶ False) ⟶ (x45 x37 ⟶ False) ⟶ ((x36 x35 ⟶ False) ⟶ False) ⟶ ((x45 x35 ⟶ False) ⟶ False) ⟶ ((x34 x33 ⟶ False) ⟶ False) ⟶ ((x36 x33 ⟶ False) ⟶ False) ⟶ ((x1 x33 ⟶ False) ⟶ False) ⟶ ((x45 x33 ⟶ False) ⟶ False) ⟶ ((x38 x32 ⟶ False) ⟶ False) ⟶ ((x10 x11 ⟶ False) ⟶ False) ⟶ ((x36 x11 ⟶ False) ⟶ False) ⟶ ((x34 x12 ⟶ False) ⟶ False) ⟶ ((x10 x12 ⟶ False) ⟶ False) ⟶ ((x36 x12 ⟶ False) ⟶ False) ⟶ ((x1 x12 ⟶ False) ⟶ False) ⟶ ((x39 x13 ⟶ False) ⟶ False) ⟶ ((x36 x13 ⟶ False) ⟶ False) ⟶ ((x34 x14 ⟶ False) ⟶ False) ⟶ ((x39 x14 ⟶ False) ⟶ False) ⟶ ((x36 x14 ⟶ False) ⟶ False) ⟶ ((x1 x14 ⟶ False) ⟶ False) ⟶ ((x1 x15 ⟶ False) ⟶ False) ⟶ (x45 x15 ⟶ False) ⟶ (x45 x16 ⟶ False) ⟶ ((x31 x30 ⟶ False) ⟶ False) ⟶ ((x17 x30 ⟶ False) ⟶ False) ⟶ ((x29 x30 ⟶ False) ⟶ False) ⟶ (x45 x30 ⟶ False) ⟶ ((x36 x28 ⟶ False) ⟶ False) ⟶ ((x34 x18 ⟶ False) ⟶ False) ⟶ ((x1 x27 ⟶ False) ⟶ False) ⟶ ((x45 x19 ⟶ False) ⟶ False) ⟶ ((x31 x26 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x41 (x2 x47 x46) = x2 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 . x1 x46 ⟶ (x41 (x41 x46) = x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x45 x47 ⟶ False) ⟶ x1 x47 ⟶ (x45 x46 ⟶ False) ⟶ x1 x46 ⟶ x45 (x2 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . x34 x47 ⟶ x34 x46 ⟶ (x34 (x2 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x45 x47 ⟶ False) ⟶ x1 x47 ⟶ (x45 x46 ⟶ False) ⟶ x1 x46 ⟶ x45 (x6 x47 x46) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x1 x46 ⟶ (x1 (x41 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x1 x46 ⟶ x45 (x41 x46) ⟶ False) ⟶ (∀ x46 x47 . x34 x47 ⟶ x34 x46 ⟶ (x34 (x6 x47 x46) ⟶ False) ⟶ False) ⟶ ((x31 x7 ⟶ False) ⟶ False) ⟶ (x45 x7 ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x1 (x2 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x34 x46 ⟶ (x34 (x41 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x34 x46 ⟶ (x1 (x41 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x1 (x6 x47 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x39 x47 ⟶ False) ⟶ x34 x47 ⟶ (x39 x46 ⟶ False) ⟶ x34 x46 ⟶ x10 (x2 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x10 x47 ⟶ False) ⟶ x34 x47 ⟶ (x10 x46 ⟶ False) ⟶ x34 x46 ⟶ x10 (x2 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x10 x47 ⟶ False) ⟶ x34 x47 ⟶ (x39 x46 ⟶ False) ⟶ x34 x46 ⟶ x39 (x2 x46 x47) ⟶ False) ⟶ (∀ x46 x47 . (x10 x47 ⟶ False) ⟶ x34 x47 ⟶ (x39 x46 ⟶ False) ⟶ x34 x46 ⟶ x39 (x2 x47 x46) ⟶ False) ⟶ (∀ x46 . (x10 x46 ⟶ False) ⟶ x34 x46 ⟶ x10 (x41 x46) ⟶ False) ⟶ (∀ x46 . (x10 x46 ⟶ False) ⟶ x34 x46 ⟶ (x1 (x41 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x10 x46 ⟶ x34 x46 ⟶ (x10 (x41 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x10 x46 ⟶ x34 x46 ⟶ (x1 (x41 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . (x39 x46 ⟶ False) ⟶ x34 x46 ⟶ x39 (x41 x46) ⟶ False) ⟶ (∀ x46 . (x39 x46 ⟶ False) ⟶ x34 x46 ⟶ (x1 (x41 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x39 x46 ⟶ x34 x46 ⟶ (x39 (x41 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x39 x46 ⟶ x34 x46 ⟶ (x1 (x41 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x10 x47 ⟶ False) ⟶ x34 x47 ⟶ (x10 x46 ⟶ False) ⟶ x34 x46 ⟶ x10 (x6 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x39 x47 ⟶ False) ⟶ x34 x47 ⟶ (x39 x46 ⟶ False) ⟶ x34 x46 ⟶ x10 (x6 x47 x46) ⟶ False) ⟶ (∀ x46 x47 . (x39 x47 ⟶ False) ⟶ x34 x47 ⟶ (x10 x46 ⟶ False) ⟶ x34 x46 ⟶ x39 (x6 x46 x47) ⟶ False) ⟶ (∀ x46 x47 . (x39 x47 ⟶ False) ⟶ x34 x47 ⟶ (x10 x46 ⟶ False) ⟶ x34 x46 ⟶ x39 (x6 x47 x46) ⟶ False) ⟶ ((x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x45 x47 ⟶ False) ⟶ (x45 x46 ⟶ False) ⟶ x42 x46 (x43 x47) ⟶ (x9 (x25 x46 x47) x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x42 (x20 x46) x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x45 x48 ⟶ False) ⟶ (x45 x46 ⟶ False) ⟶ x42 x46 (x43 x48) ⟶ x9 x47 x48 x46 ⟶ (x42 x47 x48 ⟶ False) ⟶ False) ⟶ ((x9 x4 x8 x40 ⟶ False) ⟶ False) ⟶ (∀ x46 . x1 x46 ⟶ (x1 (x41 x46) ⟶ False) ⟶ False) ⟶ ((x42 x40 (x43 x8) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ x47 = x4 ⟶ x46 = x4 ⟶ (x46 = x41 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ x47 = x4 ⟶ x46 = x41 x47 ⟶ (x46 = x4 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x47 = x4 ⟶ False) ⟶ x6 x47 x46 = x3 ⟶ (x46 = x41 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x47 = x4 ⟶ False) ⟶ x46 = x41 x47 ⟶ (x6 x47 x46 = x3 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x1 x47 ⟶ x1 x46 ⟶ (x6 x47 x46 = x6 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x21 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ (x39 x46 ⟶ False) ⟶ (x10 x46 ⟶ False) ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ (x39 x46 ⟶ False) ⟶ (x10 x46 ⟶ False) ⟶ (x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x42 x46 x7 ⟶ (x38 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x36 x46 ⟶ x10 x46 ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x36 x46 ⟶ x39 x46 ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ x36 x46 ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x38 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x36 x46 ⟶ (x39 x46 ⟶ False) ⟶ (x10 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x36 x46 ⟶ (x39 x46 ⟶ False) ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ (x31 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ x10 x46 ⟶ x39 x46 ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ x10 x46 ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ x10 x46 ⟶ x45 x46 ⟶ False) ⟶ (∀ x46 x47 . x31 x47 ⟶ x42 x46 x47 ⟶ (x31 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x36 x46 ⟶ (x10 x46 ⟶ False) ⟶ (x39 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x36 x46 ⟶ (x10 x46 ⟶ False) ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x34 x46 ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x22 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ x39 x46 ⟶ x10 x46 ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ x39 x46 ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x36 x46 ⟶ x39 x46 ⟶ x45 x46 ⟶ False) ⟶ (∀ x46 . x34 x46 ⟶ (x1 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x31 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ (x34 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x38 x46 ⟶ (x1 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x29 x46 ⟶ x17 x46 ⟶ (x31 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x42 x46 x8 ⟶ (x34 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x42 x46 x8 ⟶ (x1 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x31 x46 ⟶ (x17 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x31 x46 ⟶ (x29 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x21 x47 ⟶ x42 x46 (x43 x47) ⟶ (x21 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x0 x46 x47 ⟶ x0 x47 x46 ⟶ False) ⟶ (x6 (x2 x24 x23) (x2 x23 x24) = x3 ⟶ False) ⟶ (x23 = x4 ⟶ False) ⟶ (x24 = x4 ⟶ False) ⟶ ((x1 x23 ⟶ False) ⟶ False) ⟶ ((x1 x24 ⟶ False) ⟶ False) ⟶ False (proof)