(0) Obligation:
Clauses:concatenate([], L, L).
concatenate(.(X, L1), L2, .(X, L3)) :- concatenate(L1, L2, L3).
member(X, .(X, L)).
member(X, .(Y, L)) :- member(X, L).
reverse(L, L1) :- reverse_concatenate(L, [], L1).
reverse_concatenate([], L, L).
reverse_concatenate(.(X, L1), L2, L3) :- reverse_concatenate(L1, .(X, L2), L3).
Queries:
reverse_concatenate(g,g,a).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:reverse_concatenate1(.(T37, .(T35, T36)), T38, T40) :- reverse_concatenate1(T36, .(T35, .(T37, T38)), T40).
Clauses:
reverse_concatenatec1([], T5, T5).
reverse_concatenatec1(.(T23, []), T24, .(T23, T24)).
reverse_concatenatec1(.(T37, .(T35, T36)), T38, T40) :- reverse_concatenatec1(T36, .(T35, .(T37, T38)), T40).
Afs:
reverse_concatenate1(x1, x2, x3) = reverse_concatenate1(x1, x2)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:reverse_concatenate1_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
REVERSE_CONCATENATE1_IN_GGA(.(T37, .(T35, T36)), T38, T40) → U1_GGA(T37, T35, T36, T38, T40, reverse_concatenate1_in_gga(T36, .(T35, .(T37, T38)), T40))
REVERSE_CONCATENATE1_IN_GGA(.(T37, .(T35, T36)), T38, T40) → REVERSE_CONCATENATE1_IN_GGA(T36, .(T35, .(T37, T38)), T40)
R is empty.
The argument filtering Pi contains the following mapping:
reverse_concatenate1_in_gga(x1, x2, x3) = reverse_concatenate1_in_gga(x1, x2)
.(x1, x2) = .(x1, x2)
REVERSE_CONCATENATE1_IN_GGA(x1, x2, x3) = REVERSE_CONCATENATE1_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4, x5, x6) = U1_GGA(x1, x2, x3, x4, x6)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:The TRS P consists of the following rules:
REVERSE_CONCATENATE1_IN_GGA(.(T37, .(T35, T36)), T38, T40) → U1_GGA(T37, T35, T36, T38, T40, reverse_concatenate1_in_gga(T36, .(T35, .(T37, T38)), T40))
REVERSE_CONCATENATE1_IN_GGA(.(T37, .(T35, T36)), T38, T40) → REVERSE_CONCATENATE1_IN_GGA(T36, .(T35, .(T37, T38)), T40)
R is empty.
The argument filtering Pi contains the following mapping:
reverse_concatenate1_in_gga(x1, x2, x3) = reverse_concatenate1_in_gga(x1, x2)
.(x1, x2) = .(x1, x2)
REVERSE_CONCATENATE1_IN_GGA(x1, x2, x3) = REVERSE_CONCATENATE1_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4, x5, x6) = U1_GGA(x1, x2, x3, x4, x6)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 1 less node.(6) Obligation:
Pi DP problem:The TRS P consists of the following rules:
REVERSE_CONCATENATE1_IN_GGA(.(T37, .(T35, T36)), T38, T40) → REVERSE_CONCATENATE1_IN_GGA(T36, .(T35, .(T37, T38)), T40)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
REVERSE_CONCATENATE1_IN_GGA(x1, x2, x3) = REVERSE_CONCATENATE1_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
(7) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(8) Obligation:
Q DP problem:The TRS P consists of the following rules:
REVERSE_CONCATENATE1_IN_GGA(.(T37, .(T35, T36)), T38) → REVERSE_CONCATENATE1_IN_GGA(T36, .(T35, .(T37, T38)))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(9) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.From the DPs we obtained the following set of size-change graphs:
- REVERSE_CONCATENATE1_IN_GGA(.(T37, .(T35, T36)), T38) → REVERSE_CONCATENATE1_IN_GGA(T36, .(T35, .(T37, T38)))
The graph contains the following edges 1 > 1