Termination w.r.t. Q proof of /tmp/tmpfucATX/thiemann14.trs

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS

↳1 Overlay + Local Confluence (⇔)

↳2 QTRS

↳3 DependencyPairsProof (⇔)

↳4 QDP

↳5 DependencyGraphProof (⇔)

↳6 AND

  ↳7 QDP

    ↳8 UsableRulesProof (⇔)

    ↳9 QDP

    ↳10 QReductionProof (⇔)

    ↳11 QDP

    ↳12 QDPOrderProof (⇔)

    ↳13 QDP

    ↳14 PisEmptyProof (⇔)

    ↳15 TRUE

  ↳16 QDP

    ↳17 UsableRulesProof (⇔)

    ↳18 QDP

    ↳19 QReductionProof (⇔)

    ↳20 QDP

    ↳21 QDPSizeChangeProof (⇔)

    ↳22 TRUE

  ↳23 QDP

    ↳24 UsableRulesProof (⇔)

    ↳25 QDP

    ↳26 QReductionProof (⇔)

    ↳27 QDP

    ↳28 Narrowing (⇔)

    ↳29 QDP

    ↳30 Instantiation (⇔)

    ↳31 QDP

    ↳32 Instantiation (⇔)

    ↳33 QDP

    ↳34 Narrowing (⇔)

    ↳35 QDP

    ↳36 Instantiation (⇔)

    ↳37 QDP

    ↳38 DependencyGraphProof (⇔)

    ↳39 QDP

    ↳40 ForwardInstantiation (⇔)

    ↳41 QDP

    ↳42 Narrowing (⇔)

    ↳43 QDP

    ↳44 DependencyGraphProof (⇔)

    ↳45 QDP

    ↳46 Narrowing (⇔)

    ↳47 QDP

    ↳48 DependencyGraphProof (⇔)

    ↳49 QDP

    ↳50 Instantiation (⇔)

    ↳51 QDP

    ↳52 Instantiation (⇔)

    ↳53 QDP

    ↳54 ForwardInstantiation (⇔)

    ↳55 QDP

    ↳56 Narrowing (⇔)

    ↳57 QDP

    ↳58 DependencyGraphProof (⇔)

    ↳59 QDP

    ↳60 UsableRulesProof (⇔)

    ↳61 QDP

    ↳62 QReductionProof (⇔)

    ↳63 QDP

    ↳64 Narrowing (⇔)

    ↳65 QDP

    ↳66 DependencyGraphProof (⇔)

    ↳67 QDP

    ↳68 UsableRulesProof (⇔)

    ↳69 QDP

    ↳70 Instantiation (⇔)

    ↳71 QDP

    ↳72 ForwardInstantiation (⇔)

    ↳73 QDP

    ↳74 DependencyGraphProof (⇔)

    ↳75 AND

      ↳76 QDP

        ↳77 ForwardInstantiation (⇔)

        ↳78 QDP

        ↳79 QDPOrderProof (⇔)

        ↳80 QDP

        ↳81 DependencyGraphProof (⇔)

        ↳82 TRUE

      ↳83 QDP

        ↳84 MRRProof (⇔)

        ↳85 QDP

        ↳86 QDPOrderProof (⇔)

        ↳87 QDP

        ↳88 DependencyGraphProof (⇔)

        ↳89 TRUE

(0) Obligation:

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

empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

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

empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))

The set Q consists of the following terms:

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

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

P(s(s(x))) → P(s(x))
INTLIST(x) → IF_INTLIST(empty(x), x)
INTLIST(x) → EMPTY(x)
IF_INTLIST(false, x) → HEAD(x)
IF_INTLIST(false, x) → INTLIST(tail(x))
IF_INTLIST(false, x) → TAIL(x)
INT(x, y) → IF_INT(zero(x), zero(y), x, y)
INT(x, y) → ZERO(x)
INT(x, y) → ZERO(y)
IF_INT(true, b, x, y) → IF1(b, x, y)
IF_INT(false, b, x, y) → IF2(b, x, y)
IF1(false, x, y) → INT(s(0), y)
IF2(false, x, y) → INTLIST(int(p(x), p(y)))
IF2(false, x, y) → INT(p(x), p(y))
IF2(false, x, y) → P(x)
IF2(false, x, y) → P(y)

The TRS R consists of the following rules:

empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))

The set Q consists of the following terms:

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 8 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

IF_INTLIST(false, x) → INTLIST(tail(x))
INTLIST(x) → IF_INTLIST(empty(x), x)

The TRS R consists of the following rules:

empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))

The set Q consists of the following terms:

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

IF_INTLIST(false, x) → INTLIST(tail(x))
INTLIST(x) → IF_INTLIST(empty(x), x)

The TRS R consists of the following rules:

empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y

The set Q consists of the following terms:

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)

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

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)

(11) Obligation:

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

IF_INTLIST(false, x) → INTLIST(tail(x))
INTLIST(x) → IF_INTLIST(empty(x), x)

The TRS R consists of the following rules:

empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y

The set Q consists of the following terms:

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))

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

(12) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

IF_INTLIST(false, x) → INTLIST(tail(x))
INTLIST(x) → IF_INTLIST(empty(x), x)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO,RATPOLO]:

POL(IF_INTLIST(x₁, x₂)) = 1/2 + (1/4)x₁ + (1/2)x₂
POL(false) = 11/4
POL(INTLIST(x₁)) = 1 + x₁
POL(tail(x₁)) = (1/2)x₁
POL(empty(x₁)) = 1/4 + (2)x₁
POL(nil) = 0
POL(true) = 0
POL(cons(x₁, x₂)) = 2 + (4)x₂

The value of delta used in the strict ordering is 3/16.
The following usable rules [FROCOS05] were oriented:

empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y

(13) Obligation:

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

empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y

The set Q consists of the following terms:

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))

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

(14) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(15) TRUE

(16) Obligation:

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

P(s(s(x))) → P(s(x))

The TRS R consists of the following rules:

empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))

The set Q consists of the following terms:

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)

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

(17) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(18) Obligation:

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

P(s(s(x))) → P(s(x))

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

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)

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

(19) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)

(20) Obligation:

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

P(s(s(x))) → P(s(x))

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

P(s(s(x))) → P(s(x))
The graph contains the following edges 1 > 1

(22) TRUE

(23) Obligation:

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

IF2(false, x, y) → INT(p(x), p(y))
INT(x, y) → IF_INT(zero(x), zero(y), x, y)
IF_INT(true, b, x, y) → IF1(b, x, y)
IF1(false, x, y) → INT(s(0), y)
IF_INT(false, b, x, y) → IF2(b, x, y)

The TRS R consists of the following rules:

empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))

The set Q consists of the following terms:

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)

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

(24) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(25) Obligation:

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

IF2(false, x, y) → INT(p(x), p(y))
INT(x, y) → IF_INT(zero(x), zero(y), x, y)
IF_INT(true, b, x, y) → IF1(b, x, y)
IF1(false, x, y) → INT(s(0), y)
IF_INT(false, b, x, y) → IF2(b, x, y)

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)

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

(26) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

empty(nil)
empty(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
head(cons(x0, x1))
intlist(x0)
if_intlist(true, x0)
if_intlist(false, x0)
int(x0, x1)
if_int(true, x0, x1, x2)
if_int(false, x0, x1, x2)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)

(27) Obligation:

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

IF2(false, x, y) → INT(p(x), p(y))
INT(x, y) → IF_INT(zero(x), zero(y), x, y)
IF_INT(true, b, x, y) → IF1(b, x, y)
IF1(false, x, y) → INT(s(0), y)
IF_INT(false, b, x, y) → IF2(b, x, y)

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(28) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule INT(x, y) → IF_INT(zero(x), zero(y), x, y) at position [0] we obtained the following new rules [LPAR04]:

INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)

(29) Obligation:

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

IF2(false, x, y) → INT(p(x), p(y))
IF_INT(true, b, x, y) → IF1(b, x, y)
IF1(false, x, y) → INT(s(0), y)
IF_INT(false, b, x, y) → IF2(b, x, y)
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(30) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF_INT(true, b, x, y) → IF1(b, x, y) we obtained the following new rules [LPAR04]:

IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)

(31) Obligation:

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

IF2(false, x, y) → INT(p(x), p(y))
IF1(false, x, y) → INT(s(0), y)
IF_INT(false, b, x, y) → IF2(b, x, y)
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(32) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF1(false, x, y) → INT(s(0), y) we obtained the following new rules [LPAR04]:

IF1(false, 0, z1) → INT(s(0), z1)

(33) Obligation:

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

IF2(false, x, y) → INT(p(x), p(y))
IF_INT(false, b, x, y) → IF2(b, x, y)
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)
IF1(false, 0, z1) → INT(s(0), z1)

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(34) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule IF2(false, x, y) → INT(p(x), p(y)) at position [0] we obtained the following new rules [LPAR04]:

IF2(false, 0, y1) → INT(0, p(y1))
IF2(false, s(0), y1) → INT(0, p(y1))
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))

(35) Obligation:

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

IF_INT(false, b, x, y) → IF2(b, x, y)
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)
IF1(false, 0, z1) → INT(s(0), z1)
IF2(false, 0, y1) → INT(0, p(y1))
IF2(false, s(0), y1) → INT(0, p(y1))
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(36) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF_INT(false, b, x, y) → IF2(b, x, y) we obtained the following new rules [LPAR04]:

IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)

(37) Obligation:

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

INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)
IF1(false, 0, z1) → INT(s(0), z1)
IF2(false, 0, y1) → INT(0, p(y1))
IF2(false, s(0), y1) → INT(0, p(y1))
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(38) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(39) Obligation:

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

IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0)
IF1(false, 0, z1) → INT(s(0), z1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(0), y1) → INT(0, p(y1))
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(40) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule IF_INT(true, y_0, 0, z0) → IF1(y_0, 0, z0) we obtained the following new rules [LPAR04]:

IF_INT(true, false, 0, x1) → IF1(false, 0, x1)

(41) Obligation:

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

IF1(false, 0, z1) → INT(s(0), z1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(0), y1) → INT(0, p(y1))
INT(0, y1) → IF_INT(true, zero(y1), 0, y1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(true, false, 0, x1) → IF1(false, 0, x1)

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(42) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule INT(0, y1) → IF_INT(true, zero(y1), 0, y1) at position [1] we obtained the following new rules [LPAR04]:

INT(0, 0) → IF_INT(true, true, 0, 0)
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))

(43) Obligation:

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

IF1(false, 0, z1) → INT(s(0), z1)
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(0), y1) → INT(0, p(y1))
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(true, false, 0, x1) → IF1(false, 0, x1)
INT(0, 0) → IF_INT(true, true, 0, 0)
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(44) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(45) Obligation:

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

INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(0), y1) → INT(0, p(y1))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, x1) → IF1(false, 0, x1)
IF1(false, 0, z1) → INT(s(0), z1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(46) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule IF2(false, s(0), y1) → INT(0, p(y1)) at position [1] we obtained the following new rules [LPAR04]:

IF2(false, s(0), 0) → INT(0, 0)
IF2(false, s(0), s(0)) → INT(0, 0)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))

(47) Obligation:

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

INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, x1) → IF1(false, 0, x1)
IF1(false, 0, z1) → INT(s(0), z1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF2(false, s(0), 0) → INT(0, 0)
IF2(false, s(0), s(0)) → INT(0, 0)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(48) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(49) Obligation:

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

IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, x1) → IF1(false, 0, x1)
IF1(false, 0, z1) → INT(s(0), z1)

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(50) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF_INT(true, false, 0, x1) → IF1(false, 0, x1) we obtained the following new rules [LPAR04]:

IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))

(51) Obligation:

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

IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF1(false, 0, z1) → INT(s(0), z1)
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(52) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF1(false, 0, z1) → INT(s(0), z1) we obtained the following new rules [LPAR04]:

IF1(false, 0, s(z0)) → INT(s(0), s(z0))

(53) Obligation:

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

IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(54) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule IF_INT(false, y_0, s(z0), z1) → IF2(y_0, s(z0), z1) we obtained the following new rules [LPAR04]:

IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))

(55) Obligation:

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

IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1)
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(56) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule INT(s(x0), y1) → IF_INT(false, zero(y1), s(x0), y1) at position [1] we obtained the following new rules [LPAR04]:

INT(s(y0), 0) → IF_INT(false, true, s(y0), 0)
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))

(57) Obligation:

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

IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
INT(s(y0), 0) → IF_INT(false, true, s(y0), 0)
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(58) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(59) Obligation:

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

INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))

The TRS R consists of the following rules:

zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(60) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(61) Obligation:

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

INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
p(0) → 0

The set Q consists of the following terms:

zero(0)
zero(s(x0))
p(0)
p(s(0))
p(s(s(x0)))

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

(62) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

zero(0)
zero(s(x0))

(63) Obligation:

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

INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
p(0) → 0

The set Q consists of the following terms:

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

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

(64) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule IF2(false, s(s(x0)), y1) → INT(s(p(s(x0))), p(y1)) at position [1] we obtained the following new rules [LPAR04]:

IF2(false, s(s(y0)), s(0)) → INT(s(p(s(y0))), 0)
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
IF2(false, s(s(y0)), 0) → INT(s(p(s(y0))), 0)

(65) Obligation:

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

INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
IF2(false, s(s(y0)), s(0)) → INT(s(p(s(y0))), 0)
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
IF2(false, s(s(y0)), 0) → INT(s(p(s(y0))), 0)

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
p(0) → 0

The set Q consists of the following terms:

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

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

(66) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(67) Obligation:

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

IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
p(0) → 0

The set Q consists of the following terms:

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

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

(68) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(69) Obligation:

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

IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2)
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

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

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

(70) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF_INT(false, false, s(s(y_0)), x2) → IF2(false, s(s(y_0)), x2) we obtained the following new rules [LPAR04]:

IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))

(71) Obligation:

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

IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

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

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

(72) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule INT(s(y0), s(x0)) → IF_INT(false, false, s(y0), s(x0)) we obtained the following new rules [LPAR04]:

INT(s(0), s(s(y_0))) → IF_INT(false, false, s(0), s(s(y_0)))
INT(s(s(y_0)), s(x1)) → IF_INT(false, false, s(s(y_0)), s(x1))

(73) Obligation:

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

IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))
INT(s(0), s(s(y_0))) → IF_INT(false, false, s(0), s(s(y_0)))
INT(s(s(y_0)), s(x1)) → IF_INT(false, false, s(s(y_0)), s(x1))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

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

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

(74) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.

(75) Complex Obligation (AND)

(76) Obligation:

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

IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
IF1(false, 0, s(z0)) → INT(s(0), s(z0))
INT(s(0), s(s(y_0))) → IF_INT(false, false, s(0), s(s(y_0)))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

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

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

(77) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule IF1(false, 0, s(z0)) → INT(s(0), s(z0)) we obtained the following new rules [LPAR04]:

IF1(false, 0, s(s(y_0))) → INT(s(0), s(s(y_0)))

(78) Obligation:

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

IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))
INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
INT(s(0), s(s(y_0))) → IF_INT(false, false, s(0), s(s(y_0)))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF1(false, 0, s(s(y_0))) → INT(s(0), s(s(y_0)))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

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

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

(79) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

IF2(false, s(0), s(s(x0))) → INT(0, s(p(s(x0))))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(IF2(x₁, x₂, x₃)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂ +
/ 0 1 \

\ 0 0 /

· x₃

POL(false) =
/ 0 \

\ 0 /

POL(s(x₁)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 1 0 /

· x₁

POL(0) =
/ 0 \

\ 0 /

POL(INT(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 0 1 \

\ 0 0 /

· x₂

POL(p(x₁)) =
/ 0 \

\ 0 /

+
/ 0 1 \

\ 0 1 /

· x₁

POL(IF_INT(x₁, x₂, x₃, x₄)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂ +
/ 0 0 \

\ 0 0 /

· x₃ +
/ 0 1 \

\ 0 0 /

· x₄

POL(true) =
/ 0 \

\ 0 /

POL(IF1(x₁, x₂, x₃)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂ +
/ 0 1 \

\ 0 0 /

· x₃

The following usable rules [FROCOS05] were oriented:

p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0

(80) Obligation:

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

INT(0, s(x0)) → IF_INT(true, false, 0, s(x0))
IF_INT(true, false, 0, s(z0)) → IF1(false, 0, s(z0))
INT(s(0), s(s(y_0))) → IF_INT(false, false, s(0), s(s(y_0)))
IF_INT(false, false, s(0), s(s(y_0))) → IF2(false, s(0), s(s(y_0)))
IF1(false, 0, s(s(y_0))) → INT(s(0), s(s(y_0)))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

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

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

(81) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 5 less nodes.

(82) TRUE

(83) Obligation:

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

INT(s(s(y_0)), s(x1)) → IF_INT(false, false, s(s(y_0)), s(x1))
IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))

The TRS R consists of the following rules:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

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

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

(84) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, 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:

p(s(0)) → 0

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(IF2(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(IF_INT(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄
POL(INT(x₁, x₂)) = x₁ + x₂
POL(false) = 0
POL(p(x₁)) = x₁
POL(s(x₁)) = 1 + x₁

(85) Obligation:

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

INT(s(s(y_0)), s(x1)) → IF_INT(false, false, s(s(y_0)), s(x1))
IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))

The TRS R consists of the following rules:

p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

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

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

(86) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

INT(s(s(y_0)), s(x1)) → IF_INT(false, false, s(s(y_0)), s(x1))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(INT(x₁, x₂)) =
/ 1 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 1 0 \

\ 0 0 /

· x₂

POL(s(x₁)) =
/ 0 \

\ 1 /

+
/ 0 1 \

\ 0 1 /

· x₁

POL(IF_INT(x₁, x₂, x₃, x₄)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂ +
/ 0 0 \

\ 0 0 /

· x₃ +
/ 1 0 \

\ 0 0 /

· x₄

POL(false) =
/ 0 \

\ 0 /

POL(IF2(x₁, x₂, x₃)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 0 /

· x₂ +
/ 1 0 \

\ 0 0 /

· x₃

POL(p(x₁)) =
/ 1 \

\ 0 /

+
/ 1 0 \

\ 1 0 /

· x₁

The following usable rules [FROCOS05] were oriented:

p(s(s(x))) → s(p(s(x)))

(87) Obligation:

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

IF_INT(false, false, s(s(x0)), s(z1)) → IF2(false, s(s(x0)), s(z1))
IF2(false, s(s(y0)), s(s(x0))) → INT(s(p(s(y0))), s(p(s(x0))))

The TRS R consists of the following rules:

p(s(s(x))) → s(p(s(x)))

The set Q consists of the following terms:

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

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

(88) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.