Search for blocks/addresses/...
Proofgold Asset
asset id
dbe54c52fe4ffc587c1d49345c6e9278a44292845fd14dc2a8ef012ac2dda915
asset hash
1509e420e3ed94f0cbbb4084d5dc2ba604f21e20f334ed1bff39205dfb2a1351
bday / block
4905
tx
70a36..
preasset
doc published by
Pr6Pc..
Param
ap
ap
:
ι
→
ι
→
ι
Param
lam
Sigma
:
ι
→
(
ι
→
ι
) →
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Known
beta
beta
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
ap
(
lam
x0
x1
)
x2
=
x1
x2
Known
In_0_5
In_0_5
:
0
∈
5
Known
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Theorem
tuple_5_0_eq
tuple_5_0_eq
:
∀ x0 x1 x2 x3 x4 .
ap
(
lam
5
(
λ x6 .
If_i
(
x6
=
0
)
x0
(
If_i
(
x6
=
1
)
x1
(
If_i
(
x6
=
2
)
x2
(
If_i
(
x6
=
3
)
x3
x4
)
)
)
)
)
0
=
x0
(proof)
Known
In_1_5
In_1_5
:
1
∈
5
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
tuple_5_1_eq
tuple_5_1_eq
:
∀ x0 x1 x2 x3 x4 .
ap
(
lam
5
(
λ x6 .
If_i
(
x6
=
0
)
x0
(
If_i
(
x6
=
1
)
x1
(
If_i
(
x6
=
2
)
x2
(
If_i
(
x6
=
3
)
x3
x4
)
)
)
)
)
1
=
x1
(proof)
Known
In_2_5
In_2_5
:
2
∈
5
Known
neq_2_0
neq_2_0
:
2
=
0
⟶
∀ x0 : ο .
x0
Known
neq_2_1
neq_2_1
:
2
=
1
⟶
∀ x0 : ο .
x0
Theorem
tuple_5_2_eq
tuple_5_2_eq
:
∀ x0 x1 x2 x3 x4 .
ap
(
lam
5
(
λ x6 .
If_i
(
x6
=
0
)
x0
(
If_i
(
x6
=
1
)
x1
(
If_i
(
x6
=
2
)
x2
(
If_i
(
x6
=
3
)
x3
x4
)
)
)
)
)
2
=
x2
(proof)
Known
In_3_5
In_3_5
:
3
∈
5
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
tuple_5_3_eq
tuple_5_3_eq
:
∀ x0 x1 x2 x3 x4 .
ap
(
lam
5
(
λ x6 .
If_i
(
x6
=
0
)
x0
(
If_i
(
x6
=
1
)
x1
(
If_i
(
x6
=
2
)
x2
(
If_i
(
x6
=
3
)
x3
x4
)
)
)
)
)
3
=
x3
(proof)
Known
In_4_5
In_4_5
:
4
∈
5
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
tuple_5_4_eq
tuple_5_4_eq
:
∀ x0 x1 x2 x3 x4 .
ap
(
lam
5
(
λ x6 .
If_i
(
x6
=
0
)
x0
(
If_i
(
x6
=
1
)
x1
(
If_i
(
x6
=
2
)
x2
(
If_i
(
x6
=
3
)
x3
x4
)
)
)
)
)
4
=
x4
(proof)
Known
In_0_6
In_0_6
:
0
∈
6
Theorem
tuple_6_0_eq
tuple_6_0_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
0
=
x0
(proof)
Known
In_1_6
In_1_6
:
1
∈
6
Theorem
tuple_6_1_eq
tuple_6_1_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
1
=
x1
(proof)
Known
In_2_6
In_2_6
:
2
∈
6
Theorem
tuple_6_2_eq
tuple_6_2_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
2
=
x2
(proof)
Known
In_3_6
In_3_6
:
3
∈
6
Theorem
tuple_6_3_eq
tuple_6_3_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
3
=
x3
(proof)
Known
In_4_6
In_4_6
:
4
∈
6
Theorem
tuple_6_4_eq
tuple_6_4_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
4
=
x4
(proof)
Known
In_5_6
In_5_6
:
5
∈
6
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
tuple_6_5_eq
tuple_6_5_eq
:
∀ x0 x1 x2 x3 x4 x5 .
ap
(
lam
6
(
λ x7 .
If_i
(
x7
=
0
)
x0
(
If_i
(
x7
=
1
)
x1
(
If_i
(
x7
=
2
)
x2
(
If_i
(
x7
=
3
)
x3
(
If_i
(
x7
=
4
)
x4
x5
)
)
)
)
)
)
5
=
x5
(proof)
Known
In_0_7
In_0_7
:
0
∈
7
Theorem
tuple_7_0_eq
tuple_7_0_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 .
ap
(
lam
7
(
λ x8 .
If_i
(
x8
=
0
)
x0
(
If_i
(
x8
=
1
)
x1
(
If_i
(
x8
=
2
)
x2
(
If_i
(
x8
=
3
)
x3
(
If_i
(
x8
=
4
)
x4
(
If_i
(
x8
=
5
)
x5
x6
)
)
)
)
)
)
)
0
=
x0
(proof)
Known
In_1_7
In_1_7
:
1
∈
7
Theorem
tuple_7_1_eq
tuple_7_1_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 .
ap
(
lam
7
(
λ x8 .
If_i
(
x8
=
0
)
x0
(
If_i
(
x8
=
1
)
x1
(
If_i
(
x8
=
2
)
x2
(
If_i
(
x8
=
3
)
x3
(
If_i
(
x8
=
4
)
x4
(
If_i
(
x8
=
5
)
x5
x6
)
)
)
)
)
)
)
1
=
x1
(proof)
Known
In_2_7
In_2_7
:
2
∈
7
Theorem
tuple_7_2_eq
tuple_7_2_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 .
ap
(
lam
7
(
λ x8 .
If_i
(
x8
=
0
)
x0
(
If_i
(
x8
=
1
)
x1
(
If_i
(
x8
=
2
)
x2
(
If_i
(
x8
=
3
)
x3
(
If_i
(
x8
=
4
)
x4
(
If_i
(
x8
=
5
)
x5
x6
)
)
)
)
)
)
)
2
=
x2
(proof)
Known
In_3_7
In_3_7
:
3
∈
7
Theorem
tuple_7_3_eq
tuple_7_3_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 .
ap
(
lam
7
(
λ x8 .
If_i
(
x8
=
0
)
x0
(
If_i
(
x8
=
1
)
x1
(
If_i
(
x8
=
2
)
x2
(
If_i
(
x8
=
3
)
x3
(
If_i
(
x8
=
4
)
x4
(
If_i
(
x8
=
5
)
x5
x6
)
)
)
)
)
)
)
3
=
x3
(proof)
Known
In_4_7
In_4_7
:
4
∈
7
Theorem
tuple_7_4_eq
tuple_7_4_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 .
ap
(
lam
7
(
λ x8 .
If_i
(
x8
=
0
)
x0
(
If_i
(
x8
=
1
)
x1
(
If_i
(
x8
=
2
)
x2
(
If_i
(
x8
=
3
)
x3
(
If_i
(
x8
=
4
)
x4
(
If_i
(
x8
=
5
)
x5
x6
)
)
)
)
)
)
)
4
=
x4
(proof)
Known
In_5_7
In_5_7
:
5
∈
7
Theorem
tuple_7_5_eq
tuple_7_5_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 .
ap
(
lam
7
(
λ x8 .
If_i
(
x8
=
0
)
x0
(
If_i
(
x8
=
1
)
x1
(
If_i
(
x8
=
2
)
x2
(
If_i
(
x8
=
3
)
x3
(
If_i
(
x8
=
4
)
x4
(
If_i
(
x8
=
5
)
x5
x6
)
)
)
)
)
)
)
5
=
x5
(proof)
Known
In_6_7
In_6_7
:
6
∈
7
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
tuple_7_6_eq
tuple_7_6_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 .
ap
(
lam
7
(
λ x8 .
If_i
(
x8
=
0
)
x0
(
If_i
(
x8
=
1
)
x1
(
If_i
(
x8
=
2
)
x2
(
If_i
(
x8
=
3
)
x3
(
If_i
(
x8
=
4
)
x4
(
If_i
(
x8
=
5
)
x5
x6
)
)
)
)
)
)
)
6
=
x6
(proof)