Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(X) → if(X, c, f(true))
if(true, X, Y) → X
if(false, X, Y) → Y

The replacement map contains the following entries:

f: {1}
if: {1, 2}
c: empty set
true: empty set
false: empty set


↳ CSR
  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(X) → if(X, c, f(true))
if(true, X, Y) → X
if(false, X, Y) → Y

The replacement map contains the following entries:

f: {1}
if: {1, 2}
c: empty set
true: empty set
false: empty set

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(X) → if(X, c, f(true))
if(true, X, Y) → X
if(false, X, Y) → Y

The replacement map contains the following entries:

f: {1}
if: {1, 2}
c: empty set
true: empty set
false: empty set

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSUsableRulesProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, F} are replacing on all positions.
For all symbols f in {if, IF} we have µ(f) = {1, 2}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

F(X) → IF(X, c, f(true))

The collapsing dependency pairs are DPc:

IF(false, X, Y) → Y


The hidden terms of R are:

f(true)

Every hiding context is built from:none

Hence, the new unhiding pairs DPu are :

IF(false, X, Y) → U(Y)
U(f(true)) → F(true)

The TRS R consists of the following rules:

f(X) → if(X, c, f(true))
if(true, X, Y) → X
if(false, X, Y) → Y

The set Q consists of the following terms:

f(x0)
if(true, x0, x1)
if(false, x0, x1)


The following rules are not useable and can be deleted:

f(x0) → if(x0, c, f(true))
if(true, x0, x1) → x0
if(false, x0, x1) → x1


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSUsableRulesProof
            ↳ QCSDP
              ↳ QCSDPReductionPairProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, F} are replacing on all positions.
For all symbols f in {IF, if} we have µ(f) = {1, 2}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

F(X) → IF(X, c, f(true))

The collapsing dependency pairs are DPc:

IF(false, X, Y) → Y


Hence, the new unhiding pairs DPu are :

IF(false, X, Y) → U(Y)
U(f(true)) → F(true)

R is empty.
The set Q consists of the following terms:

f(x0)
if(true, x0, x1)
if(false, x0, x1)


Using the order
Polynomial interpretation with max and min functions [25]:

POL(F(x1)) = x1   
POL(IF(x1, x2, x3)) = x1   
POL(U(x1)) = 0   
POL(c) = 0   
POL(f(x1)) = 0   
POL(false) = 1   
POL(true) = 0   

the following usable rules
none

could all be oriented weakly.
Furthermore, the pairs

IF(false, X, Y) → U(Y)

could be oriented strictly and thus removed.
The pairs

F(X) → IF(X, c, f(true))
U(f(true)) → F(true)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSUsableRulesProof
            ↳ QCSDP
              ↳ QCSDPReductionPairProof
                ↳ QCSDP
                  ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, F} are replacing on all positions.
For all symbols f in {IF, if} we have µ(f) = {1, 2}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

F(X) → IF(X, c, f(true))
U(f(true)) → F(true)

R is empty.
The set Q consists of the following terms:

f(x0)
if(true, x0, x1)
if(false, x0, x1)


The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 2 less nodes.