(0) Obligation:
Clauses:
p(X, X).
p(f(X), g(Y)) :- ','(p(f(X), f(Z)), p(Z, g(W))).
Query: p(g,a)
(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0) → f1_out1
f1_in(f(z0)) → U1(f13_in(z0), f(z0))
f1_in(f(z0)) → U2(f13_in(z0), f(z0))
U1(f13_out1, f(z0)) → f1_out1
U2(f13_out1, f(z0)) → f1_out1
f18_in → f18_out1
f18_in → U3(f36_in)
f18_in → U4(f36_in)
U3(f36_out1) → f18_out1
U4(f36_out1) → f18_out1
f17_in(z0) → f17_out1
f38_in → f38_out1
f13_in(z0) → U5(f17_in(z0), z0)
U5(f17_out1, z0) → U6(f18_in, z0)
U6(f18_out1, z0) → f13_out1
f36_in → U7(f38_in)
U7(f38_out1) → U8(f18_in)
U8(f18_out1) → f36_out1
Tuples:
F1_IN(f(z0)) → c1(U1'(f13_in(z0), f(z0)), F13_IN(z0))
F1_IN(f(z0)) → c2(U2'(f13_in(z0), f(z0)), F13_IN(z0))
F18_IN → c6(U3'(f36_in), F36_IN)
F18_IN → c7(U4'(f36_in), F36_IN)
F13_IN(z0) → c12(U5'(f17_in(z0), z0), F17_IN(z0))
U5'(f17_out1, z0) → c13(U6'(f18_in, z0), F18_IN)
F36_IN → c15(U7'(f38_in), F38_IN)
U7'(f38_out1) → c16(U8'(f18_in), F18_IN)
S tuples:
F1_IN(f(z0)) → c1(U1'(f13_in(z0), f(z0)), F13_IN(z0))
F1_IN(f(z0)) → c2(U2'(f13_in(z0), f(z0)), F13_IN(z0))
F18_IN → c6(U3'(f36_in), F36_IN)
F18_IN → c7(U4'(f36_in), F36_IN)
F13_IN(z0) → c12(U5'(f17_in(z0), z0), F17_IN(z0))
U5'(f17_out1, z0) → c13(U6'(f18_in, z0), F18_IN)
F36_IN → c15(U7'(f38_in), F38_IN)
U7'(f38_out1) → c16(U8'(f18_in), F18_IN)
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f18_in, U3, U4, f17_in, f38_in, f13_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F1_IN, F18_IN, F13_IN, U5', F36_IN, U7'
Compound Symbols:
c1, c2, c6, c7, c12, c13, c15, c16
(3) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0) → f1_out1
f1_in(f(z0)) → U1(f13_in(z0), f(z0))
f1_in(f(z0)) → U2(f13_in(z0), f(z0))
U1(f13_out1, f(z0)) → f1_out1
U2(f13_out1, f(z0)) → f1_out1
f18_in → f18_out1
f18_in → U3(f36_in)
f18_in → U4(f36_in)
U3(f36_out1) → f18_out1
U4(f36_out1) → f18_out1
f17_in(z0) → f17_out1
f38_in → f38_out1
f13_in(z0) → U5(f17_in(z0), z0)
U5(f17_out1, z0) → U6(f18_in, z0)
U6(f18_out1, z0) → f13_out1
f36_in → U7(f38_in)
U7(f38_out1) → U8(f18_in)
U8(f18_out1) → f36_out1
Tuples:
F18_IN → c6(U3'(f36_in), F36_IN)
F18_IN → c7(U4'(f36_in), F36_IN)
F36_IN → c15(U7'(f38_in), F38_IN)
U7'(f38_out1) → c16(U8'(f18_in), F18_IN)
F1_IN(f(z0)) → c(U1'(f13_in(z0), f(z0)))
F1_IN(f(z0)) → c(F13_IN(z0))
F1_IN(f(z0)) → c(U2'(f13_in(z0), f(z0)))
F13_IN(z0) → c(U5'(f17_in(z0), z0))
F13_IN(z0) → c(F17_IN(z0))
U5'(f17_out1, z0) → c(U6'(f18_in, z0))
U5'(f17_out1, z0) → c(F18_IN)
S tuples:
F18_IN → c6(U3'(f36_in), F36_IN)
F18_IN → c7(U4'(f36_in), F36_IN)
F36_IN → c15(U7'(f38_in), F38_IN)
U7'(f38_out1) → c16(U8'(f18_in), F18_IN)
F1_IN(f(z0)) → c(U1'(f13_in(z0), f(z0)))
F1_IN(f(z0)) → c(F13_IN(z0))
F1_IN(f(z0)) → c(U2'(f13_in(z0), f(z0)))
F13_IN(z0) → c(U5'(f17_in(z0), z0))
F13_IN(z0) → c(F17_IN(z0))
U5'(f17_out1, z0) → c(U6'(f18_in, z0))
U5'(f17_out1, z0) → c(F18_IN)
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f18_in, U3, U4, f17_in, f38_in, f13_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F18_IN, F36_IN, U7', F1_IN, F13_IN, U5'
Compound Symbols:
c6, c7, c15, c16, c
(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 8 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0) → f1_out1
f1_in(f(z0)) → U1(f13_in(z0), f(z0))
f1_in(f(z0)) → U2(f13_in(z0), f(z0))
U1(f13_out1, f(z0)) → f1_out1
U2(f13_out1, f(z0)) → f1_out1
f18_in → f18_out1
f18_in → U3(f36_in)
f18_in → U4(f36_in)
U3(f36_out1) → f18_out1
U4(f36_out1) → f18_out1
f17_in(z0) → f17_out1
f38_in → f38_out1
f13_in(z0) → U5(f17_in(z0), z0)
U5(f17_out1, z0) → U6(f18_in, z0)
U6(f18_out1, z0) → f13_out1
f36_in → U7(f38_in)
U7(f38_out1) → U8(f18_in)
U8(f18_out1) → f36_out1
Tuples:
F1_IN(f(z0)) → c(F13_IN(z0))
F13_IN(z0) → c(U5'(f17_in(z0), z0))
U5'(f17_out1, z0) → c(F18_IN)
F18_IN → c6(F36_IN)
F18_IN → c7(F36_IN)
F36_IN → c15(U7'(f38_in))
U7'(f38_out1) → c16(F18_IN)
F1_IN(f(z0)) → c
F13_IN(z0) → c
U5'(f17_out1, z0) → c
S tuples:
F1_IN(f(z0)) → c(F13_IN(z0))
F13_IN(z0) → c(U5'(f17_in(z0), z0))
U5'(f17_out1, z0) → c(F18_IN)
F18_IN → c6(F36_IN)
F18_IN → c7(F36_IN)
F36_IN → c15(U7'(f38_in))
U7'(f38_out1) → c16(F18_IN)
F1_IN(f(z0)) → c
F13_IN(z0) → c
U5'(f17_out1, z0) → c
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, f18_in, U3, U4, f17_in, f38_in, f13_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F1_IN, F13_IN, U5', F18_IN, F36_IN, U7'
Compound Symbols:
c, c6, c7, c15, c16, c
(7) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F1_IN(f(z0)) → c(F13_IN(z0))
F1_IN(f(z0)) → c(F13_IN(z0))
F13_IN(z0) → c(U5'(f17_in(z0), z0))
U5'(f17_out1, z0) → c(F18_IN)
F1_IN(f(z0)) → c
F1_IN(f(z0)) → c
F13_IN(z0) → c
U5'(f17_out1, z0) → c
F13_IN(z0) → c(U5'(f17_in(z0), z0))
F13_IN(z0) → c
U5'(f17_out1, z0) → c(F18_IN)
U5'(f17_out1, z0) → c
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0) → f1_out1
f1_in(f(z0)) → U1(f13_in(z0), f(z0))
f1_in(f(z0)) → U2(f13_in(z0), f(z0))
U1(f13_out1, f(z0)) → f1_out1
U2(f13_out1, f(z0)) → f1_out1
f18_in → f18_out1
f18_in → U3(f36_in)
f18_in → U4(f36_in)
U3(f36_out1) → f18_out1
U4(f36_out1) → f18_out1
f17_in(z0) → f17_out1
f38_in → f38_out1
f13_in(z0) → U5(f17_in(z0), z0)
U5(f17_out1, z0) → U6(f18_in, z0)
U6(f18_out1, z0) → f13_out1
f36_in → U7(f38_in)
U7(f38_out1) → U8(f18_in)
U8(f18_out1) → f36_out1
Tuples:
F1_IN(f(z0)) → c(F13_IN(z0))
F13_IN(z0) → c(U5'(f17_in(z0), z0))
U5'(f17_out1, z0) → c(F18_IN)
F18_IN → c6(F36_IN)
F18_IN → c7(F36_IN)
F36_IN → c15(U7'(f38_in))
U7'(f38_out1) → c16(F18_IN)
F1_IN(f(z0)) → c
F13_IN(z0) → c
U5'(f17_out1, z0) → c
S tuples:
F18_IN → c6(F36_IN)
F18_IN → c7(F36_IN)
F36_IN → c15(U7'(f38_in))
U7'(f38_out1) → c16(F18_IN)
K tuples:
F1_IN(f(z0)) → c(F13_IN(z0))
F13_IN(z0) → c(U5'(f17_in(z0), z0))
U5'(f17_out1, z0) → c(F18_IN)
F1_IN(f(z0)) → c
F13_IN(z0) → c
U5'(f17_out1, z0) → c
Defined Rule Symbols:
f1_in, U1, U2, f18_in, U3, U4, f17_in, f38_in, f13_in, U5, U6, f36_in, U7, U8
Defined Pair Symbols:
F1_IN, F13_IN, U5', F18_IN, F36_IN, U7'
Compound Symbols:
c, c6, c7, c15, c16, c
(9) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0) → f2_out1
f2_in(f(z0)) → U1(f11_in(z0), f(z0))
f2_in(f(z0)) → U2(f48_in(z0), f(z0))
U1(f11_out1, f(z0)) → f2_out1
U2(f48_out1, f(z0)) → f2_out1
U2(f48_out2, f(z0)) → f2_out1
f19_in(g(z0)) → f19_out1
f19_in(f(z0)) → U3(f11_in(z0), f(z0))
U3(f11_out1, f(z0)) → f19_out1
f11_in(z0) → U4(f16_in(z0), z0)
U4(f16_out1, z0) → f11_out1
U4(f16_out2, z0) → f11_out1
f16_in(z0) → U5(f19_in(z0), f21_in(z0), z0)
U5(f19_out1, z0, z1) → f16_out1
U5(z0, f21_out1, z1) → f16_out2
f48_in(z0) → U6(f19_in(z0), f50_in(z0), z0)
U6(f19_out1, z0, z1) → f48_out1
U6(z0, f50_out1, z1) → f48_out2
Tuples:
F2_IN(f(z0)) → c1(U1'(f11_in(z0), f(z0)), F11_IN(z0))
F2_IN(f(z0)) → c2(U2'(f48_in(z0), f(z0)), F48_IN(z0))
F19_IN(f(z0)) → c7(U3'(f11_in(z0), f(z0)), F11_IN(z0))
F11_IN(z0) → c9(U4'(f16_in(z0), z0), F16_IN(z0))
F16_IN(z0) → c12(U5'(f19_in(z0), f21_in(z0), z0), F19_IN(z0))
F48_IN(z0) → c15(U6'(f19_in(z0), f50_in(z0), z0), F19_IN(z0))
S tuples:
F2_IN(f(z0)) → c1(U1'(f11_in(z0), f(z0)), F11_IN(z0))
F2_IN(f(z0)) → c2(U2'(f48_in(z0), f(z0)), F48_IN(z0))
F19_IN(f(z0)) → c7(U3'(f11_in(z0), f(z0)), F11_IN(z0))
F11_IN(z0) → c9(U4'(f16_in(z0), z0), F16_IN(z0))
F16_IN(z0) → c12(U5'(f19_in(z0), f21_in(z0), z0), F19_IN(z0))
F48_IN(z0) → c15(U6'(f19_in(z0), f50_in(z0), z0), F19_IN(z0))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f19_in, U3, f11_in, U4, f16_in, U5, f48_in, U6
Defined Pair Symbols:
F2_IN, F19_IN, F11_IN, F16_IN, F48_IN
Compound Symbols:
c1, c2, c7, c9, c12, c15
(11) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0) → f2_out1
f2_in(f(z0)) → U1(f11_in(z0), f(z0))
f2_in(f(z0)) → U2(f48_in(z0), f(z0))
U1(f11_out1, f(z0)) → f2_out1
U2(f48_out1, f(z0)) → f2_out1
U2(f48_out2, f(z0)) → f2_out1
f19_in(g(z0)) → f19_out1
f19_in(f(z0)) → U3(f11_in(z0), f(z0))
U3(f11_out1, f(z0)) → f19_out1
f11_in(z0) → U4(f16_in(z0), z0)
U4(f16_out1, z0) → f11_out1
U4(f16_out2, z0) → f11_out1
f16_in(z0) → U5(f19_in(z0), f21_in(z0), z0)
U5(f19_out1, z0, z1) → f16_out1
U5(z0, f21_out1, z1) → f16_out2
f48_in(z0) → U6(f19_in(z0), f50_in(z0), z0)
U6(f19_out1, z0, z1) → f48_out1
U6(z0, f50_out1, z1) → f48_out2
Tuples:
F19_IN(f(z0)) → c7(U3'(f11_in(z0), f(z0)), F11_IN(z0))
F11_IN(z0) → c9(U4'(f16_in(z0), z0), F16_IN(z0))
F16_IN(z0) → c12(U5'(f19_in(z0), f21_in(z0), z0), F19_IN(z0))
F2_IN(f(z0)) → c(U1'(f11_in(z0), f(z0)))
F2_IN(f(z0)) → c(F11_IN(z0))
F2_IN(f(z0)) → c(U2'(f48_in(z0), f(z0)))
F2_IN(f(z0)) → c(F48_IN(z0))
F48_IN(z0) → c(U6'(f19_in(z0), f50_in(z0), z0))
F48_IN(z0) → c(F19_IN(z0))
S tuples:
F19_IN(f(z0)) → c7(U3'(f11_in(z0), f(z0)), F11_IN(z0))
F11_IN(z0) → c9(U4'(f16_in(z0), z0), F16_IN(z0))
F16_IN(z0) → c12(U5'(f19_in(z0), f21_in(z0), z0), F19_IN(z0))
F2_IN(f(z0)) → c(U1'(f11_in(z0), f(z0)))
F2_IN(f(z0)) → c(F11_IN(z0))
F2_IN(f(z0)) → c(U2'(f48_in(z0), f(z0)))
F2_IN(f(z0)) → c(F48_IN(z0))
F48_IN(z0) → c(U6'(f19_in(z0), f50_in(z0), z0))
F48_IN(z0) → c(F19_IN(z0))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f19_in, U3, f11_in, U4, f16_in, U5, f48_in, U6
Defined Pair Symbols:
F19_IN, F11_IN, F16_IN, F2_IN, F48_IN
Compound Symbols:
c7, c9, c12, c
(13) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 6 trailing tuple parts
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0) → f2_out1
f2_in(f(z0)) → U1(f11_in(z0), f(z0))
f2_in(f(z0)) → U2(f48_in(z0), f(z0))
U1(f11_out1, f(z0)) → f2_out1
U2(f48_out1, f(z0)) → f2_out1
U2(f48_out2, f(z0)) → f2_out1
f19_in(g(z0)) → f19_out1
f19_in(f(z0)) → U3(f11_in(z0), f(z0))
U3(f11_out1, f(z0)) → f19_out1
f11_in(z0) → U4(f16_in(z0), z0)
U4(f16_out1, z0) → f11_out1
U4(f16_out2, z0) → f11_out1
f16_in(z0) → U5(f19_in(z0), f21_in(z0), z0)
U5(f19_out1, z0, z1) → f16_out1
U5(z0, f21_out1, z1) → f16_out2
f48_in(z0) → U6(f19_in(z0), f50_in(z0), z0)
U6(f19_out1, z0, z1) → f48_out1
U6(z0, f50_out1, z1) → f48_out2
Tuples:
F2_IN(f(z0)) → c(F11_IN(z0))
F2_IN(f(z0)) → c(F48_IN(z0))
F48_IN(z0) → c(F19_IN(z0))
F19_IN(f(z0)) → c7(F11_IN(z0))
F11_IN(z0) → c9(F16_IN(z0))
F16_IN(z0) → c12(F19_IN(z0))
F2_IN(f(z0)) → c
F48_IN(z0) → c
S tuples:
F2_IN(f(z0)) → c(F11_IN(z0))
F2_IN(f(z0)) → c(F48_IN(z0))
F48_IN(z0) → c(F19_IN(z0))
F19_IN(f(z0)) → c7(F11_IN(z0))
F11_IN(z0) → c9(F16_IN(z0))
F16_IN(z0) → c12(F19_IN(z0))
F2_IN(f(z0)) → c
F48_IN(z0) → c
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2, f19_in, U3, f11_in, U4, f16_in, U5, f48_in, U6
Defined Pair Symbols:
F2_IN, F48_IN, F19_IN, F11_IN, F16_IN
Compound Symbols:
c, c7, c9, c12, c
(15) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F2_IN(f(z0)) → c(F11_IN(z0))
F2_IN(f(z0)) → c(F48_IN(z0))
F48_IN(z0) → c(F19_IN(z0))
F2_IN(f(z0)) → c
F2_IN(f(z0)) → c
F48_IN(z0) → c
F48_IN(z0) → c(F19_IN(z0))
F48_IN(z0) → c
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0) → f2_out1
f2_in(f(z0)) → U1(f11_in(z0), f(z0))
f2_in(f(z0)) → U2(f48_in(z0), f(z0))
U1(f11_out1, f(z0)) → f2_out1
U2(f48_out1, f(z0)) → f2_out1
U2(f48_out2, f(z0)) → f2_out1
f19_in(g(z0)) → f19_out1
f19_in(f(z0)) → U3(f11_in(z0), f(z0))
U3(f11_out1, f(z0)) → f19_out1
f11_in(z0) → U4(f16_in(z0), z0)
U4(f16_out1, z0) → f11_out1
U4(f16_out2, z0) → f11_out1
f16_in(z0) → U5(f19_in(z0), f21_in(z0), z0)
U5(f19_out1, z0, z1) → f16_out1
U5(z0, f21_out1, z1) → f16_out2
f48_in(z0) → U6(f19_in(z0), f50_in(z0), z0)
U6(f19_out1, z0, z1) → f48_out1
U6(z0, f50_out1, z1) → f48_out2
Tuples:
F2_IN(f(z0)) → c(F11_IN(z0))
F2_IN(f(z0)) → c(F48_IN(z0))
F48_IN(z0) → c(F19_IN(z0))
F19_IN(f(z0)) → c7(F11_IN(z0))
F11_IN(z0) → c9(F16_IN(z0))
F16_IN(z0) → c12(F19_IN(z0))
F2_IN(f(z0)) → c
F48_IN(z0) → c
S tuples:
F19_IN(f(z0)) → c7(F11_IN(z0))
F11_IN(z0) → c9(F16_IN(z0))
F16_IN(z0) → c12(F19_IN(z0))
K tuples:
F2_IN(f(z0)) → c(F11_IN(z0))
F2_IN(f(z0)) → c(F48_IN(z0))
F48_IN(z0) → c(F19_IN(z0))
F2_IN(f(z0)) → c
F48_IN(z0) → c
Defined Rule Symbols:
f2_in, U1, U2, f19_in, U3, f11_in, U4, f16_in, U5, f48_in, U6
Defined Pair Symbols:
F2_IN, F48_IN, F19_IN, F11_IN, F16_IN
Compound Symbols:
c, c7, c9, c12, c
(17) 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.
F11_IN(z0) → c9(F16_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(f(z0)) → c(F11_IN(z0))
F2_IN(f(z0)) → c(F48_IN(z0))
F48_IN(z0) → c(F19_IN(z0))
F19_IN(f(z0)) → c7(F11_IN(z0))
F11_IN(z0) → c9(F16_IN(z0))
F16_IN(z0) → c12(F19_IN(z0))
F2_IN(f(z0)) → c
F48_IN(z0) → c
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F11_IN(x1)) = [2] + [2]x1
POL(F16_IN(x1)) = [2]x1
POL(F19_IN(x1)) = [2]x1
POL(F2_IN(x1)) = [3]x1
POL(F48_IN(x1)) = [3] + [3]x1
POL(c) = 0
POL(c(x1)) = x1
POL(c12(x1)) = x1
POL(c7(x1)) = x1
POL(c9(x1)) = x1
POL(f(x1)) = [1] + x1
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(z0) → f2_out1
f2_in(f(z0)) → U1(f11_in(z0), f(z0))
f2_in(f(z0)) → U2(f48_in(z0), f(z0))
U1(f11_out1, f(z0)) → f2_out1
U2(f48_out1, f(z0)) → f2_out1
U2(f48_out2, f(z0)) → f2_out1
f19_in(g(z0)) → f19_out1
f19_in(f(z0)) → U3(f11_in(z0), f(z0))
U3(f11_out1, f(z0)) → f19_out1
f11_in(z0) → U4(f16_in(z0), z0)
U4(f16_out1, z0) → f11_out1
U4(f16_out2, z0) → f11_out1
f16_in(z0) → U5(f19_in(z0), f21_in(z0), z0)
U5(f19_out1, z0, z1) → f16_out1
U5(z0, f21_out1, z1) → f16_out2
f48_in(z0) → U6(f19_in(z0), f50_in(z0), z0)
U6(f19_out1, z0, z1) → f48_out1
U6(z0, f50_out1, z1) → f48_out2
Tuples:
F2_IN(f(z0)) → c(F11_IN(z0))
F2_IN(f(z0)) → c(F48_IN(z0))
F48_IN(z0) → c(F19_IN(z0))
F19_IN(f(z0)) → c7(F11_IN(z0))
F11_IN(z0) → c9(F16_IN(z0))
F16_IN(z0) → c12(F19_IN(z0))
F2_IN(f(z0)) → c
F48_IN(z0) → c
S tuples:
F19_IN(f(z0)) → c7(F11_IN(z0))
F16_IN(z0) → c12(F19_IN(z0))
K tuples:
F2_IN(f(z0)) → c(F11_IN(z0))
F2_IN(f(z0)) → c(F48_IN(z0))
F48_IN(z0) → c(F19_IN(z0))
F2_IN(f(z0)) → c
F48_IN(z0) → c
F11_IN(z0) → c9(F16_IN(z0))
Defined Rule Symbols:
f2_in, U1, U2, f19_in, U3, f11_in, U4, f16_in, U5, f48_in, U6
Defined Pair Symbols:
F2_IN, F48_IN, F19_IN, F11_IN, F16_IN
Compound Symbols:
c, c7, c9, c12, c
(19) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F16_IN(z0) → c12(F19_IN(z0))
F19_IN(f(z0)) → c7(F11_IN(z0))
F11_IN(z0) → c9(F16_IN(z0))
Now S is empty
(20) BOUNDS(O(1), O(1))