Search for blocks/addresses/...
Proofgold Asset
asset id
7b80d761d0804168f5612c0695abade28ecab876f243d727f5e519acc755af5b
asset hash
36af5cfdb099445d02ff8d506076a06d9e1027af7973633c24e1dc7f2ff3fc65
bday / block
2790
tx
79be5..
preasset
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
03651..
:
prim1
4a7ef..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
Known
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Theorem
7d2e2..
:
∀ x0 x1 x2 x3 x4 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
(
λ x6 .
If_i
(
x6
=
4a7ef..
)
x0
(
If_i
(
x6
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x6
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x6
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
x4
)
)
)
)
)
4a7ef..
=
x0
...
Known
ff451..
:
prim1
(
4ae4a..
4a7ef..
)
(
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
504a8..
:
∀ x0 x1 x2 x3 x4 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
(
λ x6 .
If_i
(
x6
=
4a7ef..
)
x0
(
If_i
(
x6
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x6
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x6
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
x4
)
)
)
)
)
(
4ae4a..
4a7ef..
)
=
x1
...
Known
a7963..
:
prim1
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
Known
3a2b6..
:
4ae4a..
(
4ae4a..
4a7ef..
)
=
4a7ef..
⟶
∀ x0 : ο .
x0
Known
f9d2f..
:
4ae4a..
(
4ae4a..
4a7ef..
)
=
4ae4a..
4a7ef..
⟶
∀ x0 : ο .
x0
Theorem
fb20c..
:
∀ x0 x1 x2 x3 x4 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
(
λ x6 .
If_i
(
x6
=
4a7ef..
)
x0
(
If_i
(
x6
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x6
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x6
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
x4
)
)
)
)
)
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
x2
...
Known
9044c..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
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
431f3..
:
∀ x0 x1 x2 x3 x4 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
(
λ x6 .
If_i
(
x6
=
4a7ef..
)
x0
(
If_i
(
x6
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x6
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x6
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
x4
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
=
x3
...
Known
3b34e..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
(
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
ffdcd..
:
∀ x0 x1 x2 x3 x4 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
(
λ x6 .
If_i
(
x6
=
4a7ef..
)
x0
(
If_i
(
x6
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x6
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x6
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
x4
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
=
x4
...
Known
652a2..
:
prim1
4a7ef..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
Theorem
d842e..
:
∀ x0 x1 x2 x3 x4 x5 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
(
λ x7 .
If_i
(
x7
=
4a7ef..
)
x0
(
If_i
(
x7
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
x5
)
)
)
)
)
)
4a7ef..
=
x0
...
Known
71fcb..
:
prim1
(
4ae4a..
4a7ef..
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
Theorem
df2aa..
:
∀ x0 x1 x2 x3 x4 x5 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
(
λ x7 .
If_i
(
x7
=
4a7ef..
)
x0
(
If_i
(
x7
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
x5
)
)
)
)
)
)
(
4ae4a..
4a7ef..
)
=
x1
...
Known
7f899..
:
prim1
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
Theorem
3956e..
:
∀ x0 x1 x2 x3 x4 x5 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
(
λ x7 .
If_i
(
x7
=
4a7ef..
)
x0
(
If_i
(
x7
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
x5
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
x2
...
Known
d88ba..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
Theorem
c9d91..
:
∀ x0 x1 x2 x3 x4 x5 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
(
λ x7 .
If_i
(
x7
=
4a7ef..
)
x0
(
If_i
(
x7
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
x5
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
=
x3
...
Known
15e7b..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
Theorem
e2ad4..
:
∀ x0 x1 x2 x3 x4 x5 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
(
λ x7 .
If_i
(
x7
=
4a7ef..
)
x0
(
If_i
(
x7
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
x5
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
=
x4
...
Known
98e34..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
(
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
7039d..
:
∀ x0 x1 x2 x3 x4 x5 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
(
λ x7 .
If_i
(
x7
=
4a7ef..
)
x0
(
If_i
(
x7
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
x5
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
=
x5
...
Known
b9890..
:
prim1
4a7ef..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
Theorem
9619e..
:
∀ x0 x1 x2 x3 x4 x5 x6 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
(
λ x8 .
If_i
(
x8
=
4a7ef..
)
x0
(
If_i
(
x8
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
x6
)
)
)
)
)
)
)
4a7ef..
=
x0
...
Known
102c8..
:
prim1
(
4ae4a..
4a7ef..
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
Theorem
31081..
:
∀ x0 x1 x2 x3 x4 x5 x6 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
(
λ x8 .
If_i
(
x8
=
4a7ef..
)
x0
(
If_i
(
x8
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
x6
)
)
)
)
)
)
)
(
4ae4a..
4a7ef..
)
=
x1
...
Known
28cca..
:
prim1
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
Theorem
3daa5..
:
∀ x0 x1 x2 x3 x4 x5 x6 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
(
λ x8 .
If_i
(
x8
=
4a7ef..
)
x0
(
If_i
(
x8
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
x6
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
x2
...
Known
57aad..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
Theorem
bb257..
:
∀ x0 x1 x2 x3 x4 x5 x6 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
(
λ x8 .
If_i
(
x8
=
4a7ef..
)
x0
(
If_i
(
x8
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
x6
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
=
x3
...
Known
ea5d5..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
Theorem
85552..
:
∀ x0 x1 x2 x3 x4 x5 x6 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
(
λ x8 .
If_i
(
x8
=
4a7ef..
)
x0
(
If_i
(
x8
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
x6
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
=
x4
...
Known
1ceed..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
Theorem
33c62..
:
∀ x0 x1 x2 x3 x4 x5 x6 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
(
λ x8 .
If_i
(
x8
=
4a7ef..
)
x0
(
If_i
(
x8
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
x6
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
=
x5
...
Known
57cc6..
:
prim1
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
(
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
7a7b6..
:
∀ x0 x1 x2 x3 x4 x5 x6 .
f482f..
(
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
)
(
λ x8 .
If_i
(
x8
=
4a7ef..
)
x0
(
If_i
(
x8
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x8
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
x6
)
)
)
)
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
=
x6
...