Search for blocks/addresses/...

Proofgold Asset

asset id
cbe5627da5033fdf03b672dfea4139df2ef8a68626db8f1fdc76ec4092d86190
asset hash
801dfdf4585e14daff942a04fdb10d0c10052be983ae9451e3915eb15e9e8bce
bday / block
35123
tx
48295..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 2dbc3.. : ∀ 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 . x33 x35 ⟶ (x35 = x34 ⟶ False) ⟶ x33 x34 ⟶ False) ⟶ (∀ x34 x35 . x0 x34 x35 ⟶ x33 x35 ⟶ False) ⟶ (∀ x34 . x33 x34 ⟶ (x34 = x32 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 . x0 x34 x35 ⟶ x2 x35 (x1 x36) ⟶ x33 x36 ⟶ False) ⟶ (∀ x34 x35 . x30 x34 (x31 x34 x35) ⟶ (x35 = x32 ⟶ False) ⟶ (x30 x34 (x29 x35) ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . (x0 (x31 x34 x35) x35 ⟶ False) ⟶ (x35 = x32 ⟶ False) ⟶ (x30 x34 (x29 x35) ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 . x0 x35 x36 ⟶ x2 x36 (x1 x34) ⟶ (x2 x35 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x30 x35 x34 ⟶ (x2 x35 (x1 x34) ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x2 x35 (x1 x34) ⟶ (x30 x35 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x2 x34 x35 ⟶ (x33 x35 ⟶ False) ⟶ (x0 x34 x35 ⟶ False) ⟶ False) ⟶ (∀ x34 . (x30 (x29 x34) (x28 x34) ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 . x30 x35 x36 ⟶ x30 x36 x34 ⟶ (x30 x35 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x0 x35 x34 ⟶ (x2 x35 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 . (x30 x34 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x2 x34 (x1 (x1 x35)) ⟶ (x27 x35 x34 = x29 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x2 x34 (x1 (x1 x35)) ⟶ (x3 x35 x34 = x28 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 . x26 x34 ⟶ x23 x34 ⟶ (x25 (x24 x34) x34 ⟶ False) ⟶ False) ⟶ (∀ x34 . x26 x34 ⟶ x23 x34 ⟶ (x2 (x24 x34) (x1 (x4 x34)) ⟶ False) ⟶ False) ⟶ (∀ x34 . (x33 x34 ⟶ False) ⟶ (x21 (x22 x34) x34 ⟶ False) ⟶ False) ⟶ (∀ x34 . (x33 x34 ⟶ False) ⟶ (x2 (x22 x34) (x1 x34) ⟶ False) ⟶ False) ⟶ (∀ x34 . x21 (x20 x34) x34 ⟶ False) ⟶ (∀ x34 . (x2 (x20 x34) (x1 x34) ⟶ False) ⟶ False) ⟶ (∀ x34 . (x33 (x19 x34) ⟶ False) ⟶ False) ⟶ (∀ x34 . (x2 (x19 x34) (x1 x34) ⟶ False) ⟶ False) ⟶ (∀ x34 . (x33 x34 ⟶ False) ⟶ x33 (x18 x34) ⟶ False) ⟶ (∀ x34 . (x33 x34 ⟶ False) ⟶ (x2 (x18 x34) (x1 x34) ⟶ False) ⟶ False) ⟶ (∀ x34 . x23 x34 ⟶ (x33 (x17 x34) ⟶ False) ⟶ False) ⟶ (∀ x34 . x23 x34 ⟶ (x2 (x17 x34) (x1 (x4 x34)) ⟶ False) ⟶ False) ⟶ (∀ x34 . x33 (x1 x34) ⟶ False) ⟶ (∀ x34 . (x2 (x5 x34) x34 ⟶ False) ⟶ False) ⟶ ((x16 x15 ⟶ False) ⟶ False) ⟶ ((x23 x6 ⟶ False) ⟶ False) ⟶ ((x33 x14 ⟶ False) ⟶ False) ⟶ (∀ x34 . x23 x34 ⟶ (x16 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x2 x35 (x1 (x1 x34)) ⟶ (x2 (x27 x34 x35) (x1 x34) ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x2 x35 (x1 (x1 x34)) ⟶ (x2 (x3 x34 x35) (x1 x34) ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x23 x35 ⟶ x2 x34 (x1 (x4 x35)) ⟶ (x2 (x13 x35 x34) (x1 (x4 x35)) ⟶ False) ⟶ False) ⟶ ((x32 = x14 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 x37 . x23 x37 ⟶ x2 x34 (x1 (x4 x37)) ⟶ x2 x36 (x1 (x4 x37)) ⟶ x2 x35 (x1 (x1 (x4 x37))) ⟶ (x30 x34 (x12 x35 x36 x34 x37) ⟶ False) ⟶ (x0 (x12 x35 x36 x34 x37) x35 ⟶ False) ⟶ x3 (x4 x37) x35 = x36 ⟶ (x36 = x13 x37 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 x37 . x23 x37 ⟶ x2 x34 (x1 (x4 x37)) ⟶ x2 x36 (x1 (x4 x37)) ⟶ x2 x35 (x1 (x1 (x4 x37))) ⟶ (x7 (x12 x35 x36 x34 x37) x37 ⟶ False) ⟶ (x0 (x12 x35 x36 x34 x37) x35 ⟶ False) ⟶ x3 (x4 x37) x35 = x36 ⟶ (x36 = x13 x37 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 x37 . x23 x37 ⟶ x2 x34 (x1 (x4 x37)) ⟶ x2 x36 (x1 (x4 x37)) ⟶ x2 x35 (x1 (x1 (x4 x37))) ⟶ x0 (x12 x35 x36 x34 x37) x35 ⟶ x7 (x12 x35 x36 x34 x37) x37 ⟶ x30 x34 (x12 x35 x36 x34 x37) ⟶ x3 (x4 x37) x35 = x36 ⟶ (x36 = x13 x37 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 x37 . x23 x37 ⟶ x2 x34 (x1 (x4 x37)) ⟶ x2 x36 (x1 (x4 x37)) ⟶ x2 x35 (x1 (x1 (x4 x37))) ⟶ (x2 (x12 x35 x36 x34 x37) (x1 (x4 x37)) ⟶ False) ⟶ x3 (x4 x37) x35 = x36 ⟶ (x36 = x13 x37 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 . x23 x36 ⟶ x2 x34 (x1 (x4 x36)) ⟶ x2 x35 (x1 (x4 x36)) ⟶ x35 = x13 x36 x34 ⟶ (x3 (x4 x36) (x11 x35 x34 x36) = x35 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 x37 . x23 x37 ⟶ x2 x34 (x1 (x4 x37)) ⟶ x2 x36 (x1 (x4 x37)) ⟶ x36 = x13 x37 x34 ⟶ x2 x35 (x1 (x4 x37)) ⟶ x7 x35 x37 ⟶ x30 x34 x35 ⟶ (x0 x35 (x11 x36 x34 x37) ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 x37 . x23 x37 ⟶ x2 x34 (x1 (x4 x37)) ⟶ x2 x36 (x1 (x4 x37)) ⟶ x36 = x13 x37 x34 ⟶ x2 x35 (x1 (x4 x37)) ⟶ x0 x35 (x11 x36 x34 x37) ⟶ (x30 x34 x35 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 x37 . x23 x37 ⟶ x2 x34 (x1 (x4 x37)) ⟶ x2 x36 (x1 (x4 x37)) ⟶ x36 = x13 x37 x34 ⟶ x2 x35 (x1 (x4 x37)) ⟶ x0 x35 (x11 x36 x34 x37) ⟶ (x7 x35 x37 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 x36 . x23 x36 ⟶ x2 x34 (x1 (x4 x36)) ⟶ x2 x35 (x1 (x4 x36)) ⟶ x35 = x13 x36 x34 ⟶ (x2 (x11 x35 x34 x36) (x1 (x1 (x4 x36))) ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x33 x35 ⟶ x2 x34 (x1 x35) ⟶ x21 x34 x35 ⟶ False) ⟶ (∀ x34 x35 . x23 x35 ⟶ x2 x34 (x1 (x4 x35)) ⟶ x33 x34 ⟶ (x7 x34 x35 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . (x33 x35 ⟶ False) ⟶ x2 x34 (x1 x35) ⟶ x33 x34 ⟶ (x21 x34 x35 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . (x33 x35 ⟶ False) ⟶ x2 x34 (x1 x35) ⟶ (x21 x34 x35 ⟶ False) ⟶ x33 x34 ⟶ False) ⟶ (∀ x34 x35 . x26 x35 ⟶ x23 x35 ⟶ x2 x34 (x1 (x4 x35)) ⟶ x33 x34 ⟶ (x25 x34 x35 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x33 x35 ⟶ x2 x34 (x1 x35) ⟶ (x33 x34 ⟶ False) ⟶ False) ⟶ (∀ x34 x35 . x0 x34 x35 ⟶ x0 x35 x34 ⟶ False) ⟶ (x30 x10 (x13 x9 x10) ⟶ False) ⟶ ((x30 x10 x8 ⟶ False) ⟶ False) ⟶ ((x7 x8 x9 ⟶ False) ⟶ False) ⟶ ((x2 x8 (x1 (x4 x9)) ⟶ False) ⟶ False) ⟶ ((x2 x10 (x1 (x4 x9)) ⟶ False) ⟶ False) ⟶ ((x23 x9 ⟶ False) ⟶ False) ⟶ ((x26 x9 ⟶ False) ⟶ False) ⟶ False (proof)