(0) Obligation:
Clauses:
som3([], Bs, Bs).
som3(As, [], As).
som3(.(A, As), .(B, Bs), .(+(A, B), Cs)) :- som3(As, Bs, Cs).
som4_1(As, Bs, Cs, Ds) :- ','(som3(As, Bs, Es), som3(Es, Cs, Ds)).
som4_2(As, Bs, Cs, Ds) :- ','(som3(Es, Cs, Ds), som3(As, Bs, Es)).
Query: som3(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([]) → f2_out1
f2_in(z0) → f2_out1
f2_in(.(z0, z1)) → U1(f2_in(z1), .(z0, z1))
f2_in(.(z0, z1)) → U2(f2_in(z1), .(z0, z1))
U1(f2_out1, .(z0, z1)) → f2_out1
U2(f2_out1, .(z0, z1)) → f2_out1
Tuples:
F2_IN(.(z0, z1)) → c2(U1'(f2_in(z1), .(z0, z1)), F2_IN(z1))
F2_IN(.(z0, z1)) → c3(U2'(f2_in(z1), .(z0, z1)), F2_IN(z1))
S tuples:
F2_IN(.(z0, z1)) → c2(U1'(f2_in(z1), .(z0, z1)), F2_IN(z1))
F2_IN(.(z0, z1)) → c3(U2'(f2_in(z1), .(z0, z1)), F2_IN(z1))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2
Defined Pair Symbols:
F2_IN
Compound Symbols:
c2, c3
(3) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1
f2_in(z0) → f2_out1
f2_in(.(z0, z1)) → U1(f2_in(z1), .(z0, z1))
f2_in(.(z0, z1)) → U2(f2_in(z1), .(z0, z1))
U1(f2_out1, .(z0, z1)) → f2_out1
U2(f2_out1, .(z0, z1)) → f2_out1
Tuples:
F2_IN(.(z0, z1)) → c2(F2_IN(z1))
F2_IN(.(z0, z1)) → c3(F2_IN(z1))
S tuples:
F2_IN(.(z0, z1)) → c2(F2_IN(z1))
F2_IN(.(z0, z1)) → c3(F2_IN(z1))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2
Defined Pair Symbols:
F2_IN
Compound Symbols:
c2, c3
(5) 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(.(z0, z1)) → c2(F2_IN(z1))
F2_IN(.(z0, z1)) → c3(F2_IN(z1))
We considered the (Usable) Rules:none
And the Tuples:
F2_IN(.(z0, z1)) → c2(F2_IN(z1))
F2_IN(.(z0, z1)) → c3(F2_IN(z1))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [2] + x2
POL(F2_IN(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in([]) → f2_out1
f2_in(z0) → f2_out1
f2_in(.(z0, z1)) → U1(f2_in(z1), .(z0, z1))
f2_in(.(z0, z1)) → U2(f2_in(z1), .(z0, z1))
U1(f2_out1, .(z0, z1)) → f2_out1
U2(f2_out1, .(z0, z1)) → f2_out1
Tuples:
F2_IN(.(z0, z1)) → c2(F2_IN(z1))
F2_IN(.(z0, z1)) → c3(F2_IN(z1))
S tuples:none
K tuples:
F2_IN(.(z0, z1)) → c2(F2_IN(z1))
F2_IN(.(z0, z1)) → c3(F2_IN(z1))
Defined Rule Symbols:
f2_in, U1, U2
Defined Pair Symbols:
F2_IN
Compound Symbols:
c2, c3
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))
(9) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)
Built complexity over-approximating cdt problems from derivation graph.
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1
f1_in(z0) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, z1)) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U2(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U3(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U4(f1_in(z2), .(z0, .(z1, z2)))
U1(f1_out1, .(z0, .(z1, z2))) → f1_out1
U2(f1_out1, .(z0, .(z1, z2))) → f1_out1
U3(f1_out1, .(z0, .(z1, z2))) → f1_out1
U4(f1_out1, .(z0, .(z1, z2))) → f1_out1
Tuples:
F1_IN(.(z0, .(z1, z2))) → c4(U1'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(U2'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c6(U3'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c7(U4'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
S tuples:
F1_IN(.(z0, .(z1, z2))) → c4(U1'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(U2'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c6(U3'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c7(U4'(f1_in(z2), .(z0, .(z1, z2))), F1_IN(z2))
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, U3, U4
Defined Pair Symbols:
F1_IN
Compound Symbols:
c4, c5, c6, c7
(11) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1
f1_in(z0) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, z1)) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U2(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U3(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U4(f1_in(z2), .(z0, .(z1, z2)))
U1(f1_out1, .(z0, .(z1, z2))) → f1_out1
U2(f1_out1, .(z0, .(z1, z2))) → f1_out1
U3(f1_out1, .(z0, .(z1, z2))) → f1_out1
U4(f1_out1, .(z0, .(z1, z2))) → f1_out1
Tuples:
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c6(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c7(F1_IN(z2))
S tuples:
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c6(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c7(F1_IN(z2))
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2, U3, U4
Defined Pair Symbols:
F1_IN
Compound Symbols:
c4, c5, c6, c7
(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.
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c6(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c7(F1_IN(z2))
We considered the (Usable) Rules:none
And the Tuples:
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c6(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c7(F1_IN(z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(.(x1, x2)) = [1] + x2
POL(F1_IN(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c6(x1)) = x1
POL(c7(x1)) = x1
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in([]) → f1_out1
f1_in(z0) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, z1)) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U2(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U3(f1_in(z2), .(z0, .(z1, z2)))
f1_in(.(z0, .(z1, z2))) → U4(f1_in(z2), .(z0, .(z1, z2)))
U1(f1_out1, .(z0, .(z1, z2))) → f1_out1
U2(f1_out1, .(z0, .(z1, z2))) → f1_out1
U3(f1_out1, .(z0, .(z1, z2))) → f1_out1
U4(f1_out1, .(z0, .(z1, z2))) → f1_out1
Tuples:
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c6(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c7(F1_IN(z2))
S tuples:none
K tuples:
F1_IN(.(z0, .(z1, z2))) → c4(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c5(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c6(F1_IN(z2))
F1_IN(.(z0, .(z1, z2))) → c7(F1_IN(z2))
Defined Rule Symbols:
f1_in, U1, U2, U3, U4
Defined Pair Symbols:
F1_IN
Compound Symbols:
c4, c5, c6, c7