Search for blocks/addresses/...
Proofgold Asset
asset id
b4204298993bb89c9fa0f9faacc1ad63c41860e691ef47cc8954d732008e87b9
asset hash
e4cb15c8e91476a7dde82eea6bf984f7a3df7cd96ee49bdee18be2ac85e80676
bday / block
14937
tx
84d03..
preasset
doc published by
Pr4zB..
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
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
Param
ordsucc
ordsucc
:
ι
→
ι
Known
In_0_3
In_0_3
:
0
∈
3
Known
In_1_3
In_1_3
:
1
∈
3
Known
In_2_3
In_2_3
:
2
∈
3
Known
neq_0_1
neq_0_1
:
0
=
1
⟶
∀ x0 : ο .
x0
Known
neq_0_2
neq_0_2
:
0
=
2
⟶
∀ x0 : ο .
x0
Known
neq_1_2
neq_1_2
:
1
=
2
⟶
∀ x0 : ο .
x0
Theorem
f03aa..
:
∀ x0 .
atleastp
3
x0
⟶
∀ x1 : ο .
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
(
x2
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
(
x2
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
x1
)
⟶
x1
(proof)
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Param
setminus
setminus
:
ι
→
ι
→
ι
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
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
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Known
PowerI
PowerI
:
∀ x0 x1 .
x1
⊆
x0
⟶
x1
∈
prim4
x0
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
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
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
If_i_0
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Known
setminusE2
setminusE2
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
nIn
x2
x1
Known
setminusI
setminusI
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
nIn
x2
x1
⟶
x2
∈
setminus
x0
x1
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Known
PowerE
PowerE
:
∀ x0 x1 .
x1
∈
prim4
x0
⟶
x1
⊆
x0
Theorem
dfb49..
:
∀ x0 x1 .
x1
⊆
prim4
(
ordsucc
x0
)
⟶
(
∀ x2 .
x2
∈
x1
⟶
∀ x3 .
x3
∈
x1
⟶
(
x2
=
x3
⟶
∀ x4 : ο .
x4
)
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
ordsucc
x0
)
(
x5
∈
x2
=
x5
∈
x3
)
⟶
x4
)
⟶
x4
)
⟶
atleastp
x1
(
prim4
x0
)
(proof)
Param
binunion
binunion
:
ι
→
ι
→
ι
Param
setsum
setsum
:
ι
→
ι
→
ι
Param
Inj0
Inj0
:
ι
→
ι
Param
Inj1
Inj1
:
ι
→
ι
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
Inj0_setsum
Inj0_setsum
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
Inj0
x2
∈
setsum
x0
x1
Known
Inj1_setsum
Inj1_setsum
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
Inj1
x2
∈
setsum
x0
x1
Known
Inj0_inj
Inj0_inj
:
∀ x0 x1 .
Inj0
x0
=
Inj0
x1
⟶
x0
=
x1
Known
Inj0_Inj1_neq
Inj0_Inj1_neq
:
∀ x0 x1 .
Inj0
x0
=
Inj1
x1
⟶
∀ x2 : ο .
x2
Known
Inj1_inj
Inj1_inj
:
∀ x0 x1 .
Inj1
x0
=
Inj1
x1
⟶
x0
=
x1
Theorem
385ef..
:
∀ x0 x1 x2 x3 .
atleastp
x0
x2
⟶
atleastp
x1
x3
⟶
(
∀ x4 .
x4
∈
x0
⟶
nIn
x4
x1
)
⟶
atleastp
(
binunion
x0
x1
)
(
setsum
x2
x3
)
(proof)
Param
nat_p
nat_p
:
ι
→
ο
Known
PigeonHole_nat
PigeonHole_nat
:
∀ x0 .
nat_p
x0
⟶
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
ordsucc
x0
⟶
x1
x2
∈
x0
)
⟶
not
(
∀ x2 .
x2
∈
ordsucc
x0
⟶
∀ x3 .
x3
∈
ordsucc
x0
⟶
x1
x2
=
x1
x3
⟶
x2
=
x3
)
Theorem
4fb58..
Pigeonhole_not_atleastp_ordsucc
:
∀ x0 .
nat_p
x0
⟶
not
(
atleastp
(
ordsucc
x0
)
x0
)
(proof)
Param
bij
bij
:
ι
→
ι
→
(
ι
→
ι
) →
ο
Definition
equip
equip
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
bij
x0
x1
x3
⟶
x2
)
⟶
x2
Param
ap
ap
:
ι
→
ι
→
ι
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Param
Sing
Sing
:
ι
→
ι
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
cases_4
cases_4
:
∀ x0 .
x0
∈
4
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
2
⟶
x1
3
⟶
x1
x0
Known
tuple_4_0_eq
tuple_4_0_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
0
=
x0
Known
Empty_In_Power
Empty_In_Power
:
∀ x0 .
0
∈
prim4
x0
Known
tuple_4_1_eq
tuple_4_1_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
1
=
x1
Known
Subq_1_2
Subq_1_2
:
1
⊆
2
Known
tuple_4_2_eq
tuple_4_2_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
2
=
x2
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Known
In_1_2
In_1_2
:
1
∈
2
Known
tuple_4_3_eq
tuple_4_3_eq
:
∀ x0 x1 x2 x3 .
ap
(
lam
4
(
λ x5 .
If_i
(
x5
=
0
)
x0
(
If_i
(
x5
=
1
)
x1
(
If_i
(
x5
=
2
)
x2
x3
)
)
)
)
3
=
x3
Known
Self_In_Power
Self_In_Power
:
∀ x0 .
x0
∈
prim4
x0
Known
not_Empty_eq_Sing
:
∀ x0 .
0
=
Sing
x0
⟶
∀ x1 : ο .
x1
Known
neq_1_0
neq_1_0
:
1
=
0
⟶
∀ x0 : ο .
x0
Known
nIn_not_eq_Sing
:
∀ x0 x1 .
nIn
x0
x1
⟶
x1
=
Sing
x0
⟶
∀ x2 : ο .
x2
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Known
In_0_2
In_0_2
:
0
∈
2
Known
neq_2_0
neq_2_0
:
2
=
0
⟶
∀ x0 : ο .
x0
Known
neq_2_1
neq_2_1
:
2
=
1
⟶
∀ x0 : ο .
x0
Known
In_Power_2_cases_impred
:
∀ x0 .
x0
∈
prim4
2
⟶
∀ x1 : ο .
(
x0
=
0
⟶
x1
)
⟶
(
x0
=
1
⟶
x1
)
⟶
(
x0
=
Sing
1
⟶
x1
)
⟶
(
x0
=
2
⟶
x1
)
⟶
x1
Known
In_0_4
In_0_4
:
0
∈
4
Known
In_1_4
In_1_4
:
1
∈
4
Known
In_2_4
In_2_4
:
2
∈
4
Known
In_3_4
In_3_4
:
3
∈
4
Theorem
26d05..
:
equip
4
(
prim4
2
)
(proof)
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
Known
Inj1I2
Inj1I2
:
∀ x0 x1 .
x1
∈
x0
⟶
Inj1
x1
∈
Inj1
x0
Known
Inj1I1
Inj1I1
:
∀ x0 .
0
∈
Inj1
x0
Known
Inj1NE1
Inj1NE1
:
∀ x0 .
Inj1
x0
=
0
⟶
∀ x1 : ο .
x1
Known
Inj1E
Inj1E
:
∀ x0 x1 .
x1
∈
Inj1
x0
⟶
or
(
x1
=
0
)
(
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
x0
)
(
x1
=
Inj1
x3
)
⟶
x2
)
⟶
x2
)
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Theorem
4b32b..
:
∀ x0 x1 .
equip
x0
x1
⟶
equip
(
ordsucc
x0
)
(
Inj1
x1
)
(proof)
Known
Inj1_setsum_1L
Inj1_setsum_1L
:
∀ x0 .
setsum
1
x0
=
Inj1
x0
Theorem
bb318..
:
equip
5
(
setsum
1
(
prim4
2
)
)
(proof)
Known
nat_5
nat_5
:
nat_p
5
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
equip_sym
equip_sym
:
∀ x0 x1 .
equip
x0
x1
⟶
equip
x1
x0
Theorem
89205..
:
∀ x0 x1 .
(
∀ x2 .
x2
∈
x0
⟶
nIn
x2
x1
)
⟶
atleastp
6
(
binunion
x0
x1
)
⟶
atleastp
x0
1
⟶
atleastp
x1
(
prim4
2
)
⟶
False
(proof)
Known
cases_3
cases_3
:
∀ x0 .
x0
∈
3
⟶
∀ x1 :
ι → ο
.
x1
0
⟶
x1
1
⟶
x1
2
⟶
x1
x0
Theorem
5de9e..
:
∀ x0 .
x0
⊆
3
⟶
∀ x1 .
x1
⊆
3
⟶
0
∈
x0
=
0
∈
x1
⟶
1
∈
x0
=
1
∈
x1
⟶
2
∈
x0
=
2
∈
x1
⟶
x0
=
x1
(proof)