Search for blocks/addresses/...
Proofgold Asset
asset id
a2cff0294286399df2a3e0dcd6c1777b3b24fa6479d67ad7d144265fe6d51035
asset hash
5f7e0bbe6dd05278642bf0cc81272f0639dc3faf79c2559ad4b92b43d0f024a3
bday / block
4909
tx
3dbc4..
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_8
In_0_8
:
0
∈
8
Known
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Theorem
tuple_8_0_eq
tuple_8_0_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
ap
(
lam
8
(
λ x9 .
If_i
(
x9
=
0
)
x0
(
If_i
(
x9
=
1
)
x1
(
If_i
(
x9
=
2
)
x2
(
If_i
(
x9
=
3
)
x3
(
If_i
(
x9
=
4
)
x4
(
If_i
(
x9
=
5
)
x5
(
If_i
(
x9
=
6
)
x6
x7
)
)
)
)
)
)
)
)
0
=
x0
(proof)
Known
In_1_8
In_1_8
:
1
∈
8
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_8_1_eq
tuple_8_1_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
ap
(
lam
8
(
λ x9 .
If_i
(
x9
=
0
)
x0
(
If_i
(
x9
=
1
)
x1
(
If_i
(
x9
=
2
)
x2
(
If_i
(
x9
=
3
)
x3
(
If_i
(
x9
=
4
)
x4
(
If_i
(
x9
=
5
)
x5
(
If_i
(
x9
=
6
)
x6
x7
)
)
)
)
)
)
)
)
1
=
x1
(proof)
Known
In_2_8
In_2_8
:
2
∈
8
Known
neq_2_0
neq_2_0
:
2
=
0
⟶
∀ x0 : ο .
x0
Known
neq_2_1
neq_2_1
:
2
=
1
⟶
∀ x0 : ο .
x0
Theorem
tuple_8_2_eq
tuple_8_2_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
ap
(
lam
8
(
λ x9 .
If_i
(
x9
=
0
)
x0
(
If_i
(
x9
=
1
)
x1
(
If_i
(
x9
=
2
)
x2
(
If_i
(
x9
=
3
)
x3
(
If_i
(
x9
=
4
)
x4
(
If_i
(
x9
=
5
)
x5
(
If_i
(
x9
=
6
)
x6
x7
)
)
)
)
)
)
)
)
2
=
x2
(proof)
Known
In_3_8
In_3_8
:
3
∈
8
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_8_3_eq
tuple_8_3_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
ap
(
lam
8
(
λ x9 .
If_i
(
x9
=
0
)
x0
(
If_i
(
x9
=
1
)
x1
(
If_i
(
x9
=
2
)
x2
(
If_i
(
x9
=
3
)
x3
(
If_i
(
x9
=
4
)
x4
(
If_i
(
x9
=
5
)
x5
(
If_i
(
x9
=
6
)
x6
x7
)
)
)
)
)
)
)
)
3
=
x3
(proof)
Known
In_4_8
In_4_8
:
4
∈
8
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_8_4_eq
tuple_8_4_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
ap
(
lam
8
(
λ x9 .
If_i
(
x9
=
0
)
x0
(
If_i
(
x9
=
1
)
x1
(
If_i
(
x9
=
2
)
x2
(
If_i
(
x9
=
3
)
x3
(
If_i
(
x9
=
4
)
x4
(
If_i
(
x9
=
5
)
x5
(
If_i
(
x9
=
6
)
x6
x7
)
)
)
)
)
)
)
)
4
=
x4
(proof)
Known
In_5_8
In_5_8
:
5
∈
8
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_8_5_eq
tuple_8_5_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
ap
(
lam
8
(
λ x9 .
If_i
(
x9
=
0
)
x0
(
If_i
(
x9
=
1
)
x1
(
If_i
(
x9
=
2
)
x2
(
If_i
(
x9
=
3
)
x3
(
If_i
(
x9
=
4
)
x4
(
If_i
(
x9
=
5
)
x5
(
If_i
(
x9
=
6
)
x6
x7
)
)
)
)
)
)
)
)
5
=
x5
(proof)
Known
In_6_8
In_6_8
:
6
∈
8
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_8_6_eq
tuple_8_6_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
ap
(
lam
8
(
λ x9 .
If_i
(
x9
=
0
)
x0
(
If_i
(
x9
=
1
)
x1
(
If_i
(
x9
=
2
)
x2
(
If_i
(
x9
=
3
)
x3
(
If_i
(
x9
=
4
)
x4
(
If_i
(
x9
=
5
)
x5
(
If_i
(
x9
=
6
)
x6
x7
)
)
)
)
)
)
)
)
6
=
x6
(proof)
Known
In_7_8
In_7_8
:
7
∈
8
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
tuple_8_7_eq
tuple_8_7_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
ap
(
lam
8
(
λ x9 .
If_i
(
x9
=
0
)
x0
(
If_i
(
x9
=
1
)
x1
(
If_i
(
x9
=
2
)
x2
(
If_i
(
x9
=
3
)
x3
(
If_i
(
x9
=
4
)
x4
(
If_i
(
x9
=
5
)
x5
(
If_i
(
x9
=
6
)
x6
x7
)
)
)
)
)
)
)
)
7
=
x7
(proof)
Known
In_0_9
In_0_9
:
0
∈
9
Theorem
tuple_9_0_eq
tuple_9_0_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
ap
(
lam
9
(
λ 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
x8
)
)
)
)
)
)
)
)
)
0
=
x0
(proof)
Known
In_1_9
In_1_9
:
1
∈
9
Theorem
tuple_9_1_eq
tuple_9_1_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
ap
(
lam
9
(
λ 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
x8
)
)
)
)
)
)
)
)
)
1
=
x1
(proof)
Known
In_2_9
In_2_9
:
2
∈
9
Theorem
tuple_9_2_eq
tuple_9_2_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
ap
(
lam
9
(
λ 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
x8
)
)
)
)
)
)
)
)
)
2
=
x2
(proof)
Known
In_3_9
In_3_9
:
3
∈
9
Theorem
tuple_9_3_eq
tuple_9_3_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
ap
(
lam
9
(
λ 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
x8
)
)
)
)
)
)
)
)
)
3
=
x3
(proof)
Known
In_4_9
In_4_9
:
4
∈
9
Theorem
tuple_9_4_eq
tuple_9_4_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
ap
(
lam
9
(
λ 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
x8
)
)
)
)
)
)
)
)
)
4
=
x4
(proof)
Known
In_5_9
In_5_9
:
5
∈
9
Theorem
tuple_9_5_eq
tuple_9_5_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
ap
(
lam
9
(
λ 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
x8
)
)
)
)
)
)
)
)
)
5
=
x5
(proof)
Known
In_6_9
In_6_9
:
6
∈
9
Theorem
tuple_9_6_eq
tuple_9_6_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
ap
(
lam
9
(
λ 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
x8
)
)
)
)
)
)
)
)
)
6
=
x6
(proof)
Known
In_7_9
In_7_9
:
7
∈
9
Theorem
tuple_9_7_eq
tuple_9_7_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
ap
(
lam
9
(
λ 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
x8
)
)
)
)
)
)
)
)
)
7
=
x7
(proof)
Known
In_8_9
In_8_9
:
8
∈
9
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
tuple_9_8_eq
tuple_9_8_eq
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
ap
(
lam
9
(
λ 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
x8
)
)
)
)
)
)
)
)
)
8
=
x8
(proof)