Termination w.r.t. Q proof of /tmp/tmpQXpfIl/aprove08.trs

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

0 QTRS

↳1 AAECC Innermost (⇔)

↳2 QTRS

↳3 DependencyPairsProof (⇔)

↳4 QDP

↳5 DependencyGraphProof (⇔)

↳6 AND

  ↳7 QDP

    ↳8 QDPOrderProof (⇔)

    ↳9 QDP

    ↳10 PisEmptyProof (⇔)

    ↳11 TRUE

  ↳12 QDP

    ↳13 QDPOrderProof (⇔)

    ↳14 QDP

    ↳15 PisEmptyProof (⇔)

    ↳16 TRUE

  ↳17 QDP

    ↳18 QDPOrderProof (⇔)

    ↳19 QDP

    ↳20 PisEmptyProof (⇔)

    ↳21 TRUE

  ↳22 QDP

(0) Obligation:

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

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
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

inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)

The TRS R 2 is

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
a → b
a → c

The signature Sigma is {gcd, gcd2, if1, pair, if2, if3, if4, a, b, c}

(2) Obligation:

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

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

The set Q consists of the following terms:

gcd(x0, x1)
gcd2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4, x5)
if1(false, x0, x1, x2, x3, x4, x5)
if2(true, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if3(false, x0, x1, x2, x3)
if3(true, x0, x1, x2, x3)
if4(false, x0, x1, x2)
if4(true, x0, x1, x2)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
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:

GCD(x, y) → GCD2(x, y, 0)
GCD2(x, y, i) → IF1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
GCD2(x, y, i) → LE(x, 0)
GCD2(x, y, i) → LE(y, 0)
GCD2(x, y, i) → LE(x, y)
GCD2(x, y, i) → LE(y, x)
GCD2(x, y, i) → INC(i)
IF1(false, b1, b2, b3, x, y, i) → IF2(b1, b2, b3, x, y, i)
IF2(false, b2, b3, x, y, i) → IF3(b2, b3, x, y, i)
IF3(false, b3, x, y, i) → GCD2(minus(x, y), y, i)
IF3(false, b3, x, y, i) → MINUS(x, y)
IF3(true, b3, x, y, i) → IF4(b3, x, y, i)
IF4(false, x, y, i) → GCD2(x, minus(y, x), i)
IF4(false, x, y, i) → MINUS(y, x)
INC(s(i)) → INC(i)
LE(s(x), s(y)) → LE(x, y)
MINUS(s(x), s(y)) → MINUS(x, y)

The TRS R consists of the following rules:

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

The set Q consists of the following terms:

gcd(x0, x1)
gcd2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4, x5)
if1(false, x0, x1, x2, x3, x4, x5)
if2(true, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if3(false, x0, x1, x2, x3)
if3(true, x0, x1, x2, x3)
if4(false, x0, x1, x2)
if4(true, x0, x1, x2)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
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 4 SCCs with 8 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

MINUS(s(x), s(y)) → MINUS(x, y)

The TRS R consists of the following rules:

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

The set Q consists of the following terms:

gcd(x0, x1)
gcd2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4, x5)
if1(false, x0, x1, x2, x3, x4, x5)
if2(true, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if3(false, x0, x1, x2, x3)
if3(true, x0, x1, x2, x3)
if4(false, x0, x1, x2)
if4(true, x0, x1, x2)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
a

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

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

MINUS(s(x), s(y)) → MINUS(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MINUS(x1, x2) = MINUS(x2)
s(x1) = s(x1)
gcd(x1, x2) = x2
gcd2(x1, x2, x3) = x2
0 = 0
if1(x1, x2, x3, x4, x5, x6, x7) = x6
le(x1, x2) = le
inc(x1) = inc(x1)
true = true
pair(x1, x2) = x1
result(x1) = result
neededIterations(x1) = neededIterations
false = false
if2(x1, x2, x3, x4, x5, x6) = x5
if3(x1, x2, x3, x4, x5) = x4
minus(x1, x2) = x1
if4(x1, x2, x3, x4) = x3
a = a
b = b
c = c

Lexicographic path order with status [LPO].
Quasi-Precedence:

[le, false] > [true, result]
inc₁ > s₁ > MINUS₁ > [true, result]
inc₁ > 0 > [true, result]
neededIterations > [true, result]
[a, b] > c > [true, result]

Status:

MINUS₁: [1]
s₁: [1]
0: []
le: []
inc₁: [1]
true: []
result: []
neededIterations: []
false: []
a: []
b: []
c: []

The following usable rules [FROCOS05] were oriented:

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

(9) Obligation:

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

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

The set Q consists of the following terms:

gcd(x0, x1)
gcd2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4, x5)
if1(false, x0, x1, x2, x3, x4, x5)
if2(true, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if3(false, x0, x1, x2, x3)
if3(true, x0, x1, x2, x3)
if4(false, x0, x1, x2)
if4(true, x0, x1, x2)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
a

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

(10) PisEmptyProof (EQUIVALENT transformation)

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

(11) TRUE

(12) Obligation:

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

LE(s(x), s(y)) → LE(x, y)

The TRS R consists of the following rules:

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

The set Q consists of the following terms:

gcd(x0, x1)
gcd2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4, x5)
if1(false, x0, x1, x2, x3, x4, x5)
if2(true, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if3(false, x0, x1, x2, x3)
if3(true, x0, x1, x2, x3)
if4(false, x0, x1, x2)
if4(true, x0, x1, x2)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
a

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

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

LE(s(x), s(y)) → LE(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
LE(x1, x2) = x1
s(x1) = s(x1)
gcd(x1, x2) = gcd(x1)
gcd2(x1, x2, x3) = gcd2(x3)
0 = 0
if1(x1, x2, x3, x4, x5, x6, x7) = if1(x7)
le(x1, x2) = le
inc(x1) = x1
true = true
pair(x1, x2) = pair(x1)
result(x1) = result
neededIterations(x1) = neededIterations(x1)
false = false
if2(x1, x2, x3, x4, x5, x6) = if2(x6)
if3(x1, x2, x3, x4, x5) = if3(x5)
minus(x1, x2) = x1
if4(x1, x2, x3, x4) = if4(x4)
a = a
b = b
c = c

Lexicographic path order with status [LPO].
Quasi-Precedence:

s₁ > [le, true, pair₁, false]
[gcd₁, 0] > [gcd2₁, if1₁, if2₁, if3₁, if4₁] > result > [le, true, pair₁, false]
neededIterations₁ > [le, true, pair₁, false]
[a, b] > c > [le, true, pair₁, false]

Status:

s₁: [1]
gcd₁: [1]
gcd2₁: [1]
0: []
if1₁: [1]
le: []
true: []
pair₁: [1]
result: []
neededIterations₁: [1]
false: []
if2₁: [1]
if3₁: [1]
if4₁: [1]
a: []
b: []
c: []

The following usable rules [FROCOS05] were oriented:

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

(14) Obligation:

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

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

The set Q consists of the following terms:

gcd(x0, x1)
gcd2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4, x5)
if1(false, x0, x1, x2, x3, x4, x5)
if2(true, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if3(false, x0, x1, x2, x3)
if3(true, x0, x1, x2, x3)
if4(false, x0, x1, x2)
if4(true, x0, x1, x2)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
a

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

(15) PisEmptyProof (EQUIVALENT transformation)

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

(16) TRUE

(17) Obligation:

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

INC(s(i)) → INC(i)

The TRS R consists of the following rules:

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

The set Q consists of the following terms:

gcd(x0, x1)
gcd2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4, x5)
if1(false, x0, x1, x2, x3, x4, x5)
if2(true, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if3(false, x0, x1, x2, x3)
if3(true, x0, x1, x2, x3)
if4(false, x0, x1, x2)
if4(true, x0, x1, x2)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
a

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

(18) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

INC(s(i)) → INC(i)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
INC(x1) = INC(x1)
s(x1) = s(x1)
gcd(x1, x2) = x2
gcd2(x1, x2, x3) = x2
0 = 0
if1(x1, x2, x3, x4, x5, x6, x7) = x6
le(x1, x2) = le(x2)
inc(x1) = inc(x1)
true = true
pair(x1, x2) = x1
result(x1) = result
neededIterations(x1) = neededIterations
false = false
if2(x1, x2, x3, x4, x5, x6) = x5
if3(x1, x2, x3, x4, x5) = x4
minus(x1, x2) = x1
if4(x1, x2, x3, x4) = x3
a = a
b = b
c = c

Lexicographic path order with status [LPO].
Quasi-Precedence:

inc₁ > [INC₁, s₁, le₁] > false > [true, result]
inc₁ > 0 > false > [true, result]
neededIterations > [true, result]
a > b > [true, result]
a > c > [true, result]

Status:

INC₁: [1]
s₁: [1]
0: []
le₁: [1]
inc₁: [1]
true: []
result: []
neededIterations: []
false: []
a: []
b: []
c: []

The following usable rules [FROCOS05] were oriented:

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

(19) Obligation:

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

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

The set Q consists of the following terms:

gcd(x0, x1)
gcd2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4, x5)
if1(false, x0, x1, x2, x3, x4, x5)
if2(true, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if3(false, x0, x1, x2, x3)
if3(true, x0, x1, x2, x3)
if4(false, x0, x1, x2)
if4(true, x0, x1, x2)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
a

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

(20) PisEmptyProof (EQUIVALENT transformation)

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

(21) TRUE

(22) Obligation:

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

IF1(false, b1, b2, b3, x, y, i) → IF2(b1, b2, b3, x, y, i)
IF2(false, b2, b3, x, y, i) → IF3(b2, b3, x, y, i)
IF3(false, b3, x, y, i) → GCD2(minus(x, y), y, i)
GCD2(x, y, i) → IF1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
IF3(true, b3, x, y, i) → IF4(b3, x, y, i)
IF4(false, x, y, i) → GCD2(x, minus(y, x), i)

The TRS R consists of the following rules:

gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c

The set Q consists of the following terms:

gcd(x0, x1)
gcd2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4, x5)
if1(false, x0, x1, x2, x3, x4, x5)
if2(true, x0, x1, x2, x3, x4)
if2(false, x0, x1, x2, x3, x4)
if3(false, x0, x1, x2, x3)
if3(true, x0, x1, x2, x3)
if4(false, x0, x1, x2)
if4(true, x0, x1, x2)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
a

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