(0) Obligation:
Clauses:
p(X) :- ','(q(f(Y)), p(Y)).
p(g(X)) :- p(X).
q(g(Y)).
Query: p(g)
(1) LPReorderTransformerProof (EQUIVALENT transformation)
Reordered facts before rules in definite LP [PROLOG].
(2) Obligation:
Clauses:
q(g(Y)).
p(X) :- ','(q(f(Y)), p(Y)).
p(g(X)) :- p(X).
Query: p(g)
(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0) → U1(f4_in(z0), z0)
U1(f4_out1, z0) → f1_out1
U1(f4_out2, z0) → f1_out1
f7_in(g(z0)) → U2(f1_in(z0), g(z0))
U2(f1_out1, g(z0)) → f7_out1
f4_in(z0) → U3(f6_in(z0), f7_in(z0), z0)
U3(f6_out1, z0, z1) → f4_out1
U3(z0, f7_out1, z1) → f4_out2
Tuples:
F1_IN(z0) → c(U1'(f4_in(z0), z0), F4_IN(z0))
F7_IN(g(z0)) → c3(U2'(f1_in(z0), g(z0)), F1_IN(z0))
F4_IN(z0) → c5(U3'(f6_in(z0), f7_in(z0), z0), F7_IN(z0))
S tuples:
F1_IN(z0) → c(U1'(f4_in(z0), z0), F4_IN(z0))
F7_IN(g(z0)) → c3(U2'(f1_in(z0), g(z0)), F1_IN(z0))
F4_IN(z0) → c5(U3'(f6_in(z0), f7_in(z0), z0), F7_IN(z0))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f7_in, U2, f4_in, U3
Defined Pair Symbols:
F1_IN, F7_IN, F4_IN
Compound Symbols:
c, c3, c5
(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0) → U1(f4_in(z0), z0)
U1(f4_out1, z0) → f1_out1
U1(f4_out2, z0) → f1_out1
f7_in(g(z0)) → U2(f1_in(z0), g(z0))
U2(f1_out1, g(z0)) → f7_out1
f4_in(z0) → U3(f6_in(z0), f7_in(z0), z0)
U3(f6_out1, z0, z1) → f4_out1
U3(z0, f7_out1, z1) → f4_out2
Tuples:
F1_IN(z0) → c(F4_IN(z0))
F7_IN(g(z0)) → c3(F1_IN(z0))
F4_IN(z0) → c5(F7_IN(z0))
S tuples:
F1_IN(z0) → c(F4_IN(z0))
F7_IN(g(z0)) → c3(F1_IN(z0))
F4_IN(z0) → c5(F7_IN(z0))
K tuples:none
Defined Rule Symbols:
f1_in, U1, f7_in, U2, f4_in, U3
Defined Pair Symbols:
F1_IN, F7_IN, F4_IN
Compound Symbols:
c, c3, c5
(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.
F7_IN(g(z0)) → c3(F1_IN(z0))
F4_IN(z0) → c5(F7_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(z0) → c(F4_IN(z0))
F7_IN(g(z0)) → c3(F1_IN(z0))
F4_IN(z0) → c5(F7_IN(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F1_IN(x1)) = [1] + x1
POL(F4_IN(x1)) = [1] + x1
POL(F7_IN(x1)) = x1
POL(c(x1)) = x1
POL(c3(x1)) = x1
POL(c5(x1)) = x1
POL(g(x1)) = [2] + x1
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(z0) → U1(f4_in(z0), z0)
U1(f4_out1, z0) → f1_out1
U1(f4_out2, z0) → f1_out1
f7_in(g(z0)) → U2(f1_in(z0), g(z0))
U2(f1_out1, g(z0)) → f7_out1
f4_in(z0) → U3(f6_in(z0), f7_in(z0), z0)
U3(f6_out1, z0, z1) → f4_out1
U3(z0, f7_out1, z1) → f4_out2
Tuples:
F1_IN(z0) → c(F4_IN(z0))
F7_IN(g(z0)) → c3(F1_IN(z0))
F4_IN(z0) → c5(F7_IN(z0))
S tuples:
F1_IN(z0) → c(F4_IN(z0))
K tuples:
F7_IN(g(z0)) → c3(F1_IN(z0))
F4_IN(z0) → c5(F7_IN(z0))
Defined Rule Symbols:
f1_in, U1, f7_in, U2, f4_in, U3
Defined Pair Symbols:
F1_IN, F7_IN, F4_IN
Compound Symbols:
c, c3, c5
(9) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(g(z0)) → U1(f2_in(z0), g(z0))
U1(f2_out1, g(z0)) → f2_out1
Tuples:
F2_IN(g(z0)) → c(U1'(f2_in(z0), g(z0)), F2_IN(z0))
S tuples:
F2_IN(g(z0)) → c(U1'(f2_in(z0), g(z0)), F2_IN(z0))
K tuples:none
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c
(11) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(g(z0)) → U1(f2_in(z0), g(z0))
U1(f2_out1, g(z0)) → f2_out1
Tuples:
F2_IN(g(z0)) → c(F2_IN(z0))
S tuples:
F2_IN(g(z0)) → c(F2_IN(z0))
K tuples:none
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c
(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(g(z0)) → c(F2_IN(z0))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(g(z0)) → c(F2_IN(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(F2_IN(x1)) = x1
POL(c(x1)) = x1
POL(g(x1)) = [1] + x1
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(g(z0)) → U1(f2_in(z0), g(z0))
U1(f2_out1, g(z0)) → f2_out1
Tuples:
F2_IN(g(z0)) → c(F2_IN(z0))
S tuples:none
K tuples:
F2_IN(g(z0)) → c(F2_IN(z0))
Defined Rule Symbols:
f2_in, U1
Defined Pair Symbols:
F2_IN
Compound Symbols:
c
(15) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(16) BOUNDS(O(1), O(1))