Search for blocks/addresses/...

Proofgold Asset

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