(0) Obligation:
Clauses:p(s(0), 0).
p(s(s(X)), s(s(Y))) :- p(s(X), s(Y)).
plus(0, Y, Y).
plus(s(X), Y, s(Z)) :- ','(p(s(X), U), plus(U, Y, Z)).
Queries:
plus(g,a,a).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:p23(s(T29), s(X53)) :- p23(T29, X53).
plus1(s(s(T23)), T12, s(T13)) :- p23(T23, X36).
plus1(s(s(T23)), T12, s(T13)) :- ','(pc23(T23, T25), plus1(s(s(T25)), T12, T13)).
Clauses:
plusc1(0, T5, T5).
plusc1(s(0), T20, s(T20)).
plusc1(s(s(T23)), T12, s(T13)) :- ','(pc23(T23, T25), plusc1(s(s(T25)), T12, T13)).
pc23(s(T29), s(X53)) :- pc23(T29, X53).
Afs:
plus1(x1, x2, x3) = plus1(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:plus1_in: (b,f,f)
p23_in: (b,f)
pc23_in: (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
PLUS1_IN_GAA(s(s(T23)), T12, s(T13)) → U2_GAA(T23, T12, T13, p23_in_ga(T23, X36))
PLUS1_IN_GAA(s(s(T23)), T12, s(T13)) → P23_IN_GA(T23, X36)
P23_IN_GA(s(T29), s(X53)) → U1_GA(T29, X53, p23_in_ga(T29, X53))
P23_IN_GA(s(T29), s(X53)) → P23_IN_GA(T29, X53)
PLUS1_IN_GAA(s(s(T23)), T12, s(T13)) → U3_GAA(T23, T12, T13, pc23_in_ga(T23, T25))
U3_GAA(T23, T12, T13, pc23_out_ga(T23, T25)) → U4_GAA(T23, T12, T13, plus1_in_gaa(s(s(T25)), T12, T13))
U3_GAA(T23, T12, T13, pc23_out_ga(T23, T25)) → PLUS1_IN_GAA(s(s(T25)), T12, T13)
The TRS R consists of the following rules:
pc23_in_ga(s(T29), s(X53)) → U8_ga(T29, X53, pc23_in_ga(T29, X53))
U8_ga(T29, X53, pc23_out_ga(T29, X53)) → pc23_out_ga(s(T29), s(X53))
The argument filtering Pi contains the following mapping:
plus1_in_gaa(x1, x2, x3) = plus1_in_gaa(x1)
s(x1) = s(x1)
p23_in_ga(x1, x2) = p23_in_ga(x1)
pc23_in_ga(x1, x2) = pc23_in_ga(x1)
U8_ga(x1, x2, x3) = U8_ga(x1, x3)
pc23_out_ga(x1, x2) = pc23_out_ga(x1, x2)
PLUS1_IN_GAA(x1, x2, x3) = PLUS1_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)
P23_IN_GA(x1, x2) = P23_IN_GA(x1)
U1_GA(x1, x2, x3) = U1_GA(x1, x3)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x1, x4)
U4_GAA(x1, x2, x3, x4) = U4_GAA(x1, 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:
PLUS1_IN_GAA(s(s(T23)), T12, s(T13)) → U2_GAA(T23, T12, T13, p23_in_ga(T23, X36))
PLUS1_IN_GAA(s(s(T23)), T12, s(T13)) → P23_IN_GA(T23, X36)
P23_IN_GA(s(T29), s(X53)) → U1_GA(T29, X53, p23_in_ga(T29, X53))
P23_IN_GA(s(T29), s(X53)) → P23_IN_GA(T29, X53)
PLUS1_IN_GAA(s(s(T23)), T12, s(T13)) → U3_GAA(T23, T12, T13, pc23_in_ga(T23, T25))
U3_GAA(T23, T12, T13, pc23_out_ga(T23, T25)) → U4_GAA(T23, T12, T13, plus1_in_gaa(s(s(T25)), T12, T13))
U3_GAA(T23, T12, T13, pc23_out_ga(T23, T25)) → PLUS1_IN_GAA(s(s(T25)), T12, T13)
The TRS R consists of the following rules:
pc23_in_ga(s(T29), s(X53)) → U8_ga(T29, X53, pc23_in_ga(T29, X53))
U8_ga(T29, X53, pc23_out_ga(T29, X53)) → pc23_out_ga(s(T29), s(X53))
The argument filtering Pi contains the following mapping:
plus1_in_gaa(x1, x2, x3) = plus1_in_gaa(x1)
s(x1) = s(x1)
p23_in_ga(x1, x2) = p23_in_ga(x1)
pc23_in_ga(x1, x2) = pc23_in_ga(x1)
U8_ga(x1, x2, x3) = U8_ga(x1, x3)
pc23_out_ga(x1, x2) = pc23_out_ga(x1, x2)
PLUS1_IN_GAA(x1, x2, x3) = PLUS1_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4) = U2_GAA(x1, x4)
P23_IN_GA(x1, x2) = P23_IN_GA(x1)
U1_GA(x1, x2, x3) = U1_GA(x1, x3)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x1, x4)
U4_GAA(x1, x2, x3, x4) = U4_GAA(x1, 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:
P23_IN_GA(s(T29), s(X53)) → P23_IN_GA(T29, X53)
The TRS R consists of the following rules:
pc23_in_ga(s(T29), s(X53)) → U8_ga(T29, X53, pc23_in_ga(T29, X53))
U8_ga(T29, X53, pc23_out_ga(T29, X53)) → pc23_out_ga(s(T29), s(X53))
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
pc23_in_ga(x1, x2) = pc23_in_ga(x1)
U8_ga(x1, x2, x3) = U8_ga(x1, x3)
pc23_out_ga(x1, x2) = pc23_out_ga(x1, x2)
P23_IN_GA(x1, x2) = P23_IN_GA(x1)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(9) Obligation:
Pi DP problem:The TRS P consists of the following rules:
P23_IN_GA(s(T29), s(X53)) → P23_IN_GA(T29, X53)
R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
P23_IN_GA(x1, x2) = P23_IN_GA(x1)
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(11) Obligation:
Q DP problem:The TRS P consists of the following rules:
P23_IN_GA(s(T29)) → P23_IN_GA(T29)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) 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:
- P23_IN_GA(s(T29)) → P23_IN_GA(T29)
The graph contains the following edges 1 > 1
(13) YES
(14) Obligation:
Pi DP problem:The TRS P consists of the following rules:
PLUS1_IN_GAA(s(s(T23)), T12, s(T13)) → U3_GAA(T23, T12, T13, pc23_in_ga(T23, T25))
U3_GAA(T23, T12, T13, pc23_out_ga(T23, T25)) → PLUS1_IN_GAA(s(s(T25)), T12, T13)
The TRS R consists of the following rules:
pc23_in_ga(s(T29), s(X53)) → U8_ga(T29, X53, pc23_in_ga(T29, X53))
U8_ga(T29, X53, pc23_out_ga(T29, X53)) → pc23_out_ga(s(T29), s(X53))
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
pc23_in_ga(x1, x2) = pc23_in_ga(x1)
U8_ga(x1, x2, x3) = U8_ga(x1, x3)
pc23_out_ga(x1, x2) = pc23_out_ga(x1, x2)
PLUS1_IN_GAA(x1, x2, x3) = PLUS1_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4) = U3_GAA(x1, x4)
We have to consider all (P,R,Pi)-chains
(15) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(16) Obligation:
Q DP problem:The TRS P consists of the following rules:
PLUS1_IN_GAA(s(s(T23))) → U3_GAA(T23, pc23_in_ga(T23))
U3_GAA(T23, pc23_out_ga(T23, T25)) → PLUS1_IN_GAA(s(s(T25)))
The TRS R consists of the following rules:
pc23_in_ga(s(T29)) → U8_ga(T29, pc23_in_ga(T29))
U8_ga(T29, pc23_out_ga(T29, X53)) → pc23_out_ga(s(T29), s(X53))
The set Q consists of the following terms:
pc23_in_ga(x0)
U8_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(17) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS1_IN_GAA(s(s(T23))) → U3_GAA(T23, pc23_in_ga(T23))
Used ordering: Polynomial interpretation [POLO]:
POL(PLUS1_IN_GAA(x1)) = 1 + x1
POL(U3_GAA(x1, x2)) = x2
POL(U8_ga(x1, x2)) = x2
POL(pc23_in_ga(x1)) = x1
POL(pc23_out_ga(x1, x2)) = 1 + x2
POL(s(x1)) = x1
The following usable rules [FROCOS05] were oriented:
pc23_in_ga(s(T29)) → U8_ga(T29, pc23_in_ga(T29))
U8_ga(T29, pc23_out_ga(T29, X53)) → pc23_out_ga(s(T29), s(X53))
(18) Obligation:
Q DP problem:The TRS P consists of the following rules:
U3_GAA(T23, pc23_out_ga(T23, T25)) → PLUS1_IN_GAA(s(s(T25)))
The TRS R consists of the following rules:
pc23_in_ga(s(T29)) → U8_ga(T29, pc23_in_ga(T29))
U8_ga(T29, pc23_out_ga(T29, X53)) → pc23_out_ga(s(T29), s(X53))
The set Q consists of the following terms:
pc23_in_ga(x0)
U8_ga(x0, x1)
We have to consider all (P,Q,R)-chains.