YES Termination proof of rtL-pwl.trs

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRSRRRProof (⇔, 0 ms)
↳2 RelTRS
↳3 RelTRSRRRProof (⇔, 0 ms)
↳4 RelTRS
↳5 RelTRSSemanticLabellingPOLOProof (⇔, 69 ms)
↳6 RelTRS
↳7 RelTRSSemanticLabellingPOLOProof (⇔, 36 ms)
↳8 RelTRS
↳9 RelTRSSemanticLabellingPOLOProof (⇔, 35 ms)
↳10 RelTRS
↳11 RIsEmptyProof (⇔, 0 ms)
↳12 YES

(0) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

top(ok(queue(old(x), bot))) → top(check(queue(x, bot)))
top(ok(queue(new(x), bot))) → top(check(queue(x, bot)))
top(ok(queue(bot, old(x)))) → top(check(queue(bot, x)))
top(ok(queue(bot, new(x)))) → top(check(queue(bot, x)))
top(ok(queue(old(x), old(y)))) → top(check(queue(x, y)))
top(ok(queue(old(x), new(y)))) → top(check(queue(x, y)))
top(ok(queue(new(x), old(y)))) → top(check(queue(x, y)))
top(ok(queue(new(x), new(y)))) → top(check(queue(x, y)))

The relative TRS consists of the following S rules:

top(ok(queue(new(x), y))) → top(check(queue(x, y)))
check(old(x)) → ok(old(x))
bot → new(bot)
check(queue(x, y)) → queue(check(x), y)
queue(x, ok(y)) → ok(queue(x, y))
check(new(x)) → new(check(x))
queue(ok(x), y) → ok(queue(x, y))
top(ok(queue(old(x), y))) → top(check(queue(x, y)))
old(ok(x)) → ok(old(x))
check(queue(x, y)) → queue(x, check(y))
new(ok(x)) → ok(new(x))

(1) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(bot) = 0   
POL(check(x1)) = x1   
POL(new(x1)) = x1   
POL(ok(x1)) = x1   
POL(old(x1)) = 1 + x1   
POL(queue(x1, x2)) = x1 + x2   
POL(top(x1)) = x1   
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

top(ok(queue(old(x), bot))) → top(check(queue(x, bot)))
top(ok(queue(bot, old(x)))) → top(check(queue(bot, x)))
top(ok(queue(old(x), old(y)))) → top(check(queue(x, y)))
top(ok(queue(old(x), new(y)))) → top(check(queue(x, y)))
top(ok(queue(new(x), old(y)))) → top(check(queue(x, y)))
Rules from S:

top(ok(queue(old(x), y))) → top(check(queue(x, y)))


(2) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

top(ok(queue(new(x), bot))) → top(check(queue(x, bot)))
top(ok(queue(bot, new(x)))) → top(check(queue(bot, x)))
top(ok(queue(new(x), new(y)))) → top(check(queue(x, y)))

The relative TRS consists of the following S rules:

top(ok(queue(new(x), y))) → top(check(queue(x, y)))
check(old(x)) → ok(old(x))
bot → new(bot)
check(queue(x, y)) → queue(check(x), y)
queue(x, ok(y)) → ok(queue(x, y))
check(new(x)) → new(check(x))
queue(ok(x), y) → ok(queue(x, y))
old(ok(x)) → ok(old(x))
check(queue(x, y)) → queue(x, check(y))
new(ok(x)) → ok(new(x))

(3) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(top(x1)) =
/0\
\0/
 +
/11\
\00/
·x1

POL(ok(x1)) =
/0\
\1/
 +
/10\
\01/
·x1

POL(queue(x1, x2)) =
/0\
\0/
 +
/10\
\11/
·x1 +
/10\
\11/
·x2

POL(new(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(bot) =
/0\
\1/

POL(check(x1)) =
/0\
\1/
 +
/10\
\01/
·x1

POL(old(x1)) =
/1\
\0/
 +
/11\
\11/
·x1
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
none
Rules from S:

old(ok(x)) → ok(old(x))


(4) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

top(ok(queue(new(x), bot))) → top(check(queue(x, bot)))
top(ok(queue(bot, new(x)))) → top(check(queue(bot, x)))
top(ok(queue(new(x), new(y)))) → top(check(queue(x, y)))

The relative TRS consists of the following S rules:

top(ok(queue(new(x), y))) → top(check(queue(x, y)))
check(old(x)) → ok(old(x))
bot → new(bot)
check(queue(x, y)) → queue(check(x), y)
queue(x, ok(y)) → ok(queue(x, y))
check(new(x)) → new(check(x))
queue(ok(x), y) → ok(queue(x, y))
check(queue(x, y)) → queue(x, check(y))
new(ok(x)) → ok(new(x))

(5) RelTRSSemanticLabellingPOLOProof (EQUIVALENT transformation)

We use Semantic Labelling over tuples of bools combined with a polynomial order [SEMLAB]

We use semantic labelling over boolean tuples of size 1.

We used the following model:
top1: component 1: AND[]
ok1: component 1: OR[x11]
queue2: component 1: AND[x11, x21]
new1: component 1: AND[x11]
check1: component 1: OR[x11]
old1: component 1: OR[]
bot0: component 1: AND[]

Our labelling function was:
top1:component 1: OR[]
ok1:component 1: AND[x11]
queue2:component 1: OR[-x11, -x21]
new1:component 1: AND[x11]
check1:component 1: OR[]
old1:component 1: OR[]
bot0:component 1: AND[]


Our labelled system was:
[t]top[f]([f]ok[f]([f]queue[t]([f]new[f]([f]x), [f]y))) → [t]top[f]([f]check[f]([f]queue[t]([f]x, [f]y)))
[t]top[f]([f]ok[f]([f]queue[t]([t]new[t]([t]x), [f]y))) → [t]top[f]([f]check[f]([f]queue[t]([t]x, [f]y)))
[t]top[f]([t]ok[t]([t]queue[f]([t]new[t]([t]x), [t]y))) → [t]top[f]([t]check[f]([t]queue[f]([t]x, [t]y)))
[f]check[f]([f]old[f]([f]x)) → [f]ok[f]([f]old[f]([f]x))
[t]bot[t] → [t]new[t]([t]bot[t])
[f]check[f]([f]queue[t]([f]x, [f]y)) → [f]queue[t]([f]check[f]([f]x), [f]y)
[f]check[f]([f]queue[t]([t]x, [f]y)) → [f]queue[t]([t]check[f]([t]x), [f]y)
[t]check[f]([t]queue[f]([t]x, [t]y)) → [t]queue[f]([t]check[f]([t]x), [t]y)
[f]queue[t]([f]x, [f]ok[f]([f]y)) → [f]ok[f]([f]queue[t]([f]x, [f]y))
[f]queue[t]([f]x, [t]ok[t]([t]y)) → [f]ok[f]([f]queue[t]([f]x, [t]y))
[t]queue[f]([t]x, [t]ok[t]([t]y)) → [t]ok[t]([t]queue[f]([t]x, [t]y))
[f]check[f]([f]new[f]([f]x)) → [f]new[f]([f]check[f]([f]x))
[t]check[f]([t]new[t]([t]x)) → [t]new[t]([t]check[f]([t]x))
[f]queue[t]([f]ok[f]([f]x), [f]y) → [f]ok[f]([f]queue[t]([f]x, [f]y))
[f]queue[t]([t]ok[t]([t]x), [f]y) → [f]ok[f]([f]queue[t]([t]x, [f]y))
[t]queue[f]([t]ok[t]([t]x), [t]y) → [t]ok[t]([t]queue[f]([t]x, [t]y))
[f]check[f]([f]queue[t]([f]x, [f]y)) → [f]queue[t]([f]x, [f]check[f]([f]y))
[f]check[f]([f]queue[t]([f]x, [t]y)) → [f]queue[t]([f]x, [t]check[f]([t]y))
[t]check[f]([t]queue[f]([t]x, [t]y)) → [t]queue[f]([t]x, [t]check[f]([t]y))
[f]new[f]([f]ok[f]([f]x)) → [f]ok[f]([f]new[f]([f]x))
[t]new[t]([t]ok[t]([t]x)) → [t]ok[t]([t]new[t]([t]x))
[t]top[f]([f]ok[f]([f]queue[t]([f]new[f]([f]x), [t]bot[t]))) → [t]top[f]([f]check[f]([f]queue[t]([f]x, [t]bot[t])))
[t]top[f]([t]ok[t]([t]queue[f]([t]new[t]([t]x), [t]bot[t]))) → [t]top[f]([t]check[f]([t]queue[f]([t]x, [t]bot[t])))
[t]top[f]([f]ok[f]([f]queue[t]([t]bot[t], [f]new[f]([f]x)))) → [t]top[f]([f]check[f]([f]queue[t]([t]bot[t], [f]x)))
[t]top[f]([t]ok[t]([t]queue[f]([t]bot[t], [t]new[t]([t]x)))) → [t]top[f]([t]check[f]([t]queue[f]([t]bot[t], [t]x)))
[t]top[f]([f]ok[f]([f]queue[t]([f]new[f]([f]x), [f]new[f]([f]y)))) → [t]top[f]([f]check[f]([f]queue[t]([f]x, [f]y)))
[t]top[f]([f]ok[f]([f]queue[t]([f]new[f]([f]x), [t]new[t]([t]y)))) → [t]top[f]([f]check[f]([f]queue[t]([f]x, [t]y)))
[t]top[f]([f]ok[f]([f]queue[t]([t]new[t]([t]x), [f]new[f]([f]y)))) → [t]top[f]([f]check[f]([f]queue[t]([t]x, [f]y)))
[t]top[f]([t]ok[t]([t]queue[f]([t]new[t]([t]x), [t]new[t]([t]y)))) → [t]top[f]([t]check[f]([t]queue[f]([t]x, [t]y)))


Our polynomial interpretation was:
P(top[false])(x1) = 1 + 1·x1
P(top[true])(x1) = 0 + 1·x1
P(ok[false])(x1) = 0 + 1·x1
P(ok[true])(x1) = 1 + 1·x1
P(queue[false])(x1,x2) = 0 + 1·x1 + 1·x2
P(queue[true])(x1,x2) = 1 + 1·x1 + 1·x2
P(new[false])(x1) = 1 + 1·x1
P(new[true])(x1) = 0 + 1·x1
P(check[false])(x1) = 0 + 1·x1
P(check[true])(x1) = 0 + 1·x1
P(old[false])(x1) = 0 + 1·x1
P(old[true])(x1) = 0 + 1·x1
P(bot[false])() = 0
P(bot[true])() = 0

The following rules were deleted from R:

top(ok(queue(new(x), bot))) → top(check(queue(x, bot)))

The following rules were deleted from S:
none


(6) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

top(ok(queue(bot, new(x)))) → top(check(queue(bot, x)))
top(ok(queue(new(x), new(y)))) → top(check(queue(x, y)))

The relative TRS consists of the following S rules:

top(ok(queue(new(x), y))) → top(check(queue(x, y)))
check(old(x)) → ok(old(x))
bot → new(bot)
check(queue(x, y)) → queue(check(x), y)
queue(x, ok(y)) → ok(queue(x, y))
check(new(x)) → new(check(x))
queue(ok(x), y) → ok(queue(x, y))
check(queue(x, y)) → queue(x, check(y))
new(ok(x)) → ok(new(x))

(7) RelTRSSemanticLabellingPOLOProof (EQUIVALENT transformation)

We use Semantic Labelling over tuples of bools combined with a polynomial order [SEMLAB]

We use semantic labelling over boolean tuples of size 1.

We used the following model:
top1: component 1: OR[]
ok1: component 1: OR[]
queue2: component 1: AND[x11, x21]
new1: component 1: OR[x11]
check1: component 1: OR[x11]
old1: component 1: OR[]
bot0: component 1: AND[]

Our labelling function was:
top1:component 1: XOR[x11]
ok1:component 1: OR[x11]
queue2:component 1: XOR[x11, x21]
new1:component 1: AND[x11]
check1:component 1: OR[]
old1:component 1: OR[]
bot0:component 1: AND[]


Our labelled system was:
[f]top[f]([f]ok[f]([f]queue[f]([f]new[f]([f]x), [f]y))) → [f]top[f]([f]check[f]([f]queue[f]([f]x, [f]y)))
[f]top[f]([f]ok[f]([f]queue[t]([f]new[f]([f]x), [t]y))) → [f]top[f]([f]check[f]([f]queue[t]([f]x, [t]y)))
[f]top[f]([f]ok[f]([f]queue[t]([t]new[t]([t]x), [f]y))) → [f]top[f]([f]check[f]([f]queue[t]([t]x, [f]y)))
[f]top[f]([f]ok[t]([t]queue[f]([t]new[t]([t]x), [t]y))) → [f]top[t]([t]check[f]([t]queue[f]([t]x, [t]y)))
[f]check[f]([f]old[f]([f]x)) → [f]ok[f]([f]old[f]([f]x))
[t]bot[t] → [t]new[t]([t]bot[t])
[f]check[f]([f]queue[f]([f]x, [f]y)) → [f]queue[f]([f]check[f]([f]x), [f]y)
[f]check[f]([f]queue[t]([f]x, [t]y)) → [f]queue[t]([f]check[f]([f]x), [t]y)
[f]check[f]([f]queue[t]([t]x, [f]y)) → [f]queue[t]([t]check[f]([t]x), [f]y)
[t]check[f]([t]queue[f]([t]x, [t]y)) → [t]queue[f]([t]check[f]([t]x), [t]y)
[f]queue[f]([f]x, [f]ok[f]([f]y)) → [f]ok[f]([f]queue[f]([f]x, [f]y))
[f]queue[f]([f]x, [f]ok[t]([t]y)) → [f]ok[f]([f]queue[t]([f]x, [t]y))
[f]queue[t]([t]x, [f]ok[f]([f]y)) → [f]ok[f]([f]queue[t]([t]x, [f]y))
[f]queue[t]([t]x, [f]ok[t]([t]y)) → [f]ok[t]([t]queue[f]([t]x, [t]y))
[f]check[f]([f]new[f]([f]x)) → [f]new[f]([f]check[f]([f]x))
[t]check[f]([t]new[t]([t]x)) → [t]new[t]([t]check[f]([t]x))
[f]queue[f]([f]ok[f]([f]x), [f]y) → [f]ok[f]([f]queue[f]([f]x, [f]y))
[f]queue[t]([f]ok[f]([f]x), [t]y) → [f]ok[f]([f]queue[t]([f]x, [t]y))
[f]queue[f]([f]ok[t]([t]x), [f]y) → [f]ok[f]([f]queue[t]([t]x, [f]y))
[f]queue[t]([f]ok[t]([t]x), [t]y) → [f]ok[t]([t]queue[f]([t]x, [t]y))
[f]check[f]([f]queue[f]([f]x, [f]y)) → [f]queue[f]([f]x, [f]check[f]([f]y))
[f]check[f]([f]queue[t]([f]x, [t]y)) → [f]queue[t]([f]x, [t]check[f]([t]y))
[f]check[f]([f]queue[t]([t]x, [f]y)) → [f]queue[t]([t]x, [f]check[f]([f]y))
[t]check[f]([t]queue[f]([t]x, [t]y)) → [t]queue[f]([t]x, [t]check[f]([t]y))
[f]new[f]([f]ok[f]([f]x)) → [f]ok[f]([f]new[f]([f]x))
[f]new[f]([f]ok[t]([t]x)) → [f]ok[t]([t]new[t]([t]x))
[f]top[f]([f]ok[f]([f]queue[t]([t]bot[t], [f]new[f]([f]x)))) → [f]top[f]([f]check[f]([f]queue[t]([t]bot[t], [f]x)))
[f]top[f]([f]ok[t]([t]queue[f]([t]bot[t], [t]new[t]([t]x)))) → [f]top[t]([t]check[f]([t]queue[f]([t]bot[t], [t]x)))
[f]top[f]([f]ok[f]([f]queue[f]([f]new[f]([f]x), [f]new[f]([f]y)))) → [f]top[f]([f]check[f]([f]queue[f]([f]x, [f]y)))
[f]top[f]([f]ok[f]([f]queue[t]([f]new[f]([f]x), [t]new[t]([t]y)))) → [f]top[f]([f]check[f]([f]queue[t]([f]x, [t]y)))
[f]top[f]([f]ok[f]([f]queue[t]([t]new[t]([t]x), [f]new[f]([f]y)))) → [f]top[f]([f]check[f]([f]queue[t]([t]x, [f]y)))
[f]top[f]([f]ok[t]([t]queue[f]([t]new[t]([t]x), [t]new[t]([t]y)))) → [f]top[t]([t]check[f]([t]queue[f]([t]x, [t]y)))


Our polynomial interpretation was:
P(top[false])(x1) = 1 + 1·x1
P(top[true])(x1) = 1 + 1·x1
P(ok[false])(x1) = 0 + 1·x1
P(ok[true])(x1) = 1 + 1·x1
P(queue[false])(x1,x2) = 0 + 1·x1 + 1·x2
P(queue[true])(x1,x2) = 0 + 1·x1 + 1·x2
P(new[false])(x1) = 1 + 1·x1
P(new[true])(x1) = 0 + 1·x1
P(check[false])(x1) = 0 + 1·x1
P(check[true])(x1) = 1 + 1·x1
P(old[false])(x1) = 0 + 1·x1
P(old[true])(x1) = 0 + 1·x1
P(bot[false])() = 0
P(bot[true])() = 0

The following rules were deleted from R:

top(ok(queue(bot, new(x)))) → top(check(queue(bot, x)))

The following rules were deleted from S:
none


(8) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

top(ok(queue(new(x), new(y)))) → top(check(queue(x, y)))

The relative TRS consists of the following S rules:

top(ok(queue(new(x), y))) → top(check(queue(x, y)))
check(old(x)) → ok(old(x))
bot → new(bot)
check(queue(x, y)) → queue(check(x), y)
queue(x, ok(y)) → ok(queue(x, y))
check(new(x)) → new(check(x))
queue(ok(x), y) → ok(queue(x, y))
check(queue(x, y)) → queue(x, check(y))
new(ok(x)) → ok(new(x))

(9) RelTRSSemanticLabellingPOLOProof (EQUIVALENT transformation)

We use Semantic Labelling over tuples of bools combined with a polynomial order [SEMLAB]

We use semantic labelling over boolean tuples of size 1.

We used the following model:
top1: component 1: OR[x11]
ok1: component 1: OR[x11]
queue2: component 1: OR[x11, x21]
new1: component 1: OR[x11]
check1: component 1: AND[x11]
old1: component 1: AND[]
bot0: component 1: OR[]

Our labelling function was:
top1:component 1: OR[-x11]
ok1:component 1: AND[x11]
queue2:component 1: XOR[x11, x21]
new1:component 1: OR[-x11]
check1:component 1: AND[]
old1:component 1: OR[-x11]
bot0:component 1: AND[]


Our labelled system was:
[f]top[t]([f]ok[f]([f]queue[f]([f]new[t]([f]x), [f]y))) → [f]top[t]([f]check[t]([f]queue[f]([f]x, [f]y)))
[t]top[f]([t]ok[t]([t]queue[t]([f]new[t]([f]x), [t]y))) → [t]top[f]([t]check[t]([t]queue[t]([f]x, [t]y)))
[t]top[f]([t]ok[t]([t]queue[t]([t]new[f]([t]x), [f]y))) → [t]top[f]([t]check[t]([t]queue[t]([t]x, [f]y)))
[t]top[f]([t]ok[t]([t]queue[f]([t]new[f]([t]x), [t]y))) → [t]top[f]([t]check[t]([t]queue[f]([t]x, [t]y)))
[t]check[t]([t]old[t]([f]x)) → [t]ok[t]([t]old[t]([f]x))
[t]check[t]([t]old[f]([t]x)) → [t]ok[t]([t]old[f]([t]x))
[f]bot[t] → [f]new[t]([f]bot[t])
[f]check[t]([f]queue[f]([f]x, [f]y)) → [f]queue[f]([f]check[t]([f]x), [f]y)
[t]check[t]([t]queue[t]([f]x, [t]y)) → [t]queue[t]([f]check[t]([f]x), [t]y)
[t]check[t]([t]queue[t]([t]x, [f]y)) → [t]queue[t]([t]check[t]([t]x), [f]y)
[t]check[t]([t]queue[f]([t]x, [t]y)) → [t]queue[f]([t]check[t]([t]x), [t]y)
[f]queue[f]([f]x, [f]ok[f]([f]y)) → [f]ok[f]([f]queue[f]([f]x, [f]y))
[t]queue[t]([f]x, [t]ok[t]([t]y)) → [t]ok[t]([t]queue[t]([f]x, [t]y))
[t]queue[t]([t]x, [f]ok[f]([f]y)) → [t]ok[t]([t]queue[t]([t]x, [f]y))
[t]queue[f]([t]x, [t]ok[t]([t]y)) → [t]ok[t]([t]queue[f]([t]x, [t]y))
[f]check[t]([f]new[t]([f]x)) → [f]new[t]([f]check[t]([f]x))
[t]check[t]([t]new[f]([t]x)) → [t]new[f]([t]check[t]([t]x))
[f]queue[f]([f]ok[f]([f]x), [f]y) → [f]ok[f]([f]queue[f]([f]x, [f]y))
[t]queue[t]([f]ok[f]([f]x), [t]y) → [t]ok[t]([t]queue[t]([f]x, [t]y))
[t]queue[t]([t]ok[t]([t]x), [f]y) → [t]ok[t]([t]queue[t]([t]x, [f]y))
[t]queue[f]([t]ok[t]([t]x), [t]y) → [t]ok[t]([t]queue[f]([t]x, [t]y))
[f]check[t]([f]queue[f]([f]x, [f]y)) → [f]queue[f]([f]x, [f]check[t]([f]y))
[t]check[t]([t]queue[t]([f]x, [t]y)) → [t]queue[t]([f]x, [t]check[t]([t]y))
[t]check[t]([t]queue[t]([t]x, [f]y)) → [t]queue[t]([t]x, [f]check[t]([f]y))
[t]check[t]([t]queue[f]([t]x, [t]y)) → [t]queue[f]([t]x, [t]check[t]([t]y))
[f]new[t]([f]ok[f]([f]x)) → [f]ok[f]([f]new[t]([f]x))
[t]new[f]([t]ok[t]([t]x)) → [t]ok[t]([t]new[f]([t]x))
[f]top[t]([f]ok[f]([f]queue[f]([f]new[t]([f]x), [f]new[t]([f]y)))) → [f]top[t]([f]check[t]([f]queue[f]([f]x, [f]y)))
[t]top[f]([t]ok[t]([t]queue[t]([f]new[t]([f]x), [t]new[f]([t]y)))) → [t]top[f]([t]check[t]([t]queue[t]([f]x, [t]y)))
[t]top[f]([t]ok[t]([t]queue[t]([t]new[f]([t]x), [f]new[t]([f]y)))) → [t]top[f]([t]check[t]([t]queue[t]([t]x, [f]y)))
[t]top[f]([t]ok[t]([t]queue[f]([t]new[f]([t]x), [t]new[f]([t]y)))) → [t]top[f]([t]check[t]([t]queue[f]([t]x, [t]y)))


Our polynomial interpretation was:
P(top[false])(x1) = 1 + 1·x1
P(top[true])(x1) = 1 + 1·x1
P(ok[false])(x1) = 1 + 1·x1
P(ok[true])(x1) = 0 + 1·x1
P(queue[false])(x1,x2) = 1 + 1·x1 + 1·x2
P(queue[true])(x1,x2) = 0 + 1·x1 + 1·x2
P(new[false])(x1) = 1 + 1·x1
P(new[true])(x1) = 0 + 1·x1
P(check[false])(x1) = 1 + 1·x1
P(check[true])(x1) = 0 + 1·x1
P(old[false])(x1) = 0 + 1·x1
P(old[true])(x1) = 1 + 1·x1
P(bot[false])() = 0
P(bot[true])() = 0

The following rules were deleted from R:

top(ok(queue(new(x), new(y)))) → top(check(queue(x, y)))

The following rules were deleted from S:
none


(10) Obligation:

Relative term rewrite system:
R is empty.
The relative TRS consists of the following S rules:

top(ok(queue(new(x), y))) → top(check(queue(x, y)))
check(old(x)) → ok(old(x))
bot → new(bot)
check(queue(x, y)) → queue(check(x), y)
queue(x, ok(y)) → ok(queue(x, y))
check(new(x)) → new(check(x))
queue(ok(x), y) → ok(queue(x, y))
check(queue(x, y)) → queue(x, check(y))
new(ok(x)) → ok(new(x))

(11) RIsEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(12) YES