0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 NonInfProof (⇔)
↳27 QDP
↳28 Narrowing (⇔)
↳29 QDP
↳30 DependencyGraphProof (⇔)
↳31 QDP
↳32 Narrowing (⇔)
↳33 QDP
↳34 DependencyGraphProof (⇔)
↳35 QDP
↳36 Instantiation (⇔)
↳37 QDP
↳38 DependencyGraphProof (⇔)
↳39 AND
↳40 QDP
↳41 Rewriting (⇔)
↳42 QDP
↳43 QDPOrderProof (⇔)
↳44 QDP
↳45 DependencyGraphProof (⇔)
↳46 TRUE
↳47 QDP
↳48 UsableRulesProof (⇔)
↳49 QDP
↳50 QReductionProof (⇔)
↳51 QDP
↳52 Rewriting (⇔)
↳53 QDP
↳54 UsableRulesProof (⇔)
↳55 QDP
↳56 QReductionProof (⇔)
↳57 QDP
↳58 ForwardInstantiation (⇔)
↳59 QDP
↳60 ForwardInstantiation (⇔)
↳61 QDP
↳62 QDPSizeChangeProof (⇔)
↳63 TRUE
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
LE(s(x), s(y)) → LE(x, y)
MINUS(s(x), s(y)) → MINUS(x, y)
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
GCD(s(x), s(y)) → LE(y, x)
IF_GCD(true, x, y) → GCD(minus(x, y), y)
IF_GCD(true, x, y) → MINUS(x, y)
IF_GCD(false, x, y) → GCD(minus(y, x), x)
IF_GCD(false, x, y) → MINUS(y, x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y)) → LE(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
LE(s(x), s(y)) → LE(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
IF_GCD(false, x, y) → GCD(minus(y, x), x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
gcd(0, y) → y
gcd(s(x), 0) → s(x)
gcd(s(x), s(y)) → if_gcd(le(y, x), s(x), s(y))
if_gcd(true, x, y) → gcd(minus(x, y), y)
if_gcd(false, x, y) → gcd(minus(y, x), x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
IF_GCD(false, x, y) → GCD(minus(y, x), x)
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
gcd(0, x0)
gcd(s(x0), 0)
gcd(s(x0), s(x1))
if_gcd(true, x0, x1)
if_gcd(false, x0, x1)
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
IF_GCD(false, x, y) → GCD(minus(y, x), x)
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
(1) (GCD(minus(x2, x3), x3)=GCD(s(x4), s(x5)) ⇒ GCD(s(x4), s(x5))≥IF_GCD(le(x5, x4), s(x4), s(x5)))
(2) (s(x5)=x26∧minus(x2, x26)=s(x4) ⇒ GCD(s(x4), s(x5))≥IF_GCD(le(x5, x4), s(x4), s(x5)))
(3) (x27=s(x4)∧s(x5)=0 ⇒ GCD(s(x4), s(x5))≥IF_GCD(le(x5, x4), s(x4), s(x5)))
(4) (minus(x30, x29)=s(x4)∧s(x5)=s(x29)∧(∀x31,x32:minus(x30, x29)=s(x31)∧s(x32)=x29 ⇒ GCD(s(x31), s(x32))≥IF_GCD(le(x32, x31), s(x31), s(x32))) ⇒ GCD(s(x4), s(x5))≥IF_GCD(le(x5, x4), s(x4), s(x5)))
(5) (minus(x30, x29)=s(x4) ⇒ GCD(s(x4), s(x29))≥IF_GCD(le(x29, x4), s(x4), s(x29)))
(6) (x33=s(x4) ⇒ GCD(s(x4), s(0))≥IF_GCD(le(0, x4), s(x4), s(0)))
(7) (minus(x36, x35)=s(x4)∧(∀x37:minus(x36, x35)=s(x37) ⇒ GCD(s(x37), s(x35))≥IF_GCD(le(x35, x37), s(x37), s(x35))) ⇒ GCD(s(x4), s(s(x35)))≥IF_GCD(le(s(x35), x4), s(x4), s(s(x35))))
(8) (GCD(s(x4), s(0))≥IF_GCD(le(0, x4), s(x4), s(0)))
(9) (GCD(s(x4), s(x35))≥IF_GCD(le(x35, x4), s(x4), s(x35)) ⇒ GCD(s(x4), s(s(x35)))≥IF_GCD(le(s(x35), x4), s(x4), s(s(x35))))
(10) (GCD(minus(x7, x6), x6)=GCD(s(x8), s(x9)) ⇒ GCD(s(x8), s(x9))≥IF_GCD(le(x9, x8), s(x8), s(x9)))
(11) (s(x9)=x38∧minus(x7, x38)=s(x8) ⇒ GCD(s(x8), s(x9))≥IF_GCD(le(x9, x8), s(x8), s(x9)))
(12) (x39=s(x8)∧s(x9)=0 ⇒ GCD(s(x8), s(x9))≥IF_GCD(le(x9, x8), s(x8), s(x9)))
(13) (minus(x42, x41)=s(x8)∧s(x9)=s(x41)∧(∀x43,x44:minus(x42, x41)=s(x43)∧s(x44)=x41 ⇒ GCD(s(x43), s(x44))≥IF_GCD(le(x44, x43), s(x43), s(x44))) ⇒ GCD(s(x8), s(x9))≥IF_GCD(le(x9, x8), s(x8), s(x9)))
(14) (minus(x42, x41)=s(x8) ⇒ GCD(s(x8), s(x41))≥IF_GCD(le(x41, x8), s(x8), s(x41)))
(15) (x45=s(x8) ⇒ GCD(s(x8), s(0))≥IF_GCD(le(0, x8), s(x8), s(0)))
(16) (minus(x48, x47)=s(x8)∧(∀x49:minus(x48, x47)=s(x49) ⇒ GCD(s(x49), s(x47))≥IF_GCD(le(x47, x49), s(x49), s(x47))) ⇒ GCD(s(x8), s(s(x47)))≥IF_GCD(le(s(x47), x8), s(x8), s(s(x47))))
(17) (GCD(s(x8), s(0))≥IF_GCD(le(0, x8), s(x8), s(0)))
(18) (GCD(s(x8), s(x47))≥IF_GCD(le(x47, x8), s(x8), s(x47)) ⇒ GCD(s(x8), s(s(x47)))≥IF_GCD(le(s(x47), x8), s(x8), s(s(x47))))
(19) (IF_GCD(le(x11, x10), s(x10), s(x11))=IF_GCD(true, x12, x13) ⇒ IF_GCD(true, x12, x13)≥GCD(minus(x12, x13), x13))
(20) (le(x11, x10)=true ⇒ IF_GCD(true, s(x10), s(x11))≥GCD(minus(s(x10), s(x11)), s(x11)))
(21) (true=true ⇒ IF_GCD(true, s(x50), s(0))≥GCD(minus(s(x50), s(0)), s(0)))
(22) (le(x53, x52)=true∧(le(x53, x52)=true ⇒ IF_GCD(true, s(x52), s(x53))≥GCD(minus(s(x52), s(x53)), s(x53))) ⇒ IF_GCD(true, s(s(x52)), s(s(x53)))≥GCD(minus(s(s(x52)), s(s(x53))), s(s(x53))))
(23) (IF_GCD(true, s(x50), s(0))≥GCD(minus(s(x50), s(0)), s(0)))
(24) (IF_GCD(true, s(x52), s(x53))≥GCD(minus(s(x52), s(x53)), s(x53)) ⇒ IF_GCD(true, s(s(x52)), s(s(x53)))≥GCD(minus(s(s(x52)), s(s(x53))), s(s(x53))))
(25) (IF_GCD(le(x19, x18), s(x18), s(x19))=IF_GCD(false, x20, x21) ⇒ IF_GCD(false, x20, x21)≥GCD(minus(x21, x20), x20))
(26) (le(x19, x18)=false ⇒ IF_GCD(false, s(x18), s(x19))≥GCD(minus(s(x19), s(x18)), s(x18)))
(27) (false=false ⇒ IF_GCD(false, s(0), s(s(x55)))≥GCD(minus(s(s(x55)), s(0)), s(0)))
(28) (le(x57, x56)=false∧(le(x57, x56)=false ⇒ IF_GCD(false, s(x56), s(x57))≥GCD(minus(s(x57), s(x56)), s(x56))) ⇒ IF_GCD(false, s(s(x56)), s(s(x57)))≥GCD(minus(s(s(x57)), s(s(x56))), s(s(x56))))
(29) (IF_GCD(false, s(0), s(s(x55)))≥GCD(minus(s(s(x55)), s(0)), s(0)))
(30) (IF_GCD(false, s(x56), s(x57))≥GCD(minus(s(x57), s(x56)), s(x56)) ⇒ IF_GCD(false, s(s(x56)), s(s(x57)))≥GCD(minus(s(s(x57)), s(s(x56))), s(s(x56))))
POL(0) = 0
POL(GCD(x1, x2)) = -1 + x2
POL(IF_GCD(x1, x2, x3)) = -1 - x1 + x3
POL(c) = -1
POL(false) = 0
POL(le(x1, x2)) = 0
POL(minus(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
IF_GCD(false, x, y) → GCD(minus(y, x), x)
The following rules are usable:
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
IF_GCD(false, x, y) → GCD(minus(y, x), x)
le(x, y) → le(s(x), s(y))
true → le(0, y)
false → le(s(x), 0)
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
GCD(s(0), s(s(x0))) → IF_GCD(false, s(0), s(s(x0)))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
GCD(s(0), s(s(x0))) → IF_GCD(false, s(0), s(s(x0)))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, x, y) → GCD(minus(x, y), y)
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
IF_GCD(true, x0, 0) → GCD(x0, 0)
IF_GCD(true, 0, x0) → GCD(0, x0)
IF_GCD(true, s(x0), s(x1)) → GCD(minus(x0, x1), s(x1))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
IF_GCD(true, x0, 0) → GCD(x0, 0)
IF_GCD(true, 0, x0) → GCD(0, x0)
IF_GCD(true, s(x0), s(x1)) → GCD(minus(x0, x1), s(x1))
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
IF_GCD(true, s(x0), s(x1)) → GCD(minus(x0, x1), s(x1))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
IF_GCD(true, s(z0), s(0)) → GCD(minus(z0, 0), s(0))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(minus(s(z0), s(z1)), s(s(z1)))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
IF_GCD(true, s(z0), s(0)) → GCD(minus(z0, 0), s(0))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(minus(s(z0), s(z1)), s(s(z1)))
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(minus(s(z0), s(z1)), s(s(z1)))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(minus(z0, z1), s(s(z1)))
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(minus(z0, z1), s(s(z1)))
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(minus(z0, z1), s(s(z1)))
POL(0) = 0
POL(GCD(x1, x2)) = 1 + x1
POL(IF_GCD(x1, x2, x3)) = 1 + x2
POL(false) = 0
POL(le(x1, x2)) = 0
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(true) = 0
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
IF_GCD(true, s(z0), s(0)) → GCD(minus(z0, 0), s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
minus(x, 0) → x
minus(0, x) → 0
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
IF_GCD(true, s(z0), s(0)) → GCD(minus(z0, 0), s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
minus(x, 0) → x
minus(0, x) → 0
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
IF_GCD(true, s(z0), s(0)) → GCD(minus(z0, 0), s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
minus(x, 0) → x
minus(0, x) → 0
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
IF_GCD(true, s(z0), s(0)) → GCD(z0, s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(z0, s(0))
minus(x, 0) → x
minus(0, x) → 0
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(z0, s(0))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(z0, s(0))
IF_GCD(true, s(s(y_0)), s(0)) → GCD(s(y_0), s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(s(y_0)), s(0)) → GCD(s(y_0), s(0))
GCD(s(s(y_0)), s(0)) → IF_GCD(true, s(s(y_0)), s(0))
IF_GCD(true, s(s(y_0)), s(0)) → GCD(s(y_0), s(0))
GCD(s(s(y_0)), s(0)) → IF_GCD(true, s(s(y_0)), s(0))
From the DPs we obtained the following set of size-change graphs: