(0) Obligation:

Clauses:

mult(X1, 0, 0).
mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z)).
sum(X, 0, X).
sum(X, s(Y), s(Z)) :- sum(X, Y, Z).

Queries:

mult(g,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

sum12(s(T23), s(T25)) :- sum12(T23, T25).
mult24(T46, s(T47), X86) :- mult24(T46, T47, X85).
mult24(T46, s(T47), X86) :- ','(multc24(T46, T47, T50), sum35(T50, T46, X86)).
sum35(T64, s(T65), s(X113)) :- sum35(T64, T65, X113).
sum45(T86, s(T87), s(T89)) :- sum45(T86, T87, T89).
mult1(T18, s(0), T13) :- sum12(T18, T13).
mult1(T30, s(s(T31)), T13) :- mult24(T30, T31, X58).
mult1(T30, s(s(T31)), T13) :- ','(multc24(T30, T31, T34), sum35(T34, T30, X59)).
mult1(T30, s(s(T31)), T13) :- ','(multc24(T30, T31, T34), ','(sumc35(T34, T30, T70), sum45(T70, T30, T13))).

Clauses:

sumc12(0, 0).
sumc12(s(T23), s(T25)) :- sumc12(T23, T25).
multc24(T41, 0, 0).
multc24(T46, s(T47), X86) :- ','(multc24(T46, T47, T50), sumc35(T50, T46, X86)).
sumc35(T59, 0, T59).
sumc35(T64, s(T65), s(X113)) :- sumc35(T64, T65, X113).
sumc45(T79, 0, T79).
sumc45(T86, s(T87), s(T89)) :- sumc45(T86, T87, T89).

Afs:

mult1(x1, x2, x3)  =  mult1(x1, 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:
mult1_in: (b,b,f)
sum12_in: (b,f)
mult24_in: (b,b,f)
multc24_in: (b,b,f)
sumc35_in: (b,b,f)
sum35_in: (b,b,f)
sum45_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

MULT1_IN_GGA(T18, s(0), T13) → U7_GGA(T18, T13, sum12_in_ga(T18, T13))
MULT1_IN_GGA(T18, s(0), T13) → SUM12_IN_GA(T18, T13)
SUM12_IN_GA(s(T23), s(T25)) → U1_GA(T23, T25, sum12_in_ga(T23, T25))
SUM12_IN_GA(s(T23), s(T25)) → SUM12_IN_GA(T23, T25)
MULT1_IN_GGA(T30, s(s(T31)), T13) → U8_GGA(T30, T31, T13, mult24_in_gga(T30, T31, X58))
MULT1_IN_GGA(T30, s(s(T31)), T13) → MULT24_IN_GGA(T30, T31, X58)
MULT24_IN_GGA(T46, s(T47), X86) → U2_GGA(T46, T47, X86, mult24_in_gga(T46, T47, X85))
MULT24_IN_GGA(T46, s(T47), X86) → MULT24_IN_GGA(T46, T47, X85)
MULT24_IN_GGA(T46, s(T47), X86) → U3_GGA(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U3_GGA(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U4_GGA(T46, T47, X86, sum35_in_gga(T50, T46, X86))
U3_GGA(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → SUM35_IN_GGA(T50, T46, X86)
SUM35_IN_GGA(T64, s(T65), s(X113)) → U5_GGA(T64, T65, X113, sum35_in_gga(T64, T65, X113))
SUM35_IN_GGA(T64, s(T65), s(X113)) → SUM35_IN_GGA(T64, T65, X113)
MULT1_IN_GGA(T30, s(s(T31)), T13) → U9_GGA(T30, T31, T13, multc24_in_gga(T30, T31, T34))
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → U10_GGA(T30, T31, T13, sum35_in_gga(T34, T30, X59))
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → SUM35_IN_GGA(T34, T30, X59)
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → U11_GGA(T30, T31, T13, sumc35_in_gga(T34, T30, T70))
U11_GGA(T30, T31, T13, sumc35_out_gga(T34, T30, T70)) → U12_GGA(T30, T31, T13, sum45_in_gga(T70, T30, T13))
U11_GGA(T30, T31, T13, sumc35_out_gga(T34, T30, T70)) → SUM45_IN_GGA(T70, T30, T13)
SUM45_IN_GGA(T86, s(T87), s(T89)) → U6_GGA(T86, T87, T89, sum45_in_gga(T86, T87, T89))
SUM45_IN_GGA(T86, s(T87), s(T89)) → SUM45_IN_GGA(T86, T87, T89)

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
sum35_in_gga(x1, x2, x3)  =  sum35_in_gga(x1, x2)
sum45_in_gga(x1, x2, x3)  =  sum45_in_gga(x1, x2)
MULT1_IN_GGA(x1, x2, x3)  =  MULT1_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
SUM12_IN_GA(x1, x2)  =  SUM12_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
MULT24_IN_GGA(x1, x2, x3)  =  MULT24_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
SUM35_IN_GGA(x1, x2, x3)  =  SUM35_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
SUM45_IN_GGA(x1, x2, x3)  =  SUM45_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(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:

MULT1_IN_GGA(T18, s(0), T13) → U7_GGA(T18, T13, sum12_in_ga(T18, T13))
MULT1_IN_GGA(T18, s(0), T13) → SUM12_IN_GA(T18, T13)
SUM12_IN_GA(s(T23), s(T25)) → U1_GA(T23, T25, sum12_in_ga(T23, T25))
SUM12_IN_GA(s(T23), s(T25)) → SUM12_IN_GA(T23, T25)
MULT1_IN_GGA(T30, s(s(T31)), T13) → U8_GGA(T30, T31, T13, mult24_in_gga(T30, T31, X58))
MULT1_IN_GGA(T30, s(s(T31)), T13) → MULT24_IN_GGA(T30, T31, X58)
MULT24_IN_GGA(T46, s(T47), X86) → U2_GGA(T46, T47, X86, mult24_in_gga(T46, T47, X85))
MULT24_IN_GGA(T46, s(T47), X86) → MULT24_IN_GGA(T46, T47, X85)
MULT24_IN_GGA(T46, s(T47), X86) → U3_GGA(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U3_GGA(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U4_GGA(T46, T47, X86, sum35_in_gga(T50, T46, X86))
U3_GGA(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → SUM35_IN_GGA(T50, T46, X86)
SUM35_IN_GGA(T64, s(T65), s(X113)) → U5_GGA(T64, T65, X113, sum35_in_gga(T64, T65, X113))
SUM35_IN_GGA(T64, s(T65), s(X113)) → SUM35_IN_GGA(T64, T65, X113)
MULT1_IN_GGA(T30, s(s(T31)), T13) → U9_GGA(T30, T31, T13, multc24_in_gga(T30, T31, T34))
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → U10_GGA(T30, T31, T13, sum35_in_gga(T34, T30, X59))
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → SUM35_IN_GGA(T34, T30, X59)
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → U11_GGA(T30, T31, T13, sumc35_in_gga(T34, T30, T70))
U11_GGA(T30, T31, T13, sumc35_out_gga(T34, T30, T70)) → U12_GGA(T30, T31, T13, sum45_in_gga(T70, T30, T13))
U11_GGA(T30, T31, T13, sumc35_out_gga(T34, T30, T70)) → SUM45_IN_GGA(T70, T30, T13)
SUM45_IN_GGA(T86, s(T87), s(T89)) → U6_GGA(T86, T87, T89, sum45_in_gga(T86, T87, T89))
SUM45_IN_GGA(T86, s(T87), s(T89)) → SUM45_IN_GGA(T86, T87, T89)

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
sum35_in_gga(x1, x2, x3)  =  sum35_in_gga(x1, x2)
sum45_in_gga(x1, x2, x3)  =  sum45_in_gga(x1, x2)
MULT1_IN_GGA(x1, x2, x3)  =  MULT1_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
SUM12_IN_GA(x1, x2)  =  SUM12_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
MULT24_IN_GGA(x1, x2, x3)  =  MULT24_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
SUM35_IN_GGA(x1, x2, x3)  =  SUM35_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
SUM45_IN_GGA(x1, x2, x3)  =  SUM45_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 17 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUM45_IN_GGA(T86, s(T87), s(T89)) → SUM45_IN_GGA(T86, T87, T89)

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
SUM45_IN_GGA(x1, x2, x3)  =  SUM45_IN_GGA(x1, x2)

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:

SUM45_IN_GGA(T86, s(T87), s(T89)) → SUM45_IN_GGA(T86, T87, T89)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUM45_IN_GGA(x1, x2, x3)  =  SUM45_IN_GGA(x1, x2)

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:

SUM45_IN_GGA(T86, s(T87)) → SUM45_IN_GGA(T86, T87)

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:

  • SUM45_IN_GGA(T86, s(T87)) → SUM45_IN_GGA(T86, T87)
    The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUM35_IN_GGA(T64, s(T65), s(X113)) → SUM35_IN_GGA(T64, T65, X113)

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
SUM35_IN_GGA(x1, x2, x3)  =  SUM35_IN_GGA(x1, x2)

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:

SUM35_IN_GGA(T64, s(T65), s(X113)) → SUM35_IN_GGA(T64, T65, X113)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUM35_IN_GGA(x1, x2, x3)  =  SUM35_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND 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:

SUM35_IN_GGA(T64, s(T65)) → SUM35_IN_GGA(T64, T65)

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:

  • SUM35_IN_GGA(T64, s(T65)) → SUM35_IN_GGA(T64, T65)
    The graph contains the following edges 1 >= 1, 2 > 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULT24_IN_GGA(T46, s(T47), X86) → MULT24_IN_GGA(T46, T47, X85)

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
MULT24_IN_GGA(x1, x2, x3)  =  MULT24_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULT24_IN_GGA(T46, s(T47), X86) → MULT24_IN_GGA(T46, T47, X85)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULT24_IN_GGA(x1, x2, x3)  =  MULT24_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULT24_IN_GGA(T46, s(T47)) → MULT24_IN_GGA(T46, T47)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) 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:

  • MULT24_IN_GGA(T46, s(T47)) → MULT24_IN_GGA(T46, T47)
    The graph contains the following edges 1 >= 1, 2 > 2

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUM12_IN_GA(s(T23), s(T25)) → SUM12_IN_GA(T23, T25)

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
SUM12_IN_GA(x1, x2)  =  SUM12_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUM12_IN_GA(s(T23), s(T25)) → SUM12_IN_GA(T23, T25)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUM12_IN_GA(x1, x2)  =  SUM12_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM12_IN_GA(s(T23)) → SUM12_IN_GA(T23)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) 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:

  • SUM12_IN_GA(s(T23)) → SUM12_IN_GA(T23)
    The graph contains the following edges 1 > 1

(34) YES