(0) Obligation:
Clauses:p(M, N, s(R), RES) :- p(M, R, N, RES).
p(M, s(N), R, RES) :- p(R, N, M, RES).
p(M, X1, X2, M).
Queries:
p(g,g,g,a).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:p1(T30, s(T32), s(T31), T34) :- p1(T30, T32, T31, T34).
p1(T55, T57, s(s(T56)), T59) :- p1(T57, T56, T55, T59).
p1(T95, s(T96), s(T97), T99) :- p1(s(T97), T96, T95, T99).
p1(s(T140), s(T139), T138, T142) :- p1(T138, T140, T139, T142).
p1(T165, s(s(T164)), T163, T167) :- p1(T165, T164, T163, T167).
Clauses:
pc1(T30, s(T32), s(T31), T34) :- pc1(T30, T32, T31, T34).
pc1(T55, T57, s(s(T56)), T59) :- pc1(T57, T56, T55, T59).
pc1(T76, T78, s(T77), T76).
pc1(T95, s(T96), s(T97), T99) :- pc1(s(T97), T96, T95, T99).
pc1(T110, T111, s(T112), T110).
pc1(s(T140), s(T139), T138, T142) :- pc1(T138, T140, T139, T142).
pc1(T165, s(s(T164)), T163, T167) :- pc1(T165, T164, T163, T167).
pc1(T186, s(T185), T184, T184).
pc1(T193, s(T194), T195, T193).
pc1(T199, T200, T201, T199).
Afs:
p1(x1, x2, x3, x4) = p1(x1, x2, x3)
(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:p1_in: (b,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
P1_IN_GGGA(T30, s(T32), s(T31), T34) → U1_GGGA(T30, T32, T31, T34, p1_in_ggga(T30, T32, T31, T34))
P1_IN_GGGA(T30, s(T32), s(T31), T34) → P1_IN_GGGA(T30, T32, T31, T34)
P1_IN_GGGA(T55, T57, s(s(T56)), T59) → U2_GGGA(T55, T57, T56, T59, p1_in_ggga(T57, T56, T55, T59))
P1_IN_GGGA(T55, T57, s(s(T56)), T59) → P1_IN_GGGA(T57, T56, T55, T59)
P1_IN_GGGA(T95, s(T96), s(T97), T99) → U3_GGGA(T95, T96, T97, T99, p1_in_ggga(s(T97), T96, T95, T99))
P1_IN_GGGA(T95, s(T96), s(T97), T99) → P1_IN_GGGA(s(T97), T96, T95, T99)
P1_IN_GGGA(s(T140), s(T139), T138, T142) → U4_GGGA(T140, T139, T138, T142, p1_in_ggga(T138, T140, T139, T142))
P1_IN_GGGA(s(T140), s(T139), T138, T142) → P1_IN_GGGA(T138, T140, T139, T142)
P1_IN_GGGA(T165, s(s(T164)), T163, T167) → U5_GGGA(T165, T164, T163, T167, p1_in_ggga(T165, T164, T163, T167))
P1_IN_GGGA(T165, s(s(T164)), T163, T167) → P1_IN_GGGA(T165, T164, T163, T167)
R is empty.
The argument filtering Pi contains the following mapping:
p1_in_ggga(x1, x2, x3, x4) = p1_in_ggga(x1, x2, x3)
s(x1) = s(x1)
P1_IN_GGGA(x1, x2, x3, x4) = P1_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5) = U1_GGGA(x1, x2, x3, x5)
U2_GGGA(x1, x2, x3, x4, x5) = U2_GGGA(x1, x2, x3, x5)
U3_GGGA(x1, x2, x3, x4, x5) = U3_GGGA(x1, x2, x3, x5)
U4_GGGA(x1, x2, x3, x4, x5) = U4_GGGA(x1, x2, x3, x5)
U5_GGGA(x1, x2, x3, x4, x5) = U5_GGGA(x1, x2, x3, x5)
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:
P1_IN_GGGA(T30, s(T32), s(T31), T34) → U1_GGGA(T30, T32, T31, T34, p1_in_ggga(T30, T32, T31, T34))
P1_IN_GGGA(T30, s(T32), s(T31), T34) → P1_IN_GGGA(T30, T32, T31, T34)
P1_IN_GGGA(T55, T57, s(s(T56)), T59) → U2_GGGA(T55, T57, T56, T59, p1_in_ggga(T57, T56, T55, T59))
P1_IN_GGGA(T55, T57, s(s(T56)), T59) → P1_IN_GGGA(T57, T56, T55, T59)
P1_IN_GGGA(T95, s(T96), s(T97), T99) → U3_GGGA(T95, T96, T97, T99, p1_in_ggga(s(T97), T96, T95, T99))
P1_IN_GGGA(T95, s(T96), s(T97), T99) → P1_IN_GGGA(s(T97), T96, T95, T99)
P1_IN_GGGA(s(T140), s(T139), T138, T142) → U4_GGGA(T140, T139, T138, T142, p1_in_ggga(T138, T140, T139, T142))
P1_IN_GGGA(s(T140), s(T139), T138, T142) → P1_IN_GGGA(T138, T140, T139, T142)
P1_IN_GGGA(T165, s(s(T164)), T163, T167) → U5_GGGA(T165, T164, T163, T167, p1_in_ggga(T165, T164, T163, T167))
P1_IN_GGGA(T165, s(s(T164)), T163, T167) → P1_IN_GGGA(T165, T164, T163, T167)
R is empty.
The argument filtering Pi contains the following mapping:
p1_in_ggga(x1, x2, x3, x4) = p1_in_ggga(x1, x2, x3)
s(x1) = s(x1)
P1_IN_GGGA(x1, x2, x3, x4) = P1_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5) = U1_GGGA(x1, x2, x3, x5)
U2_GGGA(x1, x2, x3, x4, x5) = U2_GGGA(x1, x2, x3, x5)
U3_GGGA(x1, x2, x3, x4, x5) = U3_GGGA(x1, x2, x3, x5)
U4_GGGA(x1, x2, x3, x4, x5) = U4_GGGA(x1, x2, x3, x5)
U5_GGGA(x1, x2, x3, x4, x5) = U5_GGGA(x1, x2, x3, x5)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 5 less nodes.(6) Obligation:
Pi DP problem:The TRS P consists of the following rules:
P1_IN_GGGA(T55, T57, s(s(T56)), T59) → P1_IN_GGGA(T57, T56, T55, T59)
P1_IN_GGGA(T30, s(T32), s(T31), T34) → P1_IN_GGGA(T30, T32, T31, T34)
P1_IN_GGGA(T95, s(T96), s(T97), T99) → P1_IN_GGGA(s(T97), T96, T95, T99)
P1_IN_GGGA(s(T140), s(T139), T138, T142) → P1_IN_GGGA(T138, T140, T139, T142)
P1_IN_GGGA(T165, s(s(T164)), T163, T167) → P1_IN_GGGA(T165, T164, T163, T167)
R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
P1_IN_GGGA(x1, x2, x3, x4) = P1_IN_GGGA(x1, x2, x3)
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:
P1_IN_GGGA(T55, T57, s(s(T56))) → P1_IN_GGGA(T57, T56, T55)
P1_IN_GGGA(T30, s(T32), s(T31)) → P1_IN_GGGA(T30, T32, T31)
P1_IN_GGGA(T95, s(T96), s(T97)) → P1_IN_GGGA(s(T97), T96, T95)
P1_IN_GGGA(s(T140), s(T139), T138) → P1_IN_GGGA(T138, T140, T139)
P1_IN_GGGA(T165, s(s(T164)), T163) → P1_IN_GGGA(T165, T164, T163)
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:
- P1_IN_GGGA(T55, T57, s(s(T56))) → P1_IN_GGGA(T57, T56, T55)
The graph contains the following edges 2 >= 1, 3 > 2, 1 >= 3 - P1_IN_GGGA(T30, s(T32), s(T31)) → P1_IN_GGGA(T30, T32, T31)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3 - P1_IN_GGGA(T95, s(T96), s(T97)) → P1_IN_GGGA(s(T97), T96, T95)
The graph contains the following edges 3 >= 1, 2 > 2, 1 >= 3 - P1_IN_GGGA(s(T140), s(T139), T138) → P1_IN_GGGA(T138, T140, T139)
The graph contains the following edges 3 >= 1, 1 > 2, 2 > 3 - P1_IN_GGGA(T165, s(s(T164)), T163) → P1_IN_GGGA(T165, T164, T163)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3