(0) Obligation:
Clauses:
q :- p(s(s(0))).
p(s(X)) :- p(X).
p(0).
p(s(s(s(0)))) :- p(s(s(s(0)))).
Query: q()
(1) LPReorderTransformerProof (EQUIVALENT transformation)
Reordered facts before rules in definite LP [PROLOG].
(2) Obligation:
Clauses:
p(0).
q :- p(s(s(0))).
p(s(X)) :- p(X).
p(s(s(s(0)))) :- p(s(s(s(0)))).
Query: q()
(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in → U1(f15_in)
U1(f15_out1) → f2_out1
U1(f15_out2) → f2_out1
f18_in → U2(f23_in)
U2(f23_out1) → f18_out1
U2(f23_out2) → f18_out1
f25_in → f25_out1
f15_in → U3(f18_in, f19_in)
U3(f18_out1, z0) → f15_out1
U3(z0, f19_out1) → f15_out2
f23_in → U4(f25_in, f27_in)
U4(f25_out1, z0) → f23_out1
U4(z0, f27_out1) → f23_out2
Tuples:
F2_IN → c(U1'(f15_in), F15_IN)
F18_IN → c3(U2'(f23_in), F23_IN)
F15_IN → c7(U3'(f18_in, f19_in), F18_IN)
F23_IN → c10(U4'(f25_in, f27_in), F25_IN)
S tuples:
F2_IN → c(U1'(f15_in), F15_IN)
F18_IN → c3(U2'(f23_in), F23_IN)
F15_IN → c7(U3'(f18_in, f19_in), F18_IN)
F23_IN → c10(U4'(f25_in, f27_in), F25_IN)
K tuples:none
Defined Rule Symbols:
f2_in, U1, f18_in, U2, f25_in, f15_in, U3, f23_in, U4
Defined Pair Symbols:
F2_IN, F18_IN, F15_IN, F23_IN
Compound Symbols:
c, c3, c7, c10
(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in → U1(f15_in)
U1(f15_out1) → f2_out1
U1(f15_out2) → f2_out1
f18_in → U2(f23_in)
U2(f23_out1) → f18_out1
U2(f23_out2) → f18_out1
f25_in → f25_out1
f15_in → U3(f18_in, f19_in)
U3(f18_out1, z0) → f15_out1
U3(z0, f19_out1) → f15_out2
f23_in → U4(f25_in, f27_in)
U4(f25_out1, z0) → f23_out1
U4(z0, f27_out1) → f23_out2
Tuples:
F2_IN → c1(U1'(f15_in))
F2_IN → c1(F15_IN)
F18_IN → c1(U2'(f23_in))
F18_IN → c1(F23_IN)
F15_IN → c1(U3'(f18_in, f19_in))
F15_IN → c1(F18_IN)
F23_IN → c1(U4'(f25_in, f27_in))
F23_IN → c1(F25_IN)
S tuples:
F2_IN → c1(U1'(f15_in))
F2_IN → c1(F15_IN)
F18_IN → c1(U2'(f23_in))
F18_IN → c1(F23_IN)
F15_IN → c1(U3'(f18_in, f19_in))
F15_IN → c1(F18_IN)
F23_IN → c1(U4'(f25_in, f27_in))
F23_IN → c1(F25_IN)
K tuples:none
Defined Rule Symbols:
f2_in, U1, f18_in, U2, f25_in, f15_in, U3, f23_in, U4
Defined Pair Symbols:
F2_IN, F18_IN, F15_IN, F23_IN
Compound Symbols:
c1
(7) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 5 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in → U1(f15_in)
U1(f15_out1) → f2_out1
U1(f15_out2) → f2_out1
f18_in → U2(f23_in)
U2(f23_out1) → f18_out1
U2(f23_out2) → f18_out1
f25_in → f25_out1
f15_in → U3(f18_in, f19_in)
U3(f18_out1, z0) → f15_out1
U3(z0, f19_out1) → f15_out2
f23_in → U4(f25_in, f27_in)
U4(f25_out1, z0) → f23_out1
U4(z0, f27_out1) → f23_out2
Tuples:
F2_IN → c1(F15_IN)
F18_IN → c1(F23_IN)
F15_IN → c1(F18_IN)
F2_IN → c1
F18_IN → c1
F15_IN → c1
F23_IN → c1
S tuples:
F2_IN → c1(F15_IN)
F18_IN → c1(F23_IN)
F15_IN → c1(F18_IN)
F2_IN → c1
F18_IN → c1
F15_IN → c1
F23_IN → c1
K tuples:none
Defined Rule Symbols:
f2_in, U1, f18_in, U2, f25_in, f15_in, U3, f23_in, U4
Defined Pair Symbols:
F2_IN, F18_IN, F15_IN, F23_IN
Compound Symbols:
c1, c1
(9) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F2_IN → c1(F15_IN)
F15_IN → c1(F18_IN)
F2_IN → c1
F18_IN → c1
F15_IN → c1
F15_IN → c1(F18_IN)
F15_IN → c1
F18_IN → c1(F23_IN)
F18_IN → c1
F23_IN → c1
F23_IN → c1
Now S is empty
(10) BOUNDS(O(1), O(1))
(11) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in → U1(f8_in)
U1(f8_out1) → f1_out1
U1(f8_out2) → f1_out1
f9_in → U2(f14_in)
U2(f14_out1) → f9_out1
U2(f14_out2) → f9_out1
f16_in → f16_out1
f8_in → U3(f9_in, f10_in)
U3(f9_out1, z0) → f8_out1
U3(z0, f10_out1) → f8_out2
f14_in → U4(f16_in, f17_in)
U4(f16_out1, z0) → f14_out1
U4(z0, f17_out1) → f14_out2
Tuples:
F1_IN → c(U1'(f8_in), F8_IN)
F9_IN → c3(U2'(f14_in), F14_IN)
F8_IN → c7(U3'(f9_in, f10_in), F9_IN)
F14_IN → c10(U4'(f16_in, f17_in), F16_IN)
S tuples:
F1_IN → c(U1'(f8_in), F8_IN)
F9_IN → c3(U2'(f14_in), F14_IN)
F8_IN → c7(U3'(f9_in, f10_in), F9_IN)
F14_IN → c10(U4'(f16_in, f17_in), F16_IN)
K tuples:none
Defined Rule Symbols:
f1_in, U1, f9_in, U2, f16_in, f8_in, U3, f14_in, U4
Defined Pair Symbols:
F1_IN, F9_IN, F8_IN, F14_IN
Compound Symbols:
c, c3, c7, c10
(13) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in → U1(f8_in)
U1(f8_out1) → f1_out1
U1(f8_out2) → f1_out1
f9_in → U2(f14_in)
U2(f14_out1) → f9_out1
U2(f14_out2) → f9_out1
f16_in → f16_out1
f8_in → U3(f9_in, f10_in)
U3(f9_out1, z0) → f8_out1
U3(z0, f10_out1) → f8_out2
f14_in → U4(f16_in, f17_in)
U4(f16_out1, z0) → f14_out1
U4(z0, f17_out1) → f14_out2
Tuples:
F1_IN → c1(U1'(f8_in))
F1_IN → c1(F8_IN)
F9_IN → c1(U2'(f14_in))
F9_IN → c1(F14_IN)
F8_IN → c1(U3'(f9_in, f10_in))
F8_IN → c1(F9_IN)
F14_IN → c1(U4'(f16_in, f17_in))
F14_IN → c1(F16_IN)
S tuples:
F1_IN → c1(U1'(f8_in))
F1_IN → c1(F8_IN)
F9_IN → c1(U2'(f14_in))
F9_IN → c1(F14_IN)
F8_IN → c1(U3'(f9_in, f10_in))
F8_IN → c1(F9_IN)
F14_IN → c1(U4'(f16_in, f17_in))
F14_IN → c1(F16_IN)
K tuples:none
Defined Rule Symbols:
f1_in, U1, f9_in, U2, f16_in, f8_in, U3, f14_in, U4
Defined Pair Symbols:
F1_IN, F9_IN, F8_IN, F14_IN
Compound Symbols:
c1
(15) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 5 trailing tuple parts
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in → U1(f8_in)
U1(f8_out1) → f1_out1
U1(f8_out2) → f1_out1
f9_in → U2(f14_in)
U2(f14_out1) → f9_out1
U2(f14_out2) → f9_out1
f16_in → f16_out1
f8_in → U3(f9_in, f10_in)
U3(f9_out1, z0) → f8_out1
U3(z0, f10_out1) → f8_out2
f14_in → U4(f16_in, f17_in)
U4(f16_out1, z0) → f14_out1
U4(z0, f17_out1) → f14_out2
Tuples:
F1_IN → c1(F8_IN)
F9_IN → c1(F14_IN)
F8_IN → c1(F9_IN)
F1_IN → c1
F9_IN → c1
F8_IN → c1
F14_IN → c1
S tuples:
F1_IN → c1(F8_IN)
F9_IN → c1(F14_IN)
F8_IN → c1(F9_IN)
F1_IN → c1
F9_IN → c1
F8_IN → c1
F14_IN → c1
K tuples:none
Defined Rule Symbols:
f1_in, U1, f9_in, U2, f16_in, f8_in, U3, f14_in, U4
Defined Pair Symbols:
F1_IN, F9_IN, F8_IN, F14_IN
Compound Symbols:
c1, c1