Search for blocks/addresses/...
Proofgold Asset
asset id
39cc17ccc704af1efa815348a9b5db386767241e9f8306540af2c0f41bc61f6f
asset hash
71a2aacb6bbe9c08e1ae10fcbad8ca46246db5132e98cbc46214df383aff7414
bday / block
19897
tx
ecdfe..
preasset
doc published by
Pr4zB..
Param
equip
equip
:
ι
→
ι
→
ο
Param
binunion
binunion
:
ι
→
ι
→
ι
Param
Sing
Sing
:
ι
→
ι
Definition
SetAdjoin
SetAdjoin
:=
λ x0 x1 .
binunion
x0
(
Sing
x1
)
Param
UPair
UPair
:
ι
→
ι
→
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
u1
:=
1
Definition
u2
:=
ordsucc
u1
Definition
u3
:=
ordsucc
u2
Definition
u4
:=
ordsucc
u3
Definition
u5
:=
ordsucc
u4
Known
equip_sym
equip_sym
:
∀ x0 x1 .
equip
x0
x1
⟶
equip
x1
x0
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
e8bc0..
equip_adjoin_ordsucc
:
∀ x0 x1 x2 .
nIn
x2
x1
⟶
equip
x0
x1
⟶
equip
(
ordsucc
x0
)
(
binunion
x1
(
Sing
x2
)
)
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
1aece..
:
∀ x0 x1 x2 x3 x4 .
x4
∈
SetAdjoin
(
SetAdjoin
(
UPair
x0
x1
)
x2
)
x3
⟶
∀ x5 :
ι → ο
.
x5
x0
⟶
x5
x1
⟶
x5
x2
⟶
x5
x3
⟶
x5
x4
Known
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Known
d9e1e..
:
∀ x0 x1 x2 x3 .
(
x0
=
x1
⟶
∀ x4 : ο .
x4
)
⟶
(
x0
=
x2
⟶
∀ x4 : ο .
x4
)
⟶
(
x0
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
(
x1
=
x2
⟶
∀ x4 : ο .
x4
)
⟶
(
x1
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
equip
(
SetAdjoin
(
SetAdjoin
(
UPair
x0
x1
)
x2
)
x3
)
u4
Theorem
5b07e..
:
∀ x0 x1 x2 x3 x4 .
(
x0
=
x1
⟶
∀ x5 : ο .
x5
)
⟶
(
x0
=
x2
⟶
∀ x5 : ο .
x5
)
⟶
(
x0
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
(
x0
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
x1
=
x2
⟶
∀ x5 : ο .
x5
)
⟶
(
x1
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
(
x1
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
x2
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
(
x2
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
equip
(
SetAdjoin
(
SetAdjoin
(
SetAdjoin
(
UPair
x0
x1
)
x2
)
x3
)
x4
)
u5
(proof)
Param
and
and
:
ο
→
ο
→
ο
Param
Subq
Subq
:
ι
→
ι
→
ο
Definition
u6
:=
ordsucc
u5
Definition
u7
:=
ordsucc
u6
Definition
u8
:=
ordsucc
u7
Definition
u9
:=
ordsucc
u8
Known
e041c..
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 x2 .
x0
x1
x2
⟶
x0
x2
x1
)
⟶
not
(
or
(
∀ x1 : ο .
(
∀ x2 .
and
(
x2
⊆
u9
)
(
and
(
equip
u3
x2
)
(
∀ x3 .
x3
∈
x2
⟶
∀ x4 .
x4
∈
x2
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
x0
x3
x4
)
)
⟶
x1
)
⟶
x1
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
x2
⊆
u9
)
(
and
(
equip
u4
x2
)
(
∀ x3 .
x3
∈
x2
⟶
∀ x4 .
x4
∈
x2
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
not
(
x0
x3
x4
)
)
)
⟶
x1
)
⟶
x1
)
)
⟶
∀ x1 .
x1
∈
u9
⟶
∀ x2 : ο .
(
∀ x3 .
x3
∈
u9
⟶
∀ x4 .
x4
∈
u9
⟶
∀ x5 .
x5
∈
u9
⟶
(
x1
=
x3
⟶
∀ x6 : ο .
x6
)
⟶
(
x1
=
x4
⟶
∀ x6 : ο .
x6
)
⟶
(
x1
=
x5
⟶
∀ x6 : ο .
x6
)
⟶
(
x3
=
x4
⟶
∀ x6 : ο .
x6
)
⟶
(
x3
=
x5
⟶
∀ x6 : ο .
x6
)
⟶
(
x4
=
x5
⟶
∀ x6 : ο .
x6
)
⟶
x0
x1
x3
⟶
x0
x1
x4
⟶
x0
x1
x5
⟶
not
(
x0
x3
x4
)
⟶
not
(
x0
x3
x5
)
⟶
not
(
x0
x4
x5
)
⟶
(
∀ x6 .
x6
∈
u9
⟶
x0
x1
x6
⟶
x6
∈
SetAdjoin
(
SetAdjoin
(
UPair
x1
x3
)
x4
)
x5
)
⟶
x2
)
⟶
x2
Known
f1644..
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 x2 .
x0
x1
x2
⟶
x0
x2
x1
)
⟶
not
(
or
(
∀ x1 : ο .
(
∀ x2 .
and
(
x2
⊆
u9
)
(
and
(
equip
u3
x2
)
(
∀ x3 .
x3
∈
x2
⟶
∀ x4 .
x4
∈
x2
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
x0
x3
x4
)
)
⟶
x1
)
⟶
x1
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
x2
⊆
u9
)
(
and
(
equip
u4
x2
)
(
∀ x3 .
x3
∈
x2
⟶
∀ x4 .
x4
∈
x2
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
not
(
x0
x3
x4
)
)
)
⟶
x1
)
⟶
x1
)
)
⟶
∀ x1 .
x1
∈
u9
⟶
∀ x2 .
x2
∈
u9
⟶
(
x1
=
x2
⟶
∀ x3 : ο .
x3
)
⟶
x0
x1
x2
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
u9
⟶
∀ x5 .
x5
∈
u9
⟶
(
x1
=
x4
⟶
∀ x6 : ο .
x6
)
⟶
(
x1
=
x5
⟶
∀ x6 : ο .
x6
)
⟶
(
x2
=
x4
⟶
∀ x6 : ο .
x6
)
⟶
(
x2
=
x5
⟶
∀ x6 : ο .
x6
)
⟶
(
x4
=
x5
⟶
∀ x6 : ο .
x6
)
⟶
x0
x1
x4
⟶
x0
x1
x5
⟶
not
(
x0
x2
x4
)
⟶
not
(
x0
x2
x5
)
⟶
not
(
x0
x4
x5
)
⟶
(
∀ x6 .
x6
∈
u9
⟶
x0
x1
x6
⟶
x6
∈
SetAdjoin
(
SetAdjoin
(
UPair
x1
x2
)
x4
)
x5
)
⟶
x3
)
⟶
x3
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Param
nat_p
nat_p
:
ι
→
ο
Param
atleastp
atleastp
:
ι
→
ι
→
ο
Known
4fb58..
Pigeonhole_not_atleastp_ordsucc
:
∀ x0 .
nat_p
x0
⟶
not
(
atleastp
(
ordsucc
x0
)
x0
)
Known
nat_9
nat_9
:
nat_p
9
Definition
u10
:=
ordsucc
u9
Known
d140d..
:
∀ x0 x1 .
x1
∈
x0
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
(
x1
=
x2
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x3
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x3
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x4
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x4
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x4
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x5
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x5
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x5
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x5
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x6
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x6
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x6
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x6
⟶
∀ x11 : ο .
x11
)
⟶
(
x5
=
x6
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x5
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x6
=
x7
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x5
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x6
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x7
=
x8
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x5
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x6
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x7
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x8
=
x9
⟶
∀ x11 : ο .
x11
)
⟶
(
x1
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x2
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x3
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x4
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x5
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x6
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x7
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x8
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
(
x9
=
x10
⟶
∀ x11 : ο .
x11
)
⟶
atleastp
u10
x0
Known
neq_i_sym
neq_i_sym
:
∀ x0 x1 .
(
x0
=
x1
⟶
∀ x2 : ο .
x2
)
⟶
x1
=
x0
⟶
∀ x2 : ο .
x2
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
UPairE
UPairE
:
∀ x0 x1 x2 .
x0
∈
UPair
x1
x2
⟶
or
(
x0
=
x1
)
(
x0
=
x2
)
Known
binunionI1
binunionI1
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
x2
∈
binunion
x0
x1
Known
UPairI1
UPairI1
:
∀ x0 x1 .
x0
∈
UPair
x0
x1
Known
binunionI2
binunionI2
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
x2
∈
binunion
x0
x1
Known
SingI
SingI
:
∀ x0 .
x0
∈
Sing
x0
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Known
UPairI2
UPairI2
:
∀ x0 x1 .
x1
∈
UPair
x0
x1
Theorem
bd9af..
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 x2 .
x0
x1
x2
⟶
x0
x2
x1
)
⟶
not
(
or
(
∀ x1 : ο .
(
∀ x2 .
and
(
x2
⊆
u9
)
(
and
(
equip
u3
x2
)
(
∀ x3 .
x3
∈
x2
⟶
∀ x4 .
x4
∈
x2
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
x0
x3
x4
)
)
⟶
x1
)
⟶
x1
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
x2
⊆
u9
)
(
and
(
equip
u4
x2
)
(
∀ x3 .
x3
∈
x2
⟶
∀ x4 .
x4
∈
x2
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
not
(
x0
x3
x4
)
)
)
⟶
x1
)
⟶
x1
)
)
⟶
∀ x1 .
x1
∈
u9
⟶
∀ x2 : ο .
(
∀ x3 .
x3
∈
u9
⟶
∀ x4 .
x4
∈
u9
⟶
∀ x5 .
x5
∈
u9
⟶
∀ x6 .
x6
∈
u9
⟶
(
x1
=
x3
⟶
∀ x7 : ο .
x7
)
⟶
(
x1
=
x4
⟶
∀ x7 : ο .
x7
)
⟶
(
x1
=
x5
⟶
∀ x7 : ο .
x7
)
⟶
(
x1
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
(
x3
=
x4
⟶
∀ x7 : ο .
x7
)
⟶
(
x3
=
x5
⟶
∀ x7 : ο .
x7
)
⟶
(
x3
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
(
x4
=
x5
⟶
∀ x7 : ο .
x7
)
⟶
(
x4
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
(
x5
=
x6
⟶
∀ x7 : ο .
x7
)
⟶
x0
x1
x3
⟶
x0
x1
x4
⟶
x0
x1
x5
⟶
not
(
x0
x3
x4
)
⟶
not
(
x0
x3
x5
)
⟶
not
(
x0
x4
x5
)
⟶
(
∀ x7 .
x7
∈
u9
⟶
x0
x1
x7
⟶
x7
∈
SetAdjoin
(
SetAdjoin
(
UPair
x1
x3
)
x4
)
x5
)
⟶
x0
x6
x3
⟶
x0
x6
x4
⟶
x2
)
⟶
x2
(proof)