Search for blocks/addresses/...
Proofgold Asset
asset id
102d7d310302d7bd79eb6c45f8ef0bdc79c2807ecbc061848032cd23f5c7987e
asset hash
0e5f8fe3072c5adc4c8b5e9bc74ad748153208cb05c751cc53bd017f0b640063
bday / block
628
tx
2dedf..
preasset
doc published by
Pr4Ru..
Definition
False
:=
∀ x0 : ο .
x0
Known
FalseE
FalseE
:
False
⟶
False
Known
8106d..
notI
:
∀ x0 : ο .
(
x0
⟶
False
)
⟶
not
x0
Known
notE
notE
:
∀ x0 : ο .
not
x0
⟶
x0
⟶
False
Known
andE
andE
:
∀ x0 x1 : ο .
and
x0
x1
⟶
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Theorem
39854..
andEL
:
∀ x0 x1 : ο .
and
x0
x1
⟶
x0
(proof)
Theorem
eb789..
andER
:
∀ x0 x1 : ο .
and
x0
x1
⟶
x1
(proof)
Known
7c02f..
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
13bcd..
iff_def
:
iff
=
λ x1 x2 : ο .
and
(
x1
⟶
x2
)
(
x2
⟶
x1
)
Theorem
9fc94..
:
∀ x0 x1 : ο .
iff
x0
x1
⟶
and
(
x0
⟶
x1
)
(
x1
⟶
x0
)
(proof)
Theorem
50594..
iffEL
:
∀ x0 x1 : ο .
iff
x0
x1
⟶
x0
⟶
x1
(proof)
Theorem
93720..
iffER
:
∀ x0 x1 : ο .
iff
x0
x1
⟶
x1
⟶
x0
(proof)
Known
32c82..
iffI
:
∀ x0 x1 : ο .
(
x0
⟶
x1
)
⟶
(
x1
⟶
x0
)
⟶
iff
x0
x1
Theorem
ad656..
:
∀ x0 :
ι → ο
.
∀ x1 .
x0
x1
⟶
∀ x2 : ο .
(
∀ x3 .
x0
x3
⟶
x2
)
⟶
x2
(proof)
Known
c1173..
Subq_def
:
Subq
=
λ x1 x2 .
∀ x3 .
In
x3
x1
⟶
In
x3
x2
Theorem
b0dce..
SubqI
:
∀ x0 x1 .
(
∀ x2 .
In
x2
x0
⟶
In
x2
x1
)
⟶
Subq
x0
x1
(proof)
Theorem
367e6..
SubqE
:
∀ x0 x1 .
Subq
x0
x1
⟶
∀ x2 .
In
x2
x0
⟶
In
x2
x1
(proof)
Theorem
6696a..
Subq_ref
:
∀ x0 .
Subq
x0
x0
(proof)
Known
7f305..
EmptyAx
:
not
(
∀ x0 : ο .
(
∀ x1 .
In
x1
0
⟶
x0
)
⟶
x0
)
Theorem
2901c..
EmptyE
:
∀ x0 .
In
x0
0
⟶
False
(proof)
Known
da6c8..
PowerEq
:
∀ x0 x1 .
iff
(
In
x1
(
Power
x0
)
)
(
Subq
x1
x0
)
Theorem
2d44a..
PowerI
:
∀ x0 x1 .
Subq
x1
x0
⟶
In
x1
(
Power
x0
)
(proof)
Theorem
ae89b..
PowerE
:
∀ x0 x1 .
In
x1
(
Power
x0
)
⟶
Subq
x1
x0
(proof)
Theorem
7b5f8..
Self_In_Power
:
∀ x0 .
In
x0
(
Power
x0
)
(proof)
Theorem
025eb..
:
0
=
Power
0
⟶
False
(proof)
Theorem
204a5..
:
(
∀ x0 :
ι →
ι → ο
.
∀ x1 :
ι →
ι → ι
.
∀ x2 x3 :
ι → ο
.
∀ x4 :
ι → ι
.
∀ x5 x6 x7 .
and
(
x6
=
x1
(
x1
x5
(
x1
x7
(
x1
(
x1
(
x1
(
x1
x6
(
x1
(
x1
x5
(
x1
x5
(
x1
(
x1
x5
(
x1
(
x4
x5
)
(
x1
(
x1
x7
(
x1
x6
(
x1
x6
x6
)
)
)
x5
)
)
)
(
x1
(
x4
(
x1
(
x1
(
x4
x7
)
x5
)
(
x1
x5
x5
)
)
)
(
x1
x6
(
x1
x6
(
x1
(
x1
(
x1
x5
(
x1
(
x1
x5
(
x1
(
x4
x6
)
x7
)
)
(
x4
(
x1
x7
x5
)
)
)
)
x6
)
(
x4
(
x1
(
x1
x7
(
x1
x5
(
x1
(
x4
(
x1
x5
x7
)
)
x5
)
)
)
(
x1
(
x1
(
x1
x6
(
x1
(
x4
x5
)
x6
)
)
x6
)
(
x4
(
x4
(
x1
(
x1
(
x1
(
x1
x5
(
x1
(
x1
x6
(
x1
(
x1
x7
x5
)
x7
)
)
x6
)
)
x7
)
(
x1
x7
(
x1
x5
x5
)
)
)
x6
)
)
)
)
)
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x1
(
x1
(
x1
x6
(
x1
x5
x5
)
)
(
x4
(
x4
(
x1
x7
(
x4
(
x4
(
x1
x7
x5
)
)
)
)
)
)
)
x5
)
x6
)
(
x1
x6
x7
)
)
)
)
x5
)
x5
)
(
x4
x6
)
)
)
)
(
x1
(
x1
(
x4
(
x1
(
x4
(
x1
(
x1
(
x1
(
x1
x7
(
x1
(
x4
(
x4
(
x1
(
x1
x5
x6
)
x7
)
)
)
(
x4
(
x1
x5
x5
)
)
)
)
x5
)
(
x4
x5
)
)
(
x1
(
x1
(
x1
(
x1
(
x1
x5
x7
)
(
x4
(
x4
(
x4
x7
)
)
)
)
x7
)
x6
)
x5
)
)
)
(
x1
(
x1
(
x1
x6
x5
)
(
x4
x6
)
)
x6
)
)
)
x7
)
x6
)
)
(
∃ x8 .
x3
(
x4
x5
)
)
)
⟶
False
(proof)
Theorem
2b6c7..
:
(
∀ x0 :
ι →
ι → ο
.
∀ x1 :
ι →
ι → ι
.
∀ x2 x3 :
ι → ο
.
∀ x4 :
ι → ι
.
∀ x5 x6 x7 x8 x9 .
and
(
∀ x10 .
x4
x9
=
x10
⟶
and
(
x2
x10
)
(
x7
=
x5
⟶
and
(
∀ x11 .
x9
=
x8
)
(
∃ x11 .
x3
x10
)
)
⟶
∃ x11 .
x7
=
x7
)
(
not
(
x3
(
x4
(
x4
(
x1
x7
x5
)
)
)
)
)
⟶
x6
=
x9
)
⟶
False
(proof)
Theorem
1c497..
:
(
∀ x0 :
ι →
ι → ο
.
∀ x1 :
ι →
ι → ι
.
∀ x2 x3 :
ι → ο
.
∀ x4 :
ι → ι
.
∀ x5 x6 x7 .
x4
(
x1
(
x1
(
x1
(
x1
(
x1
(
x1
x6
x5
)
(
x1
(
x1
(
x1
x6
x5
)
(
x1
x7
(
x1
(
x1
(
x1
x5
x5
)
(
x1
(
x1
(
x1
(
x1
x5
(
x1
(
x1
x6
(
x1
x5
(
x1
x5
x7
)
)
)
x5
)
)
x7
)
(
x1
(
x4
x6
)
x7
)
)
(
x1
(
x1
(
x1
(
x1
x5
(
x4
(
x1
x7
x5
)
)
)
(
x1
x6
x6
)
)
(
x1
x6
(
x1
x7
x5
)
)
)
x5
)
)
)
x7
)
)
)
x5
)
)
x6
)
(
x1
x6
(
x1
x5
(
x1
(
x1
(
x4
x5
)
(
x1
(
x1
x6
x6
)
x6
)
)
x5
)
)
)
)
(
x4
(
x4
x6
)
)
)
x5
)
=
x4
(
x4
x7
)
)
⟶
False
(proof)
Theorem
d3bc2..
:
(
∀ x0 :
ι →
ι → ο
.
∀ x1 :
ι →
ι → ι
.
∀ x2 x3 :
ι → ο
.
∀ x4 :
ι → ι
.
∀ x5 x6 x7 .
∀ x8 : ο .
(
∀ x9 .
and
(
x9
=
x7
)
(
x4
(
x1
(
x1
(
x4
(
x1
(
x1
(
x1
(
x1
(
x1
x5
x7
)
(
x4
(
x4
(
x1
(
x1
x7
x5
)
x7
)
)
)
)
(
x1
(
x1
x5
x5
)
(
x1
(
x4
x5
)
(
x1
x7
(
x1
(
x4
x5
)
x9
)
)
)
)
)
x9
)
x9
)
)
x5
)
(
x4
x5
)
)
=
x6
)
⟶
x8
)
⟶
x8
)
⟶
False
(proof)