Search for blocks/addresses/...
Proofgold Asset
asset id
787376eb70c6e4644e31ca2868a87559676f3951278af7b760393284becc208b
asset hash
3db28d90475cb81c1395ba5d697964b5094dd33b3233b8610dc40f4ee2d40403
bday / block
35148
tx
735b7..
preasset
doc published by
PrPhD..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Theorem
fe42e..
:
∀ 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 .
x46
x48
⟶
(
x48
=
x47
⟶
False
)
⟶
x46
x47
⟶
False
)
⟶
(
∀ x47 x48 .
x0
x47
x48
⟶
x46
x48
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
(
x47
=
x45
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
x0
x48
x47
⟶
(
x0
(
x1
x48
)
(
x1
x47
)
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
x44
x47
x48
⟶
(
x46
x48
⟶
False
)
⟶
(
x0
x47
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
x0
x48
x47
⟶
(
x44
x48
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 x49 .
x43
x49
⟶
x0
x48
x47
⟶
x0
x47
x49
⟶
(
x0
x48
x49
⟶
False
)
⟶
False
)
⟶
(
(
x2
x3
⟶
False
)
⟶
False
)
⟶
(
x46
x3
⟶
False
)
⟶
(
(
x4
x5
⟶
False
)
⟶
False
)
⟶
(
x46
x5
⟶
False
)
⟶
(
x6
x7
⟶
False
)
⟶
(
(
x42
x7
⟶
False
)
⟶
False
)
⟶
(
(
x8
x7
⟶
False
)
⟶
False
)
⟶
(
(
x4
x41
⟶
False
)
⟶
False
)
⟶
(
(
x42
x9
⟶
False
)
⟶
False
)
⟶
(
(
x40
x9
⟶
False
)
⟶
False
)
⟶
(
(
x8
x9
⟶
False
)
⟶
False
)
⟶
(
x46
x9
⟶
False
)
⟶
(
(
x42
x10
⟶
False
)
⟶
False
)
⟶
(
(
x40
x10
⟶
False
)
⟶
False
)
⟶
(
(
x8
x10
⟶
False
)
⟶
False
)
⟶
(
x46
x39
⟶
False
)
⟶
(
(
x40
x11
⟶
False
)
⟶
False
)
⟶
(
(
x8
x11
⟶
False
)
⟶
False
)
⟶
(
(
x12
x13
⟶
False
)
⟶
False
)
⟶
(
(
x38
x13
⟶
False
)
⟶
False
)
⟶
(
(
x43
x13
⟶
False
)
⟶
False
)
⟶
(
x46
x13
⟶
False
)
⟶
(
(
x14
x15
⟶
False
)
⟶
False
)
⟶
(
(
x42
x15
⟶
False
)
⟶
False
)
⟶
(
(
x8
x15
⟶
False
)
⟶
False
)
⟶
(
(
x46
x37
⟶
False
)
⟶
False
)
⟶
(
(
x8
x16
⟶
False
)
⟶
False
)
⟶
(
x46
x16
⟶
False
)
⟶
(
(
x12
x17
⟶
False
)
⟶
False
)
⟶
(
(
x42
x36
⟶
False
)
⟶
False
)
⟶
(
(
x8
x36
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
(
x46
x47
⟶
False
)
⟶
x8
x47
⟶
x46
(
x35
x47
)
⟶
False
)
⟶
(
∀ x47 x48 x49 x50 .
(
x8
(
x18
(
x19
x48
x47
)
(
x19
x50
x49
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
(
x8
(
x34
(
x19
x48
x47
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
x46
(
x18
x47
x48
)
⟶
False
)
⟶
(
∀ x47 .
x46
(
x34
x47
)
⟶
False
)
⟶
(
∀ x47 .
x20
x47
⟶
x8
x47
⟶
(
x20
(
x35
x47
)
⟶
False
)
⟶
False
)
⟶
(
(
x46
x45
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
(
x42
(
x34
(
x19
x48
x47
)
)
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
x8
x48
⟶
x42
x48
⟶
x8
x47
⟶
x42
x47
⟶
(
x2
(
x18
x48
x47
)
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x8
x47
⟶
x42
x47
⟶
(
x2
(
x34
x47
)
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x8
x47
⟶
x42
x47
⟶
(
x6
x47
⟶
False
)
⟶
x20
(
x35
x47
)
⟶
False
)
⟶
(
∀ x47 .
x8
x47
⟶
x42
x47
⟶
x6
x47
⟶
(
x20
(
x35
x47
)
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
(
x46
(
x35
x47
)
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x8
x47
⟶
x40
x47
⟶
x42
x47
⟶
(
x21
(
x35
x47
)
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
(
x44
(
x33
x47
)
x47
⟶
False
)
⟶
False
)
⟶
(
(
x46
x22
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
(
x12
(
x1
x47
)
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
(
x19
x48
x47
=
x18
(
x18
x48
x47
)
(
x34
x48
)
⟶
False
)
⟶
False
)
⟶
(
(
x45
=
x22
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 x49 .
(
x23
x47
x48
x49
=
x49
⟶
False
)
⟶
(
x23
x47
x48
x49
=
x48
⟶
False
)
⟶
(
x0
(
x23
x47
x48
x49
)
x47
⟶
False
)
⟶
(
x47
=
x18
x49
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 x49 .
x0
(
x23
x47
x48
x49
)
x47
⟶
x23
x47
x48
x49
=
x48
⟶
(
x47
=
x18
x49
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 x49 .
x0
(
x23
x47
x48
x49
)
x47
⟶
x23
x47
x48
x49
=
x49
⟶
(
x47
=
x18
x49
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 x49 x50 .
x49
=
x18
x47
x48
⟶
x50
=
x48
⟶
(
x0
x50
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 x49 x50 .
x49
=
x18
x48
x47
⟶
x50
=
x48
⟶
(
x0
x50
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 x49 x50 .
x50
=
x18
x48
x49
⟶
x0
x47
x50
⟶
(
x47
=
x48
⟶
False
)
⟶
(
x47
=
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
(
x0
(
x19
(
x25
x48
x47
)
(
x24
x48
x47
)
)
x47
⟶
False
)
⟶
(
x0
(
x24
x48
x47
)
x48
⟶
False
)
⟶
(
x48
=
x35
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 x49 .
x0
(
x24
x49
x48
)
x49
⟶
x0
(
x19
x47
(
x24
x49
x48
)
)
x48
⟶
(
x49
=
x35
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 x49 x50 .
x49
=
x35
x50
⟶
x0
(
x19
x48
x47
)
x50
⟶
(
x0
x47
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 x49 .
x48
=
x35
x49
⟶
x0
x47
x48
⟶
(
x0
(
x19
(
x32
x47
x48
x49
)
x47
)
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
(
x18
x48
x47
=
x18
x47
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
(
x31
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
x2
x48
⟶
x44
x47
x48
⟶
(
x42
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
x2
x48
⟶
x44
x47
x48
⟶
(
x8
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
(
x4
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
(
x2
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x4
x47
⟶
(
x12
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x20
x47
⟶
x8
x47
⟶
x42
x47
⟶
(
x6
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x20
x47
⟶
x8
x47
⟶
x42
x47
⟶
(
x42
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x20
x47
⟶
x8
x47
⟶
x42
x47
⟶
(
x8
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
x12
x48
⟶
x44
x47
x48
⟶
(
x12
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x8
x47
⟶
x42
x47
⟶
(
x6
x47
⟶
False
)
⟶
(
x42
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x8
x47
⟶
x42
x47
⟶
(
x6
x47
⟶
False
)
⟶
(
x8
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x8
x47
⟶
x42
x47
⟶
(
x6
x47
⟶
False
)
⟶
x20
x47
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
x8
x47
⟶
(
x40
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
x8
x47
⟶
(
x8
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
(
x26
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
x8
x47
⟶
x42
x47
⟶
(
x6
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
x8
x47
⟶
x42
x47
⟶
(
x42
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
x8
x47
⟶
x42
x47
⟶
(
x8
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
x8
x47
⟶
(
x27
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
x8
x47
⟶
(
x8
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
(
x12
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x43
x47
⟶
x38
x47
⟶
(
x12
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
x8
x47
⟶
x42
x47
⟶
(
x14
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
x8
x47
⟶
x42
x47
⟶
(
x42
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
x8
x47
⟶
x42
x47
⟶
(
x8
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
(
x8
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x12
x47
⟶
(
x38
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x12
x47
⟶
(
x43
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 .
x46
x47
⟶
(
x42
x47
⟶
False
)
⟶
False
)
⟶
(
∀ x47 x48 .
x0
x47
x48
⟶
x0
x48
x47
⟶
False
)
⟶
(
x0
(
x1
x29
)
(
x1
(
x19
x28
x30
)
)
⟶
False
)
⟶
(
(
x0
x29
(
x35
x28
)
⟶
False
)
⟶
False
)
⟶
(
(
x8
x28
⟶
False
)
⟶
False
)
⟶
False
(proof)