Search for blocks/addresses/...
Proofgold Asset
asset id
5082bb8ed3a7d8fd1aa27044a7194992c1cc7cfcbb2a7c2af103e12069a3e796
asset hash
636dfce838959fe06909a1a2a4b84ec22e8e7283edbfe73f6e1d6ad662e61002
bday / block
1605
tx
f69d8..
preasset
theory published by
PrGxv..
Prim
0
/
5cb91..
:
(
ι
→
ο
) →
ι
Def
False
:
ο
:=
∀ x0 : ο .
x0
Def
not
:
ο
→
ο
:=
λ x0 : ο .
x0
⟶
False
Def
and
:
ο
→
ο
→
ο
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Def
or
:
ο
→
ο
→
ο
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Def
iff
:
ο
→
ο
→
ο
:=
λ x0 x1 : ο .
and
(
x0
⟶
x1
)
(
x1
⟶
x0
)
Axiom
prop_ext
:
∀ x0 x1 : ο .
iff
x0
x1
⟶
x0
=
x1
Prim
1
/
6e234..
:
ι
→
ι
→
ο
Def
Subq
:
ι
→
ι
→
ο
:=
λ x0 x1 .
∀ x2 .
prim1
x2
x0
⟶
prim1
x2
x1
Prim
2
/
f5912..
:
ι
→
ι
→
ι
Def
91630..
:
ι
→
ι
:=
λ x0 .
prim2
x0
x0
Prim
3
/
961fc..
:
ι
→
ι
Def
7ee77..
:
ι
→
ι
→
ι
:=
λ x0 x1 .
prim2
(
prim2
x0
x1
)
(
91630..
x0
)
Def
c2e41..
:
ι
→
ι
→
ο
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 .
and
(
and
(
∀ x4 .
prim1
x4
x0
⟶
∀ x5 : ο .
(
∀ x6 .
and
(
prim1
x6
x1
)
(
prim1
(
7ee77..
x4
x6
)
x3
)
⟶
x5
)
⟶
x5
)
(
∀ x4 .
prim1
x4
x1
⟶
∀ x5 : ο .
(
∀ x6 .
and
(
prim1
x6
x0
)
(
prim1
(
7ee77..
x6
x4
)
x3
)
⟶
x5
)
⟶
x5
)
)
(
∀ x4 x5 x6 x7 .
prim1
(
7ee77..
x4
x5
)
x3
⟶
prim1
(
7ee77..
x6
x7
)
x3
⟶
iff
(
x4
=
x6
)
(
x5
=
x7
)
)
⟶
x2
)
⟶
x2
Axiom
Eps_i_ax
:
∀ x0 :
ι → ο
.
∀ x1 .
x0
x1
⟶
x0
(
prim0
x0
)
Axiom
0ddd1..
:
∀ x0 x1 .
(
∀ x2 .
iff
(
prim1
x2
x0
)
(
prim1
x2
x1
)
)
⟶
x0
=
x1
Axiom
53c21..
:
∀ x0 x1 x2 .
iff
(
prim1
x0
(
prim2
x1
x2
)
)
(
or
(
x0
=
x1
)
(
x0
=
x2
)
)
Axiom
UnionEq
:
∀ x0 x1 .
iff
(
prim1
x1
(
prim3
x0
)
)
(
∀ x2 : ο .
(
∀ x3 .
and
(
prim1
x1
x3
)
(
prim1
x3
x0
)
⟶
x2
)
⟶
x2
)
Axiom
113d7..
:
∀ x0 x1 .
prim1
x1
x0
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
prim1
x3
x0
)
(
not
(
∀ x4 : ο .
(
∀ x5 .
and
(
prim1
x5
x0
)
(
prim1
x5
x3
)
⟶
x4
)
⟶
x4
)
)
⟶
x2
)
⟶
x2
Axiom
e8b3c..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 x3 x4 .
x1
x2
x3
⟶
x1
x2
x4
⟶
x3
=
x4
)
⟶
∀ x2 : ο .
(
∀ x3 .
(
∀ x4 .
iff
(
prim1
x4
x3
)
(
∀ x5 : ο .
(
∀ x6 .
and
(
prim1
x6
x0
)
(
x1
x6
x4
)
⟶
x5
)
⟶
x5
)
)
⟶
x2
)
⟶
x2
Axiom
adb47..
:
∀ x0 .
∀ x1 : ο .
(
∀ x2 .
and
(
and
(
and
(
prim1
x0
x2
)
(
∀ x3 x4 .
prim1
x3
x2
⟶
Subq
x4
x3
⟶
prim1
x4
x2
)
)
(
∀ x3 .
prim1
x3
x2
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
prim1
x5
x2
)
(
∀ x6 .
Subq
x6
x3
⟶
prim1
x6
x5
)
⟶
x4
)
⟶
x4
)
)
(
∀ x3 .
Subq
x3
x2
⟶
or
(
c2e41..
x3
x2
)
(
prim1
x3
x2
)
)
⟶
x1
)
⟶
x1