Search for blocks/addresses/...

Proofgold Asset

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