(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
top(ok(new(x))) → top(check(x))
top(ok(old(x))) → top(check(x))
The relative TRS consists of the following S rules:
check(old(x)) → ok(old(x))
bot → new(bot)
check(old(x)) → old(check(x))
check(new(x)) → new(check(x))
old(ok(x)) → ok(old(x))
new(ok(x)) → ok(new(x))
(1) RelTRS Reverse (SOUND transformation)
We have reversed the following relative TRS [REVERSE]:
The set of rules R is
top(ok(new(x))) → top(check(x))
top(ok(old(x))) → top(check(x))
The set of rules S is
check(old(x)) → ok(old(x))
bot → new(bot)
check(old(x)) → old(check(x))
check(new(x)) → new(check(x))
old(ok(x)) → ok(old(x))
new(ok(x)) → ok(new(x))
We have obtained the following relative TRS:
The set of rules R is
new(ok(top(x))) → check(top(x))
old(ok(top(x))) → check(top(x))
The set of rules S is
old(check(x)) → old(ok(x))
bot'(x) → bot'(new(x))
old(check(x)) → check(old(x))
new(check(x)) → check(new(x))
ok(old(x)) → old(ok(x))
ok(new(x)) → new(ok(x))
(2) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
new(ok(top(x))) → check(top(x))
old(ok(top(x))) → check(top(x))
The relative TRS consists of the following S rules:
old(check(x)) → old(ok(x))
bot'(x) → bot'(new(x))
old(check(x)) → check(old(x))
new(check(x)) → check(new(x))
ok(old(x)) → old(ok(x))
ok(new(x)) → new(ok(x))
(3) RelTRSRRRProof (EQUIVALENT transformation)
We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:
POL(bot'(x1)) = x1
POL(check(x1)) = x1
POL(new(x1)) = x1
POL(ok(x1)) = x1
POL(old(x1)) = 1 + x1
POL(top(x1)) = x1
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
old(ok(top(x))) → check(top(x))
Rules from S:
none
(4) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
new(ok(top(x))) → check(top(x))
The relative TRS consists of the following S rules:
old(check(x)) → old(ok(x))
bot'(x) → bot'(new(x))
old(check(x)) → check(old(x))
new(check(x)) → check(new(x))
ok(old(x)) → old(ok(x))
ok(new(x)) → new(ok(x))
(5) RelTRSRRRProof (EQUIVALENT transformation)
We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
new(ok(top(x))) → check(top(x))
Rules from S:
old(check(x)) → old(ok(x))
(6) Obligation:
Relative term rewrite system:
R is empty.
The relative TRS consists of the following S rules:
bot'(x) → bot'(new(x))
old(check(x)) → check(old(x))
new(check(x)) → check(new(x))
ok(old(x)) → old(ok(x))
ok(new(x)) → new(ok(x))
(7) RIsEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(8) YES