YES
0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 62 ms)
↳4 AND
↳5 RelADPP
↳6 RelADPCleverAfsProof (⇒, 87 ms)
↳7 QDP
↳8 MRRProof (⇔, 2 ms)
↳9 QDP
↳10 MRRProof (⇔, 2 ms)
↳11 QDP
↳12 PisEmptyProof (⇔, 0 ms)
↳13 YES
↳14 RelADPP
↳15 RelADPCleverAfsProof (⇒, 59 ms)
↳16 QDP
↳17 MRRProof (⇔, 23 ms)
↳18 QDP
↳19 QDPOrderProof (⇔, 3 ms)
↳20 QDP
↳21 PisEmptyProof (⇔, 0 ms)
↳22 YES
↳23 RelADPP
↳24 RelADPReductionPairProof (⇔, 228 ms)
↳25 RelADPP
↳26 RelADPReductionPairProof (⇔, 44 ms)
↳27 RelADPP
↳28 DAbsisEmptyProof (⇔, 0 ms)
↳29 YES
↳30 RelADPP
↳31 RelADPReductionPairProof (⇔, 164 ms)
↳32 RelADPP
↳33 DAbsisEmptyProof (⇔, 0 ms)
↳34 YES
↳35 RelADPP
↳36 RelADPReductionPairProof (⇔, 201 ms)
↳37 RelADPP
↳38 DAbsisEmptyProof (⇔, 0 ms)
↳39 YES
↳40 RelADPP
↳41 RelADPReductionPairProof (⇔, 164 ms)
↳42 RelADPP
↳43 DAbsisEmptyProof (⇔, 0 ms)
↳44 YES
↳45 RelADPP
↳46 RelADPReductionPairProof (⇔, 269 ms)
↳47 RelADPP
↳48 DAbsisEmptyProof (⇔, 0 ms)
↳49 YES
↳50 RelADPP
↳51 RelADPReductionPairProof (⇔, 162 ms)
↳52 RelADPP
↳53 DAbsisEmptyProof (⇔, 0 ms)
↳54 YES
↳55 RelADPP
↳56 RelADPReductionPairProof (⇔, 150 ms)
↳57 RelADPP
↳58 DAbsisEmptyProof (⇔, 0 ms)
↳59 YES
↳60 RelADPP
↳61 RelADPReductionPairProof (⇔, 273 ms)
↳62 RelADPP
↳63 RelADPDepGraphProof (⇔, 0 ms)
↳64 TRUE
↳65 RelADPP
↳66 RelADPReductionPairProof (⇔, 142 ms)
↳67 RelADPP
↳68 DAbsisEmptyProof (⇔, 0 ms)
↳69 YES
↳70 RelADPP
↳71 RelADPReductionPairProof (⇔, 188 ms)
↳72 RelADPP
↳73 DAbsisEmptyProof (⇔, 0 ms)
↳74 YES
↳75 RelADPP
↳76 RelADPReductionPairProof (⇔, 159 ms)
↳77 RelADPP
↳78 DAbsisEmptyProof (⇔, 0 ms)
↳79 YES
↳80 RelADPP
↳81 RelADPReductionPairProof (⇔, 249 ms)
↳82 RelADPP
↳83 DAbsisEmptyProof (⇔, 0 ms)
↳84 YES
↳85 RelADPP
↳86 RelADPReductionPairProof (⇔, 243 ms)
↳87 RelADPP
↳88 DAbsisEmptyProof (⇔, 0 ms)
↳89 YES
↳90 RelADPP
↳91 RelADPReductionPairProof (⇔, 231 ms)
↳92 RelADPP
↳93 RelADPCleverAfsProof (⇒, 0 ms)
↳94 QDP
↳95 MRRProof (⇔, 0 ms)
↳96 QDP
↳97 QDPOrderProof (⇔, 0 ms)
↳98 QDP
↳99 PisEmptyProof (⇔, 0 ms)
↳100 YES
↳101 RelADPP
↳102 RelADPReductionPairProof (⇔, 202 ms)
↳103 RelADPP
↳104 DAbsisEmptyProof (⇔, 0 ms)
↳105 YES
↳106 RelADPP
↳107 RelADPReductionPairProof (⇔, 192 ms)
↳108 RelADPP
↳109 RelADPReductionPairProof (⇔, 23 ms)
↳110 RelADPP
↳111 DAbsisEmptyProof (⇔, 0 ms)
↳112 YES
↳113 RelADPP
↳114 RelADPReductionPairProof (⇔, 221 ms)
↳115 RelADPP
↳116 DAbsisEmptyProof (⇔, 0 ms)
↳117 YES
↳118 RelADPP
↳119 RelADPReductionPairProof (⇔, 301 ms)
↳120 RelADPP
↳121 DAbsisEmptyProof (⇔, 0 ms)
↳122 YES
↳123 RelADPP
↳124 RelADPReductionPairProof (⇔, 183 ms)
↳125 RelADPP
↳126 RelADPDepGraphProof (⇔, 0 ms)
↳127 TRUE
↳128 RelADPP
↳129 RelADPReductionPairProof (⇔, 152 ms)
↳130 RelADPP
↳131 DAbsisEmptyProof (⇔, 0 ms)
↳132 YES
↳133 RelADPP
↳134 RelADPReductionPairProof (⇔, 222 ms)
↳135 RelADPP
↳136 DAbsisEmptyProof (⇔, 0 ms)
↳137 YES
↳138 RelADPP
↳139 RelADPReductionPairProof (⇔, 310 ms)
↳140 RelADPP
↳141 DAbsisEmptyProof (⇔, 0 ms)
↳142 YES
↳143 RelADPP
↳144 RelADPReductionPairProof (⇔, 224 ms)
↳145 RelADPP
↳146 DAbsisEmptyProof (⇔, 0 ms)
↳147 YES
↳148 RelADPP
↳149 RelADPReductionPairProof (⇔, 199 ms)
↳150 RelADPP
↳151 RelADPReductionPairProof (⇔, 35 ms)
↳152 RelADPP
↳153 DAbsisEmptyProof (⇔, 0 ms)
↳154 YES
↳155 RelADPP
↳156 RelADPReductionPairProof (⇔, 268 ms)
↳157 RelADPP
↳158 DAbsisEmptyProof (⇔, 0 ms)
↳159 YES
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
s(pred(x)) → pred(s(x))
log(s(0)) → 0
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
pred(s(x)) → x
We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].
minus(x, 0) → x
minus(x, s(y)) → PRED(minus(x, y))
minus(x, s(y)) → pred(MINUS(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → S(quot(minus(x, y), s(y)))
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
s(pred(x)) → PRED(S(x))
log(s(0)) → 0
pred(s(x)) → S(PRED(x))
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
log(s(s(x))) → S(log(S(quot(x, s(s(0))))))
log(s(s(x))) → S(log(s(QUOT(x, s(s(0))))))
log(s(s(x))) → S(log(s(quot(x, S(s(0))))))
log(s(s(x))) → S(log(s(quot(x, s(S(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(s(x))) → s(log(S(QUOT(x, s(s(0))))))
log(s(s(x))) → s(log(S(quot(x, S(s(0))))))
log(s(s(x))) → s(log(S(quot(x, s(S(0))))))
log(s(s(x))) → s(log(s(QUOT(x, S(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, s(S(0))))))
log(s(s(x))) → s(log(s(quot(x, S(S(0))))))
pred(s(x)) → x
We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
2 SCCs with nodes from P_abs,
25 Lassos,
Result: This relative DT problem is equivalent to 27 subproblems.
minus(x, s(y)) → pred(MINUS(x, y))
s(pred(x)) → pred(s(x))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
MINUS_2 = 0
log_1 =
pred_1 =
0 =
minus_2 = 1
quot_2 = 1
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
MINUS(x1, x2) = MINUS(x2)
s(x1) = s(x1)
quot(x1, x2) = quot(x1)
minus(x1, x2) = minus(x1)
pred(x1) = x1
0 = 0
Recursive path order with status [RPO].
Quasi-Precedence:
MINUS1 > minus1
quot1 > s1 > minus1
0 > minus1
MINUS1: multiset
s1: [1]
quot1: [1]
minus1: [1]
0: multiset
MINUS(s0(y)) → MINUS(y)
s0(pred0(x)) → pred0(s0(x))
log0(s0(00)) → 00
quot(s0(x)) → s0(quot(minus(x)))
minus(x) → pred0(minus(x))
pred0(s0(x)) → s0(pred0(x))
log0(s0(s0(x))) → s0(log0(s0(quot(x))))
minus(x) → x
quot(00) → 00
pred0(s0(x)) → x
log0(s0(00)) → 00
POL(00) = 2
POL(MINUS(x1)) = x1
POL(log0(x1)) = x1
POL(minus(x1)) = x1
POL(pred0(x1)) = x1
POL(quot(x1)) = x1
POL(s0(x1)) = 2·x1
MINUS(s0(y)) → MINUS(y)
s0(pred0(x)) → pred0(s0(x))
quot(s0(x)) → s0(quot(minus(x)))
minus(x) → pred0(minus(x))
pred0(s0(x)) → s0(pred0(x))
log0(s0(s0(x))) → s0(log0(s0(quot(x))))
minus(x) → x
quot(00) → 00
pred0(s0(x)) → x
MINUS(s0(y)) → MINUS(y)
pred0(s0(x)) → x
POL(00) = 2
POL(MINUS(x1)) = x1
POL(log0(x1)) = x1
POL(minus(x1)) = x1
POL(pred0(x1)) = x1
POL(quot(x1)) = x1
POL(s0(x1)) = 1 + 2·x1
s0(pred0(x)) → pred0(s0(x))
quot(s0(x)) → s0(quot(minus(x)))
minus(x) → pred0(minus(x))
pred0(s0(x)) → s0(pred0(x))
log0(s0(s0(x))) → s0(log0(s0(quot(x))))
minus(x) → x
quot(00) → 00
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
s(pred(x)) → pred(s(x))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
QUOT_2 =
log_1 =
pred_1 =
0 =
minus_2 = 1
quot_2 =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
QUOT(x1, x2) = QUOT(x1, x2)
s(x1) = s(x1)
minus(x1, x2) = minus(x1)
pred(x1) = x1
0 = 0
quot(x1, x2) = quot(x1, x2)
Recursive path order with status [RPO].
Quasi-Precedence:
[0, quot2] > [QUOT2, s1] > minus1
QUOT2: multiset
s1: multiset
minus1: multiset
0: multiset
quot2: [2,1]
QUOT0(s0(x), s0(y)) → QUOT0(minus(x), s0(y))
s0(pred0(x)) → pred0(s0(x))
log0(s0(00)) → 00
quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
minus(x) → pred0(minus(x))
pred0(s0(x)) → s0(pred0(x))
log0(s0(s0(x))) → s0(log0(s0(quot0(x, s0(s0(00))))))
minus(x) → x
quot0(00, s0(y)) → 00
pred0(s0(x)) → x
log0(s0(00)) → 00
POL(00) = 0
POL(QUOT0(x1, x2)) = 2·x1 + x2
POL(log0(x1)) = 2 + 2·x1
POL(minus(x1)) = x1
POL(pred0(x1)) = x1
POL(quot0(x1, x2)) = x1 + x2
POL(s0(x1)) = x1
QUOT0(s0(x), s0(y)) → QUOT0(minus(x), s0(y))
s0(pred0(x)) → pred0(s0(x))
quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
minus(x) → pred0(minus(x))
pred0(s0(x)) → s0(pred0(x))
log0(s0(s0(x))) → s0(log0(s0(quot0(x, s0(s0(00))))))
minus(x) → x
quot0(00, s0(y)) → 00
pred0(s0(x)) → x
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QUOT0(s0(x), s0(y)) → QUOT0(minus(x), s0(y))
QUOT02 > [s01, 00]
QUOT02: multiset
s01: multiset
00: multiset
s0(pred0(x)) → pred0(s0(x))
quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
minus(x) → pred0(minus(x))
pred0(s0(x)) → s0(pred0(x))
log0(s0(s0(x))) → s0(log0(s0(quot0(x, s0(s0(00))))))
minus(x) → x
quot0(00, s0(y)) → 00
pred0(s0(x)) → x
s0(pred0(x)) → pred0(s0(x))
quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
minus(x) → pred0(minus(x))
pred0(s0(x)) → s0(pred0(x))
log0(s0(s0(x))) → s0(log0(s0(quot0(x, s0(s0(00))))))
minus(x) → x
quot0(00, s0(y)) → 00
pred0(s0(x)) → x
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(S(QUOT(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
Relative ADPs:
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(S(QUOT(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 2 + x1
POL(MINUS(x1, x2)) = 2 + 2·x1 + 2·x2
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 0
POL(S(x1)) = 0
POL(log(x1)) = 2·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x2
POL(s(x1)) = x1
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 2 + 2·x1
POL(MINUS(x1, x2)) = 2 + 2·x1 + 2·x1·x2 + 2·x2
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 3·x1 + x2
POL(S(x1)) = 3
POL(log(x1)) = 2 + 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → S(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(S(QUOT(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → S(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(S(QUOT(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 2
POL(LOG(x1)) = 3 + 3·x1
POL(MINUS(x1, x2)) = 2 + 2·x1
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 1 + 3·x1
POL(S(x1)) = 3·x1
POL(log(x1)) = 2·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(0, s(y)) → 0
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, S(s(0))))))
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(0, s(y)) → 0
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, S(s(0))))))
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 3 + 3·x1
POL(MINUS(x1, x2)) = 2·x1
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 2·x1 + 2·x2
POL(S(x1)) = 3 + 2·x1
POL(log(x1)) = x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 2·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, S(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, S(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 2 + 2·x1
POL(MINUS(x1, x2)) = 1 + 3·x2
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 3 + x2
POL(S(x1)) = 2 + x1
POL(log(x1)) = 3 + 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(0, s(y)) → 0
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
log(s(s(x))) → S(log(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(0, s(y)) → 0
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
log(s(s(x))) → S(log(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 3 + 3·x1
POL(MINUS(x1, x2)) = 2 + 2·x1
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 3
POL(S(x1)) = 3 + 2·x1
POL(log(x1)) = x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 2·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
log(s(s(x))) → S(log(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
log(s(s(x))) → S(log(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 3 + 2·x1
POL(MINUS(x1, x2)) = 0
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 2
POL(S(x1)) = 1
POL(log(x1)) = 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = 1 + x1
POL(s(x1)) = 3 + x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → S(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, S(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → S(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, S(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 3 + 3·x1
POL(MINUS(x1, x2)) = 2 + 2·x1 + 2·x2
POL(PRED(x1)) = 2 + 2·x12
POL(QUOT(x1, x2)) = 3·x1 + x2
POL(S(x1)) = 2 + x1
POL(log(x1)) = 2·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 2·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
log(s(s(x))) → S(log(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
Relative ADPs:
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
log(s(s(x))) → S(log(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
POL(0) = 0
POL(LOG(x1)) = 2 + 3·x1
POL(MINUS(x1, x2)) = 2 + 2·x1
POL(PRED(x1)) = x12
POL(QUOT(x1, x2)) = x2
POL(S(x1)) = 3 + x1
POL(log(x1)) = 1 + 2·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
0 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 0 subproblems.
quot(0, s(y)) → 0
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(0, s(y)) → 0
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
pred(s(x)) → x
POL(0) = 0
POL(LOG(x1)) = 2 + 2·x1
POL(MINUS(x1, x2)) = 2 + 2·x1·x2
POL(PRED(x1)) = 2 + x12
POL(QUOT(x1, x2)) = 1 + x2
POL(S(x1)) = 3 + x1
POL(log(x1)) = 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 1 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 2 + 2·x1
POL(MINUS(x1, x2)) = 2 + 2·x1 + 2·x2
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 2 + x2
POL(S(x1)) = 2 + 2·x1
POL(log(x1)) = x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
POL(0) = 0
POL(LOG(x1)) = 2 + 2·x1
POL(MINUS(x1, x2)) = 0
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 3
POL(S(x1)) = 3 + x1
POL(log(x1)) = 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 1 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(S(QUOT(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(S(QUOT(x, s(s(0))))))
minus(x, 0) → x
POL(0) = 0
POL(LOG(x1)) = 2 + 3·x1
POL(MINUS(x1, x2)) = 2 + 2·x1
POL(PRED(x1)) = x12
POL(QUOT(x1, x2)) = 3 + 2·x1 + x2
POL(S(x1)) = 3 + 2·x1
POL(log(x1)) = 3 + 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → S(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, s(S(0))))))
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:
quot(s(x), s(y)) → S(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, s(S(0))))))
POL(0) = 0
POL(LOG(x1)) = 1 + 3·x1
POL(MINUS(x1, x2)) = 2 + 2·x1 + 2·x1·x2
POL(PRED(x1)) = 0
POL(QUOT(x1, x2)) = 3
POL(S(x1)) = 1
POL(log(x1)) = 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = 2 + x1
POL(s(x1)) = 3 + x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, s(S(0))))))
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:
Relative ADPs:
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, s(S(0))))))
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
POL(0) = 0
POL(LOG(x1)) = 3 + x1
POL(MINUS(x1, x2)) = 0
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 0
POL(S(x1)) = 1 + x1
POL(log(x1)) = x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 =
QUOT_2 =
log_1 =
0 =
pred_1 =
minus_2 = 1
quot_2 =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
QUOT(x1, x2) = QUOT(x1, x2)
s(x1) = s(x1)
minus(x1, x2) = minus(x1)
pred(x1) = x1
0 = 0
quot(x1, x2) = quot(x1, x2)
Recursive path order with status [RPO].
Quasi-Precedence:
[0, quot2] > [QUOT2, s1] > minus1
QUOT2: multiset
s1: multiset
minus1: multiset
0: multiset
quot2: [2,1]
QUOT0(s0(x), s0(y)) → QUOT0(minus(x), s0(y))
s0(pred0(x)) → pred0(s0(x))
log0(s0(00)) → 00
quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
minus(x) → pred0(minus(x))
pred0(s0(x)) → s0(pred0(x))
log0(s0(s0(x))) → s0(log0(s0(quot0(x, s0(s0(00))))))
minus(x) → x
quot0(00, s0(y)) → 00
pred0(s0(x)) → x
log0(s0(00)) → 00
POL(00) = 0
POL(QUOT0(x1, x2)) = 2·x1 + x2
POL(log0(x1)) = 2 + 2·x1
POL(minus(x1)) = x1
POL(pred0(x1)) = x1
POL(quot0(x1, x2)) = x1 + x2
POL(s0(x1)) = x1
QUOT0(s0(x), s0(y)) → QUOT0(minus(x), s0(y))
s0(pred0(x)) → pred0(s0(x))
quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
minus(x) → pred0(minus(x))
pred0(s0(x)) → s0(pred0(x))
log0(s0(s0(x))) → s0(log0(s0(quot0(x, s0(s0(00))))))
minus(x) → x
quot0(00, s0(y)) → 00
pred0(s0(x)) → x
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QUOT0(s0(x), s0(y)) → QUOT0(minus(x), s0(y))
POL( s0(x1) ) = x1 + 2 |
POL( pred0(x1) ) = x1 |
POL( quot0(x1, x2) ) = x1 |
POL( minus(x1) ) = x1 |
POL( log0(x1) ) = max{0, x1 - 2} |
POL( 00 ) = 1 |
POL( QUOT0(x1, x2) ) = 2x1 + 2x2 + 2 |
s0(pred0(x)) → pred0(s0(x))
quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
minus(x) → pred0(minus(x))
pred0(s0(x)) → s0(pred0(x))
log0(s0(s0(x))) → s0(log0(s0(quot0(x, s0(s0(00))))))
minus(x) → x
quot0(00, s0(y)) → 00
pred0(s0(x)) → x
s0(pred0(x)) → pred0(s0(x))
quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
minus(x) → pred0(minus(x))
pred0(s0(x)) → s0(pred0(x))
log0(s0(s0(x))) → s0(log0(s0(quot0(x, s0(s0(00))))))
minus(x) → x
quot0(00, s0(y)) → 00
pred0(s0(x)) → x
quot(s(x), s(y)) → S(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → S(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 2
POL(LOG(x1)) = 2 + 3·x1
POL(MINUS(x1, x2)) = 2·x1
POL(PRED(x1)) = 0
POL(QUOT(x1, x2)) = 3·x1
POL(S(x1)) = 2 + 2·x1
POL(log(x1)) = 1 + 2·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 2 + 3·x1
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, S(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
Relative ADPs:
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → s(log(s(QUOT(x, S(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 1
POL(MINUS(x1, x2)) = 2 + 2·x1
POL(PRED(x1)) = 0
POL(QUOT(x1, x2)) = 0
POL(S(x1)) = 0
POL(log(x1)) = 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 1 + 3·x1
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 2 + 2·x1
POL(MINUS(x1, x2)) = 2 + 2·x1 + 2·x1·x2 + 2·x2
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 3·x1 + x2
POL(S(x1)) = 3
POL(log(x1)) = 2 + 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, S(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, S(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
POL(0) = 0
POL(LOG(x1)) = 1 + 3·x1
POL(MINUS(x1, x2)) = 2 + 2·x1
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 2 + 2·x2
POL(S(x1)) = 3 + 2·x1
POL(log(x1)) = 3 + 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
quot(0, s(y)) → 0
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, s(S(0))))))
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:
quot(0, s(y)) → 0
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
pred(s(x)) → x
POL(0) = 1
POL(LOG(x1)) = 2·x1
POL(MINUS(x1, x2)) = 2 + 2·x1 + 2·x2
POL(PRED(x1)) = x12
POL(QUOT(x1, x2)) = 2·x1
POL(S(x1)) = 0
POL(log(x1)) = x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3·x1
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, s(S(0))))))
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(S(QUOT(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
Relative ADPs:
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(S(QUOT(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
POL(0) = 3
POL(LOG(x1)) = 3 + 3·x1
POL(MINUS(x1, x2)) = 3 + 2·x1
POL(PRED(x1)) = 0
POL(QUOT(x1, x2)) = x1
POL(S(x1)) = x1
POL(log(x1)) = 2 + 2·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 2·x1
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
0 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 0 subproblems.
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
log(s(s(x))) → S(log(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
log(s(s(x))) → S(log(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 2 + 2·x1
POL(MINUS(x1, x2)) = 0
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 1 + 2·x1 + x2
POL(S(x1)) = 1 + x1
POL(log(x1)) = x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(0, s(y)) → 0
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(S(QUOT(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(0, s(y)) → 0
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(S(QUOT(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 1
POL(LOG(x1)) = 2 + 3·x1
POL(MINUS(x1, x2)) = 2 + 2·x2
POL(PRED(x1)) = 2 + 3·x12
POL(QUOT(x1, x2)) = 3
POL(S(x1)) = x1
POL(log(x1)) = 2 + 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 2 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → S(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
log(s(s(x))) → S(log(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → S(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
log(s(s(x))) → S(log(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 1
POL(LOG(x1)) = 3·x1
POL(MINUS(x1, x2)) = 2
POL(PRED(x1)) = 0
POL(QUOT(x1, x2)) = 1 + x2
POL(S(x1)) = 3
POL(log(x1)) = x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, s(S(0))))))
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:
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, s(S(0))))))
POL(0) = 1
POL(LOG(x1)) = 3·x1
POL(MINUS(x1, x2)) = 3 + x2
POL(PRED(x1)) = 2 + x1
POL(QUOT(x1, x2)) = 2 + x2
POL(S(x1)) = 3
POL(log(x1)) = 3 + 2·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
log(s(s(x))) → s(log(s(QUOT(x, s(S(0))))))
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:
Relative ADPs:
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → s(log(s(QUOT(x, s(S(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 2 + 3·x1
POL(MINUS(x1, x2)) = 2 + 2·x1 + 2·x2
POL(PRED(x1)) = x12
POL(QUOT(x1, x2)) = 2·x1 + x2
POL(S(x1)) = 0
POL(log(x1)) = 0
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = 2·x1
POL(s(x1)) = 3·x1
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → s(quot(minus(x, y), S(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 2 + 2·x1
POL(MINUS(x1, x2)) = 2 + 2·x1 + 2·x2
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 2 + x2
POL(S(x1)) = 2 + 2·x1
POL(log(x1)) = x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
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:
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(quot(x, s(S(0))))))
log(s(0)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(s(x))) → s(LOG(s(QUOT(x, s(s(0))))))
log(s(s(x))) → s(LOG(S(quot(x, s(s(0))))))
quot(0, s(y)) → 0
pred(s(x)) → x
log(s(s(x))) → s(LOG(s(quot(x, S(s(0))))))
s(pred(x)) → pred(s(x))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
log(s(s(x))) → S(LOG(s(quot(x, s(s(0))))))
POL(0) = 0
POL(LOG(x1)) = 2 + 2·x1
POL(MINUS(x1, x2)) = 2 + 2·x1 + 2·x1·x2 + 2·x2
POL(PRED(x1)) = 2
POL(QUOT(x1, x2)) = 3·x1 + x2
POL(S(x1)) = 3
POL(log(x1)) = 2 + 3·x1
POL(minus(x1, x2)) = x1
POL(pred(x1)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 3 + 3·x1
log(s(0)) → 0
s(pred(x)) → pred(s(x))
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → s(pred(x))
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
minus(x, 0) → x
quot(0, s(y)) → 0
pred(s(x)) → x