Search for blocks/addresses/...

Proofgold Asset

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