Search for blocks/addresses/...
Proofgold Asset
asset id
0051335d26562b3e55cb83927d005492f56ec48093fffec9d816ee913263deff
asset hash
55e61ca586b716f9b22a55d0c897097b6d9dce8dfa1902c6082a8c3542c51d1a
bday / block
2277
tx
02e2d..
preasset
doc published by
PrGxv..
Definition
dfe2d..
:=
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Param
57d6a..
:
ι
→
ι
→
ι
Param
3cd3c..
:
ι
Param
7a0ec..
:
ι
Param
5b8fe..
:
ι
Param
bcddf..
:
ι
→
(
ι
→
ι
) →
ι
Param
67ee8..
:
ι
Param
25ca3..
:
ι
Param
f3baa..
:
ι
Param
2f6f1..
:
ι
Definition
bcf0f..
:=
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
7a0ec..
5b8fe..
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x0 .
57d6a..
(
57d6a..
7a0ec..
5b8fe..
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x1 .
57d6a..
(
57d6a..
7a0ec..
5b8fe..
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x2 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
f3baa..
x0
)
(
57d6a..
(
57d6a..
f3baa..
x1
)
x2
)
)
)
(
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
2f6f1..
x0
)
x1
)
)
x2
)
)
)
)
)
)
)
)
Definition
96f1c..
:=
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x1 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x2 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
f3baa..
x0
)
(
57d6a..
(
57d6a..
f3baa..
x1
)
x2
)
)
)
(
λ x3 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
2f6f1..
x0
)
x1
)
)
(
λ x4 .
57d6a..
(
57d6a..
x4
x2
)
x3
)
)
)
)
)
Param
and
:
ο
→
ο
→
ο
Param
aac29..
:
(
ι
→
ι
→
ο
) →
ο
Definition
18e36..
:=
λ x0 :
ι →
ι → ο
.
and
(
aac29..
x0
)
(
x0
dfe2d..
bcf0f..
)
Param
505b1..
:
(
ι
→
ι
→
ο
) →
ο
Param
d478c..
:
(
ι
→
ι
→
ο
) →
(
ι
→
ι
→
ο
) →
ι
→
ο
Conjecture
fe7ba..
:
∀ x0 x1 :
ι →
ι → ο
.
aac29..
x0
⟶
505b1..
x1
⟶
d478c..
x0
x1
bcf0f..
Param
6fe8d..
:
(
ι
→
ι
→
ο
) →
(
ι
→
ι
→
ο
) →
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ο
Param
5c39b..
:
ι
→
ι
→
ο
Conjecture
a2bbc..
:
∀ x0 x1 :
ι →
ι → ο
.
aac29..
x0
⟶
505b1..
x1
⟶
6fe8d..
x0
x1
5c39b..
96f1c..
bcf0f..
Definition
a1610..
:=
λ x0 :
ι →
ι → ο
.
and
(
505b1..
x0
)
(
x0
dfe2d..
96f1c..
)
Definition
f4e87..
:=
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
Definition
5ca0f..
:=
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
7a0ec..
5b8fe..
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x0 .
57d6a..
(
57d6a..
7a0ec..
5b8fe..
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x1 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
2f6f1..
x0
)
x1
)
)
x0
)
)
)
)
)
Definition
9c283..
:=
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x1 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
2f6f1..
x0
)
x1
)
)
(
57d6a..
(
57d6a..
(
57d6a..
(
57d6a..
(
57d6a..
dfe2d..
x0
)
x1
)
x0
)
(
bcddf..
(
57d6a..
3cd3c..
x0
)
(
λ x2 .
bcddf..
(
57d6a..
3cd3c..
x1
)
(
λ x3 .
x2
)
)
)
)
)
)
)
Definition
c09b1..
:=
λ x0 :
ι →
ι → ο
.
and
(
18e36..
x0
)
(
x0
f4e87..
5ca0f..
)
Conjecture
879c3..
:
∀ x0 x1 :
ι →
ι → ο
.
18e36..
x0
⟶
a1610..
x1
⟶
d478c..
x0
x1
5ca0f..
Conjecture
e348c..
:
∀ x0 x1 :
ι →
ι → ο
.
18e36..
x0
⟶
a1610..
x1
⟶
6fe8d..
x0
x1
5c39b..
9c283..
5ca0f..
Definition
c842a..
:=
λ x0 :
ι →
ι → ο
.
and
(
a1610..
x0
)
(
x0
f4e87..
9c283..
)
Definition
ff764..
:=
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
Definition
3e999..
:=
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
7a0ec..
5b8fe..
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x0 .
57d6a..
(
57d6a..
7a0ec..
5b8fe..
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x1 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
2f6f1..
x0
)
x1
)
)
x1
)
)
)
)
)
Definition
0dcda..
:=
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x1 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
2f6f1..
x0
)
x1
)
)
(
57d6a..
(
57d6a..
(
57d6a..
(
57d6a..
(
57d6a..
dfe2d..
x0
)
x1
)
x1
)
(
bcddf..
(
57d6a..
3cd3c..
x0
)
(
λ x2 .
bcddf..
(
57d6a..
3cd3c..
x1
)
(
λ x3 .
x3
)
)
)
)
)
)
)
Definition
6afe7..
:=
λ x0 :
ι →
ι → ο
.
and
(
c09b1..
x0
)
(
x0
ff764..
3e999..
)
Conjecture
f28ac..
:
∀ x0 x1 :
ι →
ι → ο
.
c09b1..
x0
⟶
c842a..
x1
⟶
d478c..
x0
x1
3e999..
Conjecture
78997..
:
∀ x0 x1 :
ι →
ι → ο
.
c09b1..
x0
⟶
c842a..
x1
⟶
6fe8d..
x0
x1
5c39b..
0dcda..
3e999..
Definition
aa823..
:=
λ x0 :
ι →
ι → ο
.
and
(
c842a..
x0
)
(
x0
ff764..
0dcda..
)
Definition
1798d..
:=
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Param
62b32..
:
ι
Definition
950bd..
:=
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
7a0ec..
5b8fe..
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x0 .
57d6a..
(
57d6a..
7a0ec..
5b8fe..
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x1 .
57d6a..
(
57d6a..
7a0ec..
5b8fe..
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x2 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
f3baa..
x0
)
x2
)
)
(
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
f3baa..
x1
)
x2
)
)
(
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
62b32..
x0
)
x1
)
)
x2
)
)
)
)
)
)
)
)
)
Definition
c75ec..
:=
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x1 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x2 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
f3baa..
x0
)
x2
)
)
(
λ x3 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
f3baa..
x1
)
x2
)
)
(
λ x4 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
62b32..
x0
)
x1
)
)
(
λ x5 .
57d6a..
(
57d6a..
(
57d6a..
x5
x2
)
x3
)
x4
)
)
)
)
)
)
Definition
8484b..
:=
λ x0 :
ι →
ι → ο
.
and
(
6afe7..
x0
)
(
x0
1798d..
950bd..
)
Conjecture
57c7a..
:
∀ x0 x1 :
ι →
ι → ο
.
6afe7..
x0
⟶
aa823..
x1
⟶
d478c..
x0
x1
950bd..
Conjecture
cbf41..
:
∀ x0 x1 :
ι →
ι → ο
.
6afe7..
x0
⟶
aa823..
x1
⟶
6fe8d..
x0
x1
5c39b..
c75ec..
950bd..
Definition
43b81..
:=
λ x0 :
ι →
ι → ο
.
and
(
aa823..
x0
)
(
x0
1798d..
c75ec..
)
Definition
e7395..
:=
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Param
62f06..
:
ι
Definition
fb4c3..
:=
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
5b8fe..
)
5b8fe..
)
)
Param
c8911..
:
ι
Definition
a08a7..
:=
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x0 .
57d6a..
(
57d6a..
62b32..
x0
)
(
57d6a..
c8911..
x0
)
)
Definition
7412a..
:=
λ x0 :
ι →
ι → ο
.
and
(
8484b..
x0
)
(
x0
e7395..
fb4c3..
)
Conjecture
104a2..
:
∀ x0 x1 :
ι →
ι → ο
.
8484b..
x0
⟶
43b81..
x1
⟶
d478c..
x0
x1
fb4c3..
Conjecture
77591..
:
∀ x0 x1 :
ι →
ι → ο
.
8484b..
x0
⟶
43b81..
x1
⟶
6fe8d..
x0
x1
5c39b..
a08a7..
fb4c3..
Definition
5b618..
:=
λ x0 :
ι →
ι → ο
.
and
(
43b81..
x0
)
(
x0
e7395..
a08a7..
)
Definition
447f5..
:=
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Param
cb931..
:
ι
Param
1f2c4..
:
ι
Param
36978..
:
ι
Definition
09d0b..
:=
57d6a..
3cd3c..
(
57d6a..
cb931..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
(
57d6a..
7a0ec..
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
(
λ x1 .
57d6a..
(
57d6a..
7a0ec..
5b8fe..
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x2 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x3 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
x1
x3
)
)
x2
)
)
)
)
(
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
36978..
x0
)
x1
)
)
x2
)
)
)
)
)
)
)
)
Definition
f1cac..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
(
λ x1 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x2 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x3 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
x1
x3
)
)
x2
)
)
)
)
(
λ x3 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
36978..
x0
)
x1
)
)
(
λ x4 .
57d6a..
(
57d6a..
x4
x2
)
x3
)
)
)
)
)
Definition
98f68..
:=
λ x0 :
ι →
ι → ο
.
and
(
7412a..
x0
)
(
x0
447f5..
09d0b..
)
Conjecture
019fe..
:
∀ x0 x1 :
ι →
ι → ο
.
7412a..
x0
⟶
5b618..
x1
⟶
d478c..
x0
x1
09d0b..
Conjecture
b45fa..
:
∀ x0 x1 :
ι →
ι → ο
.
7412a..
x0
⟶
5b618..
x1
⟶
6fe8d..
x0
x1
5c39b..
f1cac..
09d0b..
Definition
548f8..
:=
λ x0 :
ι →
ι → ο
.
and
(
5b618..
x0
)
(
x0
447f5..
f1cac..
)
Definition
98f68..
:=
98f68..
Definition
548f8..
:=
548f8..