Search for blocks/addresses/...
Proofgold Address
address
PURxq7vEGY4QbFR5cPrrZJMND61ztPi75yd
total
0
mg
-
conjpub
-
current assets
57f1e..
/
23349..
bday:
28153
doc published by
Pr5Zc..
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
omega
omega
:
ι
Param
mul_nat
mul_nat
:
ι
→
ι
→
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
even_nat
even_nat
:=
λ x0 .
and
(
x0
∈
omega
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
omega
)
(
x0
=
mul_nat
2
x2
)
⟶
x1
)
⟶
x1
)
Definition
divides_nat
divides_nat
:=
λ x0 x1 .
and
(
and
(
x0
∈
omega
)
(
x1
∈
omega
)
)
(
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
omega
)
(
mul_nat
x0
x3
=
x1
)
⟶
x2
)
⟶
x2
)
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Param
nat_p
nat_p
:
ι
→
ο
Known
nat_p_omega
nat_p_omega
:
∀ x0 .
nat_p
x0
⟶
x0
∈
omega
Known
nat_2
nat_2
:
nat_p
2
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Theorem
b2900..
:
∀ x0 .
even_nat
x0
⟶
divides_nat
2
x0
(proof)
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Definition
prime_nat
prime_nat
:=
λ x0 .
and
(
and
(
x0
∈
omega
)
(
1
∈
x0
)
)
(
∀ x1 .
x1
∈
omega
⟶
divides_nat
x1
x0
⟶
or
(
x1
=
1
)
(
x1
=
x0
)
)
Definition
False
False
:=
∀ x0 : ο .
x0
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
neq_2_1
neq_2_1
:
2
=
1
⟶
∀ x0 : ο .
x0
Theorem
447ce..
:
∀ x0 .
prime_nat
x0
⟶
even_nat
x0
⟶
x0
=
2
(proof)
Param
int
int
:
ι
Param
add_SNo
add_SNo
:
ι
→
ι
→
ι
Param
mul_SNo
mul_SNo
:
ι
→
ι
→
ι
Known
c6211..
:
∀ x0 .
x0
∈
int
⟶
∀ x1 .
x1
∈
int
⟶
∀ x2 .
x2
∈
int
⟶
∀ x3 .
x3
∈
int
⟶
∀ x4 .
x4
∈
int
⟶
∀ x5 .
x5
∈
int
⟶
x0
=
add_SNo
(
mul_SNo
x2
x2
)
(
add_SNo
(
mul_SNo
x3
x3
)
(
add_SNo
(
mul_SNo
x4
x4
)
(
mul_SNo
x5
x5
)
)
)
⟶
∀ x6 .
x6
∈
int
⟶
∀ x7 .
x7
∈
int
⟶
∀ x8 .
x8
∈
int
⟶
∀ x9 .
x9
∈
int
⟶
x1
=
add_SNo
(
mul_SNo
x6
x6
)
(
add_SNo
(
mul_SNo
x7
x7
)
(
add_SNo
(
mul_SNo
x8
x8
)
(
mul_SNo
x9
x9
)
)
)
⟶
∀ x10 : ο .
(
∀ x11 .
x11
∈
omega
⟶
∀ x12 .
x12
∈
omega
⟶
∀ x13 .
x13
∈
omega
⟶
∀ x14 .
x14
∈
omega
⟶
mul_SNo
x0
x1
=
add_SNo
(
mul_SNo
x11
x11
)
(
add_SNo
(
mul_SNo
x12
x12
)
(
add_SNo
(
mul_SNo
x13
x13
)
(
mul_SNo
x14
x14
)
)
)
⟶
x10
)
⟶
x10
Param
odd_nat
odd_nat
:
ι
→
ο
Known
omega_nat_p
omega_nat_p
:
∀ x0 .
x0
∈
omega
⟶
nat_p
x0
Known
nat_complete_ind
nat_complete_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
nat_p
x1
⟶
(
∀ x2 .
x2
∈
x1
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
054a4..
:
∀ x0 :
ι → ο
.
x0
0
⟶
x0
1
⟶
x0
2
⟶
(
∀ x1 .
nat_p
x1
⟶
x0
(
ordsucc
(
ordsucc
(
ordsucc
x1
)
)
)
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
nat_0
nat_0
:
nat_p
0
Param
SNo
SNo
:
ι
→
ο
Known
mul_SNo_zeroR
mul_SNo_zeroR
:
∀ x0 .
SNo
x0
⟶
mul_SNo
x0
0
=
0
Known
SNo_0
SNo_0
:
SNo
0
Known
add_SNo_0L
add_SNo_0L
:
∀ x0 .
SNo
x0
⟶
add_SNo
0
x0
=
x0
Known
nat_1
nat_1
:
nat_p
1
Known
mul_SNo_oneR
mul_SNo_oneR
:
∀ x0 .
SNo
x0
⟶
mul_SNo
x0
1
=
x0
Known
SNo_1
SNo_1
:
SNo
1
Known
add_SNo_1_1_2
add_SNo_1_1_2
:
add_SNo
1
1
=
2
Known
SNo_2
SNo_2
:
SNo
2
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
even_nat_or_odd_nat
even_nat_or_odd_nat
:
∀ x0 .
nat_p
x0
⟶
or
(
even_nat
x0
)
(
odd_nat
x0
)
Known
neq_ordsucc_0
neq_ordsucc_0
:
∀ x0 .
ordsucc
x0
=
0
⟶
∀ x1 : ο .
x1
Known
ordsucc_inj
ordsucc_inj
:
∀ x0 x1 .
ordsucc
x0
=
ordsucc
x1
⟶
x0
=
x1
Known
b8d2f..
:
∀ x0 .
x0
∈
omega
⟶
not
(
prime_nat
x0
)
⟶
1
∈
x0
⟶
∀ x1 : ο .
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
1
∈
x2
⟶
1
∈
x3
⟶
x0
=
mul_nat
x2
x3
⟶
x1
)
⟶
x1
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
mul_nat_mul_SNo
mul_nat_mul_SNo
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
mul_nat
x0
x1
=
mul_SNo
x0
x1
Known
Subq_omega_int
Subq_omega_int
:
omega
⊆
int
Known
nat_p_trans
nat_p_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
nat_p
x1
Known
nat_ordsucc_in_ordsucc
nat_ordsucc_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
∈
ordsucc
x0
Known
nat_0_in_ordsucc
nat_0_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
0
∈
ordsucc
x0
Known
nat_ordsucc
nat_ordsucc
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
x0
)
Theorem
8ff04..
:
(
∀ x0 .
prime_nat
x0
⟶
odd_nat
x0
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
omega
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
omega
)
(
∀ x5 : ο .
(
∀ x6 .
and
(
x6
∈
omega
)
(
∀ x7 : ο .
(
∀ x8 .
and
(
x8
∈
omega
)
(
x0
=
add_SNo
(
mul_SNo
x2
x2
)
(
add_SNo
(
mul_SNo
x4
x4
)
(
add_SNo
(
mul_SNo
x6
x6
)
(
mul_SNo
x8
x8
)
)
)
)
⟶
x7
)
⟶
x7
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
)
⟶
x1
)
⟶
x1
)
⟶
∀ x0 .
x0
∈
omega
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
omega
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
omega
)
(
∀ x5 : ο .
(
∀ x6 .
and
(
x6
∈
omega
)
(
∀ x7 : ο .
(
∀ x8 .
and
(
x8
∈
omega
)
(
x0
=
add_SNo
(
mul_SNo
x2
x2
)
(
add_SNo
(
mul_SNo
x4
x4
)
(
add_SNo
(
mul_SNo
x6
x6
)
(
mul_SNo
x8
x8
)
)
)
)
⟶
x7
)
⟶
x7
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
)
⟶
x1
)
⟶
x1
(proof)
previous assets