(0) Obligation:
Clauses:f(c(s(X), Y)) :- f(c(X, s(Y))).
g(c(X, s(Y))) :- g(c(s(X), Y)).
h(X) :- ','(f(X), g(X)).
Queries:
h(g).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:f7(s(T18), T19) :- f7(T18, s(T19)).
g8(T28, s(T29)) :- g8(s(T28), T29).
h1(c(s(T8), T9)) :- f7(T8, T9).
h1(c(s(T8), T9)) :- ','(fc7(T8, T9), g8(T8, T9)).
Clauses:
fc7(s(T18), T19) :- fc7(T18, s(T19)).
gc8(T28, s(T29)) :- gc8(s(T28), T29).
Afs:
h1(x1) = h1(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:h1_in: (b)
f7_in: (b,b)
fc7_in: (b,b)
g8_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
H1_IN_G(c(s(T8), T9)) → U3_G(T8, T9, f7_in_gg(T8, T9))
H1_IN_G(c(s(T8), T9)) → F7_IN_GG(T8, T9)
F7_IN_GG(s(T18), T19) → U1_GG(T18, T19, f7_in_gg(T18, s(T19)))
F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))
H1_IN_G(c(s(T8), T9)) → U4_G(T8, T9, fc7_in_gg(T8, T9))
U4_G(T8, T9, fc7_out_gg(T8, T9)) → U5_G(T8, T9, g8_in_gg(T8, T9))
U4_G(T8, T9, fc7_out_gg(T8, T9)) → G8_IN_GG(T8, T9)
G8_IN_GG(T28, s(T29)) → U2_GG(T28, T29, g8_in_gg(s(T28), T29))
G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), T29)
The TRS R consists of the following rules:
fc7_in_gg(s(T18), T19) → U7_gg(T18, T19, fc7_in_gg(T18, s(T19)))
U7_gg(T18, T19, fc7_out_gg(T18, s(T19))) → fc7_out_gg(s(T18), T19)
Pi is empty.
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:
H1_IN_G(c(s(T8), T9)) → U3_G(T8, T9, f7_in_gg(T8, T9))
H1_IN_G(c(s(T8), T9)) → F7_IN_GG(T8, T9)
F7_IN_GG(s(T18), T19) → U1_GG(T18, T19, f7_in_gg(T18, s(T19)))
F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))
H1_IN_G(c(s(T8), T9)) → U4_G(T8, T9, fc7_in_gg(T8, T9))
U4_G(T8, T9, fc7_out_gg(T8, T9)) → U5_G(T8, T9, g8_in_gg(T8, T9))
U4_G(T8, T9, fc7_out_gg(T8, T9)) → G8_IN_GG(T8, T9)
G8_IN_GG(T28, s(T29)) → U2_GG(T28, T29, g8_in_gg(s(T28), T29))
G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), T29)
The TRS R consists of the following rules:
fc7_in_gg(s(T18), T19) → U7_gg(T18, T19, fc7_in_gg(T18, s(T19)))
U7_gg(T18, T19, fc7_out_gg(T18, s(T19))) → fc7_out_gg(s(T18), T19)
Pi is empty.
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 7 less nodes.(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:The TRS P consists of the following rules:
G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), T29)
The TRS R consists of the following rules:
fc7_in_gg(s(T18), T19) → U7_gg(T18, T19, fc7_in_gg(T18, s(T19)))
U7_gg(T18, T19, fc7_out_gg(T18, s(T19))) → fc7_out_gg(s(T18), T19)
Pi is empty.
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:
G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), T29)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (EQUIVALENT 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:
G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), 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:
- G8_IN_GG(T28, s(T29)) → G8_IN_GG(s(T28), T29)
The graph contains the following edges 2 > 2
(13) YES
(14) Obligation:
Pi DP problem:The TRS P consists of the following rules:
F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))
The TRS R consists of the following rules:
fc7_in_gg(s(T18), T19) → U7_gg(T18, T19, fc7_in_gg(T18, s(T19)))
U7_gg(T18, T19, fc7_out_gg(T18, s(T19))) → fc7_out_gg(s(T18), T19)
Pi is empty.
We have to consider all (P,R,Pi)-chains
(15) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(16) Obligation:
Pi DP problem:The TRS P consists of the following rules:
F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(18) Obligation:
Q DP problem:The TRS P consists of the following rules:
F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(19) 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:
- F7_IN_GG(s(T18), T19) → F7_IN_GG(T18, s(T19))
The graph contains the following edges 1 > 1