(0) Obligation:
Clauses:len([], 0) :- !.
len(Xs, s(N)) :- ','(tail(Xs, Ys), len(Ys, N)).
tail([], []).
tail(.(X, Xs), Xs).
Queries:
len(g,a).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:len12(s(T11)) :- len12(T11).
len1([], s(T7)) :- len12(T7).
len1(.(T16, T17), s(T7)) :- len1(T17, T7).
Clauses:
lenc12(0).
lenc12(s(T11)) :- lenc12(T11).
lenc1([], 0).
lenc1([], s(T7)) :- lenc12(T7).
lenc1(.(T16, T17), s(T7)) :- lenc1(T17, T7).
Afs:
len1(x1, x2) = len1(x1)
(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:len1_in: (b,f)
len12_in: (f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
LEN1_IN_GA([], s(T7)) → U2_GA(T7, len12_in_a(T7))
LEN1_IN_GA([], s(T7)) → LEN12_IN_A(T7)
LEN12_IN_A(s(T11)) → U1_A(T11, len12_in_a(T11))
LEN12_IN_A(s(T11)) → LEN12_IN_A(T11)
LEN1_IN_GA(.(T16, T17), s(T7)) → U3_GA(T16, T17, T7, len1_in_ga(T17, T7))
LEN1_IN_GA(.(T16, T17), s(T7)) → LEN1_IN_GA(T17, T7)
R is empty.
The argument filtering Pi contains the following mapping:
len1_in_ga(x1, x2) = len1_in_ga(x1)
[] = []
len12_in_a(x1) = len12_in_a
.(x1, x2) = .(x1, x2)
s(x1) = s(x1)
LEN1_IN_GA(x1, x2) = LEN1_IN_GA(x1)
U2_GA(x1, x2) = U2_GA(x2)
LEN12_IN_A(x1) = LEN12_IN_A
U1_A(x1, x2) = U1_A(x2)
U3_GA(x1, x2, x3, x4) = U3_GA(x1, x2, x4)
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:
LEN1_IN_GA([], s(T7)) → U2_GA(T7, len12_in_a(T7))
LEN1_IN_GA([], s(T7)) → LEN12_IN_A(T7)
LEN12_IN_A(s(T11)) → U1_A(T11, len12_in_a(T11))
LEN12_IN_A(s(T11)) → LEN12_IN_A(T11)
LEN1_IN_GA(.(T16, T17), s(T7)) → U3_GA(T16, T17, T7, len1_in_ga(T17, T7))
LEN1_IN_GA(.(T16, T17), s(T7)) → LEN1_IN_GA(T17, T7)
R is empty.
The argument filtering Pi contains the following mapping:
len1_in_ga(x1, x2) = len1_in_ga(x1)
[] = []
len12_in_a(x1) = len12_in_a
.(x1, x2) = .(x1, x2)
s(x1) = s(x1)
LEN1_IN_GA(x1, x2) = LEN1_IN_GA(x1)
U2_GA(x1, x2) = U2_GA(x2)
LEN12_IN_A(x1) = LEN12_IN_A
U1_A(x1, x2) = U1_A(x2)
U3_GA(x1, x2, x3, x4) = U3_GA(x1, x2, x4)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 4 less nodes.(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:The TRS P consists of the following rules:
LEN12_IN_A(s(T11)) → LEN12_IN_A(T11)
R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
LEN12_IN_A(x1) = LEN12_IN_A
We have to consider all (P,R,Pi)-chains
(8) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(9) Obligation:
Q DP problem:The TRS P consists of the following rules:
LEN12_IN_A → LEN12_IN_A
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(10) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.Found a loop by semiunifying a rule from P directly.
s = LEN12_IN_A evaluates to t =LEN12_IN_A
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from LEN12_IN_A to LEN12_IN_A.
(11) NO
(12) Obligation:
Pi DP problem:The TRS P consists of the following rules:
LEN1_IN_GA(.(T16, T17), s(T7)) → LEN1_IN_GA(T17, T7)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
s(x1) = s(x1)
LEN1_IN_GA(x1, x2) = LEN1_IN_GA(x1)
We have to consider all (P,R,Pi)-chains
(13) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(14) Obligation:
Q DP problem:The TRS P consists of the following rules:
LEN1_IN_GA(.(T16, T17)) → LEN1_IN_GA(T17)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(15) 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:
- LEN1_IN_GA(.(T16, T17)) → LEN1_IN_GA(T17)
The graph contains the following edges 1 > 1