(0) Obligation:

Clauses:

div(X1, 0, X2, X3) :- failure(a).
div(0, Y, 0, 0) :- no(zero(Y)).
div(X, Y, s(Z), R) :- ','(no(zero(X)), ','(no(zero(Y)), ','(minus(X, Y, U), ','(!, div(U, Y, Z, R))))).
div(X, Y, X4, X) :- ','(no(zero(X)), no(zero(Y))).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).
failure(b).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X5).

Query: div(g,g,a,a)

(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, 0) → U1(f36_in, 0, 0)
f2_in(z0, 0) → U2(f21_in(z0), z0, 0)
f2_in(0, z0) → f2_out1
f2_in(0, z0) → U3(f196_in(z0), 0, z0)
f2_in(z0, z1) → U4(f178_in(z0, z1), z0, z1)
U1(f36_out1, 0, 0) → f2_out1
U1(f36_out2, 0, 0) → f2_out1
U2(f21_out1, z0, 0) → f2_out1
U2(f21_out2, z0, 0) → f2_out1
U3(f196_out1, 0, z0) → f2_out1
U3(f196_out2, 0, z0) → f2_out1
U4(f178_out1, z0, z1) → f2_out1
U4(f178_out2, z0, z1) → f2_out1
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
f301_in(z0, z1) → U7(f2_in(z0, z1), z0, z1)
U7(f2_out1, z0, z1) → f301_out1
f241_in(z0, z1) → U8(f294_in(z0, z1), z0, z1)
U8(f294_out1(z0), z1, z2) → f241_out1
f243_in(z0, z1) → f243_out1
f294_in(z0, z1) → U9(f300_in(z0, z1), z0, z1)
U9(f300_out1(z0), z1, z2) → U10(f301_in(z0, z2), z1, z2, z0)
U10(f301_out1, z0, z1, z2) → f294_out1(z2)
f21_in(z0) → U11(f83_in(z0), f84_in(z0), z0)
U11(f83_out1, z0, z1) → f21_out1
U11(z0, f84_out1, z1) → f21_out2
f36_inU12(f39_in, f40_in)
U12(f39_out1, z0) → f36_out1
U12(z0, f40_out1) → f36_out2
f178_in(z0, z1) → U13(f241_in(z0, z1), f243_in(z0, z1), z0, z1)
U13(f241_out1, z0, z1, z2) → f178_out1
U13(z0, f243_out1, z1, z2) → f178_out2
f196_in(z0) → U14(f199_in(z0), f200_in(z0), z0)
U14(f199_out1, z0, z1) → f196_out1
U14(z0, f200_out1, z1) → f196_out2
Tuples:

F2_IN(0, 0) → c(U1'(f36_in, 0, 0), F36_IN)
F2_IN(z0, 0) → c1(U2'(f21_in(z0), z0, 0), F21_IN(z0))
F2_IN(0, z0) → c3(U3'(f196_in(z0), 0, z0), F196_IN(z0))
F2_IN(z0, z1) → c4(U4'(f178_in(z0, z1), z0, z1), F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(U5'(f308_in(z0, z1), s(z0), s(z1)), F308_IN(z0, z1))
F300_IN(s(z0), s(z1)) → c16(U6'(f308_in(z0, z1), s(z0), s(z1)), F308_IN(z0, z1))
F301_IN(z0, z1) → c18(U7'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F241_IN(z0, z1) → c20(U8'(f294_in(z0, z1), z0, z1), F294_IN(z0, z1))
F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(U10'(f301_in(z0, z2), z1, z2, z0), F301_IN(z0, z2))
F21_IN(z0) → c26(U11'(f83_in(z0), f84_in(z0), z0))
F36_INc29(U12'(f39_in, f40_in))
F178_IN(z0, z1) → c32(U13'(f241_in(z0, z1), f243_in(z0, z1), z0, z1), F241_IN(z0, z1), F243_IN(z0, z1))
F196_IN(z0) → c35(U14'(f199_in(z0), f200_in(z0), z0))
S tuples:

F2_IN(0, 0) → c(U1'(f36_in, 0, 0), F36_IN)
F2_IN(z0, 0) → c1(U2'(f21_in(z0), z0, 0), F21_IN(z0))
F2_IN(0, z0) → c3(U3'(f196_in(z0), 0, z0), F196_IN(z0))
F2_IN(z0, z1) → c4(U4'(f178_in(z0, z1), z0, z1), F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(U5'(f308_in(z0, z1), s(z0), s(z1)), F308_IN(z0, z1))
F300_IN(s(z0), s(z1)) → c16(U6'(f308_in(z0, z1), s(z0), s(z1)), F308_IN(z0, z1))
F301_IN(z0, z1) → c18(U7'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F241_IN(z0, z1) → c20(U8'(f294_in(z0, z1), z0, z1), F294_IN(z0, z1))
F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(U10'(f301_in(z0, z2), z1, z2, z0), F301_IN(z0, z2))
F21_IN(z0) → c26(U11'(f83_in(z0), f84_in(z0), z0))
F36_INc29(U12'(f39_in, f40_in))
F178_IN(z0, z1) → c32(U13'(f241_in(z0, z1), f243_in(z0, z1), z0, z1), F241_IN(z0, z1), F243_IN(z0, z1))
F196_IN(z0) → c35(U14'(f199_in(z0), f200_in(z0), z0))
K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, f308_in, U5, f300_in, U6, f301_in, U7, f241_in, U8, f243_in, f294_in, U9, U10, f21_in, U11, f36_in, U12, f178_in, U13, f196_in, U14

Defined Pair Symbols:

F2_IN, F308_IN, F300_IN, F301_IN, F241_IN, F294_IN, U9', F21_IN, F36_IN, F178_IN, F196_IN

Compound Symbols:

c, c1, c3, c4, c14, c16, c18, c20, c23, c24, c26, c29, c32, c35

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

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, 0) → U1(f36_in, 0, 0)
f2_in(z0, 0) → U2(f21_in(z0), z0, 0)
f2_in(0, z0) → f2_out1
f2_in(0, z0) → U3(f196_in(z0), 0, z0)
f2_in(z0, z1) → U4(f178_in(z0, z1), z0, z1)
U1(f36_out1, 0, 0) → f2_out1
U1(f36_out2, 0, 0) → f2_out1
U2(f21_out1, z0, 0) → f2_out1
U2(f21_out2, z0, 0) → f2_out1
U3(f196_out1, 0, z0) → f2_out1
U3(f196_out2, 0, z0) → f2_out1
U4(f178_out1, z0, z1) → f2_out1
U4(f178_out2, z0, z1) → f2_out1
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
f301_in(z0, z1) → U7(f2_in(z0, z1), z0, z1)
U7(f2_out1, z0, z1) → f301_out1
f241_in(z0, z1) → U8(f294_in(z0, z1), z0, z1)
U8(f294_out1(z0), z1, z2) → f241_out1
f243_in(z0, z1) → f243_out1
f294_in(z0, z1) → U9(f300_in(z0, z1), z0, z1)
U9(f300_out1(z0), z1, z2) → U10(f301_in(z0, z2), z1, z2, z0)
U10(f301_out1, z0, z1, z2) → f294_out1(z2)
f21_in(z0) → U11(f83_in(z0), f84_in(z0), z0)
U11(f83_out1, z0, z1) → f21_out1
U11(z0, f84_out1, z1) → f21_out2
f36_inU12(f39_in, f40_in)
U12(f39_out1, z0) → f36_out1
U12(z0, f40_out1) → f36_out2
f178_in(z0, z1) → U13(f241_in(z0, z1), f243_in(z0, z1), z0, z1)
U13(f241_out1, z0, z1, z2) → f178_out1
U13(z0, f243_out1, z1, z2) → f178_out2
f196_in(z0) → U14(f199_in(z0), f200_in(z0), z0)
U14(f199_out1, z0, z1) → f196_out1
U14(z0, f200_out1, z1) → f196_out2
Tuples:

F2_IN(z0, z1) → c4(U4'(f178_in(z0, z1), z0, z1), F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(U5'(f308_in(z0, z1), s(z0), s(z1)), F308_IN(z0, z1))
F301_IN(z0, z1) → c18(U7'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F241_IN(z0, z1) → c20(U8'(f294_in(z0, z1), z0, z1), F294_IN(z0, z1))
F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(U10'(f301_in(z0, z2), z1, z2, z0), F301_IN(z0, z2))
F21_IN(z0) → c26(U11'(f83_in(z0), f84_in(z0), z0))
F36_INc29(U12'(f39_in, f40_in))
F178_IN(z0, z1) → c32(U13'(f241_in(z0, z1), f243_in(z0, z1), z0, z1), F241_IN(z0, z1), F243_IN(z0, z1))
F196_IN(z0) → c35(U14'(f199_in(z0), f200_in(z0), z0))
F2_IN(0, 0) → c2(U1'(f36_in, 0, 0))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(U2'(f21_in(z0), z0, 0))
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(U3'(f196_in(z0), 0, z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(U6'(f308_in(z0, z1), s(z0), s(z1)))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
S tuples:

F2_IN(z0, z1) → c4(U4'(f178_in(z0, z1), z0, z1), F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(U5'(f308_in(z0, z1), s(z0), s(z1)), F308_IN(z0, z1))
F301_IN(z0, z1) → c18(U7'(f2_in(z0, z1), z0, z1), F2_IN(z0, z1))
F241_IN(z0, z1) → c20(U8'(f294_in(z0, z1), z0, z1), F294_IN(z0, z1))
F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(U10'(f301_in(z0, z2), z1, z2, z0), F301_IN(z0, z2))
F21_IN(z0) → c26(U11'(f83_in(z0), f84_in(z0), z0))
F36_INc29(U12'(f39_in, f40_in))
F178_IN(z0, z1) → c32(U13'(f241_in(z0, z1), f243_in(z0, z1), z0, z1), F241_IN(z0, z1), F243_IN(z0, z1))
F196_IN(z0) → c35(U14'(f199_in(z0), f200_in(z0), z0))
F2_IN(0, 0) → c2(U1'(f36_in, 0, 0))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(U2'(f21_in(z0), z0, 0))
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(U3'(f196_in(z0), 0, z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(U6'(f308_in(z0, z1), s(z0), s(z1)))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, f308_in, U5, f300_in, U6, f301_in, U7, f241_in, U8, f243_in, f294_in, U9, U10, f21_in, U11, f36_in, U12, f178_in, U13, f196_in, U14

Defined Pair Symbols:

F2_IN, F308_IN, F301_IN, F241_IN, F294_IN, U9', F21_IN, F36_IN, F178_IN, F196_IN, F300_IN

Compound Symbols:

c4, c14, c18, c20, c23, c24, c26, c29, c32, c35, c2

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

Removed 14 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, 0) → U1(f36_in, 0, 0)
f2_in(z0, 0) → U2(f21_in(z0), z0, 0)
f2_in(0, z0) → f2_out1
f2_in(0, z0) → U3(f196_in(z0), 0, z0)
f2_in(z0, z1) → U4(f178_in(z0, z1), z0, z1)
U1(f36_out1, 0, 0) → f2_out1
U1(f36_out2, 0, 0) → f2_out1
U2(f21_out1, z0, 0) → f2_out1
U2(f21_out2, z0, 0) → f2_out1
U3(f196_out1, 0, z0) → f2_out1
U3(f196_out2, 0, z0) → f2_out1
U4(f178_out1, z0, z1) → f2_out1
U4(f178_out2, z0, z1) → f2_out1
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
f301_in(z0, z1) → U7(f2_in(z0, z1), z0, z1)
U7(f2_out1, z0, z1) → f301_out1
f241_in(z0, z1) → U8(f294_in(z0, z1), z0, z1)
U8(f294_out1(z0), z1, z2) → f241_out1
f243_in(z0, z1) → f243_out1
f294_in(z0, z1) → U9(f300_in(z0, z1), z0, z1)
U9(f300_out1(z0), z1, z2) → U10(f301_in(z0, z2), z1, z2, z0)
U10(f301_out1, z0, z1, z2) → f294_out1(z2)
f21_in(z0) → U11(f83_in(z0), f84_in(z0), z0)
U11(f83_out1, z0, z1) → f21_out1
U11(z0, f84_out1, z1) → f21_out2
f36_inU12(f39_in, f40_in)
U12(f39_out1, z0) → f36_out1
U12(z0, f40_out1) → f36_out2
f178_in(z0, z1) → U13(f241_in(z0, z1), f243_in(z0, z1), z0, z1)
U13(f241_out1, z0, z1, z2) → f178_out1
U13(z0, f243_out1, z1, z2) → f178_out2
f196_in(z0) → U14(f199_in(z0), f200_in(z0), z0)
U14(f199_out1, z0, z1) → f196_out1
U14(z0, f200_out1, z1) → f196_out2
Tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
S tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, f308_in, U5, f300_in, U6, f301_in, U7, f241_in, U8, f243_in, f294_in, U9, U10, f21_in, U11, f36_in, U12, f178_in, U13, f196_in, U14

Defined Pair Symbols:

F294_IN, F2_IN, F300_IN, F308_IN, F301_IN, F241_IN, U9', F21_IN, F36_IN, F178_IN, F196_IN

Compound Symbols:

c23, c2, c4, c14, c18, c20, c24, c26, c29, c32, c35, c2

(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.

F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
We considered the (Usable) Rules:

f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
And the Tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [2]   
POL(F178_IN(x1, x2)) = x2   
POL(F196_IN(x1)) = x1   
POL(F21_IN(x1)) = 0   
POL(F241_IN(x1, x2)) = x2   
POL(F294_IN(x1, x2)) = x2   
POL(F2_IN(x1, x2)) = x2   
POL(F300_IN(x1, x2)) = 0   
POL(F301_IN(x1, x2)) = x2   
POL(F308_IN(x1, x2)) = 0   
POL(F36_IN) = 0   
POL(U5(x1, x2, x3)) = 0   
POL(U6(x1, x2, x3)) = 0   
POL(U9'(x1, x2, x3)) = x3   
POL(c14(x1)) = x1   
POL(c18(x1)) = x1   
POL(c2) = 0   
POL(c2(x1)) = x1   
POL(c20(x1)) = x1   
POL(c23(x1, x2)) = x1 + x2   
POL(c24(x1)) = x1   
POL(c26) = 0   
POL(c29) = 0   
POL(c32(x1)) = x1   
POL(c35) = 0   
POL(c4(x1)) = x1   
POL(f300_in(x1, x2)) = 0   
POL(f300_out1(x1)) = 0   
POL(f308_in(x1, x2)) = 0   
POL(f308_out1(x1)) = 0   
POL(s(x1)) = 0   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, 0) → U1(f36_in, 0, 0)
f2_in(z0, 0) → U2(f21_in(z0), z0, 0)
f2_in(0, z0) → f2_out1
f2_in(0, z0) → U3(f196_in(z0), 0, z0)
f2_in(z0, z1) → U4(f178_in(z0, z1), z0, z1)
U1(f36_out1, 0, 0) → f2_out1
U1(f36_out2, 0, 0) → f2_out1
U2(f21_out1, z0, 0) → f2_out1
U2(f21_out2, z0, 0) → f2_out1
U3(f196_out1, 0, z0) → f2_out1
U3(f196_out2, 0, z0) → f2_out1
U4(f178_out1, z0, z1) → f2_out1
U4(f178_out2, z0, z1) → f2_out1
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
f301_in(z0, z1) → U7(f2_in(z0, z1), z0, z1)
U7(f2_out1, z0, z1) → f301_out1
f241_in(z0, z1) → U8(f294_in(z0, z1), z0, z1)
U8(f294_out1(z0), z1, z2) → f241_out1
f243_in(z0, z1) → f243_out1
f294_in(z0, z1) → U9(f300_in(z0, z1), z0, z1)
U9(f300_out1(z0), z1, z2) → U10(f301_in(z0, z2), z1, z2, z0)
U10(f301_out1, z0, z1, z2) → f294_out1(z2)
f21_in(z0) → U11(f83_in(z0), f84_in(z0), z0)
U11(f83_out1, z0, z1) → f21_out1
U11(z0, f84_out1, z1) → f21_out2
f36_inU12(f39_in, f40_in)
U12(f39_out1, z0) → f36_out1
U12(z0, f40_out1) → f36_out2
f178_in(z0, z1) → U13(f241_in(z0, z1), f243_in(z0, z1), z0, z1)
U13(f241_out1, z0, z1, z2) → f178_out1
U13(z0, f243_out1, z1, z2) → f178_out2
f196_in(z0) → U14(f199_in(z0), f200_in(z0), z0)
U14(f199_out1, z0, z1) → f196_out1
U14(z0, f200_out1, z1) → f196_out2
Tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
S tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
K tuples:

F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, f308_in, U5, f300_in, U6, f301_in, U7, f241_in, U8, f243_in, f294_in, U9, U10, f21_in, U11, f36_in, U12, f178_in, U13, f196_in, U14

Defined Pair Symbols:

F294_IN, F2_IN, F300_IN, F308_IN, F301_IN, F241_IN, U9', F21_IN, F36_IN, F178_IN, F196_IN

Compound Symbols:

c23, c2, c4, c14, c18, c20, c24, c26, c29, c32, c35, c2

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F21_IN(z0) → c26
F36_INc29

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, 0) → U1(f36_in, 0, 0)
f2_in(z0, 0) → U2(f21_in(z0), z0, 0)
f2_in(0, z0) → f2_out1
f2_in(0, z0) → U3(f196_in(z0), 0, z0)
f2_in(z0, z1) → U4(f178_in(z0, z1), z0, z1)
U1(f36_out1, 0, 0) → f2_out1
U1(f36_out2, 0, 0) → f2_out1
U2(f21_out1, z0, 0) → f2_out1
U2(f21_out2, z0, 0) → f2_out1
U3(f196_out1, 0, z0) → f2_out1
U3(f196_out2, 0, z0) → f2_out1
U4(f178_out1, z0, z1) → f2_out1
U4(f178_out2, z0, z1) → f2_out1
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
f301_in(z0, z1) → U7(f2_in(z0, z1), z0, z1)
U7(f2_out1, z0, z1) → f301_out1
f241_in(z0, z1) → U8(f294_in(z0, z1), z0, z1)
U8(f294_out1(z0), z1, z2) → f241_out1
f243_in(z0, z1) → f243_out1
f294_in(z0, z1) → U9(f300_in(z0, z1), z0, z1)
U9(f300_out1(z0), z1, z2) → U10(f301_in(z0, z2), z1, z2, z0)
U10(f301_out1, z0, z1, z2) → f294_out1(z2)
f21_in(z0) → U11(f83_in(z0), f84_in(z0), z0)
U11(f83_out1, z0, z1) → f21_out1
U11(z0, f84_out1, z1) → f21_out2
f36_inU12(f39_in, f40_in)
U12(f39_out1, z0) → f36_out1
U12(z0, f40_out1) → f36_out2
f178_in(z0, z1) → U13(f241_in(z0, z1), f243_in(z0, z1), z0, z1)
U13(f241_out1, z0, z1, z2) → f178_out1
U13(z0, f243_out1, z1, z2) → f178_out2
f196_in(z0) → U14(f199_in(z0), f200_in(z0), z0)
U14(f199_out1, z0, z1) → f196_out1
U14(z0, f200_out1, z1) → f196_out2
Tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
S tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
K tuples:

F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F21_IN(z0) → c26
F36_INc29
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, f308_in, U5, f300_in, U6, f301_in, U7, f241_in, U8, f243_in, f294_in, U9, U10, f21_in, U11, f36_in, U12, f178_in, U13, f196_in, U14

Defined Pair Symbols:

F294_IN, F2_IN, F300_IN, F308_IN, F301_IN, F241_IN, U9', F21_IN, F36_IN, F178_IN, F196_IN

Compound Symbols:

c23, c2, c4, c14, c18, c20, c24, c26, c29, c32, c35, c2

(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.

F196_IN(z0) → c35
F2_IN(0, z0) → c2
We considered the (Usable) Rules:

f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
And the Tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(F178_IN(x1, x2)) = [1]   
POL(F196_IN(x1)) = [1]   
POL(F21_IN(x1)) = [1]   
POL(F241_IN(x1, x2)) = [1]   
POL(F294_IN(x1, x2)) = [1]   
POL(F2_IN(x1, x2)) = [1]   
POL(F300_IN(x1, x2)) = 0   
POL(F301_IN(x1, x2)) = [1]   
POL(F308_IN(x1, x2)) = 0   
POL(F36_IN) = [1]   
POL(U5(x1, x2, x3)) = 0   
POL(U6(x1, x2, x3)) = 0   
POL(U9'(x1, x2, x3)) = [1]   
POL(c14(x1)) = x1   
POL(c18(x1)) = x1   
POL(c2) = 0   
POL(c2(x1)) = x1   
POL(c20(x1)) = x1   
POL(c23(x1, x2)) = x1 + x2   
POL(c24(x1)) = x1   
POL(c26) = 0   
POL(c29) = 0   
POL(c32(x1)) = x1   
POL(c35) = 0   
POL(c4(x1)) = x1   
POL(f300_in(x1, x2)) = 0   
POL(f300_out1(x1)) = 0   
POL(f308_in(x1, x2)) = 0   
POL(f308_out1(x1)) = 0   
POL(s(x1)) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, 0) → U1(f36_in, 0, 0)
f2_in(z0, 0) → U2(f21_in(z0), z0, 0)
f2_in(0, z0) → f2_out1
f2_in(0, z0) → U3(f196_in(z0), 0, z0)
f2_in(z0, z1) → U4(f178_in(z0, z1), z0, z1)
U1(f36_out1, 0, 0) → f2_out1
U1(f36_out2, 0, 0) → f2_out1
U2(f21_out1, z0, 0) → f2_out1
U2(f21_out2, z0, 0) → f2_out1
U3(f196_out1, 0, z0) → f2_out1
U3(f196_out2, 0, z0) → f2_out1
U4(f178_out1, z0, z1) → f2_out1
U4(f178_out2, z0, z1) → f2_out1
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
f301_in(z0, z1) → U7(f2_in(z0, z1), z0, z1)
U7(f2_out1, z0, z1) → f301_out1
f241_in(z0, z1) → U8(f294_in(z0, z1), z0, z1)
U8(f294_out1(z0), z1, z2) → f241_out1
f243_in(z0, z1) → f243_out1
f294_in(z0, z1) → U9(f300_in(z0, z1), z0, z1)
U9(f300_out1(z0), z1, z2) → U10(f301_in(z0, z2), z1, z2, z0)
U10(f301_out1, z0, z1, z2) → f294_out1(z2)
f21_in(z0) → U11(f83_in(z0), f84_in(z0), z0)
U11(f83_out1, z0, z1) → f21_out1
U11(z0, f84_out1, z1) → f21_out2
f36_inU12(f39_in, f40_in)
U12(f39_out1, z0) → f36_out1
U12(z0, f40_out1) → f36_out2
f178_in(z0, z1) → U13(f241_in(z0, z1), f243_in(z0, z1), z0, z1)
U13(f241_out1, z0, z1, z2) → f178_out1
U13(z0, f243_out1, z1, z2) → f178_out2
f196_in(z0) → U14(f199_in(z0), f200_in(z0), z0)
U14(f199_out1, z0, z1) → f196_out1
U14(z0, f200_out1, z1) → f196_out2
Tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
S tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F300_IN(s(z0), s(z1)) → c2
K tuples:

F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F21_IN(z0) → c26
F36_INc29
F196_IN(z0) → c35
F2_IN(0, z0) → c2
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, f308_in, U5, f300_in, U6, f301_in, U7, f241_in, U8, f243_in, f294_in, U9, U10, f21_in, U11, f36_in, U12, f178_in, U13, f196_in, U14

Defined Pair Symbols:

F294_IN, F2_IN, F300_IN, F308_IN, F301_IN, F241_IN, U9', F21_IN, F36_IN, F178_IN, F196_IN

Compound Symbols:

c23, c2, c4, c14, c18, c20, c24, c26, c29, c32, c35, c2

(13) 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.

F2_IN(0, z0) → c2(F196_IN(z0))
We considered the (Usable) Rules:

f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
And the Tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(F178_IN(x1, x2)) = [1]   
POL(F196_IN(x1)) = 0   
POL(F21_IN(x1)) = 0   
POL(F241_IN(x1, x2)) = [1]   
POL(F294_IN(x1, x2)) = [1]   
POL(F2_IN(x1, x2)) = [1]   
POL(F300_IN(x1, x2)) = 0   
POL(F301_IN(x1, x2)) = [1]   
POL(F308_IN(x1, x2)) = 0   
POL(F36_IN) = 0   
POL(U5(x1, x2, x3)) = 0   
POL(U6(x1, x2, x3)) = 0   
POL(U9'(x1, x2, x3)) = [1]   
POL(c14(x1)) = x1   
POL(c18(x1)) = x1   
POL(c2) = 0   
POL(c2(x1)) = x1   
POL(c20(x1)) = x1   
POL(c23(x1, x2)) = x1 + x2   
POL(c24(x1)) = x1   
POL(c26) = 0   
POL(c29) = 0   
POL(c32(x1)) = x1   
POL(c35) = 0   
POL(c4(x1)) = x1   
POL(f300_in(x1, x2)) = 0   
POL(f300_out1(x1)) = 0   
POL(f308_in(x1, x2)) = 0   
POL(f308_out1(x1)) = 0   
POL(s(x1)) = 0   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, 0) → U1(f36_in, 0, 0)
f2_in(z0, 0) → U2(f21_in(z0), z0, 0)
f2_in(0, z0) → f2_out1
f2_in(0, z0) → U3(f196_in(z0), 0, z0)
f2_in(z0, z1) → U4(f178_in(z0, z1), z0, z1)
U1(f36_out1, 0, 0) → f2_out1
U1(f36_out2, 0, 0) → f2_out1
U2(f21_out1, z0, 0) → f2_out1
U2(f21_out2, z0, 0) → f2_out1
U3(f196_out1, 0, z0) → f2_out1
U3(f196_out2, 0, z0) → f2_out1
U4(f178_out1, z0, z1) → f2_out1
U4(f178_out2, z0, z1) → f2_out1
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
f301_in(z0, z1) → U7(f2_in(z0, z1), z0, z1)
U7(f2_out1, z0, z1) → f301_out1
f241_in(z0, z1) → U8(f294_in(z0, z1), z0, z1)
U8(f294_out1(z0), z1, z2) → f241_out1
f243_in(z0, z1) → f243_out1
f294_in(z0, z1) → U9(f300_in(z0, z1), z0, z1)
U9(f300_out1(z0), z1, z2) → U10(f301_in(z0, z2), z1, z2, z0)
U10(f301_out1, z0, z1, z2) → f294_out1(z2)
f21_in(z0) → U11(f83_in(z0), f84_in(z0), z0)
U11(f83_out1, z0, z1) → f21_out1
U11(z0, f84_out1, z1) → f21_out2
f36_inU12(f39_in, f40_in)
U12(f39_out1, z0) → f36_out1
U12(z0, f40_out1) → f36_out2
f178_in(z0, z1) → U13(f241_in(z0, z1), f243_in(z0, z1), z0, z1)
U13(f241_out1, z0, z1, z2) → f178_out1
U13(z0, f243_out1, z1, z2) → f178_out2
f196_in(z0) → U14(f199_in(z0), f200_in(z0), z0)
U14(f199_out1, z0, z1) → f196_out1
U14(z0, f200_out1, z1) → f196_out2
Tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
S tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F300_IN(s(z0), s(z1)) → c2
K tuples:

F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F21_IN(z0) → c26
F36_INc29
F196_IN(z0) → c35
F2_IN(0, z0) → c2
F2_IN(0, z0) → c2(F196_IN(z0))
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, f308_in, U5, f300_in, U6, f301_in, U7, f241_in, U8, f243_in, f294_in, U9, U10, f21_in, U11, f36_in, U12, f178_in, U13, f196_in, U14

Defined Pair Symbols:

F294_IN, F2_IN, F300_IN, F308_IN, F301_IN, F241_IN, U9', F21_IN, F36_IN, F178_IN, F196_IN

Compound Symbols:

c23, c2, c4, c14, c18, c20, c24, c26, c29, c32, c35, c2

(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.

F301_IN(z0, z1) → c18(F2_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
We considered the (Usable) Rules:

f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
And the Tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [1]   
POL(F178_IN(x1, x2)) = [2] + [2]x1   
POL(F196_IN(x1)) = [1]   
POL(F21_IN(x1)) = [2] + x1   
POL(F241_IN(x1, x2)) = [2]x1   
POL(F294_IN(x1, x2)) = [2]x1   
POL(F2_IN(x1, x2)) = [2] + [2]x1   
POL(F300_IN(x1, x2)) = 0   
POL(F301_IN(x1, x2)) = [3] + [2]x1   
POL(F308_IN(x1, x2)) = 0   
POL(F36_IN) = [3]   
POL(U5(x1, x2, x3)) = x1   
POL(U6(x1, x2, x3)) = [2] + x1   
POL(U9'(x1, x2, x3)) = [2]x1   
POL(c14(x1)) = x1   
POL(c18(x1)) = x1   
POL(c2) = 0   
POL(c2(x1)) = x1   
POL(c20(x1)) = x1   
POL(c23(x1, x2)) = x1 + x2   
POL(c24(x1)) = x1   
POL(c26) = 0   
POL(c29) = 0   
POL(c32(x1)) = x1   
POL(c35) = 0   
POL(c4(x1)) = x1   
POL(f300_in(x1, x2)) = x1   
POL(f300_out1(x1)) = [2] + x1   
POL(f308_in(x1, x2)) = x1   
POL(f308_out1(x1)) = x1   
POL(s(x1)) = [2] + x1   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, 0) → U1(f36_in, 0, 0)
f2_in(z0, 0) → U2(f21_in(z0), z0, 0)
f2_in(0, z0) → f2_out1
f2_in(0, z0) → U3(f196_in(z0), 0, z0)
f2_in(z0, z1) → U4(f178_in(z0, z1), z0, z1)
U1(f36_out1, 0, 0) → f2_out1
U1(f36_out2, 0, 0) → f2_out1
U2(f21_out1, z0, 0) → f2_out1
U2(f21_out2, z0, 0) → f2_out1
U3(f196_out1, 0, z0) → f2_out1
U3(f196_out2, 0, z0) → f2_out1
U4(f178_out1, z0, z1) → f2_out1
U4(f178_out2, z0, z1) → f2_out1
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
f301_in(z0, z1) → U7(f2_in(z0, z1), z0, z1)
U7(f2_out1, z0, z1) → f301_out1
f241_in(z0, z1) → U8(f294_in(z0, z1), z0, z1)
U8(f294_out1(z0), z1, z2) → f241_out1
f243_in(z0, z1) → f243_out1
f294_in(z0, z1) → U9(f300_in(z0, z1), z0, z1)
U9(f300_out1(z0), z1, z2) → U10(f301_in(z0, z2), z1, z2, z0)
U10(f301_out1, z0, z1, z2) → f294_out1(z2)
f21_in(z0) → U11(f83_in(z0), f84_in(z0), z0)
U11(f83_out1, z0, z1) → f21_out1
U11(z0, f84_out1, z1) → f21_out2
f36_inU12(f39_in, f40_in)
U12(f39_out1, z0) → f36_out1
U12(z0, f40_out1) → f36_out2
f178_in(z0, z1) → U13(f241_in(z0, z1), f243_in(z0, z1), z0, z1)
U13(f241_out1, z0, z1, z2) → f178_out1
U13(z0, f243_out1, z1, z2) → f178_out2
f196_in(z0) → U14(f199_in(z0), f200_in(z0), z0)
U14(f199_out1, z0, z1) → f196_out1
U14(z0, f200_out1, z1) → f196_out2
Tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
S tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
F300_IN(s(z0), s(z1)) → c2
K tuples:

F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F21_IN(z0) → c26
F36_INc29
F196_IN(z0) → c35
F2_IN(0, z0) → c2
F2_IN(0, z0) → c2(F196_IN(z0))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, f308_in, U5, f300_in, U6, f301_in, U7, f241_in, U8, f243_in, f294_in, U9, U10, f21_in, U11, f36_in, U12, f178_in, U13, f196_in, U14

Defined Pair Symbols:

F294_IN, F2_IN, F300_IN, F308_IN, F301_IN, F241_IN, U9', F21_IN, F36_IN, F178_IN, F196_IN

Compound Symbols:

c23, c2, c4, c14, c18, c20, c24, c26, c29, c32, c35, c2

(17) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F300_IN(s(z0), s(z1)) → c2

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, 0) → U1(f36_in, 0, 0)
f2_in(z0, 0) → U2(f21_in(z0), z0, 0)
f2_in(0, z0) → f2_out1
f2_in(0, z0) → U3(f196_in(z0), 0, z0)
f2_in(z0, z1) → U4(f178_in(z0, z1), z0, z1)
U1(f36_out1, 0, 0) → f2_out1
U1(f36_out2, 0, 0) → f2_out1
U2(f21_out1, z0, 0) → f2_out1
U2(f21_out2, z0, 0) → f2_out1
U3(f196_out1, 0, z0) → f2_out1
U3(f196_out2, 0, z0) → f2_out1
U4(f178_out1, z0, z1) → f2_out1
U4(f178_out2, z0, z1) → f2_out1
f308_in(z0, 0) → f308_out1(z0)
f308_in(s(z0), s(z1)) → U5(f308_in(z0, z1), s(z0), s(z1))
U5(f308_out1(z0), s(z1), s(z2)) → f308_out1(z0)
f300_in(s(z0), s(z1)) → U6(f308_in(z0, z1), s(z0), s(z1))
U6(f308_out1(z0), s(z1), s(z2)) → f300_out1(z0)
f301_in(z0, z1) → U7(f2_in(z0, z1), z0, z1)
U7(f2_out1, z0, z1) → f301_out1
f241_in(z0, z1) → U8(f294_in(z0, z1), z0, z1)
U8(f294_out1(z0), z1, z2) → f241_out1
f243_in(z0, z1) → f243_out1
f294_in(z0, z1) → U9(f300_in(z0, z1), z0, z1)
U9(f300_out1(z0), z1, z2) → U10(f301_in(z0, z2), z1, z2, z0)
U10(f301_out1, z0, z1, z2) → f294_out1(z2)
f21_in(z0) → U11(f83_in(z0), f84_in(z0), z0)
U11(f83_out1, z0, z1) → f21_out1
U11(z0, f84_out1, z1) → f21_out2
f36_inU12(f39_in, f40_in)
U12(f39_out1, z0) → f36_out1
U12(z0, f40_out1) → f36_out2
f178_in(z0, z1) → U13(f241_in(z0, z1), f243_in(z0, z1), z0, z1)
U13(f241_out1, z0, z1, z2) → f178_out1
U13(z0, f243_out1, z1, z2) → f178_out2
f196_in(z0) → U14(f199_in(z0), f200_in(z0), z0)
U14(f199_out1, z0, z1) → f196_out1
U14(z0, f200_out1, z1) → f196_out2
Tuples:

F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, z0) → c2(F196_IN(z0))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F21_IN(z0) → c26
F36_INc29
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F196_IN(z0) → c35
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F2_IN(0, z0) → c2
F300_IN(s(z0), s(z1)) → c2
S tuples:

F308_IN(s(z0), s(z1)) → c14(F308_IN(z0, z1))
K tuples:

F2_IN(0, 0) → c2(F36_IN)
F2_IN(z0, 0) → c2(F21_IN(z0))
F2_IN(0, 0) → c2
F2_IN(z0, 0) → c2
F21_IN(z0) → c26
F36_INc29
F196_IN(z0) → c35
F2_IN(0, z0) → c2
F2_IN(0, z0) → c2(F196_IN(z0))
F301_IN(z0, z1) → c18(F2_IN(z0, z1))
U9'(f300_out1(z0), z1, z2) → c24(F301_IN(z0, z2))
F178_IN(z0, z1) → c32(F241_IN(z0, z1))
F2_IN(z0, z1) → c4(F178_IN(z0, z1))
F241_IN(z0, z1) → c20(F294_IN(z0, z1))
F294_IN(z0, z1) → c23(U9'(f300_in(z0, z1), z0, z1), F300_IN(z0, z1))
F300_IN(s(z0), s(z1)) → c2(F308_IN(z0, z1))
F300_IN(s(z0), s(z1)) → c2
Defined Rule Symbols:

f2_in, U1, U2, U3, U4, f308_in, U5, f300_in, U6, f301_in, U7, f241_in, U8, f243_in, f294_in, U9, U10, f21_in, U11, f36_in, U12, f178_in, U13, f196_in, U14

Defined Pair Symbols:

F294_IN, F2_IN, F300_IN, F308_IN, F301_IN, F241_IN, U9', F21_IN, F36_IN, F178_IN, F196_IN

Compound Symbols:

c23, c2, c4, c14, c18, c20, c24, c26, c29, c32, c35, c2

(19) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, 0) → U1(f34_in, 0, 0)
f1_in(z0, 0) → U2(f16_in(z0), z0, 0)
f1_in(0, z0) → f1_out1
f1_in(0, z0) → U3(f193_in(z0), 0, z0)
f1_in(z0, z1) → U4(f297_in(z0, z1), z0, z1)
f1_in(z0, z1) → f1_out1
U1(f34_out1, 0, 0) → f1_out1
U1(f34_out2, 0, 0) → f1_out1
U2(f16_out1, z0, 0) → f1_out1
U2(f16_out2, z0, 0) → f1_out1
U3(f193_out1, 0, z0) → f1_out1
U3(f193_out2, 0, z0) → f1_out1
U4(f297_out1(z0), z1, z2) → f1_out1
U4(f297_out4, z0, z1) → f1_out1
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
f303_in(z0, z1) → U7(f1_in(z0, z1), z0, z1)
U7(f1_out1, z0, z1) → f303_out1
f299_in(z0, z1) → f299_out3
f298_in(z0, z1) → U8(f302_in(z0, z1), z0, z1)
U8(f302_out1(z0), z1, z2) → U9(f303_in(z0, z2), z1, z2, z0)
U9(f303_out1, z0, z1, z2) → f298_out1(z2)
f16_in(z0) → U10(f81_in(z0), f82_in(z0), z0)
U10(f81_out1, z0, z1) → f16_out1
U10(z0, f82_out1, z1) → f16_out2
f34_inU11(f37_in, f38_in)
U11(f37_out1, z0) → f34_out1
U11(z0, f38_out1) → f34_out2
f193_in(z0) → U12(f197_in(z0), f198_in(z0), z0)
U12(f197_out1, z0, z1) → f193_out1
U12(z0, f198_out1, z1) → f193_out2
f297_in(z0, z1) → U13(f298_in(z0, z1), f299_in(z0, z1), z0, z1)
U13(f298_out1(z0), z1, z2, z3) → f297_out1(z0)
U13(z0, f299_out3, z1, z2) → f297_out4
Tuples:

F1_IN(0, 0) → c(U1'(f34_in, 0, 0), F34_IN)
F1_IN(z0, 0) → c1(U2'(f16_in(z0), z0, 0), F16_IN(z0))
F1_IN(0, z0) → c3(U3'(f193_in(z0), 0, z0), F193_IN(z0))
F1_IN(z0, z1) → c4(U4'(f297_in(z0, z1), z0, z1), F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(U5'(f309_in(z0, z1), s(z0), s(z1)), F309_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c17(U6'(f309_in(z0, z1), s(z0), s(z1)), F309_IN(z0, z1))
F303_IN(z0, z1) → c19(U7'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(U9'(f303_in(z0, z2), z1, z2, z0), F303_IN(z0, z2))
F16_IN(z0) → c25(U10'(f81_in(z0), f82_in(z0), z0))
F34_INc28(U11'(f37_in, f38_in))
F193_IN(z0) → c31(U12'(f197_in(z0), f198_in(z0), z0))
F297_IN(z0, z1) → c34(U13'(f298_in(z0, z1), f299_in(z0, z1), z0, z1), F298_IN(z0, z1), F299_IN(z0, z1))
S tuples:

F1_IN(0, 0) → c(U1'(f34_in, 0, 0), F34_IN)
F1_IN(z0, 0) → c1(U2'(f16_in(z0), z0, 0), F16_IN(z0))
F1_IN(0, z0) → c3(U3'(f193_in(z0), 0, z0), F193_IN(z0))
F1_IN(z0, z1) → c4(U4'(f297_in(z0, z1), z0, z1), F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(U5'(f309_in(z0, z1), s(z0), s(z1)), F309_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c17(U6'(f309_in(z0, z1), s(z0), s(z1)), F309_IN(z0, z1))
F303_IN(z0, z1) → c19(U7'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(U9'(f303_in(z0, z2), z1, z2, z0), F303_IN(z0, z2))
F16_IN(z0) → c25(U10'(f81_in(z0), f82_in(z0), z0))
F34_INc28(U11'(f37_in, f38_in))
F193_IN(z0) → c31(U12'(f197_in(z0), f198_in(z0), z0))
F297_IN(z0, z1) → c34(U13'(f298_in(z0, z1), f299_in(z0, z1), z0, z1), F298_IN(z0, z1), F299_IN(z0, z1))
K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, f309_in, U5, f302_in, U6, f303_in, U7, f299_in, f298_in, U8, U9, f16_in, U10, f34_in, U11, f193_in, U12, f297_in, U13

Defined Pair Symbols:

F1_IN, F309_IN, F302_IN, F303_IN, F298_IN, U8', F16_IN, F34_IN, F193_IN, F297_IN

Compound Symbols:

c, c1, c3, c4, c15, c17, c19, c22, c23, c25, c28, c31, c34

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

Split RHS of tuples not part of any SCC

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, 0) → U1(f34_in, 0, 0)
f1_in(z0, 0) → U2(f16_in(z0), z0, 0)
f1_in(0, z0) → f1_out1
f1_in(0, z0) → U3(f193_in(z0), 0, z0)
f1_in(z0, z1) → U4(f297_in(z0, z1), z0, z1)
f1_in(z0, z1) → f1_out1
U1(f34_out1, 0, 0) → f1_out1
U1(f34_out2, 0, 0) → f1_out1
U2(f16_out1, z0, 0) → f1_out1
U2(f16_out2, z0, 0) → f1_out1
U3(f193_out1, 0, z0) → f1_out1
U3(f193_out2, 0, z0) → f1_out1
U4(f297_out1(z0), z1, z2) → f1_out1
U4(f297_out4, z0, z1) → f1_out1
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
f303_in(z0, z1) → U7(f1_in(z0, z1), z0, z1)
U7(f1_out1, z0, z1) → f303_out1
f299_in(z0, z1) → f299_out3
f298_in(z0, z1) → U8(f302_in(z0, z1), z0, z1)
U8(f302_out1(z0), z1, z2) → U9(f303_in(z0, z2), z1, z2, z0)
U9(f303_out1, z0, z1, z2) → f298_out1(z2)
f16_in(z0) → U10(f81_in(z0), f82_in(z0), z0)
U10(f81_out1, z0, z1) → f16_out1
U10(z0, f82_out1, z1) → f16_out2
f34_inU11(f37_in, f38_in)
U11(f37_out1, z0) → f34_out1
U11(z0, f38_out1) → f34_out2
f193_in(z0) → U12(f197_in(z0), f198_in(z0), z0)
U12(f197_out1, z0, z1) → f193_out1
U12(z0, f198_out1, z1) → f193_out2
f297_in(z0, z1) → U13(f298_in(z0, z1), f299_in(z0, z1), z0, z1)
U13(f298_out1(z0), z1, z2, z3) → f297_out1(z0)
U13(z0, f299_out3, z1, z2) → f297_out4
Tuples:

F1_IN(z0, z1) → c4(U4'(f297_in(z0, z1), z0, z1), F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(U5'(f309_in(z0, z1), s(z0), s(z1)), F309_IN(z0, z1))
F303_IN(z0, z1) → c19(U7'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(U9'(f303_in(z0, z2), z1, z2, z0), F303_IN(z0, z2))
F16_IN(z0) → c25(U10'(f81_in(z0), f82_in(z0), z0))
F34_INc28(U11'(f37_in, f38_in))
F193_IN(z0) → c31(U12'(f197_in(z0), f198_in(z0), z0))
F297_IN(z0, z1) → c34(U13'(f298_in(z0, z1), f299_in(z0, z1), z0, z1), F298_IN(z0, z1), F299_IN(z0, z1))
F1_IN(0, 0) → c2(U1'(f34_in, 0, 0))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(U2'(f16_in(z0), z0, 0))
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(U3'(f193_in(z0), 0, z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(U6'(f309_in(z0, z1), s(z0), s(z1)))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
S tuples:

F1_IN(z0, z1) → c4(U4'(f297_in(z0, z1), z0, z1), F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(U5'(f309_in(z0, z1), s(z0), s(z1)), F309_IN(z0, z1))
F303_IN(z0, z1) → c19(U7'(f1_in(z0, z1), z0, z1), F1_IN(z0, z1))
F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(U9'(f303_in(z0, z2), z1, z2, z0), F303_IN(z0, z2))
F16_IN(z0) → c25(U10'(f81_in(z0), f82_in(z0), z0))
F34_INc28(U11'(f37_in, f38_in))
F193_IN(z0) → c31(U12'(f197_in(z0), f198_in(z0), z0))
F297_IN(z0, z1) → c34(U13'(f298_in(z0, z1), f299_in(z0, z1), z0, z1), F298_IN(z0, z1), F299_IN(z0, z1))
F1_IN(0, 0) → c2(U1'(f34_in, 0, 0))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(U2'(f16_in(z0), z0, 0))
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(U3'(f193_in(z0), 0, z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(U6'(f309_in(z0, z1), s(z0), s(z1)))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, f309_in, U5, f302_in, U6, f303_in, U7, f299_in, f298_in, U8, U9, f16_in, U10, f34_in, U11, f193_in, U12, f297_in, U13

Defined Pair Symbols:

F1_IN, F309_IN, F303_IN, F298_IN, U8', F16_IN, F34_IN, F193_IN, F297_IN, F302_IN

Compound Symbols:

c4, c15, c19, c22, c23, c25, c28, c31, c34, c2

(23) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 13 trailing tuple parts

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, 0) → U1(f34_in, 0, 0)
f1_in(z0, 0) → U2(f16_in(z0), z0, 0)
f1_in(0, z0) → f1_out1
f1_in(0, z0) → U3(f193_in(z0), 0, z0)
f1_in(z0, z1) → U4(f297_in(z0, z1), z0, z1)
f1_in(z0, z1) → f1_out1
U1(f34_out1, 0, 0) → f1_out1
U1(f34_out2, 0, 0) → f1_out1
U2(f16_out1, z0, 0) → f1_out1
U2(f16_out2, z0, 0) → f1_out1
U3(f193_out1, 0, z0) → f1_out1
U3(f193_out2, 0, z0) → f1_out1
U4(f297_out1(z0), z1, z2) → f1_out1
U4(f297_out4, z0, z1) → f1_out1
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
f303_in(z0, z1) → U7(f1_in(z0, z1), z0, z1)
U7(f1_out1, z0, z1) → f303_out1
f299_in(z0, z1) → f299_out3
f298_in(z0, z1) → U8(f302_in(z0, z1), z0, z1)
U8(f302_out1(z0), z1, z2) → U9(f303_in(z0, z2), z1, z2, z0)
U9(f303_out1, z0, z1, z2) → f298_out1(z2)
f16_in(z0) → U10(f81_in(z0), f82_in(z0), z0)
U10(f81_out1, z0, z1) → f16_out1
U10(z0, f82_out1, z1) → f16_out2
f34_inU11(f37_in, f38_in)
U11(f37_out1, z0) → f34_out1
U11(z0, f38_out1) → f34_out2
f193_in(z0) → U12(f197_in(z0), f198_in(z0), z0)
U12(f197_out1, z0, z1) → f193_out1
U12(z0, f198_out1, z1) → f193_out2
f297_in(z0, z1) → U13(f298_in(z0, z1), f299_in(z0, z1), z0, z1)
U13(f298_out1(z0), z1, z2, z3) → f297_out1(z0)
U13(z0, f299_out3, z1, z2) → f297_out4
Tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
S tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, f309_in, U5, f302_in, U6, f303_in, U7, f299_in, f298_in, U8, U9, f16_in, U10, f34_in, U11, f193_in, U12, f297_in, U13

Defined Pair Symbols:

F298_IN, F1_IN, F302_IN, F309_IN, F303_IN, U8', F16_IN, F34_IN, F193_IN, F297_IN

Compound Symbols:

c22, c2, c4, c15, c19, c23, c25, c28, c31, c34, c2

(25) 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.

F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F16_IN(z0) → c25
F34_INc28
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
We considered the (Usable) Rules:

f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
And the Tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [2]   
POL(F16_IN(x1)) = [1]   
POL(F193_IN(x1)) = x1   
POL(F1_IN(x1, x2)) = x2   
POL(F297_IN(x1, x2)) = x2   
POL(F298_IN(x1, x2)) = x2   
POL(F302_IN(x1, x2)) = 0   
POL(F303_IN(x1, x2)) = x2   
POL(F309_IN(x1, x2)) = 0   
POL(F34_IN) = [1]   
POL(U5(x1, x2, x3)) = 0   
POL(U6(x1, x2, x3)) = 0   
POL(U8'(x1, x2, x3)) = x3   
POL(c15(x1)) = x1   
POL(c19(x1)) = x1   
POL(c2) = 0   
POL(c2(x1)) = x1   
POL(c22(x1, x2)) = x1 + x2   
POL(c23(x1)) = x1   
POL(c25) = 0   
POL(c28) = 0   
POL(c31) = 0   
POL(c34(x1)) = x1   
POL(c4(x1)) = x1   
POL(f302_in(x1, x2)) = 0   
POL(f302_out1(x1)) = 0   
POL(f309_in(x1, x2)) = 0   
POL(f309_out1(x1)) = 0   
POL(s(x1)) = 0   

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, 0) → U1(f34_in, 0, 0)
f1_in(z0, 0) → U2(f16_in(z0), z0, 0)
f1_in(0, z0) → f1_out1
f1_in(0, z0) → U3(f193_in(z0), 0, z0)
f1_in(z0, z1) → U4(f297_in(z0, z1), z0, z1)
f1_in(z0, z1) → f1_out1
U1(f34_out1, 0, 0) → f1_out1
U1(f34_out2, 0, 0) → f1_out1
U2(f16_out1, z0, 0) → f1_out1
U2(f16_out2, z0, 0) → f1_out1
U3(f193_out1, 0, z0) → f1_out1
U3(f193_out2, 0, z0) → f1_out1
U4(f297_out1(z0), z1, z2) → f1_out1
U4(f297_out4, z0, z1) → f1_out1
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
f303_in(z0, z1) → U7(f1_in(z0, z1), z0, z1)
U7(f1_out1, z0, z1) → f303_out1
f299_in(z0, z1) → f299_out3
f298_in(z0, z1) → U8(f302_in(z0, z1), z0, z1)
U8(f302_out1(z0), z1, z2) → U9(f303_in(z0, z2), z1, z2, z0)
U9(f303_out1, z0, z1, z2) → f298_out1(z2)
f16_in(z0) → U10(f81_in(z0), f82_in(z0), z0)
U10(f81_out1, z0, z1) → f16_out1
U10(z0, f82_out1, z1) → f16_out2
f34_inU11(f37_in, f38_in)
U11(f37_out1, z0) → f34_out1
U11(z0, f38_out1) → f34_out2
f193_in(z0) → U12(f197_in(z0), f198_in(z0), z0)
U12(f197_out1, z0, z1) → f193_out1
U12(z0, f198_out1, z1) → f193_out2
f297_in(z0, z1) → U13(f298_in(z0, z1), f299_in(z0, z1), z0, z1)
U13(f298_out1(z0), z1, z2, z3) → f297_out1(z0)
U13(z0, f299_out3, z1, z2) → f297_out4
Tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
S tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
K tuples:

F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F16_IN(z0) → c25
F34_INc28
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, f309_in, U5, f302_in, U6, f303_in, U7, f299_in, f298_in, U8, U9, f16_in, U10, f34_in, U11, f193_in, U12, f297_in, U13

Defined Pair Symbols:

F298_IN, F1_IN, F302_IN, F309_IN, F303_IN, U8', F16_IN, F34_IN, F193_IN, F297_IN

Compound Symbols:

c22, c2, c4, c15, c19, c23, c25, c28, c31, c34, c2

(27) 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.

F1_IN(0, z0) → c2(F193_IN(z0))
F1_IN(0, z0) → c2
We considered the (Usable) Rules:

f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
And the Tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(F16_IN(x1)) = [2]   
POL(F193_IN(x1)) = 0   
POL(F1_IN(x1, x2)) = [2]   
POL(F297_IN(x1, x2)) = [2]   
POL(F298_IN(x1, x2)) = [2]   
POL(F302_IN(x1, x2)) = 0   
POL(F303_IN(x1, x2)) = [2]   
POL(F309_IN(x1, x2)) = 0   
POL(F34_IN) = [1]   
POL(U5(x1, x2, x3)) = 0   
POL(U6(x1, x2, x3)) = 0   
POL(U8'(x1, x2, x3)) = [2]   
POL(c15(x1)) = x1   
POL(c19(x1)) = x1   
POL(c2) = 0   
POL(c2(x1)) = x1   
POL(c22(x1, x2)) = x1 + x2   
POL(c23(x1)) = x1   
POL(c25) = 0   
POL(c28) = 0   
POL(c31) = 0   
POL(c34(x1)) = x1   
POL(c4(x1)) = x1   
POL(f302_in(x1, x2)) = 0   
POL(f302_out1(x1)) = 0   
POL(f309_in(x1, x2)) = 0   
POL(f309_out1(x1)) = 0   
POL(s(x1)) = 0   

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, 0) → U1(f34_in, 0, 0)
f1_in(z0, 0) → U2(f16_in(z0), z0, 0)
f1_in(0, z0) → f1_out1
f1_in(0, z0) → U3(f193_in(z0), 0, z0)
f1_in(z0, z1) → U4(f297_in(z0, z1), z0, z1)
f1_in(z0, z1) → f1_out1
U1(f34_out1, 0, 0) → f1_out1
U1(f34_out2, 0, 0) → f1_out1
U2(f16_out1, z0, 0) → f1_out1
U2(f16_out2, z0, 0) → f1_out1
U3(f193_out1, 0, z0) → f1_out1
U3(f193_out2, 0, z0) → f1_out1
U4(f297_out1(z0), z1, z2) → f1_out1
U4(f297_out4, z0, z1) → f1_out1
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
f303_in(z0, z1) → U7(f1_in(z0, z1), z0, z1)
U7(f1_out1, z0, z1) → f303_out1
f299_in(z0, z1) → f299_out3
f298_in(z0, z1) → U8(f302_in(z0, z1), z0, z1)
U8(f302_out1(z0), z1, z2) → U9(f303_in(z0, z2), z1, z2, z0)
U9(f303_out1, z0, z1, z2) → f298_out1(z2)
f16_in(z0) → U10(f81_in(z0), f82_in(z0), z0)
U10(f81_out1, z0, z1) → f16_out1
U10(z0, f82_out1, z1) → f16_out2
f34_inU11(f37_in, f38_in)
U11(f37_out1, z0) → f34_out1
U11(z0, f38_out1) → f34_out2
f193_in(z0) → U12(f197_in(z0), f198_in(z0), z0)
U12(f197_out1, z0, z1) → f193_out1
U12(z0, f198_out1, z1) → f193_out2
f297_in(z0, z1) → U13(f298_in(z0, z1), f299_in(z0, z1), z0, z1)
U13(f298_out1(z0), z1, z2, z3) → f297_out1(z0)
U13(z0, f299_out3, z1, z2) → f297_out4
Tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
S tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c2
K tuples:

F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F16_IN(z0) → c25
F34_INc28
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2(F193_IN(z0))
F1_IN(0, z0) → c2
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, f309_in, U5, f302_in, U6, f303_in, U7, f299_in, f298_in, U8, U9, f16_in, U10, f34_in, U11, f193_in, U12, f297_in, U13

Defined Pair Symbols:

F298_IN, F1_IN, F302_IN, F309_IN, F303_IN, U8', F16_IN, F34_IN, F193_IN, F297_IN

Compound Symbols:

c22, c2, c4, c15, c19, c23, c25, c28, c31, c34, c2

(29) CdtKnowledgeProof (EQUIVALENT transformation)

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

F193_IN(z0) → c31

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, 0) → U1(f34_in, 0, 0)
f1_in(z0, 0) → U2(f16_in(z0), z0, 0)
f1_in(0, z0) → f1_out1
f1_in(0, z0) → U3(f193_in(z0), 0, z0)
f1_in(z0, z1) → U4(f297_in(z0, z1), z0, z1)
f1_in(z0, z1) → f1_out1
U1(f34_out1, 0, 0) → f1_out1
U1(f34_out2, 0, 0) → f1_out1
U2(f16_out1, z0, 0) → f1_out1
U2(f16_out2, z0, 0) → f1_out1
U3(f193_out1, 0, z0) → f1_out1
U3(f193_out2, 0, z0) → f1_out1
U4(f297_out1(z0), z1, z2) → f1_out1
U4(f297_out4, z0, z1) → f1_out1
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
f303_in(z0, z1) → U7(f1_in(z0, z1), z0, z1)
U7(f1_out1, z0, z1) → f303_out1
f299_in(z0, z1) → f299_out3
f298_in(z0, z1) → U8(f302_in(z0, z1), z0, z1)
U8(f302_out1(z0), z1, z2) → U9(f303_in(z0, z2), z1, z2, z0)
U9(f303_out1, z0, z1, z2) → f298_out1(z2)
f16_in(z0) → U10(f81_in(z0), f82_in(z0), z0)
U10(f81_out1, z0, z1) → f16_out1
U10(z0, f82_out1, z1) → f16_out2
f34_inU11(f37_in, f38_in)
U11(f37_out1, z0) → f34_out1
U11(z0, f38_out1) → f34_out2
f193_in(z0) → U12(f197_in(z0), f198_in(z0), z0)
U12(f197_out1, z0, z1) → f193_out1
U12(z0, f198_out1, z1) → f193_out2
f297_in(z0, z1) → U13(f298_in(z0, z1), f299_in(z0, z1), z0, z1)
U13(f298_out1(z0), z1, z2, z3) → f297_out1(z0)
U13(z0, f299_out3, z1, z2) → f297_out4
Tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
S tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c2
K tuples:

F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F16_IN(z0) → c25
F34_INc28
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2(F193_IN(z0))
F1_IN(0, z0) → c2
F193_IN(z0) → c31
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, f309_in, U5, f302_in, U6, f303_in, U7, f299_in, f298_in, U8, U9, f16_in, U10, f34_in, U11, f193_in, U12, f297_in, U13

Defined Pair Symbols:

F298_IN, F1_IN, F302_IN, F309_IN, F303_IN, U8', F16_IN, F34_IN, F193_IN, F297_IN

Compound Symbols:

c22, c2, c4, c15, c19, c23, c25, c28, c31, c34, c2

(31) 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.

U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
We considered the (Usable) Rules:

f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
And the Tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(F16_IN(x1)) = [2]x1   
POL(F193_IN(x1)) = 0   
POL(F1_IN(x1, x2)) = [2]x1   
POL(F297_IN(x1, x2)) = [2]x1   
POL(F298_IN(x1, x2)) = [2]x1   
POL(F302_IN(x1, x2)) = 0   
POL(F303_IN(x1, x2)) = [2]x1   
POL(F309_IN(x1, x2)) = 0   
POL(F34_IN) = 0   
POL(U5(x1, x2, x3)) = x1   
POL(U6(x1, x2, x3)) = [1] + x1   
POL(U8'(x1, x2, x3)) = [2]x1   
POL(c15(x1)) = x1   
POL(c19(x1)) = x1   
POL(c2) = 0   
POL(c2(x1)) = x1   
POL(c22(x1, x2)) = x1 + x2   
POL(c23(x1)) = x1   
POL(c25) = 0   
POL(c28) = 0   
POL(c31) = 0   
POL(c34(x1)) = x1   
POL(c4(x1)) = x1   
POL(f302_in(x1, x2)) = x1   
POL(f302_out1(x1)) = [1] + x1   
POL(f309_in(x1, x2)) = x1   
POL(f309_out1(x1)) = x1   
POL(s(x1)) = [1] + x1   

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, 0) → U1(f34_in, 0, 0)
f1_in(z0, 0) → U2(f16_in(z0), z0, 0)
f1_in(0, z0) → f1_out1
f1_in(0, z0) → U3(f193_in(z0), 0, z0)
f1_in(z0, z1) → U4(f297_in(z0, z1), z0, z1)
f1_in(z0, z1) → f1_out1
U1(f34_out1, 0, 0) → f1_out1
U1(f34_out2, 0, 0) → f1_out1
U2(f16_out1, z0, 0) → f1_out1
U2(f16_out2, z0, 0) → f1_out1
U3(f193_out1, 0, z0) → f1_out1
U3(f193_out2, 0, z0) → f1_out1
U4(f297_out1(z0), z1, z2) → f1_out1
U4(f297_out4, z0, z1) → f1_out1
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
f303_in(z0, z1) → U7(f1_in(z0, z1), z0, z1)
U7(f1_out1, z0, z1) → f303_out1
f299_in(z0, z1) → f299_out3
f298_in(z0, z1) → U8(f302_in(z0, z1), z0, z1)
U8(f302_out1(z0), z1, z2) → U9(f303_in(z0, z2), z1, z2, z0)
U9(f303_out1, z0, z1, z2) → f298_out1(z2)
f16_in(z0) → U10(f81_in(z0), f82_in(z0), z0)
U10(f81_out1, z0, z1) → f16_out1
U10(z0, f82_out1, z1) → f16_out2
f34_inU11(f37_in, f38_in)
U11(f37_out1, z0) → f34_out1
U11(z0, f38_out1) → f34_out2
f193_in(z0) → U12(f197_in(z0), f198_in(z0), z0)
U12(f197_out1, z0, z1) → f193_out1
U12(z0, f198_out1, z1) → f193_out2
f297_in(z0, z1) → U13(f298_in(z0, z1), f299_in(z0, z1), z0, z1)
U13(f298_out1(z0), z1, z2, z3) → f297_out1(z0)
U13(z0, f299_out3, z1, z2) → f297_out4
Tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
S tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c2
K tuples:

F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F16_IN(z0) → c25
F34_INc28
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2(F193_IN(z0))
F1_IN(0, z0) → c2
F193_IN(z0) → c31
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, f309_in, U5, f302_in, U6, f303_in, U7, f299_in, f298_in, U8, U9, f16_in, U10, f34_in, U11, f193_in, U12, f297_in, U13

Defined Pair Symbols:

F298_IN, F1_IN, F302_IN, F309_IN, F303_IN, U8', F16_IN, F34_IN, F193_IN, F297_IN

Compound Symbols:

c22, c2, c4, c15, c19, c23, c25, c28, c31, c34, c2

(33) CdtKnowledgeProof (EQUIVALENT transformation)

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

F303_IN(z0, z1) → c19(F1_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F302_IN(s(z0), s(z1)) → c2

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, 0) → U1(f34_in, 0, 0)
f1_in(z0, 0) → U2(f16_in(z0), z0, 0)
f1_in(0, z0) → f1_out1
f1_in(0, z0) → U3(f193_in(z0), 0, z0)
f1_in(z0, z1) → U4(f297_in(z0, z1), z0, z1)
f1_in(z0, z1) → f1_out1
U1(f34_out1, 0, 0) → f1_out1
U1(f34_out2, 0, 0) → f1_out1
U2(f16_out1, z0, 0) → f1_out1
U2(f16_out2, z0, 0) → f1_out1
U3(f193_out1, 0, z0) → f1_out1
U3(f193_out2, 0, z0) → f1_out1
U4(f297_out1(z0), z1, z2) → f1_out1
U4(f297_out4, z0, z1) → f1_out1
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
f303_in(z0, z1) → U7(f1_in(z0, z1), z0, z1)
U7(f1_out1, z0, z1) → f303_out1
f299_in(z0, z1) → f299_out3
f298_in(z0, z1) → U8(f302_in(z0, z1), z0, z1)
U8(f302_out1(z0), z1, z2) → U9(f303_in(z0, z2), z1, z2, z0)
U9(f303_out1, z0, z1, z2) → f298_out1(z2)
f16_in(z0) → U10(f81_in(z0), f82_in(z0), z0)
U10(f81_out1, z0, z1) → f16_out1
U10(z0, f82_out1, z1) → f16_out2
f34_inU11(f37_in, f38_in)
U11(f37_out1, z0) → f34_out1
U11(z0, f38_out1) → f34_out2
f193_in(z0) → U12(f197_in(z0), f198_in(z0), z0)
U12(f197_out1, z0, z1) → f193_out1
U12(z0, f198_out1, z1) → f193_out2
f297_in(z0, z1) → U13(f298_in(z0, z1), f299_in(z0, z1), z0, z1)
U13(f298_out1(z0), z1, z2, z3) → f297_out1(z0)
U13(z0, f299_out3, z1, z2) → f297_out4
Tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
S tuples:

F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
K tuples:

F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F16_IN(z0) → c25
F34_INc28
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2(F193_IN(z0))
F1_IN(0, z0) → c2
F193_IN(z0) → c31
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c2
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, f309_in, U5, f302_in, U6, f303_in, U7, f299_in, f298_in, U8, U9, f16_in, U10, f34_in, U11, f193_in, U12, f297_in, U13

Defined Pair Symbols:

F298_IN, F1_IN, F302_IN, F309_IN, F303_IN, U8', F16_IN, F34_IN, F193_IN, F297_IN

Compound Symbols:

c22, c2, c4, c15, c19, c23, c25, c28, c31, c34, c2

(35) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
We considered the (Usable) Rules:

f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
And the Tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(F16_IN(x1)) = 0   
POL(F193_IN(x1)) = x1 + x12   
POL(F1_IN(x1, x2)) = x2 + x22 + x1·x2   
POL(F297_IN(x1, x2)) = x2 + x22 + x1·x2   
POL(F298_IN(x1, x2)) = x2 + x22 + x1·x2   
POL(F302_IN(x1, x2)) = x2   
POL(F303_IN(x1, x2)) = x2 + x22 + x1·x2   
POL(F309_IN(x1, x2)) = [1] + x2   
POL(F34_IN) = 0   
POL(U5(x1, x2, x3)) = x1   
POL(U6(x1, x2, x3)) = [1] + x1   
POL(U8'(x1, x2, x3)) = x32 + x1·x3   
POL(c15(x1)) = x1   
POL(c19(x1)) = x1   
POL(c2) = 0   
POL(c2(x1)) = x1   
POL(c22(x1, x2)) = x1 + x2   
POL(c23(x1)) = x1   
POL(c25) = 0   
POL(c28) = 0   
POL(c31) = 0   
POL(c34(x1)) = x1   
POL(c4(x1)) = x1   
POL(f302_in(x1, x2)) = x1   
POL(f302_out1(x1)) = [1] + x1   
POL(f309_in(x1, x2)) = x1   
POL(f309_out1(x1)) = x1   
POL(s(x1)) = [1] + x1   

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, 0) → U1(f34_in, 0, 0)
f1_in(z0, 0) → U2(f16_in(z0), z0, 0)
f1_in(0, z0) → f1_out1
f1_in(0, z0) → U3(f193_in(z0), 0, z0)
f1_in(z0, z1) → U4(f297_in(z0, z1), z0, z1)
f1_in(z0, z1) → f1_out1
U1(f34_out1, 0, 0) → f1_out1
U1(f34_out2, 0, 0) → f1_out1
U2(f16_out1, z0, 0) → f1_out1
U2(f16_out2, z0, 0) → f1_out1
U3(f193_out1, 0, z0) → f1_out1
U3(f193_out2, 0, z0) → f1_out1
U4(f297_out1(z0), z1, z2) → f1_out1
U4(f297_out4, z0, z1) → f1_out1
f309_in(z0, 0) → f309_out1(z0)
f309_in(s(z0), s(z1)) → U5(f309_in(z0, z1), s(z0), s(z1))
U5(f309_out1(z0), s(z1), s(z2)) → f309_out1(z0)
f302_in(s(z0), s(z1)) → U6(f309_in(z0, z1), s(z0), s(z1))
U6(f309_out1(z0), s(z1), s(z2)) → f302_out1(z0)
f303_in(z0, z1) → U7(f1_in(z0, z1), z0, z1)
U7(f1_out1, z0, z1) → f303_out1
f299_in(z0, z1) → f299_out3
f298_in(z0, z1) → U8(f302_in(z0, z1), z0, z1)
U8(f302_out1(z0), z1, z2) → U9(f303_in(z0, z2), z1, z2, z0)
U9(f303_out1, z0, z1, z2) → f298_out1(z2)
f16_in(z0) → U10(f81_in(z0), f82_in(z0), z0)
U10(f81_out1, z0, z1) → f16_out1
U10(z0, f82_out1, z1) → f16_out2
f34_inU11(f37_in, f38_in)
U11(f37_out1, z0) → f34_out1
U11(z0, f38_out1) → f34_out2
f193_in(z0) → U12(f197_in(z0), f198_in(z0), z0)
U12(f197_out1, z0, z1) → f193_out1
U12(z0, f198_out1, z1) → f193_out2
f297_in(z0, z1) → U13(f298_in(z0, z1), f299_in(z0, z1), z0, z1)
U13(f298_out1(z0), z1, z2, z3) → f297_out1(z0)
U13(z0, f299_out3, z1, z2) → f297_out4
Tuples:

F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F1_IN(0, z0) → c2(F193_IN(z0))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F16_IN(z0) → c25
F34_INc28
F193_IN(z0) → c31
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2
F302_IN(s(z0), s(z1)) → c2
S tuples:none
K tuples:

F1_IN(0, 0) → c2(F34_IN)
F1_IN(z0, 0) → c2(F16_IN(z0))
F16_IN(z0) → c25
F34_INc28
F1_IN(0, 0) → c2
F1_IN(z0, 0) → c2
F1_IN(0, z0) → c2(F193_IN(z0))
F1_IN(0, z0) → c2
F193_IN(z0) → c31
U8'(f302_out1(z0), z1, z2) → c23(F303_IN(z0, z2))
F303_IN(z0, z1) → c19(F1_IN(z0, z1))
F1_IN(z0, z1) → c4(F297_IN(z0, z1))
F297_IN(z0, z1) → c34(F298_IN(z0, z1))
F298_IN(z0, z1) → c22(U8'(f302_in(z0, z1), z0, z1), F302_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c2(F309_IN(z0, z1))
F302_IN(s(z0), s(z1)) → c2
F309_IN(s(z0), s(z1)) → c15(F309_IN(z0, z1))
Defined Rule Symbols:

f1_in, U1, U2, U3, U4, f309_in, U5, f302_in, U6, f303_in, U7, f299_in, f298_in, U8, U9, f16_in, U10, f34_in, U11, f193_in, U12, f297_in, U13

Defined Pair Symbols:

F298_IN, F1_IN, F302_IN, F309_IN, F303_IN, U8', F16_IN, F34_IN, F193_IN, F297_IN

Compound Symbols:

c22, c2, c4, c15, c19, c23, c25, c28, c31, c34, c2

(37) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(38) BOUNDS(O(1), O(1))