Search for blocks/addresses/...
Proofgold Asset
asset id
cc748500ff1bc4829870dbf3cf33e03434e407f5e5ea186566516914325acee7
asset hash
f3b7868f7e1f98327676ceaeff3ce587566a7739a23945f00c6a95315cfce9b7
bday / block
4824
tx
a8220..
preasset
doc published by
PrGxv..
Theorem
96d2f..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
x0
x5
x6
⟶
(
∀ x24 .
x0
x24
x7
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x5
)
)
(
x24
=
x6
)
)
⟶
(
∀ x24 .
x1
x24
x24
)
⟶
(
∀ x24 x25 .
x1
(
x11
x24
x25
)
x25
)
⟶
(
∀ x24 x25 x26 .
x2
x24
x25
⟶
x1
(
x10
x24
x25
)
(
x10
x24
x26
)
⟶
x1
x25
x26
)
⟶
(
∀ x24 x25 x26 .
x0
x26
x25
⟶
not
(
x0
x26
(
x12
x24
x25
)
)
)
⟶
(
∀ x24 x25 x26 .
x0
x25
x24
⟶
x0
x26
x24
⟶
not
(
x1
x26
x25
)
⟶
x13
x24
)
⟶
(
∀ x24 x25 .
x1
x24
x25
⟶
x17
x24
⟶
x17
x25
)
⟶
(
∀ x24 .
x15
x24
⟶
x14
x24
)
⟶
(
∀ x24 x25 .
x2
x24
x25
⟶
x13
x24
⟶
x14
x25
⟶
x16
(
x10
x24
x25
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x14
x24
⟶
x13
(
x12
x24
(
x9
x25
)
)
)
⟶
not
(
x5
=
x6
)
⟶
not
(
x1
x5
x3
)
⟶
(
∀ x24 .
x1
x24
x5
⟶
not
(
x0
x3
x24
)
⟶
not
(
x0
x4
x24
)
⟶
x24
=
x3
)
⟶
x0
x3
(
x8
(
x9
x4
)
)
⟶
x0
x3
(
x12
(
x8
x5
)
(
x9
x4
)
)
⟶
not
(
x0
x4
(
x9
x5
)
)
⟶
x1
x4
(
x8
(
x9
x4
)
)
⟶
not
(
x1
x5
(
x9
x4
)
)
⟶
not
(
x1
x5
(
x9
x5
)
)
⟶
not
(
x1
(
x9
x4
)
(
x9
x5
)
)
⟶
x1
(
x9
x4
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
(
x8
x5
)
)
⟶
(
∀ x24 .
x0
x24
(
x8
x5
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
x4
)
)
(
x24
=
x5
)
)
⟶
not
(
x9
x5
=
x6
)
⟶
x1
x6
(
x8
x5
)
⟶
not
(
x0
(
x9
x5
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x8
(
x8
(
x9
x4
)
)
)
⟶
x0
x3
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
x0
(
x9
x4
)
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x9
x4
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
)
⟶
x0
x5
(
x10
(
x12
(
x8
x5
)
x5
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x9
x5
)
(
x9
x6
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
x7
)
⟶
x0
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
⟶
x0
x4
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
x0
x5
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
not
(
x0
x6
(
x9
(
x8
x5
)
)
)
⟶
x0
(
x8
x5
)
(
x10
x6
(
x9
(
x8
x5
)
)
)
⟶
x1
x6
(
x10
x6
(
x9
(
x8
(
x9
x4
)
)
)
)
⟶
x1
(
x9
(
x9
x5
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x1
x7
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
⟶
not
(
x1
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x4
(
x9
(
x8
x5
)
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x1
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x8
x5
)
)
⟶
x12
x5
(
x9
x3
)
=
x9
x4
⟶
x12
x5
(
x9
x4
)
=
x4
⟶
x12
x6
(
x9
x3
)
=
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
⟶
x1
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x12
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
x3
)
)
⟶
x1
(
x9
x5
)
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x9
x4
)
)
⟶
x1
(
x12
(
x8
x5
)
(
x9
x3
)
)
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x1
(
x8
(
x9
(
x9
x4
)
)
)
(
x12
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
(
x9
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x24
=
x3
)
⟶
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x9
x5
)
)
⟶
not
(
x24
=
x6
)
⟶
x0
x24
x5
)
⟶
x11
(
x10
(
x9
(
x9
x4
)
)
x7
)
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
=
x12
x6
(
x9
x4
)
⟶
not
(
x15
(
x10
x5
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x16
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
)
⟶
x14
x6
⟶
x14
(
x12
x7
(
x9
x4
)
)
⟶
x15
(
x10
x6
(
x9
(
x8
x5
)
)
)
⟶
x16
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
x7
)
⟶
x19
x5
⟶
x19
(
x11
(
x10
(
x9
(
x9
x5
)
)
x7
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
)
⟶
x19
(
x12
(
x8
x5
)
x5
)
⟶
x20
(
x12
(
x8
x5
)
(
x9
x5
)
)
⟶
x20
(
x11
(
x10
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
)
⟶
not
(
x14
(
x12
(
x11
(
x10
x6
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
(
x8
(
x12
x6
(
x9
x4
)
)
)
)
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
)
⟶
x20
(
x12
(
x8
x5
)
(
x9
x3
)
)
⟶
x21
(
x10
x6
(
x9
(
x9
x5
)
)
)
⟶
x20
(
x12
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x5
(
x9
(
x8
x5
)
)
)
)
(
x9
x3
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x0
x24
(
x9
x4
)
)
⟶
x0
x24
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
⟶
x0
x24
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
⟶
not
(
x16
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
)
⟶
x22
(
x12
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
(
x9
x4
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x0
x24
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x0
x24
(
x9
x5
)
)
⟶
x0
x24
(
x10
(
x9
x4
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x0
x24
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
x0
x24
(
x10
x6
(
x9
(
x9
x5
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x0
x24
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x16
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
x24
)
)
)
)
⟶
x1
(
x12
x6
(
x9
x3
)
)
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(proof)
Known
8106d..
notI
:
∀ x0 : ο .
(
x0
⟶
False
)
⟶
not
x0
Known
notE
notE
:
∀ x0 : ο .
not
x0
⟶
x0
⟶
False
Theorem
06e0d..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
(
∀ x24 .
iff
(
x19
x24
)
(
and
(
x13
x24
)
(
not
(
x14
x24
)
)
)
)
⟶
(
∀ x24 .
iff
(
x23
x24
)
(
and
(
x17
x24
)
(
not
(
x18
x24
)
)
)
)
⟶
(
∀ x24 x25 .
x1
x24
x25
⟶
x1
x25
x24
⟶
x24
=
x25
)
⟶
(
∀ x24 .
iff
(
x0
x24
x4
)
(
x24
=
x3
)
)
⟶
(
∀ x24 x25 x26 .
iff
(
x0
x26
(
x12
x24
x25
)
)
(
and
(
x0
x26
x24
)
(
not
(
x0
x26
x25
)
)
)
)
⟶
(
∀ x24 .
x0
x24
x6
⟶
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x5
)
)
⟶
x0
x3
x7
⟶
(
∀ x24 .
x0
x3
(
x8
x24
)
)
⟶
(
∀ x24 x25 x26 .
x10
x24
(
x10
x25
x26
)
=
x10
(
x10
x24
x25
)
x26
)
⟶
(
∀ x24 x25 .
x0
x24
x25
⟶
x13
(
x8
x25
)
)
⟶
(
∀ x24 x25 .
not
(
x0
x25
x24
)
⟶
x13
x24
⟶
x14
(
x10
x24
(
x9
x25
)
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x1
(
x9
x25
)
x24
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x21
x24
⟶
x20
(
x12
x24
(
x9
x25
)
)
)
⟶
(
∀ x24 x25 x26 .
x1
x26
(
x10
x24
x25
)
⟶
∀ x27 .
x0
x27
x24
⟶
not
(
x0
x27
x26
)
⟶
x15
x26
⟶
or
(
x14
x24
)
(
x14
x25
)
)
⟶
not
(
x0
x5
x3
)
⟶
not
(
x0
x6
x6
)
⟶
(
∀ x24 .
x1
x24
x5
⟶
not
(
x0
x3
x24
)
⟶
x0
x4
x24
⟶
x24
=
x9
x4
)
⟶
x0
x4
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
not
(
x3
=
x12
x6
(
x9
x4
)
)
⟶
x0
(
x9
x4
)
(
x12
(
x8
x5
)
(
x9
x5
)
)
⟶
not
(
x4
=
x12
x6
(
x9
x4
)
)
⟶
not
(
x0
x4
(
x12
x6
(
x9
x4
)
)
)
⟶
not
(
x1
(
x9
x5
)
x5
)
⟶
not
(
x9
x4
=
x12
(
x8
x5
)
x5
)
⟶
(
∀ x24 .
x0
x24
(
x9
(
x9
x4
)
)
⟶
x24
=
x9
x4
)
⟶
not
(
x5
=
x8
(
x9
x4
)
)
⟶
not
(
x9
(
x9
x4
)
=
x8
(
x9
x4
)
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
not
(
x0
(
x9
x4
)
x24
)
⟶
not
(
x0
x3
x24
)
⟶
x24
=
x3
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
x0
(
x9
x4
)
x24
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x8
(
x9
x4
)
)
)
⟶
not
(
x0
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x12
(
x8
x5
)
(
x9
x5
)
)
)
⟶
not
(
x5
=
x9
x5
)
⟶
not
(
x1
(
x12
x6
(
x9
x4
)
)
(
x9
x5
)
)
⟶
x0
x3
(
x8
(
x9
(
x9
x4
)
)
)
⟶
not
(
x0
(
x9
x4
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
x0
(
x9
x4
)
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x0
x4
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
(
x9
(
x9
x5
)
)
)
⟶
not
(
x0
x6
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
)
⟶
x0
x3
(
x10
x6
(
x9
(
x9
x5
)
)
)
⟶
x0
(
x12
x6
(
x9
x4
)
)
(
x8
(
x12
x6
(
x9
x4
)
)
)
⟶
x2
x5
(
x10
(
x9
(
x9
x4
)
)
(
x9
x6
)
)
⟶
x0
x4
(
x12
x7
(
x8
(
x9
x5
)
)
)
⟶
x0
x3
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
⟶
x0
x5
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x0
x5
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x0
x4
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
x0
x6
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x24
=
x5
)
⟶
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x6
)
)
⟶
x1
(
x8
x5
)
(
x10
(
x8
x5
)
(
x9
(
x8
x5
)
)
)
⟶
x12
x6
(
x9
x5
)
=
x5
⟶
x12
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
x3
)
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
⟶
x1
(
x8
(
x9
x4
)
)
(
x12
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
x4
)
)
⟶
x12
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
x4
)
=
x8
(
x9
x4
)
⟶
x1
(
x9
x4
)
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x9
x5
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
⟶
not
(
x24
=
x9
(
x9
x4
)
)
⟶
x0
x24
(
x8
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x24
=
x9
x4
)
⟶
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
x5
)
⟶
not
(
x24
=
x6
)
⟶
x0
x24
(
x9
x5
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x9
x4
)
)
⟶
not
(
x24
=
x5
)
⟶
x0
x24
(
x10
x4
(
x9
x6
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x8
(
x9
x5
)
)
)
⟶
not
(
x24
=
x5
)
⟶
x0
x24
(
x10
(
x9
x4
)
(
x9
x6
)
)
)
⟶
x11
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
=
x7
⟶
x1
(
x11
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
)
(
x12
x6
(
x9
x4
)
)
⟶
not
(
x15
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x4
(
x9
(
x8
x5
)
)
)
)
)
⟶
not
(
x16
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
)
⟶
not
(
x17
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
)
⟶
x13
(
x12
(
x8
x5
)
x5
)
⟶
x14
(
x12
x7
(
x9
x5
)
)
⟶
x16
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
x7
)
⟶
x16
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
⟶
x17
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
x21
(
x10
x6
(
x9
(
x9
x5
)
)
)
⟶
x21
x7
⟶
x21
(
x10
(
x12
(
x8
x5
)
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x22
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
x1
(
x12
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x9
x6
)
)
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
⟶
x1
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
(
x8
x5
)
)
)
(
x10
x6
(
x9
(
x9
x5
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
⟶
not
(
x16
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
x24
)
)
)
)
⟶
not
(
x0
x5
x5
)
(proof)
Known
50594..
iffEL
:
∀ x0 x1 : ο .
iff
x0
x1
⟶
x0
⟶
x1
Known
b4782..
contra
:
∀ x0 : ο .
(
not
x0
⟶
False
)
⟶
x0
Theorem
43593..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
(
∀ x24 x25 .
iff
(
x1
x24
x25
)
(
∀ x26 .
x0
x26
x24
⟶
x0
x26
x25
)
)
⟶
(
∀ x24 .
iff
(
x13
x24
)
(
∀ x25 : ο .
(
∀ x26 .
and
(
x0
x26
x24
)
(
not
(
x1
x24
(
x8
x26
)
)
)
⟶
x25
)
⟶
x25
)
)
⟶
(
∀ x24 x25 .
x0
x25
(
x8
x24
)
⟶
x1
x25
x24
)
⟶
(
∀ x24 x25 .
(
∀ x26 .
x0
x26
x24
⟶
not
(
x0
x26
x25
)
)
⟶
x2
x24
x25
)
⟶
(
∀ x24 x25 .
not
(
x0
x25
(
x9
x24
)
)
⟶
not
(
x25
=
x24
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x11
x24
(
x9
x25
)
=
x9
x25
)
⟶
(
∀ x24 x25 .
x15
(
x10
x24
x25
)
⟶
or
(
x13
x24
)
(
x14
x25
)
)
⟶
not
(
x1
x5
x3
)
⟶
not
(
x0
(
x9
x4
)
x3
)
⟶
x0
x4
(
x8
x5
)
⟶
x1
(
x9
x4
)
x5
⟶
not
(
x4
=
x9
x4
)
⟶
not
(
x0
x3
(
x12
(
x8
x5
)
x5
)
)
⟶
not
(
x0
(
x9
x4
)
(
x9
x4
)
)
⟶
not
(
x0
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
⟶
x1
(
x9
x4
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x0
(
x9
(
x9
x4
)
)
x5
)
⟶
not
(
x1
x5
(
x12
x6
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x9
(
x9
x4
)
)
⟶
x24
=
x9
x4
)
⟶
not
(
x5
=
x8
(
x9
x4
)
)
⟶
not
(
x0
x5
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x1
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
(
x8
x5
)
)
⟶
not
(
x1
(
x12
x6
(
x9
x4
)
)
(
x9
x5
)
)
⟶
not
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
=
x8
x5
)
⟶
x0
(
x9
x4
)
(
x10
(
x9
(
x9
x4
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x9
(
x9
x4
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
⟶
x0
x4
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
⟶
not
(
x0
(
x8
x5
)
(
x10
x6
(
x9
(
x9
x5
)
)
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
x7
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
x7
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x0
(
x8
x5
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x0
(
x12
(
x8
x5
)
x5
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
x0
(
x8
x5
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
⟶
x0
x6
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x1
x24
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x0
(
x9
x4
)
x24
)
⟶
x0
x4
x24
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x9
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
or
(
or
(
x24
=
x4
)
(
x24
=
x9
x4
)
)
(
x24
=
x5
)
)
⟶
x1
x6
(
x10
x6
(
x9
(
x9
x5
)
)
)
⟶
not
(
x1
(
x10
x6
(
x9
(
x9
x5
)
)
)
x6
)
⟶
x1
x7
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x1
(
x12
x7
(
x9
x4
)
)
(
x12
x6
(
x9
x4
)
)
)
⟶
x1
(
x8
(
x9
(
x9
x4
)
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x1
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
x12
x5
(
x9
x4
)
=
x4
⟶
x12
x6
(
x9
x3
)
=
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
⟶
x1
(
x12
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
x3
)
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
not
(
x24
=
x4
)
⟶
x0
x24
(
x12
(
x8
x5
)
x5
)
)
⟶
x1
(
x12
(
x8
x5
)
(
x9
(
x9
x4
)
)
)
x6
⟶
x1
x6
(
x12
(
x8
x5
)
(
x9
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x24
=
x3
)
⟶
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
)
⟶
x1
(
x10
(
x9
x4
)
(
x9
x6
)
)
(
x12
(
x12
x7
(
x8
(
x9
x5
)
)
)
(
x9
x5
)
)
⟶
x1
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
⟶
x1
(
x8
(
x9
x5
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
x1
(
x8
(
x9
x5
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x1
(
x12
x6
(
x9
x4
)
)
(
x10
(
x9
(
x9
x4
)
)
x7
)
⟶
x11
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x12
x7
(
x9
x4
)
)
=
x12
x6
(
x9
x4
)
⟶
x11
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
=
x12
x6
(
x9
x4
)
⟶
not
(
x13
(
x9
(
x8
x5
)
)
)
⟶
not
(
x14
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x14
(
x10
(
x9
(
x9
x4
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
)
⟶
not
(
x14
(
x10
x4
(
x9
x6
)
)
)
⟶
(
∀ x24 .
x0
x24
x6
⟶
not
(
x14
(
x12
x6
(
x9
x24
)
)
)
)
⟶
not
(
x16
(
x10
(
x9
x4
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x15
(
x12
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x9
x24
)
)
)
)
⟶
not
(
x17
(
x10
(
x9
(
x9
x4
)
)
x7
)
)
⟶
x13
(
x12
x7
x5
)
⟶
x15
(
x10
x6
(
x9
(
x8
x5
)
)
)
⟶
x19
x5
⟶
x19
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
x19
(
x12
x7
x5
)
⟶
x19
(
x10
(
x9
x6
)
(
x9
(
x8
x5
)
)
)
⟶
x21
(
x10
x5
(
x10
(
x9
x6
)
(
x9
(
x8
x5
)
)
)
)
⟶
x21
(
x11
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
)
⟶
x20
(
x12
(
x10
x6
(
x9
(
x8
x5
)
)
)
(
x9
x3
)
)
⟶
x22
(
x10
(
x9
(
x9
x4
)
)
x7
)
⟶
x20
(
x12
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
⟶
x22
(
x12
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
(
x9
x4
)
)
⟶
x1
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
x3
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x1
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
(
x9
x5
)
)
)
(
x10
x6
(
x9
(
x8
x5
)
)
)
⟶
not
(
x16
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
x4
)
)
)
⟶
not
(
x0
(
x9
x4
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(proof)
Theorem
0d2eb..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
(
∀ x24 .
iff
(
x15
x24
)
(
∀ x25 : ο .
(
∀ x26 .
and
(
x1
x26
x24
)
(
and
(
not
(
x1
x24
x26
)
)
(
x14
x26
)
)
⟶
x25
)
⟶
x25
)
)
⟶
(
∀ x24 .
iff
(
x20
x24
)
(
and
(
x14
x24
)
(
not
(
x15
x24
)
)
)
)
⟶
(
∀ x24 x25 .
iff
(
x0
x25
(
x8
x24
)
)
(
x1
x25
x24
)
)
⟶
(
∀ x24 x25 x26 .
x0
x26
x24
⟶
x0
x26
(
x10
x24
x25
)
)
⟶
(
∀ x24 x25 x26 .
x0
x25
x24
⟶
x0
x26
x24
⟶
not
(
x25
=
x26
)
⟶
x13
x24
)
⟶
(
∀ x24 x25 .
x1
x24
x25
⟶
x15
x24
⟶
x15
x25
)
⟶
(
∀ x24 x25 .
x1
x24
x25
⟶
x16
x24
⟶
x16
x25
)
⟶
(
∀ x24 x25 .
x15
(
x10
x24
x25
)
⟶
or
(
x14
x24
)
(
x13
x25
)
)
⟶
(
∀ x24 x25 .
x16
x24
⟶
not
(
x14
(
x11
x24
x25
)
)
⟶
x14
(
x12
x24
x25
)
)
⟶
(
∀ x24 .
x1
x24
x5
⟶
not
(
x0
x3
x24
)
⟶
not
(
x0
x4
x24
)
⟶
x24
=
x3
)
⟶
not
(
x3
=
x9
x4
)
⟶
not
(
x1
x5
(
x9
x4
)
)
⟶
not
(
x0
x3
(
x12
(
x8
x5
)
x5
)
)
⟶
not
(
x9
x4
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x9
x4
=
x12
(
x8
x5
)
x5
)
⟶
not
(
x9
x4
=
x8
x5
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
x0
(
x9
x4
)
x24
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x8
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
not
(
x0
(
x9
x4
)
x24
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x8
(
x9
x4
)
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
(
x9
x5
)
)
⟶
not
(
x0
(
x12
(
x8
x5
)
x5
)
x6
)
⟶
x1
(
x12
(
x8
x5
)
x5
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
⟶
not
(
x1
(
x8
x5
)
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
⟶
not
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
=
x8
x5
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x8
(
x9
(
x9
x4
)
)
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x8
(
x8
(
x9
x4
)
)
)
⟶
x0
x3
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x0
x5
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x12
(
x8
x5
)
x5
)
(
x9
(
x9
x5
)
)
)
⟶
not
(
x0
x6
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
)
⟶
not
(
x0
(
x8
x5
)
(
x10
x6
(
x9
(
x9
x5
)
)
)
)
⟶
not
(
x0
x5
(
x9
x6
)
)
⟶
x0
x6
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
⟶
x0
(
x9
x4
)
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
x0
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
⟶
x0
(
x8
x5
)
(
x10
x4
(
x9
(
x8
x5
)
)
)
⟶
x0
(
x8
x5
)
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x4
(
x9
(
x8
x5
)
)
)
)
⟶
x0
x5
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x0
x3
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
or
(
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
x4
)
)
(
x24
=
x5
)
)
(
x24
=
x9
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x9
x5
)
)
⟶
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x6
)
)
⟶
not
(
x1
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
x6
)
⟶
x1
x7
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
⟶
x1
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
x12
x6
(
x9
x3
)
=
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
⟶
x1
(
x9
x5
)
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x9
x4
)
)
⟶
x12
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
(
x9
x4
)
)
=
x12
x6
(
x9
x4
)
⟶
x1
(
x8
(
x9
x4
)
)
(
x12
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
x5
)
)
⟶
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
x5
)
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
⟶
(
∀ x24 .
x0
x24
(
x8
x5
)
⟶
not
(
x24
=
x9
x4
)
⟶
x0
x24
x6
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x24
=
x9
x4
)
⟶
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x24
=
x9
(
x9
x4
)
)
⟶
x0
x24
(
x8
x5
)
)
⟶
x1
(
x12
(
x12
x7
x5
)
(
x9
x5
)
)
(
x9
x6
)
⟶
x12
(
x12
x7
(
x9
x4
)
)
(
x9
x6
)
=
x12
x6
(
x9
x4
)
⟶
x12
(
x12
x7
(
x8
(
x9
x5
)
)
)
(
x9
x4
)
=
x12
x7
x5
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x8
(
x9
x5
)
)
)
⟶
not
(
x24
=
x5
)
⟶
x0
x24
(
x10
(
x9
x4
)
(
x9
x6
)
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x24
=
x3
)
⟶
x0
x24
(
x12
x7
(
x8
(
x9
x5
)
)
)
)
⟶
x1
(
x12
x6
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
⟶
x1
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
x1
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
⟶
x11
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x10
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
=
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
⟶
x0
x24
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x0
x24
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x8
x5
)
⟶
or
(
x0
x24
x6
)
(
x24
=
x9
x4
)
)
⟶
x11
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
=
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x6
(
x9
x4
)
)
⟶
not
(
x13
(
x12
(
x12
x6
(
x9
x4
)
)
(
x9
x24
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
⟶
not
(
x13
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x9
x24
)
)
)
)
⟶
not
(
x14
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
)
⟶
not
(
x14
(
x8
(
x9
x5
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x15
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x9
x24
)
)
)
)
⟶
not
(
x18
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
)
⟶
x14
(
x12
(
x8
x5
)
(
x9
x4
)
)
⟶
x14
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
⟶
x15
(
x10
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
⟶
x16
(
x10
(
x8
x5
)
(
x9
(
x8
x5
)
)
)
⟶
x16
(
x10
x7
(
x9
(
x8
x5
)
)
)
⟶
x17
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
x20
(
x11
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
)
⟶
x21
(
x10
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
⟶
x21
(
x12
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x9
x3
)
)
⟶
x21
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
not
(
x0
(
x8
x5
)
x6
)
(proof)
Known
93720..
iffER
:
∀ x0 x1 : ο .
iff
x0
x1
⟶
x1
⟶
x0
Known
eca40..
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Known
dcbd9..
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Theorem
9013d..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
(
∀ x24 .
iff
(
x13
x24
)
(
∀ x25 : ο .
(
∀ x26 .
and
(
x0
x26
x24
)
(
not
(
x1
x24
(
x8
x26
)
)
)
⟶
x25
)
⟶
x25
)
)
⟶
(
∀ x24 .
iff
(
x0
x24
x6
)
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x5
)
)
)
⟶
(
∀ x24 x25 x26 .
iff
(
x0
x26
(
x11
x24
x25
)
)
(
and
(
x0
x26
x24
)
(
x0
x26
x25
)
)
)
⟶
(
∀ x24 x25 x26 .
x0
x26
x25
⟶
x0
x26
(
x10
x24
x25
)
)
⟶
(
∀ x24 x25 x26 .
x1
(
x10
x24
(
x10
x25
x26
)
)
(
x10
(
x10
x24
x25
)
x26
)
)
⟶
(
∀ x24 x25 x26 .
x1
x26
x25
⟶
x1
(
x12
x24
x25
)
(
x12
x24
x26
)
)
⟶
(
∀ x24 x25 x26 .
(
∀ x27 .
x0
x27
x24
⟶
not
(
x0
x27
x25
)
⟶
x0
x27
x26
)
⟶
x1
(
x12
x24
x25
)
x26
)
⟶
(
∀ x24 x25 .
(
∀ x26 .
x0
x26
x24
⟶
not
(
x0
x26
x25
)
)
⟶
x2
x24
x25
)
⟶
(
∀ x24 x25 x26 .
not
(
x0
x26
x24
)
⟶
not
(
x0
x26
(
x12
x24
x25
)
)
)
⟶
(
∀ x24 x25 x26 .
x0
x25
x24
⟶
x0
x26
x24
⟶
not
(
x25
=
x26
)
⟶
x13
x24
)
⟶
(
∀ x24 x25 .
not
(
x24
=
x25
)
⟶
x13
(
x10
(
x9
x24
)
(
x9
x25
)
)
)
⟶
(
∀ x24 x25 .
x1
x24
x25
⟶
x14
x24
⟶
x14
x25
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x14
x24
⟶
x13
(
x12
x24
(
x9
x25
)
)
)
⟶
not
(
x4
=
x5
)
⟶
(
∀ x24 .
x0
x24
(
x9
x4
)
⟶
x24
=
x4
)
⟶
not
(
x4
=
x9
x4
)
⟶
not
(
x0
(
x9
x4
)
x5
)
⟶
x0
x4
(
x12
(
x8
x5
)
(
x9
x5
)
)
⟶
not
(
x0
(
x9
x5
)
x4
)
⟶
not
(
x0
x3
(
x9
(
x9
x4
)
)
)
⟶
x0
(
x9
x4
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
x1
x4
(
x12
x6
(
x9
x4
)
)
⟶
not
(
x1
x5
(
x12
x6
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x8
(
x9
x4
)
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
⟶
not
(
x0
(
x8
x5
)
(
x8
(
x8
(
x9
x4
)
)
)
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x4
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x0
x3
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
⟶
x0
x4
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x0
x5
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x0
x3
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x0
(
x12
x6
(
x9
x4
)
)
(
x8
(
x12
x6
(
x9
x4
)
)
)
⟶
x0
(
x8
x5
)
(
x10
x6
(
x9
(
x8
x5
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x5
)
)
(
x24
=
x9
(
x9
x4
)
)
)
⟶
not
(
x1
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
x5
)
⟶
x1
x7
(
x10
(
x9
(
x9
x4
)
)
x7
)
⟶
not
(
x1
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
x7
)
⟶
x1
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x1
(
x12
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
x3
)
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x9
x4
)
=
x9
x5
⟶
x1
(
x12
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
x5
)
)
(
x8
(
x9
x4
)
)
⟶
x12
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
=
x8
(
x9
x4
)
⟶
x1
x6
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
⟶
not
(
x13
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x9
x24
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
x5
)
⟶
not
(
x13
(
x12
(
x12
(
x8
x5
)
x5
)
(
x9
x24
)
)
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x0
x24
x5
)
⟶
not
(
x13
(
x12
(
x12
x7
x5
)
(
x9
x24
)
)
)
)
⟶
not
(
x15
(
x12
x7
(
x9
x4
)
)
)
⟶
not
(
x15
(
x10
x5
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x16
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
x24
)
)
⟶
not
(
x24
=
x4
)
)
⟶
not
(
x18
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
⟶
x13
(
x12
x6
(
x9
x4
)
)
⟶
x15
(
x10
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
⟶
x19
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
⟶
x19
(
x10
x4
(
x9
(
x8
x5
)
)
)
⟶
x19
(
x12
(
x12
x7
(
x9
x5
)
)
(
x9
x4
)
)
⟶
x1
(
x12
(
x11
(
x10
x6
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
(
x8
(
x12
x6
(
x9
x4
)
)
)
)
(
x9
x3
)
)
(
x10
(
x9
x4
)
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
⟶
x20
(
x12
x7
(
x9
x3
)
)
⟶
x21
(
x10
x5
(
x10
(
x9
x6
)
(
x9
(
x8
x5
)
)
)
)
⟶
x21
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
x3
)
)
⟶
x1
(
x12
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x9
x4
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
⟶
x22
(
x12
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
(
x9
x6
)
)
⟶
not
(
x9
x5
=
x6
)
(proof)
Theorem
67e67..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
(
∀ x24 x25 .
iff
(
x2
x24
x25
)
(
x11
x24
x25
=
x3
)
)
⟶
(
∀ x24 x25 .
iff
(
x0
x25
(
x9
x24
)
)
(
x25
=
x24
)
)
⟶
x0
x4
x7
⟶
(
∀ x24 x25 x26 .
x0
x26
(
x11
x24
x25
)
⟶
x0
x26
x25
)
⟶
(
∀ x24 x25 x26 .
x0
x26
x24
⟶
not
(
x0
x26
x25
)
⟶
x0
x26
(
x12
x24
x25
)
)
⟶
(
∀ x24 x25 .
x1
(
x10
x24
x25
)
(
x10
x25
x24
)
)
⟶
(
∀ x24 x25 x26 .
x2
x24
x25
⟶
x1
(
x10
x24
x25
)
(
x10
x24
x26
)
⟶
x1
x25
x26
)
⟶
(
∀ x24 x25 .
x0
x24
x25
⟶
x13
(
x8
x25
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
not
(
x17
x24
)
⟶
not
(
x16
(
x12
x24
(
x9
x25
)
)
)
)
⟶
(
∀ x24 x25 .
x1
x24
(
x10
(
x12
x24
x25
)
(
x11
x24
x25
)
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x20
x24
⟶
x19
(
x12
x24
(
x9
x25
)
)
)
⟶
not
(
x3
=
x4
)
⟶
not
(
x0
(
x9
x4
)
x3
)
⟶
not
(
x1
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
x5
)
⟶
x1
(
x9
(
x9
x4
)
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
(
x9
x4
)
x24
⟶
x0
x3
x24
⟶
x1
(
x8
(
x9
x4
)
)
x24
)
⟶
not
(
x1
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
⟶
not
(
x1
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x0
x6
(
x8
x5
)
)
⟶
not
(
x0
x6
(
x12
x6
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x8
x5
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
x4
)
)
(
x24
=
x5
)
)
⟶
not
(
x12
x6
(
x9
x4
)
=
x6
)
⟶
not
(
x0
x4
(
x9
(
x8
(
x9
x4
)
)
)
)
⟶
x0
(
x9
x4
)
(
x10
(
x9
(
x9
x4
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
⟶
x0
(
x9
x5
)
(
x9
(
x9
x5
)
)
⟶
not
(
x0
x5
(
x8
(
x12
x6
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x12
(
x8
x5
)
x5
)
x7
)
⟶
x0
(
x9
x4
)
(
x10
(
x9
(
x9
x4
)
)
x7
)
⟶
not
(
x0
(
x9
x4
)
(
x12
x7
x5
)
)
⟶
x0
(
x8
(
x9
x4
)
)
(
x10
(
x9
(
x8
(
x9
x4
)
)
)
x7
)
⟶
not
(
x0
(
x8
x5
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
x0
x3
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
x0
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
⟶
not
(
x0
(
x9
x4
)
(
x9
(
x8
x5
)
)
)
⟶
x0
x3
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
⟶
x0
x4
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x0
(
x9
x4
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
⟶
not
(
x1
(
x12
x7
(
x9
x5
)
)
x5
)
⟶
x1
(
x10
x6
(
x9
(
x9
x5
)
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x1
x7
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
x7
)
⟶
x1
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x10
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
⟶
x1
(
x12
x5
(
x9
x3
)
)
(
x9
x4
)
⟶
(
∀ x24 .
x0
x24
x6
⟶
not
(
x24
=
x3
)
⟶
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
)
⟶
x1
(
x12
(
x12
(
x8
x5
)
x5
)
(
x9
x5
)
)
(
x9
(
x9
x4
)
)
⟶
x12
(
x12
(
x8
x5
)
x5
)
(
x9
x5
)
=
x9
(
x9
x4
)
⟶
x12
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
(
x9
x4
)
)
=
x12
x6
(
x9
x4
)
⟶
x1
(
x8
(
x9
x4
)
)
(
x12
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
x5
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x24
=
x4
)
⟶
x0
x24
(
x10
(
x12
(
x8
x5
)
x5
)
(
x8
(
x9
(
x9
x4
)
)
)
)
)
⟶
x1
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x24
=
x9
(
x9
x4
)
)
⟶
x0
x24
(
x8
x5
)
)
⟶
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
=
x8
x5
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x8
(
x9
x5
)
)
)
⟶
not
(
x24
=
x6
)
⟶
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x24
=
x3
)
⟶
x0
x24
(
x12
x7
(
x8
(
x9
x5
)
)
)
)
⟶
x1
(
x12
x7
(
x8
(
x9
x5
)
)
)
(
x12
x7
(
x9
x3
)
)
⟶
x1
(
x10
x6
(
x9
(
x9
x5
)
)
)
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
⟶
x1
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
x5
)
)
)
⟶
x1
(
x12
x6
(
x9
x4
)
)
x7
⟶
(
∀ x24 .
x0
x24
x6
⟶
x0
x24
(
x8
(
x12
x6
(
x9
x4
)
)
)
⟶
x0
x24
x5
)
⟶
not
(
x14
x5
)
⟶
not
(
x14
(
x8
(
x9
x5
)
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x24
=
x4
)
⟶
not
(
x14
(
x12
(
x12
x7
(
x9
x4
)
)
(
x9
x24
)
)
)
)
⟶
not
(
x16
(
x8
x5
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x15
(
x12
x7
(
x9
x24
)
)
)
)
⟶
not
(
x16
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x5
(
x9
(
x8
x5
)
)
)
)
)
⟶
not
(
x17
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x18
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
⟶
x15
x7
⟶
x15
(
x10
x6
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
⟶
x15
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x5
(
x9
(
x8
x5
)
)
)
)
⟶
x16
(
x10
(
x9
(
x8
(
x9
x4
)
)
)
x7
)
⟶
x17
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
x20
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
⟶
x21
(
x12
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x9
x5
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x0
x24
(
x9
x6
)
)
⟶
x0
x24
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
⟶
x0
x24
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
)
⟶
not
(
x15
(
x12
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x9
x6
)
)
)
⟶
x1
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
(
x10
(
x9
x4
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
⟶
not
(
x16
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
x24
)
)
)
)
⟶
not
(
x0
x3
(
x9
(
x8
x5
)
)
)
(proof)
Theorem
8de73..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
(
∀ x24 .
iff
(
x13
x24
)
(
∀ x25 : ο .
(
∀ x26 .
and
(
x0
x26
x24
)
(
not
(
x1
x24
(
x8
x26
)
)
)
⟶
x25
)
⟶
x25
)
)
⟶
(
∀ x24 .
iff
(
x17
x24
)
(
∀ x25 : ο .
(
∀ x26 .
and
(
x1
x26
x24
)
(
and
(
not
(
x1
x24
x26
)
)
(
x16
x26
)
)
⟶
x25
)
⟶
x25
)
)
⟶
(
∀ x24 .
not
(
x0
x24
x24
)
)
⟶
(
∀ x24 x25 x26 .
x1
x26
x25
⟶
x1
(
x12
x24
x25
)
(
x12
x24
x26
)
)
⟶
(
∀ x24 x25 .
x0
x24
x25
⟶
x13
(
x8
x25
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
not
(
x18
x24
)
⟶
not
(
x17
(
x12
x24
(
x9
x25
)
)
)
)
⟶
(
∀ x24 x25 .
x1
x24
x25
⟶
x14
x24
⟶
x14
x25
)
⟶
(
∀ x24 x25 .
not
(
x17
x24
)
⟶
x13
(
x11
x24
x25
)
⟶
not
(
x15
(
x12
x24
x25
)
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x16
x24
⟶
x15
(
x12
x24
(
x9
x25
)
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x14
(
x12
x24
(
x9
x25
)
)
⟶
x15
x24
)
⟶
(
∀ x24 x25 .
x2
x24
x25
⟶
x19
x24
⟶
x19
x25
⟶
x21
(
x10
x24
x25
)
)
⟶
not
(
x0
x3
x3
)
⟶
not
(
x3
=
x12
(
x8
x5
)
x5
)
⟶
x0
(
x9
x4
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x1
x5
(
x9
x5
)
)
⟶
not
(
x1
(
x9
x4
)
(
x9
x5
)
)
⟶
not
(
x1
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x0
(
x9
x4
)
x6
)
⟶
not
(
x0
(
x9
x4
)
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
not
(
x0
(
x9
x4
)
x24
)
⟶
not
(
x0
x3
x24
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x8
(
x9
x4
)
)
)
⟶
not
(
x0
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x12
(
x8
x5
)
(
x9
x5
)
)
)
⟶
not
(
x0
(
x9
(
x9
x4
)
)
x6
)
⟶
not
(
x3
=
x8
x5
)
⟶
not
(
x8
(
x9
x4
)
=
x6
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
x5
)
⟶
or
(
x24
=
x9
x4
)
(
x24
=
x5
)
)
⟶
not
(
x1
(
x8
x5
)
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
⟶
x0
x3
(
x12
(
x8
(
x8
(
x9
x4
)
)
)
(
x9
(
x8
(
x9
x4
)
)
)
)
⟶
x0
(
x9
x5
)
(
x9
(
x9
x5
)
)
⟶
not
(
x0
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
⟶
x0
x3
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
)
⟶
not
(
x0
(
x12
(
x8
x5
)
x5
)
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
)
⟶
x0
x6
(
x12
x7
(
x9
x4
)
)
⟶
x0
x6
(
x12
x7
(
x8
(
x9
x5
)
)
)
⟶
x0
x6
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
⟶
x0
x4
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
x0
x5
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
x0
x3
(
x10
x4
(
x9
(
x8
x5
)
)
)
⟶
x0
x4
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x0
(
x9
x5
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x1
x24
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
x0
(
x9
x4
)
x24
⟶
not
(
x0
x4
x24
)
⟶
x24
=
x9
(
x9
x4
)
)
⟶
(
∀ x24 .
x1
x24
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x0
(
x9
x4
)
x24
)
⟶
not
(
x0
x4
x24
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x9
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x8
(
x9
x5
)
)
)
⟶
or
(
or
(
x24
=
x4
)
(
x24
=
x5
)
)
(
x24
=
x6
)
)
⟶
not
(
x1
(
x10
x5
(
x9
(
x8
x5
)
)
)
x5
)
⟶
x1
x6
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x1
x7
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
x7
)
⟶
x1
x7
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
not
(
x1
(
x12
x7
(
x9
x4
)
)
(
x12
x6
(
x9
x4
)
)
)
⟶
x1
(
x8
x5
)
(
x10
(
x8
x5
)
(
x9
(
x8
x5
)
)
)
⟶
x1
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x1
(
x12
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
(
x9
x4
)
)
)
x5
⟶
x1
(
x12
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
x3
)
)
(
x12
(
x8
x5
)
x5
)
⟶
x1
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x9
x4
)
)
)
⟶
x1
(
x12
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
⟶
x1
(
x12
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
(
x8
(
x9
x4
)
)
⟶
x1
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
x3
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
⟶
x1
(
x10
(
x12
(
x8
x5
)
x5
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
x4
)
)
⟶
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
x5
)
=
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
⟶
x12
(
x12
x7
(
x9
x5
)
)
(
x9
x4
)
=
x10
x4
(
x9
x6
)
⟶
x1
(
x12
(
x12
x7
x5
)
(
x9
x5
)
)
(
x9
x6
)
⟶
x1
(
x9
x5
)
(
x12
(
x12
x7
x5
)
(
x9
x6
)
)
⟶
x1
(
x12
x6
(
x9
x4
)
)
x7
⟶
x11
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
=
x7
⟶
x11
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
=
x7
⟶
x1
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x11
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
⟶
x11
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
=
x12
x6
(
x9
x4
)
⟶
not
(
x14
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x14
(
x10
(
x9
x4
)
(
x9
x6
)
)
)
⟶
not
(
x15
(
x12
x7
(
x9
x5
)
)
)
⟶
x13
(
x12
(
x8
x5
)
x5
)
⟶
x14
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x15
(
x10
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
⟶
x16
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
x14
(
x11
(
x10
x6
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
(
x8
(
x12
x6
(
x9
x4
)
)
)
)
⟶
x19
(
x8
(
x9
x5
)
)
⟶
x20
(
x12
(
x8
x5
)
(
x9
x4
)
)
⟶
x20
(
x11
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
)
⟶
x20
(
x11
(
x10
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
)
⟶
x1
(
x12
(
x11
(
x10
x6
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
(
x8
(
x12
x6
(
x9
x4
)
)
)
)
(
x9
x3
)
)
(
x10
(
x9
x4
)
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
⟶
x21
(
x10
(
x8
(
x9
x4
)
)
(
x12
x7
x5
)
)
⟶
x22
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
⟶
x21
(
x12
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x9
x4
)
)
⟶
x1
(
x12
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x9
x6
)
)
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
⟶
not
(
x16
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x0
x24
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
x0
x24
(
x10
x6
(
x9
(
x8
x5
)
)
)
)
⟶
x1
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
(
x9
x5
)
)
)
(
x10
x6
(
x9
(
x8
x5
)
)
)
⟶
not
(
x0
x6
x6
)
(proof)
Theorem
64754..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
(
∀ x24 .
iff
(
x0
x24
x5
)
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
x4
⟶
x24
=
x3
)
⟶
(
∀ x24 x25 .
x0
x25
(
x9
x24
)
⟶
x25
=
x24
)
⟶
(
∀ x24 x25 x26 .
x0
x26
x24
⟶
not
(
x0
x26
x25
)
⟶
x0
x26
(
x12
x24
x25
)
)
⟶
(
∀ x24 x25 .
x1
x25
(
x10
x24
x25
)
)
⟶
(
∀ x24 x25 x26 .
x0
x26
x25
⟶
not
(
x0
x26
(
x12
x24
x25
)
)
)
⟶
(
∀ x24 x25 .
x2
x24
x25
⟶
x13
x24
⟶
x13
x25
⟶
x15
(
x10
x24
x25
)
)
⟶
(
∀ x24 x25 .
x2
x24
x25
⟶
x13
x24
⟶
x14
x25
⟶
x16
(
x10
x24
x25
)
)
⟶
(
∀ x24 x25 .
x2
x24
x25
⟶
x13
x24
⟶
x15
x25
⟶
x17
(
x10
x24
x25
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x20
x24
⟶
x19
(
x12
x24
(
x9
x25
)
)
)
⟶
(
∀ x24 x25 x26 .
x1
x26
(
x10
x24
x25
)
⟶
∀ x27 .
x0
x27
x24
⟶
not
(
x0
x27
x26
)
⟶
x14
x26
⟶
x14
(
x10
(
x12
x24
(
x9
x27
)
)
x25
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x23
x24
⟶
x22
(
x12
x24
(
x9
x25
)
)
)
⟶
(
∀ x24 x25 .
not
(
x16
x24
)
⟶
not
(
x17
(
x10
x24
(
x9
x25
)
)
)
)
⟶
(
∀ x24 x25 .
not
(
x17
x24
)
⟶
not
(
x18
(
x10
x24
(
x9
x25
)
)
)
)
⟶
x0
x4
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x4
=
x9
x4
)
⟶
not
(
x0
(
x9
x5
)
x4
)
⟶
not
(
x0
(
x9
x4
)
(
x9
x5
)
)
⟶
not
(
x1
x5
(
x9
x5
)
)
⟶
not
(
x0
(
x9
x4
)
(
x9
x4
)
)
⟶
not
(
x1
(
x12
x6
(
x9
x4
)
)
x5
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
not
(
x0
(
x9
x4
)
x24
)
⟶
x0
x3
x24
⟶
x24
=
x4
)
⟶
not
(
x1
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x0
x6
(
x12
x6
(
x9
x4
)
)
)
⟶
not
(
x0
(
x12
(
x8
x5
)
x5
)
x6
)
⟶
not
(
x12
x6
(
x9
x4
)
=
x8
x5
)
⟶
not
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
=
x8
x5
)
⟶
not
(
x0
(
x9
x4
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x0
(
x9
x4
)
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
x0
x5
(
x10
x6
(
x9
(
x9
x5
)
)
)
⟶
x0
x4
(
x8
(
x12
x6
(
x9
x4
)
)
)
⟶
not
(
x0
x5
(
x10
x4
(
x9
x6
)
)
)
⟶
x0
x6
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
x0
(
x8
x5
)
(
x10
x5
(
x9
(
x8
x5
)
)
)
⟶
x0
x4
(
x10
x6
(
x9
(
x8
x5
)
)
)
⟶
x0
(
x8
x5
)
(
x10
x6
(
x9
(
x8
x5
)
)
)
⟶
x0
x4
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x5
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x1
x24
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x0
(
x9
x4
)
x24
)
⟶
x0
x4
x24
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x9
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x8
(
x9
(
x9
x4
)
)
)
⟶
or
(
x24
=
x3
)
(
x24
=
x9
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
⟶
x1
x7
(
x10
(
x9
(
x9
x4
)
)
x7
)
⟶
x1
x7
(
x10
(
x9
(
x8
(
x9
x4
)
)
)
x7
)
⟶
x1
x7
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
⟶
x1
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
x1
x4
(
x12
x5
(
x9
x4
)
)
⟶
(
∀ x24 .
x0
x24
x6
⟶
not
(
x24
=
x3
)
⟶
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
)
⟶
x1
(
x12
x6
(
x9
x3
)
)
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
⟶
x1
x5
(
x12
x6
(
x9
x5
)
)
⟶
x1
x4
(
x12
(
x12
x6
(
x9
x4
)
)
(
x9
x5
)
)
⟶
x1
(
x9
x4
)
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x9
x5
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
not
(
x24
=
x9
x4
)
⟶
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
)
⟶
x1
(
x8
(
x9
(
x9
x4
)
)
)
(
x12
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
(
x9
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x9
x5
)
)
⟶
not
(
x24
=
x4
)
⟶
x0
x24
(
x10
x4
(
x9
x6
)
)
)
⟶
x12
(
x12
x7
(
x9
x5
)
)
(
x9
x4
)
=
x10
x4
(
x9
x6
)
⟶
x12
(
x12
x7
(
x9
x4
)
)
(
x9
x3
)
=
x12
x7
x5
⟶
x12
(
x12
x7
(
x8
(
x9
x5
)
)
)
(
x9
x4
)
=
x12
x7
x5
⟶
x1
x6
(
x12
x7
(
x9
x6
)
)
⟶
x1
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
x5
)
)
)
⟶
x1
(
x8
(
x9
x5
)
)
(
x10
x6
(
x9
(
x9
x5
)
)
)
⟶
x11
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
=
x7
⟶
x1
(
x11
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x12
x7
(
x9
x4
)
)
)
(
x12
x6
(
x9
x4
)
)
⟶
not
(
x14
(
x12
(
x8
x5
)
x5
)
)
⟶
not
(
x14
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x15
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
)
⟶
not
(
x15
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
⟶
not
(
x14
(
x12
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
(
x9
x24
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x15
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x9
x24
)
)
)
)
⟶
x13
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
⟶
x14
(
x12
x7
(
x9
x4
)
)
⟶
x15
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x5
(
x9
(
x8
x5
)
)
)
)
⟶
x19
(
x10
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
(
x9
(
x8
x5
)
)
)
⟶
x20
(
x12
(
x8
x5
)
(
x9
x4
)
)
⟶
x20
(
x10
x5
(
x9
(
x8
x5
)
)
)
⟶
x20
(
x12
(
x8
x5
)
(
x9
(
x9
x4
)
)
)
⟶
x22
(
x10
x7
(
x9
(
x8
x5
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x0
x24
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x0
x24
(
x9
x4
)
)
⟶
x0
x24
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x0
x24
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
x0
x24
(
x10
x6
(
x9
(
x8
x5
)
)
)
)
⟶
x1
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
(
x9
x5
)
)
)
(
x10
x6
(
x9
(
x8
x5
)
)
)
⟶
not
(
x16
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
x3
)
)
)
⟶
not
(
x0
x3
(
x12
(
x8
x5
)
x5
)
)
(proof)
Theorem
67f36..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
(
∀ x24 x25 x26 .
iff
(
x0
x26
(
x11
x24
x25
)
)
(
and
(
x0
x26
x24
)
(
x0
x26
x25
)
)
)
⟶
(
∀ x24 x25 x26 .
x0
x26
x24
⟶
not
(
x0
x26
x25
)
⟶
x0
x26
(
x12
x24
x25
)
)
⟶
(
∀ x24 x25 .
x1
x24
(
x10
x24
x25
)
)
⟶
(
∀ x24 x25 x26 .
x1
x25
x26
⟶
x1
(
x10
x24
x25
)
(
x10
x24
x26
)
)
⟶
(
∀ x24 x25 x26 .
x2
x24
x25
⟶
x0
x26
x24
⟶
not
(
x0
x26
x25
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
not
(
x1
x24
(
x12
x24
(
x9
x25
)
)
)
)
⟶
(
∀ x24 x25 .
x1
x25
x24
⟶
not
(
x1
x24
x25
)
⟶
∀ x26 : ο .
(
∀ x27 .
and
(
x0
x27
x24
)
(
x1
x25
(
x12
x24
(
x9
x27
)
)
)
⟶
x26
)
⟶
x26
)
⟶
(
∀ x24 x25 .
x1
x24
x25
⟶
x16
x24
⟶
x16
x25
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x16
x24
⟶
x15
(
x12
x24
(
x9
x25
)
)
)
⟶
(
∀ x24 x25 .
not
(
x15
x24
)
⟶
not
(
x16
(
x10
x24
(
x9
x25
)
)
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x23
x24
⟶
x22
(
x12
x24
(
x9
x25
)
)
)
⟶
not
(
x0
x5
x3
)
⟶
not
(
x0
x6
x6
)
⟶
not
(
x1
x6
x5
)
⟶
not
(
x4
=
x5
)
⟶
not
(
x3
=
x6
)
⟶
(
∀ x24 .
x1
x24
(
x9
x4
)
⟶
or
(
x24
=
x3
)
(
x24
=
x9
x4
)
)
⟶
x0
(
x9
x4
)
(
x9
(
x9
x4
)
)
⟶
x0
x3
(
x8
(
x9
x4
)
)
⟶
not
(
x0
x3
(
x9
x5
)
)
⟶
(
∀ x24 .
x0
x24
(
x9
x4
)
⟶
x24
=
x4
)
⟶
not
(
x3
=
x9
x4
)
⟶
not
(
x0
(
x9
x4
)
x5
)
⟶
not
(
x0
(
x9
x4
)
(
x9
x4
)
)
⟶
x1
(
x9
x4
)
(
x12
(
x8
x5
)
(
x9
x5
)
)
⟶
not
(
x4
=
x9
(
x9
x4
)
)
⟶
not
(
x0
(
x12
(
x8
x5
)
x5
)
(
x9
(
x9
x4
)
)
)
⟶
x1
(
x9
(
x9
x4
)
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x1
(
x8
x5
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x0
(
x9
x5
)
x6
)
⟶
(
∀ x24 .
x0
x24
(
x8
x5
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
x4
)
)
(
x24
=
x5
)
)
⟶
not
(
x9
(
x9
x4
)
=
x6
)
⟶
not
(
x0
(
x8
x5
)
(
x8
(
x8
(
x9
x4
)
)
)
)
⟶
x0
x4
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x10
(
x12
(
x8
x5
)
x5
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x9
x4
)
(
x9
(
x9
x5
)
)
)
⟶
not
(
x0
x6
(
x9
(
x9
x5
)
)
)
⟶
not
(
x0
(
x12
(
x8
x5
)
x5
)
(
x9
(
x9
x5
)
)
)
⟶
x0
x3
(
x8
(
x12
x6
(
x9
x4
)
)
)
⟶
x0
(
x12
x6
(
x9
x4
)
)
(
x10
x6
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x9
(
x9
x4
)
)
x7
)
⟶
x0
(
x9
x4
)
(
x10
(
x9
(
x9
x4
)
)
x7
)
⟶
x0
x6
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
⟶
x0
x4
(
x12
(
x10
(
x9
(
x9
x5
)
)
x7
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
)
⟶
x0
x3
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
not
(
x0
(
x8
x5
)
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x4
(
x9
(
x8
x5
)
)
)
)
⟶
x0
(
x8
x5
)
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x4
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
)
⟶
x0
(
x8
x5
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x1
x24
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
x0
(
x9
x4
)
x24
⟶
not
(
x0
x4
x24
)
⟶
x24
=
x9
(
x9
x4
)
)
⟶
(
∀ x24 .
x0
x24
(
x9
(
x9
(
x9
x4
)
)
)
⟶
x24
=
x9
(
x9
x4
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x0
x24
x5
)
⟶
or
(
x24
=
x5
)
(
x24
=
x6
)
)
⟶
not
(
x1
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
x7
)
x7
)
⟶
x1
x7
(
x10
x7
(
x9
(
x8
x5
)
)
)
⟶
x1
(
x8
(
x9
(
x9
x4
)
)
)
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
⟶
not
(
x1
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x5
(
x9
(
x8
x5
)
)
)
)
(
x12
(
x8
(
x8
(
x9
x4
)
)
)
(
x9
(
x8
(
x9
x4
)
)
)
)
)
⟶
x1
(
x9
x4
)
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x9
x5
)
)
⟶
x1
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x9
x4
)
)
)
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
⟶
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
x5
)
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
⟶
x12
(
x8
x5
)
(
x9
x3
)
=
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
⟶
x12
(
x12
x7
x5
)
(
x9
x6
)
=
x9
x5
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x8
(
x9
x5
)
)
)
⟶
not
(
x24
=
x6
)
⟶
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x24
=
x3
)
⟶
x0
x24
(
x12
x7
(
x8
(
x9
x5
)
)
)
)
⟶
x12
x7
(
x9
x6
)
=
x6
⟶
x1
x5
(
x10
x6
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
⟶
x1
(
x12
x6
(
x9
x4
)
)
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
⟶
x11
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
=
x6
⟶
x11
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
=
x10
x6
(
x9
(
x9
x5
)
)
⟶
x11
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
=
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
⟶
x1
(
x12
x6
(
x9
x4
)
)
(
x11
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
)
⟶
not
(
x14
(
x12
(
x8
x5
)
x5
)
)
⟶
not
(
x15
(
x12
x7
(
x8
(
x9
x5
)
)
)
)
⟶
not
(
x17
(
x10
(
x8
x5
)
(
x9
(
x8
x5
)
)
)
)
⟶
x13
(
x12
(
x8
x5
)
x5
)
⟶
x15
x7
⟶
x19
x5
⟶
x19
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
⟶
x19
(
x12
(
x8
x5
)
x5
)
⟶
(
∀ x24 .
x0
x24
x6
⟶
x0
x24
(
x8
(
x12
x6
(
x9
x4
)
)
)
⟶
not
(
x0
x24
(
x9
x4
)
)
⟶
x0
x24
(
x10
(
x9
x3
)
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
)
⟶
x21
(
x10
x5
(
x10
(
x9
x6
)
(
x9
(
x8
x5
)
)
)
)
⟶
x21
(
x12
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x9
x6
)
)
⟶
x20
(
x12
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x12
x7
(
x9
x4
)
)
)
⟶
x15
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
not
(
x15
(
x12
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x9
x6
)
)
)
⟶
x1
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x10
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
(proof)
Theorem
8cf9e..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
(
∀ x24 .
iff
(
x0
x24
x4
)
(
x24
=
x3
)
)
⟶
(
∀ x24 .
iff
(
x0
x24
x5
)
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
)
⟶
(
∀ x24 x25 .
iff
(
x0
x25
(
x8
x24
)
)
(
x1
x25
x24
)
)
⟶
(
∀ x24 .
x1
x24
x3
⟶
x24
=
x3
)
⟶
(
∀ x24 x25 x26 .
x1
x24
x26
⟶
x1
x25
x26
⟶
x1
(
x10
x24
x25
)
x26
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
not
(
x1
x24
(
x12
x24
(
x9
x25
)
)
)
)
⟶
(
∀ x24 x25 .
not
(
x0
x25
x24
)
⟶
x13
x24
⟶
x14
(
x10
x24
(
x9
x25
)
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x1
(
x9
x25
)
x24
)
⟶
(
∀ x24 x25 x26 .
x1
x26
(
x10
x24
x25
)
⟶
not
(
x1
x26
x24
)
⟶
not
(
x1
x26
x25
)
⟶
not
(
x1
(
x10
x24
x25
)
x26
)
⟶
or
(
x13
x24
)
(
x13
x25
)
)
⟶
(
∀ x24 x25 .
x17
(
x10
x24
x25
)
⟶
or
(
x16
x24
)
(
x13
x25
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x23
x24
⟶
x22
(
x12
x24
(
x9
x25
)
)
)
⟶
(
∀ x24 x25 .
x18
(
x10
x24
x25
)
⟶
or
(
x17
x24
)
(
x13
x25
)
)
⟶
(
∀ x24 .
x0
x3
x24
⟶
x1
x4
x24
)
⟶
(
∀ x24 x25 .
x1
x25
(
x9
x24
)
⟶
or
(
x25
=
x3
)
(
x25
=
x9
x24
)
)
⟶
not
(
x0
x3
(
x9
x5
)
)
⟶
not
(
x0
x4
(
x8
(
x9
x4
)
)
)
⟶
not
(
x0
x4
(
x8
(
x9
x5
)
)
)
⟶
not
(
x0
(
x9
(
x9
x4
)
)
x5
)
⟶
not
(
x0
(
x9
x5
)
x5
)
⟶
x1
(
x9
(
x9
x4
)
)
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x0
(
x9
x4
)
x6
)
⟶
not
(
x0
(
x9
x4
)
(
x12
x6
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
not
(
x0
x3
x24
)
⟶
x1
x24
(
x9
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
not
(
x0
(
x9
x4
)
x24
)
⟶
x0
x3
x24
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x8
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x8
(
x9
x4
)
)
)
⟶
x1
(
x12
x6
(
x9
x4
)
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
⟶
not
(
x0
x6
(
x12
(
x8
x5
)
(
x9
x4
)
)
)
⟶
not
(
x0
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x0
x3
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x0
(
x9
x5
)
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
)
⟶
not
(
x0
(
x9
x4
)
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
)
⟶
x0
x5
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x0
(
x12
x6
(
x9
x4
)
)
(
x9
(
x12
x6
(
x9
x4
)
)
)
⟶
x0
(
x12
x6
(
x9
x4
)
)
(
x8
(
x12
x6
(
x9
x4
)
)
)
⟶
x0
x6
(
x10
x4
(
x9
x6
)
)
⟶
x0
x3
(
x12
x7
(
x9
x5
)
)
⟶
not
(
x0
(
x8
x5
)
x7
)
⟶
not
(
x0
(
x8
x5
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
not
(
x0
x3
(
x9
(
x8
x5
)
)
)
⟶
not
(
x0
x6
(
x9
(
x8
x5
)
)
)
⟶
x0
x4
(
x10
x5
(
x9
(
x8
x5
)
)
)
⟶
x0
x3
(
x10
x7
(
x9
(
x8
x5
)
)
)
⟶
x0
(
x9
x5
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
or
(
x24
=
x4
)
(
x24
=
x9
x4
)
)
⟶
not
(
x1
(
x12
(
x8
(
x8
(
x9
x4
)
)
)
(
x9
(
x8
(
x9
x4
)
)
)
)
x5
)
⟶
x1
x7
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
⟶
not
(
x1
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x4
(
x9
(
x8
x5
)
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x1
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x1
(
x12
(
x12
x6
(
x9
x4
)
)
(
x9
x5
)
)
x4
⟶
x12
(
x12
x6
(
x9
x4
)
)
(
x9
x5
)
=
x4
⟶
x1
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x9
x4
)
)
(
x9
x5
)
⟶
x1
(
x8
(
x9
x4
)
)
(
x12
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
x5
)
)
⟶
x1
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x9
x4
)
)
)
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
⟶
x1
x6
(
x12
(
x8
x5
)
(
x9
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x9
x5
)
)
⟶
not
(
x24
=
x6
)
⟶
x0
x24
x5
)
⟶
x1
(
x12
(
x12
x7
(
x9
x5
)
)
(
x9
x6
)
)
x5
⟶
(
∀ x24 .
x0
x24
(
x12
x7
x5
)
⟶
not
(
x24
=
x5
)
⟶
x0
x24
(
x9
x6
)
)
⟶
x1
(
x12
x7
x5
)
(
x12
(
x12
x7
(
x9
x4
)
)
(
x9
x3
)
)
⟶
x12
(
x12
x7
(
x9
x4
)
)
(
x9
x6
)
=
x12
x6
(
x9
x4
)
⟶
x1
x6
(
x12
x7
(
x9
x6
)
)
⟶
x1
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
⟶
x1
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
x7
⟶
(
∀ x24 .
x0
x24
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
⟶
x0
x24
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x0
x24
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
)
⟶
x11
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
=
x7
⟶
(
∀ x24 .
x0
x24
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
x0
x24
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x0
x24
(
x9
(
x8
x5
)
)
)
)
⟶
x11
(
x10
(
x9
(
x9
x5
)
)
x7
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
=
x12
x6
(
x9
x4
)
⟶
(
∀ x24 .
x0
x24
(
x12
x6
(
x9
x4
)
)
⟶
not
(
x13
(
x12
(
x12
x6
(
x9
x4
)
)
(
x9
x24
)
)
)
)
⟶
not
(
x14
(
x12
(
x8
x5
)
x5
)
)
⟶
not
(
x15
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x24
=
x4
)
⟶
not
(
x14
(
x12
(
x12
x7
(
x9
x4
)
)
(
x9
x24
)
)
)
)
⟶
not
(
x16
(
x10
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x16
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
x24
)
)
)
)
⟶
not
(
x17
(
x10
(
x9
(
x9
x4
)
)
x7
)
)
⟶
x13
(
x12
x6
(
x9
x4
)
)
⟶
x14
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x4
(
x9
(
x8
x5
)
)
)
)
⟶
x21
(
x11
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
⟶
x22
(
x10
(
x9
(
x8
(
x9
x4
)
)
)
x7
)
⟶
not
(
x16
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
x3
)
)
)
⟶
not
(
x16
(
x12
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
(
x9
(
x9
x5
)
)
)
)
⟶
x1
x4
(
x12
(
x12
x6
(
x9
x4
)
)
(
x9
x5
)
)
(proof)
Theorem
260da..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
(
∀ x24 x25 .
iff
(
x1
x24
x25
)
(
∀ x26 .
x0
x26
x24
⟶
x0
x26
x25
)
)
⟶
(
∀ x24 .
iff
(
x16
x24
)
(
∀ x25 : ο .
(
∀ x26 .
and
(
x1
x26
x24
)
(
and
(
not
(
x1
x24
x26
)
)
(
x15
x26
)
)
⟶
x25
)
⟶
x25
)
)
⟶
(
∀ x24 x25 .
x0
x24
x25
⟶
not
(
x0
x25
x24
)
)
⟶
(
∀ x24 .
iff
(
x0
x24
x6
)
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x5
)
)
)
⟶
(
∀ x24 x25 x26 .
x0
x26
x24
⟶
x0
x26
x25
⟶
x0
x26
(
x11
x24
x25
)
)
⟶
(
∀ x24 x25 x26 .
x1
x25
x26
⟶
x1
(
x10
x24
x25
)
(
x10
x24
x26
)
)
⟶
(
∀ x24 x25 .
x2
(
x12
x24
x25
)
(
x11
x24
x25
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x1
(
x9
x25
)
x24
)
⟶
(
∀ x24 x25 .
x0
x24
(
x8
(
x9
x25
)
)
⟶
or
(
x24
=
x3
)
(
x24
=
x9
x25
)
)
⟶
(
∀ x24 x25 x26 .
x1
x26
(
x10
x24
x25
)
⟶
∀ x27 .
x0
x27
x24
⟶
not
(
x0
x27
x26
)
⟶
x15
x26
⟶
x15
(
x10
(
x12
x24
(
x9
x27
)
)
x25
)
)
⟶
(
∀ x24 x25 .
x16
(
x10
x24
x25
)
⟶
or
(
x13
x24
)
(
x15
x25
)
)
⟶
not
(
x4
=
x5
)
⟶
(
∀ x24 .
x0
x3
x24
⟶
x1
x4
x24
)
⟶
(
∀ x24 .
x1
x24
(
x9
x4
)
⟶
or
(
x24
=
x3
)
(
x24
=
x9
x4
)
)
⟶
(
∀ x24 .
x1
x24
(
x9
(
x9
x4
)
)
⟶
or
(
x24
=
x3
)
(
x24
=
x9
(
x9
x4
)
)
)
⟶
not
(
x0
x4
(
x8
(
x9
x4
)
)
)
⟶
not
(
x9
x4
=
x5
)
⟶
not
(
x0
(
x9
x4
)
(
x9
x5
)
)
⟶
x0
(
x9
x4
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
⟶
not
(
x4
=
x9
(
x9
x4
)
)
⟶
not
(
x1
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
x5
)
⟶
not
(
x5
=
x12
x6
(
x9
x4
)
)
⟶
not
(
x0
(
x9
(
x9
x4
)
)
x6
)
⟶
not
(
x0
(
x9
x5
)
(
x12
x6
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
x5
)
⟶
or
(
x24
=
x9
x4
)
(
x24
=
x5
)
)
⟶
x0
x4
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
x0
(
x9
x4
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
⟶
x0
x3
(
x12
x7
(
x9
x5
)
)
⟶
x2
(
x8
(
x9
x4
)
)
(
x12
x7
x5
)
⟶
x0
x3
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
⟶
x0
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
⟶
x0
x4
(
x12
(
x10
(
x9
(
x9
x5
)
)
x7
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
)
⟶
not
(
x0
(
x9
x4
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
)
⟶
not
(
x0
x4
(
x9
(
x8
x5
)
)
)
⟶
not
(
x0
x6
(
x9
(
x8
x5
)
)
)
⟶
x0
x3
(
x10
x4
(
x9
(
x8
x5
)
)
)
⟶
x0
x5
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x0
(
x9
x4
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
⟶
(
∀ x24 .
x0
(
x9
x4
)
x24
⟶
x0
x4
x24
⟶
x1
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
x24
)
⟶
(
∀ x24 .
x1
x24
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
x0
(
x9
x4
)
x24
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x9
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
x5
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x9
x4
)
)
(
x24
=
x5
)
)
(
x24
=
x9
(
x9
x4
)
)
)
⟶
x1
x5
(
x12
x7
(
x9
x5
)
)
⟶
x1
(
x10
x6
(
x9
(
x9
x5
)
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x1
x7
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
not
(
x1
(
x10
(
x9
(
x9
x5
)
)
x7
)
x7
)
⟶
x1
(
x10
x6
(
x9
(
x9
x5
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x1
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
)
⟶
x1
(
x10
(
x9
(
x9
x5
)
)
x7
)
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
not
(
x1
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
x12
x5
(
x9
x4
)
=
x4
⟶
x1
(
x12
x6
(
x9
x4
)
)
(
x12
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
(
x9
x4
)
)
)
⟶
x12
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
(
x9
x4
)
)
=
x12
x6
(
x9
x4
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
not
(
x24
=
x5
)
⟶
x0
x24
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
x1
(
x12
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
(
x8
(
x9
x4
)
)
⟶
x1
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
⟶
not
(
x24
=
x9
(
x9
x4
)
)
⟶
x0
x24
(
x8
x5
)
)
⟶
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
=
x8
x5
⟶
x1
(
x12
(
x12
x7
(
x8
(
x9
x5
)
)
)
(
x9
x5
)
)
(
x10
(
x9
x4
)
(
x9
x6
)
)
⟶
x12
(
x12
x7
(
x8
(
x9
x5
)
)
)
(
x9
x6
)
=
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
⟶
x1
x5
(
x10
x6
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
⟶
x1
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
⟶
x1
(
x11
(
x10
(
x9
(
x9
x5
)
)
x7
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
)
(
x12
x6
(
x9
x4
)
)
⟶
not
(
x13
(
x9
(
x8
x5
)
)
)
⟶
not
(
x15
(
x12
(
x8
x5
)
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x15
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x9
x24
)
)
)
)
⟶
x13
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
x13
(
x8
(
x9
(
x9
x4
)
)
)
⟶
x19
(
x12
x7
x5
)
⟶
x19
(
x11
(
x10
x7
(
x9
(
x8
x5
)
)
)
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
⟶
x21
(
x10
(
x10
(
x9
x5
)
(
x9
(
x9
x5
)
)
)
(
x10
x4
(
x9
x6
)
)
)
⟶
x21
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x5
(
x9
(
x8
x5
)
)
)
)
⟶
x22
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
⟶
x21
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x0
x24
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x0
x24
(
x9
x4
)
)
⟶
x0
x24
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
)
⟶
not
(
x17
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
)
⟶
x22
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
⟶
not
(
x0
x4
x4
)
(proof)
Theorem
46a3e..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
x0
x6
x7
⟶
(
∀ x24 x25 x26 .
x0
x26
x24
⟶
not
(
x0
x26
x25
)
⟶
x0
x26
(
x12
x24
x25
)
)
⟶
(
∀ x24 x25 .
not
(
x0
x25
(
x9
x24
)
)
⟶
not
(
x25
=
x24
)
)
⟶
(
∀ x24 .
not
(
x13
(
x9
x24
)
)
)
⟶
(
∀ x24 x25 x26 .
x1
x26
(
x10
x24
x25
)
⟶
∀ x27 .
not
(
x0
x27
x26
)
⟶
x1
x26
(
x10
(
x12
x24
(
x9
x27
)
)
x25
)
)
⟶
(
∀ x24 x25 x26 .
x1
x26
(
x10
x24
x25
)
⟶
∀ x27 .
x0
x27
x24
⟶
not
(
x0
x27
x26
)
⟶
x15
x26
⟶
x15
(
x10
(
x12
x24
(
x9
x27
)
)
x25
)
)
⟶
not
(
x0
x3
(
x9
x5
)
)
⟶
x1
x4
(
x12
x6
(
x9
x4
)
)
⟶
not
(
x0
x5
(
x8
(
x9
x4
)
)
)
⟶
not
(
x1
x5
(
x9
x5
)
)
⟶
not
(
x3
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x1
(
x12
(
x8
x5
)
x5
)
x5
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x8
(
x9
x4
)
)
)
⟶
not
(
x0
(
x8
x5
)
x6
)
⟶
not
(
x9
x5
=
x6
)
⟶
x0
(
x9
(
x9
x4
)
)
(
x12
(
x8
(
x8
(
x9
x4
)
)
)
(
x9
(
x8
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x9
x4
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
⟶
x0
(
x8
(
x9
x4
)
)
(
x10
x6
(
x9
(
x8
(
x9
x4
)
)
)
)
⟶
not
(
x0
(
x12
x6
(
x9
x4
)
)
(
x9
(
x9
x5
)
)
)
⟶
not
(
x0
x6
(
x8
(
x9
x5
)
)
)
⟶
x0
x3
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
⟶
not
(
x0
(
x9
x4
)
x7
)
⟶
x0
(
x9
x5
)
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
⟶
not
(
x0
x5
(
x10
x4
(
x9
x6
)
)
)
⟶
not
(
x0
(
x9
x4
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
x0
x5
(
x10
(
x9
(
x9
x5
)
)
x7
)
⟶
not
(
x0
(
x9
x4
)
(
x9
(
x8
x5
)
)
)
⟶
x0
(
x8
x5
)
(
x9
(
x8
x5
)
)
⟶
x0
x4
(
x10
(
x9
x4
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x2
x5
(
x10
(
x9
x6
)
(
x9
(
x8
x5
)
)
)
⟶
x0
x5
(
x10
x7
(
x9
(
x8
x5
)
)
)
⟶
x0
x6
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
x5
)
⟶
or
(
x24
=
x5
)
(
x24
=
x6
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x24
=
x4
)
⟶
or
(
or
(
x24
=
x3
)
(
x24
=
x5
)
)
(
x24
=
x6
)
)
⟶
x1
x5
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
⟶
not
(
x1
(
x10
x7
(
x9
(
x8
x5
)
)
)
x7
)
⟶
not
(
x1
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
)
⟶
x1
x4
(
x12
x5
(
x9
x4
)
)
⟶
x1
(
x12
(
x12
(
x8
x5
)
x5
)
(
x9
x5
)
)
(
x9
(
x9
x4
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x9
x4
)
)
⟶
not
(
x24
=
x3
)
⟶
x0
x24
(
x12
(
x8
x5
)
x5
)
)
⟶
x12
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
x5
)
=
x8
(
x9
x4
)
⟶
x1
(
x12
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
(
x9
x3
)
)
(
x10
(
x9
(
x9
x4
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
⟶
x12
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
(
x9
(
x9
x4
)
)
=
x8
(
x9
(
x9
x4
)
)
⟶
x12
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
=
x8
(
x9
x4
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x8
(
x9
x5
)
)
)
⟶
not
(
x24
=
x4
)
⟶
x0
x24
(
x12
x7
x5
)
)
⟶
x1
(
x10
(
x9
x4
)
(
x9
x6
)
)
(
x12
(
x12
x7
(
x8
(
x9
x5
)
)
)
(
x9
x5
)
)
⟶
x1
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x9
x5
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x1
(
x10
(
x9
x4
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
⟶
x1
(
x8
(
x9
x5
)
)
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x0
x24
x6
⟶
not
(
x14
(
x12
x6
(
x9
x24
)
)
)
)
⟶
(
∀ x24 .
x0
x24
x7
⟶
not
(
x24
=
x5
)
⟶
not
(
x14
(
x12
(
x12
x7
(
x9
x5
)
)
(
x9
x24
)
)
)
)
⟶
not
(
x16
(
x10
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
)
⟶
(
∀ x24 .
x16
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
x24
)
)
⟶
not
(
x24
=
x9
(
x9
x4
)
)
)
⟶
not
(
x17
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
x7
)
)
⟶
x14
(
x10
x5
(
x9
(
x8
x5
)
)
)
⟶
x15
(
x10
x6
(
x9
(
x8
(
x9
x4
)
)
)
)
⟶
x16
(
x10
x7
(
x9
(
x8
x5
)
)
)
⟶
x19
(
x8
(
x9
x4
)
)
⟶
x20
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x20
(
x12
(
x10
x6
(
x9
(
x9
x5
)
)
)
(
x9
x5
)
)
⟶
x21
(
x10
x5
(
x10
(
x9
x6
)
(
x9
(
x8
x5
)
)
)
)
⟶
x21
(
x12
(
x10
(
x9
(
x9
x5
)
)
x7
)
(
x9
x6
)
)
⟶
x22
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
⟶
x23
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
x20
(
x12
(
x10
(
x9
(
x9
x5
)
)
x7
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
)
⟶
x1
(
x12
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x9
(
x9
x5
)
)
)
(
x12
x7
(
x9
x5
)
)
⟶
not
(
x15
(
x12
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x9
x3
)
)
)
⟶
not
(
x17
(
x11
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
)
)
⟶
x0
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
(proof)