Search for blocks/addresses/...
Proofgold Proposition
∀ x0 .
nat_p
x0
⟶
0
∈
x0
⟶
∃ x1 .
and
(
x1
∈
omega
)
(
∃ x3 :
ι → ι
.
and
(
and
(
168aa..
prime_nat
x1
x3
)
(
05ecb..
x3
x1
=
x0
)
)
(
∀ x5 .
x5
∈
omega
⟶
∀ x6 :
ι → ι
.
168aa..
prime_nat
x5
x6
⟶
05ecb..
x6
x5
=
x0
⟶
and
(
x5
=
x1
)
(
∀ x7 .
x7
∈
x1
⟶
x6
x7
=
x3
x7
)
)
)
type
prop
theory
HotG
name
-
proof
PUQQ9..
Megalodon
prime_factorization_ex_uniq
proofgold address
TMaSw..
prime_factorization_ex_uniq
creator
30111
PrQUS..
/
1cb16..
owner
30111
PrQUS..
/
1cb16..
term root
ae2a4..