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 Instantiation (⇔)
↳27 QDP
↳28 NonInfProof (⇔)
↳29 QDP
↳30 Instantiation (⇔)
↳31 QDP
↳32 Narrowing (⇔)
↳33 QDP
↳34 DependencyGraphProof (⇔)
↳35 QDP
↳36 Narrowing (⇔)
↳37 QDP
↳38 DependencyGraphProof (⇔)
↳39 QDP
↳40 Instantiation (⇔)
↳41 QDP
↳42 DependencyGraphProof (⇔)
↳43 AND
↳44 QDP
↳45 Rewriting (⇔)
↳46 QDP
↳47 QDPOrderProof (⇔)
↳48 QDP
↳49 DependencyGraphProof (⇔)
↳50 TRUE
↳51 QDP
↳52 UsableRulesProof (⇔)
↳53 QDP
↳54 QReductionProof (⇔)
↳55 QDP
↳56 Rewriting (⇔)
↳57 QDP
↳58 UsableRulesProof (⇔)
↳59 QDP
↳60 QReductionProof (⇔)
↳61 QDP
↳62 Rewriting (⇔)
↳63 QDP
↳64 UsableRulesProof (⇔)
↳65 QDP
↳66 QReductionProof (⇔)
↳67 QDP
↳68 ForwardInstantiation (⇔)
↳69 QDP
↳70 ForwardInstantiation (⇔)
↳71 QDP
↳72 QDPSizeChangeProof (⇔)
↳73 TRUE
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(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)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(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))
pred(s(x0))
minus(x0, 0)
minus(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(x, s(y)) → PRED(minus(x, y))
MINUS(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)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(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))
pred(s(x0))
minus(x0, 0)
minus(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(x, s(y)) → MINUS(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(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))
pred(s(x0))
minus(x0, 0)
minus(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(x, s(y)) → MINUS(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(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))
pred(s(x0))
minus(x0, 0)
minus(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(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)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(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))
pred(s(x0))
minus(x0, 0)
minus(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))
pred(s(x0))
minus(x0, 0)
minus(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))
pred(s(x0))
minus(x0, 0)
minus(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)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(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))
pred(s(x0))
minus(x0, 0)
minus(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(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(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(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
IF_GCD(true, s(z0), s(z1)) → GCD(minus(s(z0), s(z1)), s(z1))
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(false, x, y) → GCD(minus(y, x), x)
IF_GCD(true, s(z0), s(z1)) → GCD(minus(s(z0), s(z1)), s(z1))
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(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) (pred(minus(x29, x28))=s(x4)∧s(x5)=s(x28)∧(∀x30,x31:minus(x29, x28)=s(x30)∧s(x31)=x28 ⇒ GCD(s(x30), s(x31))≥IF_GCD(le(x31, x30), s(x30), s(x31))) ⇒ GCD(s(x4), s(x5))≥IF_GCD(le(x5, x4), s(x4), s(x5)))
(5) (minus(x29, x28)=x32∧pred(x32)=s(x4)∧(∀x30,x31:minus(x29, x28)=s(x30)∧s(x31)=x28 ⇒ GCD(s(x30), s(x31))≥IF_GCD(le(x31, x30), s(x30), s(x31))) ⇒ GCD(s(x4), s(x28))≥IF_GCD(le(x28, x4), s(x4), s(x28)))
(6) (x33=s(x4)∧minus(x29, x28)=s(x33)∧(∀x30,x31:minus(x29, x28)=s(x30)∧s(x31)=x28 ⇒ GCD(s(x30), s(x31))≥IF_GCD(le(x31, x30), s(x30), s(x31))) ⇒ GCD(s(x4), s(x28))≥IF_GCD(le(x28, x4), s(x4), s(x28)))
(7) (minus(x29, x28)=s(s(x4)) ⇒ GCD(s(x4), s(x28))≥IF_GCD(le(x28, x4), s(x4), s(x28)))
(8) (x34=s(s(x4)) ⇒ GCD(s(x4), s(0))≥IF_GCD(le(0, x4), s(x4), s(0)))
(9) (pred(minus(x36, x35))=s(s(x4))∧(∀x37:minus(x36, x35)=s(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))))
(10) (GCD(s(x4), s(0))≥IF_GCD(le(0, x4), s(x4), s(0)))
(11) (GCD(s(x4), s(s(x35)))≥IF_GCD(le(s(x35), x4), s(x4), s(s(x35))))
(12) (GCD(minus(x7, x6), x6)=GCD(s(x8), s(x9)) ⇒ GCD(s(x8), s(x9))≥IF_GCD(le(x9, x8), s(x8), s(x9)))
(13) (s(x9)=x39∧minus(x7, x39)=s(x8) ⇒ GCD(s(x8), s(x9))≥IF_GCD(le(x9, x8), s(x8), s(x9)))
(14) (x40=s(x8)∧s(x9)=0 ⇒ GCD(s(x8), s(x9))≥IF_GCD(le(x9, x8), s(x8), s(x9)))
(15) (pred(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)))
(16) (minus(x42, x41)=x45∧pred(x45)=s(x8)∧(∀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(x41))≥IF_GCD(le(x41, x8), s(x8), s(x41)))
(17) (x46=s(x8)∧minus(x42, x41)=s(x46)∧(∀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(x41))≥IF_GCD(le(x41, x8), s(x8), s(x41)))
(18) (minus(x42, x41)=s(s(x8)) ⇒ GCD(s(x8), s(x41))≥IF_GCD(le(x41, x8), s(x8), s(x41)))
(19) (x47=s(s(x8)) ⇒ GCD(s(x8), s(0))≥IF_GCD(le(0, x8), s(x8), s(0)))
(20) (pred(minus(x49, x48))=s(s(x8))∧(∀x50:minus(x49, x48)=s(s(x50)) ⇒ GCD(s(x50), s(x48))≥IF_GCD(le(x48, x50), s(x50), s(x48))) ⇒ GCD(s(x8), s(s(x48)))≥IF_GCD(le(s(x48), x8), s(x8), s(s(x48))))
(21) (GCD(s(x8), s(0))≥IF_GCD(le(0, x8), s(x8), s(0)))
(22) (GCD(s(x8), s(s(x48)))≥IF_GCD(le(s(x48), x8), s(x8), s(s(x48))))
(23) (IF_GCD(le(x11, x10), s(x10), s(x11))=IF_GCD(true, x12, x13) ⇒ IF_GCD(true, x12, x13)≥GCD(minus(x12, x13), x13))
(24) (le(x11, x10)=true ⇒ IF_GCD(true, s(x10), s(x11))≥GCD(minus(s(x10), s(x11)), s(x11)))
(25) (true=true ⇒ IF_GCD(true, s(x52), s(0))≥GCD(minus(s(x52), s(0)), s(0)))
(26) (le(x55, x54)=true∧(le(x55, x54)=true ⇒ IF_GCD(true, s(x54), s(x55))≥GCD(minus(s(x54), s(x55)), s(x55))) ⇒ IF_GCD(true, s(s(x54)), s(s(x55)))≥GCD(minus(s(s(x54)), s(s(x55))), s(s(x55))))
(27) (IF_GCD(true, s(x52), s(0))≥GCD(minus(s(x52), s(0)), s(0)))
(28) (IF_GCD(true, s(x54), s(x55))≥GCD(minus(s(x54), s(x55)), s(x55)) ⇒ IF_GCD(true, s(s(x54)), s(s(x55)))≥GCD(minus(s(s(x54)), s(s(x55))), s(s(x55))))
(29) (IF_GCD(le(x19, x18), s(x18), s(x19))=IF_GCD(false, x20, x21) ⇒ IF_GCD(false, x20, x21)≥GCD(minus(x21, x20), x20))
(30) (le(x19, x18)=false ⇒ IF_GCD(false, s(x18), s(x19))≥GCD(minus(s(x19), s(x18)), s(x18)))
(31) (false=false ⇒ IF_GCD(false, s(0), s(s(x57)))≥GCD(minus(s(s(x57)), s(0)), s(0)))
(32) (le(x59, x58)=false∧(le(x59, x58)=false ⇒ IF_GCD(false, s(x58), s(x59))≥GCD(minus(s(x59), s(x58)), s(x58))) ⇒ IF_GCD(false, s(s(x58)), s(s(x59)))≥GCD(minus(s(s(x59)), s(s(x58))), s(s(x58))))
(33) (IF_GCD(false, s(0), s(s(x57)))≥GCD(minus(s(s(x57)), s(0)), s(0)))
(34) (IF_GCD(false, s(x58), s(x59))≥GCD(minus(s(x59), s(x58)), s(x58)) ⇒ IF_GCD(false, s(s(x58)), s(s(x59)))≥GCD(minus(s(s(x59)), s(s(x58))), s(s(x58))))
POL(0) = 0
POL(GCD(x1, x2)) = -1 + x2
POL(IF_GCD(x1, x2, x3)) = -1 + x3
POL(c) = -1
POL(false) = 1
POL(le(x1, x2)) = 0
POL(minus(x1, x2)) = 0
POL(pred(x1)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 1
The following pairs are in Pbound:
IF_GCD(false, x, y) → GCD(minus(y, x), x)
There are no usable rules
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)
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(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
IF_GCD(true, s(z0), s(z1)) → GCD(minus(s(z0), s(z1)), s(z1))
GCD(s(x), s(y)) → IF_GCD(le(y, x), s(x), s(y))
IF_GCD(true, s(z0), s(z1)) → GCD(minus(s(z0), s(z1)), s(z1))
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(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(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(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(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
IF_GCD(true, x0, 0) → GCD(x0, 0)
IF_GCD(true, x0, s(x1)) → GCD(pred(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, x0, s(x1)) → GCD(pred(minus(x0, x1)), s(x1))
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
IF_GCD(true, x0, s(x1)) → GCD(pred(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(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
IF_GCD(true, s(z0), s(0)) → GCD(pred(minus(s(z0), 0)), s(0))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(minus(s(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(pred(minus(s(z0), 0)), s(0))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(minus(s(s(z0)), s(z1))), s(s(z1)))
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(minus(s(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(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(pred(minus(s(s(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(pred(pred(minus(s(s(z0)), z1))), s(s(z1)))
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GCD(s(s(x1)), s(s(x0))) → IF_GCD(le(x0, x1), s(s(x1)), s(s(x0)))
POL(GCD(x1, x2)) =
/ 0 \ \ 0 / +
/ 1 0 \ \ 0 0 / · x1 +
/ 0 0 \ \ 1 0 / · x2
POL(s(x1)) =
/ 1 \ \ 0 / +
/ 1 1 \ \ 1 1 / · x1
POL(IF_GCD(x1, x2, x3)) =
/ 0 \ \ 1 / +
/ 0 0 \ \ 0 0 / · x1 +
/ 0 1 \ \ 0 0 / · x2 +
/ 0 0 \ \ 0 1 / · x3
POL(le(x1, x2)) =
/ 0 \ \ 0 / +
/ 0 0 \ \ 0 0 / · x1 +
/ 1 1 \ \ 1 1 / · x2
POL(true) =
/ 1 \ \ 1 /
POL(pred(x1)) =
/ 0 \ \ 0 / +
/ 0 1 \ \ 0 1 / · x1
POL(minus(x1, x2)) =
/ 0 \ \ 0 / +
/ 1 1 \ \ 0 1 / · x1 +
/ 0 0 \ \ 0 0 / · x2
POL(0) =
/ 0 \ \ 0 /
POL(false) =
/ 1 \ \ 0 /
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
IF_GCD(true, s(s(z0)), s(s(z1))) → GCD(pred(pred(minus(s(s(z0)), z1))), s(s(z1)))
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
IF_GCD(true, s(z0), s(0)) → GCD(pred(minus(s(z0), 0)), s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
pred(s(x)) → x
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))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
IF_GCD(true, s(z0), s(0)) → GCD(pred(minus(s(z0), 0)), s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
minus(x, 0) → x
pred(s(x)) → x
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
IF_GCD(true, s(z0), s(0)) → GCD(pred(minus(s(z0), 0)), s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
minus(x, 0) → x
pred(s(x)) → x
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
IF_GCD(true, s(z0), s(0)) → GCD(pred(s(z0)), s(0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(pred(s(z0)), s(0))
minus(x, 0) → x
pred(s(x)) → x
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(pred(s(z0)), s(0))
pred(s(x)) → x
pred(s(x0))
minus(x0, 0)
minus(x0, s(x1))
minus(x0, 0)
minus(x0, s(x1))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(pred(s(z0)), s(0))
pred(s(x)) → x
pred(s(x0))
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))
pred(s(x)) → x
pred(s(x0))
GCD(s(x0), s(0)) → IF_GCD(true, s(x0), s(0))
IF_GCD(true, s(z0), s(0)) → GCD(z0, s(0))
pred(s(x0))
pred(s(x0))
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: