(0) Obligation:

Clauses:

times(X, Y, Z) :- mult(X, Y, 0, Z).
mult(0, Y, 0, Z) :- ','(!, eq(Z, 0)).
mult(s(X), Y, 0, Z) :- ','(!, mult(X, Y, Y, Z)).
mult(X, Y, W, s(Z)) :- ','(p(W, P), mult(X, Y, P, Z)).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

times(g,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

mult29(s(T81), T83) :- mult29(T81, T83).
mult29(T89, s(T91)) :- mult29(T89, T91).
mult71(T148, s(T150)) :- mult79(T148, T150).
mult79(s(T169), T171) :- mult71(T169, T171).
mult79(T179, s(T181)) :- mult79(T179, T181).
mult121(T253, s(s(T255))) :- mult137(T253, T255).
mult137(s(T274), T276) :- mult121(T274, T276).
mult137(T284, s(T286)) :- mult137(T284, T286).
mult179(T373, s(s(s(T375)))) :- mult203(T373, T375).
mult203(s(T394), T396) :- mult179(T394, T396).
mult203(T404, s(T406)) :- mult203(T404, T406).
mult245(T508, s(s(s(s(T510))))) :- mult277(T508, T510).
mult277(s(T529), T531) :- mult245(T529, T531).
mult277(T539, s(T541)) :- mult277(T539, T541).
mult319(T658, s(s(s(s(s(T660)))))) :- mult359(T658, T660).
mult359(s(T679), T681) :- mult319(T679, T681).
mult359(T689, s(T691)) :- mult359(T689, T691).
mult401(T823, s(s(s(s(s(s(T825))))))) :- mult449(T823, T825).
mult449(s(T844), T846) :- mult401(T844, T846).
mult449(T854, s(T856)) :- mult449(T854, T856).
mult491(T1003, s(s(s(s(s(s(s(T1005)))))))) :- mult547(T1003, T1005).
mult547(s(T1024), T1026) :- mult491(T1024, T1026).
mult547(T1034, s(T1036)) :- mult547(T1034, T1036).
mult16(s(T61), 0, T64) :- mult29(T61, T64).
mult16(T102, 0, s(T105)) :- mult29(T102, T105).
mult16(s(T136), s(0), s(T139)) :- mult71(T136, T139).
mult16(T192, s(0), s(s(T195))) :- mult79(T192, T195).
mult16(s(T226), s(s(0)), s(s(T229))) :- mult121(T226, T229).
mult16(T297, s(s(0)), s(s(s(T300)))) :- mult137(T297, T300).
mult16(s(T331), s(s(s(0))), s(s(s(T334)))) :- mult179(T331, T334).
mult16(T417, s(s(s(0))), s(s(s(s(T420))))) :- mult203(T417, T420).
mult16(s(T451), s(s(s(s(0)))), s(s(s(s(T454))))) :- mult245(T451, T454).
mult16(T552, s(s(s(s(0)))), s(s(s(s(s(T555)))))) :- mult277(T552, T555).
mult16(s(T586), s(s(s(s(s(0))))), s(s(s(s(s(T589)))))) :- mult319(T586, T589).
mult16(T702, s(s(s(s(s(0))))), s(s(s(s(s(s(T705))))))) :- mult359(T702, T705).
mult16(s(T736), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T739))))))) :- mult401(T736, T739).
mult16(T867, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T870)))))))) :- mult449(T867, T870).
mult16(s(T901), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T904)))))))) :- mult491(T901, T904).
mult16(T1047, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T1050))))))))) :- mult547(T1047, T1050).
mult16(T1047, s(s(s(s(s(s(s(s(T1056)))))))), s(s(s(s(s(s(s(s(T1050))))))))) :- mult577(T1047, s(s(s(s(s(s(s(T1056))))))), T1056, T1050).
mult3(s(T33), T34, T36) :- mult16(T33, T34, T36).
mult3(T1122, T1123, s(T1125)) :- mult3(T1122, T1123, T1125).
mult577(s(T1084), T1085, 0, T1087) :- mult16(T1084, s(T1085), T1087).
mult577(T1102, T1103, 0, s(T1106)) :- mult3(T1102, s(T1103), T1106).
mult577(T1102, T1103, s(T1113), s(T1106)) :- mult577(T1102, T1103, T1113, T1106).
times1(T7, T8, T10) :- mult3(T7, T8, T10).

Clauses:

multc29(0, 0).
multc29(s(T81), T83) :- multc29(T81, T83).
multc29(T89, s(T91)) :- multc29(T89, T91).
multc71(T148, s(T150)) :- multc79(T148, T150).
multc79(0, 0).
multc79(s(T169), T171) :- multc71(T169, T171).
multc79(T179, s(T181)) :- multc79(T179, T181).
multc121(T253, s(s(T255))) :- multc137(T253, T255).
multc137(0, 0).
multc137(s(T274), T276) :- multc121(T274, T276).
multc137(T284, s(T286)) :- multc137(T284, T286).
multc179(T373, s(s(s(T375)))) :- multc203(T373, T375).
multc203(0, 0).
multc203(s(T394), T396) :- multc179(T394, T396).
multc203(T404, s(T406)) :- multc203(T404, T406).
multc245(T508, s(s(s(s(T510))))) :- multc277(T508, T510).
multc277(0, 0).
multc277(s(T529), T531) :- multc245(T529, T531).
multc277(T539, s(T541)) :- multc277(T539, T541).
multc319(T658, s(s(s(s(s(T660)))))) :- multc359(T658, T660).
multc359(0, 0).
multc359(s(T679), T681) :- multc319(T679, T681).
multc359(T689, s(T691)) :- multc359(T689, T691).
multc401(T823, s(s(s(s(s(s(T825))))))) :- multc449(T823, T825).
multc449(0, 0).
multc449(s(T844), T846) :- multc401(T844, T846).
multc449(T854, s(T856)) :- multc449(T854, T856).
multc491(T1003, s(s(s(s(s(s(s(T1005)))))))) :- multc547(T1003, T1005).
multc547(0, 0).
multc547(s(T1024), T1026) :- multc491(T1024, T1026).
multc547(T1034, s(T1036)) :- multc547(T1034, T1036).
multc16(0, 0, 0).
multc16(s(T61), 0, T64) :- multc29(T61, T64).
multc16(T102, 0, s(T105)) :- multc29(T102, T105).
multc16(0, s(0), s(0)).
multc16(s(T136), s(0), s(T139)) :- multc71(T136, T139).
multc16(T192, s(0), s(s(T195))) :- multc79(T192, T195).
multc16(0, s(s(0)), s(s(0))).
multc16(s(T226), s(s(0)), s(s(T229))) :- multc121(T226, T229).
multc16(T297, s(s(0)), s(s(s(T300)))) :- multc137(T297, T300).
multc16(0, s(s(s(0))), s(s(s(0)))).
multc16(s(T331), s(s(s(0))), s(s(s(T334)))) :- multc179(T331, T334).
multc16(T417, s(s(s(0))), s(s(s(s(T420))))) :- multc203(T417, T420).
multc16(0, s(s(s(s(0)))), s(s(s(s(0))))).
multc16(s(T451), s(s(s(s(0)))), s(s(s(s(T454))))) :- multc245(T451, T454).
multc16(T552, s(s(s(s(0)))), s(s(s(s(s(T555)))))) :- multc277(T552, T555).
multc16(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))).
multc16(s(T586), s(s(s(s(s(0))))), s(s(s(s(s(T589)))))) :- multc319(T586, T589).
multc16(T702, s(s(s(s(s(0))))), s(s(s(s(s(s(T705))))))) :- multc359(T702, T705).
multc16(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))).
multc16(s(T736), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T739))))))) :- multc401(T736, T739).
multc16(T867, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T870)))))))) :- multc449(T867, T870).
multc16(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))).
multc16(s(T901), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T904)))))))) :- multc491(T901, T904).
multc16(T1047, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T1050))))))))) :- multc547(T1047, T1050).
multc16(T1047, s(s(s(s(s(s(s(s(T1056)))))))), s(s(s(s(s(s(s(s(T1050))))))))) :- multc577(T1047, s(s(s(s(s(s(s(T1056))))))), T1056, T1050).
multc3(0, T15, 0).
multc3(s(T33), T34, T36) :- multc16(T33, T34, T36).
multc3(T1122, T1123, s(T1125)) :- multc3(T1122, T1123, T1125).
multc577(0, T1066, 0, 0).
multc577(s(T1084), T1085, 0, T1087) :- multc16(T1084, s(T1085), T1087).
multc577(T1102, T1103, 0, s(T1106)) :- multc3(T1102, s(T1103), T1106).
multc577(T1102, T1103, s(T1113), s(T1106)) :- multc577(T1102, T1103, T1113, T1106).

Afs:

times1(x1, x2, x3)  =  times1(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:
times1_in: (b,b,f)
mult3_in: (b,b,f)
mult16_in: (b,b,f)
mult29_in: (b,f)
mult71_in: (b,f)
mult79_in: (b,f)
mult121_in: (b,f)
mult137_in: (b,f)
mult179_in: (b,f)
mult203_in: (b,f)
mult245_in: (b,f)
mult277_in: (b,f)
mult319_in: (b,f)
mult359_in: (b,f)
mult401_in: (b,f)
mult449_in: (b,f)
mult491_in: (b,f)
mult547_in: (b,f)
mult577_in: (b,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

TIMES1_IN_GGA(T7, T8, T10) → U46_GGA(T7, T8, T10, mult3_in_gga(T7, T8, T10))
TIMES1_IN_GGA(T7, T8, T10) → MULT3_IN_GGA(T7, T8, T10)
MULT3_IN_GGA(s(T33), T34, T36) → U41_GGA(T33, T34, T36, mult16_in_gga(T33, T34, T36))
MULT3_IN_GGA(s(T33), T34, T36) → MULT16_IN_GGA(T33, T34, T36)
MULT16_IN_GGA(s(T61), 0, T64) → U24_GGA(T61, T64, mult29_in_ga(T61, T64))
MULT16_IN_GGA(s(T61), 0, T64) → MULT29_IN_GA(T61, T64)
MULT29_IN_GA(s(T81), T83) → U1_GA(T81, T83, mult29_in_ga(T81, T83))
MULT29_IN_GA(s(T81), T83) → MULT29_IN_GA(T81, T83)
MULT29_IN_GA(T89, s(T91)) → U2_GA(T89, T91, mult29_in_ga(T89, T91))
MULT29_IN_GA(T89, s(T91)) → MULT29_IN_GA(T89, T91)
MULT16_IN_GGA(T102, 0, s(T105)) → U25_GGA(T102, T105, mult29_in_ga(T102, T105))
MULT16_IN_GGA(T102, 0, s(T105)) → MULT29_IN_GA(T102, T105)
MULT16_IN_GGA(s(T136), s(0), s(T139)) → U26_GGA(T136, T139, mult71_in_ga(T136, T139))
MULT16_IN_GGA(s(T136), s(0), s(T139)) → MULT71_IN_GA(T136, T139)
MULT71_IN_GA(T148, s(T150)) → U3_GA(T148, T150, mult79_in_ga(T148, T150))
MULT71_IN_GA(T148, s(T150)) → MULT79_IN_GA(T148, T150)
MULT79_IN_GA(s(T169), T171) → U4_GA(T169, T171, mult71_in_ga(T169, T171))
MULT79_IN_GA(s(T169), T171) → MULT71_IN_GA(T169, T171)
MULT79_IN_GA(T179, s(T181)) → U5_GA(T179, T181, mult79_in_ga(T179, T181))
MULT79_IN_GA(T179, s(T181)) → MULT79_IN_GA(T179, T181)
MULT16_IN_GGA(T192, s(0), s(s(T195))) → U27_GGA(T192, T195, mult79_in_ga(T192, T195))
MULT16_IN_GGA(T192, s(0), s(s(T195))) → MULT79_IN_GA(T192, T195)
MULT16_IN_GGA(s(T226), s(s(0)), s(s(T229))) → U28_GGA(T226, T229, mult121_in_ga(T226, T229))
MULT16_IN_GGA(s(T226), s(s(0)), s(s(T229))) → MULT121_IN_GA(T226, T229)
MULT121_IN_GA(T253, s(s(T255))) → U6_GA(T253, T255, mult137_in_ga(T253, T255))
MULT121_IN_GA(T253, s(s(T255))) → MULT137_IN_GA(T253, T255)
MULT137_IN_GA(s(T274), T276) → U7_GA(T274, T276, mult121_in_ga(T274, T276))
MULT137_IN_GA(s(T274), T276) → MULT121_IN_GA(T274, T276)
MULT137_IN_GA(T284, s(T286)) → U8_GA(T284, T286, mult137_in_ga(T284, T286))
MULT137_IN_GA(T284, s(T286)) → MULT137_IN_GA(T284, T286)
MULT16_IN_GGA(T297, s(s(0)), s(s(s(T300)))) → U29_GGA(T297, T300, mult137_in_ga(T297, T300))
MULT16_IN_GGA(T297, s(s(0)), s(s(s(T300)))) → MULT137_IN_GA(T297, T300)
MULT16_IN_GGA(s(T331), s(s(s(0))), s(s(s(T334)))) → U30_GGA(T331, T334, mult179_in_ga(T331, T334))
MULT16_IN_GGA(s(T331), s(s(s(0))), s(s(s(T334)))) → MULT179_IN_GA(T331, T334)
MULT179_IN_GA(T373, s(s(s(T375)))) → U9_GA(T373, T375, mult203_in_ga(T373, T375))
MULT179_IN_GA(T373, s(s(s(T375)))) → MULT203_IN_GA(T373, T375)
MULT203_IN_GA(s(T394), T396) → U10_GA(T394, T396, mult179_in_ga(T394, T396))
MULT203_IN_GA(s(T394), T396) → MULT179_IN_GA(T394, T396)
MULT203_IN_GA(T404, s(T406)) → U11_GA(T404, T406, mult203_in_ga(T404, T406))
MULT203_IN_GA(T404, s(T406)) → MULT203_IN_GA(T404, T406)
MULT16_IN_GGA(T417, s(s(s(0))), s(s(s(s(T420))))) → U31_GGA(T417, T420, mult203_in_ga(T417, T420))
MULT16_IN_GGA(T417, s(s(s(0))), s(s(s(s(T420))))) → MULT203_IN_GA(T417, T420)
MULT16_IN_GGA(s(T451), s(s(s(s(0)))), s(s(s(s(T454))))) → U32_GGA(T451, T454, mult245_in_ga(T451, T454))
MULT16_IN_GGA(s(T451), s(s(s(s(0)))), s(s(s(s(T454))))) → MULT245_IN_GA(T451, T454)
MULT245_IN_GA(T508, s(s(s(s(T510))))) → U12_GA(T508, T510, mult277_in_ga(T508, T510))
MULT245_IN_GA(T508, s(s(s(s(T510))))) → MULT277_IN_GA(T508, T510)
MULT277_IN_GA(s(T529), T531) → U13_GA(T529, T531, mult245_in_ga(T529, T531))
MULT277_IN_GA(s(T529), T531) → MULT245_IN_GA(T529, T531)
MULT277_IN_GA(T539, s(T541)) → U14_GA(T539, T541, mult277_in_ga(T539, T541))
MULT277_IN_GA(T539, s(T541)) → MULT277_IN_GA(T539, T541)
MULT16_IN_GGA(T552, s(s(s(s(0)))), s(s(s(s(s(T555)))))) → U33_GGA(T552, T555, mult277_in_ga(T552, T555))
MULT16_IN_GGA(T552, s(s(s(s(0)))), s(s(s(s(s(T555)))))) → MULT277_IN_GA(T552, T555)
MULT16_IN_GGA(s(T586), s(s(s(s(s(0))))), s(s(s(s(s(T589)))))) → U34_GGA(T586, T589, mult319_in_ga(T586, T589))
MULT16_IN_GGA(s(T586), s(s(s(s(s(0))))), s(s(s(s(s(T589)))))) → MULT319_IN_GA(T586, T589)
MULT319_IN_GA(T658, s(s(s(s(s(T660)))))) → U15_GA(T658, T660, mult359_in_ga(T658, T660))
MULT319_IN_GA(T658, s(s(s(s(s(T660)))))) → MULT359_IN_GA(T658, T660)
MULT359_IN_GA(s(T679), T681) → U16_GA(T679, T681, mult319_in_ga(T679, T681))
MULT359_IN_GA(s(T679), T681) → MULT319_IN_GA(T679, T681)
MULT359_IN_GA(T689, s(T691)) → U17_GA(T689, T691, mult359_in_ga(T689, T691))
MULT359_IN_GA(T689, s(T691)) → MULT359_IN_GA(T689, T691)
MULT16_IN_GGA(T702, s(s(s(s(s(0))))), s(s(s(s(s(s(T705))))))) → U35_GGA(T702, T705, mult359_in_ga(T702, T705))
MULT16_IN_GGA(T702, s(s(s(s(s(0))))), s(s(s(s(s(s(T705))))))) → MULT359_IN_GA(T702, T705)
MULT16_IN_GGA(s(T736), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T739))))))) → U36_GGA(T736, T739, mult401_in_ga(T736, T739))
MULT16_IN_GGA(s(T736), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T739))))))) → MULT401_IN_GA(T736, T739)
MULT401_IN_GA(T823, s(s(s(s(s(s(T825))))))) → U18_GA(T823, T825, mult449_in_ga(T823, T825))
MULT401_IN_GA(T823, s(s(s(s(s(s(T825))))))) → MULT449_IN_GA(T823, T825)
MULT449_IN_GA(s(T844), T846) → U19_GA(T844, T846, mult401_in_ga(T844, T846))
MULT449_IN_GA(s(T844), T846) → MULT401_IN_GA(T844, T846)
MULT449_IN_GA(T854, s(T856)) → U20_GA(T854, T856, mult449_in_ga(T854, T856))
MULT449_IN_GA(T854, s(T856)) → MULT449_IN_GA(T854, T856)
MULT16_IN_GGA(T867, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T870)))))))) → U37_GGA(T867, T870, mult449_in_ga(T867, T870))
MULT16_IN_GGA(T867, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T870)))))))) → MULT449_IN_GA(T867, T870)
MULT16_IN_GGA(s(T901), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T904)))))))) → U38_GGA(T901, T904, mult491_in_ga(T901, T904))
MULT16_IN_GGA(s(T901), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T904)))))))) → MULT491_IN_GA(T901, T904)
MULT491_IN_GA(T1003, s(s(s(s(s(s(s(T1005)))))))) → U21_GA(T1003, T1005, mult547_in_ga(T1003, T1005))
MULT491_IN_GA(T1003, s(s(s(s(s(s(s(T1005)))))))) → MULT547_IN_GA(T1003, T1005)
MULT547_IN_GA(s(T1024), T1026) → U22_GA(T1024, T1026, mult491_in_ga(T1024, T1026))
MULT547_IN_GA(s(T1024), T1026) → MULT491_IN_GA(T1024, T1026)
MULT547_IN_GA(T1034, s(T1036)) → U23_GA(T1034, T1036, mult547_in_ga(T1034, T1036))
MULT547_IN_GA(T1034, s(T1036)) → MULT547_IN_GA(T1034, T1036)
MULT16_IN_GGA(T1047, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T1050))))))))) → U39_GGA(T1047, T1050, mult547_in_ga(T1047, T1050))
MULT16_IN_GGA(T1047, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T1050))))))))) → MULT547_IN_GA(T1047, T1050)
MULT16_IN_GGA(T1047, s(s(s(s(s(s(s(s(T1056)))))))), s(s(s(s(s(s(s(s(T1050))))))))) → U40_GGA(T1047, T1056, T1050, mult577_in_ggga(T1047, s(s(s(s(s(s(s(T1056))))))), T1056, T1050))
MULT16_IN_GGA(T1047, s(s(s(s(s(s(s(s(T1056)))))))), s(s(s(s(s(s(s(s(T1050))))))))) → MULT577_IN_GGGA(T1047, s(s(s(s(s(s(s(T1056))))))), T1056, T1050)
MULT577_IN_GGGA(s(T1084), T1085, 0, T1087) → U43_GGGA(T1084, T1085, T1087, mult16_in_gga(T1084, s(T1085), T1087))
MULT577_IN_GGGA(s(T1084), T1085, 0, T1087) → MULT16_IN_GGA(T1084, s(T1085), T1087)
MULT577_IN_GGGA(T1102, T1103, 0, s(T1106)) → U44_GGGA(T1102, T1103, T1106, mult3_in_gga(T1102, s(T1103), T1106))
MULT577_IN_GGGA(T1102, T1103, 0, s(T1106)) → MULT3_IN_GGA(T1102, s(T1103), T1106)
MULT3_IN_GGA(T1122, T1123, s(T1125)) → U42_GGA(T1122, T1123, T1125, mult3_in_gga(T1122, T1123, T1125))
MULT3_IN_GGA(T1122, T1123, s(T1125)) → MULT3_IN_GGA(T1122, T1123, T1125)
MULT577_IN_GGGA(T1102, T1103, s(T1113), s(T1106)) → U45_GGGA(T1102, T1103, T1113, T1106, mult577_in_ggga(T1102, T1103, T1113, T1106))
MULT577_IN_GGGA(T1102, T1103, s(T1113), s(T1106)) → MULT577_IN_GGGA(T1102, T1103, T1113, T1106)

R is empty.
The argument filtering Pi contains the following mapping:
mult3_in_gga(x1, x2, x3)  =  mult3_in_gga(x1, x2)
s(x1)  =  s(x1)
mult16_in_gga(x1, x2, x3)  =  mult16_in_gga(x1, x2)
0  =  0
mult29_in_ga(x1, x2)  =  mult29_in_ga(x1)
mult71_in_ga(x1, x2)  =  mult71_in_ga(x1)
mult79_in_ga(x1, x2)  =  mult79_in_ga(x1)
mult121_in_ga(x1, x2)  =  mult121_in_ga(x1)
mult137_in_ga(x1, x2)  =  mult137_in_ga(x1)
mult179_in_ga(x1, x2)  =  mult179_in_ga(x1)
mult203_in_ga(x1, x2)  =  mult203_in_ga(x1)
mult245_in_ga(x1, x2)  =  mult245_in_ga(x1)
mult277_in_ga(x1, x2)  =  mult277_in_ga(x1)
mult319_in_ga(x1, x2)  =  mult319_in_ga(x1)
mult359_in_ga(x1, x2)  =  mult359_in_ga(x1)
mult401_in_ga(x1, x2)  =  mult401_in_ga(x1)
mult449_in_ga(x1, x2)  =  mult449_in_ga(x1)
mult491_in_ga(x1, x2)  =  mult491_in_ga(x1)
mult547_in_ga(x1, x2)  =  mult547_in_ga(x1)
mult577_in_ggga(x1, x2, x3, x4)  =  mult577_in_ggga(x1, x2, x3)
TIMES1_IN_GGA(x1, x2, x3)  =  TIMES1_IN_GGA(x1, x2)
U46_GGA(x1, x2, x3, x4)  =  U46_GGA(x1, x2, x4)
MULT3_IN_GGA(x1, x2, x3)  =  MULT3_IN_GGA(x1, x2)
U41_GGA(x1, x2, x3, x4)  =  U41_GGA(x1, x2, x4)
MULT16_IN_GGA(x1, x2, x3)  =  MULT16_IN_GGA(x1, x2)
U24_GGA(x1, x2, x3)  =  U24_GGA(x1, x3)
MULT29_IN_GA(x1, x2)  =  MULT29_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U25_GGA(x1, x2, x3)  =  U25_GGA(x1, x3)
U26_GGA(x1, x2, x3)  =  U26_GGA(x1, x3)
MULT71_IN_GA(x1, x2)  =  MULT71_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
MULT79_IN_GA(x1, x2)  =  MULT79_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U27_GGA(x1, x2, x3)  =  U27_GGA(x1, x3)
U28_GGA(x1, x2, x3)  =  U28_GGA(x1, x3)
MULT121_IN_GA(x1, x2)  =  MULT121_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
MULT137_IN_GA(x1, x2)  =  MULT137_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U29_GGA(x1, x2, x3)  =  U29_GGA(x1, x3)
U30_GGA(x1, x2, x3)  =  U30_GGA(x1, x3)
MULT179_IN_GA(x1, x2)  =  MULT179_IN_GA(x1)
U9_GA(x1, x2, x3)  =  U9_GA(x1, x3)
MULT203_IN_GA(x1, x2)  =  MULT203_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
U31_GGA(x1, x2, x3)  =  U31_GGA(x1, x3)
U32_GGA(x1, x2, x3)  =  U32_GGA(x1, x3)
MULT245_IN_GA(x1, x2)  =  MULT245_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
MULT277_IN_GA(x1, x2)  =  MULT277_IN_GA(x1)
U13_GA(x1, x2, x3)  =  U13_GA(x1, x3)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
U33_GGA(x1, x2, x3)  =  U33_GGA(x1, x3)
U34_GGA(x1, x2, x3)  =  U34_GGA(x1, x3)
MULT319_IN_GA(x1, x2)  =  MULT319_IN_GA(x1)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
MULT359_IN_GA(x1, x2)  =  MULT359_IN_GA(x1)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
U35_GGA(x1, x2, x3)  =  U35_GGA(x1, x3)
U36_GGA(x1, x2, x3)  =  U36_GGA(x1, x3)
MULT401_IN_GA(x1, x2)  =  MULT401_IN_GA(x1)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)
MULT449_IN_GA(x1, x2)  =  MULT449_IN_GA(x1)
U19_GA(x1, x2, x3)  =  U19_GA(x1, x3)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U37_GGA(x1, x2, x3)  =  U37_GGA(x1, x3)
U38_GGA(x1, x2, x3)  =  U38_GGA(x1, x3)
MULT491_IN_GA(x1, x2)  =  MULT491_IN_GA(x1)
U21_GA(x1, x2, x3)  =  U21_GA(x1, x3)
MULT547_IN_GA(x1, x2)  =  MULT547_IN_GA(x1)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
U39_GGA(x1, x2, x3)  =  U39_GGA(x1, x3)
U40_GGA(x1, x2, x3, x4)  =  U40_GGA(x1, x2, x4)
MULT577_IN_GGGA(x1, x2, x3, x4)  =  MULT577_IN_GGGA(x1, x2, x3)
U43_GGGA(x1, x2, x3, x4)  =  U43_GGGA(x1, x2, x4)
U44_GGGA(x1, x2, x3, x4)  =  U44_GGGA(x1, x2, x4)
U42_GGA(x1, x2, x3, x4)  =  U42_GGA(x1, x2, x4)
U45_GGGA(x1, x2, x3, x4, x5)  =  U45_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:

TIMES1_IN_GGA(T7, T8, T10) → U46_GGA(T7, T8, T10, mult3_in_gga(T7, T8, T10))
TIMES1_IN_GGA(T7, T8, T10) → MULT3_IN_GGA(T7, T8, T10)
MULT3_IN_GGA(s(T33), T34, T36) → U41_GGA(T33, T34, T36, mult16_in_gga(T33, T34, T36))
MULT3_IN_GGA(s(T33), T34, T36) → MULT16_IN_GGA(T33, T34, T36)
MULT16_IN_GGA(s(T61), 0, T64) → U24_GGA(T61, T64, mult29_in_ga(T61, T64))
MULT16_IN_GGA(s(T61), 0, T64) → MULT29_IN_GA(T61, T64)
MULT29_IN_GA(s(T81), T83) → U1_GA(T81, T83, mult29_in_ga(T81, T83))
MULT29_IN_GA(s(T81), T83) → MULT29_IN_GA(T81, T83)
MULT29_IN_GA(T89, s(T91)) → U2_GA(T89, T91, mult29_in_ga(T89, T91))
MULT29_IN_GA(T89, s(T91)) → MULT29_IN_GA(T89, T91)
MULT16_IN_GGA(T102, 0, s(T105)) → U25_GGA(T102, T105, mult29_in_ga(T102, T105))
MULT16_IN_GGA(T102, 0, s(T105)) → MULT29_IN_GA(T102, T105)
MULT16_IN_GGA(s(T136), s(0), s(T139)) → U26_GGA(T136, T139, mult71_in_ga(T136, T139))
MULT16_IN_GGA(s(T136), s(0), s(T139)) → MULT71_IN_GA(T136, T139)
MULT71_IN_GA(T148, s(T150)) → U3_GA(T148, T150, mult79_in_ga(T148, T150))
MULT71_IN_GA(T148, s(T150)) → MULT79_IN_GA(T148, T150)
MULT79_IN_GA(s(T169), T171) → U4_GA(T169, T171, mult71_in_ga(T169, T171))
MULT79_IN_GA(s(T169), T171) → MULT71_IN_GA(T169, T171)
MULT79_IN_GA(T179, s(T181)) → U5_GA(T179, T181, mult79_in_ga(T179, T181))
MULT79_IN_GA(T179, s(T181)) → MULT79_IN_GA(T179, T181)
MULT16_IN_GGA(T192, s(0), s(s(T195))) → U27_GGA(T192, T195, mult79_in_ga(T192, T195))
MULT16_IN_GGA(T192, s(0), s(s(T195))) → MULT79_IN_GA(T192, T195)
MULT16_IN_GGA(s(T226), s(s(0)), s(s(T229))) → U28_GGA(T226, T229, mult121_in_ga(T226, T229))
MULT16_IN_GGA(s(T226), s(s(0)), s(s(T229))) → MULT121_IN_GA(T226, T229)
MULT121_IN_GA(T253, s(s(T255))) → U6_GA(T253, T255, mult137_in_ga(T253, T255))
MULT121_IN_GA(T253, s(s(T255))) → MULT137_IN_GA(T253, T255)
MULT137_IN_GA(s(T274), T276) → U7_GA(T274, T276, mult121_in_ga(T274, T276))
MULT137_IN_GA(s(T274), T276) → MULT121_IN_GA(T274, T276)
MULT137_IN_GA(T284, s(T286)) → U8_GA(T284, T286, mult137_in_ga(T284, T286))
MULT137_IN_GA(T284, s(T286)) → MULT137_IN_GA(T284, T286)
MULT16_IN_GGA(T297, s(s(0)), s(s(s(T300)))) → U29_GGA(T297, T300, mult137_in_ga(T297, T300))
MULT16_IN_GGA(T297, s(s(0)), s(s(s(T300)))) → MULT137_IN_GA(T297, T300)
MULT16_IN_GGA(s(T331), s(s(s(0))), s(s(s(T334)))) → U30_GGA(T331, T334, mult179_in_ga(T331, T334))
MULT16_IN_GGA(s(T331), s(s(s(0))), s(s(s(T334)))) → MULT179_IN_GA(T331, T334)
MULT179_IN_GA(T373, s(s(s(T375)))) → U9_GA(T373, T375, mult203_in_ga(T373, T375))
MULT179_IN_GA(T373, s(s(s(T375)))) → MULT203_IN_GA(T373, T375)
MULT203_IN_GA(s(T394), T396) → U10_GA(T394, T396, mult179_in_ga(T394, T396))
MULT203_IN_GA(s(T394), T396) → MULT179_IN_GA(T394, T396)
MULT203_IN_GA(T404, s(T406)) → U11_GA(T404, T406, mult203_in_ga(T404, T406))
MULT203_IN_GA(T404, s(T406)) → MULT203_IN_GA(T404, T406)
MULT16_IN_GGA(T417, s(s(s(0))), s(s(s(s(T420))))) → U31_GGA(T417, T420, mult203_in_ga(T417, T420))
MULT16_IN_GGA(T417, s(s(s(0))), s(s(s(s(T420))))) → MULT203_IN_GA(T417, T420)
MULT16_IN_GGA(s(T451), s(s(s(s(0)))), s(s(s(s(T454))))) → U32_GGA(T451, T454, mult245_in_ga(T451, T454))
MULT16_IN_GGA(s(T451), s(s(s(s(0)))), s(s(s(s(T454))))) → MULT245_IN_GA(T451, T454)
MULT245_IN_GA(T508, s(s(s(s(T510))))) → U12_GA(T508, T510, mult277_in_ga(T508, T510))
MULT245_IN_GA(T508, s(s(s(s(T510))))) → MULT277_IN_GA(T508, T510)
MULT277_IN_GA(s(T529), T531) → U13_GA(T529, T531, mult245_in_ga(T529, T531))
MULT277_IN_GA(s(T529), T531) → MULT245_IN_GA(T529, T531)
MULT277_IN_GA(T539, s(T541)) → U14_GA(T539, T541, mult277_in_ga(T539, T541))
MULT277_IN_GA(T539, s(T541)) → MULT277_IN_GA(T539, T541)
MULT16_IN_GGA(T552, s(s(s(s(0)))), s(s(s(s(s(T555)))))) → U33_GGA(T552, T555, mult277_in_ga(T552, T555))
MULT16_IN_GGA(T552, s(s(s(s(0)))), s(s(s(s(s(T555)))))) → MULT277_IN_GA(T552, T555)
MULT16_IN_GGA(s(T586), s(s(s(s(s(0))))), s(s(s(s(s(T589)))))) → U34_GGA(T586, T589, mult319_in_ga(T586, T589))
MULT16_IN_GGA(s(T586), s(s(s(s(s(0))))), s(s(s(s(s(T589)))))) → MULT319_IN_GA(T586, T589)
MULT319_IN_GA(T658, s(s(s(s(s(T660)))))) → U15_GA(T658, T660, mult359_in_ga(T658, T660))
MULT319_IN_GA(T658, s(s(s(s(s(T660)))))) → MULT359_IN_GA(T658, T660)
MULT359_IN_GA(s(T679), T681) → U16_GA(T679, T681, mult319_in_ga(T679, T681))
MULT359_IN_GA(s(T679), T681) → MULT319_IN_GA(T679, T681)
MULT359_IN_GA(T689, s(T691)) → U17_GA(T689, T691, mult359_in_ga(T689, T691))
MULT359_IN_GA(T689, s(T691)) → MULT359_IN_GA(T689, T691)
MULT16_IN_GGA(T702, s(s(s(s(s(0))))), s(s(s(s(s(s(T705))))))) → U35_GGA(T702, T705, mult359_in_ga(T702, T705))
MULT16_IN_GGA(T702, s(s(s(s(s(0))))), s(s(s(s(s(s(T705))))))) → MULT359_IN_GA(T702, T705)
MULT16_IN_GGA(s(T736), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T739))))))) → U36_GGA(T736, T739, mult401_in_ga(T736, T739))
MULT16_IN_GGA(s(T736), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T739))))))) → MULT401_IN_GA(T736, T739)
MULT401_IN_GA(T823, s(s(s(s(s(s(T825))))))) → U18_GA(T823, T825, mult449_in_ga(T823, T825))
MULT401_IN_GA(T823, s(s(s(s(s(s(T825))))))) → MULT449_IN_GA(T823, T825)
MULT449_IN_GA(s(T844), T846) → U19_GA(T844, T846, mult401_in_ga(T844, T846))
MULT449_IN_GA(s(T844), T846) → MULT401_IN_GA(T844, T846)
MULT449_IN_GA(T854, s(T856)) → U20_GA(T854, T856, mult449_in_ga(T854, T856))
MULT449_IN_GA(T854, s(T856)) → MULT449_IN_GA(T854, T856)
MULT16_IN_GGA(T867, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T870)))))))) → U37_GGA(T867, T870, mult449_in_ga(T867, T870))
MULT16_IN_GGA(T867, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T870)))))))) → MULT449_IN_GA(T867, T870)
MULT16_IN_GGA(s(T901), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T904)))))))) → U38_GGA(T901, T904, mult491_in_ga(T901, T904))
MULT16_IN_GGA(s(T901), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T904)))))))) → MULT491_IN_GA(T901, T904)
MULT491_IN_GA(T1003, s(s(s(s(s(s(s(T1005)))))))) → U21_GA(T1003, T1005, mult547_in_ga(T1003, T1005))
MULT491_IN_GA(T1003, s(s(s(s(s(s(s(T1005)))))))) → MULT547_IN_GA(T1003, T1005)
MULT547_IN_GA(s(T1024), T1026) → U22_GA(T1024, T1026, mult491_in_ga(T1024, T1026))
MULT547_IN_GA(s(T1024), T1026) → MULT491_IN_GA(T1024, T1026)
MULT547_IN_GA(T1034, s(T1036)) → U23_GA(T1034, T1036, mult547_in_ga(T1034, T1036))
MULT547_IN_GA(T1034, s(T1036)) → MULT547_IN_GA(T1034, T1036)
MULT16_IN_GGA(T1047, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T1050))))))))) → U39_GGA(T1047, T1050, mult547_in_ga(T1047, T1050))
MULT16_IN_GGA(T1047, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T1050))))))))) → MULT547_IN_GA(T1047, T1050)
MULT16_IN_GGA(T1047, s(s(s(s(s(s(s(s(T1056)))))))), s(s(s(s(s(s(s(s(T1050))))))))) → U40_GGA(T1047, T1056, T1050, mult577_in_ggga(T1047, s(s(s(s(s(s(s(T1056))))))), T1056, T1050))
MULT16_IN_GGA(T1047, s(s(s(s(s(s(s(s(T1056)))))))), s(s(s(s(s(s(s(s(T1050))))))))) → MULT577_IN_GGGA(T1047, s(s(s(s(s(s(s(T1056))))))), T1056, T1050)
MULT577_IN_GGGA(s(T1084), T1085, 0, T1087) → U43_GGGA(T1084, T1085, T1087, mult16_in_gga(T1084, s(T1085), T1087))
MULT577_IN_GGGA(s(T1084), T1085, 0, T1087) → MULT16_IN_GGA(T1084, s(T1085), T1087)
MULT577_IN_GGGA(T1102, T1103, 0, s(T1106)) → U44_GGGA(T1102, T1103, T1106, mult3_in_gga(T1102, s(T1103), T1106))
MULT577_IN_GGGA(T1102, T1103, 0, s(T1106)) → MULT3_IN_GGA(T1102, s(T1103), T1106)
MULT3_IN_GGA(T1122, T1123, s(T1125)) → U42_GGA(T1122, T1123, T1125, mult3_in_gga(T1122, T1123, T1125))
MULT3_IN_GGA(T1122, T1123, s(T1125)) → MULT3_IN_GGA(T1122, T1123, T1125)
MULT577_IN_GGGA(T1102, T1103, s(T1113), s(T1106)) → U45_GGGA(T1102, T1103, T1113, T1106, mult577_in_ggga(T1102, T1103, T1113, T1106))
MULT577_IN_GGGA(T1102, T1103, s(T1113), s(T1106)) → MULT577_IN_GGGA(T1102, T1103, T1113, T1106)

R is empty.
The argument filtering Pi contains the following mapping:
mult3_in_gga(x1, x2, x3)  =  mult3_in_gga(x1, x2)
s(x1)  =  s(x1)
mult16_in_gga(x1, x2, x3)  =  mult16_in_gga(x1, x2)
0  =  0
mult29_in_ga(x1, x2)  =  mult29_in_ga(x1)
mult71_in_ga(x1, x2)  =  mult71_in_ga(x1)
mult79_in_ga(x1, x2)  =  mult79_in_ga(x1)
mult121_in_ga(x1, x2)  =  mult121_in_ga(x1)
mult137_in_ga(x1, x2)  =  mult137_in_ga(x1)
mult179_in_ga(x1, x2)  =  mult179_in_ga(x1)
mult203_in_ga(x1, x2)  =  mult203_in_ga(x1)
mult245_in_ga(x1, x2)  =  mult245_in_ga(x1)
mult277_in_ga(x1, x2)  =  mult277_in_ga(x1)
mult319_in_ga(x1, x2)  =  mult319_in_ga(x1)
mult359_in_ga(x1, x2)  =  mult359_in_ga(x1)
mult401_in_ga(x1, x2)  =  mult401_in_ga(x1)
mult449_in_ga(x1, x2)  =  mult449_in_ga(x1)
mult491_in_ga(x1, x2)  =  mult491_in_ga(x1)
mult547_in_ga(x1, x2)  =  mult547_in_ga(x1)
mult577_in_ggga(x1, x2, x3, x4)  =  mult577_in_ggga(x1, x2, x3)
TIMES1_IN_GGA(x1, x2, x3)  =  TIMES1_IN_GGA(x1, x2)
U46_GGA(x1, x2, x3, x4)  =  U46_GGA(x1, x2, x4)
MULT3_IN_GGA(x1, x2, x3)  =  MULT3_IN_GGA(x1, x2)
U41_GGA(x1, x2, x3, x4)  =  U41_GGA(x1, x2, x4)
MULT16_IN_GGA(x1, x2, x3)  =  MULT16_IN_GGA(x1, x2)
U24_GGA(x1, x2, x3)  =  U24_GGA(x1, x3)
MULT29_IN_GA(x1, x2)  =  MULT29_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U25_GGA(x1, x2, x3)  =  U25_GGA(x1, x3)
U26_GGA(x1, x2, x3)  =  U26_GGA(x1, x3)
MULT71_IN_GA(x1, x2)  =  MULT71_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
MULT79_IN_GA(x1, x2)  =  MULT79_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U27_GGA(x1, x2, x3)  =  U27_GGA(x1, x3)
U28_GGA(x1, x2, x3)  =  U28_GGA(x1, x3)
MULT121_IN_GA(x1, x2)  =  MULT121_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
MULT137_IN_GA(x1, x2)  =  MULT137_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U29_GGA(x1, x2, x3)  =  U29_GGA(x1, x3)
U30_GGA(x1, x2, x3)  =  U30_GGA(x1, x3)
MULT179_IN_GA(x1, x2)  =  MULT179_IN_GA(x1)
U9_GA(x1, x2, x3)  =  U9_GA(x1, x3)
MULT203_IN_GA(x1, x2)  =  MULT203_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
U31_GGA(x1, x2, x3)  =  U31_GGA(x1, x3)
U32_GGA(x1, x2, x3)  =  U32_GGA(x1, x3)
MULT245_IN_GA(x1, x2)  =  MULT245_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
MULT277_IN_GA(x1, x2)  =  MULT277_IN_GA(x1)
U13_GA(x1, x2, x3)  =  U13_GA(x1, x3)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
U33_GGA(x1, x2, x3)  =  U33_GGA(x1, x3)
U34_GGA(x1, x2, x3)  =  U34_GGA(x1, x3)
MULT319_IN_GA(x1, x2)  =  MULT319_IN_GA(x1)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
MULT359_IN_GA(x1, x2)  =  MULT359_IN_GA(x1)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
U35_GGA(x1, x2, x3)  =  U35_GGA(x1, x3)
U36_GGA(x1, x2, x3)  =  U36_GGA(x1, x3)
MULT401_IN_GA(x1, x2)  =  MULT401_IN_GA(x1)
U18_GA(x1, x2, x3)  =  U18_GA(x1, x3)
MULT449_IN_GA(x1, x2)  =  MULT449_IN_GA(x1)
U19_GA(x1, x2, x3)  =  U19_GA(x1, x3)
U20_GA(x1, x2, x3)  =  U20_GA(x1, x3)
U37_GGA(x1, x2, x3)  =  U37_GGA(x1, x3)
U38_GGA(x1, x2, x3)  =  U38_GGA(x1, x3)
MULT491_IN_GA(x1, x2)  =  MULT491_IN_GA(x1)
U21_GA(x1, x2, x3)  =  U21_GA(x1, x3)
MULT547_IN_GA(x1, x2)  =  MULT547_IN_GA(x1)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
U39_GGA(x1, x2, x3)  =  U39_GGA(x1, x3)
U40_GGA(x1, x2, x3, x4)  =  U40_GGA(x1, x2, x4)
MULT577_IN_GGGA(x1, x2, x3, x4)  =  MULT577_IN_GGGA(x1, x2, x3)
U43_GGGA(x1, x2, x3, x4)  =  U43_GGGA(x1, x2, x4)
U44_GGGA(x1, x2, x3, x4)  =  U44_GGGA(x1, x2, x4)
U42_GGA(x1, x2, x3, x4)  =  U42_GGA(x1, x2, x4)
U45_GGGA(x1, x2, x3, x4, x5)  =  U45_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 9 SCCs with 63 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

MULT491_IN_GA(T1003, s(s(s(s(s(s(s(T1005)))))))) → MULT547_IN_GA(T1003, T1005)
MULT547_IN_GA(s(T1024), T1026) → MULT491_IN_GA(T1024, T1026)
MULT547_IN_GA(T1034, s(T1036)) → MULT547_IN_GA(T1034, T1036)

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

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:

MULT491_IN_GA(T1003) → MULT547_IN_GA(T1003)
MULT547_IN_GA(s(T1024)) → MULT491_IN_GA(T1024)
MULT547_IN_GA(T1034) → MULT547_IN_GA(T1034)

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

(10) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

MULT547_IN_GA(s(T1024)) → MULT491_IN_GA(T1024)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(MULT491_IN_GA(x1)) = 2 + x1   
POL(MULT547_IN_GA(x1)) = 2 + x1   
POL(s(x1)) = 2 + 2·x1   

(11) Obligation:

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

MULT491_IN_GA(T1003) → MULT547_IN_GA(T1003)
MULT547_IN_GA(T1034) → MULT547_IN_GA(T1034)

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

(12) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(13) Obligation:

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

MULT547_IN_GA(T1034) → MULT547_IN_GA(T1034)

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

(14) 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 = MULT547_IN_GA(T1034) evaluates to t =MULT547_IN_GA(T1034)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from MULT547_IN_GA(T1034) to MULT547_IN_GA(T1034).



(15) NO

(16) Obligation:

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

MULT401_IN_GA(T823, s(s(s(s(s(s(T825))))))) → MULT449_IN_GA(T823, T825)
MULT449_IN_GA(s(T844), T846) → MULT401_IN_GA(T844, T846)
MULT449_IN_GA(T854, s(T856)) → MULT449_IN_GA(T854, T856)

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

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:

MULT401_IN_GA(T823) → MULT449_IN_GA(T823)
MULT449_IN_GA(s(T844)) → MULT401_IN_GA(T844)
MULT449_IN_GA(T854) → MULT449_IN_GA(T854)

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

(19) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

MULT449_IN_GA(s(T844)) → MULT401_IN_GA(T844)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(MULT401_IN_GA(x1)) = 2 + x1   
POL(MULT449_IN_GA(x1)) = 2 + x1   
POL(s(x1)) = 2 + 2·x1   

(20) Obligation:

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

MULT401_IN_GA(T823) → MULT449_IN_GA(T823)
MULT449_IN_GA(T854) → MULT449_IN_GA(T854)

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

(21) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(22) Obligation:

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

MULT449_IN_GA(T854) → MULT449_IN_GA(T854)

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

(23) 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 = MULT449_IN_GA(T854) evaluates to t =MULT449_IN_GA(T854)

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 MULT449_IN_GA(T854) to MULT449_IN_GA(T854).



(24) NO

(25) Obligation:

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

MULT319_IN_GA(T658, s(s(s(s(s(T660)))))) → MULT359_IN_GA(T658, T660)
MULT359_IN_GA(s(T679), T681) → MULT319_IN_GA(T679, T681)
MULT359_IN_GA(T689, s(T691)) → MULT359_IN_GA(T689, T691)

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

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

MULT319_IN_GA(T658) → MULT359_IN_GA(T658)
MULT359_IN_GA(s(T679)) → MULT319_IN_GA(T679)
MULT359_IN_GA(T689) → MULT359_IN_GA(T689)

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

(28) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

MULT359_IN_GA(s(T679)) → MULT319_IN_GA(T679)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(MULT319_IN_GA(x1)) = 2 + x1   
POL(MULT359_IN_GA(x1)) = 2 + x1   
POL(s(x1)) = 2 + 2·x1   

(29) Obligation:

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

MULT319_IN_GA(T658) → MULT359_IN_GA(T658)
MULT359_IN_GA(T689) → MULT359_IN_GA(T689)

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

(30) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(31) Obligation:

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

MULT359_IN_GA(T689) → MULT359_IN_GA(T689)

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

(32) 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 = MULT359_IN_GA(T689) evaluates to t =MULT359_IN_GA(T689)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from MULT359_IN_GA(T689) to MULT359_IN_GA(T689).



(33) NO

(34) Obligation:

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

MULT245_IN_GA(T508, s(s(s(s(T510))))) → MULT277_IN_GA(T508, T510)
MULT277_IN_GA(s(T529), T531) → MULT245_IN_GA(T529, T531)
MULT277_IN_GA(T539, s(T541)) → MULT277_IN_GA(T539, T541)

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

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

(35) PiDPToQDPProof (SOUND transformation)

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

(36) Obligation:

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

MULT245_IN_GA(T508) → MULT277_IN_GA(T508)
MULT277_IN_GA(s(T529)) → MULT245_IN_GA(T529)
MULT277_IN_GA(T539) → MULT277_IN_GA(T539)

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

(37) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

MULT277_IN_GA(s(T529)) → MULT245_IN_GA(T529)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(MULT245_IN_GA(x1)) = 2 + x1   
POL(MULT277_IN_GA(x1)) = 2 + x1   
POL(s(x1)) = 2 + 2·x1   

(38) Obligation:

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

MULT245_IN_GA(T508) → MULT277_IN_GA(T508)
MULT277_IN_GA(T539) → MULT277_IN_GA(T539)

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

(39) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(40) Obligation:

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

MULT277_IN_GA(T539) → MULT277_IN_GA(T539)

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

(41) 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 = MULT277_IN_GA(T539) evaluates to t =MULT277_IN_GA(T539)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from MULT277_IN_GA(T539) to MULT277_IN_GA(T539).



(42) NO

(43) Obligation:

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

MULT179_IN_GA(T373, s(s(s(T375)))) → MULT203_IN_GA(T373, T375)
MULT203_IN_GA(s(T394), T396) → MULT179_IN_GA(T394, T396)
MULT203_IN_GA(T404, s(T406)) → MULT203_IN_GA(T404, T406)

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

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

(44) PiDPToQDPProof (SOUND transformation)

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

(45) Obligation:

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

MULT179_IN_GA(T373) → MULT203_IN_GA(T373)
MULT203_IN_GA(s(T394)) → MULT179_IN_GA(T394)
MULT203_IN_GA(T404) → MULT203_IN_GA(T404)

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

(46) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

MULT203_IN_GA(s(T394)) → MULT179_IN_GA(T394)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(MULT179_IN_GA(x1)) = 2 + x1   
POL(MULT203_IN_GA(x1)) = 2 + x1   
POL(s(x1)) = 2 + 2·x1   

(47) Obligation:

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

MULT179_IN_GA(T373) → MULT203_IN_GA(T373)
MULT203_IN_GA(T404) → MULT203_IN_GA(T404)

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

(48) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(49) Obligation:

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

MULT203_IN_GA(T404) → MULT203_IN_GA(T404)

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

(50) 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 = MULT203_IN_GA(T404) evaluates to t =MULT203_IN_GA(T404)

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 MULT203_IN_GA(T404) to MULT203_IN_GA(T404).



(51) NO

(52) Obligation:

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

MULT121_IN_GA(T253, s(s(T255))) → MULT137_IN_GA(T253, T255)
MULT137_IN_GA(s(T274), T276) → MULT121_IN_GA(T274, T276)
MULT137_IN_GA(T284, s(T286)) → MULT137_IN_GA(T284, T286)

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

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

(53) PiDPToQDPProof (SOUND transformation)

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

(54) Obligation:

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

MULT121_IN_GA(T253) → MULT137_IN_GA(T253)
MULT137_IN_GA(s(T274)) → MULT121_IN_GA(T274)
MULT137_IN_GA(T284) → MULT137_IN_GA(T284)

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

(55) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

MULT137_IN_GA(s(T274)) → MULT121_IN_GA(T274)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(MULT121_IN_GA(x1)) = 2 + x1   
POL(MULT137_IN_GA(x1)) = 2 + x1   
POL(s(x1)) = 2 + 2·x1   

(56) Obligation:

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

MULT121_IN_GA(T253) → MULT137_IN_GA(T253)
MULT137_IN_GA(T284) → MULT137_IN_GA(T284)

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

(57) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(58) Obligation:

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

MULT137_IN_GA(T284) → MULT137_IN_GA(T284)

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

(59) 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 = MULT137_IN_GA(T284) evaluates to t =MULT137_IN_GA(T284)

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 MULT137_IN_GA(T284) to MULT137_IN_GA(T284).



(60) NO

(61) Obligation:

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

MULT71_IN_GA(T148, s(T150)) → MULT79_IN_GA(T148, T150)
MULT79_IN_GA(s(T169), T171) → MULT71_IN_GA(T169, T171)
MULT79_IN_GA(T179, s(T181)) → MULT79_IN_GA(T179, T181)

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

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

(62) PiDPToQDPProof (SOUND transformation)

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

(63) Obligation:

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

MULT71_IN_GA(T148) → MULT79_IN_GA(T148)
MULT79_IN_GA(s(T169)) → MULT71_IN_GA(T169)
MULT79_IN_GA(T179) → MULT79_IN_GA(T179)

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

(64) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

MULT79_IN_GA(s(T169)) → MULT71_IN_GA(T169)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(MULT71_IN_GA(x1)) = 2 + x1   
POL(MULT79_IN_GA(x1)) = 2 + x1   
POL(s(x1)) = 2 + 2·x1   

(65) Obligation:

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

MULT71_IN_GA(T148) → MULT79_IN_GA(T148)
MULT79_IN_GA(T179) → MULT79_IN_GA(T179)

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

(66) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(67) Obligation:

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

MULT79_IN_GA(T179) → MULT79_IN_GA(T179)

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

(68) 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 = MULT79_IN_GA(T179) evaluates to t =MULT79_IN_GA(T179)

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 MULT79_IN_GA(T179) to MULT79_IN_GA(T179).



(69) NO

(70) Obligation:

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

MULT29_IN_GA(T89, s(T91)) → MULT29_IN_GA(T89, T91)
MULT29_IN_GA(s(T81), T83) → MULT29_IN_GA(T81, T83)

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

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

(71) PiDPToQDPProof (SOUND transformation)

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

(72) Obligation:

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

MULT29_IN_GA(T89) → MULT29_IN_GA(T89)
MULT29_IN_GA(s(T81)) → MULT29_IN_GA(T81)

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

(73) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

MULT29_IN_GA(s(T81)) → MULT29_IN_GA(T81)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(MULT29_IN_GA(x1)) = 2·x1   
POL(s(x1)) = 2·x1   

(74) Obligation:

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

MULT29_IN_GA(T89) → MULT29_IN_GA(T89)

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

(75) 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 = MULT29_IN_GA(T89) evaluates to t =MULT29_IN_GA(T89)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from MULT29_IN_GA(T89) to MULT29_IN_GA(T89).



(76) NO

(77) Obligation:

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

MULT3_IN_GGA(s(T33), T34, T36) → MULT16_IN_GGA(T33, T34, T36)
MULT16_IN_GGA(T1047, s(s(s(s(s(s(s(s(T1056)))))))), s(s(s(s(s(s(s(s(T1050))))))))) → MULT577_IN_GGGA(T1047, s(s(s(s(s(s(s(T1056))))))), T1056, T1050)
MULT577_IN_GGGA(s(T1084), T1085, 0, T1087) → MULT16_IN_GGA(T1084, s(T1085), T1087)
MULT577_IN_GGGA(T1102, T1103, 0, s(T1106)) → MULT3_IN_GGA(T1102, s(T1103), T1106)
MULT3_IN_GGA(T1122, T1123, s(T1125)) → MULT3_IN_GGA(T1122, T1123, T1125)
MULT577_IN_GGGA(T1102, T1103, s(T1113), s(T1106)) → MULT577_IN_GGGA(T1102, T1103, T1113, T1106)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
MULT3_IN_GGA(x1, x2, x3)  =  MULT3_IN_GGA(x1, x2)
MULT16_IN_GGA(x1, x2, x3)  =  MULT16_IN_GGA(x1, x2)
MULT577_IN_GGGA(x1, x2, x3, x4)  =  MULT577_IN_GGGA(x1, x2, x3)

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

(78) PiDPToQDPProof (SOUND transformation)

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

(79) Obligation:

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

MULT3_IN_GGA(s(T33), T34) → MULT16_IN_GGA(T33, T34)
MULT16_IN_GGA(T1047, s(s(s(s(s(s(s(s(T1056))))))))) → MULT577_IN_GGGA(T1047, s(s(s(s(s(s(s(T1056))))))), T1056)
MULT577_IN_GGGA(s(T1084), T1085, 0) → MULT16_IN_GGA(T1084, s(T1085))
MULT577_IN_GGGA(T1102, T1103, 0) → MULT3_IN_GGA(T1102, s(T1103))
MULT3_IN_GGA(T1122, T1123) → MULT3_IN_GGA(T1122, T1123)
MULT577_IN_GGGA(T1102, T1103, s(T1113)) → MULT577_IN_GGGA(T1102, T1103, T1113)

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

(80) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MULT577_IN_GGGA(s(T1084), T1085, 0) → MULT16_IN_GGA(T1084, s(T1085))
MULT577_IN_GGGA(T1102, T1103, 0) → MULT3_IN_GGA(T1102, s(T1103))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(MULT16_IN_GGA(x1, x2)) = 1 + x1   
POL(MULT3_IN_GGA(x1, x2)) = x1   
POL(MULT577_IN_GGGA(x1, x2, x3)) = 1 + x1   
POL(s(x1)) = 1 + x1   

The following usable rules [FROCOS05] were oriented: none

(81) Obligation:

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

MULT3_IN_GGA(s(T33), T34) → MULT16_IN_GGA(T33, T34)
MULT16_IN_GGA(T1047, s(s(s(s(s(s(s(s(T1056))))))))) → MULT577_IN_GGGA(T1047, s(s(s(s(s(s(s(T1056))))))), T1056)
MULT3_IN_GGA(T1122, T1123) → MULT3_IN_GGA(T1122, T1123)
MULT577_IN_GGGA(T1102, T1103, s(T1113)) → MULT577_IN_GGGA(T1102, T1103, T1113)

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

(82) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 2 less nodes.

(83) Complex Obligation (AND)

(84) Obligation:

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

MULT577_IN_GGGA(T1102, T1103, s(T1113)) → MULT577_IN_GGGA(T1102, T1103, T1113)

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

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

  • MULT577_IN_GGGA(T1102, T1103, s(T1113)) → MULT577_IN_GGGA(T1102, T1103, T1113)
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3

(86) YES

(87) Obligation:

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

MULT3_IN_GGA(T1122, T1123) → MULT3_IN_GGA(T1122, T1123)

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

(88) 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 = MULT3_IN_GGA(T1122, T1123) evaluates to t =MULT3_IN_GGA(T1122, T1123)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from MULT3_IN_GGA(T1122, T1123) to MULT3_IN_GGA(T1122, T1123).



(89) NO