(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
topB(i, N1, y) → topA(1, T1, y)
topA(i, x, N2) → topB(0, x, T2)
topB(i, S1, y) → topA(i, N1, y)
topA(i, x, S2) → topB(i, x, N2)
topA(i, N1, T2) → topB(i, N1, S2)
topA(1, T1, T2) → topB(1, T1, S2)
The relative TRS consists of the following S rules:
topB(i, N1, T2) → topB(i, N1, S2)
topA(i, S1, y) → topA(i, N1, y)
topB(1, T1, T2) → topB(1, T1, S2)
topB(i, x, S2) → topB(i, x, N2)
topB(i, x, N2) → topB(0, x, T2)
topA(i, N1, y) → topA(1, T1, y)
(1) RelTRSRRRProof (EQUIVALENT transformation)
We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(1) = 0
POL(N1) = 1
POL(N2) = 1
POL(S1) = 1
POL(S2) = 1
POL(T1) = 0
POL(T2) = 1
POL(topA(x1, x2, x3)) = x1 + x2 + x3
POL(topB(x1, x2, x3)) = x1 + x2 + x3
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
topB(i, N1, y) → topA(1, T1, y)
Rules from S:
topA(i, N1, y) → topA(1, T1, y)
(2) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
topA(i, x, N2) → topB(0, x, T2)
topB(i, S1, y) → topA(i, N1, y)
topA(i, x, S2) → topB(i, x, N2)
topA(i, N1, T2) → topB(i, N1, S2)
topA(1, T1, T2) → topB(1, T1, S2)
The relative TRS consists of the following S rules:
topB(i, N1, T2) → topB(i, N1, S2)
topA(i, S1, y) → topA(i, N1, y)
topB(1, T1, T2) → topB(1, T1, S2)
topB(i, x, S2) → topB(i, x, N2)
topB(i, x, N2) → topB(0, x, T2)
(3) RelTRSRRRProof (EQUIVALENT transformation)
We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(1) = 0
POL(N1) = 0
POL(N2) = 0
POL(S1) = 1
POL(S2) = 0
POL(T1) = 0
POL(T2) = 0
POL(topA(x1, x2, x3)) = x1 + x2 + x3
POL(topB(x1, x2, x3)) = x1 + x2 + x3
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
topB(i, S1, y) → topA(i, N1, y)
Rules from S:
topA(i, S1, y) → topA(i, N1, y)
(4) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
topA(i, x, N2) → topB(0, x, T2)
topA(i, x, S2) → topB(i, x, N2)
topA(i, N1, T2) → topB(i, N1, S2)
topA(1, T1, T2) → topB(1, T1, S2)
The relative TRS consists of the following S rules:
topB(i, N1, T2) → topB(i, N1, S2)
topB(1, T1, T2) → topB(1, T1, S2)
topB(i, x, S2) → topB(i, x, N2)
topB(i, x, N2) → topB(0, x, T2)
(5) RelTRSRRRProof (EQUIVALENT transformation)
We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(1) = 0
POL(N1) = 0
POL(N2) = 0
POL(S2) = 0
POL(T1) = 0
POL(T2) = 0
POL(topA(x1, x2, x3)) = 1 + x1 + x2 + x3
POL(topB(x1, x2, x3)) = x1 + x2 + x3
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
topA(i, x, N2) → topB(0, x, T2)
topA(i, x, S2) → topB(i, x, N2)
topA(i, N1, T2) → topB(i, N1, S2)
topA(1, T1, T2) → topB(1, T1, S2)
Rules from S:
none
(6) Obligation:
Relative term rewrite system:
R is empty.
The relative TRS consists of the following S rules:
topB(i, N1, T2) → topB(i, N1, S2)
topB(1, T1, T2) → topB(1, T1, S2)
topB(i, x, S2) → topB(i, x, N2)
topB(i, x, N2) → topB(0, x, T2)
(7) RIsEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(8) YES