Search for blocks/addresses/...
Proofgold Asset
asset id
e37a5d989a49091724ffddde9de83efa321743b7124254fc784331a65cc7b9e6
asset hash
2939ad670b6c12c427e860b97115c73b91b7f0ba6f6acd2b37392407ac32b21b
bday / block
2310
tx
ca535..
preasset
doc published by
PrGxv..
Param
and
:
ο
→
ο
→
ο
Param
244aa..
:
(
ι
→
ι
→
ο
) →
ο
Param
98f68..
:
(
ι
→
ι
→
ο
) →
ο
Param
5d0c6..
:
(
ι
→
ι
→
ο
) →
ο
Param
True
:
ο
Definition
0c0ca..
:=
λ x0 :
ι →
ι → ο
.
and
(
and
(
and
(
244aa..
x0
)
(
98f68..
x0
)
)
(
5d0c6..
x0
)
)
True
Param
39ffe..
:
(
ι
→
ι
→
ο
) →
ο
Param
548f8..
:
(
ι
→
ι
→
ο
) →
ο
Param
29aed..
:
(
ι
→
ι
→
ο
) →
ο
Definition
8e808..
:=
λ x0 :
ι →
ι → ο
.
and
(
and
(
and
(
39ffe..
x0
)
(
548f8..
x0
)
)
(
29aed..
x0
)
)
True
Definition
de13a..
:=
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
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
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
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
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
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
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
x0
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
x0
)
(
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
)
)
)
)
)
(
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
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
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
57d6a..
:
ι
→
ι
→
ι
Param
67ee8..
:
ι
Param
27862..
:
ι
Param
bcddf..
:
ι
→
(
ι
→
ι
) →
ι
Param
1f2c4..
:
ι
Param
25ca3..
:
ι
Param
62f06..
:
ι
Param
5b8fe..
:
ι
Definition
60acf..
:=
57d6a..
67ee8..
(
57d6a..
27862..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
5b8fe..
)
)
)
)
Param
7a0ec..
:
ι
Definition
64fce..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
)
(
λ x1 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x2 .
57d6a..
(
57d6a..
x1
x2
)
x2
)
)
)
)
Definition
bba79..
:=
λ x0 :
ι →
ι → ο
.
and
(
0c0ca..
x0
)
(
x0
de13a..
60acf..
)
Param
d478c..
:
(
ι
→
ι
→
ο
) →
(
ι
→
ι
→
ο
) →
ι
→
ο
Conjecture
98a99..
:
∀ x0 x1 :
ι →
ι → ο
.
0c0ca..
x0
⟶
8e808..
x1
⟶
d478c..
x0
x1
60acf..
Param
6fe8d..
:
(
ι
→
ι
→
ο
) →
(
ι
→
ι
→
ο
) →
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ο
Param
5c39b..
:
ι
→
ι
→
ο
Conjecture
7abd2..
:
∀ x0 x1 :
ι →
ι → ο
.
0c0ca..
x0
⟶
8e808..
x1
⟶
6fe8d..
x0
x1
5c39b..
64fce..
60acf..
Definition
1bfa8..
:=
λ x0 :
ι →
ι → ο
.
and
(
8e808..
x0
)
(
x0
de13a..
64fce..
)
Definition
c95dd..
:=
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
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
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
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
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
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
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
x0
)
(
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
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
x0
)
)
(
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
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Definition
60acf..
:=
57d6a..
67ee8..
(
57d6a..
27862..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
5b8fe..
)
)
)
)
Param
f3baa..
:
ι
Definition
8123e..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
)
(
λ x1 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x2 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x3 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x4 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
x1
x2
)
x3
)
)
(
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
x1
x3
)
x4
)
)
(
57d6a..
(
57d6a..
x1
x2
)
x4
)
)
)
)
)
)
)
)
)
)
Definition
d613a..
:=
λ x0 :
ι →
ι → ο
.
and
(
bba79..
x0
)
(
x0
c95dd..
60acf..
)
Conjecture
9b592..
:
∀ x0 x1 :
ι →
ι → ο
.
bba79..
x0
⟶
1bfa8..
x1
⟶
d478c..
x0
x1
60acf..
Conjecture
53ae6..
:
∀ x0 x1 :
ι →
ι → ο
.
bba79..
x0
⟶
1bfa8..
x1
⟶
6fe8d..
x0
x1
5c39b..
8123e..
60acf..
Definition
e2a7c..
:=
λ x0 :
ι →
ι → ο
.
and
(
1bfa8..
x0
)
(
x0
c95dd..
8123e..
)
Definition
4aa6c..
:=
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
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
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
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
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
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
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
x1
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x1
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
Definition
914f6..
:=
57d6a..
67ee8..
(
57d6a..
27862..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
)
)
)
Param
62b32..
:
ι
Param
0eacd..
:
ι
Definition
b0d1f..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
)
(
λ x1 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x2 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x3 .
57d6a..
(
57d6a..
62b32..
(
57d6a..
(
57d6a..
x1
x2
)
x3
)
)
(
57d6a..
(
57d6a..
(
57d6a..
0eacd..
x0
)
x2
)
x3
)
)
)
)
)
Definition
7804e..
:=
λ x0 :
ι →
ι → ο
.
and
(
d613a..
x0
)
(
x0
4aa6c..
914f6..
)
Conjecture
b9046..
:
∀ x0 x1 :
ι →
ι → ο
.
d613a..
x0
⟶
e2a7c..
x1
⟶
d478c..
x0
x1
914f6..
Conjecture
a9ae7..
:
∀ x0 x1 :
ι →
ι → ο
.
d613a..
x0
⟶
e2a7c..
x1
⟶
6fe8d..
x0
x1
5c39b..
b0d1f..
914f6..
Definition
8cdbd..
:=
λ x0 :
ι →
ι → ο
.
and
(
e2a7c..
x0
)
(
x0
4aa6c..
b0d1f..
)
Definition
b5f6e..
:=
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
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
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
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
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
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
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
x1
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
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
x0
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
x0
)
(
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
)
)
)
)
)
(
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
x0
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
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
3cd3c..
:
ι
Param
cb931..
:
ι
Definition
cd821..
:=
57d6a..
3cd3c..
(
57d6a..
cb931..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
(
57d6a..
7a0ec..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
)
(
λ x1 .
57d6a..
(
57d6a..
de13a..
x0
)
(
57d6a..
(
57d6a..
4aa6c..
x0
)
x1
)
)
)
)
)
)
Param
c85c4..
:
ι
Definition
52c1f..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
)
(
λ x1 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x2 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
5b8fe..
)
)
(
λ x3 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
x1
x2
)
x2
)
)
x3
)
)
(
λ x4 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
(
57d6a..
0eacd..
x0
)
x2
)
x2
)
)
x3
)
)
(
λ x5 .
57d6a..
x5
(
57d6a..
(
57d6a..
c85c4..
x0
)
x2
)
)
)
)
)
)
)
Definition
0b1f3..
:=
λ x0 :
ι →
ι → ο
.
and
(
7804e..
x0
)
(
x0
b5f6e..
cd821..
)
Conjecture
142d8..
:
∀ x0 x1 :
ι →
ι → ο
.
7804e..
x0
⟶
8cdbd..
x1
⟶
d478c..
x0
x1
cd821..
Conjecture
c382f..
:
∀ x0 x1 :
ι →
ι → ο
.
7804e..
x0
⟶
8cdbd..
x1
⟶
6fe8d..
x0
x1
5c39b..
52c1f..
cd821..
Definition
9a5fa..
:=
λ x0 :
ι →
ι → ο
.
and
(
8cdbd..
x0
)
(
x0
b5f6e..
52c1f..
)
Definition
d27f1..
:=
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
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
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
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
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
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
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
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
x0
x1
)
(
prim0
x0
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
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Definition
5571d..
:=
57d6a..
67ee8..
(
57d6a..
27862..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
27862..
(
bcddf..
1f2c4..
(
λ x1 .
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
(
57d6a..
(
57d6a..
62f06..
x0
)
x1
)
)
5b8fe..
)
)
)
)
)
)
Definition
1ba04..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
1f2c4..
(
λ x1 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
x1
)
)
)
(
λ x2 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x3 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x4 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
(
57d6a..
0eacd..
x1
)
(
57d6a..
x2
x3
)
)
(
57d6a..
x2
x4
)
)
)
(
57d6a..
(
57d6a..
(
57d6a..
0eacd..
x0
)
x3
)
x4
)
)
)
)
)
)
)
)
Definition
7c3c8..
:=
λ x0 :
ι →
ι → ο
.
and
(
0b1f3..
x0
)
(
x0
d27f1..
5571d..
)
Conjecture
1c10a..
:
∀ x0 x1 :
ι →
ι → ο
.
0b1f3..
x0
⟶
9a5fa..
x1
⟶
d478c..
x0
x1
5571d..
Conjecture
e0608..
:
∀ x0 x1 :
ι →
ι → ο
.
0b1f3..
x0
⟶
9a5fa..
x1
⟶
6fe8d..
x0
x1
5c39b..
1ba04..
5571d..
Definition
8c884..
:=
λ x0 :
ι →
ι → ο
.
and
(
9a5fa..
x0
)
(
x0
d27f1..
1ba04..
)
Definition
a6d01..
:=
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
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
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
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
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
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
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
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
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
x0
)
(
prim0
x1
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
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
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
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Definition
a7402..
:=
57d6a..
67ee8..
(
57d6a..
27862..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
x0
)
)
)
5b8fe..
)
)
)
)
Definition
d1d50..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
x0
)
)
)
)
(
λ x1 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x2 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x3 .
57d6a..
(
57d6a..
(
57d6a..
0eacd..
x0
)
(
57d6a..
(
57d6a..
x1
x2
)
x3
)
)
(
57d6a..
(
57d6a..
x1
x3
)
x2
)
)
)
)
)
)
)
Definition
980fb..
:=
λ x0 :
ι →
ι → ο
.
and
(
7c3c8..
x0
)
(
x0
a6d01..
a7402..
)
Conjecture
f604f..
:
∀ x0 x1 :
ι →
ι → ο
.
7c3c8..
x0
⟶
8c884..
x1
⟶
d478c..
x0
x1
a7402..
Conjecture
2a8a4..
:
∀ x0 x1 :
ι →
ι → ο
.
7c3c8..
x0
⟶
8c884..
x1
⟶
6fe8d..
x0
x1
5c39b..
d1d50..
a7402..
Definition
af7b1..
:=
λ x0 :
ι →
ι → ο
.
and
(
8c884..
x0
)
(
x0
a6d01..
d1d50..
)
Definition
c2196..
:=
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
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
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
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
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
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
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
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
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
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
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Definition
a7402..
:=
57d6a..
67ee8..
(
57d6a..
27862..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
x0
)
)
)
5b8fe..
)
)
)
)
Definition
3f3ae..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
x0
)
)
)
)
(
λ x1 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x2 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x3 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x4 .
57d6a..
(
57d6a..
(
57d6a..
0eacd..
x0
)
(
57d6a..
(
57d6a..
x1
(
57d6a..
(
57d6a..
x1
x2
)
x3
)
)
x4
)
)
(
57d6a..
(
57d6a..
x1
x2
)
(
57d6a..
(
57d6a..
x1
x3
)
x4
)
)
)
)
)
)
)
)
)
)
Definition
527b1..
:=
λ x0 :
ι →
ι → ο
.
and
(
980fb..
x0
)
(
x0
c2196..
a7402..
)
Conjecture
a8c34..
:
∀ x0 x1 :
ι →
ι → ο
.
980fb..
x0
⟶
af7b1..
x1
⟶
d478c..
x0
x1
a7402..
Conjecture
c1d7c..
:
∀ x0 x1 :
ι →
ι → ο
.
980fb..
x0
⟶
af7b1..
x1
⟶
6fe8d..
x0
x1
5c39b..
3f3ae..
a7402..
Definition
1b56f..
:=
λ x0 :
ι →
ι → ο
.
and
(
af7b1..
x0
)
(
x0
c2196..
3f3ae..
)
Definition
9b61a..
:=
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
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
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
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
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
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
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
x0
x0
)
(
prim0
x0
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
x0
x0
)
(
prim0
x0
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
x0
x0
)
(
prim0
x0
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
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
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Definition
ef6b7..
:=
57d6a..
67ee8..
(
57d6a..
27862..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
(
57d6a..
(
57d6a..
62f06..
(
57d6a..
(
57d6a..
62f06..
x0
)
x0
)
)
5b8fe..
)
)
)
)
)
Definition
75cd2..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
)
(
λ x1 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
x0
)
)
)
(
λ x2 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x3 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x4 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
x1
x3
)
x4
)
)
(
57d6a..
(
57d6a..
x1
(
57d6a..
x2
x3
)
)
(
57d6a..
x2
x4
)
)
)
)
)
)
)
)
)
Definition
8100b..
:=
λ x0 :
ι →
ι → ο
.
and
(
527b1..
x0
)
(
x0
9b61a..
ef6b7..
)
Conjecture
66cc8..
:
∀ x0 x1 :
ι →
ι → ο
.
527b1..
x0
⟶
1b56f..
x1
⟶
d478c..
x0
x1
ef6b7..
Conjecture
e7dc6..
:
∀ x0 x1 :
ι →
ι → ο
.
527b1..
x0
⟶
1b56f..
x1
⟶
6fe8d..
x0
x1
5c39b..
75cd2..
ef6b7..
Definition
4b2cb..
:=
λ x0 :
ι →
ι → ο
.
and
(
1b56f..
x0
)
(
x0
9b61a..
75cd2..
)
Definition
90dd1..
:=
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
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
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
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
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
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
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
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
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
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
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
x0
x1
)
(
prim0
x1
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Definition
0f09c..
:=
57d6a..
67ee8..
(
57d6a..
27862..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
x0
)
)
)
(
57d6a..
(
57d6a..
62f06..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
x0
)
)
)
5b8fe..
)
)
)
)
)
Definition
ae6de..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
x0
)
)
)
)
(
λ x1 .
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
x0
)
)
)
)
(
λ x2 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x3 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x4 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67ee8..
(
57d6a..
25ca3..
x0
)
)
(
λ x5 .
57d6a..
(
57d6a..
(
57d6a..
0eacd..
x0
)
(
57d6a..
(
57d6a..
x1
x3
)
(
57d6a..
(
57d6a..
x2
x4
)
x5
)
)
)
(
57d6a..
(
57d6a..
x2
(
57d6a..
(
57d6a..
x1
x3
)
x4
)
)
(
57d6a..
(
57d6a..
x1
x3
)
x5
)
)
)
)
)
)
)
)
)
)
)
Definition
e34e9..
:=
λ x0 :
ι →
ι → ο
.
and
(
8100b..
x0
)
(
x0
90dd1..
0f09c..
)
Conjecture
46c2b..
:
∀ x0 x1 :
ι →
ι → ο
.
8100b..
x0
⟶
4b2cb..
x1
⟶
d478c..
x0
x1
0f09c..
Conjecture
4c81c..
:
∀ x0 x1 :
ι →
ι → ο
.
8100b..
x0
⟶
4b2cb..
x1
⟶
6fe8d..
x0
x1
5c39b..
ae6de..
0f09c..
Definition
17cd1..
:=
λ x0 :
ι →
ι → ο
.
and
(
4b2cb..
x0
)
(
x0
90dd1..
ae6de..
)
Definition
e34e9..
:=
e34e9..
Definition
17cd1..
:=
17cd1..