(0) Obligation:
Clauses:
gopher(nil, nil).
gopher(X, cons(nil, T)) :- ','(no(empty(X)), ','(head(X, nil), tail(X, T))).
gopher(X, Y) :- ','(no(empty(X)), ','(head(X, H), ','(no(empty(H)), ','(head(H, U), ','(tail(H, V), ','(tail(X, W), gopher(cons(U, cons(V, W)), Y))))))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, X), X).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).
Query: gopher(g,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(nil) → f2_out1
f2_in(.(nil, z0)) → f2_out1
f2_in(.(.(z0, z1), z2)) → U1(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
f2_in(.(.(z0, z1), z2)) → U2(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f2_out1, .(.(z0, z1), z2)) → f2_out1
U2(f2_out1, .(.(z0, z1), z2)) → f2_out1
Tuples:
F2_IN(.(.(z0, z1), z2)) → c2(U1'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F2_IN(cons(z0, cons(z1, z2))))
F2_IN(.(.(z0, z1), z2)) → c3(U2'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F2_IN(cons(z0, cons(z1, z2))))
S tuples:
F2_IN(.(.(z0, z1), z2)) → c2(U1'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F2_IN(cons(z0, cons(z1, z2))))
F2_IN(.(.(z0, z1), z2)) → c3(U2'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F2_IN(cons(z0, cons(z1, z2))))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2
Defined Pair Symbols:
F2_IN
Compound Symbols:
c2, c3
(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(nil) → f2_out1
f2_in(.(nil, z0)) → f2_out1
f2_in(.(.(z0, z1), z2)) → U1(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
f2_in(.(.(z0, z1), z2)) → U2(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f2_out1, .(.(z0, z1), z2)) → f2_out1
U2(f2_out1, .(.(z0, z1), z2)) → f2_out1
Tuples:
F2_IN(.(.(z0, z1), z2)) → c(U1'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
F2_IN(.(.(z0, z1), z2)) → c(F2_IN(cons(z0, cons(z1, z2))))
F2_IN(.(.(z0, z1), z2)) → c(U2'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
S tuples:
F2_IN(.(.(z0, z1), z2)) → c(U1'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
F2_IN(.(.(z0, z1), z2)) → c(F2_IN(cons(z0, cons(z1, z2))))
F2_IN(.(.(z0, z1), z2)) → c(U2'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2
Defined Pair Symbols:
F2_IN
Compound Symbols:
c
(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f2_in(nil) → f2_out1
f2_in(.(nil, z0)) → f2_out1
f2_in(.(.(z0, z1), z2)) → U1(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
f2_in(.(.(z0, z1), z2)) → U2(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f2_out1, .(.(z0, z1), z2)) → f2_out1
U2(f2_out1, .(.(z0, z1), z2)) → f2_out1
Tuples:
F2_IN(.(.(z0, z1), z2)) → c
S tuples:
F2_IN(.(.(z0, z1), z2)) → c
K tuples:none
Defined Rule Symbols:
f2_in, U1, U2
Defined Pair Symbols:
F2_IN
Compound Symbols:
c
(7) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
F2_IN(.(.(z0, z1), z2)) → c
F2_IN(.(.(z0, z1), z2)) → c
F2_IN(.(.(z0, z1), z2)) → c
F2_IN(.(.(z0, z1), z2)) → c
Now 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(nil) → f1_out1
f1_in(.(nil, z0)) → f1_out1
f1_in(.(.(z0, z1), z2)) → U1(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
f1_in(.(.(z0, z1), z2)) → U2(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f1_out1, .(.(z0, z1), z2)) → f1_out1
U2(f1_out1, .(.(z0, z1), z2)) → f1_out1
Tuples:
F1_IN(.(.(z0, z1), z2)) → c2(U1'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F1_IN(cons(z0, cons(z1, z2))))
F1_IN(.(.(z0, z1), z2)) → c3(U2'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F1_IN(cons(z0, cons(z1, z2))))
S tuples:
F1_IN(.(.(z0, z1), z2)) → c2(U1'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F1_IN(cons(z0, cons(z1, z2))))
F1_IN(.(.(z0, z1), z2)) → c3(U2'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F1_IN(cons(z0, cons(z1, z2))))
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2
Defined Pair Symbols:
F1_IN
Compound Symbols:
c2, c3
(11) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(nil) → f1_out1
f1_in(.(nil, z0)) → f1_out1
f1_in(.(.(z0, z1), z2)) → U1(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
f1_in(.(.(z0, z1), z2)) → U2(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f1_out1, .(.(z0, z1), z2)) → f1_out1
U2(f1_out1, .(.(z0, z1), z2)) → f1_out1
Tuples:
F1_IN(.(.(z0, z1), z2)) → c(U1'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
F1_IN(.(.(z0, z1), z2)) → c(F1_IN(cons(z0, cons(z1, z2))))
F1_IN(.(.(z0, z1), z2)) → c(U2'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
S tuples:
F1_IN(.(.(z0, z1), z2)) → c(U1'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
F1_IN(.(.(z0, z1), z2)) → c(F1_IN(cons(z0, cons(z1, z2))))
F1_IN(.(.(z0, z1), z2)) → c(U2'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2
Defined Pair Symbols:
F1_IN
Compound Symbols:
c
(13) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f1_in(nil) → f1_out1
f1_in(.(nil, z0)) → f1_out1
f1_in(.(.(z0, z1), z2)) → U1(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
f1_in(.(.(z0, z1), z2)) → U2(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f1_out1, .(.(z0, z1), z2)) → f1_out1
U2(f1_out1, .(.(z0, z1), z2)) → f1_out1
Tuples:
F1_IN(.(.(z0, z1), z2)) → c
S tuples:
F1_IN(.(.(z0, z1), z2)) → c
K tuples:none
Defined Rule Symbols:
f1_in, U1, U2
Defined Pair Symbols:
F1_IN
Compound Symbols:
c