YES
0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 AND
↳5 RelADPP
↳6 RelADPCleverAfsProof (⇒, 114 ms)
↳7 QDP
↳8 MRRProof (⇔, 12 ms)
↳9 QDP
↳10 PisEmptyProof (⇔, 0 ms)
↳11 YES
↳12 RelADPP
↳13 RelADPCleverAfsProof (⇒, 122 ms)
↳14 QDP
↳15 MRRProof (⇔, 14 ms)
↳16 QDP
↳17 PisEmptyProof (⇔, 0 ms)
↳18 YES
↳19 RelADPP
↳20 RelADPReductionPairProof (⇔, 110 ms)
↳21 RelADPP
↳22 DAbsisEmptyProof (⇔, 0 ms)
↳23 YES
↳24 RelADPP
↳25 RelADPReductionPairProof (⇔, 108 ms)
↳26 RelADPP
↳27 DAbsisEmptyProof (⇔, 0 ms)
↳28 YES
↳29 RelADPP
↳30 RelADPReductionPairProof (⇔, 125 ms)
↳31 RelADPP
↳32 DAbsisEmptyProof (⇔, 0 ms)
↳33 YES
↳34 RelADPP
↳35 RelADPReductionPairProof (⇔, 108 ms)
↳36 RelADPP
↳37 DAbsisEmptyProof (⇔, 0 ms)
↳38 YES
↳39 RelADPP
↳40 RelADPReductionPairProof (⇔, 101 ms)
↳41 RelADPP
↳42 DAbsisEmptyProof (⇔, 0 ms)
↳43 YES
↳44 RelADPP
↳45 RelADPReductionPairProof (⇔, 111 ms)
↳46 RelADPP
↳47 DAbsisEmptyProof (⇔, 0 ms)
↳48 YES
remove(nil, x) → nil
remove(cons(x, xs), 0) → cons(x, xs)
remove(cons(x, xs), s(y)) → remove(xs, y)
first(nil, x) → nil
first(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
consSwap(x, xs) → cons(x, xs)
sublist(cons(x, xs), z) → sublist(consSwap(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].
remove(nil, x) → nil
remove(cons(x, xs), 0) → cons(x, xs)
remove(cons(x, xs), s(y)) → REMOVE(xs, y)
first(nil, x) → nil
first(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, FIRST(xs, y))
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
sublist(cons(x, xs), s(y)) → cons(cons(x, FIRST(xs, y)), sublist(remove(xs, y), s(y)))
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), SUBLIST(remove(xs, y), s(y)))
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(REMOVE(xs, y), s(y)))
consSwap(x, xs) → cons(x, xs)
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, CONSSWAP(x, xs))
We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
3 SCCs with nodes from P_abs,
5 Lassos,
Result: This relative DT problem is equivalent to 8 subproblems.
remove(cons(x, xs), s(y)) → REMOVE(xs, y)
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
sublist(cons(x, xs), z) → sublist(consSwap(x, xs), z)
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
first(cons(x, xs), 0) → nil
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
REMOVE_2 =
0 =
remove_2 = 1
cons_2 = 0
first_2 = 0, 1
sublist_2 = 0
consSwap_2 = 0
nil =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
REMOVE(x1, x2) = REMOVE(x1, x2)
cons(x1, x2) = x2
s(x1) = s(x1)
sublist(x1, x2) = x2
first(x1, x2) = first
remove(x1, x2) = remove(x1)
0 = 0
nil = nil
consSwap(x1, x2) = x2
Recursive path order with status [RPO].
Quasi-Precedence:
REMOVE2 > [remove1, nil]
[s1, first] > [remove1, nil]
0 > [remove1, nil]
REMOVE2: multiset
s1: multiset
first: []
remove1: [1]
0: multiset
nil: multiset
REMOVE0(cons(xs), s0(y)) → REMOVE0(xs, y)
consSwap(xs) → cons(xs)
remove(cons(xs)) → cons(xs)
sublist(s0(y)) → cons(sublist(s0(y)))
first → nil0
remove(nil0) → nil0
sublist(x) → nil0
sublist(00) → nil0
sublist(z) → sublist(z)
first → cons(first)
consSwap(cons(xs)) → cons(consSwap(xs))
remove(cons(xs)) → remove(xs)
REMOVE0(cons(xs), s0(y)) → REMOVE0(xs, y)
consSwap(xs) → cons(xs)
remove(cons(xs)) → cons(xs)
first → nil0
remove(nil0) → nil0
sublist(x) → nil0
sublist(00) → nil0
POL(00) = 2
POL(REMOVE0(x1, x2)) = x1 + x2
POL(cons(x1)) = x1
POL(consSwap(x1)) = 2 + 2·x1
POL(first) = 1
POL(nil0) = 0
POL(remove(x1)) = 2 + x1
POL(s0(x1)) = 1 + x1
POL(sublist(x1)) = 1 + 2·x1
sublist(s0(y)) → cons(sublist(s0(y)))
sublist(z) → sublist(z)
first → cons(first)
consSwap(cons(xs)) → cons(consSwap(xs))
remove(cons(xs)) → remove(xs)
first(cons(x, xs), s(y)) → cons(x, FIRST(xs, y))
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
sublist(cons(x, xs), z) → sublist(consSwap(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
FIRST_2 =
0 =
cons_2 = 0
remove_2 = 1
first_2 = 0, 1
sublist_2 = 0
consSwap_2 = 0
nil =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
FIRST(x1, x2) = FIRST(x1, x2)
cons(x1, x2) = x2
s(x1) = s(x1)
sublist(x1, x2) = x2
first(x1, x2) = first
remove(x1, x2) = remove(x1)
0 = 0
nil = nil
consSwap(x1, x2) = x2
Recursive path order with status [RPO].
Quasi-Precedence:
FIRST2 > [remove1, nil]
[s1, first] > [remove1, nil]
0 > [remove1, nil]
FIRST2: multiset
s1: multiset
first: []
remove1: [1]
0: multiset
nil: multiset
FIRST0(cons(xs), s0(y)) → FIRST0(xs, y)
consSwap(xs) → cons(xs)
remove(cons(xs)) → cons(xs)
sublist(s0(y)) → cons(sublist(s0(y)))
first → nil0
remove(nil0) → nil0
sublist(x) → nil0
sublist(00) → nil0
sublist(z) → sublist(z)
first → cons(first)
consSwap(cons(xs)) → cons(consSwap(xs))
remove(cons(xs)) → remove(xs)
FIRST0(cons(xs), s0(y)) → FIRST0(xs, y)
consSwap(xs) → cons(xs)
remove(cons(xs)) → cons(xs)
first → nil0
remove(nil0) → nil0
sublist(x) → nil0
sublist(00) → nil0
POL(00) = 2
POL(FIRST0(x1, x2)) = x1 + x2
POL(cons(x1)) = x1
POL(consSwap(x1)) = 2 + 2·x1
POL(first) = 1
POL(nil0) = 0
POL(remove(x1)) = 2 + x1
POL(s0(x1)) = 1 + x1
POL(sublist(x1)) = 1 + 2·x1
sublist(s0(y)) → cons(sublist(s0(y)))
sublist(z) → sublist(z)
first → cons(first)
consSwap(cons(xs)) → cons(consSwap(xs))
remove(cons(xs)) → remove(xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), SUBLIST(remove(xs, y), s(y)))
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), SUBLIST(remove(xs, y), s(y)))
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
POL(0) = 0
POL(CONSSWAP(x1, x2)) = 0
POL(FIRST(x1, x2)) = 2 + x1·x2 + x2
POL(REMOVE(x1, x2)) = 2
POL(SUBLIST(x1, x2)) = 2 + 3·x1
POL(cons(x1, x2)) = 1 + x2
POL(consSwap(x1, x2)) = 1 + x2
POL(first(x1, x2)) = x1
POL(nil) = 0
POL(remove(x1, x2)) = x1
POL(s(x1)) = 3
POL(sublist(x1, x2)) = 2·x1 + 3·x2
consSwap(x, xs) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
remove(cons(x, xs), 0) → cons(x, xs)
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
sublist(cons(x, xs), 0) → nil
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:
sublist(cons(x, xs), 0) → nil
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
POL(0) = 0
POL(CONSSWAP(x1, x2)) = 0
POL(FIRST(x1, x2)) = x2
POL(REMOVE(x1, x2)) = 2
POL(SUBLIST(x1, x2)) = 2·x1
POL(cons(x1, x2)) = 1
POL(consSwap(x1, x2)) = 1
POL(first(x1, x2)) = 3·x2
POL(nil) = 0
POL(remove(x1, x2)) = 1
POL(s(x1)) = 2 + 2·x1
POL(sublist(x1, x2)) = 2 + 2·x1
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
sublist(nil, x) → nil
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:
sublist(nil, x) → nil
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
POL(0) = 0
POL(CONSSWAP(x1, x2)) = 0
POL(FIRST(x1, x2)) = 2 + 2·x1
POL(REMOVE(x1, x2)) = 2
POL(SUBLIST(x1, x2)) = 1 + 2·x1
POL(cons(x1, x2)) = 1
POL(consSwap(x1, x2)) = 1
POL(first(x1, x2)) = 2·x2
POL(nil) = 0
POL(remove(x1, x2)) = 1
POL(s(x1)) = 3 + x1
POL(sublist(x1, x2)) = 3·x2
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(REMOVE(xs, y), s(y)))
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(REMOVE(xs, y), s(y)))
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
POL(0) = 0
POL(CONSSWAP(x1, x2)) = 0
POL(FIRST(x1, x2)) = 2
POL(REMOVE(x1, x2)) = 1 + 2·x1
POL(SUBLIST(x1, x2)) = 2 + 3·x1 + 3·x2
POL(cons(x1, x2)) = 1 + 3·x2
POL(consSwap(x1, x2)) = 1 + 3·x2
POL(first(x1, x2)) = x1
POL(nil) = 0
POL(remove(x1, x2)) = x1
POL(s(x1)) = 3
POL(sublist(x1, x2)) = x1
consSwap(x, xs) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
remove(cons(x, xs), 0) → cons(x, xs)
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), SUBLIST(remove(xs, y), s(y)))
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), SUBLIST(remove(xs, y), s(y)))
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
POL(0) = 0
POL(CONSSWAP(x1, x2)) = 0
POL(FIRST(x1, x2)) = 2 + x1·x2 + x2
POL(REMOVE(x1, x2)) = 2
POL(SUBLIST(x1, x2)) = 2 + 3·x1
POL(cons(x1, x2)) = 1 + x2
POL(consSwap(x1, x2)) = 1 + x2
POL(first(x1, x2)) = x1
POL(nil) = 0
POL(remove(x1, x2)) = x1
POL(s(x1)) = 3
POL(sublist(x1, x2)) = 2·x1 + 3·x2
consSwap(x, xs) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
remove(cons(x, xs), 0) → cons(x, xs)
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
sublist(cons(x, xs), s(y)) → cons(cons(x, FIRST(xs, y)), sublist(remove(xs, y), s(y)))
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:
sublist(cons(x, xs), s(y)) → cons(cons(x, FIRST(xs, y)), sublist(remove(xs, y), s(y)))
consSwap(x, xs) → cons(x, xs)
remove(cons(x, xs), 0) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil
POL(0) = 1
POL(CONSSWAP(x1, x2)) = 0
POL(FIRST(x1, x2)) = 1
POL(REMOVE(x1, x2)) = x2
POL(SUBLIST(x1, x2)) = 1 + 2·x1 + 3·x2
POL(cons(x1, x2)) = 1
POL(consSwap(x1, x2)) = 1
POL(first(x1, x2)) = x1
POL(nil) = 1
POL(remove(x1, x2)) = 1
POL(s(x1)) = 3 + 2·x1
POL(sublist(x1, x2)) = 2·x1 + 2·x2
consSwap(x, xs) → cons(x, xs)
sublist(cons(x, xs), s(y)) → cons(cons(x, first(xs, y)), sublist(remove(xs, y), s(y)))
remove(cons(x, xs), 0) → cons(x, xs)
first(nil, x) → nil
remove(nil, x) → nil
sublist(nil, x) → nil
sublist(cons(x, xs), 0) → nil
first(cons(x, xs), s(y)) → cons(x, first(xs, y))
sublist(cons(x, xs), z) → SUBLIST(CONSSWAP(x, xs), z)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
remove(cons(x, xs), s(y)) → remove(xs, y)
first(cons(x, xs), 0) → nil