Search for blocks/addresses/...

Proofgold Asset

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