Search for blocks/addresses/...
Proofgold Address
address
PUbWYj8nbhsJTjYWvRsquTyLPfV7wDqjXXS
total
0
mg
-
conjpub
-
current assets
b73d9..
/
4894a..
bday:
15286
doc published by
Pr4zB..
Param
nat_p
nat_p
:
ι
→
ο
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Param
add_nat
add_nat
:
ι
→
ι
→
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Known
nat_ind
nat_ind
:
∀ x0 :
ι → ο
.
x0
0
⟶
(
∀ x1 .
nat_p
x1
⟶
x0
x1
⟶
x0
(
ordsucc
x1
)
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
add_nat_0R
add_nat_0R
:
∀ x0 .
add_nat
x0
0
=
x0
Known
Subq_ref
Subq_ref
:
∀ x0 .
x0
⊆
x0
Known
add_nat_SR
add_nat_SR
:
∀ x0 x1 .
nat_p
x1
⟶
add_nat
x0
(
ordsucc
x1
)
=
ordsucc
(
add_nat
x0
x1
)
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Theorem
4d87b..
:
∀ x0 x1 .
nat_p
x1
⟶
x0
⊆
add_nat
x0
x1
(proof)
Param
mul_nat
mul_nat
:
ι
→
ι
→
ι
Known
mul_nat_SR
mul_nat_SR
:
∀ x0 x1 .
nat_p
x1
⟶
mul_nat
x0
(
ordsucc
x1
)
=
add_nat
x0
(
mul_nat
x0
x1
)
Known
nat_0
nat_0
:
nat_p
0
Known
mul_nat_0R
mul_nat_0R
:
∀ x0 .
mul_nat
x0
0
=
0
Theorem
mul_nat_1R
mul_nat_1R
:
∀ x0 .
mul_nat
x0
1
=
x0
(proof)
Known
mul_nat_com
mul_nat_com
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
mul_nat
x0
x1
=
mul_nat
x1
x0
Known
nat_1
nat_1
:
nat_p
1
Theorem
f11bb..
:
∀ x0 .
nat_p
x0
⟶
mul_nat
1
x0
=
x0
(proof)
Param
nat_primrec
nat_primrec
:
ι
→
(
ι
→
ι
→
ι
) →
ι
→
ι
Definition
exp_nat
exp_nat
:=
λ x0 .
nat_primrec
1
(
λ x1 .
mul_nat
x0
)
Known
nat_primrec_0
nat_primrec_0
:
∀ x0 .
∀ x1 :
ι →
ι → ι
.
nat_primrec
x0
x1
0
=
x0
Known
nat_primrec_S
nat_primrec_S
:
∀ x0 .
∀ x1 :
ι →
ι → ι
.
∀ x2 .
nat_p
x2
⟶
nat_primrec
x0
x1
(
ordsucc
x2
)
=
x1
x2
(
nat_primrec
x0
x1
x2
)
Known
mul_nat_p
mul_nat_p
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
nat_p
(
mul_nat
x0
x1
)
Theorem
4f402..
exp_nat_p
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
nat_p
(
exp_nat
x0
x1
)
(proof)
Param
setminus
setminus
:
ι
→
ι
→
ι
Param
Sing
Sing
:
ι
→
ι
Known
PowerI
PowerI
:
∀ x0 x1 .
x1
⊆
x0
⟶
x1
∈
prim4
x0
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Known
PowerE
PowerE
:
∀ x0 x1 .
x1
∈
prim4
x0
⟶
x1
⊆
x0
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
setminusI
setminusI
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
nIn
x2
x1
⟶
x2
∈
setminus
x0
x1
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Theorem
39f67..
:
∀ x0 x1 .
setminus
x1
(
Sing
x0
)
∈
prim4
x0
⟶
x1
∈
prim4
(
ordsucc
x0
)
(proof)
Param
binunion
binunion
:
ι
→
ι
→
ι
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Theorem
35356..
:
∀ x0 x1 .
x1
∈
prim4
x0
⟶
binunion
x1
(
Sing
x0
)
∈
prim4
(
ordsucc
x0
)
(proof)
Param
Inj0
Inj0
:
ι
→
ι
Param
Inj1
Inj1
:
ι
→
ι
Param
setsum
setsum
:
ι
→
ι
→
ι
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Known
setsum_Inj_inv
setsum_Inj_inv
:
∀ x0 x1 x2 .
x2
∈
setsum
x0
x1
⟶
or
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
x2
=
Inj0
x4
)
⟶
x3
)
⟶
x3
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x1
)
(
x2
=
Inj1
x4
)
⟶
x3
)
⟶
x3
)
Theorem
f4c7c..
:
∀ x0 x1 .
∀ x2 :
ι → ο
.
(
∀ x3 .
x3
∈
x0
⟶
x2
(
Inj0
x3
)
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
x2
(
Inj1
x3
)
)
⟶
∀ x3 .
x3
∈
setsum
x0
x1
⟶
x2
x3
(proof)
Param
bij
bij
:
ι
→
ι
→
(
ι
→
ι
) →
ο
Definition
equip
equip
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
bij
x0
x1
x3
⟶
x2
)
⟶
x2
Known
Power_0_Sing_0
Power_0_Sing_0
:
prim4
0
=
Sing
0
Known
eq_1_Sing0
eq_1_Sing0
:
1
=
Sing
0
Known
equip_ref
equip_ref
:
∀ x0 .
equip
x0
x0
Known
add_nat_1_1_2
add_nat_1_1_2
:
add_nat
1
1
=
2
Known
mul_add_nat_distrR
mul_add_nat_distrR
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
∀ x2 .
nat_p
x2
⟶
mul_nat
(
add_nat
x0
x1
)
x2
=
add_nat
(
mul_nat
x0
x2
)
(
mul_nat
x1
x2
)
Known
equip_sym
equip_sym
:
∀ x0 x1 .
equip
x0
x1
⟶
equip
x1
x0
Known
equip_tra
equip_tra
:
∀ x0 x1 x2 .
equip
x0
x1
⟶
equip
x1
x2
⟶
equip
x0
x2
Known
c88e0..
:
∀ x0 x1 x2 x3 .
nat_p
x0
⟶
nat_p
x1
⟶
equip
x0
x2
⟶
equip
x1
x3
⟶
equip
(
add_nat
x0
x1
)
(
setsum
x2
x3
)
Known
bijE
bijE
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
bij
x0
x1
x2
⟶
∀ x3 : ο .
(
(
∀ x4 .
x4
∈
x0
⟶
x2
x4
∈
x1
)
⟶
(
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
x2
x4
=
x2
x5
⟶
x4
=
x5
)
⟶
(
∀ x4 .
x4
∈
x1
⟶
∀ x5 : ο .
(
∀ x6 .
and
(
x6
∈
x0
)
(
x2
x6
=
x4
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
Param
combine_funcs
combine_funcs
:
ι
→
ι
→
(
ι
→
ι
) →
(
ι
→
ι
) →
ι
→
ι
Known
bijI
bijI
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
x0
)
(
x2
x5
=
x3
)
⟶
x4
)
⟶
x4
)
⟶
bij
x0
x1
x2
Known
combine_funcs_eq1
combine_funcs_eq1
:
∀ x0 x1 .
∀ x2 x3 :
ι → ι
.
∀ x4 .
combine_funcs
x0
x1
x2
x3
(
Inj0
x4
)
=
x2
x4
Known
Power_Subq
Power_Subq
:
∀ x0 x1 .
x0
⊆
x1
⟶
prim4
x0
⊆
prim4
x1
Known
combine_funcs_eq2
combine_funcs_eq2
:
∀ x0 x1 .
∀ x2 x3 :
ι → ι
.
∀ x4 .
combine_funcs
x0
x1
x2
x3
(
Inj1
x4
)
=
x3
x4
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Known
binunionI2
binunionI2
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
x2
∈
binunion
x0
x1
Known
SingI
SingI
:
∀ x0 .
x0
∈
Sing
x0
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Known
binunionI1
binunionI1
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
x2
∈
binunion
x0
x1
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
Inj1_setsum
Inj1_setsum
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
Inj1
x2
∈
setsum
x0
x1
Known
eb0c4..
binunion_remove1_eq
:
∀ x0 x1 .
x1
∈
x0
⟶
x0
=
binunion
(
setminus
x0
(
Sing
x1
)
)
(
Sing
x1
)
Known
setminusE
setminusE
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
and
(
x2
∈
x0
)
(
nIn
x2
x1
)
Known
ordsuccE
ordsuccE
:
∀ x0 x1 .
x1
∈
ordsucc
x0
⟶
or
(
x1
∈
x0
)
(
x1
=
x0
)
Known
Inj0_setsum
Inj0_setsum
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
Inj0
x2
∈
setsum
x0
x1
Known
nat_2
nat_2
:
nat_p
2
Theorem
293d3..
:
∀ x0 .
nat_p
x0
⟶
equip
(
prim4
x0
)
(
exp_nat
2
x0
)
(proof)
Definition
inj
inj
:=
λ x0 x1 .
λ x2 :
ι → ι
.
and
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
Definition
atleastp
atleastp
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
inj
x0
x1
x3
⟶
x2
)
⟶
x2
Known
EmptyE
EmptyE
:
∀ x0 .
nIn
x0
0
Theorem
71267..
:
∀ x0 .
atleastp
0
x0
(proof)
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Known
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Known
If_i_0
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Known
nat_ordsucc_in_ordsucc
nat_ordsucc_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
∈
ordsucc
x0
Known
nat_trans
nat_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
x1
⊆
x0
Known
ordsucc_inj
ordsucc_inj
:
∀ x0 x1 .
ordsucc
x0
=
ordsucc
x1
⟶
x0
=
x1
Known
nat_ordsucc_trans
nat_ordsucc_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
ordsucc
x0
⟶
x1
⊆
x0
Known
nat_inv
nat_inv
:
∀ x0 .
nat_p
x0
⟶
or
(
x0
=
0
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
nat_p
x2
)
(
x0
=
ordsucc
x2
)
⟶
x1
)
⟶
x1
)
Known
nat_0_in_ordsucc
nat_0_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
0
∈
ordsucc
x0
Param
ordinal
ordinal
:
ι
→
ο
Known
ordinal_trichotomy_or_impred
ordinal_trichotomy_or_impred
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
∀ x2 : ο .
(
x0
∈
x1
⟶
x2
)
⟶
(
x0
=
x1
⟶
x2
)
⟶
(
x1
∈
x0
⟶
x2
)
⟶
x2
Known
nat_p_ordinal
nat_p_ordinal
:
∀ x0 .
nat_p
x0
⟶
ordinal
x0
Known
In_no2cycle
In_no2cycle
:
∀ x0 x1 .
x0
∈
x1
⟶
x1
∈
x0
⟶
False
Known
nat_p_trans
nat_p_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
nat_p
x1
Known
nat_ordsucc
nat_ordsucc
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
x0
)
Theorem
8ac0e..
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
ordsucc
x0
⟶
equip
x0
(
setminus
(
ordsucc
x0
)
(
Sing
x1
)
)
(proof)
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Known
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Known
setminusE1
setminusE1
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
x2
∈
x0
Known
setminusE2
setminusE2
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
nIn
x2
x1
Known
atleastp_tra
atleastp_tra
:
∀ x0 x1 x2 .
atleastp
x0
x1
⟶
atleastp
x1
x2
⟶
atleastp
x0
x2
Known
equip_atleastp
equip_atleastp
:
∀ x0 x1 .
equip
x0
x1
⟶
atleastp
x0
x1
Known
add_nat_p
add_nat_p
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
nat_p
(
add_nat
x0
x1
)
Theorem
9da24..
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
∀ x2 x3 .
atleastp
(
add_nat
x0
x1
)
(
binunion
x2
x3
)
⟶
or
(
atleastp
x0
x2
)
(
atleastp
x1
x3
)
(proof)
previous assets