Search for blocks/addresses/...
Proofgold Address
address
PUfT1kHsNpXM4zt5v1ygzMW7nsfVriVyuN8
total
0
mg
-
conjpub
-
current assets
17640..
/
b471c..
bday:
2789
doc published by
PrGxv..
Param
f482f..
:
ι
→
ι
→
ι
Param
0fc90..
:
ι
→
(
ι
→
ι
) →
ι
Param
4ae4a..
:
ι
→
ι
Param
4a7ef..
:
ι
Param
If_i
:
ο
→
ι
→
ι
→
ι
Known
f22ec..
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
prim1
x2
x0
⟶
f482f..
(
0fc90..
x0
x1
)
x2
=
x1
x2
Known
06ef3..
:
prim1
4a7ef..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
Known
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Theorem
5e6e0..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
(
λ x9 .
If_i
(
x9
=
4a7ef..
)
x0
(
If_i
(
x9
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
x7
)
)
)
)
)
)
)
)
4a7ef..
=
x0
(proof)
Known
71150..
:
prim1
(
4ae4a..
4a7ef..
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
Definition
False
:=
∀ x0 : ο .
x0
Definition
not
:=
λ x0 : ο .
x0
⟶
False
Known
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Known
5c667..
:
4ae4a..
4a7ef..
=
4a7ef..
⟶
∀ x0 : ο .
x0
Theorem
96508..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
(
λ x9 .
If_i
(
x9
=
4a7ef..
)
x0
(
If_i
(
x9
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
x7
)
)
)
)
)
)
)
)
(
4ae4a..
4a7ef..
)
=
x1
(proof)
Known
49aa4..
:
prim1
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
Known
3a2b6..
:
4ae4a..
(
4ae4a..
4a7ef..
)
=
4a7ef..
⟶
∀ x0 : ο .
x0
Known
f9d2f..
:
4ae4a..
(
4ae4a..
4a7ef..
)
=
4ae4a..
4a7ef..
⟶
∀ x0 : ο .
x0
Theorem
ce37f..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
(
λ x9 .
If_i
(
x9
=
4a7ef..
)
x0
(
If_i
(
x9
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
x7
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
x2
(proof)
Known
caeb5..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
Known
57b7e..
:
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4a7ef..
⟶
∀ x0 : ο .
x0
Known
daead..
:
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
4a7ef..
⟶
∀ x0 : ο .
x0
Known
0c325..
:
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
4a7ef..
)
⟶
∀ x0 : ο .
x0
Theorem
0eec3..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
(
λ x9 .
If_i
(
x9
=
4a7ef..
)
x0
(
If_i
(
x9
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
x7
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
=
x3
(proof)
Known
d4e8e..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
Known
37f0a..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
=
4a7ef..
⟶
∀ x0 : ο .
x0
Known
d1b49..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
=
4ae4a..
4a7ef..
⟶
∀ x0 : ο .
x0
Known
05e02..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
=
4ae4a..
(
4ae4a..
4a7ef..
)
⟶
∀ x0 : ο .
x0
Known
2f510..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
⟶
∀ x0 : ο .
x0
Theorem
04e57..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
(
λ x9 .
If_i
(
x9
=
4a7ef..
)
x0
(
If_i
(
x9
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
x7
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
=
x4
(proof)
Known
69e64..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
Known
3dae7..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
=
4a7ef..
⟶
∀ x0 : ο .
x0
Known
a82a2..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
=
4ae4a..
4a7ef..
⟶
∀ x0 : ο .
x0
Known
7fa57..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
=
4ae4a..
(
4ae4a..
4a7ef..
)
⟶
∀ x0 : ο .
x0
Known
67cbd..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
⟶
∀ x0 : ο .
x0
Known
e25a7..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
⟶
∀ x0 : ο .
x0
Theorem
5c2dd..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
(
λ x9 .
If_i
(
x9
=
4a7ef..
)
x0
(
If_i
(
x9
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
x7
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
=
x5
(proof)
Known
4b5d5..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
Known
cdcd4..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
=
4a7ef..
⟶
∀ x0 : ο .
x0
Known
31e4d..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
=
4ae4a..
4a7ef..
⟶
∀ x0 : ο .
x0
Known
5ccd2..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
=
4ae4a..
(
4ae4a..
4a7ef..
)
⟶
∀ x0 : ο .
x0
Known
7357c..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
⟶
∀ x0 : ο .
x0
Known
d13e3..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
⟶
∀ x0 : ο .
x0
Known
2d896..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
⟶
∀ x0 : ο .
x0
Theorem
2df14..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
(
λ x9 .
If_i
(
x9
=
4a7ef..
)
x0
(
If_i
(
x9
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
x7
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
=
x6
(proof)
Known
cbdee..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
Known
ecc01..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
=
4a7ef..
⟶
∀ x0 : ο .
x0
Known
c6805..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
=
4ae4a..
4a7ef..
⟶
∀ x0 : ο .
x0
Known
58158..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
=
4ae4a..
(
4ae4a..
4a7ef..
)
⟶
∀ x0 : ο .
x0
Known
16901..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
⟶
∀ x0 : ο .
x0
Known
ee53e..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
⟶
∀ x0 : ο .
x0
Known
ac13b..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
⟶
∀ x0 : ο .
x0
Known
516c5..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
⟶
∀ x0 : ο .
x0
Theorem
98497..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
(
λ x9 .
If_i
(
x9
=
4a7ef..
)
x0
(
If_i
(
x9
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x9
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
x7
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
=
x7
(proof)
Known
1cd68..
:
prim1
4a7ef..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
Theorem
83b97..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
(
λ x10 .
If_i
(
x10
=
4a7ef..
)
x0
(
If_i
(
x10
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
x7
x8
)
)
)
)
)
)
)
)
)
4a7ef..
=
x0
(proof)
Known
4e80f..
:
prim1
(
4ae4a..
4a7ef..
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
Theorem
edf3f..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
(
λ x10 .
If_i
(
x10
=
4a7ef..
)
x0
(
If_i
(
x10
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
x7
x8
)
)
)
)
)
)
)
)
)
(
4ae4a..
4a7ef..
)
=
x1
(proof)
Known
384d5..
:
prim1
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
Theorem
6bdd5..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
(
λ x10 .
If_i
(
x10
=
4a7ef..
)
x0
(
If_i
(
x10
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
x7
x8
)
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
x2
(proof)
Known
c8b62..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
Theorem
ddf23..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
(
λ x10 .
If_i
(
x10
=
4a7ef..
)
x0
(
If_i
(
x10
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
x7
x8
)
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
=
x3
(proof)
Known
1ebb9..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
Theorem
bd5cb..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
(
λ x10 .
If_i
(
x10
=
4a7ef..
)
x0
(
If_i
(
x10
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
x7
x8
)
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
=
x4
(proof)
Known
9bb00..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
Theorem
e19f0..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
(
λ x10 .
If_i
(
x10
=
4a7ef..
)
x0
(
If_i
(
x10
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
x7
x8
)
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
=
x5
(proof)
Known
0d93c..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
Theorem
0ceda..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
(
λ x10 .
If_i
(
x10
=
4a7ef..
)
x0
(
If_i
(
x10
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
x7
x8
)
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
=
x6
(proof)
Known
65954..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
Theorem
b09b1..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
(
λ x10 .
If_i
(
x10
=
4a7ef..
)
x0
(
If_i
(
x10
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
x7
x8
)
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
=
x7
(proof)
Known
a1e1a..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
Known
58716..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
=
4a7ef..
⟶
∀ x0 : ο .
x0
Known
19797..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
=
4ae4a..
4a7ef..
⟶
∀ x0 : ο .
x0
Known
8fcc8..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
=
4ae4a..
(
4ae4a..
4a7ef..
)
⟶
∀ x0 : ο .
x0
Known
f5d01..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
⟶
∀ x0 : ο .
x0
Known
622d4..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
⟶
∀ x0 : ο .
x0
Known
17be6..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
⟶
∀ x0 : ο .
x0
Known
cc164..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
⟶
∀ x0 : ο .
x0
Known
c4f4e..
:
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
⟶
∀ x0 : ο .
x0
Theorem
212cb..
:
∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
)
(
λ x10 .
If_i
(
x10
=
4a7ef..
)
x0
(
If_i
(
x10
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
x6
(
If_i
(
x10
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
x7
x8
)
)
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
)
=
x8
(proof)
previous assets