YES Termination w.r.t. Q proof of Secret_07_TRS_aprove04.ari

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

0 QTRS
↳1 AAECC Innermost (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 QDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 QReductionProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 QDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 QReductionProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 QDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 QDP
        ↳24 QReductionProof (⇔, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES
    ↳28 QDP
        ↳29 UsableRulesProof (⇔, 0 ms)
        ↳30 QDP
        ↳31 QReductionProof (⇔, 0 ms)
        ↳32 QDP
        ↳33 TransformationProof (⇔, 0 ms)
        ↳34 QDP
        ↳35 DependencyGraphProof (⇔, 0 ms)
        ↳36 QDP
        ↳37 UsableRulesProof (⇔, 0 ms)
        ↳38 QDP
        ↳39 QReductionProof (⇔, 0 ms)
        ↳40 QDP
        ↳41 TransformationProof (⇔, 0 ms)
        ↳42 QDP
        ↳43 UsableRulesProof (⇔, 0 ms)
        ↳44 QDP
        ↳45 TransformationProof (⇔, 0 ms)
        ↳46 QDP
        ↳47 UsableRulesProof (⇔, 0 ms)
        ↳48 QDP
        ↳49 QReductionProof (⇔, 0 ms)
        ↳50 QDP
        ↳51 TransformationProof (⇔, 0 ms)
        ↳52 QDP
        ↳53 TransformationProof (⇔, 0 ms)
        ↳54 QDP
        ↳55 QDPSizeChangeProof (⇔, 0 ms)
        ↳56 YES
    ↳57 QDP
        ↳58 UsableRulesProof (⇔, 0 ms)
        ↳59 QDP
        ↳60 QReductionProof (⇔, 0 ms)
        ↳61 QDP
        ↳62 NonInfProof (⇔, 57 ms)
        ↳63 QDP
        ↳64 DependencyGraphProof (⇔, 0 ms)
        ↳65 TRUE

(0) Obligation:

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

lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c

Q is empty.

(1) AAECC Innermost (EQUIVALENT transformation)

We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is

if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)

The TRS R 2 is

a → b
a → c

The signature Sigma is {a, b, c}

(2) Obligation:

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

lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c

The set Q consists of the following terms:

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

(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:

LCM(x, y) → LCMITER(x, y, 0, times(x, y))
LCM(x, y) → TIMES(x, y)
LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)
LCMITER(x, y, z, u) → OR(ge(0, x), ge(z, u))
LCMITER(x, y, z, u) → GE(0, x)
LCMITER(x, y, z, u) → GE(z, u)
IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
IF(false, x, y, z, u) → DIVISIBLE(z, y)
IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
IF2(false, x, y, z, u) → PLUS(x, z)
PLUS(s(x), y) → PLUS(x, y)
TIMES(x, y) → IFTIMES(ge(0, x), x, y)
TIMES(x, y) → GE(0, x)
IFTIMES(false, x, y) → PLUS(y, times(y, p(x)))
IFTIMES(false, x, y) → TIMES(y, p(x))
IFTIMES(false, x, y) → P(x)
GE(s(x), s(y)) → GE(x, y)
DIVISIBLE(s(x), s(y)) → DIV(s(x), s(y), s(y))
DIV(x, y, 0) → DIVISIBLE(x, y)
DIV(s(x), y, s(z)) → DIV(x, y, z)

The TRS R consists of the following rules:

lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c

The set Q consists of the following terms:

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

DIV(s(x), y, s(z)) → DIV(x, y, z)
DIV(x, y, 0) → DIVISIBLE(x, y)
DIVISIBLE(s(x), s(y)) → DIV(s(x), s(y), s(y))

The TRS R consists of the following rules:

lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c

The set Q consists of the following terms:

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

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:

DIV(s(x), y, s(z)) → DIV(x, y, z)
DIV(x, y, 0) → DIVISIBLE(x, y)
DIVISIBLE(s(x), s(y)) → DIV(s(x), s(y), s(y))

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

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

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].

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

(11) Obligation:

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

DIV(s(x), y, s(z)) → DIV(x, y, z)
DIV(x, y, 0) → DIVISIBLE(x, y)
DIVISIBLE(s(x), s(y)) → DIV(s(x), s(y), s(y))

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

(12) 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:

  • DIV(s(x), y, s(z)) → DIV(x, y, z)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 > 3

  • DIV(x, y, 0) → DIVISIBLE(x, y)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DIVISIBLE(s(x), s(y)) → DIV(s(x), s(y), s(y))
    The graph contains the following edges 1 >= 1, 2 >= 2, 2 >= 3

(13) YES

(14) Obligation:

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

GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c

The set Q consists of the following terms:

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

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

(15) 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.

(16) Obligation:

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

GE(s(x), s(y)) → GE(x, y)

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

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

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

(17) 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].

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

(18) Obligation:

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

GE(s(x), s(y)) → GE(x, y)

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

(19) 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:

  • GE(s(x), s(y)) → GE(x, y)
    The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

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

PLUS(s(x), y) → PLUS(x, y)

The TRS R consists of the following rules:

lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c

The set Q consists of the following terms:

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

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

(22) 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.

(23) Obligation:

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

PLUS(s(x), y) → PLUS(x, y)

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

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

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

(24) 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].

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

(25) Obligation:

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

PLUS(s(x), y) → PLUS(x, y)

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

(26) 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:

  • PLUS(s(x), y) → PLUS(x, y)
    The graph contains the following edges 1 > 1, 2 >= 2

(27) YES

(28) Obligation:

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

IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(x, y) → IFTIMES(ge(0, x), x, y)

The TRS R consists of the following rules:

lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c

The set Q consists of the following terms:

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

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

(29) 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.

(30) Obligation:

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

IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(x, y) → IFTIMES(ge(0, x), x, y)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

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

(31) 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].

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

(32) Obligation:

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

IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(x, y) → IFTIMES(ge(0, x), x, y)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

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

(33) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TIMES(x, y) → IFTIMES(ge(0, x), x, y) at position [0] we obtained the following new rules [LPAR04]:

TIMES(0, y1) → IFTIMES(true, 0, y1) → TIMES(0, y1) → IFTIMES(true, 0, y1)
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1) → TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)

(34) Obligation:

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

IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(0, y1) → IFTIMES(true, 0, y1)
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

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

(35) DependencyGraphProof (EQUIVALENT transformation)

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

(36) Obligation:

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

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, x, y) → TIMES(y, p(x))

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

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

(37) 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.

(38) Obligation:

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

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, x, y) → TIMES(y, p(x))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

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

(39) 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].

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

(40) Obligation:

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

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, x, y) → TIMES(y, p(x))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

p(s(x0))
p(0)

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

(41) TransformationProof (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IFTIMES(false, x, y) → TIMES(y, p(x)) we obtained the following new rules [LPAR04]:

IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0))) → IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))

(42) Obligation:

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

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

p(s(x0))
p(0)

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

(43) 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.

(44) Obligation:

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

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))

The TRS R consists of the following rules:

p(s(x)) → x

The set Q consists of the following terms:

p(s(x0))
p(0)

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

(45) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0))) at position [1] we obtained the following new rules [LPAR04]:

IFTIMES(false, s(z0), z1) → TIMES(z1, z0) → IFTIMES(false, s(z0), z1) → TIMES(z1, z0)

(46) Obligation:

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

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, z0)

The TRS R consists of the following rules:

p(s(x)) → x

The set Q consists of the following terms:

p(s(x0))
p(0)

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

(47) 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.

(48) Obligation:

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

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, z0)

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

p(s(x0))
p(0)

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

(49) 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].

p(s(x0))
p(0)

(50) Obligation:

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

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, z0)

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

(51) TransformationProof (EQUIVALENT transformation)

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

IFTIMES(false, s(x0), s(y_0)) → TIMES(s(y_0), x0) → IFTIMES(false, s(x0), s(y_0)) → TIMES(s(y_0), x0)

(52) Obligation:

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

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(x0), s(y_0)) → TIMES(s(y_0), x0)

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

(53) TransformationProof (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1) we obtained the following new rules [LPAR04]:

TIMES(s(x0), s(y_1)) → IFTIMES(false, s(x0), s(y_1)) → TIMES(s(x0), s(y_1)) → IFTIMES(false, s(x0), s(y_1))

(54) Obligation:

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

IFTIMES(false, s(x0), s(y_0)) → TIMES(s(y_0), x0)
TIMES(s(x0), s(y_1)) → IFTIMES(false, s(x0), s(y_1))

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

(55) 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:

  • TIMES(s(x0), s(y_1)) → IFTIMES(false, s(x0), s(y_1))
    The graph contains the following edges 1 >= 2, 2 >= 3

  • IFTIMES(false, s(x0), s(y_0)) → TIMES(s(y_0), x0)
    The graph contains the following edges 3 >= 1, 2 > 2

(56) YES

(57) Obligation:

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

IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)

The TRS R consists of the following rules:

lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c

The set Q consists of the following terms:

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

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

(58) 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.

(59) Obligation:

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

IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(s(x), y, s(z)) → div(x, y, z)
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false

The set Q consists of the following terms:

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a

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

(60) 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].

lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
a

(61) Obligation:

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

IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(s(x), y, s(z)) → div(x, y, z)
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false

The set Q consists of the following terms:

plus(0, x0)
plus(s(x0), x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))

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

(62) NonInfProof (EQUIVALENT transformation)

The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u) the following chains were created:
  • We consider the chain LCMITER(x8, x9, x10, x11) → IF(or(ge(0, x8), ge(x10, x11)), x8, x9, x10, x11), IF(false, x12, x13, x14, x15) → IF2(divisible(x14, x13), x12, x13, x14, x15) which results in the following constraint:
    (1)    (IF(or(ge(0, x8), ge(x10, x11)), x8, x9, x10, x11)=IF(false, x12, x13, x14, x15) ⇒ IF(false, x12, x13, x14, x15)≥IF2(divisible(x14, x13), x12, x13, x14, x15))


    We simplified constraint (1) using rules (I), (II), (III), (VII) which results in the following new constraint:
    (2)    (0=x50∧ge(x50, x8)=x48∧ge(x10, x11)=x49∧or(x48, x49)=false ⇒ IF(false, x8, x9, x10, x11)≥IF2(divisible(x10, x9), x8, x9, x10, x11))


    We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on or(x48, x49)=false which results in the following new constraint:
    (3)    (x52=false∧0=x50∧ge(x50, x8)=false∧ge(x10, x11)=x52 ⇒ IF(false, x8, x9, x10, x11)≥IF2(divisible(x10, x9), x8, x9, x10, x11))


    We simplified constraint (3) using rule (III) which results in the following new constraint:
    (4)    (0=x50∧ge(x50, x8)=false∧ge(x10, x11)=false ⇒ IF(false, x8, x9, x10, x11)≥IF2(divisible(x10, x9), x8, x9, x10, x11))


    We simplified constraint (4) using rule (V) (with possible (I) afterwards) using induction on ge(x50, x8)=false which results in the following new constraints:
    (5)    (false=false∧0=0∧ge(x10, x11)=false ⇒ IF(false, s(x54), x9, x10, x11)≥IF2(divisible(x10, x9), s(x54), x9, x10, x11))

    (6)    (ge(x56, x55)=false∧0=s(x56)∧ge(x10, x11)=false∧(∀x57,x58,x59:ge(x56, x55)=false∧0=x56∧ge(x57, x58)=false ⇒ IF(false, x55, x59, x57, x58)≥IF2(divisible(x57, x59), x55, x59, x57, x58)) ⇒ IF(false, s(x55), x9, x10, x11)≥IF2(divisible(x10, x9), s(x55), x9, x10, x11))


    We simplified constraint (5) using rules (I), (II) which results in the following new constraint:
    (7)    (ge(x10, x11)=false ⇒ IF(false, s(x54), x9, x10, x11)≥IF2(divisible(x10, x9), s(x54), x9, x10, x11))


    We solved constraint (6) using rules (I), (II).We simplified constraint (7) using rule (V) (with possible (I) afterwards) using induction on ge(x10, x11)=false which results in the following new constraints:
    (8)    (false=false ⇒ IF(false, s(x54), x9, 0, s(x61))≥IF2(divisible(0, x9), s(x54), x9, 0, s(x61)))

    (9)    (ge(x63, x62)=false∧(∀x64,x65:ge(x63, x62)=false ⇒ IF(false, s(x64), x65, x63, x62)≥IF2(divisible(x63, x65), s(x64), x65, x63, x62)) ⇒ IF(false, s(x54), x9, s(x63), s(x62))≥IF2(divisible(s(x63), x9), s(x54), x9, s(x63), s(x62)))


    We simplified constraint (8) using rules (I), (II) which results in the following new constraint:
    (10)    (IF(false, s(x54), x9, 0, s(x61))≥IF2(divisible(0, x9), s(x54), x9, 0, s(x61)))


    We simplified constraint (9) using rule (VI) where we applied the induction hypothesis (∀x64,x65:ge(x63, x62)=false ⇒ IF(false, s(x64), x65, x63, x62)≥IF2(divisible(x63, x65), s(x64), x65, x63, x62)) with σ = [x64 / x54, x65 / x9] which results in the following new constraint:
    (11)    (IF(false, s(x54), x9, x63, x62)≥IF2(divisible(x63, x9), s(x54), x9, x63, x62) ⇒ IF(false, s(x54), x9, s(x63), s(x62))≥IF2(divisible(s(x63), x9), s(x54), x9, s(x63), s(x62)))






For Pair IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u) the following chains were created:
  • We consider the chain IF(false, x16, x17, x18, x19) → IF2(divisible(x18, x17), x16, x17, x18, x19), IF2(false, x20, x21, x22, x23) → LCMITER(x20, x21, plus(x20, x22), x23) which results in the following constraint:
    (1)    (IF2(divisible(x18, x17), x16, x17, x18, x19)=IF2(false, x20, x21, x22, x23) ⇒ IF2(false, x20, x21, x22, x23)≥LCMITER(x20, x21, plus(x20, x22), x23))


    We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
    (2)    (divisible(x18, x17)=false ⇒ IF2(false, x16, x17, x18, x19)≥LCMITER(x16, x17, plus(x16, x18), x19))


    We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on divisible(x18, x17)=false which results in the following new constraint:
    (3)    (div(s(x68), s(x67), s(x67))=false ⇒ IF2(false, x16, s(x67), s(x68), x19)≥LCMITER(x16, s(x67), plus(x16, s(x68)), x19))


    We simplified constraint (3) using rule (VII) which results in the following new constraint:
    (4)    (s(x68)=x69∧s(x67)=x70∧s(x67)=x71∧div(x69, x70, x71)=false ⇒ IF2(false, x16, s(x67), s(x68), x19)≥LCMITER(x16, s(x67), plus(x16, s(x68)), x19))


    We simplified constraint (4) using rule (V) (with possible (I) afterwards) using induction on div(x69, x70, x71)=false which results in the following new constraints:
    (5)    (div(x74, x73, x72)=false∧s(x68)=s(x74)∧s(x67)=x73∧s(x67)=s(x72)∧(∀x75,x76,x77,x78:div(x74, x73, x72)=false∧s(x75)=x74∧s(x76)=x73∧s(x76)=x72 ⇒ IF2(false, x77, s(x76), s(x75), x78)≥LCMITER(x77, s(x76), plus(x77, s(x75)), x78)) ⇒ IF2(false, x16, s(x67), s(x68), x19)≥LCMITER(x16, s(x67), plus(x16, s(x68)), x19))

    (6)    (divisible(x80, x79)=false∧s(x68)=x80∧s(x67)=x79∧s(x67)=0 ⇒ IF2(false, x16, s(x67), s(x68), x19)≥LCMITER(x16, s(x67), plus(x16, s(x68)), x19))

    (7)    (false=false∧s(x68)=0∧s(x67)=x82∧s(x67)=s(x81) ⇒ IF2(false, x16, s(x67), s(x68), x19)≥LCMITER(x16, s(x67), plus(x16, s(x68)), x19))


    We simplified constraint (5) using rules (I), (II), (III), (IV) which results in the following new constraint:
    (8)    (IF2(false, x16, s(x72), s(x74), x19)≥LCMITER(x16, s(x72), plus(x16, s(x74)), x19))


    We solved constraint (6) using rules (I), (II).We solved constraint (7) using rules (I), (II).




For Pair LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u) the following chains were created:
  • We consider the chain IF2(false, x36, x37, x38, x39) → LCMITER(x36, x37, plus(x36, x38), x39), LCMITER(x40, x41, x42, x43) → IF(or(ge(0, x40), ge(x42, x43)), x40, x41, x42, x43) which results in the following constraint:
    (1)    (LCMITER(x36, x37, plus(x36, x38), x39)=LCMITER(x40, x41, x42, x43) ⇒ LCMITER(x40, x41, x42, x43)≥IF(or(ge(0, x40), ge(x42, x43)), x40, x41, x42, x43))


    We simplified constraint (1) using rules (I), (II), (III), (IV) which results in the following new constraint:
    (2)    (LCMITER(x36, x37, x42, x39)≥IF(or(ge(0, x36), ge(x42, x39)), x36, x37, x42, x39))






To summarize, we get the following constraints P≥ for the following pairs.
  • IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
    • (IF(false, s(x54), x9, 0, s(x61))≥IF2(divisible(0, x9), s(x54), x9, 0, s(x61)))
    • (IF(false, s(x54), x9, x63, x62)≥IF2(divisible(x63, x9), s(x54), x9, x63, x62) ⇒ IF(false, s(x54), x9, s(x63), s(x62))≥IF2(divisible(s(x63), x9), s(x54), x9, s(x63), s(x62)))

  • IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
    • (IF2(false, x16, s(x72), s(x74), x19)≥LCMITER(x16, s(x72), plus(x16, s(x74)), x19))

  • LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)
    • (LCMITER(x36, x37, x42, x39)≥IF(or(ge(0, x36), ge(x42, x39)), x36, x37, x42, x39))




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:

POL(0) = 0   
POL(IF(x1, x2, x3, x4, x5)) = -1 + x1 + x2 + x3 - x4 + x5   
POL(IF2(x1, x2, x3, x4, x5)) = x3 - x4 + x5   
POL(LCMITER(x1, x2, x3, x4)) = x1 + x2 - x3 + x4   
POL(c) = -1   
POL(div(x1, x2, x3)) = x1 + x2   
POL(divisible(x1, x2)) = 1 + x1 + x2   
POL(false) = 1   
POL(ge(x1, x2)) = 1   
POL(or(x1, x2)) = x2   
POL(plus(x1, x2)) = x1 + x2   
POL(s(x1)) = 1 + x1   
POL(true) = 0   

The following pairs are in P>:

IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
The following pairs are in Pbound:

IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
The following rules are usable:

y → plus(0, y)
s(plus(x, y)) → plus(s(x), y)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y

(63) Obligation:

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

IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(s(x), y, s(z)) → div(x, y, z)
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false

The set Q consists of the following terms:

plus(0, x0)
plus(s(x0), x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))

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

(64) DependencyGraphProof (EQUIVALENT transformation)

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

(65) TRUE