(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 sequenceThe 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 sequenceThe 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 sequenceThe 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 sequenceThe 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 sequenceThe 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 sequenceThe 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 sequenceThe 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 sequenceThe 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 sequenceThe DP semiunifies directly so there is only one rewrite step from MULT3_IN_GGA(T1122, T1123) to MULT3_IN_GGA(T1122, T1123).
(89) NO