Search for blocks/addresses/...

Proofgold Asset

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