(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
ackin(s(X), s(Y)) → u21(ackin(s(X), Y), X)
u21(ackout(X), Y) → u22(ackin(Y, X))
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Combined order from the following AFS and order.
ackin(
x1,
x2) =
ackin(
x1,
x2)
s(
x1) =
s(
x1)
u21(
x1,
x2) =
u21(
x1,
x2)
ackout(
x1) =
ackout(
x1)
u22(
x1) =
x1
Recursive path order with status [RPO].
Quasi-Precedence:
ackout1 > [ackin2, u212] > s1
Status:
ackin2: [1,2]
s1: multiset
u212: [2,1]
ackout1: [1]
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
ackin(s(X), s(Y)) → u21(ackin(s(X), Y), X)
u21(ackout(X), Y) → u22(ackin(Y, X))
(2) Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.
(3) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(4) YES