(0) Obligation:

Clauses:

even(0, true).
even(s(0), false).
even(s(s(X)), B) :- even(X, B).
half(0, 0).
half(s(s(X)), s(Y)) :- half(X, Y).
plus(0, Y, Y).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
times(0, Y, 0).
times(s(X), Y, Z) :- ','(even(s(X), B), if(B, s(X), Y, Z)).
if(true, s(X), Y, Z) :- ','(half(s(X), X1), ','(times(X1, Y, Y1), plus(Y1, Y1, Z))).
if(false, s(X), Y, Z) :- ','(times(X, Y, U), plus(Y, U, Z)).

Queries:

times(g,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

plus19(s(T49), T50, s(T52)) :- plus19(T49, T50, T52).
even36(s(s(T61)), X101) :- even36(T61, X101).
half60(s(s(T89)), s(X156)) :- half60(T89, X156).
times69(s(T104), T105, X182) :- even36(s(T104), X181).
times69(s(T117), T118, X217) :- ','(evenc36(s(T117), true), half60(s(T117), X215)).
times69(s(T117), T118, X217) :- ','(evenc36(s(T117), true), ','(halfc60(s(T117), T120), times69(T120, T118, X216))).
times69(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) :- ','(evenc36(s(T117), true), ','(halfc60(s(T117), T120), ','(timesc69(T120, T118, s(s(s(s(s(s(s(s(T150))))))))), plus154(T150, s(s(s(s(s(s(s(T150))))))), X411)))).
times69(s(T171), T172, X455) :- ','(evenc36(s(T171), false), times69(T171, T172, X454)).
times69(s(T171), T172, X455) :- ','(evenc36(s(T171), false), ','(timesc69(T171, T172, T175), plus166(T172, T175, X455))).
plus154(s(T163), T164, s(X436)) :- plus154(T163, T164, X436).
plus166(s(T189), T190, s(X482)) :- plus166(T189, T190, X482).
times1(s(0), T23, T25) :- ','(timesc18(T23, T29), plus19(T23, T29, T25)).
times1(s(s(T57)), T10, T12) :- even36(T57, X90).
times1(s(s(T86)), T78, T80) :- ','(evenc36(T86, true), half60(T86, X147)).
times1(s(s(T77)), T78, T80) :- ','(evenc36(T77, true), ','(halfc56(T77, T82), times69(T82, T78, X129))).
times1(s(s(T77)), T78, s(s(s(s(s(s(s(s(T248))))))))) :- ','(evenc36(T77, true), ','(halfc56(T77, T82), ','(timesc69(T82, T78, s(s(s(s(s(s(s(s(T246))))))))), plus19(T246, s(s(s(s(s(s(s(s(T246)))))))), T248)))).
times1(s(s(T258)), T259, T261) :- ','(evenc36(T258, false), times69(s(T258), T259, X662)).
times1(s(s(T258)), T259, T261) :- ','(evenc36(T258, false), ','(timesc69(s(T258), T259, T264), plus19(T259, T264, T261))).

Clauses:

plusc19(0, T42, T42).
plusc19(s(T49), T50, s(T52)) :- plusc19(T49, T50, T52).
evenc36(0, true).
evenc36(s(0), false).
evenc36(s(s(T61)), X101) :- evenc36(T61, X101).
halfc60(0, 0).
halfc60(s(s(T89)), s(X156)) :- halfc60(T89, X156).
timesc69(0, T99, 0).
timesc69(s(T117), T118, 0) :- ','(evenc36(s(T117), true), ','(halfc60(s(T117), T120), timesc69(T120, T118, 0))).
timesc69(s(T117), T118, s(s(0))) :- ','(evenc36(s(T117), true), ','(halfc60(s(T117), T120), timesc69(T120, T118, s(0)))).
timesc69(s(T117), T118, s(s(s(s(0))))) :- ','(evenc36(s(T117), true), ','(halfc60(s(T117), T120), timesc69(T120, T118, s(s(0))))).
timesc69(s(T117), T118, s(s(s(s(s(s(0))))))) :- ','(evenc36(s(T117), true), ','(halfc60(s(T117), T120), timesc69(T120, T118, s(s(s(0)))))).
timesc69(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) :- ','(evenc36(s(T117), true), ','(halfc60(s(T117), T120), timesc69(T120, T118, s(s(s(s(0))))))).
timesc69(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) :- ','(evenc36(s(T117), true), ','(halfc60(s(T117), T120), timesc69(T120, T118, s(s(s(s(s(0)))))))).
timesc69(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) :- ','(evenc36(s(T117), true), ','(halfc60(s(T117), T120), timesc69(T120, T118, s(s(s(s(s(s(0))))))))).
timesc69(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) :- ','(evenc36(s(T117), true), ','(halfc60(s(T117), T120), timesc69(T120, T118, s(s(s(s(s(s(s(0)))))))))).
timesc69(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) :- ','(evenc36(s(T117), true), ','(halfc60(s(T117), T120), ','(timesc69(T120, T118, s(s(s(s(s(s(s(s(T150))))))))), plusc154(T150, s(s(s(s(s(s(s(T150))))))), X411)))).
timesc69(s(T171), T172, X455) :- ','(evenc36(s(T171), false), ','(timesc69(T171, T172, T175), plusc166(T172, T175, X455))).
plusc154(0, T158, s(T158)).
plusc154(s(T163), T164, s(X436)) :- plusc154(T163, T164, X436).
plusc166(0, T184, T184).
plusc166(s(T189), T190, s(X482)) :- plusc166(T189, T190, X482).
timesc18(T35, 0).
halfc56(T86, s(X147)) :- halfc60(T86, X147).

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)
plus19_in: (b,b,f)
even36_in: (b,f)
evenc36_in: (b,b)
half60_in: (b,f)
halfc56_in: (b,f)
halfc60_in: (b,f)
times69_in: (b,b,f)
timesc69_in: (b,b,f) (b,b,b)
plusc166_in: (b,b,f) (b,b,b)
plusc154_in: (b,b,f) (b,b,b)
plus154_in: (b,b,f)
plus166_in: (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(s(0), T23, T25) → U19_GGA(T23, T25, timesc18_in_ga(T23, T29))
U19_GGA(T23, T25, timesc18_out_ga(T23, T29)) → U20_GGA(T23, T25, plus19_in_gga(T23, T29, T25))
U19_GGA(T23, T25, timesc18_out_ga(T23, T29)) → PLUS19_IN_GGA(T23, T29, T25)
PLUS19_IN_GGA(s(T49), T50, s(T52)) → U1_GGA(T49, T50, T52, plus19_in_gga(T49, T50, T52))
PLUS19_IN_GGA(s(T49), T50, s(T52)) → PLUS19_IN_GGA(T49, T50, T52)
TIMES1_IN_GGA(s(s(T57)), T10, T12) → U21_GGA(T57, T10, T12, even36_in_ga(T57, X90))
TIMES1_IN_GGA(s(s(T57)), T10, T12) → EVEN36_IN_GA(T57, X90)
EVEN36_IN_GA(s(s(T61)), X101) → U2_GA(T61, X101, even36_in_ga(T61, X101))
EVEN36_IN_GA(s(s(T61)), X101) → EVEN36_IN_GA(T61, X101)
TIMES1_IN_GGA(s(s(T86)), T78, T80) → U22_GGA(T86, T78, T80, evenc36_in_gg(T86, true))
U22_GGA(T86, T78, T80, evenc36_out_gg(T86, true)) → U23_GGA(T86, T78, T80, half60_in_ga(T86, X147))
U22_GGA(T86, T78, T80, evenc36_out_gg(T86, true)) → HALF60_IN_GA(T86, X147)
HALF60_IN_GA(s(s(T89)), s(X156)) → U3_GA(T89, X156, half60_in_ga(T89, X156))
HALF60_IN_GA(s(s(T89)), s(X156)) → HALF60_IN_GA(T89, X156)
TIMES1_IN_GGA(s(s(T77)), T78, T80) → U24_GGA(T77, T78, T80, evenc36_in_gg(T77, true))
U24_GGA(T77, T78, T80, evenc36_out_gg(T77, true)) → U25_GGA(T77, T78, T80, halfc56_in_ga(T77, T82))
U25_GGA(T77, T78, T80, halfc56_out_ga(T77, T82)) → U26_GGA(T77, T78, T80, times69_in_gga(T82, T78, X129))
U25_GGA(T77, T78, T80, halfc56_out_ga(T77, T82)) → TIMES69_IN_GGA(T82, T78, X129)
TIMES69_IN_GGA(s(T104), T105, X182) → U4_GGA(T104, T105, X182, even36_in_ga(s(T104), X181))
TIMES69_IN_GGA(s(T104), T105, X182) → EVEN36_IN_GA(s(T104), X181)
TIMES69_IN_GGA(s(T117), T118, X217) → U5_GGA(T117, T118, X217, evenc36_in_gg(s(T117), true))
U5_GGA(T117, T118, X217, evenc36_out_gg(s(T117), true)) → U6_GGA(T117, T118, X217, half60_in_ga(s(T117), X215))
U5_GGA(T117, T118, X217, evenc36_out_gg(s(T117), true)) → HALF60_IN_GA(s(T117), X215)
U5_GGA(T117, T118, X217, evenc36_out_gg(s(T117), true)) → U7_GGA(T117, T118, X217, halfc60_in_ga(s(T117), T120))
U7_GGA(T117, T118, X217, halfc60_out_ga(s(T117), T120)) → U8_GGA(T117, T118, X217, times69_in_gga(T120, T118, X216))
U7_GGA(T117, T118, X217, halfc60_out_ga(s(T117), T120)) → TIMES69_IN_GGA(T120, T118, X216)
TIMES69_IN_GGA(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U9_GGA(T117, T118, X411, evenc36_in_gg(s(T117), true))
U9_GGA(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U10_GGA(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U10_GGA(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U11_GGA(T117, T118, X411, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
U11_GGA(T117, T118, X411, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U12_GGA(T117, T118, X411, plus154_in_gga(T150, s(s(s(s(s(s(s(T150))))))), X411))
U11_GGA(T117, T118, X411, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → PLUS154_IN_GGA(T150, s(s(s(s(s(s(s(T150))))))), X411)
PLUS154_IN_GGA(s(T163), T164, s(X436)) → U17_GGA(T163, T164, X436, plus154_in_gga(T163, T164, X436))
PLUS154_IN_GGA(s(T163), T164, s(X436)) → PLUS154_IN_GGA(T163, T164, X436)
TIMES69_IN_GGA(s(T171), T172, X455) → U13_GGA(T171, T172, X455, evenc36_in_gg(s(T171), false))
U13_GGA(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U14_GGA(T171, T172, X455, times69_in_gga(T171, T172, X454))
U13_GGA(T171, T172, X455, evenc36_out_gg(s(T171), false)) → TIMES69_IN_GGA(T171, T172, X454)
U13_GGA(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U15_GGA(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
U15_GGA(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U16_GGA(T171, T172, X455, plus166_in_gga(T172, T175, X455))
U15_GGA(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → PLUS166_IN_GGA(T172, T175, X455)
PLUS166_IN_GGA(s(T189), T190, s(X482)) → U18_GGA(T189, T190, X482, plus166_in_gga(T189, T190, X482))
PLUS166_IN_GGA(s(T189), T190, s(X482)) → PLUS166_IN_GGA(T189, T190, X482)
TIMES1_IN_GGA(s(s(T77)), T78, s(s(s(s(s(s(s(s(T248))))))))) → U27_GGA(T77, T78, T248, evenc36_in_gg(T77, true))
U27_GGA(T77, T78, T248, evenc36_out_gg(T77, true)) → U28_GGA(T77, T78, T248, halfc56_in_ga(T77, T82))
U28_GGA(T77, T78, T248, halfc56_out_ga(T77, T82)) → U29_GGA(T77, T78, T248, timesc69_in_gga(T82, T78, s(s(s(s(s(s(s(s(T246))))))))))
U29_GGA(T77, T78, T248, timesc69_out_gga(T82, T78, s(s(s(s(s(s(s(s(T246)))))))))) → U30_GGA(T77, T78, T248, plus19_in_gga(T246, s(s(s(s(s(s(s(s(T246)))))))), T248))
U29_GGA(T77, T78, T248, timesc69_out_gga(T82, T78, s(s(s(s(s(s(s(s(T246)))))))))) → PLUS19_IN_GGA(T246, s(s(s(s(s(s(s(s(T246)))))))), T248)
TIMES1_IN_GGA(s(s(T258)), T259, T261) → U31_GGA(T258, T259, T261, evenc36_in_gg(T258, false))
U31_GGA(T258, T259, T261, evenc36_out_gg(T258, false)) → U32_GGA(T258, T259, T261, times69_in_gga(s(T258), T259, X662))
U31_GGA(T258, T259, T261, evenc36_out_gg(T258, false)) → TIMES69_IN_GGA(s(T258), T259, X662)
U31_GGA(T258, T259, T261, evenc36_out_gg(T258, false)) → U33_GGA(T258, T259, T261, timesc69_in_gga(s(T258), T259, T264))
U33_GGA(T258, T259, T261, timesc69_out_gga(s(T258), T259, T264)) → U34_GGA(T258, T259, T261, plus19_in_gga(T259, T264, T261))
U33_GGA(T258, T259, T261, timesc69_out_gga(s(T258), T259, T264)) → PLUS19_IN_GGA(T259, T264, T261)

The TRS R consists of the following rules:

timesc18_in_ga(T35, 0) → timesc18_out_ga(T35, 0)
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
halfc56_in_ga(T86, s(X147)) → U72_ga(T86, X147, halfc60_in_ga(T86, X147))
halfc60_in_ga(0, 0) → halfc60_out_ga(0, 0)
halfc60_in_ga(s(s(T89)), s(X156)) → U38_ga(T89, X156, halfc60_in_ga(T89, X156))
U38_ga(T89, X156, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
U72_ga(T86, X147, halfc60_out_ga(T86, X147)) → halfc56_out_ga(T86, s(X147))
timesc69_in_gga(0, T99, 0) → timesc69_out_gga(0, T99, 0)
timesc69_in_gga(s(T117), T118, 0) → U39_gga(T117, T118, evenc36_in_gg(s(T117), true))
U39_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U40_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U40_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_gga(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(0, T99, 0) → timesc69_out_ggg(0, T99, 0)
timesc69_in_ggg(s(T117), T118, 0) → U39_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U39_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U40_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U40_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_ggg(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(s(T117), T118, s(s(0))) → U42_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U42_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U43_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U43_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T117), T118, s(s(s(s(0))))) → U45_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U45_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U46_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U46_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U48_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U49_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U49_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U51_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U52_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U52_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U54_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U55_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U55_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U57_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U58_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U58_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U60_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U61_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U61_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_ggg(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_ggg(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_ggg(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_ggg(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_ggg(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T117), T118, s(s(0))) → U42_gga(T117, T118, evenc36_in_gg(s(T117), true))
U42_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U43_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U43_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_gga(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T171), T172, X455) → U67_ggg(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_ggg(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_ggg(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
timesc69_in_gga(s(T117), T118, s(s(s(s(0))))) → U45_gga(T117, T118, evenc36_in_gg(s(T117), true))
U45_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U46_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U46_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
U47_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_gga(s(T117), T118, s(s(s(s(0)))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_gga(T117, T118, evenc36_in_gg(s(T117), true))
U48_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U49_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U49_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
U50_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(0)))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_gga(T117, T118, evenc36_in_gg(s(T117), true))
U51_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U52_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U52_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
U53_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_gga(T117, T118, evenc36_in_gg(s(T117), true))
U54_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U55_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U55_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
U56_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_gga(T117, T118, evenc36_in_gg(s(T117), true))
U57_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U58_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U58_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
U59_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_gga(T117, T118, evenc36_in_gg(s(T117), true))
U60_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U61_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U61_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
U62_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_gga(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_gga(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_gga(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_gga(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_gga(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T171), T172, X455) → U67_gga(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_gga(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_gga(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
U68_gga(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_gga(T171, T172, X455, plusc166_in_gga(T172, T175, X455))
plusc166_in_gga(0, T184, T184) → plusc166_out_gga(0, T184, T184)
plusc166_in_gga(s(T189), T190, s(X482)) → U71_gga(T189, T190, X482, plusc166_in_gga(T189, T190, X482))
U71_gga(T189, T190, X482, plusc166_out_gga(T189, T190, X482)) → plusc166_out_gga(s(T189), T190, s(X482))
U69_gga(T171, T172, X455, plusc166_out_gga(T172, T175, X455)) → timesc69_out_gga(s(T171), T172, X455)
U65_gga(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_gga(T117, T118, X411, plusc154_in_gga(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_gga(0, T158, s(T158)) → plusc154_out_gga(0, T158, s(T158))
plusc154_in_gga(s(T163), T164, s(X436)) → U70_gga(T163, T164, X436, plusc154_in_gga(T163, T164, X436))
U70_gga(T163, T164, X436, plusc154_out_gga(T163, T164, X436)) → plusc154_out_gga(s(T163), T164, s(X436))
U66_gga(T117, T118, X411, plusc154_out_gga(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U68_ggg(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_ggg(T171, T172, X455, plusc166_in_ggg(T172, T175, X455))
plusc166_in_ggg(0, T184, T184) → plusc166_out_ggg(0, T184, T184)
plusc166_in_ggg(s(T189), T190, s(X482)) → U71_ggg(T189, T190, X482, plusc166_in_ggg(T189, T190, X482))
U71_ggg(T189, T190, X482, plusc166_out_ggg(T189, T190, X482)) → plusc166_out_ggg(s(T189), T190, s(X482))
U69_ggg(T171, T172, X455, plusc166_out_ggg(T172, T175, X455)) → timesc69_out_ggg(s(T171), T172, X455)
U44_gga(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_gga(s(T117), T118, s(s(0)))
U65_ggg(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_ggg(T117, T118, X411, plusc154_in_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_ggg(0, T158, s(T158)) → plusc154_out_ggg(0, T158, s(T158))
plusc154_in_ggg(s(T163), T164, s(X436)) → U70_ggg(T163, T164, X436, plusc154_in_ggg(T163, T164, X436))
U70_ggg(T163, T164, X436, plusc154_out_ggg(T163, T164, X436)) → plusc154_out_ggg(s(T163), T164, s(X436))
U66_ggg(T117, T118, X411, plusc154_out_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U62_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U59_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U56_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U53_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
U50_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(0)))))))
U47_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(0)))))
U44_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_ggg(s(T117), T118, s(s(0)))
U41_ggg(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_ggg(s(T117), T118, 0)
U41_gga(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_gga(s(T117), T118, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timesc18_in_ga(x1, x2)  =  timesc18_in_ga(x1)
timesc18_out_ga(x1, x2)  =  timesc18_out_ga(x1, x2)
plus19_in_gga(x1, x2, x3)  =  plus19_in_gga(x1, x2)
even36_in_ga(x1, x2)  =  even36_in_ga(x1)
evenc36_in_gg(x1, x2)  =  evenc36_in_gg(x1, x2)
true  =  true
evenc36_out_gg(x1, x2)  =  evenc36_out_gg(x1, x2)
false  =  false
U37_gg(x1, x2, x3)  =  U37_gg(x1, x2, x3)
half60_in_ga(x1, x2)  =  half60_in_ga(x1)
halfc56_in_ga(x1, x2)  =  halfc56_in_ga(x1)
U72_ga(x1, x2, x3)  =  U72_ga(x1, x3)
halfc60_in_ga(x1, x2)  =  halfc60_in_ga(x1)
halfc60_out_ga(x1, x2)  =  halfc60_out_ga(x1, x2)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
halfc56_out_ga(x1, x2)  =  halfc56_out_ga(x1, x2)
times69_in_gga(x1, x2, x3)  =  times69_in_gga(x1, x2)
timesc69_in_gga(x1, x2, x3)  =  timesc69_in_gga(x1, x2)
timesc69_out_gga(x1, x2, x3)  =  timesc69_out_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
timesc69_in_ggg(x1, x2, x3)  =  timesc69_in_ggg(x1, x2, x3)
timesc69_out_ggg(x1, x2, x3)  =  timesc69_out_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3)  =  U62_ggg(x1, x2, x3)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4, x5)  =  U65_ggg(x1, x2, x3, x5)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3)  =  U62_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4, x5)  =  U65_gga(x1, x2, x5)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
plusc166_in_gga(x1, x2, x3)  =  plusc166_in_gga(x1, x2)
plusc166_out_gga(x1, x2, x3)  =  plusc166_out_gga(x1, x2, x3)
U71_gga(x1, x2, x3, x4)  =  U71_gga(x1, x2, x4)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
plusc154_in_gga(x1, x2, x3)  =  plusc154_in_gga(x1, x2)
plusc154_out_gga(x1, x2, x3)  =  plusc154_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
plusc166_in_ggg(x1, x2, x3)  =  plusc166_in_ggg(x1, x2, x3)
plusc166_out_ggg(x1, x2, x3)  =  plusc166_out_ggg(x1, x2, x3)
U71_ggg(x1, x2, x3, x4)  =  U71_ggg(x1, x2, x3, x4)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
plusc154_in_ggg(x1, x2, x3)  =  plusc154_in_ggg(x1, x2, x3)
plusc154_out_ggg(x1, x2, x3)  =  plusc154_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
plus154_in_gga(x1, x2, x3)  =  plus154_in_gga(x1, x2)
plus166_in_gga(x1, x2, x3)  =  plus166_in_gga(x1, x2)
TIMES1_IN_GGA(x1, x2, x3)  =  TIMES1_IN_GGA(x1, x2)
U19_GGA(x1, x2, x3)  =  U19_GGA(x1, x3)
U20_GGA(x1, x2, x3)  =  U20_GGA(x1, x3)
PLUS19_IN_GGA(x1, x2, x3)  =  PLUS19_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U21_GGA(x1, x2, x3, x4)  =  U21_GGA(x1, x2, x4)
EVEN36_IN_GA(x1, x2)  =  EVEN36_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
HALF60_IN_GA(x1, x2)  =  HALF60_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x1, x2, x4)
TIMES69_IN_GGA(x1, x2, x3)  =  TIMES69_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
PLUS154_IN_GGA(x1, x2, x3)  =  PLUS154_IN_GGA(x1, x2)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x1, x2, x4)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
PLUS166_IN_GGA(x1, x2, x3)  =  PLUS166_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4)  =  U28_GGA(x1, x2, x4)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x1, x2, x4)
U30_GGA(x1, x2, x3, x4)  =  U30_GGA(x1, x2, x4)
U31_GGA(x1, x2, x3, x4)  =  U31_GGA(x1, x2, x4)
U32_GGA(x1, x2, x3, x4)  =  U32_GGA(x1, x2, x4)
U33_GGA(x1, x2, x3, x4)  =  U33_GGA(x1, x2, x4)
U34_GGA(x1, x2, x3, x4)  =  U34_GGA(x1, x2, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

TIMES1_IN_GGA(s(0), T23, T25) → U19_GGA(T23, T25, timesc18_in_ga(T23, T29))
U19_GGA(T23, T25, timesc18_out_ga(T23, T29)) → U20_GGA(T23, T25, plus19_in_gga(T23, T29, T25))
U19_GGA(T23, T25, timesc18_out_ga(T23, T29)) → PLUS19_IN_GGA(T23, T29, T25)
PLUS19_IN_GGA(s(T49), T50, s(T52)) → U1_GGA(T49, T50, T52, plus19_in_gga(T49, T50, T52))
PLUS19_IN_GGA(s(T49), T50, s(T52)) → PLUS19_IN_GGA(T49, T50, T52)
TIMES1_IN_GGA(s(s(T57)), T10, T12) → U21_GGA(T57, T10, T12, even36_in_ga(T57, X90))
TIMES1_IN_GGA(s(s(T57)), T10, T12) → EVEN36_IN_GA(T57, X90)
EVEN36_IN_GA(s(s(T61)), X101) → U2_GA(T61, X101, even36_in_ga(T61, X101))
EVEN36_IN_GA(s(s(T61)), X101) → EVEN36_IN_GA(T61, X101)
TIMES1_IN_GGA(s(s(T86)), T78, T80) → U22_GGA(T86, T78, T80, evenc36_in_gg(T86, true))
U22_GGA(T86, T78, T80, evenc36_out_gg(T86, true)) → U23_GGA(T86, T78, T80, half60_in_ga(T86, X147))
U22_GGA(T86, T78, T80, evenc36_out_gg(T86, true)) → HALF60_IN_GA(T86, X147)
HALF60_IN_GA(s(s(T89)), s(X156)) → U3_GA(T89, X156, half60_in_ga(T89, X156))
HALF60_IN_GA(s(s(T89)), s(X156)) → HALF60_IN_GA(T89, X156)
TIMES1_IN_GGA(s(s(T77)), T78, T80) → U24_GGA(T77, T78, T80, evenc36_in_gg(T77, true))
U24_GGA(T77, T78, T80, evenc36_out_gg(T77, true)) → U25_GGA(T77, T78, T80, halfc56_in_ga(T77, T82))
U25_GGA(T77, T78, T80, halfc56_out_ga(T77, T82)) → U26_GGA(T77, T78, T80, times69_in_gga(T82, T78, X129))
U25_GGA(T77, T78, T80, halfc56_out_ga(T77, T82)) → TIMES69_IN_GGA(T82, T78, X129)
TIMES69_IN_GGA(s(T104), T105, X182) → U4_GGA(T104, T105, X182, even36_in_ga(s(T104), X181))
TIMES69_IN_GGA(s(T104), T105, X182) → EVEN36_IN_GA(s(T104), X181)
TIMES69_IN_GGA(s(T117), T118, X217) → U5_GGA(T117, T118, X217, evenc36_in_gg(s(T117), true))
U5_GGA(T117, T118, X217, evenc36_out_gg(s(T117), true)) → U6_GGA(T117, T118, X217, half60_in_ga(s(T117), X215))
U5_GGA(T117, T118, X217, evenc36_out_gg(s(T117), true)) → HALF60_IN_GA(s(T117), X215)
U5_GGA(T117, T118, X217, evenc36_out_gg(s(T117), true)) → U7_GGA(T117, T118, X217, halfc60_in_ga(s(T117), T120))
U7_GGA(T117, T118, X217, halfc60_out_ga(s(T117), T120)) → U8_GGA(T117, T118, X217, times69_in_gga(T120, T118, X216))
U7_GGA(T117, T118, X217, halfc60_out_ga(s(T117), T120)) → TIMES69_IN_GGA(T120, T118, X216)
TIMES69_IN_GGA(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U9_GGA(T117, T118, X411, evenc36_in_gg(s(T117), true))
U9_GGA(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U10_GGA(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U10_GGA(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U11_GGA(T117, T118, X411, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
U11_GGA(T117, T118, X411, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U12_GGA(T117, T118, X411, plus154_in_gga(T150, s(s(s(s(s(s(s(T150))))))), X411))
U11_GGA(T117, T118, X411, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → PLUS154_IN_GGA(T150, s(s(s(s(s(s(s(T150))))))), X411)
PLUS154_IN_GGA(s(T163), T164, s(X436)) → U17_GGA(T163, T164, X436, plus154_in_gga(T163, T164, X436))
PLUS154_IN_GGA(s(T163), T164, s(X436)) → PLUS154_IN_GGA(T163, T164, X436)
TIMES69_IN_GGA(s(T171), T172, X455) → U13_GGA(T171, T172, X455, evenc36_in_gg(s(T171), false))
U13_GGA(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U14_GGA(T171, T172, X455, times69_in_gga(T171, T172, X454))
U13_GGA(T171, T172, X455, evenc36_out_gg(s(T171), false)) → TIMES69_IN_GGA(T171, T172, X454)
U13_GGA(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U15_GGA(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
U15_GGA(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U16_GGA(T171, T172, X455, plus166_in_gga(T172, T175, X455))
U15_GGA(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → PLUS166_IN_GGA(T172, T175, X455)
PLUS166_IN_GGA(s(T189), T190, s(X482)) → U18_GGA(T189, T190, X482, plus166_in_gga(T189, T190, X482))
PLUS166_IN_GGA(s(T189), T190, s(X482)) → PLUS166_IN_GGA(T189, T190, X482)
TIMES1_IN_GGA(s(s(T77)), T78, s(s(s(s(s(s(s(s(T248))))))))) → U27_GGA(T77, T78, T248, evenc36_in_gg(T77, true))
U27_GGA(T77, T78, T248, evenc36_out_gg(T77, true)) → U28_GGA(T77, T78, T248, halfc56_in_ga(T77, T82))
U28_GGA(T77, T78, T248, halfc56_out_ga(T77, T82)) → U29_GGA(T77, T78, T248, timesc69_in_gga(T82, T78, s(s(s(s(s(s(s(s(T246))))))))))
U29_GGA(T77, T78, T248, timesc69_out_gga(T82, T78, s(s(s(s(s(s(s(s(T246)))))))))) → U30_GGA(T77, T78, T248, plus19_in_gga(T246, s(s(s(s(s(s(s(s(T246)))))))), T248))
U29_GGA(T77, T78, T248, timesc69_out_gga(T82, T78, s(s(s(s(s(s(s(s(T246)))))))))) → PLUS19_IN_GGA(T246, s(s(s(s(s(s(s(s(T246)))))))), T248)
TIMES1_IN_GGA(s(s(T258)), T259, T261) → U31_GGA(T258, T259, T261, evenc36_in_gg(T258, false))
U31_GGA(T258, T259, T261, evenc36_out_gg(T258, false)) → U32_GGA(T258, T259, T261, times69_in_gga(s(T258), T259, X662))
U31_GGA(T258, T259, T261, evenc36_out_gg(T258, false)) → TIMES69_IN_GGA(s(T258), T259, X662)
U31_GGA(T258, T259, T261, evenc36_out_gg(T258, false)) → U33_GGA(T258, T259, T261, timesc69_in_gga(s(T258), T259, T264))
U33_GGA(T258, T259, T261, timesc69_out_gga(s(T258), T259, T264)) → U34_GGA(T258, T259, T261, plus19_in_gga(T259, T264, T261))
U33_GGA(T258, T259, T261, timesc69_out_gga(s(T258), T259, T264)) → PLUS19_IN_GGA(T259, T264, T261)

The TRS R consists of the following rules:

timesc18_in_ga(T35, 0) → timesc18_out_ga(T35, 0)
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
halfc56_in_ga(T86, s(X147)) → U72_ga(T86, X147, halfc60_in_ga(T86, X147))
halfc60_in_ga(0, 0) → halfc60_out_ga(0, 0)
halfc60_in_ga(s(s(T89)), s(X156)) → U38_ga(T89, X156, halfc60_in_ga(T89, X156))
U38_ga(T89, X156, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
U72_ga(T86, X147, halfc60_out_ga(T86, X147)) → halfc56_out_ga(T86, s(X147))
timesc69_in_gga(0, T99, 0) → timesc69_out_gga(0, T99, 0)
timesc69_in_gga(s(T117), T118, 0) → U39_gga(T117, T118, evenc36_in_gg(s(T117), true))
U39_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U40_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U40_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_gga(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(0, T99, 0) → timesc69_out_ggg(0, T99, 0)
timesc69_in_ggg(s(T117), T118, 0) → U39_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U39_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U40_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U40_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_ggg(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(s(T117), T118, s(s(0))) → U42_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U42_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U43_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U43_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T117), T118, s(s(s(s(0))))) → U45_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U45_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U46_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U46_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U48_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U49_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U49_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U51_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U52_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U52_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U54_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U55_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U55_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U57_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U58_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U58_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U60_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U61_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U61_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_ggg(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_ggg(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_ggg(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_ggg(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_ggg(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T117), T118, s(s(0))) → U42_gga(T117, T118, evenc36_in_gg(s(T117), true))
U42_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U43_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U43_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_gga(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T171), T172, X455) → U67_ggg(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_ggg(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_ggg(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
timesc69_in_gga(s(T117), T118, s(s(s(s(0))))) → U45_gga(T117, T118, evenc36_in_gg(s(T117), true))
U45_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U46_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U46_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
U47_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_gga(s(T117), T118, s(s(s(s(0)))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_gga(T117, T118, evenc36_in_gg(s(T117), true))
U48_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U49_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U49_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
U50_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(0)))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_gga(T117, T118, evenc36_in_gg(s(T117), true))
U51_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U52_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U52_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
U53_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_gga(T117, T118, evenc36_in_gg(s(T117), true))
U54_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U55_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U55_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
U56_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_gga(T117, T118, evenc36_in_gg(s(T117), true))
U57_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U58_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U58_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
U59_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_gga(T117, T118, evenc36_in_gg(s(T117), true))
U60_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U61_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U61_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
U62_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_gga(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_gga(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_gga(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_gga(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_gga(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T171), T172, X455) → U67_gga(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_gga(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_gga(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
U68_gga(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_gga(T171, T172, X455, plusc166_in_gga(T172, T175, X455))
plusc166_in_gga(0, T184, T184) → plusc166_out_gga(0, T184, T184)
plusc166_in_gga(s(T189), T190, s(X482)) → U71_gga(T189, T190, X482, plusc166_in_gga(T189, T190, X482))
U71_gga(T189, T190, X482, plusc166_out_gga(T189, T190, X482)) → plusc166_out_gga(s(T189), T190, s(X482))
U69_gga(T171, T172, X455, plusc166_out_gga(T172, T175, X455)) → timesc69_out_gga(s(T171), T172, X455)
U65_gga(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_gga(T117, T118, X411, plusc154_in_gga(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_gga(0, T158, s(T158)) → plusc154_out_gga(0, T158, s(T158))
plusc154_in_gga(s(T163), T164, s(X436)) → U70_gga(T163, T164, X436, plusc154_in_gga(T163, T164, X436))
U70_gga(T163, T164, X436, plusc154_out_gga(T163, T164, X436)) → plusc154_out_gga(s(T163), T164, s(X436))
U66_gga(T117, T118, X411, plusc154_out_gga(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U68_ggg(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_ggg(T171, T172, X455, plusc166_in_ggg(T172, T175, X455))
plusc166_in_ggg(0, T184, T184) → plusc166_out_ggg(0, T184, T184)
plusc166_in_ggg(s(T189), T190, s(X482)) → U71_ggg(T189, T190, X482, plusc166_in_ggg(T189, T190, X482))
U71_ggg(T189, T190, X482, plusc166_out_ggg(T189, T190, X482)) → plusc166_out_ggg(s(T189), T190, s(X482))
U69_ggg(T171, T172, X455, plusc166_out_ggg(T172, T175, X455)) → timesc69_out_ggg(s(T171), T172, X455)
U44_gga(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_gga(s(T117), T118, s(s(0)))
U65_ggg(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_ggg(T117, T118, X411, plusc154_in_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_ggg(0, T158, s(T158)) → plusc154_out_ggg(0, T158, s(T158))
plusc154_in_ggg(s(T163), T164, s(X436)) → U70_ggg(T163, T164, X436, plusc154_in_ggg(T163, T164, X436))
U70_ggg(T163, T164, X436, plusc154_out_ggg(T163, T164, X436)) → plusc154_out_ggg(s(T163), T164, s(X436))
U66_ggg(T117, T118, X411, plusc154_out_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U62_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U59_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U56_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U53_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
U50_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(0)))))))
U47_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(0)))))
U44_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_ggg(s(T117), T118, s(s(0)))
U41_ggg(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_ggg(s(T117), T118, 0)
U41_gga(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_gga(s(T117), T118, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timesc18_in_ga(x1, x2)  =  timesc18_in_ga(x1)
timesc18_out_ga(x1, x2)  =  timesc18_out_ga(x1, x2)
plus19_in_gga(x1, x2, x3)  =  plus19_in_gga(x1, x2)
even36_in_ga(x1, x2)  =  even36_in_ga(x1)
evenc36_in_gg(x1, x2)  =  evenc36_in_gg(x1, x2)
true  =  true
evenc36_out_gg(x1, x2)  =  evenc36_out_gg(x1, x2)
false  =  false
U37_gg(x1, x2, x3)  =  U37_gg(x1, x2, x3)
half60_in_ga(x1, x2)  =  half60_in_ga(x1)
halfc56_in_ga(x1, x2)  =  halfc56_in_ga(x1)
U72_ga(x1, x2, x3)  =  U72_ga(x1, x3)
halfc60_in_ga(x1, x2)  =  halfc60_in_ga(x1)
halfc60_out_ga(x1, x2)  =  halfc60_out_ga(x1, x2)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
halfc56_out_ga(x1, x2)  =  halfc56_out_ga(x1, x2)
times69_in_gga(x1, x2, x3)  =  times69_in_gga(x1, x2)
timesc69_in_gga(x1, x2, x3)  =  timesc69_in_gga(x1, x2)
timesc69_out_gga(x1, x2, x3)  =  timesc69_out_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
timesc69_in_ggg(x1, x2, x3)  =  timesc69_in_ggg(x1, x2, x3)
timesc69_out_ggg(x1, x2, x3)  =  timesc69_out_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3)  =  U62_ggg(x1, x2, x3)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4, x5)  =  U65_ggg(x1, x2, x3, x5)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3)  =  U62_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4, x5)  =  U65_gga(x1, x2, x5)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
plusc166_in_gga(x1, x2, x3)  =  plusc166_in_gga(x1, x2)
plusc166_out_gga(x1, x2, x3)  =  plusc166_out_gga(x1, x2, x3)
U71_gga(x1, x2, x3, x4)  =  U71_gga(x1, x2, x4)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
plusc154_in_gga(x1, x2, x3)  =  plusc154_in_gga(x1, x2)
plusc154_out_gga(x1, x2, x3)  =  plusc154_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
plusc166_in_ggg(x1, x2, x3)  =  plusc166_in_ggg(x1, x2, x3)
plusc166_out_ggg(x1, x2, x3)  =  plusc166_out_ggg(x1, x2, x3)
U71_ggg(x1, x2, x3, x4)  =  U71_ggg(x1, x2, x3, x4)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
plusc154_in_ggg(x1, x2, x3)  =  plusc154_in_ggg(x1, x2, x3)
plusc154_out_ggg(x1, x2, x3)  =  plusc154_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
plus154_in_gga(x1, x2, x3)  =  plus154_in_gga(x1, x2)
plus166_in_gga(x1, x2, x3)  =  plus166_in_gga(x1, x2)
TIMES1_IN_GGA(x1, x2, x3)  =  TIMES1_IN_GGA(x1, x2)
U19_GGA(x1, x2, x3)  =  U19_GGA(x1, x3)
U20_GGA(x1, x2, x3)  =  U20_GGA(x1, x3)
PLUS19_IN_GGA(x1, x2, x3)  =  PLUS19_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U21_GGA(x1, x2, x3, x4)  =  U21_GGA(x1, x2, x4)
EVEN36_IN_GA(x1, x2)  =  EVEN36_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
HALF60_IN_GA(x1, x2)  =  HALF60_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x1, x2, x4)
TIMES69_IN_GGA(x1, x2, x3)  =  TIMES69_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
PLUS154_IN_GGA(x1, x2, x3)  =  PLUS154_IN_GGA(x1, x2)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x1, x2, x4)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
PLUS166_IN_GGA(x1, x2, x3)  =  PLUS166_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4)  =  U28_GGA(x1, x2, x4)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x1, x2, x4)
U30_GGA(x1, x2, x3, x4)  =  U30_GGA(x1, x2, x4)
U31_GGA(x1, x2, x3, x4)  =  U31_GGA(x1, x2, x4)
U32_GGA(x1, x2, x3, x4)  =  U32_GGA(x1, x2, x4)
U33_GGA(x1, x2, x3, x4)  =  U33_GGA(x1, x2, x4)
U34_GGA(x1, x2, x3, x4)  =  U34_GGA(x1, x2, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 42 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

PLUS166_IN_GGA(s(T189), T190, s(X482)) → PLUS166_IN_GGA(T189, T190, X482)

The TRS R consists of the following rules:

timesc18_in_ga(T35, 0) → timesc18_out_ga(T35, 0)
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
halfc56_in_ga(T86, s(X147)) → U72_ga(T86, X147, halfc60_in_ga(T86, X147))
halfc60_in_ga(0, 0) → halfc60_out_ga(0, 0)
halfc60_in_ga(s(s(T89)), s(X156)) → U38_ga(T89, X156, halfc60_in_ga(T89, X156))
U38_ga(T89, X156, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
U72_ga(T86, X147, halfc60_out_ga(T86, X147)) → halfc56_out_ga(T86, s(X147))
timesc69_in_gga(0, T99, 0) → timesc69_out_gga(0, T99, 0)
timesc69_in_gga(s(T117), T118, 0) → U39_gga(T117, T118, evenc36_in_gg(s(T117), true))
U39_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U40_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U40_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_gga(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(0, T99, 0) → timesc69_out_ggg(0, T99, 0)
timesc69_in_ggg(s(T117), T118, 0) → U39_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U39_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U40_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U40_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_ggg(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(s(T117), T118, s(s(0))) → U42_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U42_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U43_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U43_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T117), T118, s(s(s(s(0))))) → U45_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U45_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U46_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U46_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U48_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U49_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U49_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U51_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U52_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U52_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U54_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U55_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U55_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U57_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U58_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U58_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U60_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U61_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U61_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_ggg(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_ggg(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_ggg(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_ggg(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_ggg(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T117), T118, s(s(0))) → U42_gga(T117, T118, evenc36_in_gg(s(T117), true))
U42_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U43_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U43_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_gga(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T171), T172, X455) → U67_ggg(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_ggg(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_ggg(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
timesc69_in_gga(s(T117), T118, s(s(s(s(0))))) → U45_gga(T117, T118, evenc36_in_gg(s(T117), true))
U45_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U46_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U46_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
U47_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_gga(s(T117), T118, s(s(s(s(0)))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_gga(T117, T118, evenc36_in_gg(s(T117), true))
U48_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U49_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U49_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
U50_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(0)))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_gga(T117, T118, evenc36_in_gg(s(T117), true))
U51_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U52_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U52_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
U53_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_gga(T117, T118, evenc36_in_gg(s(T117), true))
U54_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U55_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U55_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
U56_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_gga(T117, T118, evenc36_in_gg(s(T117), true))
U57_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U58_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U58_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
U59_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_gga(T117, T118, evenc36_in_gg(s(T117), true))
U60_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U61_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U61_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
U62_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_gga(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_gga(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_gga(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_gga(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_gga(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T171), T172, X455) → U67_gga(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_gga(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_gga(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
U68_gga(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_gga(T171, T172, X455, plusc166_in_gga(T172, T175, X455))
plusc166_in_gga(0, T184, T184) → plusc166_out_gga(0, T184, T184)
plusc166_in_gga(s(T189), T190, s(X482)) → U71_gga(T189, T190, X482, plusc166_in_gga(T189, T190, X482))
U71_gga(T189, T190, X482, plusc166_out_gga(T189, T190, X482)) → plusc166_out_gga(s(T189), T190, s(X482))
U69_gga(T171, T172, X455, plusc166_out_gga(T172, T175, X455)) → timesc69_out_gga(s(T171), T172, X455)
U65_gga(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_gga(T117, T118, X411, plusc154_in_gga(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_gga(0, T158, s(T158)) → plusc154_out_gga(0, T158, s(T158))
plusc154_in_gga(s(T163), T164, s(X436)) → U70_gga(T163, T164, X436, plusc154_in_gga(T163, T164, X436))
U70_gga(T163, T164, X436, plusc154_out_gga(T163, T164, X436)) → plusc154_out_gga(s(T163), T164, s(X436))
U66_gga(T117, T118, X411, plusc154_out_gga(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U68_ggg(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_ggg(T171, T172, X455, plusc166_in_ggg(T172, T175, X455))
plusc166_in_ggg(0, T184, T184) → plusc166_out_ggg(0, T184, T184)
plusc166_in_ggg(s(T189), T190, s(X482)) → U71_ggg(T189, T190, X482, plusc166_in_ggg(T189, T190, X482))
U71_ggg(T189, T190, X482, plusc166_out_ggg(T189, T190, X482)) → plusc166_out_ggg(s(T189), T190, s(X482))
U69_ggg(T171, T172, X455, plusc166_out_ggg(T172, T175, X455)) → timesc69_out_ggg(s(T171), T172, X455)
U44_gga(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_gga(s(T117), T118, s(s(0)))
U65_ggg(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_ggg(T117, T118, X411, plusc154_in_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_ggg(0, T158, s(T158)) → plusc154_out_ggg(0, T158, s(T158))
plusc154_in_ggg(s(T163), T164, s(X436)) → U70_ggg(T163, T164, X436, plusc154_in_ggg(T163, T164, X436))
U70_ggg(T163, T164, X436, plusc154_out_ggg(T163, T164, X436)) → plusc154_out_ggg(s(T163), T164, s(X436))
U66_ggg(T117, T118, X411, plusc154_out_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U62_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U59_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U56_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U53_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
U50_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(0)))))))
U47_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(0)))))
U44_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_ggg(s(T117), T118, s(s(0)))
U41_ggg(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_ggg(s(T117), T118, 0)
U41_gga(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_gga(s(T117), T118, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timesc18_in_ga(x1, x2)  =  timesc18_in_ga(x1)
timesc18_out_ga(x1, x2)  =  timesc18_out_ga(x1, x2)
evenc36_in_gg(x1, x2)  =  evenc36_in_gg(x1, x2)
true  =  true
evenc36_out_gg(x1, x2)  =  evenc36_out_gg(x1, x2)
false  =  false
U37_gg(x1, x2, x3)  =  U37_gg(x1, x2, x3)
halfc56_in_ga(x1, x2)  =  halfc56_in_ga(x1)
U72_ga(x1, x2, x3)  =  U72_ga(x1, x3)
halfc60_in_ga(x1, x2)  =  halfc60_in_ga(x1)
halfc60_out_ga(x1, x2)  =  halfc60_out_ga(x1, x2)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
halfc56_out_ga(x1, x2)  =  halfc56_out_ga(x1, x2)
timesc69_in_gga(x1, x2, x3)  =  timesc69_in_gga(x1, x2)
timesc69_out_gga(x1, x2, x3)  =  timesc69_out_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
timesc69_in_ggg(x1, x2, x3)  =  timesc69_in_ggg(x1, x2, x3)
timesc69_out_ggg(x1, x2, x3)  =  timesc69_out_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3)  =  U62_ggg(x1, x2, x3)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4, x5)  =  U65_ggg(x1, x2, x3, x5)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3)  =  U62_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4, x5)  =  U65_gga(x1, x2, x5)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
plusc166_in_gga(x1, x2, x3)  =  plusc166_in_gga(x1, x2)
plusc166_out_gga(x1, x2, x3)  =  plusc166_out_gga(x1, x2, x3)
U71_gga(x1, x2, x3, x4)  =  U71_gga(x1, x2, x4)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
plusc154_in_gga(x1, x2, x3)  =  plusc154_in_gga(x1, x2)
plusc154_out_gga(x1, x2, x3)  =  plusc154_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
plusc166_in_ggg(x1, x2, x3)  =  plusc166_in_ggg(x1, x2, x3)
plusc166_out_ggg(x1, x2, x3)  =  plusc166_out_ggg(x1, x2, x3)
U71_ggg(x1, x2, x3, x4)  =  U71_ggg(x1, x2, x3, x4)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
plusc154_in_ggg(x1, x2, x3)  =  plusc154_in_ggg(x1, x2, x3)
plusc154_out_ggg(x1, x2, x3)  =  plusc154_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
PLUS166_IN_GGA(x1, x2, x3)  =  PLUS166_IN_GGA(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

PLUS166_IN_GGA(s(T189), T190, s(X482)) → PLUS166_IN_GGA(T189, T190, X482)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

PLUS166_IN_GGA(s(T189), T190) → PLUS166_IN_GGA(T189, T190)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PLUS166_IN_GGA(s(T189), T190) → PLUS166_IN_GGA(T189, T190)
    The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

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

PLUS154_IN_GGA(s(T163), T164, s(X436)) → PLUS154_IN_GGA(T163, T164, X436)

The TRS R consists of the following rules:

timesc18_in_ga(T35, 0) → timesc18_out_ga(T35, 0)
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
halfc56_in_ga(T86, s(X147)) → U72_ga(T86, X147, halfc60_in_ga(T86, X147))
halfc60_in_ga(0, 0) → halfc60_out_ga(0, 0)
halfc60_in_ga(s(s(T89)), s(X156)) → U38_ga(T89, X156, halfc60_in_ga(T89, X156))
U38_ga(T89, X156, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
U72_ga(T86, X147, halfc60_out_ga(T86, X147)) → halfc56_out_ga(T86, s(X147))
timesc69_in_gga(0, T99, 0) → timesc69_out_gga(0, T99, 0)
timesc69_in_gga(s(T117), T118, 0) → U39_gga(T117, T118, evenc36_in_gg(s(T117), true))
U39_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U40_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U40_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_gga(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(0, T99, 0) → timesc69_out_ggg(0, T99, 0)
timesc69_in_ggg(s(T117), T118, 0) → U39_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U39_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U40_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U40_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_ggg(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(s(T117), T118, s(s(0))) → U42_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U42_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U43_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U43_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T117), T118, s(s(s(s(0))))) → U45_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U45_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U46_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U46_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U48_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U49_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U49_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U51_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U52_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U52_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U54_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U55_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U55_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U57_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U58_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U58_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U60_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U61_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U61_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_ggg(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_ggg(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_ggg(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_ggg(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_ggg(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T117), T118, s(s(0))) → U42_gga(T117, T118, evenc36_in_gg(s(T117), true))
U42_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U43_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U43_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_gga(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T171), T172, X455) → U67_ggg(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_ggg(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_ggg(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
timesc69_in_gga(s(T117), T118, s(s(s(s(0))))) → U45_gga(T117, T118, evenc36_in_gg(s(T117), true))
U45_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U46_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U46_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
U47_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_gga(s(T117), T118, s(s(s(s(0)))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_gga(T117, T118, evenc36_in_gg(s(T117), true))
U48_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U49_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U49_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
U50_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(0)))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_gga(T117, T118, evenc36_in_gg(s(T117), true))
U51_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U52_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U52_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
U53_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_gga(T117, T118, evenc36_in_gg(s(T117), true))
U54_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U55_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U55_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
U56_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_gga(T117, T118, evenc36_in_gg(s(T117), true))
U57_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U58_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U58_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
U59_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_gga(T117, T118, evenc36_in_gg(s(T117), true))
U60_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U61_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U61_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
U62_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_gga(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_gga(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_gga(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_gga(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_gga(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T171), T172, X455) → U67_gga(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_gga(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_gga(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
U68_gga(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_gga(T171, T172, X455, plusc166_in_gga(T172, T175, X455))
plusc166_in_gga(0, T184, T184) → plusc166_out_gga(0, T184, T184)
plusc166_in_gga(s(T189), T190, s(X482)) → U71_gga(T189, T190, X482, plusc166_in_gga(T189, T190, X482))
U71_gga(T189, T190, X482, plusc166_out_gga(T189, T190, X482)) → plusc166_out_gga(s(T189), T190, s(X482))
U69_gga(T171, T172, X455, plusc166_out_gga(T172, T175, X455)) → timesc69_out_gga(s(T171), T172, X455)
U65_gga(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_gga(T117, T118, X411, plusc154_in_gga(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_gga(0, T158, s(T158)) → plusc154_out_gga(0, T158, s(T158))
plusc154_in_gga(s(T163), T164, s(X436)) → U70_gga(T163, T164, X436, plusc154_in_gga(T163, T164, X436))
U70_gga(T163, T164, X436, plusc154_out_gga(T163, T164, X436)) → plusc154_out_gga(s(T163), T164, s(X436))
U66_gga(T117, T118, X411, plusc154_out_gga(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U68_ggg(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_ggg(T171, T172, X455, plusc166_in_ggg(T172, T175, X455))
plusc166_in_ggg(0, T184, T184) → plusc166_out_ggg(0, T184, T184)
plusc166_in_ggg(s(T189), T190, s(X482)) → U71_ggg(T189, T190, X482, plusc166_in_ggg(T189, T190, X482))
U71_ggg(T189, T190, X482, plusc166_out_ggg(T189, T190, X482)) → plusc166_out_ggg(s(T189), T190, s(X482))
U69_ggg(T171, T172, X455, plusc166_out_ggg(T172, T175, X455)) → timesc69_out_ggg(s(T171), T172, X455)
U44_gga(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_gga(s(T117), T118, s(s(0)))
U65_ggg(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_ggg(T117, T118, X411, plusc154_in_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_ggg(0, T158, s(T158)) → plusc154_out_ggg(0, T158, s(T158))
plusc154_in_ggg(s(T163), T164, s(X436)) → U70_ggg(T163, T164, X436, plusc154_in_ggg(T163, T164, X436))
U70_ggg(T163, T164, X436, plusc154_out_ggg(T163, T164, X436)) → plusc154_out_ggg(s(T163), T164, s(X436))
U66_ggg(T117, T118, X411, plusc154_out_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U62_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U59_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U56_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U53_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
U50_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(0)))))))
U47_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(0)))))
U44_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_ggg(s(T117), T118, s(s(0)))
U41_ggg(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_ggg(s(T117), T118, 0)
U41_gga(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_gga(s(T117), T118, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timesc18_in_ga(x1, x2)  =  timesc18_in_ga(x1)
timesc18_out_ga(x1, x2)  =  timesc18_out_ga(x1, x2)
evenc36_in_gg(x1, x2)  =  evenc36_in_gg(x1, x2)
true  =  true
evenc36_out_gg(x1, x2)  =  evenc36_out_gg(x1, x2)
false  =  false
U37_gg(x1, x2, x3)  =  U37_gg(x1, x2, x3)
halfc56_in_ga(x1, x2)  =  halfc56_in_ga(x1)
U72_ga(x1, x2, x3)  =  U72_ga(x1, x3)
halfc60_in_ga(x1, x2)  =  halfc60_in_ga(x1)
halfc60_out_ga(x1, x2)  =  halfc60_out_ga(x1, x2)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
halfc56_out_ga(x1, x2)  =  halfc56_out_ga(x1, x2)
timesc69_in_gga(x1, x2, x3)  =  timesc69_in_gga(x1, x2)
timesc69_out_gga(x1, x2, x3)  =  timesc69_out_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
timesc69_in_ggg(x1, x2, x3)  =  timesc69_in_ggg(x1, x2, x3)
timesc69_out_ggg(x1, x2, x3)  =  timesc69_out_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3)  =  U62_ggg(x1, x2, x3)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4, x5)  =  U65_ggg(x1, x2, x3, x5)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3)  =  U62_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4, x5)  =  U65_gga(x1, x2, x5)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
plusc166_in_gga(x1, x2, x3)  =  plusc166_in_gga(x1, x2)
plusc166_out_gga(x1, x2, x3)  =  plusc166_out_gga(x1, x2, x3)
U71_gga(x1, x2, x3, x4)  =  U71_gga(x1, x2, x4)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
plusc154_in_gga(x1, x2, x3)  =  plusc154_in_gga(x1, x2)
plusc154_out_gga(x1, x2, x3)  =  plusc154_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
plusc166_in_ggg(x1, x2, x3)  =  plusc166_in_ggg(x1, x2, x3)
plusc166_out_ggg(x1, x2, x3)  =  plusc166_out_ggg(x1, x2, x3)
U71_ggg(x1, x2, x3, x4)  =  U71_ggg(x1, x2, x3, x4)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
plusc154_in_ggg(x1, x2, x3)  =  plusc154_in_ggg(x1, x2, x3)
plusc154_out_ggg(x1, x2, x3)  =  plusc154_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
PLUS154_IN_GGA(x1, x2, x3)  =  PLUS154_IN_GGA(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

PLUS154_IN_GGA(s(T163), T164, s(X436)) → PLUS154_IN_GGA(T163, T164, X436)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

PLUS154_IN_GGA(s(T163), T164) → PLUS154_IN_GGA(T163, T164)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PLUS154_IN_GGA(s(T163), T164) → PLUS154_IN_GGA(T163, T164)
    The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

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

HALF60_IN_GA(s(s(T89)), s(X156)) → HALF60_IN_GA(T89, X156)

The TRS R consists of the following rules:

timesc18_in_ga(T35, 0) → timesc18_out_ga(T35, 0)
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
halfc56_in_ga(T86, s(X147)) → U72_ga(T86, X147, halfc60_in_ga(T86, X147))
halfc60_in_ga(0, 0) → halfc60_out_ga(0, 0)
halfc60_in_ga(s(s(T89)), s(X156)) → U38_ga(T89, X156, halfc60_in_ga(T89, X156))
U38_ga(T89, X156, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
U72_ga(T86, X147, halfc60_out_ga(T86, X147)) → halfc56_out_ga(T86, s(X147))
timesc69_in_gga(0, T99, 0) → timesc69_out_gga(0, T99, 0)
timesc69_in_gga(s(T117), T118, 0) → U39_gga(T117, T118, evenc36_in_gg(s(T117), true))
U39_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U40_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U40_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_gga(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(0, T99, 0) → timesc69_out_ggg(0, T99, 0)
timesc69_in_ggg(s(T117), T118, 0) → U39_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U39_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U40_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U40_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_ggg(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(s(T117), T118, s(s(0))) → U42_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U42_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U43_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U43_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T117), T118, s(s(s(s(0))))) → U45_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U45_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U46_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U46_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U48_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U49_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U49_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U51_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U52_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U52_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U54_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U55_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U55_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U57_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U58_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U58_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U60_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U61_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U61_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_ggg(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_ggg(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_ggg(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_ggg(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_ggg(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T117), T118, s(s(0))) → U42_gga(T117, T118, evenc36_in_gg(s(T117), true))
U42_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U43_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U43_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_gga(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T171), T172, X455) → U67_ggg(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_ggg(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_ggg(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
timesc69_in_gga(s(T117), T118, s(s(s(s(0))))) → U45_gga(T117, T118, evenc36_in_gg(s(T117), true))
U45_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U46_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U46_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
U47_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_gga(s(T117), T118, s(s(s(s(0)))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_gga(T117, T118, evenc36_in_gg(s(T117), true))
U48_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U49_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U49_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
U50_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(0)))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_gga(T117, T118, evenc36_in_gg(s(T117), true))
U51_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U52_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U52_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
U53_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_gga(T117, T118, evenc36_in_gg(s(T117), true))
U54_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U55_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U55_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
U56_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_gga(T117, T118, evenc36_in_gg(s(T117), true))
U57_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U58_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U58_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
U59_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_gga(T117, T118, evenc36_in_gg(s(T117), true))
U60_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U61_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U61_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
U62_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_gga(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_gga(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_gga(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_gga(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_gga(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T171), T172, X455) → U67_gga(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_gga(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_gga(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
U68_gga(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_gga(T171, T172, X455, plusc166_in_gga(T172, T175, X455))
plusc166_in_gga(0, T184, T184) → plusc166_out_gga(0, T184, T184)
plusc166_in_gga(s(T189), T190, s(X482)) → U71_gga(T189, T190, X482, plusc166_in_gga(T189, T190, X482))
U71_gga(T189, T190, X482, plusc166_out_gga(T189, T190, X482)) → plusc166_out_gga(s(T189), T190, s(X482))
U69_gga(T171, T172, X455, plusc166_out_gga(T172, T175, X455)) → timesc69_out_gga(s(T171), T172, X455)
U65_gga(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_gga(T117, T118, X411, plusc154_in_gga(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_gga(0, T158, s(T158)) → plusc154_out_gga(0, T158, s(T158))
plusc154_in_gga(s(T163), T164, s(X436)) → U70_gga(T163, T164, X436, plusc154_in_gga(T163, T164, X436))
U70_gga(T163, T164, X436, plusc154_out_gga(T163, T164, X436)) → plusc154_out_gga(s(T163), T164, s(X436))
U66_gga(T117, T118, X411, plusc154_out_gga(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U68_ggg(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_ggg(T171, T172, X455, plusc166_in_ggg(T172, T175, X455))
plusc166_in_ggg(0, T184, T184) → plusc166_out_ggg(0, T184, T184)
plusc166_in_ggg(s(T189), T190, s(X482)) → U71_ggg(T189, T190, X482, plusc166_in_ggg(T189, T190, X482))
U71_ggg(T189, T190, X482, plusc166_out_ggg(T189, T190, X482)) → plusc166_out_ggg(s(T189), T190, s(X482))
U69_ggg(T171, T172, X455, plusc166_out_ggg(T172, T175, X455)) → timesc69_out_ggg(s(T171), T172, X455)
U44_gga(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_gga(s(T117), T118, s(s(0)))
U65_ggg(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_ggg(T117, T118, X411, plusc154_in_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_ggg(0, T158, s(T158)) → plusc154_out_ggg(0, T158, s(T158))
plusc154_in_ggg(s(T163), T164, s(X436)) → U70_ggg(T163, T164, X436, plusc154_in_ggg(T163, T164, X436))
U70_ggg(T163, T164, X436, plusc154_out_ggg(T163, T164, X436)) → plusc154_out_ggg(s(T163), T164, s(X436))
U66_ggg(T117, T118, X411, plusc154_out_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U62_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U59_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U56_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U53_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
U50_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(0)))))))
U47_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(0)))))
U44_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_ggg(s(T117), T118, s(s(0)))
U41_ggg(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_ggg(s(T117), T118, 0)
U41_gga(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_gga(s(T117), T118, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timesc18_in_ga(x1, x2)  =  timesc18_in_ga(x1)
timesc18_out_ga(x1, x2)  =  timesc18_out_ga(x1, x2)
evenc36_in_gg(x1, x2)  =  evenc36_in_gg(x1, x2)
true  =  true
evenc36_out_gg(x1, x2)  =  evenc36_out_gg(x1, x2)
false  =  false
U37_gg(x1, x2, x3)  =  U37_gg(x1, x2, x3)
halfc56_in_ga(x1, x2)  =  halfc56_in_ga(x1)
U72_ga(x1, x2, x3)  =  U72_ga(x1, x3)
halfc60_in_ga(x1, x2)  =  halfc60_in_ga(x1)
halfc60_out_ga(x1, x2)  =  halfc60_out_ga(x1, x2)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
halfc56_out_ga(x1, x2)  =  halfc56_out_ga(x1, x2)
timesc69_in_gga(x1, x2, x3)  =  timesc69_in_gga(x1, x2)
timesc69_out_gga(x1, x2, x3)  =  timesc69_out_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
timesc69_in_ggg(x1, x2, x3)  =  timesc69_in_ggg(x1, x2, x3)
timesc69_out_ggg(x1, x2, x3)  =  timesc69_out_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3)  =  U62_ggg(x1, x2, x3)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4, x5)  =  U65_ggg(x1, x2, x3, x5)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3)  =  U62_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4, x5)  =  U65_gga(x1, x2, x5)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
plusc166_in_gga(x1, x2, x3)  =  plusc166_in_gga(x1, x2)
plusc166_out_gga(x1, x2, x3)  =  plusc166_out_gga(x1, x2, x3)
U71_gga(x1, x2, x3, x4)  =  U71_gga(x1, x2, x4)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
plusc154_in_gga(x1, x2, x3)  =  plusc154_in_gga(x1, x2)
plusc154_out_gga(x1, x2, x3)  =  plusc154_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
plusc166_in_ggg(x1, x2, x3)  =  plusc166_in_ggg(x1, x2, x3)
plusc166_out_ggg(x1, x2, x3)  =  plusc166_out_ggg(x1, x2, x3)
U71_ggg(x1, x2, x3, x4)  =  U71_ggg(x1, x2, x3, x4)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
plusc154_in_ggg(x1, x2, x3)  =  plusc154_in_ggg(x1, x2, x3)
plusc154_out_ggg(x1, x2, x3)  =  plusc154_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
HALF60_IN_GA(x1, x2)  =  HALF60_IN_GA(x1)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

HALF60_IN_GA(s(s(T89)), s(X156)) → HALF60_IN_GA(T89, X156)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

HALF60_IN_GA(s(s(T89))) → HALF60_IN_GA(T89)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • HALF60_IN_GA(s(s(T89))) → HALF60_IN_GA(T89)
    The graph contains the following edges 1 > 1

(27) YES

(28) Obligation:

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

EVEN36_IN_GA(s(s(T61)), X101) → EVEN36_IN_GA(T61, X101)

The TRS R consists of the following rules:

timesc18_in_ga(T35, 0) → timesc18_out_ga(T35, 0)
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
halfc56_in_ga(T86, s(X147)) → U72_ga(T86, X147, halfc60_in_ga(T86, X147))
halfc60_in_ga(0, 0) → halfc60_out_ga(0, 0)
halfc60_in_ga(s(s(T89)), s(X156)) → U38_ga(T89, X156, halfc60_in_ga(T89, X156))
U38_ga(T89, X156, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
U72_ga(T86, X147, halfc60_out_ga(T86, X147)) → halfc56_out_ga(T86, s(X147))
timesc69_in_gga(0, T99, 0) → timesc69_out_gga(0, T99, 0)
timesc69_in_gga(s(T117), T118, 0) → U39_gga(T117, T118, evenc36_in_gg(s(T117), true))
U39_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U40_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U40_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_gga(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(0, T99, 0) → timesc69_out_ggg(0, T99, 0)
timesc69_in_ggg(s(T117), T118, 0) → U39_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U39_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U40_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U40_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_ggg(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(s(T117), T118, s(s(0))) → U42_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U42_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U43_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U43_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T117), T118, s(s(s(s(0))))) → U45_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U45_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U46_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U46_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U48_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U49_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U49_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U51_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U52_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U52_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U54_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U55_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U55_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U57_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U58_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U58_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U60_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U61_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U61_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_ggg(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_ggg(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_ggg(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_ggg(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_ggg(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T117), T118, s(s(0))) → U42_gga(T117, T118, evenc36_in_gg(s(T117), true))
U42_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U43_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U43_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_gga(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T171), T172, X455) → U67_ggg(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_ggg(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_ggg(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
timesc69_in_gga(s(T117), T118, s(s(s(s(0))))) → U45_gga(T117, T118, evenc36_in_gg(s(T117), true))
U45_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U46_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U46_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
U47_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_gga(s(T117), T118, s(s(s(s(0)))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_gga(T117, T118, evenc36_in_gg(s(T117), true))
U48_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U49_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U49_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
U50_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(0)))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_gga(T117, T118, evenc36_in_gg(s(T117), true))
U51_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U52_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U52_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
U53_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_gga(T117, T118, evenc36_in_gg(s(T117), true))
U54_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U55_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U55_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
U56_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_gga(T117, T118, evenc36_in_gg(s(T117), true))
U57_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U58_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U58_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
U59_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_gga(T117, T118, evenc36_in_gg(s(T117), true))
U60_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U61_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U61_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
U62_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_gga(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_gga(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_gga(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_gga(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_gga(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T171), T172, X455) → U67_gga(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_gga(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_gga(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
U68_gga(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_gga(T171, T172, X455, plusc166_in_gga(T172, T175, X455))
plusc166_in_gga(0, T184, T184) → plusc166_out_gga(0, T184, T184)
plusc166_in_gga(s(T189), T190, s(X482)) → U71_gga(T189, T190, X482, plusc166_in_gga(T189, T190, X482))
U71_gga(T189, T190, X482, plusc166_out_gga(T189, T190, X482)) → plusc166_out_gga(s(T189), T190, s(X482))
U69_gga(T171, T172, X455, plusc166_out_gga(T172, T175, X455)) → timesc69_out_gga(s(T171), T172, X455)
U65_gga(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_gga(T117, T118, X411, plusc154_in_gga(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_gga(0, T158, s(T158)) → plusc154_out_gga(0, T158, s(T158))
plusc154_in_gga(s(T163), T164, s(X436)) → U70_gga(T163, T164, X436, plusc154_in_gga(T163, T164, X436))
U70_gga(T163, T164, X436, plusc154_out_gga(T163, T164, X436)) → plusc154_out_gga(s(T163), T164, s(X436))
U66_gga(T117, T118, X411, plusc154_out_gga(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U68_ggg(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_ggg(T171, T172, X455, plusc166_in_ggg(T172, T175, X455))
plusc166_in_ggg(0, T184, T184) → plusc166_out_ggg(0, T184, T184)
plusc166_in_ggg(s(T189), T190, s(X482)) → U71_ggg(T189, T190, X482, plusc166_in_ggg(T189, T190, X482))
U71_ggg(T189, T190, X482, plusc166_out_ggg(T189, T190, X482)) → plusc166_out_ggg(s(T189), T190, s(X482))
U69_ggg(T171, T172, X455, plusc166_out_ggg(T172, T175, X455)) → timesc69_out_ggg(s(T171), T172, X455)
U44_gga(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_gga(s(T117), T118, s(s(0)))
U65_ggg(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_ggg(T117, T118, X411, plusc154_in_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_ggg(0, T158, s(T158)) → plusc154_out_ggg(0, T158, s(T158))
plusc154_in_ggg(s(T163), T164, s(X436)) → U70_ggg(T163, T164, X436, plusc154_in_ggg(T163, T164, X436))
U70_ggg(T163, T164, X436, plusc154_out_ggg(T163, T164, X436)) → plusc154_out_ggg(s(T163), T164, s(X436))
U66_ggg(T117, T118, X411, plusc154_out_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U62_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U59_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U56_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U53_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
U50_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(0)))))))
U47_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(0)))))
U44_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_ggg(s(T117), T118, s(s(0)))
U41_ggg(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_ggg(s(T117), T118, 0)
U41_gga(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_gga(s(T117), T118, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timesc18_in_ga(x1, x2)  =  timesc18_in_ga(x1)
timesc18_out_ga(x1, x2)  =  timesc18_out_ga(x1, x2)
evenc36_in_gg(x1, x2)  =  evenc36_in_gg(x1, x2)
true  =  true
evenc36_out_gg(x1, x2)  =  evenc36_out_gg(x1, x2)
false  =  false
U37_gg(x1, x2, x3)  =  U37_gg(x1, x2, x3)
halfc56_in_ga(x1, x2)  =  halfc56_in_ga(x1)
U72_ga(x1, x2, x3)  =  U72_ga(x1, x3)
halfc60_in_ga(x1, x2)  =  halfc60_in_ga(x1)
halfc60_out_ga(x1, x2)  =  halfc60_out_ga(x1, x2)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
halfc56_out_ga(x1, x2)  =  halfc56_out_ga(x1, x2)
timesc69_in_gga(x1, x2, x3)  =  timesc69_in_gga(x1, x2)
timesc69_out_gga(x1, x2, x3)  =  timesc69_out_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
timesc69_in_ggg(x1, x2, x3)  =  timesc69_in_ggg(x1, x2, x3)
timesc69_out_ggg(x1, x2, x3)  =  timesc69_out_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3)  =  U62_ggg(x1, x2, x3)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4, x5)  =  U65_ggg(x1, x2, x3, x5)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3)  =  U62_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4, x5)  =  U65_gga(x1, x2, x5)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
plusc166_in_gga(x1, x2, x3)  =  plusc166_in_gga(x1, x2)
plusc166_out_gga(x1, x2, x3)  =  plusc166_out_gga(x1, x2, x3)
U71_gga(x1, x2, x3, x4)  =  U71_gga(x1, x2, x4)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
plusc154_in_gga(x1, x2, x3)  =  plusc154_in_gga(x1, x2)
plusc154_out_gga(x1, x2, x3)  =  plusc154_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
plusc166_in_ggg(x1, x2, x3)  =  plusc166_in_ggg(x1, x2, x3)
plusc166_out_ggg(x1, x2, x3)  =  plusc166_out_ggg(x1, x2, x3)
U71_ggg(x1, x2, x3, x4)  =  U71_ggg(x1, x2, x3, x4)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
plusc154_in_ggg(x1, x2, x3)  =  plusc154_in_ggg(x1, x2, x3)
plusc154_out_ggg(x1, x2, x3)  =  plusc154_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
EVEN36_IN_GA(x1, x2)  =  EVEN36_IN_GA(x1)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

EVEN36_IN_GA(s(s(T61)), X101) → EVEN36_IN_GA(T61, X101)

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

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

EVEN36_IN_GA(s(s(T61))) → EVEN36_IN_GA(T61)

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

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • EVEN36_IN_GA(s(s(T61))) → EVEN36_IN_GA(T61)
    The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

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

TIMES69_IN_GGA(s(T117), T118, X217) → U5_GGA(T117, T118, X217, evenc36_in_gg(s(T117), true))
U5_GGA(T117, T118, X217, evenc36_out_gg(s(T117), true)) → U7_GGA(T117, T118, X217, halfc60_in_ga(s(T117), T120))
U7_GGA(T117, T118, X217, halfc60_out_ga(s(T117), T120)) → TIMES69_IN_GGA(T120, T118, X216)
TIMES69_IN_GGA(s(T171), T172, X455) → U13_GGA(T171, T172, X455, evenc36_in_gg(s(T171), false))
U13_GGA(T171, T172, X455, evenc36_out_gg(s(T171), false)) → TIMES69_IN_GGA(T171, T172, X454)

The TRS R consists of the following rules:

timesc18_in_ga(T35, 0) → timesc18_out_ga(T35, 0)
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
halfc56_in_ga(T86, s(X147)) → U72_ga(T86, X147, halfc60_in_ga(T86, X147))
halfc60_in_ga(0, 0) → halfc60_out_ga(0, 0)
halfc60_in_ga(s(s(T89)), s(X156)) → U38_ga(T89, X156, halfc60_in_ga(T89, X156))
U38_ga(T89, X156, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
U72_ga(T86, X147, halfc60_out_ga(T86, X147)) → halfc56_out_ga(T86, s(X147))
timesc69_in_gga(0, T99, 0) → timesc69_out_gga(0, T99, 0)
timesc69_in_gga(s(T117), T118, 0) → U39_gga(T117, T118, evenc36_in_gg(s(T117), true))
U39_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U40_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U40_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_gga(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(0, T99, 0) → timesc69_out_ggg(0, T99, 0)
timesc69_in_ggg(s(T117), T118, 0) → U39_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U39_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U40_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U40_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_ggg(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(s(T117), T118, s(s(0))) → U42_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U42_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U43_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U43_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T117), T118, s(s(s(s(0))))) → U45_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U45_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U46_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U46_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U48_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U49_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U49_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U51_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U52_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U52_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U54_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U55_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U55_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U57_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U58_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U58_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U60_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U61_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U61_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_ggg(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_ggg(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_ggg(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_ggg(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_ggg(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T117), T118, s(s(0))) → U42_gga(T117, T118, evenc36_in_gg(s(T117), true))
U42_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U43_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U43_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_gga(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T171), T172, X455) → U67_ggg(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_ggg(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_ggg(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
timesc69_in_gga(s(T117), T118, s(s(s(s(0))))) → U45_gga(T117, T118, evenc36_in_gg(s(T117), true))
U45_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U46_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U46_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
U47_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_gga(s(T117), T118, s(s(s(s(0)))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_gga(T117, T118, evenc36_in_gg(s(T117), true))
U48_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U49_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U49_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
U50_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(0)))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_gga(T117, T118, evenc36_in_gg(s(T117), true))
U51_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U52_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U52_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
U53_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_gga(T117, T118, evenc36_in_gg(s(T117), true))
U54_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U55_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U55_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
U56_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_gga(T117, T118, evenc36_in_gg(s(T117), true))
U57_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U58_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U58_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
U59_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_gga(T117, T118, evenc36_in_gg(s(T117), true))
U60_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U61_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U61_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
U62_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_gga(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_gga(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_gga(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_gga(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_gga(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T171), T172, X455) → U67_gga(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_gga(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_gga(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
U68_gga(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_gga(T171, T172, X455, plusc166_in_gga(T172, T175, X455))
plusc166_in_gga(0, T184, T184) → plusc166_out_gga(0, T184, T184)
plusc166_in_gga(s(T189), T190, s(X482)) → U71_gga(T189, T190, X482, plusc166_in_gga(T189, T190, X482))
U71_gga(T189, T190, X482, plusc166_out_gga(T189, T190, X482)) → plusc166_out_gga(s(T189), T190, s(X482))
U69_gga(T171, T172, X455, plusc166_out_gga(T172, T175, X455)) → timesc69_out_gga(s(T171), T172, X455)
U65_gga(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_gga(T117, T118, X411, plusc154_in_gga(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_gga(0, T158, s(T158)) → plusc154_out_gga(0, T158, s(T158))
plusc154_in_gga(s(T163), T164, s(X436)) → U70_gga(T163, T164, X436, plusc154_in_gga(T163, T164, X436))
U70_gga(T163, T164, X436, plusc154_out_gga(T163, T164, X436)) → plusc154_out_gga(s(T163), T164, s(X436))
U66_gga(T117, T118, X411, plusc154_out_gga(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U68_ggg(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_ggg(T171, T172, X455, plusc166_in_ggg(T172, T175, X455))
plusc166_in_ggg(0, T184, T184) → plusc166_out_ggg(0, T184, T184)
plusc166_in_ggg(s(T189), T190, s(X482)) → U71_ggg(T189, T190, X482, plusc166_in_ggg(T189, T190, X482))
U71_ggg(T189, T190, X482, plusc166_out_ggg(T189, T190, X482)) → plusc166_out_ggg(s(T189), T190, s(X482))
U69_ggg(T171, T172, X455, plusc166_out_ggg(T172, T175, X455)) → timesc69_out_ggg(s(T171), T172, X455)
U44_gga(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_gga(s(T117), T118, s(s(0)))
U65_ggg(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_ggg(T117, T118, X411, plusc154_in_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_ggg(0, T158, s(T158)) → plusc154_out_ggg(0, T158, s(T158))
plusc154_in_ggg(s(T163), T164, s(X436)) → U70_ggg(T163, T164, X436, plusc154_in_ggg(T163, T164, X436))
U70_ggg(T163, T164, X436, plusc154_out_ggg(T163, T164, X436)) → plusc154_out_ggg(s(T163), T164, s(X436))
U66_ggg(T117, T118, X411, plusc154_out_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U62_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U59_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U56_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U53_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
U50_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(0)))))))
U47_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(0)))))
U44_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_ggg(s(T117), T118, s(s(0)))
U41_ggg(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_ggg(s(T117), T118, 0)
U41_gga(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_gga(s(T117), T118, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timesc18_in_ga(x1, x2)  =  timesc18_in_ga(x1)
timesc18_out_ga(x1, x2)  =  timesc18_out_ga(x1, x2)
evenc36_in_gg(x1, x2)  =  evenc36_in_gg(x1, x2)
true  =  true
evenc36_out_gg(x1, x2)  =  evenc36_out_gg(x1, x2)
false  =  false
U37_gg(x1, x2, x3)  =  U37_gg(x1, x2, x3)
halfc56_in_ga(x1, x2)  =  halfc56_in_ga(x1)
U72_ga(x1, x2, x3)  =  U72_ga(x1, x3)
halfc60_in_ga(x1, x2)  =  halfc60_in_ga(x1)
halfc60_out_ga(x1, x2)  =  halfc60_out_ga(x1, x2)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
halfc56_out_ga(x1, x2)  =  halfc56_out_ga(x1, x2)
timesc69_in_gga(x1, x2, x3)  =  timesc69_in_gga(x1, x2)
timesc69_out_gga(x1, x2, x3)  =  timesc69_out_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
timesc69_in_ggg(x1, x2, x3)  =  timesc69_in_ggg(x1, x2, x3)
timesc69_out_ggg(x1, x2, x3)  =  timesc69_out_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3)  =  U62_ggg(x1, x2, x3)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4, x5)  =  U65_ggg(x1, x2, x3, x5)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3)  =  U62_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4, x5)  =  U65_gga(x1, x2, x5)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
plusc166_in_gga(x1, x2, x3)  =  plusc166_in_gga(x1, x2)
plusc166_out_gga(x1, x2, x3)  =  plusc166_out_gga(x1, x2, x3)
U71_gga(x1, x2, x3, x4)  =  U71_gga(x1, x2, x4)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
plusc154_in_gga(x1, x2, x3)  =  plusc154_in_gga(x1, x2)
plusc154_out_gga(x1, x2, x3)  =  plusc154_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
plusc166_in_ggg(x1, x2, x3)  =  plusc166_in_ggg(x1, x2, x3)
plusc166_out_ggg(x1, x2, x3)  =  plusc166_out_ggg(x1, x2, x3)
U71_ggg(x1, x2, x3, x4)  =  U71_ggg(x1, x2, x3, x4)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
plusc154_in_ggg(x1, x2, x3)  =  plusc154_in_ggg(x1, x2, x3)
plusc154_out_ggg(x1, x2, x3)  =  plusc154_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
TIMES69_IN_GGA(x1, x2, x3)  =  TIMES69_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

TIMES69_IN_GGA(s(T117), T118, X217) → U5_GGA(T117, T118, X217, evenc36_in_gg(s(T117), true))
U5_GGA(T117, T118, X217, evenc36_out_gg(s(T117), true)) → U7_GGA(T117, T118, X217, halfc60_in_ga(s(T117), T120))
U7_GGA(T117, T118, X217, halfc60_out_ga(s(T117), T120)) → TIMES69_IN_GGA(T120, T118, X216)
TIMES69_IN_GGA(s(T171), T172, X455) → U13_GGA(T171, T172, X455, evenc36_in_gg(s(T171), false))
U13_GGA(T171, T172, X455, evenc36_out_gg(s(T171), false)) → TIMES69_IN_GGA(T171, T172, X454)

The TRS R consists of the following rules:

evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
halfc60_in_ga(s(s(T89)), s(X156)) → U38_ga(T89, X156, halfc60_in_ga(T89, X156))
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
U38_ga(T89, X156, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
halfc60_in_ga(0, 0) → halfc60_out_ga(0, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
evenc36_in_gg(x1, x2)  =  evenc36_in_gg(x1, x2)
true  =  true
evenc36_out_gg(x1, x2)  =  evenc36_out_gg(x1, x2)
false  =  false
U37_gg(x1, x2, x3)  =  U37_gg(x1, x2, x3)
halfc60_in_ga(x1, x2)  =  halfc60_in_ga(x1)
halfc60_out_ga(x1, x2)  =  halfc60_out_ga(x1, x2)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
TIMES69_IN_GGA(x1, x2, x3)  =  TIMES69_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

TIMES69_IN_GGA(s(T117), T118) → U5_GGA(T117, T118, evenc36_in_gg(s(T117), true))
U5_GGA(T117, T118, evenc36_out_gg(s(T117), true)) → U7_GGA(T117, T118, halfc60_in_ga(s(T117)))
U7_GGA(T117, T118, halfc60_out_ga(s(T117), T120)) → TIMES69_IN_GGA(T120, T118)
TIMES69_IN_GGA(s(T171), T172) → U13_GGA(T171, T172, evenc36_in_gg(s(T171), false))
U13_GGA(T171, T172, evenc36_out_gg(s(T171), false)) → TIMES69_IN_GGA(T171, T172)

The TRS R consists of the following rules:

evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
halfc60_in_ga(s(s(T89))) → U38_ga(T89, halfc60_in_ga(T89))
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
U38_ga(T89, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
halfc60_in_ga(0) → halfc60_out_ga(0, 0)

The set Q consists of the following terms:

evenc36_in_gg(x0, x1)
halfc60_in_ga(x0)
U37_gg(x0, x1, x2)
U38_ga(x0, x1)

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

(40) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


TIMES69_IN_GGA(s(T171), T172) → U13_GGA(T171, T172, evenc36_in_gg(s(T171), false))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(TIMES69_IN_GGA(x1, x2)) = x1   
POL(U13_GGA(x1, x2, x3)) = x1   
POL(U37_gg(x1, x2, x3)) = 0   
POL(U38_ga(x1, x2)) = 1 + x2   
POL(U5_GGA(x1, x2, x3)) = 1 + x1   
POL(U7_GGA(x1, x2, x3)) = x3   
POL(evenc36_in_gg(x1, x2)) = 0   
POL(evenc36_out_gg(x1, x2)) = 0   
POL(false) = 0   
POL(halfc60_in_ga(x1)) = x1   
POL(halfc60_out_ga(x1, x2)) = x2   
POL(s(x1)) = 1 + x1   
POL(true) = 0   

The following usable rules [FROCOS05] were oriented:

halfc60_in_ga(s(s(T89))) → U38_ga(T89, halfc60_in_ga(T89))
halfc60_in_ga(0) → halfc60_out_ga(0, 0)
U38_ga(T89, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))

(41) Obligation:

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

TIMES69_IN_GGA(s(T117), T118) → U5_GGA(T117, T118, evenc36_in_gg(s(T117), true))
U5_GGA(T117, T118, evenc36_out_gg(s(T117), true)) → U7_GGA(T117, T118, halfc60_in_ga(s(T117)))
U7_GGA(T117, T118, halfc60_out_ga(s(T117), T120)) → TIMES69_IN_GGA(T120, T118)
U13_GGA(T171, T172, evenc36_out_gg(s(T171), false)) → TIMES69_IN_GGA(T171, T172)

The TRS R consists of the following rules:

evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
halfc60_in_ga(s(s(T89))) → U38_ga(T89, halfc60_in_ga(T89))
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
U38_ga(T89, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
halfc60_in_ga(0) → halfc60_out_ga(0, 0)

The set Q consists of the following terms:

evenc36_in_gg(x0, x1)
halfc60_in_ga(x0)
U37_gg(x0, x1, x2)
U38_ga(x0, x1)

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

(42) DependencyGraphProof (EQUIVALENT transformation)

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

(43) Obligation:

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

U5_GGA(T117, T118, evenc36_out_gg(s(T117), true)) → U7_GGA(T117, T118, halfc60_in_ga(s(T117)))
U7_GGA(T117, T118, halfc60_out_ga(s(T117), T120)) → TIMES69_IN_GGA(T120, T118)
TIMES69_IN_GGA(s(T117), T118) → U5_GGA(T117, T118, evenc36_in_gg(s(T117), true))

The TRS R consists of the following rules:

evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
halfc60_in_ga(s(s(T89))) → U38_ga(T89, halfc60_in_ga(T89))
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
U38_ga(T89, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
halfc60_in_ga(0) → halfc60_out_ga(0, 0)

The set Q consists of the following terms:

evenc36_in_gg(x0, x1)
halfc60_in_ga(x0)
U37_gg(x0, x1, x2)
U38_ga(x0, x1)

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

(44) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


TIMES69_IN_GGA(s(T117), T118) → U5_GGA(T117, T118, evenc36_in_gg(s(T117), true))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U5_GGA(x1, x2, x3)) = 0 +
[0,1]
·x1 +
[0,0]
·x2 +
[0,0]
·x3

POL(evenc36_out_gg(x1, x2)) =
/0\
\1/
+
/10\
\11/
·x1 +
/00\
\11/
·x2

POL(s(x1)) =
/0\
\1/
+
/01\
\01/
·x1

POL(true) =
/1\
\1/

POL(U7_GGA(x1, x2, x3)) = 0 +
[0,0]
·x1 +
[0,0]
·x2 +
[0,1]
·x3

POL(halfc60_in_ga(x1)) =
/0\
\0/
+
/01\
\10/
·x1

POL(halfc60_out_ga(x1, x2)) =
/0\
\0/
+
/00\
\00/
·x1 +
/01\
\01/
·x2

POL(TIMES69_IN_GGA(x1, x2)) = 0 +
[0,1]
·x1 +
[0,0]
·x2

POL(evenc36_in_gg(x1, x2)) =
/0\
\0/
+
/00\
\00/
·x1 +
/11\
\00/
·x2

POL(U38_ga(x1, x2)) =
/1\
\1/
+
/00\
\00/
·x1 +
/10\
\10/
·x2

POL(U37_gg(x1, x2, x3)) =
/0\
\1/
+
/10\
\11/
·x1 +
/11\
\00/
·x2 +
/10\
\10/
·x3

POL(0) =
/0\
\0/

POL(false) =
/0\
\0/

The following usable rules [FROCOS05] were oriented:

halfc60_in_ga(s(s(T89))) → U38_ga(T89, halfc60_in_ga(T89))
halfc60_in_ga(0) → halfc60_out_ga(0, 0)
U38_ga(T89, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))

(45) Obligation:

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

U5_GGA(T117, T118, evenc36_out_gg(s(T117), true)) → U7_GGA(T117, T118, halfc60_in_ga(s(T117)))
U7_GGA(T117, T118, halfc60_out_ga(s(T117), T120)) → TIMES69_IN_GGA(T120, T118)

The TRS R consists of the following rules:

evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
halfc60_in_ga(s(s(T89))) → U38_ga(T89, halfc60_in_ga(T89))
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
U38_ga(T89, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
halfc60_in_ga(0) → halfc60_out_ga(0, 0)

The set Q consists of the following terms:

evenc36_in_gg(x0, x1)
halfc60_in_ga(x0)
U37_gg(x0, x1, x2)
U38_ga(x0, x1)

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

(46) DependencyGraphProof (EQUIVALENT transformation)

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

(47) TRUE

(48) Obligation:

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

PLUS19_IN_GGA(s(T49), T50, s(T52)) → PLUS19_IN_GGA(T49, T50, T52)

The TRS R consists of the following rules:

timesc18_in_ga(T35, 0) → timesc18_out_ga(T35, 0)
evenc36_in_gg(0, true) → evenc36_out_gg(0, true)
evenc36_in_gg(s(0), false) → evenc36_out_gg(s(0), false)
evenc36_in_gg(s(s(T61)), X101) → U37_gg(T61, X101, evenc36_in_gg(T61, X101))
U37_gg(T61, X101, evenc36_out_gg(T61, X101)) → evenc36_out_gg(s(s(T61)), X101)
halfc56_in_ga(T86, s(X147)) → U72_ga(T86, X147, halfc60_in_ga(T86, X147))
halfc60_in_ga(0, 0) → halfc60_out_ga(0, 0)
halfc60_in_ga(s(s(T89)), s(X156)) → U38_ga(T89, X156, halfc60_in_ga(T89, X156))
U38_ga(T89, X156, halfc60_out_ga(T89, X156)) → halfc60_out_ga(s(s(T89)), s(X156))
U72_ga(T86, X147, halfc60_out_ga(T86, X147)) → halfc56_out_ga(T86, s(X147))
timesc69_in_gga(0, T99, 0) → timesc69_out_gga(0, T99, 0)
timesc69_in_gga(s(T117), T118, 0) → U39_gga(T117, T118, evenc36_in_gg(s(T117), true))
U39_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U40_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U40_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_gga(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(0, T99, 0) → timesc69_out_ggg(0, T99, 0)
timesc69_in_ggg(s(T117), T118, 0) → U39_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U39_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U40_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U40_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U41_ggg(T117, T118, timesc69_in_ggg(T120, T118, 0))
timesc69_in_ggg(s(T117), T118, s(s(0))) → U42_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U42_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U43_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U43_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T117), T118, s(s(s(s(0))))) → U45_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U45_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U46_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U46_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U48_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U49_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U49_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U51_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U52_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U52_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U54_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U55_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U55_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U57_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U58_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U58_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_ggg(T117, T118, evenc36_in_gg(s(T117), true))
U60_ggg(T117, T118, evenc36_out_gg(s(T117), true)) → U61_ggg(T117, T118, halfc60_in_ga(s(T117), T120))
U61_ggg(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_ggg(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
timesc69_in_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_ggg(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_ggg(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_ggg(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_ggg(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_ggg(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T117), T118, s(s(0))) → U42_gga(T117, T118, evenc36_in_gg(s(T117), true))
U42_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U43_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U43_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U44_gga(T117, T118, timesc69_in_ggg(T120, T118, s(0)))
timesc69_in_ggg(s(T171), T172, X455) → U67_ggg(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_ggg(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_ggg(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
timesc69_in_gga(s(T117), T118, s(s(s(s(0))))) → U45_gga(T117, T118, evenc36_in_gg(s(T117), true))
U45_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U46_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U46_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U47_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(0))))
U47_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_gga(s(T117), T118, s(s(s(s(0)))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(0))))))) → U48_gga(T117, T118, evenc36_in_gg(s(T117), true))
U48_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U49_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U49_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U50_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(0)))))
U50_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(0)))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(0))))))))) → U51_gga(T117, T118, evenc36_in_gg(s(T117), true))
U51_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U52_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U52_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U53_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(0))))))
U53_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0))))))))))) → U54_gga(T117, T118, evenc36_in_gg(s(T117), true))
U54_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U55_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U55_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U56_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(0)))))))
U56_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → U57_gga(T117, T118, evenc36_in_gg(s(T117), true))
U57_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U58_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U58_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U59_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(0))))))))
U59_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → U60_gga(T117, T118, evenc36_in_gg(s(T117), true))
U60_gga(T117, T118, evenc36_out_gg(s(T117), true)) → U61_gga(T117, T118, halfc60_in_ga(s(T117), T120))
U61_gga(T117, T118, halfc60_out_ga(s(T117), T120)) → U62_gga(T117, T118, timesc69_in_ggg(T120, T118, s(s(s(s(s(s(s(0)))))))))
U62_gga(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
timesc69_in_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411))))))))) → U63_gga(T117, T118, X411, evenc36_in_gg(s(T117), true))
U63_gga(T117, T118, X411, evenc36_out_gg(s(T117), true)) → U64_gga(T117, T118, X411, halfc60_in_ga(s(T117), T120))
U64_gga(T117, T118, X411, halfc60_out_ga(s(T117), T120)) → U65_gga(T117, T118, X411, T120, timesc69_in_gga(T120, T118, s(s(s(s(s(s(s(s(T150))))))))))
timesc69_in_gga(s(T171), T172, X455) → U67_gga(T171, T172, X455, evenc36_in_gg(s(T171), false))
U67_gga(T171, T172, X455, evenc36_out_gg(s(T171), false)) → U68_gga(T171, T172, X455, timesc69_in_gga(T171, T172, T175))
U68_gga(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_gga(T171, T172, X455, plusc166_in_gga(T172, T175, X455))
plusc166_in_gga(0, T184, T184) → plusc166_out_gga(0, T184, T184)
plusc166_in_gga(s(T189), T190, s(X482)) → U71_gga(T189, T190, X482, plusc166_in_gga(T189, T190, X482))
U71_gga(T189, T190, X482, plusc166_out_gga(T189, T190, X482)) → plusc166_out_gga(s(T189), T190, s(X482))
U69_gga(T171, T172, X455, plusc166_out_gga(T172, T175, X455)) → timesc69_out_gga(s(T171), T172, X455)
U65_gga(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_gga(T117, T118, X411, plusc154_in_gga(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_gga(0, T158, s(T158)) → plusc154_out_gga(0, T158, s(T158))
plusc154_in_gga(s(T163), T164, s(X436)) → U70_gga(T163, T164, X436, plusc154_in_gga(T163, T164, X436))
U70_gga(T163, T164, X436, plusc154_out_gga(T163, T164, X436)) → plusc154_out_gga(s(T163), T164, s(X436))
U66_gga(T117, T118, X411, plusc154_out_gga(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_gga(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U68_ggg(T171, T172, X455, timesc69_out_gga(T171, T172, T175)) → U69_ggg(T171, T172, X455, plusc166_in_ggg(T172, T175, X455))
plusc166_in_ggg(0, T184, T184) → plusc166_out_ggg(0, T184, T184)
plusc166_in_ggg(s(T189), T190, s(X482)) → U71_ggg(T189, T190, X482, plusc166_in_ggg(T189, T190, X482))
U71_ggg(T189, T190, X482, plusc166_out_ggg(T189, T190, X482)) → plusc166_out_ggg(s(T189), T190, s(X482))
U69_ggg(T171, T172, X455, plusc166_out_ggg(T172, T175, X455)) → timesc69_out_ggg(s(T171), T172, X455)
U44_gga(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_gga(s(T117), T118, s(s(0)))
U65_ggg(T117, T118, X411, T120, timesc69_out_gga(T120, T118, s(s(s(s(s(s(s(s(T150)))))))))) → U66_ggg(T117, T118, X411, plusc154_in_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411))
plusc154_in_ggg(0, T158, s(T158)) → plusc154_out_ggg(0, T158, s(T158))
plusc154_in_ggg(s(T163), T164, s(X436)) → U70_ggg(T163, T164, X436, plusc154_in_ggg(T163, T164, X436))
U70_ggg(T163, T164, X436, plusc154_out_ggg(T163, T164, X436)) → plusc154_out_ggg(s(T163), T164, s(X436))
U66_ggg(T117, T118, X411, plusc154_out_ggg(T150, s(s(s(s(s(s(s(T150))))))), X411)) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(X411)))))))))
U62_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(s(0))))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
U59_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(s(0)))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
U56_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(s(0))))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(s(s(0)))))))))))
U53_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(s(0)))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(s(s(0)))))))))
U50_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(s(0))))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(s(s(0)))))))
U47_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(s(0)))) → timesc69_out_ggg(s(T117), T118, s(s(s(s(0)))))
U44_ggg(T117, T118, timesc69_out_ggg(T120, T118, s(0))) → timesc69_out_ggg(s(T117), T118, s(s(0)))
U41_ggg(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_ggg(s(T117), T118, 0)
U41_gga(T117, T118, timesc69_out_ggg(T120, T118, 0)) → timesc69_out_gga(s(T117), T118, 0)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
timesc18_in_ga(x1, x2)  =  timesc18_in_ga(x1)
timesc18_out_ga(x1, x2)  =  timesc18_out_ga(x1, x2)
evenc36_in_gg(x1, x2)  =  evenc36_in_gg(x1, x2)
true  =  true
evenc36_out_gg(x1, x2)  =  evenc36_out_gg(x1, x2)
false  =  false
U37_gg(x1, x2, x3)  =  U37_gg(x1, x2, x3)
halfc56_in_ga(x1, x2)  =  halfc56_in_ga(x1)
U72_ga(x1, x2, x3)  =  U72_ga(x1, x3)
halfc60_in_ga(x1, x2)  =  halfc60_in_ga(x1)
halfc60_out_ga(x1, x2)  =  halfc60_out_ga(x1, x2)
U38_ga(x1, x2, x3)  =  U38_ga(x1, x3)
halfc56_out_ga(x1, x2)  =  halfc56_out_ga(x1, x2)
timesc69_in_gga(x1, x2, x3)  =  timesc69_in_gga(x1, x2)
timesc69_out_gga(x1, x2, x3)  =  timesc69_out_gga(x1, x2, x3)
U39_gga(x1, x2, x3)  =  U39_gga(x1, x2, x3)
U40_gga(x1, x2, x3)  =  U40_gga(x1, x2, x3)
U41_gga(x1, x2, x3)  =  U41_gga(x1, x2, x3)
timesc69_in_ggg(x1, x2, x3)  =  timesc69_in_ggg(x1, x2, x3)
timesc69_out_ggg(x1, x2, x3)  =  timesc69_out_ggg(x1, x2, x3)
U39_ggg(x1, x2, x3)  =  U39_ggg(x1, x2, x3)
U40_ggg(x1, x2, x3)  =  U40_ggg(x1, x2, x3)
U41_ggg(x1, x2, x3)  =  U41_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3)  =  U42_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3)  =  U43_ggg(x1, x2, x3)
U44_ggg(x1, x2, x3)  =  U44_ggg(x1, x2, x3)
U45_ggg(x1, x2, x3)  =  U45_ggg(x1, x2, x3)
U46_ggg(x1, x2, x3)  =  U46_ggg(x1, x2, x3)
U47_ggg(x1, x2, x3)  =  U47_ggg(x1, x2, x3)
U48_ggg(x1, x2, x3)  =  U48_ggg(x1, x2, x3)
U49_ggg(x1, x2, x3)  =  U49_ggg(x1, x2, x3)
U50_ggg(x1, x2, x3)  =  U50_ggg(x1, x2, x3)
U51_ggg(x1, x2, x3)  =  U51_ggg(x1, x2, x3)
U52_ggg(x1, x2, x3)  =  U52_ggg(x1, x2, x3)
U53_ggg(x1, x2, x3)  =  U53_ggg(x1, x2, x3)
U54_ggg(x1, x2, x3)  =  U54_ggg(x1, x2, x3)
U55_ggg(x1, x2, x3)  =  U55_ggg(x1, x2, x3)
U56_ggg(x1, x2, x3)  =  U56_ggg(x1, x2, x3)
U57_ggg(x1, x2, x3)  =  U57_ggg(x1, x2, x3)
U58_ggg(x1, x2, x3)  =  U58_ggg(x1, x2, x3)
U59_ggg(x1, x2, x3)  =  U59_ggg(x1, x2, x3)
U60_ggg(x1, x2, x3)  =  U60_ggg(x1, x2, x3)
U61_ggg(x1, x2, x3)  =  U61_ggg(x1, x2, x3)
U62_ggg(x1, x2, x3)  =  U62_ggg(x1, x2, x3)
U63_ggg(x1, x2, x3, x4)  =  U63_ggg(x1, x2, x3, x4)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x1, x2, x3, x4)
U65_ggg(x1, x2, x3, x4, x5)  =  U65_ggg(x1, x2, x3, x5)
U42_gga(x1, x2, x3)  =  U42_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x2, x3)
U44_gga(x1, x2, x3)  =  U44_gga(x1, x2, x3)
U67_ggg(x1, x2, x3, x4)  =  U67_ggg(x1, x2, x3, x4)
U68_ggg(x1, x2, x3, x4)  =  U68_ggg(x1, x2, x3, x4)
U45_gga(x1, x2, x3)  =  U45_gga(x1, x2, x3)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x2, x3)
U47_gga(x1, x2, x3)  =  U47_gga(x1, x2, x3)
U48_gga(x1, x2, x3)  =  U48_gga(x1, x2, x3)
U49_gga(x1, x2, x3)  =  U49_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x2, x3)
U51_gga(x1, x2, x3)  =  U51_gga(x1, x2, x3)
U52_gga(x1, x2, x3)  =  U52_gga(x1, x2, x3)
U53_gga(x1, x2, x3)  =  U53_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x2, x3)
U58_gga(x1, x2, x3)  =  U58_gga(x1, x2, x3)
U59_gga(x1, x2, x3)  =  U59_gga(x1, x2, x3)
U60_gga(x1, x2, x3)  =  U60_gga(x1, x2, x3)
U61_gga(x1, x2, x3)  =  U61_gga(x1, x2, x3)
U62_gga(x1, x2, x3)  =  U62_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4)  =  U63_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x1, x2, x4)
U65_gga(x1, x2, x3, x4, x5)  =  U65_gga(x1, x2, x5)
U67_gga(x1, x2, x3, x4)  =  U67_gga(x1, x2, x4)
U68_gga(x1, x2, x3, x4)  =  U68_gga(x1, x2, x4)
U69_gga(x1, x2, x3, x4)  =  U69_gga(x1, x2, x4)
plusc166_in_gga(x1, x2, x3)  =  plusc166_in_gga(x1, x2)
plusc166_out_gga(x1, x2, x3)  =  plusc166_out_gga(x1, x2, x3)
U71_gga(x1, x2, x3, x4)  =  U71_gga(x1, x2, x4)
U66_gga(x1, x2, x3, x4)  =  U66_gga(x1, x2, x4)
plusc154_in_gga(x1, x2, x3)  =  plusc154_in_gga(x1, x2)
plusc154_out_gga(x1, x2, x3)  =  plusc154_out_gga(x1, x2, x3)
U70_gga(x1, x2, x3, x4)  =  U70_gga(x1, x2, x4)
U69_ggg(x1, x2, x3, x4)  =  U69_ggg(x1, x2, x3, x4)
plusc166_in_ggg(x1, x2, x3)  =  plusc166_in_ggg(x1, x2, x3)
plusc166_out_ggg(x1, x2, x3)  =  plusc166_out_ggg(x1, x2, x3)
U71_ggg(x1, x2, x3, x4)  =  U71_ggg(x1, x2, x3, x4)
U66_ggg(x1, x2, x3, x4)  =  U66_ggg(x1, x2, x3, x4)
plusc154_in_ggg(x1, x2, x3)  =  plusc154_in_ggg(x1, x2, x3)
plusc154_out_ggg(x1, x2, x3)  =  plusc154_out_ggg(x1, x2, x3)
U70_ggg(x1, x2, x3, x4)  =  U70_ggg(x1, x2, x3, x4)
PLUS19_IN_GGA(x1, x2, x3)  =  PLUS19_IN_GGA(x1, x2)

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

(49) UsableRulesProof (EQUIVALENT transformation)

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

(50) Obligation:

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

PLUS19_IN_GGA(s(T49), T50, s(T52)) → PLUS19_IN_GGA(T49, T50, T52)

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

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

(51) PiDPToQDPProof (SOUND transformation)

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

(52) Obligation:

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

PLUS19_IN_GGA(s(T49), T50) → PLUS19_IN_GGA(T49, T50)

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

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

  • PLUS19_IN_GGA(s(T49), T50) → PLUS19_IN_GGA(T49, T50)
    The graph contains the following edges 1 > 1, 2 >= 2

(54) YES