Search for blocks/addresses/...
Proofgold Asset
asset id
3aa605b2b338fe8f5ad920314bdcf5fffceb7e7be7358edd0b2f7ba1ddb364a0
asset hash
6f2c04b9b9a45d3d4960c1588e22774df4590b5c017f3446222ec8ac64c33b23
bday / block
20898
tx
362a2..
preasset
doc published by
Pr4zB..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Theorem
3c838..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι →
ι →
ι → ο
.
(
∀ x3 x4 x5 x6 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
∀ x7 : ο .
(
x1
x3
x4
x5
x6
⟶
x7
)
⟶
(
x2
x3
x4
x5
x6
⟶
x7
)
⟶
(
x1
x5
x6
x3
x4
⟶
x7
)
⟶
x7
)
⟶
(
∀ x3 x4 x5 x6 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x2
x3
x4
x5
x6
⟶
x2
x5
x6
x3
x4
)
⟶
∀ x3 .
x0
x3
⟶
∀ x4 .
x0
x4
⟶
∀ x5 .
x0
x5
⟶
∀ x6 .
x0
x6
⟶
∀ x7 .
x0
x7
⟶
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
∀ x11 .
x0
x11
⟶
∀ x12 .
x0
x12
⟶
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
not
(
x2
x3
x4
x5
x6
)
⟶
not
(
x2
x3
x4
x7
x8
)
⟶
not
(
x2
x3
x4
x9
x10
)
⟶
not
(
x2
x3
x4
x11
x12
)
⟶
not
(
x2
x3
x4
x13
x14
)
⟶
not
(
x2
x5
x6
x7
x8
)
⟶
not
(
x2
x5
x6
x9
x10
)
⟶
not
(
x2
x5
x6
x11
x12
)
⟶
not
(
x2
x5
x6
x13
x14
)
⟶
not
(
x2
x7
x8
x9
x10
)
⟶
not
(
x2
x7
x8
x11
x12
)
⟶
not
(
x2
x7
x8
x13
x14
)
⟶
not
(
x2
x9
x10
x11
x12
)
⟶
not
(
x2
x9
x10
x13
x14
)
⟶
not
(
x2
x11
x12
x13
x14
)
⟶
∀ x15 : ο .
(
∀ x16 .
x0
x16
⟶
∀ x17 .
x0
x17
⟶
∀ x18 .
x0
x18
⟶
∀ x19 .
x0
x19
⟶
∀ x20 .
x0
x20
⟶
∀ x21 .
x0
x21
⟶
∀ x22 .
x0
x22
⟶
∀ x23 .
x0
x23
⟶
∀ x24 .
x0
x24
⟶
∀ x25 .
x0
x25
⟶
∀ x26 .
x0
x26
⟶
∀ x27 .
x0
x27
⟶
x1
x16
x17
x18
x19
⟶
x1
x18
x19
x20
x21
⟶
x1
x20
x21
x22
x23
⟶
x1
x22
x23
x24
x25
⟶
x1
x24
x25
x26
x27
⟶
not
(
x2
x16
x17
x18
x19
)
⟶
not
(
x2
x16
x17
x20
x21
)
⟶
not
(
x2
x16
x17
x22
x23
)
⟶
not
(
x2
x16
x17
x24
x25
)
⟶
not
(
x2
x16
x17
x26
x27
)
⟶
not
(
x2
x18
x19
x20
x21
)
⟶
not
(
x2
x18
x19
x22
x23
)
⟶
not
(
x2
x18
x19
x24
x25
)
⟶
not
(
x2
x18
x19
x26
x27
)
⟶
not
(
x2
x20
x21
x22
x23
)
⟶
not
(
x2
x20
x21
x24
x25
)
⟶
not
(
x2
x20
x21
x26
x27
)
⟶
not
(
x2
x22
x23
x24
x25
)
⟶
not
(
x2
x22
x23
x26
x27
)
⟶
not
(
x2
x24
x25
x26
x27
)
⟶
(
∀ x28 : ο .
(
x16
=
x3
⟶
x17
=
x4
⟶
x18
=
x5
⟶
x19
=
x6
⟶
x28
)
⟶
(
x16
=
x3
⟶
x17
=
x4
⟶
x20
=
x5
⟶
x21
=
x6
⟶
x28
)
⟶
(
x16
=
x3
⟶
x17
=
x4
⟶
x22
=
x5
⟶
x23
=
x6
⟶
x28
)
⟶
(
x16
=
x3
⟶
x17
=
x4
⟶
x24
=
x5
⟶
x25
=
x6
⟶
x28
)
⟶
(
x16
=
x3
⟶
x17
=
x4
⟶
x26
=
x5
⟶
x27
=
x6
⟶
x28
)
⟶
(
x18
=
x3
⟶
x19
=
x4
⟶
x16
=
x5
⟶
x17
=
x6
⟶
x28
)
⟶
(
x18
=
x3
⟶
x19
=
x4
⟶
x20
=
x5
⟶
x21
=
x6
⟶
x28
)
⟶
(
x18
=
x3
⟶
x19
=
x4
⟶
x22
=
x5
⟶
x23
=
x6
⟶
x28
)
⟶
(
x18
=
x3
⟶
x19
=
x4
⟶
x24
=
x5
⟶
x25
=
x6
⟶
x28
)
⟶
(
x18
=
x3
⟶
x19
=
x4
⟶
x26
=
x5
⟶
x27
=
x6
⟶
x28
)
⟶
(
x20
=
x3
⟶
x21
=
x4
⟶
x16
=
x5
⟶
x17
=
x6
⟶
x28
)
⟶
(
x20
=
x3
⟶
x21
=
x4
⟶
x18
=
x5
⟶
x19
=
x6
⟶
x28
)
⟶
(
x20
=
x3
⟶
x21
=
x4
⟶
x22
=
x5
⟶
x23
=
x6
⟶
x28
)
⟶
(
x20
=
x3
⟶
x21
=
x4
⟶
x24
=
x5
⟶
x25
=
x6
⟶
x28
)
⟶
(
x20
=
x3
⟶
x21
=
x4
⟶
x26
=
x5
⟶
x27
=
x6
⟶
x28
)
⟶
(
x22
=
x3
⟶
x23
=
x4
⟶
x16
=
x5
⟶
x17
=
x6
⟶
x28
)
⟶
(
x22
=
x3
⟶
x23
=
x4
⟶
x18
=
x5
⟶
x19
=
x6
⟶
x28
)
⟶
(
x22
=
x3
⟶
x23
=
x4
⟶
x20
=
x5
⟶
x21
=
x6
⟶
x28
)
⟶
(
x22
=
x3
⟶
x23
=
x4
⟶
x24
=
x5
⟶
x25
=
x6
⟶
x28
)
⟶
(
x22
=
x3
⟶
x23
=
x4
⟶
x26
=
x5
⟶
x27
=
x6
⟶
x28
)
⟶
(
x24
=
x3
⟶
x25
=
x4
⟶
x16
=
x5
⟶
x17
=
x6
⟶
x28
)
⟶
(
x24
=
x3
⟶
x25
=
x4
⟶
x18
=
x5
⟶
x19
=
x6
⟶
x28
)
⟶
(
x24
=
x3
⟶
x25
=
x4
⟶
x20
=
x5
⟶
x21
=
x6
⟶
x28
)
⟶
(
x24
=
x3
⟶
x25
=
x4
⟶
x22
=
x5
⟶
x23
=
x6
⟶
x28
)
⟶
(
x24
=
x3
⟶
x25
=
x4
⟶
x26
=
x5
⟶
x27
=
x6
⟶
x28
)
⟶
(
x26
=
x3
⟶
x27
=
x4
⟶
x16
=
x5
⟶
x17
=
x6
⟶
x28
)
⟶
(
x26
=
x3
⟶
x27
=
x4
⟶
x18
=
x5
⟶
x19
=
x6
⟶
x28
)
⟶
(
x26
=
x3
⟶
x27
=
x4
⟶
x20
=
x5
⟶
x21
=
x6
⟶
x28
)
⟶
(
x26
=
x3
⟶
x27
=
x4
⟶
x22
=
x5
⟶
x23
=
x6
⟶
x28
)
⟶
(
x26
=
x3
⟶
x27
=
x4
⟶
x24
=
x5
⟶
x25
=
x6
⟶
x28
)
⟶
x28
)
⟶
x15
)
⟶
x15
(proof)
Theorem
16baa..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι →
ι →
ι → ο
.
(
∀ x3 x4 x5 x6 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
∀ x7 : ο .
(
x1
x3
x4
x5
x6
⟶
x7
)
⟶
(
x2
x3
x4
x5
x6
⟶
x7
)
⟶
(
x1
x5
x6
x3
x4
⟶
x7
)
⟶
x7
)
⟶
(
∀ x3 x4 x5 x6 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x2
x3
x4
x5
x6
⟶
x2
x5
x6
x3
x4
)
⟶
∀ x3 .
x0
x3
⟶
∀ x4 .
x0
x4
⟶
∀ x5 .
x0
x5
⟶
∀ x6 .
x0
x6
⟶
∀ x7 .
x0
x7
⟶
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
∀ x10 .
x0
x10
⟶
∀ x11 .
x0
x11
⟶
∀ x12 .
x0
x12
⟶
∀ x13 .
x0
x13
⟶
∀ x14 .
x0
x14
⟶
not
(
x2
x3
x4
x5
x6
)
⟶
not
(
x2
x3
x4
x7
x8
)
⟶
not
(
x2
x3
x4
x9
x10
)
⟶
not
(
x2
x3
x4
x11
x12
)
⟶
not
(
x2
x3
x4
x13
x14
)
⟶
not
(
x2
x5
x6
x7
x8
)
⟶
not
(
x2
x5
x6
x9
x10
)
⟶
not
(
x2
x5
x6
x11
x12
)
⟶
not
(
x2
x5
x6
x13
x14
)
⟶
not
(
x2
x7
x8
x9
x10
)
⟶
not
(
x2
x7
x8
x11
x12
)
⟶
not
(
x2
x7
x8
x13
x14
)
⟶
not
(
x2
x9
x10
x11
x12
)
⟶
not
(
x2
x9
x10
x13
x14
)
⟶
not
(
x2
x11
x12
x13
x14
)
⟶
∀ x15 : ο .
(
∀ x16 .
x0
x16
⟶
∀ x17 .
x0
x17
⟶
∀ x18 .
x0
x18
⟶
∀ x19 .
x0
x19
⟶
∀ x20 .
x0
x20
⟶
∀ x21 .
x0
x21
⟶
∀ x22 .
x0
x22
⟶
∀ x23 .
x0
x23
⟶
∀ x24 .
x0
x24
⟶
∀ x25 .
x0
x25
⟶
∀ x26 .
x0
x26
⟶
∀ x27 .
x0
x27
⟶
x1
x16
x17
x18
x19
⟶
x1
x18
x19
x20
x21
⟶
x1
x20
x21
x22
x23
⟶
x1
x22
x23
x24
x25
⟶
x1
x24
x25
x26
x27
⟶
not
(
x2
x16
x17
x18
x19
)
⟶
not
(
x2
x16
x17
x20
x21
)
⟶
not
(
x2
x16
x17
x22
x23
)
⟶
not
(
x2
x16
x17
x24
x25
)
⟶
not
(
x2
x16
x17
x26
x27
)
⟶
not
(
x2
x18
x19
x20
x21
)
⟶
not
(
x2
x18
x19
x22
x23
)
⟶
not
(
x2
x18
x19
x24
x25
)
⟶
not
(
x2
x18
x19
x26
x27
)
⟶
not
(
x2
x20
x21
x22
x23
)
⟶
not
(
x2
x20
x21
x24
x25
)
⟶
not
(
x2
x20
x21
x26
x27
)
⟶
not
(
x2
x22
x23
x24
x25
)
⟶
not
(
x2
x22
x23
x26
x27
)
⟶
not
(
x2
x24
x25
x26
x27
)
⟶
(
∀ x28 : ο .
(
x16
=
x3
⟶
x17
=
x4
⟶
x28
)
⟶
(
x18
=
x3
⟶
x19
=
x4
⟶
x28
)
⟶
(
x20
=
x3
⟶
x21
=
x4
⟶
x28
)
⟶
(
x22
=
x3
⟶
x23
=
x4
⟶
x28
)
⟶
(
x24
=
x3
⟶
x25
=
x4
⟶
x28
)
⟶
(
x26
=
x3
⟶
x27
=
x4
⟶
x28
)
⟶
x28
)
⟶
x15
)
⟶
x15
(proof)