Search for blocks/addresses/...

Proofgold Asset

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