Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1

Q is empty.


↳ QTRS
  ↳ RRRPoloQTRSProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

0(x1) → x1
Used ordering:
Polynomial interpretation [25]:

POL(0(x1)) = 2 + 2·x1   
POL(half(x1)) = x1   
POL(log(x1)) = 2·x1   
POL(p(x1)) = x1   
POL(s(x1)) = x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

HALF(s(s(x1))) → P(s(s(x1)))
HALF(0(x1)) → S(half(x1))
HALF(0(x1)) → HALF(x1)
HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → S(half(half(x1)))
P(s(s(s(x1)))) → S(p(s(s(x1))))
S(s(p(s(x1)))) → S(s(x1))
LOG(s(x1)) → HALF(s(x1))
P(s(s(s(x1)))) → P(s(s(x1)))
LOG(s(x1)) → LOG(half(s(x1)))
HALF(s(s(x1))) → S(half(p(s(s(x1)))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))
LOG(s(x1)) → S(log(half(s(x1))))
HALF(0(x1)) → S(s(half(x1)))
HALF(half(s(s(s(s(x1)))))) → S(s(half(half(x1))))

The TRS R consists of the following rules:

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(s(s(x1))) → P(s(s(x1)))
HALF(0(x1)) → S(half(x1))
HALF(0(x1)) → HALF(x1)
HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → S(half(half(x1)))
P(s(s(s(x1)))) → S(p(s(s(x1))))
S(s(p(s(x1)))) → S(s(x1))
LOG(s(x1)) → HALF(s(x1))
P(s(s(s(x1)))) → P(s(s(x1)))
LOG(s(x1)) → LOG(half(s(x1)))
HALF(s(s(x1))) → S(half(p(s(s(x1)))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))
LOG(s(x1)) → S(log(half(s(x1))))
HALF(0(x1)) → S(s(half(x1)))
HALF(half(s(s(s(s(x1)))))) → S(s(half(half(x1))))

The TRS R consists of the following rules:

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 9 less nodes.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

S(s(p(s(x1)))) → S(s(x1))

The TRS R consists of the following rules:

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

S(s(p(s(x1)))) → S(s(x1))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ UsableRulesReductionPairsProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

S(s(p(s(x1)))) → S(s(x1))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

S(s(p(s(x1)))) → S(s(x1))
The following rules are removed from R:

s(s(p(s(x1)))) → s(s(x1))
Used ordering: POLO with Polynomial interpretation [25]:

POL(S(x1)) = 2·x1   
POL(p(x1)) = 2·x1   
POL(s(x1)) = 2·x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ UsableRulesReductionPairsProof
                      ↳ QDP
                        ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

P(s(s(s(x1)))) → P(s(s(x1)))

The TRS R consists of the following rules:

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ UsableRulesReductionPairsProof
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

P(s(s(s(x1)))) → P(s(s(x1)))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

The following rules are removed from R:

s(s(p(s(x1)))) → s(s(x1))
Used ordering: POLO with Polynomial interpretation [25]:

POL(P(x1)) = 2·x1   
POL(p(x1)) = 2·x1   
POL(s(x1)) = 2·x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ UsableRulesReductionPairsProof
                      ↳ QDP
                        ↳ RuleRemovalProof
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

P(s(s(s(x1)))) → P(s(s(x1)))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

P(s(s(s(x1)))) → P(s(s(x1)))


Used ordering: POLO with Polynomial interpretation [25]:

POL(P(x1)) = 2·x1   
POL(s(x1)) = 1 + 2·x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ UsableRulesReductionPairsProof
                      ↳ QDP
                        ↳ RuleRemovalProof
                          ↳ QDP
                            ↳ PisEmptyProof
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                ↳ UsableRulesProof
                  ↳ QDP
              ↳ QDP
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

P(s(s(s(x1)))) → P(s(s(x1)))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(0(x1)) → HALF(x1)
HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))

The TRS R consists of the following rules:

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(0(x1)) → HALF(x1)
HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
p(s(s(s(x1)))) → s(p(s(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

HALF(0(x1)) → HALF(x1)


Used ordering: POLO with Polynomial interpretation [25]:

POL(0(x1)) = 1 + x1   
POL(HALF(x1)) = 2·x1   
POL(half(x1)) = x1   
POL(p(x1)) = x1   
POL(s(x1)) = x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
p(s(s(s(x1)))) → s(p(s(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ AND
                            ↳ QDP
                              ↳ UsableRulesProof
                            ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(s(s(x1))) → HALF(p(s(s(x1))))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
p(s(s(s(x1)))) → s(p(s(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ AND
                            ↳ QDP
                              ↳ UsableRulesProof
                                ↳ QDP
                                  ↳ RuleRemovalProof
                            ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(s(s(x1))) → HALF(p(s(s(x1))))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
p(s(s(s(x1)))) → s(p(s(s(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

s(s(p(s(x1)))) → s(s(x1))

Used ordering: POLO with Polynomial interpretation [25]:

POL(HALF(x1)) = 2·x1   
POL(p(x1)) = x1   
POL(s(x1)) = 2 + 2·x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ AND
                            ↳ QDP
                              ↳ UsableRulesProof
                                ↳ QDP
                                  ↳ RuleRemovalProof
                                    ↳ QDP
                                      ↳ MNOCProof
                            ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(s(s(x1))) → HALF(p(s(s(x1))))

The TRS R consists of the following rules:

p(s(s(s(x1)))) → s(p(s(s(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [15] to enlarge Q to all left-hand sides of R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ AND
                            ↳ QDP
                              ↳ UsableRulesProof
                                ↳ QDP
                                  ↳ RuleRemovalProof
                                    ↳ QDP
                                      ↳ MNOCProof
                                        ↳ QDP
                                          ↳ QDPOrderProof
                            ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(s(s(x1))) → HALF(p(s(s(x1))))

The TRS R consists of the following rules:

p(s(s(s(x1)))) → s(p(s(s(x1))))

The set Q consists of the following terms:

p(s(s(s(x0))))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


HALF(s(s(x1))) → HALF(p(s(s(x1))))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [21,25] with Interpretation:

POL( p(x1) ) = max{0, x1 - 1}


POL( s(x1) ) = x1 + 1


POL( HALF(x1) ) = max{0, x1 - 1}



The following usable rules [17] were oriented:

p(s(s(s(x1)))) → s(p(s(s(x1))))



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ AND
                            ↳ QDP
                              ↳ UsableRulesProof
                                ↳ QDP
                                  ↳ RuleRemovalProof
                                    ↳ QDP
                                      ↳ MNOCProof
                                        ↳ QDP
                                          ↳ QDPOrderProof
                                            ↳ QDP
                                              ↳ PisEmptyProof
                            ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
P is empty.
The TRS R consists of the following rules:

p(s(s(s(x1)))) → s(p(s(s(x1))))

The set Q consists of the following terms:

p(s(s(s(x0))))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ AND
                            ↳ QDP
                            ↳ QDP
                              ↳ RuleRemovalProof
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
p(s(s(s(x1)))) → s(p(s(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

HALF(half(s(s(s(s(x1)))))) → HALF(x1)

Strictly oriented rules of the TRS R:

half(s(0(x1))) → 0(x1)

Used ordering: POLO with Polynomial interpretation [25]:

POL(0(x1)) = 2 + x1   
POL(HALF(x1)) = x1   
POL(half(x1)) = 1 + x1   
POL(p(x1)) = x1   
POL(s(x1)) = x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ AND
                            ↳ QDP
                            ↳ QDP
                              ↳ RuleRemovalProof
                                ↳ QDP
                                  ↳ RuleRemovalProof
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
p(s(s(s(x1)))) → s(p(s(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

half(0(x1)) → 0(s(s(half(x1))))

Used ordering: POLO with Polynomial interpretation [25]:

POL(0(x1)) = 1 + 2·x1   
POL(HALF(x1)) = x1   
POL(half(x1)) = 2·x1   
POL(p(x1)) = x1   
POL(s(x1)) = x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ AND
                            ↳ QDP
                            ↳ QDP
                              ↳ RuleRemovalProof
                                ↳ QDP
                                  ↳ RuleRemovalProof
                                    ↳ QDP
                                      ↳ QDPOrderProof
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
p(s(s(s(x1)))) → s(p(s(s(x1))))
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [21,25] with Interpretation:

POL( p(x1) ) = max{0, x1 - 1}


POL( s(x1) ) = x1 + 1


POL( half(x1) ) = max{0, x1 - 1}


POL( HALF(x1) ) = max{0, x1 - 1}



The following usable rules [17] were oriented:

half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
s(s(p(s(x1)))) → s(s(x1))
p(s(s(s(x1)))) → s(p(s(s(x1))))



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ AND
                            ↳ QDP
                            ↳ QDP
                              ↳ RuleRemovalProof
                                ↳ QDP
                                  ↳ RuleRemovalProof
                                    ↳ QDP
                                      ↳ QDPOrderProof
                                        ↳ QDP
                                          ↳ PisEmptyProof
                ↳ UsableRulesProof
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
P is empty.
The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
p(s(s(s(x1)))) → s(p(s(s(x1))))
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                ↳ UsableRulesProof
                  ↳ QDP
              ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

HALF(0(x1)) → HALF(x1)
HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
p(s(s(s(x1)))) → s(p(s(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                ↳ UsableRulesProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

LOG(s(x1)) → LOG(half(s(x1)))

The TRS R consists of the following rules:

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QDPOrderProof
                ↳ UsableRulesProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

LOG(s(x1)) → LOG(half(s(x1)))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


LOG(s(x1)) → LOG(half(s(x1)))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [21,25] with Interpretation:

POL( s(x1) ) = x1 + 1


POL( p(x1) ) = max{0, x1 - 1}


POL( half(x1) ) = max{0, x1 - 1}


POL( 0(x1) ) = 0


POL( LOG(x1) ) = x1 + 1



The following usable rules [17] were oriented:

half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
half(s(0(x1))) → 0(x1)
half(0(x1)) → 0(s(s(half(x1))))
s(s(p(s(x1)))) → s(s(x1))



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ PisEmptyProof
                ↳ UsableRulesProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
P is empty.
The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                ↳ UsableRulesProof
                  ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

LOG(s(x1)) → LOG(half(s(x1)))

The TRS R consists of the following rules:

s(s(p(s(x1)))) → s(s(x1))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We have reversed the following QTRS:
The set of rules R is

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1

The set Q is empty.
We have obtained the following QTRS:

s(log(x)) → s(half(log(s(x))))
0(half(x)) → half(s(s(0(x))))
0(s(half(x))) → 0(x)
s(s(half(x))) → s(s(p(half(s(x)))))
s(s(s(s(half(half(x)))))) → half(half(s(s(x))))
s(s(s(p(x)))) → s(s(p(s(x))))
s(p(s(s(x)))) → s(s(x))
0(x) → x

The set Q is empty.

↳ QTRS
  ↳ RRRPoloQTRSProof
  ↳ QTRS Reverse
    ↳ QTRS
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

s(log(x)) → s(half(log(s(x))))
0(half(x)) → half(s(s(0(x))))
0(s(half(x))) → 0(x)
s(s(half(x))) → s(s(p(half(s(x)))))
s(s(s(s(half(half(x)))))) → half(half(s(s(x))))
s(s(s(p(x)))) → s(s(p(s(x))))
s(p(s(s(x)))) → s(s(x))
0(x) → x

Q is empty.

We have reversed the following QTRS:
The set of rules R is

log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1

The set Q is empty.
We have obtained the following QTRS:

s(log(x)) → s(half(log(s(x))))
0(half(x)) → half(s(s(0(x))))
0(s(half(x))) → 0(x)
s(s(half(x))) → s(s(p(half(s(x)))))
s(s(s(s(half(half(x)))))) → half(half(s(s(x))))
s(s(s(p(x)))) → s(s(p(s(x))))
s(p(s(s(x)))) → s(s(x))
0(x) → x

The set Q is empty.

↳ QTRS
  ↳ RRRPoloQTRSProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse
    ↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

s(log(x)) → s(half(log(s(x))))
0(half(x)) → half(s(s(0(x))))
0(s(half(x))) → 0(x)
s(s(half(x))) → s(s(p(half(s(x)))))
s(s(s(s(half(half(x)))))) → half(half(s(s(x))))
s(s(s(p(x)))) → s(s(p(s(x))))
s(p(s(s(x)))) → s(s(x))
0(x) → x

Q is empty.