YES
The TRS could be proven terminating. The proof took 26101 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (735ms).
| – Problem 2 was processed with processor SubtermCriterion (3ms).
| | – Problem 4 was processed with processor SubtermCriterion (0ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (6239ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4iUR (5690ms).
| | | – Problem 6 was processed with processor PolynomialLinearRange4iUR (4181ms).
| | | | – Problem 7 was processed with processor PolynomialLinearRange4iUR (5846ms).
| | | | | – Problem 8 was processed with processor DependencyGraph (8ms).
| | | | | | – Problem 9 was processed with processor PolynomialLinearRange4iUR (1043ms).
| | | | | | | – Problem 10 was processed with processor PolynomialLinearRange4iUR (1019ms).
| | | | | | | | – Problem 11 was processed with processor PolynomialLinearRange4iUR (981ms).
| | | | | | | | | – Problem 12 was processed with processor DependencyGraph (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| intersect'ii'in#(cons(X0, Xs), Ys) | → | u'2'1#(intersect'ii'in(Xs, Ys)) | | reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF) |
| reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF) |
| reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF) | | reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) |
| intersect'ii'in#(Xs, cons(X0, Ys)) | → | u'1'1#(intersect'ii'in(Xs, Ys)) | | u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) | → | reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) |
| reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) | | reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| intersect'ii'in#(cons(X0, Xs), Ys) | → | intersect'ii'in#(Xs, Ys) | | reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| reduce'ii'in#(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | reduce'ii'in#(sequent(nil, Gs), sequent(Left, cons(p(V), Right))) | | reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1#(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) |
| reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)) | | reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) |
| reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF) | | reduce'ii'in#(sequent(nil, nil), sequent(F1, F2)) | → | intersect'ii'in#(F1, F2) |
| u'12'1#(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) | | reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF) | | tautology'i'in#(F) | → | reduce'ii'in#(sequent(nil, cons(F, nil)), sequent(nil, nil)) |
| reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF) |
| reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF) | | reduce'ii'in#(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1#(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| reduce'ii'in#(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1#(intersect'ii'in(F1, F2)) | | tautology'i'in#(F) | → | u'16'1#(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) |
| reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1#(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF) |
| intersect'ii'in#(Xs, cons(X0, Ys)) | → | intersect'ii'in#(Xs, Ys) | | u'12'1#(reduce'ii'out, Fs, G2, Gs, NF) | → | reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, u'11'1, x'2a, sequent, intersect'ii'out, u'5'1, u'9'1, u'14'1, u'12'1, u'4'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, u'8'1, nil
Strategy
The following SCCs where found
| intersect'ii'in#(cons(X0, Xs), Ys) → intersect'ii'in#(Xs, Ys) | intersect'ii'in#(Xs, cons(X0, Ys)) → intersect'ii'in#(Xs, Ys) |
| reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)) | reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) → reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF) |
| reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) → reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF) | reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF) |
| reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) → reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF) | reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) → reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF) |
| reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF) | reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF) |
| reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) → reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF) | reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF) |
| u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) → reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) | reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) |
| reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) → reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF) | reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| reduce'ii'in#(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → reduce'ii'in#(sequent(nil, Gs), sequent(Left, cons(p(V), Right))) | u'12'1#(reduce'ii'out, Fs, G2, Gs, NF) → reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| intersect'ii'in#(cons(X0, Xs), Ys) | → | intersect'ii'in#(Xs, Ys) | | intersect'ii'in#(Xs, cons(X0, Ys)) | → | intersect'ii'in#(Xs, Ys) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, u'11'1, x'2a, sequent, intersect'ii'out, u'5'1, u'9'1, u'14'1, u'12'1, u'4'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, u'8'1, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| intersect'ii'in#(cons(X0, Xs), Ys) | → | intersect'ii'in#(Xs, Ys) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| intersect'ii'in#(Xs, cons(X0, Ys)) | → | intersect'ii'in#(Xs, Ys) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, x'2a, u'11'1, sequent, intersect'ii'out, u'5'1, u'14'1, u'9'1, u'4'1, u'12'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, nil, u'8'1
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| intersect'ii'in#(Xs, cons(X0, Ys)) | → | intersect'ii'in#(Xs, Ys) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)) | | reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF) |
| reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF) | | reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF) |
| reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF) |
| reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF) | | reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF) |
| reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF) | | reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF) |
| u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) | → | reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) |
| reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF) | | reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| reduce'ii'in#(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | reduce'ii'in#(sequent(nil, Gs), sequent(Left, cons(p(V), Right))) | | u'12'1#(reduce'ii'out, Fs, G2, Gs, NF) | → | reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, u'11'1, x'2a, sequent, intersect'ii'out, u'5'1, u'9'1, u'14'1, u'12'1, u'4'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, u'8'1, nil
Strategy
Polynomial Interpretation
- cons(x,y): y + x
- if(x,y): 2y + x
- iff(x,y): 3y + 3x
- intersect'ii'in(x,y): 0
- intersect'ii'out: 1
- nil: 0
- p(x): 1
- reduce'ii'in(x,y): 0
- reduce'ii'in#(x,y): x
- reduce'ii'out: 0
- sequent(x,y): 2y + x
- tautology'i'in(x): 0
- tautology'i'out: 0
- u'1'1(x): 0
- u'10'1(x): 2
- u'11'1(x): 1
- u'12'1(x1,x2,x3,x4,x5): 3x5 + 3x4 + 2x2 + 1
- u'12'1#(x1,x2,x3,x4,x5): 2x4 + 2x3 + x2
- u'12'2(x): 0
- u'13'1(x): 0
- u'14'1(x): 2
- u'15'1(x): 2x
- u'16'1(x): 0
- u'2'1(x): 0
- u'3'1(x): 2
- u'4'1(x): 0
- u'5'1(x): 2
- u'6'1(x1,x2,x3,x4,x5): x5 + x4 + 3x3 + 3x2 + 3
- u'6'1#(x1,x2,x3,x4,x5): 2x4 + x3 + x2
- u'6'2(x): 1
- u'7'1(x): 0
- u'8'1(x): 2
- u'9'1(x): 1
- x'2a(x,y): y + x
- x'2b(x,y): y + x
- x'2d(x): 2x
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)) | | reduce'ii'in#(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | reduce'ii'in#(sequent(nil, Gs), sequent(Left, cons(p(V), Right))) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF) | | reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF) |
| reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF) |
| reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF) |
| reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF) | | reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF) |
| reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF) | | u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) | → | reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) |
| reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF) |
| reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) | | u'12'1#(reduce'ii'out, Fs, G2, Gs, NF) | → | reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, x'2a, u'11'1, sequent, intersect'ii'out, u'5'1, u'14'1, u'9'1, u'4'1, u'12'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, nil, u'8'1
Strategy
Polynomial Interpretation
- cons(x,y): y + x
- if(x,y): y + x
- iff(x,y): 3y + 3x + 1
- intersect'ii'in(x,y): 0
- intersect'ii'out: 0
- nil: 0
- p(x): x
- reduce'ii'in(x,y): 2y + 1
- reduce'ii'in#(x,y): 2x
- reduce'ii'out: 0
- sequent(x,y): y + x
- tautology'i'in(x): 0
- tautology'i'out: 0
- u'1'1(x): 2
- u'10'1(x): 0
- u'11'1(x): 1
- u'12'1(x1,x2,x3,x4,x5): 3x5 + 3x4 + 3x3 + 3x2 + 2
- u'12'1#(x1,x2,x3,x4,x5): 2x4 + 2x3 + 2x2
- u'12'2(x): 0
- u'13'1(x): 2
- u'14'1(x): 2x
- u'15'1(x): 0
- u'16'1(x): 0
- u'2'1(x): 1
- u'3'1(x): 2
- u'4'1(x): 1
- u'5'1(x): 3
- u'6'1(x1,x2,x3,x4,x5): 2x4 + x2
- u'6'1#(x1,x2,x3,x4,x5): 2x4 + 2x3 + 2x2
- u'6'2(x): 0
- u'7'1(x): 0
- u'8'1(x): 1
- u'9'1(x): 0
- x'2a(x,y): y + 2x
- x'2b(x,y): y + x
- x'2d(x): x
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF) | | reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF) |
Problem 6: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF) | | reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF) |
| u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) | → | reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) |
| reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF) | | reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF) |
| reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF) |
| reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF) | | reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF) | | u'12'1#(reduce'ii'out, Fs, G2, Gs, NF) | → | reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, u'11'1, x'2a, sequent, intersect'ii'out, u'5'1, u'9'1, u'14'1, u'12'1, u'4'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, u'8'1, nil
Strategy
Polynomial Interpretation
- cons(x,y): y + x
- if(x,y): 2y + x + 1
- iff(x,y): 2
- intersect'ii'in(x,y): 0
- intersect'ii'out: 0
- nil: 0
- p(x): 2
- reduce'ii'in(x,y): 0
- reduce'ii'in#(x,y): x
- reduce'ii'out: 0
- sequent(x,y): y + x
- tautology'i'in(x): 0
- tautology'i'out: 0
- u'1'1(x): 0
- u'10'1(x): 0
- u'11'1(x): 0
- u'12'1(x1,x2,x3,x4,x5): x5 + 3x4 + x3 + 3x2
- u'12'1#(x1,x2,x3,x4,x5): x4 + x3 + x2
- u'12'2(x): 1
- u'13'1(x): 0
- u'14'1(x): 1
- u'15'1(x): 0
- u'16'1(x): 0
- u'2'1(x): 1
- u'3'1(x): 0
- u'4'1(x): 0
- u'5'1(x): 0
- u'6'1(x1,x2,x3,x4,x5): 3x5 + 3x4 + x3 + 3x2
- u'6'1#(x1,x2,x3,x4,x5): x4 + x3 + x2
- u'6'2(x): 1
- u'7'1(x): 2
- u'8'1(x): 0
- u'9'1(x): 0
- x'2a(x,y): 2y + x
- x'2b(x,y): y + 2x
- x'2d(x): x
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF) | | reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF) |
Problem 7: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF) | | u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) | → | reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) |
| reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF) |
| reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF) |
| reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF) | | reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF) | | u'12'1#(reduce'ii'out, Fs, G2, Gs, NF) | → | reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, x'2a, u'11'1, sequent, intersect'ii'out, u'5'1, u'14'1, u'9'1, u'4'1, u'12'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, nil, u'8'1
Strategy
Polynomial Interpretation
- cons(x,y): y + x
- if(x,y): y + 3x
- iff(x,y): 2y + 1
- intersect'ii'in(x,y): 0
- intersect'ii'out: 0
- nil: 0
- p(x): 2
- reduce'ii'in(x,y): 0
- reduce'ii'in#(x,y): 2x
- reduce'ii'out: 0
- sequent(x,y): y + x
- tautology'i'in(x): 0
- tautology'i'out: 0
- u'1'1(x): 1
- u'10'1(x): 0
- u'11'1(x): 0
- u'12'1(x1,x2,x3,x4,x5): 3x5 + 3x4 + 3x3 + 3x2
- u'12'1#(x1,x2,x3,x4,x5): 2x4 + 2x3 + 2x2
- u'12'2(x): 0
- u'13'1(x): 2
- u'14'1(x): 1
- u'15'1(x): 0
- u'16'1(x): 0
- u'2'1(x): 3
- u'3'1(x): 0
- u'4'1(x): 1
- u'5'1(x): 0
- u'6'1(x1,x2,x3,x4,x5): x5 + 3x4 + 3x3 + x2
- u'6'1#(x1,x2,x3,x4,x5): 2x4 + 2x3 + 2x2
- u'6'2(x): 3
- u'7'1(x): 0
- u'8'1(x): 0
- u'9'1(x): 0
- x'2a(x,y): y + 2x + 1
- x'2b(x,y): y + 3x
- x'2d(x): x + 1
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) |
| reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF) |
| reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) | → | reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF) |
| reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) | | reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF) |
| u'12'1#(reduce'ii'out, Fs, G2, Gs, NF) | → | reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, u'11'1, x'2a, sequent, intersect'ii'out, u'5'1, u'9'1, u'14'1, u'12'1, u'4'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, u'8'1, nil
Strategy
The following SCCs where found
| u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) → reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) | reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF) |
| reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) | reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF) |
Problem 9: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) | → | reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF) |
| reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) | | reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, u'11'1, x'2a, sequent, intersect'ii'out, u'5'1, u'9'1, u'14'1, u'12'1, u'4'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, u'8'1, nil
Strategy
Polynomial Interpretation
- cons(x,y): x
- if(x,y): 0
- iff(x,y): y + 2
- intersect'ii'in(x,y): y
- intersect'ii'out: 0
- nil: 2
- p(x): 2x + 2
- reduce'ii'in(x,y): 1
- reduce'ii'in#(x,y): 2x
- reduce'ii'out: 0
- sequent(x,y): x
- tautology'i'in(x): 0
- tautology'i'out: 0
- u'1'1(x): 2x + 1
- u'10'1(x): 1
- u'11'1(x): x
- u'12'1(x1,x2,x3,x4,x5): 1
- u'12'2(x): 0
- u'13'1(x): 0
- u'14'1(x): 0
- u'15'1(x): 0
- u'16'1(x): 0
- u'2'1(x): 3
- u'3'1(x): x
- u'4'1(x): 0
- u'5'1(x): 0
- u'6'1(x1,x2,x3,x4,x5): 0
- u'6'1#(x1,x2,x3,x4,x5): 2x2 + 2x1
- u'6'2(x): 0
- u'7'1(x): 0
- u'8'1(x): 0
- u'9'1(x): x
- x'2a(x,y): 2x + 2
- x'2b(x,y): 2y + x + 1
- x'2d(x): 1
Improved Usable rules
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'5'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'8'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'7'1(reduce'ii'out) | → | reduce'ii'out | | u'14'1(reduce'ii'out) | → | reduce'ii'out |
| u'9'1(reduce'ii'out) | → | reduce'ii'out | | u'12'2(reduce'ii'out) | → | reduce'ii'out |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) |
| reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'10'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | u'3'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) | | u'4'1(reduce'ii'out) | → | reduce'ii'out |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF) |
Problem 10: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) | → | reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) | | reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF) |
| reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, x'2a, u'11'1, sequent, intersect'ii'out, u'5'1, u'14'1, u'9'1, u'4'1, u'12'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, nil, u'8'1
Strategy
Polynomial Interpretation
- cons(x,y): 2x
- if(x,y): 0
- iff(x,y): x
- intersect'ii'in(x,y): 2
- intersect'ii'out: 2
- nil: 1
- p(x): 0
- reduce'ii'in(x,y): x
- reduce'ii'in#(x,y): x
- reduce'ii'out: 0
- sequent(x,y): y
- tautology'i'in(x): 0
- tautology'i'out: 0
- u'1'1(x): 2
- u'10'1(x): 0
- u'11'1(x): 0
- u'12'1(x1,x2,x3,x4,x5): 3x5 + 2x4 + 2x2
- u'12'2(x): 3
- u'13'1(x): 2x
- u'14'1(x): 0
- u'15'1(x): x + 1
- u'16'1(x): 0
- u'2'1(x): x
- u'3'1(x): 3
- u'4'1(x): 0
- u'5'1(x): 0
- u'6'1(x1,x2,x3,x4,x5): 3x5 + 3x4 + 3x3 + 3x2
- u'6'1#(x1,x2,x3,x4,x5): x4
- u'6'2(x): 0
- u'7'1(x): 1
- u'8'1(x): 0
- u'9'1(x): 1
- x'2a(x,y): 1
- x'2b(x,y): y + 2x + 1
- x'2d(x): 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF) |
Problem 11: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) | → | reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) | | reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, u'11'1, x'2a, sequent, intersect'ii'out, u'5'1, u'9'1, u'14'1, u'12'1, u'4'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, u'8'1, nil
Strategy
Polynomial Interpretation
- cons(x,y): x
- if(x,y): 2x
- iff(x,y): 2x
- intersect'ii'in(x,y): 0
- intersect'ii'out: 0
- nil: 1
- p(x): 0
- reduce'ii'in(x,y): y + 1
- reduce'ii'in#(x,y): x
- reduce'ii'out: 0
- sequent(x,y): x + 2
- tautology'i'in(x): 0
- tautology'i'out: 0
- u'1'1(x): 0
- u'10'1(x): 0
- u'11'1(x): 0
- u'12'1(x1,x2,x3,x4,x5): 3x5 + 3x4 + 3x3 + 3x2
- u'12'2(x): 0
- u'13'1(x): 0
- u'14'1(x): 0
- u'15'1(x): 0
- u'16'1(x): 0
- u'2'1(x): 0
- u'3'1(x): 0
- u'4'1(x): 0
- u'5'1(x): 0
- u'6'1(x1,x2,x3,x4,x5): 3x5 + 3x4 + 2x3 + 3x2
- u'6'1#(x1,x2,x3,x4,x5): 3x2 + 3
- u'6'2(x): 0
- u'7'1(x): 1
- u'8'1(x): 0
- u'9'1(x): 1
- x'2a(x,y): 2y
- x'2b(x,y): 3y + 1
- x'2d(x): 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| u'6'1#(reduce'ii'out, F2, Fs, Gs, NF) | → | reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF) |
Problem 12: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
Rewrite Rules
| intersect'ii'in(cons(X, X0), cons(X, X1)) | → | intersect'ii'out | | intersect'ii'in(Xs, cons(X0, Ys)) | → | u'1'1(intersect'ii'in(Xs, Ys)) |
| u'1'1(intersect'ii'out) | → | intersect'ii'out | | intersect'ii'in(cons(X0, Xs), Ys) | → | u'2'1(intersect'ii'in(Xs, Ys)) |
| u'2'1(intersect'ii'out) | → | intersect'ii'out | | reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) | → | u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) |
| u'3'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) | → | u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) |
| u'4'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) | → | u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) |
| u'5'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) | → | u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) |
| u'6'1(reduce'ii'out, F2, Fs, Gs, NF) | → | u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) | | u'6'2(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) | → | u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) | | u'7'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) | → | u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) | | u'8'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) | → | u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) | | u'9'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) | → | u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) | | u'10'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) | → | u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) | | u'11'1(reduce'ii'out) | → | reduce'ii'out |
| reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) | → | u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) | | u'12'1(reduce'ii'out, Fs, G2, Gs, NF) | → | u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) |
| u'12'2(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) | → | u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) |
| u'13'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) | → | u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right)))) |
| u'14'1(reduce'ii'out) | → | reduce'ii'out | | reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) | → | u'15'1(intersect'ii'in(F1, F2)) |
| u'15'1(intersect'ii'out) | → | reduce'ii'out | | tautology'i'in(F) | → | u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil))) |
| u'16'1(reduce'ii'out) | → | tautology'i'out |
Original Signature
Termination of terms over the following signature is verified: x'2b, x'2a, u'11'1, sequent, intersect'ii'out, u'5'1, u'14'1, u'9'1, u'4'1, u'12'1, tautology'i'out, u'12'2, u'10'1, tautology'i'in, if, u'6'2, u'6'1, intersect'ii'in, cons, u'2'1, reduce'ii'in, reduce'ii'out, u'7'1, u'16'1, u'3'1, iff, u'15'1, u'13'1, p, u'1'1, x'2d, nil, u'8'1
Strategy
There are no SCCs!