Search for blocks/addresses/...
Proofgold Signed Transaction
vin
PrEvg..
/
e5537..
PUbXo..
/
3060e..
vout
PrEvg..
/
18146..
0.36 bars
TMbVg..
/
2307e..
ownership of
29aed..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJSY..
/
2a892..
ownership of
c2130..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFEG..
/
3f870..
ownership of
5d0c6..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMZV8..
/
43e77..
ownership of
20cee..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMSc1..
/
a3bec..
ownership of
21cd8..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMSyD..
/
434ed..
ownership of
bb94b..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMF8z..
/
501b8..
ownership of
de260..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMEsA..
/
9a027..
ownership of
5bbbd..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMajf..
/
1e9b3..
ownership of
5920d..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMNb8..
/
77e91..
ownership of
ad41d..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFe8..
/
701e3..
ownership of
ed937..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFwX..
/
42a0c..
ownership of
8691a..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMdaR..
/
ddf14..
ownership of
7e7e4..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJRk..
/
572f7..
ownership of
5bbcd..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMUi1..
/
66a99..
ownership of
63f8a..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPHr..
/
0628a..
ownership of
33c84..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMUSZ..
/
fd34c..
ownership of
9da57..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMVg1..
/
e30a1..
ownership of
5d52e..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMdCP..
/
4f55d..
ownership of
39d15..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXw3..
/
4c28f..
ownership of
a9d5c..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMRnn..
/
5b10e..
ownership of
e0314..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJN2..
/
895b3..
ownership of
6a6e1..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMby1..
/
48b74..
ownership of
472f9..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMVMV..
/
1cf7e..
ownership of
90a45..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMMKY..
/
47d79..
ownership of
5bcaf..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJyf..
/
43c0a..
ownership of
d3e5c..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMP7b..
/
37204..
ownership of
bd9b5..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMaSo..
/
f83be..
ownership of
c1fa7..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPsT..
/
a546f..
ownership of
b531a..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMddN..
/
7b26c..
ownership of
3b516..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQJF..
/
cab39..
ownership of
9d73b..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMc9Q..
/
d01e5..
ownership of
c690d..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFbr..
/
30a53..
ownership of
77d26..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMYgR..
/
6f331..
ownership of
dd093..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMUCz..
/
e987f..
ownership of
9315d..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFBT..
/
a29d2..
ownership of
8a85e..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMc7k..
/
89493..
ownership of
e8415..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMMdF..
/
6c861..
ownership of
b667c..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMZbJ..
/
32fe1..
ownership of
d9462..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMHMR..
/
9b917..
ownership of
92f24..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXL6..
/
d9ca2..
ownership of
657ef..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMdng..
/
f9f96..
ownership of
e4d19..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMLzH..
/
e0543..
ownership of
cb931..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMY45..
/
a1bf6..
ownership of
ec8af..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXUb..
/
298e6..
ownership of
7afff..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMT1Q..
/
acf7c..
ownership of
a1e82..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGzL..
/
22416..
ownership of
99fb9..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMNP5..
/
a53a8..
ownership of
90f6d..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQRG..
/
36354..
ownership of
7a0ec..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMUyr..
/
711c9..
ownership of
64950..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGxo..
/
cf186..
ownership of
8cc3c..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMHAn..
/
bd542..
ownership of
05100..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXwg..
/
78699..
ownership of
af815..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXfH..
/
24948..
ownership of
0af08..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXxJ..
/
daa5f..
ownership of
f3baa..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQtf..
/
d2feb..
ownership of
fc755..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMdpj..
/
54d14..
ownership of
3cabe..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQx3..
/
8a728..
ownership of
fdf84..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPfz..
/
f1f7d..
ownership of
68b13..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMc8q..
/
c6394..
ownership of
453db..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMNXr..
/
c032f..
ownership of
3cd3c..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQVm..
/
646c6..
ownership of
9e11e..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMLq5..
/
3a6d2..
ownership of
9888f..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGx2..
/
c04c5..
ownership of
fbc04..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMGCm..
/
7135a..
ownership of
1b59f..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQ1d..
/
e110b..
ownership of
bc384..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMN1H..
/
7857c..
ownership of
27862..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMVXt..
/
7b3fe..
ownership of
72b39..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMQQY..
/
2d2a6..
ownership of
d6106..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJDS..
/
107ad..
ownership of
3946d..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMNxP..
/
1a826..
ownership of
d7c0d..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMUbq..
/
67f4a..
ownership of
66b87..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMRGJ..
/
1c080..
ownership of
67ee8..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPWb..
/
b7ab8..
ownership of
1e5e6..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPt8..
/
09563..
ownership of
0c961..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMHn3..
/
d68ab..
ownership of
97dd6..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMY6B..
/
b4a65..
ownership of
f2088..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMTgF..
/
d334a..
ownership of
e88aa..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMTzt..
/
a1499..
ownership of
25ca3..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMSMn..
/
66532..
ownership of
f8cb3..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMWFg..
/
0a485..
ownership of
4a50e..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMZr8..
/
094db..
ownership of
c72c4..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMd7u..
/
67ec5..
ownership of
e36e8..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPyx..
/
efadb..
ownership of
96c22..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMPHh..
/
f8e71..
ownership of
61af4..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMWng..
/
0bb2a..
ownership of
1153f..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXUf..
/
76a39..
ownership of
302e5..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMWeA..
/
1973b..
ownership of
c0f24..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMW2p..
/
71178..
ownership of
67794..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMbYr..
/
67d34..
ownership of
6b978..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMFYw..
/
b5981..
ownership of
ffdc7..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMVe5..
/
64ec1..
ownership of
541d9..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMJMj..
/
22272..
ownership of
1f2c4..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMSvy..
/
38386..
ownership of
93a56..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TML6R..
/
176c9..
ownership of
5b8fe..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMakR..
/
c0738..
ownership of
93d41..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMdy8..
/
96154..
ownership of
edc3c..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMWYW..
/
128e4..
ownership of
46449..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMS2p..
/
17618..
ownership of
48ac8..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMKeS..
/
1cd9c..
ownership of
1ffeb..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TML4h..
/
b1329..
ownership of
62f06..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMXdu..
/
ac8b7..
ownership of
b4bb9..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMc6i..
/
1e650..
ownership of
934b2..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMV3N..
/
ca59b..
ownership of
18289..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMVWp..
/
8be77..
ownership of
bb8e6..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
TMNrg..
/
a65eb..
ownership of
9f625..
as obj with payaddr
PrGxv..
rights free controlledby
PrGxv..
upto 0
PUWQ4..
/
fe90b..
doc published by
PrGxv..
Param
True
:
ο
Definition
bb8e6..
:=
λ x0 :
ι →
ι → ο
.
True
Definition
bb8e6..
:=
λ x0 :
ι →
ι → ο
.
True
Definition
1f2c4..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
x0
x1
)
(
prim0
x1
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
x1
)
)
(
prim0
(
prim0
x1
x0
)
(
prim0
x1
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
Param
32d20..
:
ι
Definition
32d20..
:=
32d20..
Param
and
:
ο
→
ο
→
ο
Definition
934b2..
:=
λ x0 :
ι →
ι → ο
.
and
(
bb8e6..
x0
)
(
x0
1f2c4..
32d20..
)
Param
d478c..
:
(
ι
→
ι
→
ο
) →
(
ι
→
ι
→
ο
) →
ι
→
ο
Conjecture
a1ac9..
:
∀ x0 x1 :
ι →
ι → ο
.
bb8e6..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
32d20..
Definition
62f06..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
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
x0
)
(
prim0
x0
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
Param
91fd5..
:
ι
→
ι
→
ι
Definition
48ac8..
:=
91fd5..
1f2c4..
(
91fd5..
1f2c4..
1f2c4..
)
Definition
edc3c..
:=
λ x0 :
ι →
ι → ο
.
and
(
934b2..
x0
)
(
x0
62f06..
48ac8..
)
Conjecture
75198..
:
∀ x0 x1 :
ι →
ι → ο
.
934b2..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
48ac8..
Definition
5b8fe..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
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
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
Definition
1f2c4..
:=
1f2c4..
Definition
ffdc7..
:=
λ x0 :
ι →
ι → ο
.
and
(
edc3c..
x0
)
(
x0
5b8fe..
1f2c4..
)
Conjecture
f6498..
:
∀ x0 x1 :
ι →
ι → ο
.
edc3c..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
1f2c4..
Definition
67794..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
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
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
Definition
302e5..
:=
91fd5..
1f2c4..
32d20..
Definition
61af4..
:=
λ x0 :
ι →
ι → ο
.
and
(
ffdc7..
x0
)
(
x0
67794..
302e5..
)
Conjecture
51037..
:
∀ x0 x1 :
ι →
ι → ο
.
ffdc7..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
302e5..
Definition
e36e8..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
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
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
)
)
)
)
)
)
)
)
)
)
)
)
Definition
32d20..
:=
32d20..
Definition
4a50e..
:=
λ x0 :
ι →
ι → ο
.
and
(
61af4..
x0
)
(
x0
e36e8..
32d20..
)
Conjecture
3b7e7..
:
∀ x0 x1 :
ι →
ι → ο
.
61af4..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
32d20..
Definition
25ca3..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
Definition
f2088..
:=
91fd5..
1f2c4..
e36e8..
Definition
0c961..
:=
λ x0 :
ι →
ι → ο
.
and
(
4a50e..
x0
)
(
x0
25ca3..
f2088..
)
Conjecture
3fadb..
:
∀ x0 x1 :
ι →
ι → ο
.
4a50e..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
f2088..
Definition
67ee8..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
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
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
Definition
d7c0d..
:=
91fd5..
e36e8..
32d20..
Definition
d6106..
:=
λ x0 :
ι →
ι → ο
.
and
(
0c961..
x0
)
(
x0
67ee8..
d7c0d..
)
Conjecture
ddcd3..
:
∀ x0 x1 :
ι →
ι → ο
.
0c961..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
d7c0d..
Definition
27862..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
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
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
x1
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
x1
x1
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x0
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Definition
1b59f..
:=
91fd5..
(
91fd5..
1f2c4..
e36e8..
)
e36e8..
Definition
9888f..
:=
λ x0 :
ι →
ι → ο
.
and
(
d6106..
x0
)
(
x0
27862..
1b59f..
)
Conjecture
fa148..
:
∀ x0 x1 :
ι →
ι → ο
.
d6106..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
1b59f..
Definition
3cd3c..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
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
x0
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
Param
57d6a..
:
ι
→
ι
→
ι
Definition
68b13..
:=
91fd5..
(
57d6a..
67794..
5b8fe..
)
32d20..
Definition
3cabe..
:=
λ x0 :
ι →
ι → ο
.
and
(
9888f..
x0
)
(
x0
3cd3c..
68b13..
)
Conjecture
57580..
:
∀ x0 x1 :
ι →
ι → ο
.
9888f..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
68b13..
Definition
f3baa..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
x1
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
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
Definition
af815..
:=
91fd5..
(
57d6a..
67794..
5b8fe..
)
(
91fd5..
(
57d6a..
67794..
5b8fe..
)
(
57d6a..
67794..
5b8fe..
)
)
Definition
8cc3c..
:=
λ x0 :
ι →
ι → ο
.
and
(
3cabe..
x0
)
(
x0
f3baa..
af815..
)
Conjecture
4ef9d..
:
∀ x0 x1 :
ι →
ι → ο
.
3cabe..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
af815..
Definition
7a0ec..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
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
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
x1
x1
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x1
)
)
(
prim0
(
prim0
x0
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
Param
d7cf0..
:
ι
→
(
ι
→
ι
) →
ι
Definition
99fb9..
:=
d7cf0..
1f2c4..
(
λ x0 .
91fd5..
(
91fd5..
(
57d6a..
67794..
x0
)
(
57d6a..
67794..
5b8fe..
)
)
(
57d6a..
67794..
5b8fe..
)
)
Definition
7afff..
:=
λ x0 :
ι →
ι → ο
.
and
(
8cc3c..
x0
)
(
x0
7a0ec..
99fb9..
)
Conjecture
26e08..
:
∀ x0 x1 :
ι →
ι → ο
.
8cc3c..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
99fb9..
Definition
cb931..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
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
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
x1
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
x1
x0
)
)
(
prim0
(
prim0
x1
x1
)
(
prim0
x1
x1
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Definition
657ef..
:=
91fd5..
(
91fd5..
1f2c4..
(
57d6a..
67794..
5b8fe..
)
)
(
57d6a..
67794..
5b8fe..
)
Definition
d9462..
:=
λ x0 :
ι →
ι → ο
.
and
(
7afff..
x0
)
(
x0
cb931..
657ef..
)
Conjecture
64c5c..
:
∀ x0 x1 :
ι →
ι → ο
.
7afff..
x0
⟶
bb8e6..
x1
⟶
d478c..
x0
x1
657ef..
Param
bcddf..
:
ι
→
(
ι
→
ι
) →
ι
Param
236c6..
:
ι
Definition
e8415..
:=
λ x0 :
ι →
ι → ο
.
and
(
bb8e6..
x0
)
(
x0
67794..
(
bcddf..
236c6..
(
λ x1 .
57d6a..
67ee8..
(
57d6a..
25ca3..
x1
)
)
)
)
Definition
9315d..
:=
λ x0 :
ι →
ι → ο
.
and
(
e8415..
x0
)
(
∀ x1 x2 .
x0
(
57d6a..
67ee8..
(
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x1
)
x2
)
)
)
(
91fd5..
(
57d6a..
67794..
x1
)
(
57d6a..
67794..
x2
)
)
)
Definition
77d26..
:=
λ x0 :
ι →
ι → ο
.
and
(
9315d..
x0
)
(
∀ x1 .
x0
(
57d6a..
67ee8..
(
57d6a..
27862..
x1
)
)
(
d7cf0..
1f2c4..
(
λ x2 .
57d6a..
67ee8..
(
57d6a..
x1
x2
)
)
)
)
Definition
9d73b..
:=
λ x0 :
ι →
ι → ο
.
and
(
77d26..
x0
)
(
∀ x1 x2 .
x0
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
7a0ec..
x1
)
x2
)
)
(
d7cf0..
(
57d6a..
67794..
x1
)
(
λ x3 .
57d6a..
3cd3c..
(
57d6a..
x2
x3
)
)
)
)
Definition
b531a..
:=
λ x0 :
ι →
ι → ο
.
and
(
9d73b..
x0
)
(
∀ x1 x2 .
x0
(
57d6a..
3cd3c..
(
57d6a..
(
57d6a..
f3baa..
x1
)
x2
)
)
(
91fd5..
(
57d6a..
3cd3c..
x1
)
(
57d6a..
3cd3c..
x2
)
)
)
Definition
bd9b5..
:=
λ x0 :
ι →
ι → ο
.
and
(
b531a..
x0
)
(
∀ x1 .
x0
(
57d6a..
3cd3c..
(
57d6a..
cb931..
x1
)
)
(
d7cf0..
1f2c4..
(
λ x2 .
57d6a..
3cd3c..
(
57d6a..
x1
x2
)
)
)
)
Definition
5bcaf..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
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
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
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
x0
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Definition
472f9..
:=
57d6a..
67ee8..
(
57d6a..
27862..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
25ca3..
(
57d6a..
(
57d6a..
62f06..
x0
)
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
)
)
)
Definition
e0314..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
(
57d6a..
67794..
x0
)
(
λ x1 .
bcddf..
(
57d6a..
67794..
x0
)
(
λ x2 .
57d6a..
(
57d6a..
7a0ec..
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
(
bcddf..
236c6..
(
λ x3 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
x3
x1
)
)
(
57d6a..
x3
x2
)
)
)
)
)
)
Definition
39d15..
:=
λ x0 :
ι →
ι → ο
.
and
(
d9462..
x0
)
(
x0
5bcaf..
472f9..
)
Conjecture
235b5..
:
∀ x0 x1 :
ι →
ι → ο
.
d9462..
x0
⟶
bd9b5..
x1
⟶
d478c..
x0
x1
472f9..
Param
6fe8d..
:
(
ι
→
ι
→
ο
) →
(
ι
→
ι
→
ο
) →
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ο
Param
5c39b..
:
ι
→
ι
→
ο
Conjecture
d3a4f..
:
∀ x0 x1 :
ι →
ι → ο
.
d9462..
x0
⟶
bd9b5..
x1
⟶
6fe8d..
x0
x1
5c39b..
e0314..
472f9..
Definition
9da57..
:=
λ x0 :
ι →
ι → ο
.
and
(
bd9b5..
x0
)
(
x0
5bcaf..
e0314..
)
Definition
63f8a..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
Definition
7e7e4..
:=
57d6a..
3cd3c..
(
57d6a..
cb931..
(
bcddf..
236c6..
(
λ x0 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67794..
x0
)
(
λ x1 .
57d6a..
(
57d6a..
(
57d6a..
5bcaf..
x0
)
x1
)
x1
)
)
)
)
)
Definition
ed937..
:=
bcddf..
1f2c4..
(
λ x0 .
bcddf..
(
57d6a..
67794..
x0
)
(
λ x1 .
bcddf..
(
57d6a..
67794..
(
57d6a..
(
57d6a..
62f06..
x0
)
5b8fe..
)
)
(
λ x2 .
bcddf..
(
57d6a..
3cd3c..
(
57d6a..
x2
x1
)
)
(
λ x3 .
x3
)
)
)
)
Definition
5920d..
:=
λ x0 :
ι →
ι → ο
.
and
(
39d15..
x0
)
(
x0
63f8a..
7e7e4..
)
Conjecture
4daf7..
:
∀ x0 x1 :
ι →
ι → ο
.
39d15..
x0
⟶
9da57..
x1
⟶
d478c..
x0
x1
7e7e4..
Conjecture
ad088..
:
∀ x0 x1 :
ι →
ι → ο
.
39d15..
x0
⟶
9da57..
x1
⟶
6fe8d..
x0
x1
5c39b..
ed937..
7e7e4..
Definition
29aed..
:=
λ x0 :
ι →
ι → ο
.
and
(
9da57..
x0
)
(
x0
63f8a..
ed937..
)
Definition
de260..
:=
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
x0
)
(
prim0
x1
x1
)
)
)
)
)
(
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
x1
x1
)
(
prim0
x1
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
x0
)
)
)
)
)
(
prim0
(
prim1
(
λ x0 .
prim1
(
λ x1 .
prim0
(
prim0
(
prim0
x1
x0
)
(
prim0
x0
x0
)
)
(
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
x1
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
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
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
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
x0
)
)
(
prim0
(
prim0
x0
x1
)
(
prim0
x0
x1
)
)
)
)
)
(
prim1
(
λ x0 .
x0
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Definition
21cd8..
:=
57d6a..
3cd3c..
(
57d6a..
cb931..
(
bcddf..
1f2c4..
(
λ x0 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67794..
x0
)
(
λ x1 .
57d6a..
(
57d6a..
7a0ec..
x0
)
(
bcddf..
(
57d6a..
67794..
x0
)
(
λ x2 .
57d6a..
(
57d6a..
f3baa..
(
57d6a..
(
57d6a..
(
57d6a..
5bcaf..
x0
)
x1
)
x2
)
)
(
57d6a..
(
57d6a..
(
57d6a..
5bcaf..
x0
)
x2
)
x1
)
)
)
)
)
)
)
)
Definition
5d0c6..
:=
λ x0 :
ι →
ι → ο
.
and
(
5920d..
x0
)
(
x0
de260..
21cd8..
)
Conjecture
fcb0d..
:
∀ x0 x1 :
ι →
ι → ο
.
5920d..
x0
⟶
29aed..
x1
⟶
d478c..
x0
x1
21cd8..
Definition
5d0c6..
:=
5d0c6..
Definition
29aed..
:=
29aed..