Search for blocks/addresses/...

Proofgold Asset

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