I
n
[
]
:
=
F
i
n
d
E
q
u
a
t
i
o
n
a
l
P
r
o
o
f
[
a
·
b
b
·
a
,
F
o
r
A
l
l
[
{
a
,
b
,
c
}
,
(
(
a
·
b
)
·
c
)
·
(
a
·
(
(
a
·
c
)
·
a
)
)
c
]
]
I
n
[
]
:
=
C
o
u
n
t
s
F
i
r
s
t
/
@
K
e
y
s
N
o
r
m
a
l
P
r
o
o
f
O
b
j
e
c
t
L
o
g
i
c
:
E
q
u
a
t
i
o
n
a
l
L
o
g
i
c
S
t
e
p
s
:
1
0
2
T
h
e
o
r
e
m
:
a
·
b
b
·
a
[
"
P
r
o
o
f
D
a
t
a
s
e
t
"
]
O
u
t
[
]
=
A
x
i
o
m
1
,
H
y
p
o
t
h
e
s
i
s
1
,
C
r
i
t
i
c
a
l
P
a
i
r
L
e
m
m
a
5
2
,
S
u
b
s
t
i
t
u
t
i
o
n
L
e
m
m
a
4
7
,
C
o
n
c
l
u
s
i
o
n
1
