Search for blocks/addresses/...
Proofgold Asset
asset id
de62943283e4269ed8a34b7ea63364959bfe6692e0d579586c4b08a33ed2b43b
asset hash
0c47cf8d039326013dcf3077db27d2faca5202efaca30aaf6ef5b55b3efb9372
bday / block
19015
tx
2fd35..
preasset
doc published by
Pr4zB..
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
u1
:=
1
Definition
u2
:=
ordsucc
u1
Definition
u3
:=
ordsucc
u2
Definition
u4
:=
ordsucc
u3
Definition
u5
:=
ordsucc
u4
Definition
u6
:=
ordsucc
u5
Definition
u7
:=
ordsucc
u6
Definition
u8
:=
ordsucc
u7
Definition
u9
:=
ordsucc
u8
Definition
u10
:=
ordsucc
u9
Definition
u11
:=
ordsucc
u10
Definition
u12
:=
ordsucc
u11
Definition
u13
:=
ordsucc
u12
Definition
u14
:=
ordsucc
u13
Definition
u15
:=
ordsucc
u14
Definition
u16
:=
ordsucc
u15
Definition
u17
:=
ordsucc
u16
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Known
fdaf0..
:
9
∈
16
Theorem
fd1a6..
:
u9
∈
u17
(proof)
Known
662c8..
:
10
∈
16
Theorem
e886d..
:
u10
∈
u17
(proof)
Known
2039c..
:
11
∈
16
Theorem
e57ea..
:
u11
∈
u17
(proof)
Known
be924..
:
12
∈
16
Theorem
a1a10..
:
u12
∈
u17
(proof)
Param
ap
ap
:
ι
→
ι
→
ι
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Known
neq_9_0
neq_9_0
:
u9
=
0
⟶
∀ x0 : ο .
x0
Known
neq_9_1
neq_9_1
:
u9
=
u1
⟶
∀ x0 : ο .
x0
Known
neq_9_2
neq_9_2
:
u9
=
u2
⟶
∀ x0 : ο .
x0
Known
neq_9_3
neq_9_3
:
u9
=
u3
⟶
∀ x0 : ο .
x0
Known
neq_9_4
neq_9_4
:
u9
=
u4
⟶
∀ x0 : ο .
x0
Known
neq_9_5
neq_9_5
:
u9
=
u5
⟶
∀ x0 : ο .
x0
Known
neq_9_6
neq_9_6
:
u9
=
u6
⟶
∀ x0 : ο .
x0
Known
neq_9_7
neq_9_7
:
u9
=
u7
⟶
∀ x0 : ο .
x0
Known
neq_9_8
neq_9_8
:
u9
=
u8
⟶
∀ x0 : ο .
x0
Theorem
511d7..
:
(
∀ x0 x1 .
∀ x2 :
ι →
ι → ι
.
∀ x3 .
x3
∈
x1
⟶
ap
(
lam
x1
(
λ x5 .
If_i
(
x5
=
x3
)
x0
(
x2
(
ordsucc
x3
)
x5
)
)
)
x3
=
x0
)
⟶
(
∀ x0 x1 .
∀ x2 :
ι →
ι → ι
.
∀ x3 x4 .
(
x4
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
ap
(
lam
x1
(
λ x6 .
If_i
(
x6
=
x3
)
x0
(
x2
(
ordsucc
x3
)
x6
)
)
)
x4
=
ap
(
lam
x1
(
x2
(
ordsucc
x3
)
)
)
x4
)
⟶
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
ap
(
lam
17
(
λ x18 .
If_i
(
x18
=
0
)
x0
(
If_i
(
x18
=
1
)
x1
(
If_i
(
x18
=
2
)
x2
(
If_i
(
x18
=
3
)
x3
(
If_i
(
x18
=
4
)
x4
(
If_i
(
x18
=
5
)
x5
(
If_i
(
x18
=
6
)
x6
(
If_i
(
x18
=
7
)
x7
(
If_i
(
x18
=
8
)
x8
(
If_i
(
x18
=
9
)
x9
(
If_i
(
x18
=
10
)
x10
(
If_i
(
x18
=
11
)
x11
(
If_i
(
x18
=
12
)
x12
(
If_i
(
x18
=
13
)
x13
(
If_i
(
x18
=
14
)
x14
(
If_i
(
x18
=
15
)
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
u9
=
x9
(proof)
Known
0e10e..
:
u10
=
0
⟶
∀ x0 : ο .
x0
Known
d183f..
:
u10
=
u1
⟶
∀ x0 : ο .
x0
Known
e02d9..
:
u10
=
u2
⟶
∀ x0 : ο .
x0
Known
68152..
:
u10
=
u3
⟶
∀ x0 : ο .
x0
Known
33d16..
:
u10
=
u4
⟶
∀ x0 : ο .
x0
Known
a7d50..
:
u10
=
u5
⟶
∀ x0 : ο .
x0
Known
d0401..
:
u10
=
u6
⟶
∀ x0 : ο .
x0
Known
7d7a8..
:
u10
=
u7
⟶
∀ x0 : ο .
x0
Known
96175..
:
u10
=
u8
⟶
∀ x0 : ο .
x0
Known
4fc31..
:
u10
=
u9
⟶
∀ x0 : ο .
x0
Theorem
929f6..
:
(
∀ x0 x1 .
∀ x2 :
ι →
ι → ι
.
∀ x3 .
x3
∈
x1
⟶
ap
(
lam
x1
(
λ x5 .
If_i
(
x5
=
x3
)
x0
(
x2
(
ordsucc
x3
)
x5
)
)
)
x3
=
x0
)
⟶
(
∀ x0 x1 .
∀ x2 :
ι →
ι → ι
.
∀ x3 x4 .
(
x4
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
ap
(
lam
x1
(
λ x6 .
If_i
(
x6
=
x3
)
x0
(
x2
(
ordsucc
x3
)
x6
)
)
)
x4
=
ap
(
lam
x1
(
x2
(
ordsucc
x3
)
)
)
x4
)
⟶
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
ap
(
lam
17
(
λ x18 .
If_i
(
x18
=
0
)
x0
(
If_i
(
x18
=
1
)
x1
(
If_i
(
x18
=
2
)
x2
(
If_i
(
x18
=
3
)
x3
(
If_i
(
x18
=
4
)
x4
(
If_i
(
x18
=
5
)
x5
(
If_i
(
x18
=
6
)
x6
(
If_i
(
x18
=
7
)
x7
(
If_i
(
x18
=
8
)
x8
(
If_i
(
x18
=
9
)
x9
(
If_i
(
x18
=
10
)
x10
(
If_i
(
x18
=
11
)
x11
(
If_i
(
x18
=
12
)
x12
(
If_i
(
x18
=
13
)
x13
(
If_i
(
x18
=
14
)
x14
(
If_i
(
x18
=
15
)
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
u10
=
x10
(proof)
Known
19f75..
:
u11
=
0
⟶
∀ x0 : ο .
x0
Known
618f7..
:
u11
=
u1
⟶
∀ x0 : ο .
x0
Known
2c42c..
:
u11
=
u2
⟶
∀ x0 : ο .
x0
Known
b06e1..
:
u11
=
u3
⟶
∀ x0 : ο .
x0
Known
6a6f1..
:
u11
=
u4
⟶
∀ x0 : ο .
x0
Known
1b659..
:
u11
=
u5
⟶
∀ x0 : ο .
x0
Known
949f2..
:
u11
=
u6
⟶
∀ x0 : ο .
x0
Known
4abfa..
:
u11
=
u7
⟶
∀ x0 : ο .
x0
Known
b3a20..
:
u11
=
u8
⟶
∀ x0 : ο .
x0
Known
4f03f..
:
u11
=
u9
⟶
∀ x0 : ο .
x0
Known
ebfb7..
:
u11
=
u10
⟶
∀ x0 : ο .
x0
Theorem
02699..
:
(
∀ x0 x1 .
∀ x2 :
ι →
ι → ι
.
∀ x3 .
x3
∈
x1
⟶
ap
(
lam
x1
(
λ x5 .
If_i
(
x5
=
x3
)
x0
(
x2
(
ordsucc
x3
)
x5
)
)
)
x3
=
x0
)
⟶
(
∀ x0 x1 .
∀ x2 :
ι →
ι → ι
.
∀ x3 x4 .
(
x4
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
ap
(
lam
x1
(
λ x6 .
If_i
(
x6
=
x3
)
x0
(
x2
(
ordsucc
x3
)
x6
)
)
)
x4
=
ap
(
lam
x1
(
x2
(
ordsucc
x3
)
)
)
x4
)
⟶
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
ap
(
lam
17
(
λ x18 .
If_i
(
x18
=
0
)
x0
(
If_i
(
x18
=
1
)
x1
(
If_i
(
x18
=
2
)
x2
(
If_i
(
x18
=
3
)
x3
(
If_i
(
x18
=
4
)
x4
(
If_i
(
x18
=
5
)
x5
(
If_i
(
x18
=
6
)
x6
(
If_i
(
x18
=
7
)
x7
(
If_i
(
x18
=
8
)
x8
(
If_i
(
x18
=
9
)
x9
(
If_i
(
x18
=
10
)
x10
(
If_i
(
x18
=
11
)
x11
(
If_i
(
x18
=
12
)
x12
(
If_i
(
x18
=
13
)
x13
(
If_i
(
x18
=
14
)
x14
(
If_i
(
x18
=
15
)
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
u11
=
x11
(proof)
Known
efdfc..
:
u12
=
0
⟶
∀ x0 : ο .
x0
Known
ce0cd..
:
u12
=
u1
⟶
∀ x0 : ο .
x0
Known
8158b..
:
u12
=
u2
⟶
∀ x0 : ο .
x0
Known
e015c..
:
u12
=
u3
⟶
∀ x0 : ο .
x0
Known
7aa79..
:
u12
=
u4
⟶
∀ x0 : ο .
x0
Known
07eba..
:
u12
=
u5
⟶
∀ x0 : ο .
x0
Known
0bd83..
:
u12
=
u6
⟶
∀ x0 : ο .
x0
Known
6a15f..
:
u12
=
u7
⟶
∀ x0 : ο .
x0
Known
a6a6c..
:
u12
=
u8
⟶
∀ x0 : ο .
x0
Known
22885..
:
u12
=
u9
⟶
∀ x0 : ο .
x0
Known
6c583..
:
u12
=
u10
⟶
∀ x0 : ο .
x0
Known
ab306..
:
u12
=
u11
⟶
∀ x0 : ο .
x0
Theorem
6f2dd..
:
(
∀ x0 x1 .
∀ x2 :
ι →
ι → ι
.
∀ x3 .
x3
∈
x1
⟶
ap
(
lam
x1
(
λ x5 .
If_i
(
x5
=
x3
)
x0
(
x2
(
ordsucc
x3
)
x5
)
)
)
x3
=
x0
)
⟶
(
∀ x0 x1 .
∀ x2 :
ι →
ι → ι
.
∀ x3 x4 .
(
x4
=
x3
⟶
∀ x5 : ο .
x5
)
⟶
ap
(
lam
x1
(
λ x6 .
If_i
(
x6
=
x3
)
x0
(
x2
(
ordsucc
x3
)
x6
)
)
)
x4
=
ap
(
lam
x1
(
x2
(
ordsucc
x3
)
)
)
x4
)
⟶
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
ap
(
lam
17
(
λ x18 .
If_i
(
x18
=
0
)
x0
(
If_i
(
x18
=
1
)
x1
(
If_i
(
x18
=
2
)
x2
(
If_i
(
x18
=
3
)
x3
(
If_i
(
x18
=
4
)
x4
(
If_i
(
x18
=
5
)
x5
(
If_i
(
x18
=
6
)
x6
(
If_i
(
x18
=
7
)
x7
(
If_i
(
x18
=
8
)
x8
(
If_i
(
x18
=
9
)
x9
(
If_i
(
x18
=
10
)
x10
(
If_i
(
x18
=
11
)
x11
(
If_i
(
x18
=
12
)
x12
(
If_i
(
x18
=
13
)
x13
(
If_i
(
x18
=
14
)
x14
(
If_i
(
x18
=
15
)
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
u12
=
x12
(proof)