(0) Obligation:
Clauses:add(X, 0, X) :- !.
add(X, Y, s(Z)) :- ','(p(Y, P), add(X, P, Z)).
p(0, 0).
p(s(X), X).
Queries:
add(a,g,a).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:add12(T24, s(T25)) :- add12(T24, T25).
add1(T12, 0, s(T13)) :- add12(T12, T13).
add1(T12, s(T32), s(T13)) :- add1(T12, T32, T13).
Clauses:
addc12(T17, T17).
addc12(T24, s(T25)) :- addc12(T24, T25).
addc1(T5, 0, T5).
addc1(T12, 0, s(T13)) :- addc12(T12, T13).
addc1(T12, s(T32), s(T13)) :- addc1(T12, T32, T13).
Afs:
add1(x1, x2, x3) = add1(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:add1_in: (f,b,f)
add12_in: (f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
ADD1_IN_AGA(T12, 0, s(T13)) → U2_AGA(T12, T13, add12_in_aa(T12, T13))
ADD1_IN_AGA(T12, 0, s(T13)) → ADD12_IN_AA(T12, T13)
ADD12_IN_AA(T24, s(T25)) → U1_AA(T24, T25, add12_in_aa(T24, T25))
ADD12_IN_AA(T24, s(T25)) → ADD12_IN_AA(T24, T25)
ADD1_IN_AGA(T12, s(T32), s(T13)) → U3_AGA(T12, T32, T13, add1_in_aga(T12, T32, T13))
ADD1_IN_AGA(T12, s(T32), s(T13)) → ADD1_IN_AGA(T12, T32, T13)
R is empty.
The argument filtering Pi contains the following mapping:
add1_in_aga(x1, x2, x3) = add1_in_aga(x2)
0 = 0
add12_in_aa(x1, x2) = add12_in_aa
s(x1) = s(x1)
ADD1_IN_AGA(x1, x2, x3) = ADD1_IN_AGA(x2)
U2_AGA(x1, x2, x3) = U2_AGA(x3)
ADD12_IN_AA(x1, x2) = ADD12_IN_AA
U1_AA(x1, x2, x3) = U1_AA(x3)
U3_AGA(x1, x2, x3, x4) = U3_AGA(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:
ADD1_IN_AGA(T12, 0, s(T13)) → U2_AGA(T12, T13, add12_in_aa(T12, T13))
ADD1_IN_AGA(T12, 0, s(T13)) → ADD12_IN_AA(T12, T13)
ADD12_IN_AA(T24, s(T25)) → U1_AA(T24, T25, add12_in_aa(T24, T25))
ADD12_IN_AA(T24, s(T25)) → ADD12_IN_AA(T24, T25)
ADD1_IN_AGA(T12, s(T32), s(T13)) → U3_AGA(T12, T32, T13, add1_in_aga(T12, T32, T13))
ADD1_IN_AGA(T12, s(T32), s(T13)) → ADD1_IN_AGA(T12, T32, T13)
R is empty.
The argument filtering Pi contains the following mapping:
add1_in_aga(x1, x2, x3) = add1_in_aga(x2)
0 = 0
add12_in_aa(x1, x2) = add12_in_aa
s(x1) = s(x1)
ADD1_IN_AGA(x1, x2, x3) = ADD1_IN_AGA(x2)
U2_AGA(x1, x2, x3) = U2_AGA(x3)
ADD12_IN_AA(x1, x2) = ADD12_IN_AA
U1_AA(x1, x2, x3) = U1_AA(x3)
U3_AGA(x1, x2, x3, x4) = U3_AGA(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:
ADD12_IN_AA(T24, s(T25)) → ADD12_IN_AA(T24, T25)
R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
ADD12_IN_AA(x1, x2) = ADD12_IN_AA
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:
ADD12_IN_AA → ADD12_IN_AA
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 = ADD12_IN_AA evaluates to t =ADD12_IN_AA
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 ADD12_IN_AA to ADD12_IN_AA.
(11) NO
(12) Obligation:
Pi DP problem:The TRS P consists of the following rules:
ADD1_IN_AGA(T12, s(T32), s(T13)) → ADD1_IN_AGA(T12, T32, T13)
R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
ADD1_IN_AGA(x1, x2, x3) = ADD1_IN_AGA(x2)
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:
ADD1_IN_AGA(s(T32)) → ADD1_IN_AGA(T32)
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:
- ADD1_IN_AGA(s(T32)) → ADD1_IN_AGA(T32)
The graph contains the following edges 1 > 1