Certification Problem
Input (TPDB TRS_Standard/SK90/2.30)
The rewrite relation of the following TRS is considered.
not
(
x
)
→
xor
(
x
,
true
)
(1)
implies
(
x
,
y
)
→
xor
(
and
(
x
,
y
),
xor
(
x
,
true
))
(2)
or
(
x
,
y
)
→
xor
(
and
(
x
,
y
),
xor
(
x
,
y
))
(3)
=
(
x
,
y
)
→
xor
(
x
,
xor
(
y
,
true
))
(4)
Property / Task
Prove or disprove termination.
Answer / Result
Yes.
Proof (by NaTT @ termCOMP 2023)
1 Dependency Pair Transformation
The set of initial dependency pairs is empty, and hence the TRS is terminating.