Termination proof of rtL-cbn1.trs

Termination of the given RelTRS could be proven:

0 RelTRS

↳1 RelTRSRRRProof (⇔, 53 ms)

↳2 RelTRS

↳3 RelTRSRRRProof (⇔, 42 ms)

↳4 RelTRS

↳5 RelTRSRRRProof (⇔, 0 ms)

↳6 RelTRS

↳7 RelTRSSemanticLabellingPOLOProof (⇔, 216 ms)

↳8 RelTRS

↳9 RelTRSSemanticLabellingPOLOProof (⇔, 106 ms)

↳10 RelTRS

↳11 RelTRSSemanticLabellingPOLOProof (⇔, 71 ms)

↳12 RelTRS

↳13 RelTRSRRRProof (⇔, 0 ms)

↳14 RelTRS

↳15 RelTRSSemanticLabellingPOLOProof (⇔, 42 ms)

↳16 RelTRS

↳17 RelTRSSemanticLabellingPOLOProof (⇔, 52 ms)

↳18 RelTRS

↳19 RelTRSRRRProof (⇔, 0 ms)

↳20 RelTRS

↳21 RIsEmptyProof (⇔, 0 ms)

↳22 YES

(0) Obligation:

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

Tl(O(x), y) → Wr(check(x), y)
Tl(O(x), y) → Wr(x, check(y))
Tl(N(x), y) → Wr(check(x), y)
Tl(N(x), y) → Wr(x, check(y))
Tr(x, O(y)) → Wl(check(x), y)
Tr(x, O(y)) → Wl(x, check(y))
Tr(x, N(y)) → Wl(check(x), y)
Tr(x, N(y)) → Wl(x, check(y))
Tl(B, y) → Wr(check(B), y)
Tl(B, y) → Wr(B, check(y))
Tr(x, B) → Wl(check(x), B)
Tr(x, B) → Wl(x, check(B))

The relative TRS consists of the following S rules:

Tl(N(x), y) → Wl(x, check(y))
Tr(x, N(y)) → Wr(x, check(y))
Wr(ok(x), y) → Tr(x, y)
O(ok(x)) → ok(O(x))
Wl(x, ok(y)) → Tl(x, y)
Tl(N(x), y) → Wl(check(x), y)
Tr(x, O(y)) → Wr(x, check(y))
Tr(x, N(y)) → Wr(check(x), y)
check(N(x)) → N(check(x))
B → N(B)
Tl(O(x), y) → Wl(check(x), y)
Tr(x, O(y)) → Wr(check(x), y)
Tl(O(x), y) → Wl(x, check(y))
check(O(x)) → O(check(x))
N(ok(x)) → ok(N(x))
Wl(ok(x), y) → Tl(x, y)
Wr(x, ok(y)) → Tr(x, y)
check(O(x)) → ok(O(x))

(1) RelTRSRRRProof (EQUIVALENT transformation)

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

POL(B) = 0
POL(N(x₁)) = x₁
POL(O(x₁)) = 1 + x₁
POL(Tl(x₁, x₂)) = x₁ + x₂
POL(Tr(x₁, x₂)) = x₁ + x₂
POL(Wl(x₁, x₂)) = x₁ + x₂
POL(Wr(x₁, x₂)) = x₁ + x₂
POL(check(x₁)) = x₁
POL(ok(x₁)) = x₁

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

Tl(O(x), y) → Wr(check(x), y)
Tl(O(x), y) → Wr(x, check(y))
Tr(x, O(y)) → Wl(check(x), y)
Tr(x, O(y)) → Wl(x, check(y))

Rules from S:

Tr(x, O(y)) → Wr(x, check(y))
Tl(O(x), y) → Wl(check(x), y)
Tr(x, O(y)) → Wr(check(x), y)
Tl(O(x), y) → Wl(x, check(y))

(2) Obligation:

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

Tl(N(x), y) → Wr(check(x), y)
Tl(N(x), y) → Wr(x, check(y))
Tr(x, N(y)) → Wl(check(x), y)
Tr(x, N(y)) → Wl(x, check(y))
Tl(B, y) → Wr(check(B), y)
Tl(B, y) → Wr(B, check(y))
Tr(x, B) → Wl(check(x), B)
Tr(x, B) → Wl(x, check(B))

The relative TRS consists of the following S rules:

Tl(N(x), y) → Wl(x, check(y))
Tr(x, N(y)) → Wr(x, check(y))
Wr(ok(x), y) → Tr(x, y)
O(ok(x)) → ok(O(x))
Wl(x, ok(y)) → Tl(x, y)
Tl(N(x), y) → Wl(check(x), y)
Tr(x, N(y)) → Wr(check(x), y)
check(N(x)) → N(check(x))
B → N(B)
check(O(x)) → O(check(x))
N(ok(x)) → ok(N(x))
Wl(ok(x), y) → Tl(x, y)
Wr(x, ok(y)) → Tr(x, y)
check(O(x)) → ok(O(x))

(3) RelTRSRRRProof (EQUIVALENT transformation)

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

POL(Tl(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(N(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(Wr(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(check(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(Tr(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(Wl(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(B) =
/ 0 \

\ 1 /

POL(ok(x₁)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁

POL(O(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

Tr(x, B) → Wl(x, check(B))

Rules from S:
none

(4) Obligation:

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

Tl(N(x), y) → Wr(check(x), y)
Tl(N(x), y) → Wr(x, check(y))
Tr(x, N(y)) → Wl(check(x), y)
Tr(x, N(y)) → Wl(x, check(y))
Tl(B, y) → Wr(check(B), y)
Tl(B, y) → Wr(B, check(y))
Tr(x, B) → Wl(check(x), B)

The relative TRS consists of the following S rules:

Tl(N(x), y) → Wl(x, check(y))
Tr(x, N(y)) → Wr(x, check(y))
Wr(ok(x), y) → Tr(x, y)
O(ok(x)) → ok(O(x))
Wl(x, ok(y)) → Tl(x, y)
Tl(N(x), y) → Wl(check(x), y)
Tr(x, N(y)) → Wr(check(x), y)
check(N(x)) → N(check(x))
B → N(B)
check(O(x)) → O(check(x))
N(ok(x)) → ok(N(x))
Wl(ok(x), y) → Tl(x, y)
Wr(x, ok(y)) → Tr(x, y)
check(O(x)) → ok(O(x))

(5) RelTRSRRRProof (EQUIVALENT transformation)

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

POL(Tl(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 0 0 /

· x₂

POL(N(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(Wr(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 0 0 /

· x₂

POL(check(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(Tr(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 0 0 /

· x₂

POL(Wl(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 0 0 /

· x₂

POL(B) =
/ 0 \

\ 1 /

POL(ok(x₁)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁

POL(O(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

Tl(B, y) → Wr(check(B), y)

Rules from S:
none

(6) Obligation:

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

Tl(N(x), y) → Wr(check(x), y)
Tl(N(x), y) → Wr(x, check(y))
Tr(x, N(y)) → Wl(check(x), y)
Tr(x, N(y)) → Wl(x, check(y))
Tl(B, y) → Wr(B, check(y))
Tr(x, B) → Wl(check(x), B)

The relative TRS consists of the following S rules:

Tl(N(x), y) → Wl(x, check(y))
Tr(x, N(y)) → Wr(x, check(y))
Wr(ok(x), y) → Tr(x, y)
O(ok(x)) → ok(O(x))
Wl(x, ok(y)) → Tl(x, y)
Tl(N(x), y) → Wl(check(x), y)
Tr(x, N(y)) → Wr(check(x), y)
check(N(x)) → N(check(x))
B → N(B)
check(O(x)) → O(check(x))
N(ok(x)) → ok(N(x))
Wl(ok(x), y) → Tl(x, y)
Wr(x, ok(y)) → Tr(x, y)
check(O(x)) → ok(O(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:
Tl₂: component 1: OR[]
N₁: component 1: OR[x₁¹]
Wl₂: component 1: OR[]
check₁: component 1: OR[x₁¹]
Tr₂: component 1: OR[]
Wr₂: component 1: OR[]
ok₁: component 1: OR[x₁¹]
O₁: component 1: AND[]
B₀: component 1: OR[]

Our labelling function was:
Tl₂:component 1: XOR[x₁¹]
N₁:component 1: XOR[-x₁¹]
Wl₂:component 1: AND[-x₁¹]
check₁:component 1: OR[]
Tr₂:component 1: AND[-x₁¹, -x₂¹]
Wr₂:component 1: AND[x₁¹]
ok₁:component 1: XOR[x₁¹]
O₁:component 1: AND[]
B₀:component 1: AND[]

Our labelled system was:
^[f]Tl^[f](^[f]N^[t](^[f]x), ^[f]y) → ^[f]Wl^[t](^[f]x, ^[f]check^[f](^[f]y))
^[f]Tl^[f](^[f]N^[t](^[f]x), ^[t]y) → ^[f]Wl^[t](^[f]x, ^[t]check^[f](^[t]y))
^[f]Tl^[t](^[t]N^[f](^[t]x), ^[f]y) → ^[f]Wl^[f](^[t]x, ^[f]check^[f](^[f]y))
^[f]Tl^[t](^[t]N^[f](^[t]x), ^[t]y) → ^[f]Wl^[f](^[t]x, ^[t]check^[f](^[t]y))
^[f]Tr^[t](^[f]x, ^[f]N^[t](^[f]y)) → ^[f]Wr^[f](^[f]x, ^[f]check^[f](^[f]y))
^[f]Tr^[f](^[f]x, ^[t]N^[f](^[t]y)) → ^[f]Wr^[f](^[f]x, ^[t]check^[f](^[t]y))
^[f]Tr^[f](^[t]x, ^[f]N^[t](^[f]y)) → ^[f]Wr^[t](^[t]x, ^[f]check^[f](^[f]y))
^[f]Tr^[f](^[t]x, ^[t]N^[f](^[t]y)) → ^[f]Wr^[t](^[t]x, ^[t]check^[f](^[t]y))
^[f]Wr^[f](^[f]ok^[f](^[f]x), ^[f]y) → ^[f]Tr^[t](^[f]x, ^[f]y)
^[f]Wr^[f](^[f]ok^[f](^[f]x), ^[t]y) → ^[f]Tr^[f](^[f]x, ^[t]y)
^[f]Wr^[t](^[t]ok^[t](^[t]x), ^[f]y) → ^[f]Tr^[f](^[t]x, ^[f]y)
^[t]O^[t](^[f]ok^[f](^[f]x)) → ^[t]ok^[t](^[t]O^[t](^[f]x))
^[t]O^[t](^[t]ok^[t](^[t]x)) → ^[t]ok^[t](^[t]O^[t](^[t]x))
^[f]Wl^[t](^[f]x, ^[f]ok^[f](^[f]y)) → ^[f]Tl^[f](^[f]x, ^[f]y)
^[f]Wl^[t](^[f]x, ^[t]ok^[t](^[t]y)) → ^[f]Tl^[f](^[f]x, ^[t]y)
^[f]Wl^[f](^[t]x, ^[f]ok^[f](^[f]y)) → ^[f]Tl^[t](^[t]x, ^[f]y)
^[f]Wl^[f](^[t]x, ^[t]ok^[t](^[t]y)) → ^[f]Tl^[t](^[t]x, ^[t]y)
^[f]Tl^[f](^[f]N^[t](^[f]x), ^[f]y) → ^[f]Wl^[t](^[f]check^[f](^[f]x), ^[f]y)
^[f]Tl^[t](^[t]N^[f](^[t]x), ^[f]y) → ^[f]Wl^[f](^[t]check^[f](^[t]x), ^[f]y)
^[f]Tr^[t](^[f]x, ^[f]N^[t](^[f]y)) → ^[f]Wr^[f](^[f]check^[f](^[f]x), ^[f]y)
^[f]Tr^[f](^[f]x, ^[t]N^[f](^[t]y)) → ^[f]Wr^[f](^[f]check^[f](^[f]x), ^[t]y)
^[f]Tr^[f](^[t]x, ^[f]N^[t](^[f]y)) → ^[f]Wr^[t](^[t]check^[f](^[t]x), ^[f]y)
^[f]Tr^[f](^[t]x, ^[t]N^[f](^[t]y)) → ^[f]Wr^[t](^[t]check^[f](^[t]x), ^[t]y)
^[f]check^[f](^[f]N^[t](^[f]x)) → ^[f]N^[t](^[f]check^[f](^[f]x))
^[t]check^[f](^[t]N^[f](^[t]x)) → ^[t]N^[f](^[t]check^[f](^[t]x))
^[f]B^[t] → ^[f]N^[t](^[f]B^[t])
^[t]check^[f](^[t]O^[t](^[f]x)) → ^[t]O^[t](^[f]check^[f](^[f]x))
^[t]check^[f](^[t]O^[t](^[t]x)) → ^[t]O^[t](^[t]check^[f](^[t]x))
^[f]N^[t](^[f]ok^[f](^[f]x)) → ^[f]ok^[f](^[f]N^[t](^[f]x))
^[t]N^[f](^[t]ok^[t](^[t]x)) → ^[t]ok^[t](^[t]N^[f](^[t]x))
^[f]Wl^[t](^[f]ok^[f](^[f]x), ^[f]y) → ^[f]Tl^[f](^[f]x, ^[f]y)
^[f]Wl^[f](^[t]ok^[t](^[t]x), ^[f]y) → ^[f]Tl^[t](^[t]x, ^[f]y)
^[f]Wr^[f](^[f]x, ^[f]ok^[f](^[f]y)) → ^[f]Tr^[t](^[f]x, ^[f]y)
^[f]Wr^[f](^[f]x, ^[t]ok^[t](^[t]y)) → ^[f]Tr^[f](^[f]x, ^[t]y)
^[f]Wr^[t](^[t]x, ^[f]ok^[f](^[f]y)) → ^[f]Tr^[f](^[t]x, ^[f]y)
^[f]Wr^[t](^[t]x, ^[t]ok^[t](^[t]y)) → ^[f]Tr^[f](^[t]x, ^[t]y)
^[t]check^[f](^[t]O^[t](^[f]x)) → ^[t]ok^[t](^[t]O^[t](^[f]x))
^[f]Tl^[f](^[f]N^[t](^[f]x), ^[f]y) → ^[f]Wr^[f](^[f]check^[f](^[f]x), ^[f]y)
^[f]Tl^[t](^[t]N^[f](^[t]x), ^[f]y) → ^[f]Wr^[t](^[t]check^[f](^[t]x), ^[f]y)
^[f]Tl^[f](^[f]N^[t](^[f]x), ^[f]y) → ^[f]Wr^[f](^[f]x, ^[f]check^[f](^[f]y))
^[f]Tl^[f](^[f]N^[t](^[f]x), ^[t]y) → ^[f]Wr^[f](^[f]x, ^[t]check^[f](^[t]y))
^[f]Tl^[t](^[t]N^[f](^[t]x), ^[f]y) → ^[f]Wr^[t](^[t]x, ^[f]check^[f](^[f]y))
^[f]Tl^[t](^[t]N^[f](^[t]x), ^[t]y) → ^[f]Wr^[t](^[t]x, ^[t]check^[f](^[t]y))
^[f]Tr^[t](^[f]x, ^[f]N^[t](^[f]y)) → ^[f]Wl^[t](^[f]check^[f](^[f]x), ^[f]y)
^[f]Tr^[f](^[f]x, ^[t]N^[f](^[t]y)) → ^[f]Wl^[t](^[f]check^[f](^[f]x), ^[t]y)
^[f]Tr^[f](^[t]x, ^[f]N^[t](^[f]y)) → ^[f]Wl^[f](^[t]check^[f](^[t]x), ^[f]y)
^[f]Tr^[f](^[t]x, ^[t]N^[f](^[t]y)) → ^[f]Wl^[f](^[t]check^[f](^[t]x), ^[t]y)
^[f]Tr^[t](^[f]x, ^[f]N^[t](^[f]y)) → ^[f]Wl^[t](^[f]x, ^[f]check^[f](^[f]y))
^[f]Tr^[f](^[f]x, ^[t]N^[f](^[t]y)) → ^[f]Wl^[t](^[f]x, ^[t]check^[f](^[t]y))
^[f]Tr^[f](^[t]x, ^[f]N^[t](^[f]y)) → ^[f]Wl^[f](^[t]x, ^[f]check^[f](^[f]y))
^[f]Tr^[f](^[t]x, ^[t]N^[f](^[t]y)) → ^[f]Wl^[f](^[t]x, ^[t]check^[f](^[t]y))
^[f]Tl^[f](^[f]B^[t], ^[f]y) → ^[f]Wr^[f](^[f]B^[t], ^[f]check^[f](^[f]y))
^[f]Tl^[f](^[f]B^[t], ^[t]y) → ^[f]Wr^[f](^[f]B^[t], ^[t]check^[f](^[t]y))
^[f]Tr^[t](^[f]x, ^[f]B^[t]) → ^[f]Wl^[t](^[f]check^[f](^[f]x), ^[f]B^[t])
^[f]Tr^[f](^[t]x, ^[f]B^[t]) → ^[f]Wl^[f](^[t]check^[f](^[t]x), ^[f]B^[t])

Our polynomial interpretation was:
P(Tl^[false])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Tl^[true])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(N^[false])(x₁) = 1 + 1·x₁
P(N^[true])(x₁) = 0 + 1·x₁
P(Wl^[false])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Wl^[true])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(check^[false])(x₁) = 0 + 1·x₁
P(check^[true])(x₁) = 1 + 1·x₁
P(Tr^[false])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Tr^[true])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Wr^[false])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Wr^[true])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(ok^[false])(x₁) = 1 + 1·x₁
P(ok^[true])(x₁) = 0 + 1·x₁
P(O^[false])(x₁) = 1 + 1·x₁
P(O^[true])(x₁) = 0 + 1·x₁
P(B^[false])() = 1
P(B^[true])() = 1

The following rules were deleted from R:

Tl(N(x), y) → Wr(x, check(y))

The following rules were deleted from S:
none

(8) Obligation:

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

Tl(N(x), y) → Wr(check(x), y)
Tr(x, N(y)) → Wl(check(x), y)
Tr(x, N(y)) → Wl(x, check(y))
Tl(B, y) → Wr(B, check(y))
Tr(x, B) → Wl(check(x), B)

The relative TRS consists of the following S rules:

Tl(N(x), y) → Wl(x, check(y))
Tr(x, N(y)) → Wr(x, check(y))
Wr(ok(x), y) → Tr(x, y)
O(ok(x)) → ok(O(x))
Wl(x, ok(y)) → Tl(x, y)
Tl(N(x), y) → Wl(check(x), y)
Tr(x, N(y)) → Wr(check(x), y)
check(N(x)) → N(check(x))
B → N(B)
check(O(x)) → O(check(x))
N(ok(x)) → ok(N(x))
Wl(ok(x), y) → Tl(x, y)
Wr(x, ok(y)) → Tr(x, y)
check(O(x)) → ok(O(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:
Tl₂: component 1: AND[]
N₁: component 1: AND[x₁¹]
Wl₂: component 1: AND[]
check₁: component 1: AND[x₁¹]
Tr₂: component 1: AND[]
Wr₂: component 1: AND[]
ok₁: component 1: OR[]
O₁: component 1: OR[]
B₀: component 1: AND[]

Our labelling function was:
Tl₂:component 1: OR[-x₁¹, -x₂¹]
N₁:component 1: XOR[-x₁¹]
Wl₂:component 1: XOR[]
check₁:component 1: AND[]
Tr₂:component 1: XOR[-x₂¹]
Wr₂:component 1: XOR[x₂¹]
ok₁:component 1: XOR[-x₁¹]
O₁:component 1: OR[x₁¹]
B₀:component 1: AND[]

Our labelled system was:
^[t]Tl^[t](^[f]N^[t](^[f]x), ^[f]y) → ^[t]Wl^[f](^[f]x, ^[f]check^[t](^[f]y))
^[t]Tl^[t](^[f]N^[t](^[f]x), ^[t]y) → ^[t]Wl^[f](^[f]x, ^[t]check^[t](^[t]y))
^[t]Tl^[t](^[t]N^[f](^[t]x), ^[f]y) → ^[t]Wl^[f](^[t]x, ^[f]check^[t](^[f]y))
^[t]Tl^[f](^[t]N^[f](^[t]x), ^[t]y) → ^[t]Wl^[f](^[t]x, ^[t]check^[t](^[t]y))
^[t]Tr^[t](^[f]x, ^[f]N^[t](^[f]y)) → ^[t]Wr^[f](^[f]x, ^[f]check^[t](^[f]y))
^[t]Tr^[f](^[f]x, ^[t]N^[f](^[t]y)) → ^[t]Wr^[t](^[f]x, ^[t]check^[t](^[t]y))
^[t]Wr^[f](^[f]ok^[t](^[f]x), ^[f]y) → ^[t]Tr^[t](^[f]x, ^[f]y)
^[t]Wr^[t](^[f]ok^[t](^[f]x), ^[t]y) → ^[t]Tr^[f](^[f]x, ^[t]y)
^[t]Wr^[f](^[f]ok^[f](^[t]x), ^[f]y) → ^[t]Tr^[t](^[t]x, ^[f]y)
^[t]Wr^[t](^[f]ok^[f](^[t]x), ^[t]y) → ^[t]Tr^[f](^[t]x, ^[t]y)
^[f]O^[f](^[f]ok^[t](^[f]x)) → ^[f]ok^[t](^[f]O^[f](^[f]x))
^[f]O^[f](^[f]ok^[f](^[t]x)) → ^[f]ok^[t](^[f]O^[t](^[t]x))
^[t]Wl^[f](^[f]x, ^[f]ok^[t](^[f]y)) → ^[t]Tl^[t](^[f]x, ^[f]y)
^[t]Wl^[f](^[f]x, ^[f]ok^[f](^[t]y)) → ^[t]Tl^[t](^[f]x, ^[t]y)
^[t]Wl^[f](^[t]x, ^[f]ok^[f](^[t]y)) → ^[t]Tl^[f](^[t]x, ^[t]y)
^[t]Tl^[t](^[f]N^[t](^[f]x), ^[f]y) → ^[t]Wl^[f](^[f]check^[t](^[f]x), ^[f]y)
^[t]Tl^[t](^[t]N^[f](^[t]x), ^[f]y) → ^[t]Wl^[f](^[t]check^[t](^[t]x), ^[f]y)
^[t]Tl^[f](^[t]N^[f](^[t]x), ^[t]y) → ^[t]Wl^[f](^[t]check^[t](^[t]x), ^[t]y)
^[t]Tr^[t](^[f]x, ^[f]N^[t](^[f]y)) → ^[t]Wr^[f](^[f]check^[t](^[f]x), ^[f]y)
^[t]Tr^[f](^[f]x, ^[t]N^[f](^[t]y)) → ^[t]Wr^[t](^[f]check^[t](^[f]x), ^[t]y)
^[t]Tr^[t](^[t]x, ^[f]N^[t](^[f]y)) → ^[t]Wr^[f](^[t]check^[t](^[t]x), ^[f]y)
^[t]Tr^[f](^[t]x, ^[t]N^[f](^[t]y)) → ^[t]Wr^[t](^[t]check^[t](^[t]x), ^[t]y)
^[f]check^[t](^[f]N^[t](^[f]x)) → ^[f]N^[t](^[f]check^[t](^[f]x))
^[t]check^[t](^[t]N^[f](^[t]x)) → ^[t]N^[f](^[t]check^[t](^[t]x))
^[t]B^[t] → ^[t]N^[f](^[t]B^[t])
^[f]check^[t](^[f]O^[f](^[f]x)) → ^[f]O^[f](^[f]check^[t](^[f]x))
^[f]check^[t](^[f]O^[t](^[t]x)) → ^[f]O^[t](^[t]check^[t](^[t]x))
^[f]N^[t](^[f]ok^[t](^[f]x)) → ^[f]ok^[t](^[f]N^[t](^[f]x))
^[f]N^[t](^[f]ok^[f](^[t]x)) → ^[f]ok^[f](^[t]N^[f](^[t]x))
^[t]Wl^[f](^[f]ok^[t](^[f]x), ^[f]y) → ^[t]Tl^[t](^[f]x, ^[f]y)
^[t]Wl^[f](^[f]ok^[f](^[t]x), ^[f]y) → ^[t]Tl^[t](^[t]x, ^[f]y)
^[t]Wl^[f](^[f]ok^[f](^[t]x), ^[t]y) → ^[t]Tl^[f](^[t]x, ^[t]y)
^[t]Wr^[f](^[f]x, ^[f]ok^[t](^[f]y)) → ^[t]Tr^[t](^[f]x, ^[f]y)
^[t]Wr^[f](^[f]x, ^[f]ok^[f](^[t]y)) → ^[t]Tr^[f](^[f]x, ^[t]y)
^[f]check^[t](^[f]O^[f](^[f]x)) → ^[f]ok^[t](^[f]O^[f](^[f]x))
^[f]check^[t](^[f]O^[t](^[t]x)) → ^[f]ok^[t](^[f]O^[t](^[t]x))
^[t]Tl^[t](^[f]N^[t](^[f]x), ^[f]y) → ^[t]Wr^[f](^[f]check^[t](^[f]x), ^[f]y)
^[t]Tl^[t](^[f]N^[t](^[f]x), ^[t]y) → ^[t]Wr^[t](^[f]check^[t](^[f]x), ^[t]y)
^[t]Tl^[t](^[t]N^[f](^[t]x), ^[f]y) → ^[t]Wr^[f](^[t]check^[t](^[t]x), ^[f]y)
^[t]Tl^[f](^[t]N^[f](^[t]x), ^[t]y) → ^[t]Wr^[t](^[t]check^[t](^[t]x), ^[t]y)
^[t]Tr^[t](^[f]x, ^[f]N^[t](^[f]y)) → ^[t]Wl^[f](^[f]check^[t](^[f]x), ^[f]y)
^[t]Tr^[f](^[f]x, ^[t]N^[f](^[t]y)) → ^[t]Wl^[f](^[f]check^[t](^[f]x), ^[t]y)
^[t]Tr^[t](^[t]x, ^[f]N^[t](^[f]y)) → ^[t]Wl^[f](^[t]check^[t](^[t]x), ^[f]y)
^[t]Tr^[f](^[t]x, ^[t]N^[f](^[t]y)) → ^[t]Wl^[f](^[t]check^[t](^[t]x), ^[t]y)
^[t]Tr^[t](^[f]x, ^[f]N^[t](^[f]y)) → ^[t]Wl^[f](^[f]x, ^[f]check^[t](^[f]y))
^[t]Tr^[f](^[f]x, ^[t]N^[f](^[t]y)) → ^[t]Wl^[f](^[f]x, ^[t]check^[t](^[t]y))
^[t]Tl^[t](^[t]B^[t], ^[f]y) → ^[t]Wr^[f](^[t]B^[t], ^[f]check^[t](^[f]y))
^[t]Tl^[f](^[t]B^[t], ^[t]y) → ^[t]Wr^[t](^[t]B^[t], ^[t]check^[t](^[t]y))
^[t]Tr^[f](^[f]x, ^[t]B^[t]) → ^[t]Wl^[f](^[f]check^[t](^[f]x), ^[t]B^[t])
^[t]Tr^[f](^[t]x, ^[t]B^[t]) → ^[t]Wl^[f](^[t]check^[t](^[t]x), ^[t]B^[t])

Our polynomial interpretation was:
P(Tl^[false])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Tl^[true])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(N^[false])(x₁) = 0 + 1·x₁
P(N^[true])(x₁) = 1 + 1·x₁
P(Wl^[false])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Wl^[true])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(check^[false])(x₁) = 1 + 1·x₁
P(check^[true])(x₁) = 0 + 1·x₁
P(Tr^[false])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Tr^[true])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Wr^[false])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Wr^[true])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(ok^[false])(x₁) = 1 + 1·x₁
P(ok^[true])(x₁) = 0 + 1·x₁
P(O^[false])(x₁) = 0 + 1·x₁
P(O^[true])(x₁) = 0 + 1·x₁
P(B^[false])() = 1
P(B^[true])() = 1

The following rules were deleted from R:

Tr(x, B) → Wl(check(x), B)

The following rules were deleted from S:
none

(10) Obligation:

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

Tl(N(x), y) → Wr(check(x), y)
Tr(x, N(y)) → Wl(check(x), y)
Tr(x, N(y)) → Wl(x, check(y))
Tl(B, y) → Wr(B, check(y))

The relative TRS consists of the following S rules:

Tl(N(x), y) → Wl(x, check(y))
Tr(x, N(y)) → Wr(x, check(y))
Wr(ok(x), y) → Tr(x, y)
O(ok(x)) → ok(O(x))
Wl(x, ok(y)) → Tl(x, y)
Tl(N(x), y) → Wl(check(x), y)
Tr(x, N(y)) → Wr(check(x), y)
check(N(x)) → N(check(x))
B → N(B)
check(O(x)) → O(check(x))
N(ok(x)) → ok(N(x))
Wl(ok(x), y) → Tl(x, y)
Wr(x, ok(y)) → Tr(x, y)
check(O(x)) → ok(O(x))

(11) 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:
Tl₂: component 1: OR[]
N₁: component 1: AND[x₁¹]
Wl₂: component 1: OR[]
check₁: component 1: OR[x₁¹]
Tr₂: component 1: OR[]
Wr₂: component 1: OR[]
ok₁: component 1: OR[]
O₁: component 1: OR[]
B₀: component 1: AND[]

Our labelling function was:
Tl₂:component 1: XOR[x₂¹]
N₁:component 1: XOR[x₁¹]
Wl₂:component 1: AND[x₂¹]
check₁:component 1: AND[]
Tr₂:component 1: OR[]
Wr₂:component 1: OR[-x₁¹, -x₂¹]
ok₁:component 1: OR[x₁¹]
O₁:component 1: AND[]
B₀:component 1: XOR[]

Our labelled system was:
^[f]Tl^[f](^[f]N^[f](^[f]x), ^[f]y) → ^[f]Wl^[f](^[f]x, ^[f]check^[t](^[f]y))
^[f]Tl^[t](^[f]N^[f](^[f]x), ^[t]y) → ^[f]Wl^[t](^[f]x, ^[t]check^[t](^[t]y))
^[f]Tl^[f](^[t]N^[t](^[t]x), ^[f]y) → ^[f]Wl^[f](^[t]x, ^[f]check^[t](^[f]y))
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[t]y) → ^[f]Wl^[t](^[t]x, ^[t]check^[t](^[t]y))
^[f]Tr^[f](^[f]x, ^[f]N^[f](^[f]y)) → ^[f]Wr^[t](^[f]x, ^[f]check^[t](^[f]y))
^[f]Tr^[f](^[f]x, ^[t]N^[t](^[t]y)) → ^[f]Wr^[t](^[f]x, ^[t]check^[t](^[t]y))
^[f]Tr^[f](^[t]x, ^[t]N^[t](^[t]y)) → ^[f]Wr^[f](^[t]x, ^[t]check^[t](^[t]y))
^[f]Wr^[t](^[f]ok^[f](^[f]x), ^[f]y) → ^[f]Tr^[f](^[f]x, ^[f]y)
^[f]Wr^[t](^[f]ok^[t](^[t]x), ^[f]y) → ^[f]Tr^[f](^[t]x, ^[f]y)
^[f]O^[t](^[f]ok^[f](^[f]x)) → ^[f]ok^[f](^[f]O^[t](^[f]x))
^[f]O^[t](^[f]ok^[t](^[t]x)) → ^[f]ok^[f](^[f]O^[t](^[t]x))
^[f]Wl^[f](^[f]x, ^[f]ok^[f](^[f]y)) → ^[f]Tl^[f](^[f]x, ^[f]y)
^[f]Wl^[f](^[f]x, ^[f]ok^[t](^[t]y)) → ^[f]Tl^[t](^[f]x, ^[t]y)
^[f]Tl^[f](^[f]N^[f](^[f]x), ^[f]y) → ^[f]Wl^[f](^[f]check^[t](^[f]x), ^[f]y)
^[f]Tl^[t](^[f]N^[f](^[f]x), ^[t]y) → ^[f]Wl^[t](^[f]check^[t](^[f]x), ^[t]y)
^[f]Tl^[f](^[t]N^[t](^[t]x), ^[f]y) → ^[f]Wl^[f](^[t]check^[t](^[t]x), ^[f]y)
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[t]y) → ^[f]Wl^[t](^[t]check^[t](^[t]x), ^[t]y)
^[f]Tr^[f](^[f]x, ^[f]N^[f](^[f]y)) → ^[f]Wr^[t](^[f]check^[t](^[f]x), ^[f]y)
^[f]Tr^[f](^[f]x, ^[t]N^[t](^[t]y)) → ^[f]Wr^[t](^[f]check^[t](^[f]x), ^[t]y)
^[f]Tr^[f](^[t]x, ^[f]N^[f](^[f]y)) → ^[f]Wr^[t](^[t]check^[t](^[t]x), ^[f]y)
^[f]Tr^[f](^[t]x, ^[t]N^[t](^[t]y)) → ^[f]Wr^[f](^[t]check^[t](^[t]x), ^[t]y)
^[f]check^[t](^[f]N^[f](^[f]x)) → ^[f]N^[f](^[f]check^[t](^[f]x))
^[t]check^[t](^[t]N^[t](^[t]x)) → ^[t]N^[t](^[t]check^[t](^[t]x))
^[t]B^[f] → ^[t]N^[t](^[t]B^[f])
^[f]check^[t](^[f]O^[t](^[f]x)) → ^[f]O^[t](^[f]check^[t](^[f]x))
^[f]check^[t](^[f]O^[t](^[t]x)) → ^[f]O^[t](^[t]check^[t](^[t]x))
^[f]N^[f](^[f]ok^[f](^[f]x)) → ^[f]ok^[f](^[f]N^[f](^[f]x))
^[f]N^[f](^[f]ok^[t](^[t]x)) → ^[f]ok^[t](^[t]N^[t](^[t]x))
^[f]Wl^[f](^[f]ok^[f](^[f]x), ^[f]y) → ^[f]Tl^[f](^[f]x, ^[f]y)
^[f]Wl^[t](^[f]ok^[f](^[f]x), ^[t]y) → ^[f]Tl^[t](^[f]x, ^[t]y)
^[f]Wl^[f](^[f]ok^[t](^[t]x), ^[f]y) → ^[f]Tl^[f](^[t]x, ^[f]y)
^[f]Wl^[t](^[f]ok^[t](^[t]x), ^[t]y) → ^[f]Tl^[t](^[t]x, ^[t]y)
^[f]Wr^[t](^[f]x, ^[f]ok^[f](^[f]y)) → ^[f]Tr^[f](^[f]x, ^[f]y)
^[f]Wr^[t](^[f]x, ^[f]ok^[t](^[t]y)) → ^[f]Tr^[f](^[f]x, ^[t]y)
^[f]check^[t](^[f]O^[t](^[f]x)) → ^[f]ok^[f](^[f]O^[t](^[f]x))
^[f]Tl^[f](^[f]N^[f](^[f]x), ^[f]y) → ^[f]Wr^[t](^[f]check^[t](^[f]x), ^[f]y)
^[f]Tl^[t](^[f]N^[f](^[f]x), ^[t]y) → ^[f]Wr^[t](^[f]check^[t](^[f]x), ^[t]y)
^[f]Tl^[f](^[t]N^[t](^[t]x), ^[f]y) → ^[f]Wr^[t](^[t]check^[t](^[t]x), ^[f]y)
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[t]y) → ^[f]Wr^[f](^[t]check^[t](^[t]x), ^[t]y)
^[f]Tr^[f](^[f]x, ^[f]N^[f](^[f]y)) → ^[f]Wl^[f](^[f]check^[t](^[f]x), ^[f]y)
^[f]Tr^[f](^[f]x, ^[t]N^[t](^[t]y)) → ^[f]Wl^[t](^[f]check^[t](^[f]x), ^[t]y)
^[f]Tr^[f](^[t]x, ^[f]N^[f](^[f]y)) → ^[f]Wl^[f](^[t]check^[t](^[t]x), ^[f]y)
^[f]Tr^[f](^[t]x, ^[t]N^[t](^[t]y)) → ^[f]Wl^[t](^[t]check^[t](^[t]x), ^[t]y)
^[f]Tr^[f](^[f]x, ^[f]N^[f](^[f]y)) → ^[f]Wl^[f](^[f]x, ^[f]check^[t](^[f]y))
^[f]Tr^[f](^[f]x, ^[t]N^[t](^[t]y)) → ^[f]Wl^[t](^[f]x, ^[t]check^[t](^[t]y))
^[f]Tl^[f](^[t]B^[f], ^[f]y) → ^[f]Wr^[t](^[t]B^[f], ^[f]check^[t](^[f]y))
^[f]Tl^[t](^[t]B^[f], ^[t]y) → ^[f]Wr^[f](^[t]B^[f], ^[t]check^[t](^[t]y))

Our polynomial interpretation was:
P(Tl^[false])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Tl^[true])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(N^[false])(x₁) = 1 + 1·x₁
P(N^[true])(x₁) = 0 + 1·x₁
P(Wl^[false])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Wl^[true])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(check^[false])(x₁) = 0 + 1·x₁
P(check^[true])(x₁) = 0 + 1·x₁
P(Tr^[false])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Tr^[true])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Wr^[false])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Wr^[true])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(ok^[false])(x₁) = 0 + 1·x₁
P(ok^[true])(x₁) = 0 + 1·x₁
P(O^[false])(x₁) = 1 + 1·x₁
P(O^[true])(x₁) = 0 + 1·x₁
P(B^[false])() = 0
P(B^[true])() = 0

The following rules were deleted from R:

Tr(x, N(y)) → Wl(x, check(y))

The following rules were deleted from S:
none

(12) Obligation:

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

Tl(N(x), y) → Wr(check(x), y)
Tr(x, N(y)) → Wl(check(x), y)
Tl(B, y) → Wr(B, check(y))

The relative TRS consists of the following S rules:

Tl(N(x), y) → Wl(x, check(y))
Tr(x, N(y)) → Wr(x, check(y))
Wr(ok(x), y) → Tr(x, y)
O(ok(x)) → ok(O(x))
Wl(x, ok(y)) → Tl(x, y)
Tl(N(x), y) → Wl(check(x), y)
Tr(x, N(y)) → Wr(check(x), y)
check(N(x)) → N(check(x))
B → N(B)
check(O(x)) → O(check(x))
N(ok(x)) → ok(N(x))
Wl(ok(x), y) → Tl(x, y)
Wr(x, ok(y)) → Tr(x, y)
check(O(x)) → ok(O(x))

(13) RelTRSRRRProof (EQUIVALENT transformation)

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

POL(Tl(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(N(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(Wr(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(check(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁

POL(Tr(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(Wl(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁ +
/ 1 1 \

\ 0 0 /

· x₂

POL(B) =
/ 0 \

\ 1 /

POL(ok(x₁)) =
/ 0 \

\ 0 /

+
/ 1 0 \

\ 0 1 /

· x₁

POL(O(x₁)) =
/ 1 \

\ 0 /

+
/ 1 1 \

\ 0 0 /

· x₁

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

Tl(B, y) → Wr(B, check(y))

Rules from S:
none

(14) Obligation:

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

Tl(N(x), y) → Wr(check(x), y)
Tr(x, N(y)) → Wl(check(x), y)

The relative TRS consists of the following S rules:

Tl(N(x), y) → Wl(x, check(y))
Tr(x, N(y)) → Wr(x, check(y))
Wr(ok(x), y) → Tr(x, y)
O(ok(x)) → ok(O(x))
Wl(x, ok(y)) → Tl(x, y)
Tl(N(x), y) → Wl(check(x), y)
Tr(x, N(y)) → Wr(check(x), y)
check(N(x)) → N(check(x))
B → N(B)
check(O(x)) → O(check(x))
N(ok(x)) → ok(N(x))
Wl(ok(x), y) → Tl(x, y)
Wr(x, ok(y)) → Tr(x, y)
check(O(x)) → ok(O(x))

(15) 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:
Tl₂: component 1: OR[]
N₁: component 1: OR[x₁¹]
Wl₂: component 1: OR[]
check₁: component 1: AND[x₁¹]
Tr₂: component 1: OR[]
Wr₂: component 1: OR[]
ok₁: component 1: AND[x₁¹]
O₁: component 1: AND[]
B₀: component 1: OR[]

Our labelling function was:
Tl₂:component 1: OR[-x₁¹, x₂¹]
N₁:component 1: AND[x₁¹]
Wl₂:component 1: XOR[x₁¹]
check₁:component 1: OR[]
Tr₂:component 1: OR[-x₁¹, x₂¹]
Wr₂:component 1: AND[x₁¹]
ok₁:component 1: OR[x₁¹]
O₁:component 1: XOR[x₁¹]
B₀:component 1: AND[]

Our labelled system was:
^[f]Tl^[t](^[f]N^[f](^[f]x), ^[f]y) → ^[f]Wl^[f](^[f]x, ^[f]check^[f](^[f]y))
^[f]Tl^[t](^[f]N^[f](^[f]x), ^[t]y) → ^[f]Wl^[f](^[f]x, ^[t]check^[f](^[t]y))
^[f]Tl^[f](^[t]N^[t](^[t]x), ^[f]y) → ^[f]Wl^[t](^[t]x, ^[f]check^[f](^[f]y))
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[t]y) → ^[f]Wl^[t](^[t]x, ^[t]check^[f](^[t]y))
^[f]Tr^[t](^[f]x, ^[f]N^[f](^[f]y)) → ^[f]Wr^[f](^[f]x, ^[f]check^[f](^[f]y))
^[f]Tr^[t](^[f]x, ^[t]N^[t](^[t]y)) → ^[f]Wr^[f](^[f]x, ^[t]check^[f](^[t]y))
^[f]Tr^[f](^[t]x, ^[f]N^[f](^[f]y)) → ^[f]Wr^[t](^[t]x, ^[f]check^[f](^[f]y))
^[f]Tr^[t](^[t]x, ^[t]N^[t](^[t]y)) → ^[f]Wr^[t](^[t]x, ^[t]check^[f](^[t]y))
^[f]Wr^[f](^[f]ok^[f](^[f]x), ^[f]y) → ^[f]Tr^[t](^[f]x, ^[f]y)
^[f]Wr^[t](^[t]ok^[t](^[t]x), ^[f]y) → ^[f]Tr^[f](^[t]x, ^[f]y)
^[f]Wr^[t](^[t]ok^[t](^[t]x), ^[t]y) → ^[f]Tr^[t](^[t]x, ^[t]y)
^[t]O^[f](^[f]ok^[f](^[f]x)) → ^[t]ok^[t](^[t]O^[f](^[f]x))
^[t]O^[t](^[t]ok^[t](^[t]x)) → ^[t]ok^[t](^[t]O^[t](^[t]x))
^[f]Wl^[f](^[f]x, ^[f]ok^[f](^[f]y)) → ^[f]Tl^[t](^[f]x, ^[f]y)
^[f]Wl^[f](^[f]x, ^[t]ok^[t](^[t]y)) → ^[f]Tl^[t](^[f]x, ^[t]y)
^[f]Wl^[t](^[t]x, ^[f]ok^[f](^[f]y)) → ^[f]Tl^[f](^[t]x, ^[f]y)
^[f]Wl^[t](^[t]x, ^[t]ok^[t](^[t]y)) → ^[f]Tl^[t](^[t]x, ^[t]y)
^[f]Tl^[t](^[f]N^[f](^[f]x), ^[f]y) → ^[f]Wl^[f](^[f]check^[f](^[f]x), ^[f]y)
^[f]Tl^[f](^[t]N^[t](^[t]x), ^[f]y) → ^[f]Wl^[t](^[t]check^[f](^[t]x), ^[f]y)
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[t]y) → ^[f]Wl^[t](^[t]check^[f](^[t]x), ^[t]y)
^[f]Tr^[t](^[f]x, ^[f]N^[f](^[f]y)) → ^[f]Wr^[f](^[f]check^[f](^[f]x), ^[f]y)
^[f]Tr^[t](^[f]x, ^[t]N^[t](^[t]y)) → ^[f]Wr^[f](^[f]check^[f](^[f]x), ^[t]y)
^[f]Tr^[f](^[t]x, ^[f]N^[f](^[f]y)) → ^[f]Wr^[t](^[t]check^[f](^[t]x), ^[f]y)
^[f]Tr^[t](^[t]x, ^[t]N^[t](^[t]y)) → ^[f]Wr^[t](^[t]check^[f](^[t]x), ^[t]y)
^[f]check^[f](^[f]N^[f](^[f]x)) → ^[f]N^[f](^[f]check^[f](^[f]x))
^[t]check^[f](^[t]N^[t](^[t]x)) → ^[t]N^[t](^[t]check^[f](^[t]x))
^[f]B^[t] → ^[f]N^[f](^[f]B^[t])
^[t]check^[f](^[t]O^[f](^[f]x)) → ^[t]O^[f](^[f]check^[f](^[f]x))
^[t]check^[f](^[t]O^[t](^[t]x)) → ^[t]O^[t](^[t]check^[f](^[t]x))
^[f]N^[f](^[f]ok^[f](^[f]x)) → ^[f]ok^[f](^[f]N^[f](^[f]x))
^[t]N^[t](^[t]ok^[t](^[t]x)) → ^[t]ok^[t](^[t]N^[t](^[t]x))
^[f]Wl^[f](^[f]ok^[f](^[f]x), ^[f]y) → ^[f]Tl^[t](^[f]x, ^[f]y)
^[f]Wl^[t](^[t]ok^[t](^[t]x), ^[f]y) → ^[f]Tl^[f](^[t]x, ^[f]y)
^[f]Wl^[t](^[t]ok^[t](^[t]x), ^[t]y) → ^[f]Tl^[t](^[t]x, ^[t]y)
^[f]Wr^[f](^[f]x, ^[f]ok^[f](^[f]y)) → ^[f]Tr^[t](^[f]x, ^[f]y)
^[f]Wr^[f](^[f]x, ^[t]ok^[t](^[t]y)) → ^[f]Tr^[t](^[f]x, ^[t]y)
^[f]Wr^[t](^[t]x, ^[f]ok^[f](^[f]y)) → ^[f]Tr^[f](^[t]x, ^[f]y)
^[f]Wr^[t](^[t]x, ^[t]ok^[t](^[t]y)) → ^[f]Tr^[t](^[t]x, ^[t]y)
^[t]check^[f](^[t]O^[f](^[f]x)) → ^[t]ok^[t](^[t]O^[f](^[f]x))
^[t]check^[f](^[t]O^[t](^[t]x)) → ^[t]ok^[t](^[t]O^[t](^[t]x))
^[f]Tl^[t](^[f]N^[f](^[f]x), ^[f]y) → ^[f]Wr^[f](^[f]check^[f](^[f]x), ^[f]y)
^[f]Tl^[f](^[t]N^[t](^[t]x), ^[f]y) → ^[f]Wr^[t](^[t]check^[f](^[t]x), ^[f]y)
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[t]y) → ^[f]Wr^[t](^[t]check^[f](^[t]x), ^[t]y)
^[f]Tr^[t](^[f]x, ^[f]N^[f](^[f]y)) → ^[f]Wl^[f](^[f]check^[f](^[f]x), ^[f]y)
^[f]Tr^[t](^[f]x, ^[t]N^[t](^[t]y)) → ^[f]Wl^[f](^[f]check^[f](^[f]x), ^[t]y)
^[f]Tr^[f](^[t]x, ^[f]N^[f](^[f]y)) → ^[f]Wl^[t](^[t]check^[f](^[t]x), ^[f]y)
^[f]Tr^[t](^[t]x, ^[t]N^[t](^[t]y)) → ^[f]Wl^[t](^[t]check^[f](^[t]x), ^[t]y)

Our polynomial interpretation was:
P(Tl^[false])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Tl^[true])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(N^[false])(x₁) = 0 + 1·x₁
P(N^[true])(x₁) = 1 + 1·x₁
P(Wl^[false])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Wl^[true])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(check^[false])(x₁) = 0 + 1·x₁
P(check^[true])(x₁) = 0 + 1·x₁
P(Tr^[false])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Tr^[true])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Wr^[false])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Wr^[true])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(ok^[false])(x₁) = 1 + 1·x₁
P(ok^[true])(x₁) = 0 + 1·x₁
P(O^[false])(x₁) = 0 + 1·x₁
P(O^[true])(x₁) = 0 + 1·x₁
P(B^[false])() = 0
P(B^[true])() = 0

The following rules were deleted from R:
none

The following rules were deleted from S:

Wl(ok(x), y) → Tl(x, y)

(16) Obligation:

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

Tl(N(x), y) → Wr(check(x), y)
Tr(x, N(y)) → Wl(check(x), y)

The relative TRS consists of the following S rules:

Tl(N(x), y) → Wl(x, check(y))
Tr(x, N(y)) → Wr(x, check(y))
Wr(ok(x), y) → Tr(x, y)
O(ok(x)) → ok(O(x))
Wl(x, ok(y)) → Tl(x, y)
Tl(N(x), y) → Wl(check(x), y)
Tr(x, N(y)) → Wr(check(x), y)
check(N(x)) → N(check(x))
B → N(B)
check(O(x)) → O(check(x))
N(ok(x)) → ok(N(x))
Wr(x, ok(y)) → Tr(x, y)
check(O(x)) → ok(O(x))

(17) 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:
Tl₂: component 1: OR[]
N₁: component 1: AND[x₁¹]
Wl₂: component 1: OR[]
check₁: component 1: OR[x₁¹]
Tr₂: component 1: OR[]
Wr₂: component 1: OR[]
ok₁: component 1: OR[]
O₁: component 1: OR[]
B₀: component 1: AND[]

Our labelling function was:
Tl₂:component 1: XOR[x₁¹]
N₁:component 1: AND[x₁¹]
Wl₂:component 1: OR[x₂¹]
check₁:component 1: AND[]
Tr₂:component 1: AND[]
Wr₂:component 1: OR[-x₂¹]
ok₁:component 1: AND[-x₁¹]
O₁:component 1: AND[]
B₀:component 1: XOR[]

Our labelled system was:
^[f]Tl^[f](^[f]N^[f](^[f]x), ^[f]y) → ^[f]Wl^[f](^[f]x, ^[f]check^[t](^[f]y))
^[f]Tl^[f](^[f]N^[f](^[f]x), ^[t]y) → ^[f]Wl^[t](^[f]x, ^[t]check^[t](^[t]y))
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[f]y) → ^[f]Wl^[f](^[t]x, ^[f]check^[t](^[f]y))
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[t]y) → ^[f]Wl^[t](^[t]x, ^[t]check^[t](^[t]y))
^[f]Tr^[t](^[f]x, ^[f]N^[f](^[f]y)) → ^[f]Wr^[t](^[f]x, ^[f]check^[t](^[f]y))
^[f]Tr^[t](^[f]x, ^[t]N^[t](^[t]y)) → ^[f]Wr^[f](^[f]x, ^[t]check^[t](^[t]y))
^[f]Wr^[t](^[f]ok^[t](^[f]x), ^[f]y) → ^[f]Tr^[t](^[f]x, ^[f]y)
^[f]Wr^[f](^[f]ok^[t](^[f]x), ^[t]y) → ^[f]Tr^[t](^[f]x, ^[t]y)
^[f]Wr^[t](^[f]ok^[f](^[t]x), ^[f]y) → ^[f]Tr^[t](^[t]x, ^[f]y)
^[f]Wr^[f](^[f]ok^[f](^[t]x), ^[t]y) → ^[f]Tr^[t](^[t]x, ^[t]y)
^[f]O^[t](^[f]ok^[t](^[f]x)) → ^[f]ok^[t](^[f]O^[t](^[f]x))
^[f]O^[t](^[f]ok^[f](^[t]x)) → ^[f]ok^[t](^[f]O^[t](^[t]x))
^[f]Wl^[f](^[f]x, ^[f]ok^[t](^[f]y)) → ^[f]Tl^[f](^[f]x, ^[f]y)
^[f]Wl^[f](^[f]x, ^[f]ok^[f](^[t]y)) → ^[f]Tl^[f](^[f]x, ^[t]y)
^[f]Wl^[f](^[t]x, ^[f]ok^[t](^[f]y)) → ^[f]Tl^[t](^[t]x, ^[f]y)
^[f]Wl^[f](^[t]x, ^[f]ok^[f](^[t]y)) → ^[f]Tl^[t](^[t]x, ^[t]y)
^[f]Tl^[f](^[f]N^[f](^[f]x), ^[f]y) → ^[f]Wl^[f](^[f]check^[t](^[f]x), ^[f]y)
^[f]Tl^[f](^[f]N^[f](^[f]x), ^[t]y) → ^[f]Wl^[t](^[f]check^[t](^[f]x), ^[t]y)
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[f]y) → ^[f]Wl^[f](^[t]check^[t](^[t]x), ^[f]y)
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[t]y) → ^[f]Wl^[t](^[t]check^[t](^[t]x), ^[t]y)
^[f]Tr^[t](^[f]x, ^[f]N^[f](^[f]y)) → ^[f]Wr^[t](^[f]check^[t](^[f]x), ^[f]y)
^[f]Tr^[t](^[f]x, ^[t]N^[t](^[t]y)) → ^[f]Wr^[f](^[f]check^[t](^[f]x), ^[t]y)
^[f]Tr^[t](^[t]x, ^[f]N^[f](^[f]y)) → ^[f]Wr^[t](^[t]check^[t](^[t]x), ^[f]y)
^[f]Tr^[t](^[t]x, ^[t]N^[t](^[t]y)) → ^[f]Wr^[f](^[t]check^[t](^[t]x), ^[t]y)
^[f]check^[t](^[f]N^[f](^[f]x)) → ^[f]N^[f](^[f]check^[t](^[f]x))
^[t]check^[t](^[t]N^[t](^[t]x)) → ^[t]N^[t](^[t]check^[t](^[t]x))
^[t]B^[f] → ^[t]N^[t](^[t]B^[f])
^[f]check^[t](^[f]O^[t](^[f]x)) → ^[f]O^[t](^[f]check^[t](^[f]x))
^[f]check^[t](^[f]O^[t](^[t]x)) → ^[f]O^[t](^[t]check^[t](^[t]x))
^[f]N^[f](^[f]ok^[t](^[f]x)) → ^[f]ok^[t](^[f]N^[f](^[f]x))
^[f]N^[f](^[f]ok^[f](^[t]x)) → ^[f]ok^[f](^[t]N^[t](^[t]x))
^[f]Wr^[t](^[f]x, ^[f]ok^[t](^[f]y)) → ^[f]Tr^[t](^[f]x, ^[f]y)
^[f]Wr^[t](^[f]x, ^[f]ok^[f](^[t]y)) → ^[f]Tr^[t](^[f]x, ^[t]y)
^[f]check^[t](^[f]O^[t](^[f]x)) → ^[f]ok^[t](^[f]O^[t](^[f]x))
^[f]Tl^[f](^[f]N^[f](^[f]x), ^[f]y) → ^[f]Wr^[t](^[f]check^[t](^[f]x), ^[f]y)
^[f]Tl^[f](^[f]N^[f](^[f]x), ^[t]y) → ^[f]Wr^[f](^[f]check^[t](^[f]x), ^[t]y)
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[f]y) → ^[f]Wr^[t](^[t]check^[t](^[t]x), ^[f]y)
^[f]Tl^[t](^[t]N^[t](^[t]x), ^[t]y) → ^[f]Wr^[f](^[t]check^[t](^[t]x), ^[t]y)
^[f]Tr^[t](^[f]x, ^[f]N^[f](^[f]y)) → ^[f]Wl^[f](^[f]check^[t](^[f]x), ^[f]y)
^[f]Tr^[t](^[f]x, ^[t]N^[t](^[t]y)) → ^[f]Wl^[t](^[f]check^[t](^[f]x), ^[t]y)
^[f]Tr^[t](^[t]x, ^[f]N^[f](^[f]y)) → ^[f]Wl^[f](^[t]check^[t](^[t]x), ^[f]y)
^[f]Tr^[t](^[t]x, ^[t]N^[t](^[t]y)) → ^[f]Wl^[t](^[t]check^[t](^[t]x), ^[t]y)

Our polynomial interpretation was:
P(Tl^[false])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Tl^[true])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(N^[false])(x₁) = 1 + 1·x₁
P(N^[true])(x₁) = 0 + 1·x₁
P(Wl^[false])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Wl^[true])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(check^[false])(x₁) = 1 + 1·x₁
P(check^[true])(x₁) = 0 + 1·x₁
P(Tr^[false])(x₁,x₂) = 0 + 1·x₁ + 1·x₂
P(Tr^[true])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Wr^[false])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(Wr^[true])(x₁,x₂) = 1 + 1·x₁ + 1·x₂
P(ok^[false])(x₁) = 0 + 1·x₁
P(ok^[true])(x₁) = 0 + 1·x₁
P(O^[false])(x₁) = 0 + 1·x₁
P(O^[true])(x₁) = 0 + 1·x₁
P(B^[false])() = 0
P(B^[true])() = 0

The following rules were deleted from R:

Tr(x, N(y)) → Wl(check(x), y)

The following rules were deleted from S:
none

(18) Obligation:

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

Tl(N(x), y) → Wr(check(x), y)

The relative TRS consists of the following S rules:

Tl(N(x), y) → Wl(x, check(y))
Tr(x, N(y)) → Wr(x, check(y))
Wr(ok(x), y) → Tr(x, y)
O(ok(x)) → ok(O(x))
Wl(x, ok(y)) → Tl(x, y)
Tl(N(x), y) → Wl(check(x), y)
Tr(x, N(y)) → Wr(check(x), y)
check(N(x)) → N(check(x))
B → N(B)
check(O(x)) → O(check(x))
N(ok(x)) → ok(N(x))
Wr(x, ok(y)) → Tr(x, y)
check(O(x)) → ok(O(x))

(19) RelTRSRRRProof (EQUIVALENT transformation)

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

POL(B) = 0
POL(N(x₁)) = x₁
POL(O(x₁)) = x₁
POL(Tl(x₁, x₂)) = 1 + x₁ + x₂
POL(Tr(x₁, x₂)) = x₁ + x₂
POL(Wl(x₁, x₂)) = 1 + x₁ + x₂
POL(Wr(x₁, x₂)) = x₁ + x₂
POL(check(x₁)) = x₁
POL(ok(x₁)) = x₁

With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

Tl(N(x), y) → Wr(check(x), y)

Rules from S:
none

(20) Obligation:

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

Tl(N(x), y) → Wl(x, check(y))
Tr(x, N(y)) → Wr(x, check(y))
Wr(ok(x), y) → Tr(x, y)
O(ok(x)) → ok(O(x))
Wl(x, ok(y)) → Tl(x, y)
Tl(N(x), y) → Wl(check(x), y)
Tr(x, N(y)) → Wr(check(x), y)
check(N(x)) → N(check(x))
B → N(B)
check(O(x)) → O(check(x))
N(ok(x)) → ok(N(x))
Wr(x, ok(y)) → Tr(x, y)
check(O(x)) → ok(O(x))

(21) RIsEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) RelTRSRRRProof (EQUIVALENT transformation)

(2) Obligation:

(3) RelTRSRRRProof (EQUIVALENT transformation)

(4) Obligation:

(5) RelTRSRRRProof (EQUIVALENT transformation)

(6) Obligation:

(7) RelTRSSemanticLabellingPOLOProof (EQUIVALENT transformation)

(8) Obligation:

(9) RelTRSSemanticLabellingPOLOProof (EQUIVALENT transformation)

(10) Obligation:

(11) RelTRSSemanticLabellingPOLOProof (EQUIVALENT transformation)

(12) Obligation:

(13) RelTRSRRRProof (EQUIVALENT transformation)

(14) Obligation:

(15) RelTRSSemanticLabellingPOLOProof (EQUIVALENT transformation)

(16) Obligation:

(17) RelTRSSemanticLabellingPOLOProof (EQUIVALENT transformation)

(18) Obligation:

(19) RelTRSRRRProof (EQUIVALENT transformation)

(20) Obligation:

(21) RIsEmptyProof (EQUIVALENT transformation)

(22) YES