Termination w.r.t. Q proof of /tmp/tmpVTcTbV/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) = 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:

s₁ > pair
gcd₂ > 0 > pair
le₂ > true > pair
le₂ > false > pair
neededIterations₁ > pair
a > b > pair
a > c > pair

Status:

s₁: [1]
gcd₂: [1,2]
0: []
le₂: [1,2]
true: []
pair: []
neededIterations₁: [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)
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) = 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:

s₁ > pair
gcd₂ > 0 > pair
le₂ > true > pair
le₂ > false > pair
neededIterations₁ > pair
a > b > pair
a > c > pair

Status:

s₁: [1]
gcd₂: [1,2]
0: []
le₂: [1,2]
true: []
pair: []
neededIterations₁: [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)
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) = 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:

s₁ > false > neededIterations
0 > false > neededIterations
le > true > neededIterations
le > false > neededIterations
result > neededIterations
a > b > neededIterations
a > c > neededIterations

Status:

s₁: [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)
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.