(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_in → U12(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_IN → c29(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_IN → c29(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_in → U12(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_IN → c29(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_IN → c29(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_in → U12(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_IN → c29
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_IN → c29
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_IN → c29
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_in → U12(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_IN → c29
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_IN → c29
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_IN → c29
(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_in → U12(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_IN → c29
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_IN → c29
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_IN → c29
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_in → U12(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_IN → c29
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_IN → c29
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_IN → c29
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_in → U12(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_IN → c29
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_IN → c29
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_IN → c29
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_in → U12(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_IN → c29
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_IN → c29
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_in → U12(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_IN → c29
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_IN → c29
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_in → U11(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_IN → c28(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_IN → c28(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_in → U11(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_IN → c28(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_IN → c28(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_in → U11(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_IN → c28
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_IN → c28
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_IN → c28
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_IN → c28
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_in → U11(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_IN → c28
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_IN → c28
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_IN → c28
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_in → U11(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_IN → c28
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_IN → c28
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_in → U11(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_IN → c28
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_IN → c28
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_IN → c28
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_in → U11(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_IN → c28
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_IN → c28
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_in → U11(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_IN → c28
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_IN → c28
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_IN → c28
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_in → U11(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_IN → c28
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_IN → c28
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))