Search for blocks/addresses/...
Proofgold Asset
asset id
20e76153a61d5f58ff2d058e54b40f50e1299950e0b837fd100081713be63132
asset hash
4b057e3f422ac5538eb25da06c619e2dd442dac1bac219bb1cb8b07f9fd844f9
bday / block
9342
tx
29d26..
preasset
doc published by
PrGxv..
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Known
In_0_9
In_0_9
:
0
∈
9
Theorem
d4e95..
:
0
∈
10
(proof)
Known
In_1_9
In_1_9
:
1
∈
9
Theorem
b7a5e..
:
1
∈
10
(proof)
Known
In_2_9
In_2_9
:
2
∈
9
Theorem
3c603..
:
2
∈
10
(proof)
Known
In_3_9
In_3_9
:
3
∈
9
Theorem
01826..
:
3
∈
10
(proof)
Known
In_4_9
In_4_9
:
4
∈
9
Theorem
35ffd..
:
4
∈
10
(proof)
Known
In_5_9
In_5_9
:
5
∈
9
Theorem
a1b2a..
:
5
∈
10
(proof)
Known
In_6_9
In_6_9
:
6
∈
9
Theorem
1beb5..
:
6
∈
10
(proof)
Known
In_7_9
In_7_9
:
7
∈
9
Theorem
16542..
:
7
∈
10
(proof)
Known
In_8_9
In_8_9
:
8
∈
9
Theorem
56b84..
:
8
∈
10
(proof)
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Theorem
fa1e6..
:
9
∈
10
(proof)
Param
ap
ap
:
ι
→
ι
→
ι
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Known
beta
beta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
ap
(
lam
x0
x1
)
x2
=
x1
x2
Known
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Theorem
3105e..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
lam
10
(
λ x11 .
If_i
(
x11
=
0
)
x0
(
If_i
(
x11
=
1
)
x1
(
If_i
(
x11
=
2
)
x2
(
If_i
(
x11
=
3
)
x3
(
If_i
(
x11
=
4
)
x4
(
If_i
(
x11
=
5
)
x5
(
If_i
(
x11
=
6
)
x6
(
If_i
(
x11
=
7
)
x7
(
If_i
(
x11
=
8
)
x8
x9
)
)
)
)
)
)
)
)
)
)
0
=
x0
(proof)
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
If_i_0
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Known
neq_1_0
neq_1_0
:
1
=
0
⟶
∀ x0 : ο .
x0
Theorem
f0027..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
lam
10
(
λ x11 .
If_i
(
x11
=
0
)
x0
(
If_i
(
x11
=
1
)
x1
(
If_i
(
x11
=
2
)
x2
(
If_i
(
x11
=
3
)
x3
(
If_i
(
x11
=
4
)
x4
(
If_i
(
x11
=
5
)
x5
(
If_i
(
x11
=
6
)
x6
(
If_i
(
x11
=
7
)
x7
(
If_i
(
x11
=
8
)
x8
x9
)
)
)
)
)
)
)
)
)
)
1
=
x1
(proof)
Known
neq_2_0
neq_2_0
:
2
=
0
⟶
∀ x0 : ο .
x0
Known
neq_2_1
neq_2_1
:
2
=
1
⟶
∀ x0 : ο .
x0
Theorem
71234..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
lam
10
(
λ x11 .
If_i
(
x11
=
0
)
x0
(
If_i
(
x11
=
1
)
x1
(
If_i
(
x11
=
2
)
x2
(
If_i
(
x11
=
3
)
x3
(
If_i
(
x11
=
4
)
x4
(
If_i
(
x11
=
5
)
x5
(
If_i
(
x11
=
6
)
x6
(
If_i
(
x11
=
7
)
x7
(
If_i
(
x11
=
8
)
x8
x9
)
)
)
)
)
)
)
)
)
)
2
=
x2
(proof)
Known
neq_3_0
neq_3_0
:
3
=
0
⟶
∀ x0 : ο .
x0
Known
neq_3_1
neq_3_1
:
3
=
1
⟶
∀ x0 : ο .
x0
Known
neq_3_2
neq_3_2
:
3
=
2
⟶
∀ x0 : ο .
x0
Theorem
cb998..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
lam
10
(
λ x11 .
If_i
(
x11
=
0
)
x0
(
If_i
(
x11
=
1
)
x1
(
If_i
(
x11
=
2
)
x2
(
If_i
(
x11
=
3
)
x3
(
If_i
(
x11
=
4
)
x4
(
If_i
(
x11
=
5
)
x5
(
If_i
(
x11
=
6
)
x6
(
If_i
(
x11
=
7
)
x7
(
If_i
(
x11
=
8
)
x8
x9
)
)
)
)
)
)
)
)
)
)
3
=
x3
(proof)
Known
neq_4_0
neq_4_0
:
4
=
0
⟶
∀ x0 : ο .
x0
Known
neq_4_1
neq_4_1
:
4
=
1
⟶
∀ x0 : ο .
x0
Known
neq_4_2
neq_4_2
:
4
=
2
⟶
∀ x0 : ο .
x0
Known
neq_4_3
neq_4_3
:
4
=
3
⟶
∀ x0 : ο .
x0
Theorem
bd5cb..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
lam
10
(
λ x11 .
If_i
(
x11
=
0
)
x0
(
If_i
(
x11
=
1
)
x1
(
If_i
(
x11
=
2
)
x2
(
If_i
(
x11
=
3
)
x3
(
If_i
(
x11
=
4
)
x4
(
If_i
(
x11
=
5
)
x5
(
If_i
(
x11
=
6
)
x6
(
If_i
(
x11
=
7
)
x7
(
If_i
(
x11
=
8
)
x8
x9
)
)
)
)
)
)
)
)
)
)
4
=
x4
(proof)
Known
neq_5_0
neq_5_0
:
5
=
0
⟶
∀ x0 : ο .
x0
Known
neq_5_1
neq_5_1
:
5
=
1
⟶
∀ x0 : ο .
x0
Known
neq_5_2
neq_5_2
:
5
=
2
⟶
∀ x0 : ο .
x0
Known
neq_5_3
neq_5_3
:
5
=
3
⟶
∀ x0 : ο .
x0
Known
neq_5_4
neq_5_4
:
5
=
4
⟶
∀ x0 : ο .
x0
Theorem
11217..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
lam
10
(
λ x11 .
If_i
(
x11
=
0
)
x0
(
If_i
(
x11
=
1
)
x1
(
If_i
(
x11
=
2
)
x2
(
If_i
(
x11
=
3
)
x3
(
If_i
(
x11
=
4
)
x4
(
If_i
(
x11
=
5
)
x5
(
If_i
(
x11
=
6
)
x6
(
If_i
(
x11
=
7
)
x7
(
If_i
(
x11
=
8
)
x8
x9
)
)
)
)
)
)
)
)
)
)
5
=
x5
(proof)
Known
neq_6_0
neq_6_0
:
6
=
0
⟶
∀ x0 : ο .
x0
Known
neq_6_1
neq_6_1
:
6
=
1
⟶
∀ x0 : ο .
x0
Known
neq_6_2
neq_6_2
:
6
=
2
⟶
∀ x0 : ο .
x0
Known
neq_6_3
neq_6_3
:
6
=
3
⟶
∀ x0 : ο .
x0
Known
neq_6_4
neq_6_4
:
6
=
4
⟶
∀ x0 : ο .
x0
Known
neq_6_5
neq_6_5
:
6
=
5
⟶
∀ x0 : ο .
x0
Theorem
bc2b8..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
lam
10
(
λ x11 .
If_i
(
x11
=
0
)
x0
(
If_i
(
x11
=
1
)
x1
(
If_i
(
x11
=
2
)
x2
(
If_i
(
x11
=
3
)
x3
(
If_i
(
x11
=
4
)
x4
(
If_i
(
x11
=
5
)
x5
(
If_i
(
x11
=
6
)
x6
(
If_i
(
x11
=
7
)
x7
(
If_i
(
x11
=
8
)
x8
x9
)
)
)
)
)
)
)
)
)
)
6
=
x6
(proof)
Known
neq_7_0
neq_7_0
:
7
=
0
⟶
∀ x0 : ο .
x0
Known
neq_7_1
neq_7_1
:
7
=
1
⟶
∀ x0 : ο .
x0
Known
neq_7_2
neq_7_2
:
7
=
2
⟶
∀ x0 : ο .
x0
Known
neq_7_3
neq_7_3
:
7
=
3
⟶
∀ x0 : ο .
x0
Known
neq_7_4
neq_7_4
:
7
=
4
⟶
∀ x0 : ο .
x0
Known
neq_7_5
neq_7_5
:
7
=
5
⟶
∀ x0 : ο .
x0
Known
neq_7_6
neq_7_6
:
7
=
6
⟶
∀ x0 : ο .
x0
Theorem
c16dd..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
lam
10
(
λ x11 .
If_i
(
x11
=
0
)
x0
(
If_i
(
x11
=
1
)
x1
(
If_i
(
x11
=
2
)
x2
(
If_i
(
x11
=
3
)
x3
(
If_i
(
x11
=
4
)
x4
(
If_i
(
x11
=
5
)
x5
(
If_i
(
x11
=
6
)
x6
(
If_i
(
x11
=
7
)
x7
(
If_i
(
x11
=
8
)
x8
x9
)
)
)
)
)
)
)
)
)
)
7
=
x7
(proof)
Known
neq_8_0
neq_8_0
:
8
=
0
⟶
∀ x0 : ο .
x0
Known
neq_8_1
neq_8_1
:
8
=
1
⟶
∀ x0 : ο .
x0
Known
neq_8_2
neq_8_2
:
8
=
2
⟶
∀ x0 : ο .
x0
Known
neq_8_3
neq_8_3
:
8
=
3
⟶
∀ x0 : ο .
x0
Known
neq_8_4
neq_8_4
:
8
=
4
⟶
∀ x0 : ο .
x0
Known
neq_8_5
neq_8_5
:
8
=
5
⟶
∀ x0 : ο .
x0
Known
neq_8_6
neq_8_6
:
8
=
6
⟶
∀ x0 : ο .
x0
Known
neq_8_7
neq_8_7
:
8
=
7
⟶
∀ x0 : ο .
x0
Theorem
0f630..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
lam
10
(
λ x11 .
If_i
(
x11
=
0
)
x0
(
If_i
(
x11
=
1
)
x1
(
If_i
(
x11
=
2
)
x2
(
If_i
(
x11
=
3
)
x3
(
If_i
(
x11
=
4
)
x4
(
If_i
(
x11
=
5
)
x5
(
If_i
(
x11
=
6
)
x6
(
If_i
(
x11
=
7
)
x7
(
If_i
(
x11
=
8
)
x8
x9
)
)
)
)
)
)
)
)
)
)
8
=
x8
(proof)
Known
neq_9_0
neq_9_0
:
9
=
0
⟶
∀ x0 : ο .
x0
Known
neq_9_1
neq_9_1
:
9
=
1
⟶
∀ x0 : ο .
x0
Known
neq_9_2
neq_9_2
:
9
=
2
⟶
∀ x0 : ο .
x0
Known
neq_9_3
neq_9_3
:
9
=
3
⟶
∀ x0 : ο .
x0
Known
neq_9_4
neq_9_4
:
9
=
4
⟶
∀ x0 : ο .
x0
Known
neq_9_5
neq_9_5
:
9
=
5
⟶
∀ x0 : ο .
x0
Known
neq_9_6
neq_9_6
:
9
=
6
⟶
∀ x0 : ο .
x0
Known
neq_9_7
neq_9_7
:
9
=
7
⟶
∀ x0 : ο .
x0
Known
neq_9_8
neq_9_8
:
9
=
8
⟶
∀ x0 : ο .
x0
Theorem
06839..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
lam
10
(
λ x11 .
If_i
(
x11
=
0
)
x0
(
If_i
(
x11
=
1
)
x1
(
If_i
(
x11
=
2
)
x2
(
If_i
(
x11
=
3
)
x3
(
If_i
(
x11
=
4
)
x4
(
If_i
(
x11
=
5
)
x5
(
If_i
(
x11
=
6
)
x6
(
If_i
(
x11
=
7
)
x7
(
If_i
(
x11
=
8
)
x8
x9
)
)
)
)
)
)
)
)
)
)
9
=
x9
(proof)
Definition
4a740..
:=
λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
lam
10
(
λ x10 .
If_i
(
x10
=
0
)
x0
(
If_i
(
x10
=
1
)
x1
(
If_i
(
x10
=
2
)
x2
(
If_i
(
x10
=
3
)
x3
(
If_i
(
x10
=
4
)
x4
(
If_i
(
x10
=
5
)
x5
(
If_i
(
x10
=
6
)
x6
(
If_i
(
x10
=
7
)
x7
(
If_i
(
x10
=
8
)
x8
x9
)
)
)
)
)
)
)
)
)
Theorem
1d6af..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
4a740..
x0
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
0
=
x0
(proof)
Theorem
ada9b..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
4a740..
x0
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
1
=
x1
(proof)
Theorem
5b3bf..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
4a740..
x0
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
2
=
x2
(proof)
Theorem
7684e..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
4a740..
x0
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
3
=
x3
(proof)
Theorem
601d3..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
4a740..
x0
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
4
=
x4
(proof)
Theorem
f536c..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
4a740..
x0
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
5
=
x5
(proof)
Theorem
6a688..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
4a740..
x0
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
6
=
x6
(proof)
Theorem
83113..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
4a740..
x0
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
7
=
x7
(proof)
Theorem
1d841..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
4a740..
x0
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
8
=
x8
(proof)
Theorem
d7ed7..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 .
ap
(
4a740..
x0
x1
x2
x3
x4
x5
x6
x7
x8
x9
)
9
=
x9
(proof)