18.16/5.10 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

18.16/5.10

18.16/5.10
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxRelTRS

18.16/5.10

↳1 CpxRelTrsToCDT (UPPER BOUND (ID))

18.16/5.10

↳2 CdtProblem

18.16/5.10

↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

18.16/5.10

↳4 CdtProblem

18.16/5.10

↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))

18.16/5.10

↳6 CdtProblem

18.16/5.10

↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

18.16/5.10

↳8 CdtProblem

18.16/5.10

↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

18.16/5.10

↳10 CdtProblem

18.16/5.10

↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

18.16/5.10

↳12 CdtProblem

18.16/5.10

↳13 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))

18.16/5.10

↳14 CdtProblem

18.16/5.10

↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

18.16/5.10

↳16 CdtProblem

18.16/5.10

↳17 CdtKnowledgeProof (⇔)

18.16/5.10

↳18 BOUNDS(O(1), O(1))

18.16/5.10

18.16/5.10 18.16/5.10

18.16/5.10

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

m2(S(0), b, res, True) → False 18.16/5.10
m2(S(S(x)), b, res, True) → True 18.16/5.10
m2(0, b, res, True) → False 18.16/5.10
m3(S(0), b, res, t) → False 18.16/5.10
m3(S(S(x)), b, res, t) → True 18.16/5.10
m3(0, b, res, t) → False 18.16/5.10
l8(res, y, res', True, mtmp, t) → res 18.16/5.10
l5(x, y, res, tmp, mtmp, True) → 0 18.16/5.10
help1(S(0)) → False 18.16/5.10
help1(S(S(x))) → True 18.16/5.10
e4(a, b, res, False) → False 18.16/5.10
e4(a, b, res, True) → True 18.16/5.10
e2(a, b, res, False) → False 18.16/5.10
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0), tmp, False, t) 18.16/5.10
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0)), tmp, True, t) 18.16/5.10
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0, y), tmp, False, t) 19.31/5.32
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0), y), tmp, True, t) 19.31/5.32
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t) 19.31/5.32
m2(a, b, res, False) → m4(a, b, res, False) 19.31/5.32
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t) 19.31/5.32
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False) 19.31/5.32
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False) 19.31/5.32
l2(x, y, res, tmp, mtmp, True) → res 19.31/5.32
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False) 19.31/5.32
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True) 19.31/5.32
help1(0) → False 19.31/5.32
e2(a, b, res, True) → e3(a, b, res, True) 19.31/5.32
bool2Nat(False) → 0 19.31/5.32
bool2Nat(True) → S(0) 19.31/5.32
m1(a, x, res, t) → m2(a, x, res, False) 19.31/5.32
l9(res, y, res', tmp, mtmp, t) → res 19.31/5.32
l6(x, y, res, tmp, mtmp, t) → 0 19.31/5.32
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False) 19.31/5.32
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False) 19.31/5.32
e7(a, b, res, t) → False 19.31/5.32
e6(a, b, res, t) → False 19.31/5.32
e5(a, b, res, t) → True 19.31/5.32
monus(a, b) → m1(a, b, False, False) 19.31/5.32
m5(a, b, res, t) → res 19.31/5.32
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t) 19.31/5.32
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0, tmp, mtmp, t) 19.31/5.32
l16(x, y, res, tmp, mtmp, t) → res 19.31/5.32
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t) 19.31/5.32
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t) 19.31/5.32
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y)) 19.31/5.32
gcd(x, y) → l1(x, y, 0, False, False, False) 19.31/5.32
equal0(a, b) → e1(a, b, False, False) 19.31/5.32
e8(a, b, res, t) → res 19.31/5.32
e3(a, b, res, t) → e4(a, b, res, <(b, a)) 19.31/5.32
e1(a, b, res, t) → e2(a, b, res, <(a, b))

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y) 19.31/5.32
<(0, S(y)) → True 19.31/5.32
<(x, 0) → False

Rewrite Strategy: INNERMOST

19.31/5.32

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.

19.31/5.32

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.32
<(0, S(z0)) → True 19.31/5.32
<(z0, 0) → False 19.31/5.32
m2(S(0), z0, z1, True) → False 19.31/5.32
m2(S(S(z0)), z1, z2, True) → True 19.31/5.32
m2(0, z0, z1, True) → False 19.31/5.32
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.32
m3(S(0), z0, z1, z2) → False 19.31/5.32
m3(S(S(z0)), z1, z2, z3) → True 19.31/5.32
m3(0, z0, z1, z2) → False 19.31/5.32
l8(z0, z1, z2, True, z3, z4) → z0 19.31/5.32
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4) 19.31/5.32
l5(z0, z1, z2, z3, z4, True) → 0 19.31/5.32
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False) 19.31/5.32
help1(S(0)) → False 19.31/5.32
help1(S(S(z0))) → True 19.31/5.32
help1(0) → False 19.31/5.32
e4(z0, z1, z2, False) → False 19.31/5.32
e4(z0, z1, z2, True) → True 19.31/5.32
e2(z0, z1, z2, False) → False 19.31/5.32
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.32
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4) 19.31/5.32
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4) 19.31/5.32
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4) 19.31/5.32
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4) 19.31/5.32
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.32
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False) 19.31/5.32
l2(z0, z1, z2, z3, z4, True) → z2 19.31/5.32
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False) 19.31/5.32
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True) 19.31/5.32
bool2Nat(False) → 0 19.31/5.32
bool2Nat(True) → S(0) 19.31/5.32
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.32
l9(z0, z1, z2, z3, z4, z5) → z0 19.31/5.32
l6(z0, z1, z2, z3, z4, z5) → 0 19.31/5.32
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False) 19.31/5.32
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False) 19.31/5.32
e7(z0, z1, z2, z3) → False 19.31/5.32
e6(z0, z1, z2, z3) → False 19.31/5.32
e5(z0, z1, z2, z3) → True 19.31/5.32
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.32
m5(z0, z1, z2, z3) → z2 19.31/5.32
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5) 19.31/5.32
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5) 19.31/5.32
l16(z0, z1, z2, z3, z4, z5) → z2 19.31/5.32
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.32
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.32
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1)) 19.31/5.32
gcd(z0, z1) → l1(z0, z1, 0, False, False, False) 19.31/5.32
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.32
e8(z0, z1, z2, z3) → z2 19.31/5.32
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.32
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.32
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.32
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.32
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.32
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.32
L15(z0, z1, z2, z3, False, z4) → c21(L16(z0, z1, gcd(z1, 0), z3, False, z4), GCD(z1, 0)) 19.31/5.32
L15(z0, z1, z2, z3, True, z4) → c22(L16(z0, z1, gcd(z1, S(0)), z3, True, z4), GCD(z1, S(0))) 19.31/5.32
L13(z0, z1, z2, z3, False, z4) → c23(L16(z0, z1, gcd(0, z1), z3, False, z4), GCD(0, z1)) 19.31/5.32
L13(z0, z1, z2, z3, True, z4) → c24(L16(z0, z1, gcd(S(0), z1), z3, True, z4), GCD(S(0), z1)) 19.31/5.32
M4(S(z0), S(z1), z2, z3) → c25(M5(S(z0), S(z1), monus(z0, z1), z3), MONUS(z0, z1)) 19.31/5.32
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.32
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.32
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.32
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.32
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.32
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.32
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.32
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.32
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.32
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.32
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.32
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.32
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.32
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.32
E3(z0, z1, z2, z3) → c51(E4(z0, z1, z2, <(z1, z0)), <'(z1, z0)) 19.31/5.32
E1(z0, z1, z2, z3) → c52(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.32
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.32
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.32
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.32
L15(z0, z1, z2, z3, False, z4) → c21(L16(z0, z1, gcd(z1, 0), z3, False, z4), GCD(z1, 0)) 19.31/5.32
L15(z0, z1, z2, z3, True, z4) → c22(L16(z0, z1, gcd(z1, S(0)), z3, True, z4), GCD(z1, S(0))) 19.31/5.32
L13(z0, z1, z2, z3, False, z4) → c23(L16(z0, z1, gcd(0, z1), z3, False, z4), GCD(0, z1)) 19.31/5.32
L13(z0, z1, z2, z3, True, z4) → c24(L16(z0, z1, gcd(S(0), z1), z3, True, z4), GCD(S(0), z1)) 19.31/5.36
M4(S(z0), S(z1), z2, z3) → c25(M5(S(z0), S(z1), monus(z0, z1), z3), MONUS(z0, z1)) 19.31/5.36
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.36
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.36
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.36
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.36
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.36
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.36
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.36
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.36
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.36
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.36
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.36
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.36
E3(z0, z1, z2, z3) → c51(E4(z0, z1, z2, <(z1, z0)), <'(z1, z0)) 19.31/5.36
E1(z0, z1, z2, z3) → c52(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1))

K tuples:none
Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, L8, L5, E2, L15, L13, M4, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c21, c22, c23, c24, c25, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c51, c52

19.31/5.36

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 6 trailing tuple parts

19.31/5.36

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.36
<(0, S(z0)) → True 19.31/5.36
<(z0, 0) → False 19.31/5.36
m2(S(0), z0, z1, True) → False 19.31/5.36
m2(S(S(z0)), z1, z2, True) → True 19.31/5.36
m2(0, z0, z1, True) → False 19.31/5.36
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.36
m3(S(0), z0, z1, z2) → False 19.31/5.36
m3(S(S(z0)), z1, z2, z3) → True 19.31/5.36
m3(0, z0, z1, z2) → False 19.31/5.36
l8(z0, z1, z2, True, z3, z4) → z0 19.31/5.36
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4) 19.31/5.36
l5(z0, z1, z2, z3, z4, True) → 0 19.31/5.36
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False) 19.31/5.36
help1(S(0)) → False 19.31/5.36
help1(S(S(z0))) → True 19.31/5.36
help1(0) → False 19.31/5.36
e4(z0, z1, z2, False) → False 19.31/5.36
e4(z0, z1, z2, True) → True 19.31/5.36
e2(z0, z1, z2, False) → False 19.31/5.36
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.36
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4) 19.31/5.36
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4) 19.31/5.36
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4) 19.31/5.36
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4) 19.31/5.36
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.36
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False) 19.31/5.36
l2(z0, z1, z2, z3, z4, True) → z2 19.31/5.36
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False) 19.31/5.36
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True) 19.31/5.36
bool2Nat(False) → 0 19.31/5.36
bool2Nat(True) → S(0) 19.31/5.36
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.36
l9(z0, z1, z2, z3, z4, z5) → z0 19.31/5.36
l6(z0, z1, z2, z3, z4, z5) → 0 19.31/5.36
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False) 19.31/5.36
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False) 19.31/5.36
e7(z0, z1, z2, z3) → False 19.31/5.36
e6(z0, z1, z2, z3) → False 19.31/5.36
e5(z0, z1, z2, z3) → True 19.31/5.36
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.36
m5(z0, z1, z2, z3) → z2 19.31/5.36
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5) 19.31/5.36
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5) 19.31/5.36
l16(z0, z1, z2, z3, z4, z5) → z2 19.31/5.36
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.36
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.36
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1)) 19.31/5.36
gcd(z0, z1) → l1(z0, z1, 0, False, False, False) 19.31/5.36
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.36
e8(z0, z1, z2, z3) → z2 19.31/5.36
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.36
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.36
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.36
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.36
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.36
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.36
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.36
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.36
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.36
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.36
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.36
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.36
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.36
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.36
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.36
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.36
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.36
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.36
E1(z0, z1, z2, z3) → c52(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1)) 19.31/5.36
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.36
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.36
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.36
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.36
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.36
E3(z0, z1, z2, z3) → c51(<'(z1, z0))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.36
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.36
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.36
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.36
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.36
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.36
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.36
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.36
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.36
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.36
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.36
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.36
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.36
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.36
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.36
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.36
E1(z0, z1, z2, z3) → c52(E2(z0, z1, z2, <(z0, z1)), <'(z0, z1)) 19.31/5.36
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.36
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.36
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.36
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.36
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.36
E3(z0, z1, z2, z3) → c51(<'(z1, z0))

K tuples:none
Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, E1, L15, L13, M4, E3

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c52, c21, c22, c23, c24, c25, c51

19.31/5.36

(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

19.31/5.36

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.36
<(0, S(z0)) → True 19.31/5.36
<(z0, 0) → False 19.31/5.36
m2(S(0), z0, z1, True) → False 19.31/5.36
m2(S(S(z0)), z1, z2, True) → True 19.31/5.36
m2(0, z0, z1, True) → False 19.31/5.36
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.36
m3(S(0), z0, z1, z2) → False 19.31/5.36
m3(S(S(z0)), z1, z2, z3) → True 19.31/5.36
m3(0, z0, z1, z2) → False 19.31/5.36
l8(z0, z1, z2, True, z3, z4) → z0 19.31/5.36
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4) 19.31/5.36
l5(z0, z1, z2, z3, z4, True) → 0 19.31/5.36
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False) 19.31/5.36
help1(S(0)) → False 19.31/5.36
help1(S(S(z0))) → True 19.31/5.36
help1(0) → False 19.31/5.36
e4(z0, z1, z2, False) → False 19.31/5.36
e4(z0, z1, z2, True) → True 19.31/5.36
e2(z0, z1, z2, False) → False 19.31/5.36
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.36
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4) 19.31/5.36
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4) 19.31/5.36
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4) 19.31/5.36
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4) 19.31/5.36
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.36
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False) 19.31/5.36
l2(z0, z1, z2, z3, z4, True) → z2 19.31/5.36
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False) 19.31/5.36
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True) 19.31/5.36
bool2Nat(False) → 0 19.31/5.36
bool2Nat(True) → S(0) 19.31/5.36
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.36
l9(z0, z1, z2, z3, z4, z5) → z0 19.31/5.36
l6(z0, z1, z2, z3, z4, z5) → 0 19.31/5.36
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False) 19.31/5.36
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False) 19.31/5.36
e7(z0, z1, z2, z3) → False 19.31/5.36
e6(z0, z1, z2, z3) → False 19.31/5.36
e5(z0, z1, z2, z3) → True 19.31/5.36
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.36
m5(z0, z1, z2, z3) → z2 19.31/5.36
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5) 19.31/5.36
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5) 19.31/5.36
l16(z0, z1, z2, z3, z4, z5) → z2 19.31/5.36
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.36
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.36
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1)) 19.31/5.36
gcd(z0, z1) → l1(z0, z1, 0, False, False, False) 19.31/5.36
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.36
e8(z0, z1, z2, z3) → z2 19.31/5.36
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.36
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.36
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.36
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.36
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.36
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.36
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.36
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.36
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.36
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.36
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.36
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.36
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.36
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.36
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.36
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.36
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.36
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.36
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.36
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.36
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.36
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.36
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.36
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.36
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.36
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.36
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.36
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.36
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.36
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.36
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.36
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.36
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.36
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.36
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.36
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.36
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.36
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.36
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.36
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.36
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.36
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.36
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.36
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.36
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.36
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.36
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.36
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.36
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

K tuples:none
Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

19.31/5.36

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))

We considered the (Usable) Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.36
<(0, S(z0)) → True 19.31/5.36
<(z0, 0) → False 19.31/5.36
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.36
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.36
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.36
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.36
m5(z0, z1, z2, z3) → z2 19.31/5.36
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.36
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1)) 19.31/5.36
e2(z0, z1, z2, False) → False 19.31/5.36
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.36
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.36
e4(z0, z1, z2, False) → False 19.31/5.36
e4(z0, z1, z2, True) → True

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.36
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.36
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.36
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.36
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.36
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.36
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.36
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.36
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.36
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.36
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.36
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.36
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.36
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.37
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.37
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.37
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.37
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.37
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.37
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.37
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.37
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.37
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.37
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.37
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.37
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 19.31/5.37

POL(0) = 0 19.31/5.37
POL(<(x₁, x₂)) = 0 19.31/5.37
POL(<'(x₁, x₂)) = 0 19.31/5.37
POL(E1(x₁, x₂, x₃, x₄)) = x₃ + x₄ 19.31/5.37
POL(E2(x₁, x₂, x₃, x₄)) = 0 19.31/5.37
POL(E3(x₁, x₂, x₃, x₄)) = 0 19.31/5.37
POL(EQUAL0(x₁, x₂)) = 0 19.31/5.37
POL(False) = 0 19.31/5.37
POL(GCD(x₁, x₂)) = 0 19.31/5.37
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃ + x₄ + x₅ + x₆ 19.31/5.37
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄ 19.31/5.37
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = 0 19.31/5.37
POL(L12(x₁, x₂, x₃, x₄, x₅, x₆)) = 0 19.31/5.37
POL(L13(x₁, x₂, x₃, x₄, x₅, x₆)) = x₅ 19.31/5.37
POL(L14(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆ 19.31/5.37
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = 0 19.31/5.37
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄ + x₆ 19.31/5.37
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄ + x₆ 19.31/5.37
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃ 19.31/5.37
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆ 19.31/5.37
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆ 19.31/5.37
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆ 19.31/5.37
POL(M1(x₁, x₂, x₃, x₄)) = x₃ + x₄ 19.31/5.37
POL(M2(x₁, x₂, x₃, x₄)) = x₄ 19.31/5.37
POL(M4(x₁, x₂, x₃, x₄)) = x₄ 19.31/5.37
POL(MONUS(x₁, x₂)) = 0 19.31/5.37
POL(S(x₁)) = 0 19.31/5.37
POL(True) = [1] 19.31/5.37
POL(c(x₁)) = x₁ 19.31/5.37
POL(c1(x₁)) = x₁ 19.31/5.37
POL(c11(x₁)) = x₁ 19.31/5.37
POL(c13(x₁)) = x₁ 19.31/5.37
POL(c20(x₁)) = x₁ 19.31/5.37
POL(c21(x₁)) = x₁ 19.31/5.37
POL(c22(x₁)) = x₁ 19.31/5.37
POL(c23(x₁)) = x₁ 19.31/5.37
POL(c24(x₁)) = x₁ 19.31/5.37
POL(c25(x₁)) = x₁ 19.31/5.37
POL(c26(x₁)) = x₁ 19.31/5.37
POL(c28(x₁)) = x₁ 19.31/5.37
POL(c29(x₁)) = x₁ 19.31/5.37
POL(c32(x₁)) = x₁ 19.31/5.37
POL(c35(x₁)) = x₁ 19.31/5.37
POL(c36(x₁)) = x₁ 19.31/5.37
POL(c40(x₁)) = x₁ 19.31/5.37
POL(c42(x₁, x₂)) = x₁ + x₂ 19.31/5.37
POL(c43(x₁)) = x₁ 19.31/5.37
POL(c45(x₁, x₂)) = x₁ + x₂ 19.31/5.37
POL(c46(x₁, x₂)) = x₁ + x₂ 19.31/5.37
POL(c47(x₁, x₂)) = x₁ + x₂ 19.31/5.37
POL(c48(x₁)) = x₁ 19.31/5.37
POL(c49(x₁)) = x₁ 19.31/5.37
POL(c51(x₁)) = x₁ 19.31/5.37
POL(c6(x₁)) = x₁ 19.31/5.37
POL(e1(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + x₃ + x₄ 19.31/5.37
POL(e2(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ 19.31/5.37
POL(e3(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ + x₄ 19.31/5.37
POL(e4(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ 19.31/5.37
POL(equal0(x₁, x₂)) = 0 19.31/5.37
POL(m1(x₁, x₂, x₃, x₄)) = x₃ + x₄ 19.31/5.37
POL(m2(x₁, x₂, x₃, x₄)) = x₄ 19.31/5.37
POL(m4(x₁, x₂, x₃, x₄)) = x₄ 19.31/5.37
POL(m5(x₁, x₂, x₃, x₄)) = [4]x₃ 19.31/5.37
POL(monus(x₁, x₂)) = 0

19.31/5.37

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.37
<(0, S(z0)) → True 19.31/5.37
<(z0, 0) → False 19.31/5.37
m2(S(0), z0, z1, True) → False 19.31/5.37
m2(S(S(z0)), z1, z2, True) → True 19.31/5.37
m2(0, z0, z1, True) → False 19.31/5.37
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.37
m3(S(0), z0, z1, z2) → False 19.31/5.37
m3(S(S(z0)), z1, z2, z3) → True 19.31/5.37
m3(0, z0, z1, z2) → False 19.31/5.37
l8(z0, z1, z2, True, z3, z4) → z0 19.31/5.37
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4) 19.31/5.37
l5(z0, z1, z2, z3, z4, True) → 0 19.31/5.37
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False) 19.31/5.37
help1(S(0)) → False 19.31/5.37
help1(S(S(z0))) → True 19.31/5.37
help1(0) → False 19.31/5.37
e4(z0, z1, z2, False) → False 19.31/5.37
e4(z0, z1, z2, True) → True 19.31/5.37
e2(z0, z1, z2, False) → False 19.31/5.37
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.37
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4) 19.31/5.37
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4) 19.31/5.37
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4) 19.31/5.37
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4) 19.31/5.37
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.37
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False) 19.31/5.37
l2(z0, z1, z2, z3, z4, True) → z2 19.31/5.37
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False) 19.31/5.37
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True) 19.31/5.37
bool2Nat(False) → 0 19.31/5.37
bool2Nat(True) → S(0) 19.31/5.37
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.37
l9(z0, z1, z2, z3, z4, z5) → z0 19.31/5.37
l6(z0, z1, z2, z3, z4, z5) → 0 19.31/5.37
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False) 19.31/5.37
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False) 19.31/5.37
e7(z0, z1, z2, z3) → False 19.31/5.37
e6(z0, z1, z2, z3) → False 19.31/5.37
e5(z0, z1, z2, z3) → True 19.31/5.37
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.37
m5(z0, z1, z2, z3) → z2 19.31/5.37
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5) 19.31/5.37
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5) 19.31/5.37
l16(z0, z1, z2, z3, z4, z5) → z2 19.31/5.37
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.37
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.37
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1)) 19.31/5.37
gcd(z0, z1) → l1(z0, z1, 0, False, False, False) 19.31/5.37
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.37
e8(z0, z1, z2, z3) → z2 19.31/5.37
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.37
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.37
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.37
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.37
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.37
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.37
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.37
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.37
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.37
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.37
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.37
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.37
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.37
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.37
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.37
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.37
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.37
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.37
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.37
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.37
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.37
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.37
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.37
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.37
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.37
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.37
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.37
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.37
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.37
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.37
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.37
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.37
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.37
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.37
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.37
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.37
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.37
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.37
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.37
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.37
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.37
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.37
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.37
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.37
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.37
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.37
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.37
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.37
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.37
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.37
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.37
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

K tuples:

L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))

Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

19.31/5.37

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))

We considered the (Usable) Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.37
<(0, S(z0)) → True 19.31/5.37
<(z0, 0) → False 19.31/5.37
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.37
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.37
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.37
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.37
m5(z0, z1, z2, z3) → z2 19.31/5.37
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.37
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1)) 19.31/5.37
e2(z0, z1, z2, False) → False 19.31/5.37
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.37
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.37
e4(z0, z1, z2, False) → False 19.31/5.37
e4(z0, z1, z2, True) → True

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.37
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.37
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.37
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.37
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.37
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.37
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.37
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.37
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.37
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.37
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.37
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.37
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.37
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.37
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.37
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.37
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.37
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.39
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 19.31/5.39

POL(0) = 0 19.31/5.39
POL(<(x₁, x₂)) = 0 19.31/5.39
POL(<'(x₁, x₂)) = 0 19.31/5.39
POL(E1(x₁, x₂, x₃, x₄)) = x₃ + x₄ 19.31/5.39
POL(E2(x₁, x₂, x₃, x₄)) = x₃ 19.31/5.39
POL(E3(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(EQUAL0(x₁, x₂)) = 0 19.31/5.39
POL(False) = 0 19.31/5.39
POL(GCD(x₁, x₂)) = 0 19.31/5.39
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃ + x₄ + x₅ + x₆ 19.31/5.39
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄ 19.31/5.39
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄ 19.31/5.39
POL(L12(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄ 19.31/5.39
POL(L13(x₁, x₂, x₃, x₄, x₅, x₆)) = 0 19.31/5.39
POL(L14(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆ 19.31/5.39
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = x₅ 19.31/5.39
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃ + x₆ 19.31/5.39
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆ 19.31/5.39
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃ 19.31/5.39
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃ + x₆ 19.31/5.39
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆ 19.31/5.39
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆ 19.31/5.39
POL(M1(x₁, x₂, x₃, x₄)) = x₃ + x₄ 19.31/5.39
POL(M2(x₁, x₂, x₃, x₄)) = x₄ 19.31/5.39
POL(M4(x₁, x₂, x₃, x₄)) = x₄ 19.31/5.39
POL(MONUS(x₁, x₂)) = 0 19.31/5.39
POL(S(x₁)) = 0 19.31/5.39
POL(True) = [2] 19.31/5.39
POL(c(x₁)) = x₁ 19.31/5.39
POL(c1(x₁)) = x₁ 19.31/5.39
POL(c11(x₁)) = x₁ 19.31/5.39
POL(c13(x₁)) = x₁ 19.31/5.39
POL(c20(x₁)) = x₁ 19.31/5.39
POL(c21(x₁)) = x₁ 19.31/5.39
POL(c22(x₁)) = x₁ 19.31/5.39
POL(c23(x₁)) = x₁ 19.31/5.39
POL(c24(x₁)) = x₁ 19.31/5.39
POL(c25(x₁)) = x₁ 19.31/5.39
POL(c26(x₁)) = x₁ 19.31/5.39
POL(c28(x₁)) = x₁ 19.31/5.39
POL(c29(x₁)) = x₁ 19.31/5.39
POL(c32(x₁)) = x₁ 19.31/5.39
POL(c35(x₁)) = x₁ 19.31/5.39
POL(c36(x₁)) = x₁ 19.31/5.39
POL(c40(x₁)) = x₁ 19.31/5.39
POL(c42(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c43(x₁)) = x₁ 19.31/5.39
POL(c45(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c46(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c47(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c48(x₁)) = x₁ 19.31/5.39
POL(c49(x₁)) = x₁ 19.31/5.39
POL(c51(x₁)) = x₁ 19.31/5.39
POL(c6(x₁)) = x₁ 19.31/5.39
POL(e1(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + x₃ + x₄ 19.31/5.39
POL(e2(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ 19.31/5.39
POL(e3(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ + x₄ 19.31/5.39
POL(e4(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ 19.31/5.39
POL(equal0(x₁, x₂)) = 0 19.31/5.39
POL(m1(x₁, x₂, x₃, x₄)) = x₃ + x₄ 19.31/5.39
POL(m2(x₁, x₂, x₃, x₄)) = x₃ + x₄ 19.31/5.39
POL(m4(x₁, x₂, x₃, x₄)) = x₄ 19.31/5.39
POL(m5(x₁, x₂, x₃, x₄)) = [4]x₃ 19.31/5.39
POL(monus(x₁, x₂)) = 0

19.31/5.39

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.39
<(0, S(z0)) → True 19.31/5.39
<(z0, 0) → False 19.31/5.39
m2(S(0), z0, z1, True) → False 19.31/5.39
m2(S(S(z0)), z1, z2, True) → True 19.31/5.39
m2(0, z0, z1, True) → False 19.31/5.39
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.39
m3(S(0), z0, z1, z2) → False 19.31/5.39
m3(S(S(z0)), z1, z2, z3) → True 19.31/5.39
m3(0, z0, z1, z2) → False 19.31/5.39
l8(z0, z1, z2, True, z3, z4) → z0 19.31/5.39
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4) 19.31/5.39
l5(z0, z1, z2, z3, z4, True) → 0 19.31/5.39
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False) 19.31/5.39
help1(S(0)) → False 19.31/5.39
help1(S(S(z0))) → True 19.31/5.39
help1(0) → False 19.31/5.39
e4(z0, z1, z2, False) → False 19.31/5.39
e4(z0, z1, z2, True) → True 19.31/5.39
e2(z0, z1, z2, False) → False 19.31/5.39
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.39
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4) 19.31/5.39
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4) 19.31/5.39
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4) 19.31/5.39
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4) 19.31/5.39
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.39
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False) 19.31/5.39
l2(z0, z1, z2, z3, z4, True) → z2 19.31/5.39
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False) 19.31/5.39
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True) 19.31/5.39
bool2Nat(False) → 0 19.31/5.39
bool2Nat(True) → S(0) 19.31/5.39
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.39
l9(z0, z1, z2, z3, z4, z5) → z0 19.31/5.39
l6(z0, z1, z2, z3, z4, z5) → 0 19.31/5.39
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False) 19.31/5.39
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False) 19.31/5.39
e7(z0, z1, z2, z3) → False 19.31/5.39
e6(z0, z1, z2, z3) → False 19.31/5.39
e5(z0, z1, z2, z3) → True 19.31/5.39
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.39
m5(z0, z1, z2, z3) → z2 19.31/5.39
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5) 19.31/5.39
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5) 19.31/5.39
l16(z0, z1, z2, z3, z4, z5) → z2 19.31/5.39
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.39
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.39
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1)) 19.31/5.39
gcd(z0, z1) → l1(z0, z1, 0, False, False, False) 19.31/5.39
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.39
e8(z0, z1, z2, z3) → z2 19.31/5.39
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.39
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.39
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.39
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.39
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.39
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.39
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.39
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.39
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.39
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.39
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.39
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.39
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.39
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.39
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.39
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.39
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.39
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.39
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.39
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.39
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.39
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.39
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.39
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

K tuples:

L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0)))

Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

19.31/5.39

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))

We considered the (Usable) Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.39
<(0, S(z0)) → True 19.31/5.39
<(z0, 0) → False 19.31/5.39
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.39
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.39
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.39
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.39
m5(z0, z1, z2, z3) → z2 19.31/5.39
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.39
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1)) 19.31/5.39
e2(z0, z1, z2, False) → False 19.31/5.39
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.39
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.39
e4(z0, z1, z2, False) → False 19.31/5.39
e4(z0, z1, z2, True) → True

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.39
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.39
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.39
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.39
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.39
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.39
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.39
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.39
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.39
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.39
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.39
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.39
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 19.31/5.39

POL(0) = 0 19.31/5.39
POL(<(x₁, x₂)) = 0 19.31/5.39
POL(<'(x₁, x₂)) = 0 19.31/5.39
POL(E1(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(E2(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(E3(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(EQUAL0(x₁, x₂)) = 0 19.31/5.39
POL(False) = [4] 19.31/5.39
POL(GCD(x₁, x₂)) = [2] 19.31/5.39
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = [2] + x₃ 19.31/5.39
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = 0 19.31/5.39
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = 0 19.31/5.39
POL(L12(x₁, x₂, x₃, x₄, x₅, x₆)) = 0 19.31/5.39
POL(L13(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₅ 19.31/5.39
POL(L14(x₁, x₂, x₃, x₄, x₅, x₆)) = 0 19.31/5.39
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = [4]x₅ 19.31/5.39
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = [2] 19.31/5.39
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = [1] 19.31/5.39
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = [1] + x₃ 19.31/5.39
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = [1] + x₃ 19.31/5.39
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = 0 19.31/5.39
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = 0 19.31/5.39
POL(M1(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(M2(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(M4(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(MONUS(x₁, x₂)) = 0 19.31/5.39
POL(S(x₁)) = 0 19.31/5.39
POL(True) = [1] 19.31/5.39
POL(c(x₁)) = x₁ 19.31/5.39
POL(c1(x₁)) = x₁ 19.31/5.39
POL(c11(x₁)) = x₁ 19.31/5.39
POL(c13(x₁)) = x₁ 19.31/5.39
POL(c20(x₁)) = x₁ 19.31/5.39
POL(c21(x₁)) = x₁ 19.31/5.39
POL(c22(x₁)) = x₁ 19.31/5.39
POL(c23(x₁)) = x₁ 19.31/5.39
POL(c24(x₁)) = x₁ 19.31/5.39
POL(c25(x₁)) = x₁ 19.31/5.39
POL(c26(x₁)) = x₁ 19.31/5.39
POL(c28(x₁)) = x₁ 19.31/5.39
POL(c29(x₁)) = x₁ 19.31/5.39
POL(c32(x₁)) = x₁ 19.31/5.39
POL(c35(x₁)) = x₁ 19.31/5.39
POL(c36(x₁)) = x₁ 19.31/5.39
POL(c40(x₁)) = x₁ 19.31/5.39
POL(c42(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c43(x₁)) = x₁ 19.31/5.39
POL(c45(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c46(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c47(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c48(x₁)) = x₁ 19.31/5.39
POL(c49(x₁)) = x₁ 19.31/5.39
POL(c51(x₁)) = x₁ 19.31/5.39
POL(c6(x₁)) = x₁ 19.31/5.39
POL(e1(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + x₃ + x₄ 19.31/5.39
POL(e2(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ 19.31/5.39
POL(e3(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ + x₄ 19.31/5.39
POL(e4(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ 19.31/5.39
POL(equal0(x₁, x₂)) = 0 19.31/5.39
POL(m1(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(m2(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(m4(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(m5(x₁, x₂, x₃, x₄)) = [2]x₃ 19.31/5.39
POL(monus(x₁, x₂)) = 0

19.31/5.39

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.39
<(0, S(z0)) → True 19.31/5.39
<(z0, 0) → False 19.31/5.39
m2(S(0), z0, z1, True) → False 19.31/5.39
m2(S(S(z0)), z1, z2, True) → True 19.31/5.39
m2(0, z0, z1, True) → False 19.31/5.39
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.39
m3(S(0), z0, z1, z2) → False 19.31/5.39
m3(S(S(z0)), z1, z2, z3) → True 19.31/5.39
m3(0, z0, z1, z2) → False 19.31/5.39
l8(z0, z1, z2, True, z3, z4) → z0 19.31/5.39
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4) 19.31/5.39
l5(z0, z1, z2, z3, z4, True) → 0 19.31/5.39
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False) 19.31/5.39
help1(S(0)) → False 19.31/5.39
help1(S(S(z0))) → True 19.31/5.39
help1(0) → False 19.31/5.39
e4(z0, z1, z2, False) → False 19.31/5.39
e4(z0, z1, z2, True) → True 19.31/5.39
e2(z0, z1, z2, False) → False 19.31/5.39
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.39
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4) 19.31/5.39
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4) 19.31/5.39
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4) 19.31/5.39
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4) 19.31/5.39
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.39
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False) 19.31/5.39
l2(z0, z1, z2, z3, z4, True) → z2 19.31/5.39
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False) 19.31/5.39
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True) 19.31/5.39
bool2Nat(False) → 0 19.31/5.39
bool2Nat(True) → S(0) 19.31/5.39
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.39
l9(z0, z1, z2, z3, z4, z5) → z0 19.31/5.39
l6(z0, z1, z2, z3, z4, z5) → 0 19.31/5.39
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False) 19.31/5.39
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False) 19.31/5.39
e7(z0, z1, z2, z3) → False 19.31/5.39
e6(z0, z1, z2, z3) → False 19.31/5.39
e5(z0, z1, z2, z3) → True 19.31/5.39
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.39
m5(z0, z1, z2, z3) → z2 19.31/5.39
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5) 19.31/5.39
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5) 19.31/5.39
l16(z0, z1, z2, z3, z4, z5) → z2 19.31/5.39
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.39
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.39
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1)) 19.31/5.39
gcd(z0, z1) → l1(z0, z1, 0, False, False, False) 19.31/5.39
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.39
e8(z0, z1, z2, z3) → z2 19.31/5.39
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.39
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.39
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.39
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.39
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.39
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.39
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.39
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.39
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.39
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.39
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.39
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.39
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.39
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.39
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.39
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.39
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.39
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.39
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.39
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.39
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.39
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.39
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.39
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.39
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

K tuples:

L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.39
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1))

Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

19.31/5.39

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.39
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.39
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1)) 19.31/5.39
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.39
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1)) 19.31/5.39
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.39
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.39
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.39
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.39
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1))

19.31/5.39

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.39
<(0, S(z0)) → True 19.31/5.39
<(z0, 0) → False 19.31/5.39
m2(S(0), z0, z1, True) → False 19.31/5.39
m2(S(S(z0)), z1, z2, True) → True 19.31/5.39
m2(0, z0, z1, True) → False 19.31/5.39
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.39
m3(S(0), z0, z1, z2) → False 19.31/5.39
m3(S(S(z0)), z1, z2, z3) → True 19.31/5.39
m3(0, z0, z1, z2) → False 19.31/5.39
l8(z0, z1, z2, True, z3, z4) → z0 19.31/5.39
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4) 19.31/5.39
l5(z0, z1, z2, z3, z4, True) → 0 19.31/5.39
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False) 19.31/5.39
help1(S(0)) → False 19.31/5.39
help1(S(S(z0))) → True 19.31/5.39
help1(0) → False 19.31/5.39
e4(z0, z1, z2, False) → False 19.31/5.39
e4(z0, z1, z2, True) → True 19.31/5.39
e2(z0, z1, z2, False) → False 19.31/5.39
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.39
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4) 19.31/5.39
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4) 19.31/5.39
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4) 19.31/5.39
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4) 19.31/5.39
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.39
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False) 19.31/5.39
l2(z0, z1, z2, z3, z4, True) → z2 19.31/5.39
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False) 19.31/5.39
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True) 19.31/5.39
bool2Nat(False) → 0 19.31/5.39
bool2Nat(True) → S(0) 19.31/5.39
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.39
l9(z0, z1, z2, z3, z4, z5) → z0 19.31/5.39
l6(z0, z1, z2, z3, z4, z5) → 0 19.31/5.39
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False) 19.31/5.39
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False) 19.31/5.39
e7(z0, z1, z2, z3) → False 19.31/5.39
e6(z0, z1, z2, z3) → False 19.31/5.39
e5(z0, z1, z2, z3) → True 19.31/5.39
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.39
m5(z0, z1, z2, z3) → z2 19.31/5.39
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5) 19.31/5.39
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5) 19.31/5.39
l16(z0, z1, z2, z3, z4, z5) → z2 19.31/5.39
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.39
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.39
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1)) 19.31/5.39
gcd(z0, z1) → l1(z0, z1, 0, False, False, False) 19.31/5.39
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.39
e8(z0, z1, z2, z3) → z2 19.31/5.39
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.39
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.39
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.39
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.39
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.39
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.39
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.39
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.39
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.39
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.39
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.39
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.39
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.39
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.39
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.39
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))

K tuples:

L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.39
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.39
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.39
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.39
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1)) 19.31/5.39
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.39
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.39
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.39
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.39
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.39
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1))

Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

19.31/5.39

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))

We considered the (Usable) Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.39
<(0, S(z0)) → True 19.31/5.39
<(z0, 0) → False 19.31/5.39
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.39
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.39
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.39
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.39
m5(z0, z1, z2, z3) → z2 19.31/5.39
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.39
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1)) 19.31/5.39
e2(z0, z1, z2, False) → False 19.31/5.39
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.39
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.39
e4(z0, z1, z2, False) → False 19.31/5.39
e4(z0, z1, z2, True) → True

And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.39
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.39
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.39
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.39
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.39
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.39
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.39
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.39
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.39
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.39
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.39
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.39
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 19.31/5.39

POL(0) = 0 19.31/5.39
POL(<(x₁, x₂)) = 0 19.31/5.39
POL(<'(x₁, x₂)) = 0 19.31/5.39
POL(E1(x₁, x₂, x₃, x₄)) = x₃ + x₄ 19.31/5.39
POL(E2(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(E3(x₁, x₂, x₃, x₄)) = 0 19.31/5.39
POL(EQUAL0(x₁, x₂)) = 0 19.31/5.39
POL(False) = 0 19.31/5.39
POL(GCD(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(L1(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₃ + x₄ + x₅ + x₆ 19.31/5.39
POL(L10(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₄ 19.31/5.39
POL(L11(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₄ 19.31/5.39
POL(L12(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ 19.31/5.39
POL(L13(x₁, x₂, x₃, x₄, x₅, x₆)) = x₂ + [4]x₅ 19.31/5.39
POL(L14(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₄ + x₆ 19.31/5.39
POL(L15(x₁, x₂, x₃, x₄, x₅, x₆)) = x₂ + x₅ + x₆ 19.31/5.39
POL(L2(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₃ + x₄ + x₆ 19.31/5.39
POL(L3(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₃ + x₄ + x₆ 19.31/5.39
POL(L4(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₃ + x₄ 19.31/5.39
POL(L5(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₄ + x₆ 19.31/5.39
POL(L7(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₆ 19.31/5.39
POL(L8(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ 19.31/5.39
POL(M1(x₁, x₂, x₃, x₄)) = x₁ + x₃ + x₄ 19.31/5.39
POL(M2(x₁, x₂, x₃, x₄)) = x₁ + x₃ + x₄ 19.31/5.39
POL(M4(x₁, x₂, x₃, x₄)) = x₁ + x₃ + x₄ 19.31/5.39
POL(MONUS(x₁, x₂)) = x₁ 19.31/5.39
POL(S(x₁)) = [1] + x₁ 19.31/5.39
POL(True) = [1] 19.31/5.39
POL(c(x₁)) = x₁ 19.31/5.39
POL(c1(x₁)) = x₁ 19.31/5.39
POL(c11(x₁)) = x₁ 19.31/5.39
POL(c13(x₁)) = x₁ 19.31/5.39
POL(c20(x₁)) = x₁ 19.31/5.39
POL(c21(x₁)) = x₁ 19.31/5.39
POL(c22(x₁)) = x₁ 19.31/5.39
POL(c23(x₁)) = x₁ 19.31/5.39
POL(c24(x₁)) = x₁ 19.31/5.39
POL(c25(x₁)) = x₁ 19.31/5.39
POL(c26(x₁)) = x₁ 19.31/5.39
POL(c28(x₁)) = x₁ 19.31/5.39
POL(c29(x₁)) = x₁ 19.31/5.39
POL(c32(x₁)) = x₁ 19.31/5.39
POL(c35(x₁)) = x₁ 19.31/5.39
POL(c36(x₁)) = x₁ 19.31/5.39
POL(c40(x₁)) = x₁ 19.31/5.39
POL(c42(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c43(x₁)) = x₁ 19.31/5.39
POL(c45(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c46(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c47(x₁, x₂)) = x₁ + x₂ 19.31/5.39
POL(c48(x₁)) = x₁ 19.31/5.39
POL(c49(x₁)) = x₁ 19.31/5.39
POL(c51(x₁)) = x₁ 19.31/5.39
POL(c6(x₁)) = x₁ 19.31/5.39
POL(e1(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + x₃ + x₄ 19.31/5.39
POL(e2(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ 19.31/5.39
POL(e3(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ + x₄ 19.31/5.39
POL(e4(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ 19.31/5.39
POL(equal0(x₁, x₂)) = 0 19.31/5.39
POL(m1(x₁, x₂, x₃, x₄)) = x₃ + x₄ 19.31/5.39
POL(m2(x₁, x₂, x₃, x₄)) = x₄ 19.31/5.39
POL(m4(x₁, x₂, x₃, x₄)) = x₄ 19.31/5.39
POL(m5(x₁, x₂, x₃, x₄)) = [4]x₃ + x₄ 19.31/5.39
POL(monus(x₁, x₂)) = 0

19.31/5.39

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 19.31/5.39
<(0, S(z0)) → True 19.31/5.39
<(z0, 0) → False 19.31/5.39
m2(S(0), z0, z1, True) → False 19.31/5.39
m2(S(S(z0)), z1, z2, True) → True 19.31/5.39
m2(0, z0, z1, True) → False 19.31/5.39
m2(z0, z1, z2, False) → m4(z0, z1, z2, False) 19.31/5.39
m3(S(0), z0, z1, z2) → False 19.31/5.39
m3(S(S(z0)), z1, z2, z3) → True 19.31/5.39
m3(0, z0, z1, z2) → False 19.31/5.39
l8(z0, z1, z2, True, z3, z4) → z0 19.31/5.39
l8(z0, z1, z2, False, z3, z4) → l10(z0, z1, z2, False, z3, z4) 19.31/5.39
l5(z0, z1, z2, z3, z4, True) → 0 19.31/5.39
l5(z0, z1, z2, z3, z4, False) → l7(z0, z1, z2, z3, z4, False) 19.31/5.39
help1(S(0)) → False 19.31/5.39
help1(S(S(z0))) → True 19.31/5.39
help1(0) → False 19.31/5.39
e4(z0, z1, z2, False) → False 19.31/5.39
e4(z0, z1, z2, True) → True 19.31/5.39
e2(z0, z1, z2, False) → False 19.31/5.39
e2(z0, z1, z2, True) → e3(z0, z1, z2, True) 19.31/5.39
l15(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(z1, 0), z3, False, z4) 19.31/5.39
l15(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(z1, S(0)), z3, True, z4) 19.31/5.39
l13(z0, z1, z2, z3, False, z4) → l16(z0, z1, gcd(0, z1), z3, False, z4) 19.31/5.39
l13(z0, z1, z2, z3, True, z4) → l16(z0, z1, gcd(S(0), z1), z3, True, z4) 19.31/5.39
m4(S(z0), S(z1), z2, z3) → m5(S(z0), S(z1), monus(z0, z1), z3) 19.31/5.39
l2(z0, z1, z2, z3, z4, False) → l3(z0, z1, z2, z3, z4, False) 19.31/5.39
l2(z0, z1, z2, z3, z4, True) → z2 19.31/5.39
l11(z0, z1, z2, z3, z4, False) → l14(z0, z1, z2, z3, z4, False) 19.31/5.39
l11(z0, z1, z2, z3, z4, True) → l12(z0, z1, z2, z3, z4, True) 19.31/5.39
bool2Nat(False) → 0 19.31/5.39
bool2Nat(True) → S(0) 19.31/5.39
m1(z0, z1, z2, z3) → m2(z0, z1, z2, False) 19.31/5.39
l9(z0, z1, z2, z3, z4, z5) → z0 19.31/5.39
l6(z0, z1, z2, z3, z4, z5) → 0 19.31/5.39
l4(z0, z1, z2, z3, z4, z5) → l5(z0, z1, z2, z3, z4, False) 19.31/5.39
l1(z0, z1, z2, z3, z4, z5) → l2(z0, z1, z2, z3, z4, False) 19.31/5.39
e7(z0, z1, z2, z3) → False 19.31/5.39
e6(z0, z1, z2, z3) → False 19.31/5.39
e5(z0, z1, z2, z3) → True 19.31/5.39
monus(z0, z1) → m1(z0, z1, False, False) 19.31/5.39
m5(z0, z1, z2, z3) → z2 19.31/5.39
l7(z0, z1, z2, z3, z4, z5) → l8(z0, z1, z2, equal0(z0, z1), z4, z5) 19.31/5.39
l3(z0, z1, z2, z3, z4, z5) → l4(z0, z1, 0, z3, z4, z5) 19.31/5.39
l16(z0, z1, z2, z3, z4, z5) → z2 19.31/5.39
l14(z0, z1, z2, z3, z4, z5) → l15(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.39
l12(z0, z1, z2, z3, z4, z5) → l13(z0, z1, z2, z3, monus(z0, z1), z5) 19.31/5.39
l10(z0, z1, z2, z3, z4, z5) → l11(z0, z1, z2, z3, z4, <(z0, z1)) 19.31/5.39
gcd(z0, z1) → l1(z0, z1, 0, False, False, False) 19.31/5.39
equal0(z0, z1) → e1(z0, z1, False, False) 19.31/5.39
e8(z0, z1, z2, z3) → z2 19.31/5.39
e3(z0, z1, z2, z3) → e4(z0, z1, z2, <(z1, z0)) 19.31/5.39
e1(z0, z1, z2, z3) → e2(z0, z1, z2, <(z0, z1))

Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 19.31/5.39
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.39
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.39
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.39
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.39
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.39
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.39
MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.39
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.39
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.39
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.39
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.39
L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1))

S tuples:

M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.39
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.39
MONUS(z0, z1) → c40(M1(z0, z1, False, False))

K tuples:

L13(z0, z1, z2, z3, True, z4) → c24(GCD(S(0), z1)) 19.31/5.39
L15(z0, z1, z2, z3, True, z4) → c22(GCD(z1, S(0))) 19.31/5.39
L5(z0, z1, z2, z3, z4, False) → c13(L7(z0, z1, z2, z3, z4, False)) 19.31/5.39
L2(z0, z1, z2, z3, z4, False) → c26(L3(z0, z1, z2, z3, z4, False)) 19.31/5.39
L15(z0, z1, z2, z3, False, z4) → c21(GCD(z1, 0)) 19.31/5.39
L13(z0, z1, z2, z3, False, z4) → c23(GCD(0, z1)) 19.31/5.39
L7(z0, z1, z2, z3, z4, z5) → c42(L8(z0, z1, z2, equal0(z0, z1), z4, z5), EQUAL0(z0, z1)) 19.31/5.39
L3(z0, z1, z2, z3, z4, z5) → c43(L4(z0, z1, 0, z3, z4, z5)) 19.31/5.39
GCD(z0, z1) → c48(L1(z0, z1, 0, False, False, False)) 19.31/5.39
EQUAL0(z0, z1) → c49(E1(z0, z1, False, False)) 19.31/5.39
E1(z0, z1, z2, z3) → c1(E2(z0, z1, z2, <(z0, z1))) 19.31/5.39
E1(z0, z1, z2, z3) → c1(<'(z0, z1)) 19.31/5.39
L8(z0, z1, z2, False, z3, z4) → c11(L10(z0, z1, z2, False, z3, z4)) 19.31/5.39
L4(z0, z1, z2, z3, z4, z5) → c35(L5(z0, z1, z2, z3, z4, False)) 19.31/5.39
L1(z0, z1, z2, z3, z4, z5) → c36(L2(z0, z1, z2, z3, z4, False)) 19.31/5.39
E2(z0, z1, z2, True) → c20(E3(z0, z1, z2, True)) 19.31/5.39
L10(z0, z1, z2, z3, z4, z5) → c47(L11(z0, z1, z2, z3, z4, <(z0, z1)), <'(z0, z1)) 19.31/5.39
E3(z0, z1, z2, z3) → c51(<'(z1, z0)) 19.31/5.39
L11(z0, z1, z2, z3, z4, False) → c28(L14(z0, z1, z2, z3, z4, False)) 19.31/5.39
L11(z0, z1, z2, z3, z4, True) → c29(L12(z0, z1, z2, z3, z4, True)) 19.31/5.39
L14(z0, z1, z2, z3, z4, z5) → c45(L15(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
L12(z0, z1, z2, z3, z4, z5) → c46(L13(z0, z1, z2, z3, monus(z0, z1), z5), MONUS(z0, z1)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))

Defined Rule Symbols:

m2, m3, l8, l5, help1, e4, e2, l15, l13, m4, l2, l11, bool2Nat, m1, l9, l6, l4, l1, e7, e6, e5, monus, m5, l7, l3, l16, l14, l12, l10, gcd, equal0, e8, e3, e1, <

Defined Pair Symbols:

<', M2, L8, L5, E2, L2, L11, M1, L4, L1, MONUS, L7, L3, L14, L12, L10, GCD, EQUAL0, L15, L13, M4, E3, E1

Compound Symbols:

c, c6, c11, c13, c20, c26, c28, c29, c32, c35, c36, c40, c42, c43, c45, c46, c47, c48, c49, c21, c22, c23, c24, c25, c51, c1

19.31/5.39

(17) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

MONUS(z0, z1) → c40(M1(z0, z1, False, False)) 19.31/5.39
M1(z0, z1, z2, z3) → c32(M2(z0, z1, z2, False)) 19.31/5.39
M2(z0, z1, z2, False) → c6(M4(z0, z1, z2, False)) 19.31/5.39
M4(S(z0), S(z1), z2, z3) → c25(MONUS(z0, z1))

Now S is empty

19.31/5.39

(18) BOUNDS(O(1), O(1))

19.31/5.39