YES Termination proof of rtL-cbn5.trs

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRSSemanticLabellingPOLOProof (⇔, 376 ms)
↳2 RelTRS
↳3 RelTRSSemanticLabellingPOLOProof (⇔, 227 ms)
↳4 RelTRS
↳5 RelTRSSemanticLabellingPOLOProof (⇔, 264 ms)
↳6 RelTRS
↳7 RelTRSRRRProof (⇔, 0 ms)
↳8 RelTRS
↳9 RIsEmptyProof (⇔, 0 ms)
↳10 YES

(0) Obligation:

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

top(ok(left(car(x, y), z))) → top(check(right(y, z)))
top(ok(right(x, car(y, z)))) → top(check(left(x, z)))
top(ok(left(bot, x))) → top(check(right(bot, x)))
top(ok(right(x, bot))) → top(check(left(x, bot)))

The relative TRS consists of the following S rules:

check(car(x, y)) → car(check(x), y)
check(right(x, y)) → right(x, check(y))
bot → car(new, bot)
check(old) → ok(old)
top(ok(left(car(x, y), z))) → top(check(left(y, z)))
car(x, ok(y)) → ok(car(x, y))
top(ok(right(x, car(y, z)))) → top(check(right(x, z)))
check(car(x, y)) → car(x, check(y))
check(right(x, y)) → right(check(x), y)
left(ok(x), y) → ok(left(x, y))
right(x, ok(y)) → ok(right(x, y))
check(left(x, y)) → left(x, check(y))
car(ok(x), y) → ok(car(x, y))
left(x, ok(y)) → ok(left(x, y))
right(ok(x), y) → ok(right(x, y))
check(left(x, y)) → left(check(x), y)

(1) 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:
check1: component 1: AND[x11]
car2: component 1: OR[x11, x21]
right2: component 1: AND[]
bot0: component 1: OR[]
new0: component 1: OR[]
old0: component 1: AND[]
ok1: component 1: AND[x11]
top1: component 1: OR[]
left2: component 1: OR[x11, x21]

Our labelling function was:
check1:component 1: XOR[]
car2:component 1: AND[-x11, -x21]
right2:component 1: AND[x11]
bot0:component 1: AND[]
new0:component 1: XOR[]
old0:component 1: AND[]
ok1:component 1: OR[-x11]
top1:component 1: XOR[x11]
left2:component 1: OR[-x11, -x21]


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


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

The following rules were deleted from R:

top(ok(right(x, car(y, z)))) → top(check(left(x, z)))

The following rules were deleted from S:
none


(2) Obligation:

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

top(ok(left(car(x, y), z))) → top(check(right(y, z)))
top(ok(left(bot, x))) → top(check(right(bot, x)))
top(ok(right(x, bot))) → top(check(left(x, bot)))

The relative TRS consists of the following S rules:

check(car(x, y)) → car(check(x), y)
check(right(x, y)) → right(x, check(y))
bot → car(new, bot)
check(old) → ok(old)
top(ok(left(car(x, y), z))) → top(check(left(y, z)))
car(x, ok(y)) → ok(car(x, y))
top(ok(right(x, car(y, z)))) → top(check(right(x, z)))
check(car(x, y)) → car(x, check(y))
check(right(x, y)) → right(check(x), y)
left(ok(x), y) → ok(left(x, y))
right(x, ok(y)) → ok(right(x, y))
check(left(x, y)) → left(x, check(y))
car(ok(x), y) → ok(car(x, y))
left(x, ok(y)) → ok(left(x, y))
right(ok(x), y) → ok(right(x, y))
check(left(x, y)) → left(check(x), y)

(3) 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:
check1: component 1: OR[x11]
car2: component 1: AND[x11, x21]
right2: component 1: AND[x11, x21]
bot0: component 1: AND[]
new0: component 1: AND[]
old0: component 1: OR[]
ok1: component 1: AND[x11]
top1: component 1: OR[]
left2: component 1: OR[]

Our labelling function was:
check1:component 1: OR[]
car2:component 1: AND[x11, x21]
right2:component 1: OR[-x11, -x21]
bot0:component 1: XOR[]
new0:component 1: XOR[]
old0:component 1: AND[]
ok1:component 1: AND[x11]
top1:component 1: OR[x11]
left2:component 1: XOR[-x11]


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


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

The following rules were deleted from R:

top(ok(left(car(x, y), z))) → top(check(right(y, z)))

The following rules were deleted from S:
none


(4) Obligation:

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

top(ok(left(bot, x))) → top(check(right(bot, x)))
top(ok(right(x, bot))) → top(check(left(x, bot)))

The relative TRS consists of the following S rules:

check(car(x, y)) → car(check(x), y)
check(right(x, y)) → right(x, check(y))
bot → car(new, bot)
check(old) → ok(old)
top(ok(left(car(x, y), z))) → top(check(left(y, z)))
car(x, ok(y)) → ok(car(x, y))
top(ok(right(x, car(y, z)))) → top(check(right(x, z)))
check(car(x, y)) → car(x, check(y))
check(right(x, y)) → right(check(x), y)
left(ok(x), y) → ok(left(x, y))
right(x, ok(y)) → ok(right(x, y))
check(left(x, y)) → left(x, check(y))
car(ok(x), y) → ok(car(x, y))
left(x, ok(y)) → ok(left(x, y))
right(ok(x), y) → ok(right(x, y))
check(left(x, y)) → left(check(x), y)

(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:
check1: component 1: OR[x11]
car2: component 1: OR[x11, x21]
right2: component 1: AND[]
bot0: component 1: OR[]
new0: component 1: OR[]
old0: component 1: AND[]
ok1: component 1: AND[]
top1: component 1: OR[]
left2: component 1: OR[x11, x21]

Our labelling function was:
check1:component 1: XOR[x11]
car2:component 1: OR[x11]
right2:component 1: XOR[-x11]
bot0:component 1: XOR[]
new0:component 1: XOR[]
old0:component 1: AND[]
ok1:component 1: AND[x11]
top1:component 1: OR[-x11]
left2:component 1: AND[x11, x21]


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


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

The following rules were deleted from R:

top(ok(right(x, bot))) → top(check(left(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(left(bot, x))) → top(check(right(bot, x)))

The relative TRS consists of the following S rules:

check(car(x, y)) → car(check(x), y)
check(right(x, y)) → right(x, check(y))
bot → car(new, bot)
check(old) → ok(old)
top(ok(left(car(x, y), z))) → top(check(left(y, z)))
car(x, ok(y)) → ok(car(x, y))
top(ok(right(x, car(y, z)))) → top(check(right(x, z)))
check(car(x, y)) → car(x, check(y))
check(right(x, y)) → right(check(x), y)
left(ok(x), y) → ok(left(x, y))
right(x, ok(y)) → ok(right(x, y))
check(left(x, y)) → left(x, check(y))
car(ok(x), y) → ok(car(x, y))
left(x, ok(y)) → ok(left(x, y))
right(ok(x), y) → ok(right(x, y))
check(left(x, y)) → left(check(x), y)

(7) RelTRSRRRProof (EQUIVALENT transformation)

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

POL(bot) = 0   
POL(car(x1, x2)) = x1 + x2   
POL(check(x1)) = x1   
POL(left(x1, x2)) = 1 + x1 + x2   
POL(new) = 0   
POL(ok(x1)) = x1   
POL(old) = 0   
POL(right(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(left(bot, x))) → top(check(right(bot, x)))
Rules from S:
none


(8) Obligation:

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

check(car(x, y)) → car(check(x), y)
check(right(x, y)) → right(x, check(y))
bot → car(new, bot)
check(old) → ok(old)
top(ok(left(car(x, y), z))) → top(check(left(y, z)))
car(x, ok(y)) → ok(car(x, y))
top(ok(right(x, car(y, z)))) → top(check(right(x, z)))
check(car(x, y)) → car(x, check(y))
check(right(x, y)) → right(check(x), y)
left(ok(x), y) → ok(left(x, y))
right(x, ok(y)) → ok(right(x, y))
check(left(x, y)) → left(x, check(y))
car(ok(x), y) → ok(car(x, y))
left(x, ok(y)) → ok(left(x, y))
right(ok(x), y) → ok(right(x, y))
check(left(x, y)) → left(check(x), y)

(9) RIsEmptyProof (EQUIVALENT transformation)

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

(10) YES