(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)
ab
ac

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))
ab
ac

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)
ab
ac

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)
ab
ac

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)
ab
ac

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)  =  x2
s(x1)  =  s(x1)
gcd(x1, x2)  =  gcd(x1, x2)
gcd2(x1, x2, x3)  =  x3
0  =  0
if1(x1, x2, x3, x4, x5, x6, x7)  =  x7
le(x1, x2)  =  le(x1, x2)
inc(x1)  =  x1
true  =  true
pair(x1, x2)  =  pair
result(x1)  =  x1
neededIterations(x1)  =  neededIterations(x1)
false  =  false
if2(x1, x2, x3, x4, x5, x6)  =  x6
if3(x1, x2, x3, x4, x5)  =  x5
minus(x1, x2)  =  x1
if4(x1, x2, x3, x4)  =  x4
a  =  a
b  =  b
c  =  c

Lexicographic path order with status [LPO].
Precedence:
s1 > pair
gcd2 > 0 > pair
le2 > true > pair
le2 > false > pair
neededIterations1 > pair
a > b > pair
a > c > pair

Status:
s1: [1]
gcd2: [1,2]
0: []
le2: [1,2]
true: []
pair: []
neededIterations1: [1]
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)
ab
ac

(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)
ab
ac

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)
ab
ac

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)  =  x2
s(x1)  =  s(x1)
gcd(x1, x2)  =  gcd(x1, x2)
gcd2(x1, x2, x3)  =  x3
0  =  0
if1(x1, x2, x3, x4, x5, x6, x7)  =  x7
le(x1, x2)  =  le(x1, x2)
inc(x1)  =  x1
true  =  true
pair(x1, x2)  =  pair
result(x1)  =  x1
neededIterations(x1)  =  neededIterations(x1)
false  =  false
if2(x1, x2, x3, x4, x5, x6)  =  x6
if3(x1, x2, x3, x4, x5)  =  x5
minus(x1, x2)  =  x1
if4(x1, x2, x3, x4)  =  x4
a  =  a
b  =  b
c  =  c

Lexicographic path order with status [LPO].
Precedence:
s1 > pair
gcd2 > 0 > pair
le2 > true > pair
le2 > false > pair
neededIterations1 > pair
a > b > pair
a > c > pair

Status:
s1: [1]
gcd2: [1,2]
0: []
le2: [1,2]
true: []
pair: []
neededIterations1: [1]
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)
ab
ac

(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)
ab
ac

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)
ab
ac

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)  =  x1
s(x1)  =  s(x1)
gcd(x1, x2)  =  x1
gcd2(x1, x2, x3)  =  x1
0  =  0
if1(x1, x2, x3, x4, x5, x6, x7)  =  x5
le(x1, x2)  =  le
inc(x1)  =  x1
true  =  true
pair(x1, x2)  =  x2
result(x1)  =  result
neededIterations(x1)  =  neededIterations
false  =  false
if2(x1, x2, x3, x4, x5, x6)  =  x4
if3(x1, x2, x3, x4, x5)  =  x3
minus(x1, x2)  =  x1
if4(x1, x2, x3, x4)  =  x2
a  =  a
b  =  b
c  =  c

Lexicographic path order with status [LPO].
Precedence:
s1 > false > neededIterations
0 > false > neededIterations
le > true > neededIterations
le > false > neededIterations
result > neededIterations
a > b > neededIterations
a > c > neededIterations

Status:
s1: [1]
0: []
le: []
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)
ab
ac

(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)
ab
ac

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)
ab
ac

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.