(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)).

Query: times(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
timesK_in_ga(x1, x2)  =  timesK_in_ga(x1)
timesK_out_ga(x1, x2)  =  timesK_out_ga(x1, x2)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
plusD_in_gga(x1, x2, x3)  =  plusD_in_gga(x1, x2)
plusD_out_gga(x1, x2, x3)  =  plusD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U18_gaga(x1, x2, x3, x4, x5)  =  U18_gaga(x1, x3, x5)
evenE_in_ga(x1, x2)  =  evenE_in_ga(x1)
evenE_out_ga(x1, x2)  =  evenE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x2, x3, x5)
ifL_in_ggga(x1, x2, x3, x4)  =  ifL_in_ggga(x1, x2, x3)
true  =  true
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
pM_in_gagaa(x1, x2, x3, x4, x5)  =  pM_in_gagaa(x1, x3)
U20_gagaa(x1, x2, x3, x4, x5, x6)  =  U20_gagaa(x1, x3, x6)
halfO_in_ga(x1, x2)  =  halfO_in_ga(x1)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
halfF_in_ga(x1, x2)  =  halfF_in_ga(x1)
halfF_out_ga(x1, x2)  =  halfF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
halfO_out_ga(x1, x2)  =  halfO_out_ga(x1, x2)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x2, x3, x6)
pU_in_ggaa(x1, x2, x3, x4)  =  pU_in_ggaa(x1, x2)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U24_gaga(x1, x2, x3, x4, x5)  =  U24_gaga(x1, x3, x5)
U25_gaga(x1, x2, x3, x4, x5)  =  U25_gaga(x1, x2, x3, x5)
ifQ_in_ggga(x1, x2, x3, x4)  =  ifQ_in_ggga(x1, x2, x3)
U13_ggga(x1, x2, x3, x4)  =  U13_ggga(x1, x2, x4)
pR_in_gagaa(x1, x2, x3, x4, x5)  =  pR_in_gagaa(x1, x3)
U26_gagaa(x1, x2, x3, x4, x5, x6)  =  U26_gagaa(x1, x3, x6)
U27_gagaa(x1, x2, x3, x4, x5, x6)  =  U27_gagaa(x1, x2, x3, x6)
pV_in_ggaa(x1, x2, x3, x4)  =  pV_in_ggaa(x1, x2)
U28_ggaa(x1, x2, x3, x4, x5)  =  U28_ggaa(x1, x2, x5)
U29_ggaa(x1, x2, x3, x4, x5)  =  U29_ggaa(x1, x2, x3, x5)
plusT_in_ga(x1, x2)  =  plusT_in_ga(x1)
plusT_out_ga(x1, x2)  =  plusT_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pV_out_ggaa(x1, x2, x3, x4)  =  pV_out_ggaa(x1, x2, x3, x4)
pR_out_gagaa(x1, x2, x3, x4, x5)  =  pR_out_gagaa(x1, x2, x3, x4, x5)
ifQ_out_ggga(x1, x2, x3, x4)  =  ifQ_out_ggga(x1, x2, x3, x4)
false  =  false
U14_ggga(x1, x2, x3, x4)  =  U14_ggga(x1, x2, x4)
pS_in_ggaa(x1, x2, x3, x4)  =  pS_in_ggaa(x1, x2)
U30_ggaa(x1, x2, x3, x4, x5)  =  U30_ggaa(x1, x2, x5)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pS_out_ggaa(x1, x2, x3, x4)  =  pS_out_ggaa(x1, x2, x3, x4)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x3, x5)
plusP_in_ga(x1, x2)  =  plusP_in_ga(x1)
plusP_out_ga(x1, x2)  =  plusP_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
pU_out_ggaa(x1, x2, x3, x4)  =  pU_out_ggaa(x1, x2, x3, x4)
pM_out_gagaa(x1, x2, x3, x4, x5)  =  pM_out_gagaa(x1, x2, x3, x4, x5)
ifL_out_ggga(x1, x2, x3, x4)  =  ifL_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
pN_in_ggaa(x1, x2, x3, x4)  =  pN_in_ggaa(x1, x2)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x5)
U33_ggaa(x1, x2, x3, x4, x5)  =  U33_ggaa(x1, x2, x3, x5)
pN_out_ggaa(x1, x2, x3, x4)  =  pN_out_ggaa(x1, x2, x3, x4)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x1, x2, x3, x4)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

TIMESA_IN_GGA(s(0), T21, T23) → U1_GGA(T21, T23, pB_in_gaa(T21, X37, T23))
TIMESA_IN_GGA(s(0), T21, T23) → PB_IN_GAA(T21, X37, T23)
PB_IN_GAA(T21, T27, T23) → U16_GAA(T21, T27, T23, timesK_in_ga(T21, T27))
PB_IN_GAA(T21, T27, T23) → TIMESK_IN_GA(T21, T27)
U16_GAA(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_GAA(T21, T27, T23, plusD_in_gga(T21, T27, T23))
U16_GAA(T21, T27, T23, timesK_out_ga(T21, T27)) → PLUSD_IN_GGA(T21, T27, T23)
PLUSD_IN_GGA(s(T47), T48, s(T50)) → U3_GGA(T47, T48, T50, plusD_in_gga(T47, T48, T50))
PLUSD_IN_GGA(s(T47), T48, s(T50)) → PLUSD_IN_GGA(T47, T48, T50)
TIMESA_IN_GGA(s(s(T55)), T10, T12) → U2_GGA(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
TIMESA_IN_GGA(s(s(T55)), T10, T12) → PC_IN_GAGA(T55, X78, T10, T12)
PC_IN_GAGA(T55, T56, T10, T12) → U18_GAGA(T55, T56, T10, T12, evenE_in_ga(T55, T56))
PC_IN_GAGA(T55, T56, T10, T12) → EVENE_IN_GA(T55, T56)
EVENE_IN_GA(s(s(T59)), X87) → U4_GA(T59, X87, evenE_in_ga(T59, X87))
EVENE_IN_GA(s(s(T59)), X87) → EVENE_IN_GA(T59, X87)
U18_GAGA(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_GAGA(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
U18_GAGA(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → IFL_IN_GGGA(T56, T55, T10, T12)
IFL_IN_GGGA(true, T75, T76, T78) → U9_GGGA(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
IFL_IN_GGGA(true, T75, T76, T78) → PM_IN_GAGAA(T75, X112, T76, X113, T78)
PM_IN_GAGAA(T75, T79, T76, X113, T78) → U20_GAGAA(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
PM_IN_GAGAA(T75, T79, T76, X113, T78) → HALFO_IN_GA(T75, T79)
HALFO_IN_GA(T82, s(X122)) → U11_GA(T82, X122, halfF_in_ga(T82, X122))
HALFO_IN_GA(T82, s(X122)) → HALFF_IN_GA(T82, X122)
HALFF_IN_GA(s(s(T85)), s(X131)) → U5_GA(T85, X131, halfF_in_ga(T85, X131))
HALFF_IN_GA(s(s(T85)), s(X131)) → HALFF_IN_GA(T85, X131)
U20_GAGAA(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_GAGAA(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
U20_GAGAA(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → PU_IN_GGAA(T79, T76, X113, T78)
PU_IN_GGAA(T79, T76, T88, T78) → U22_GGAA(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
PU_IN_GGAA(T79, T76, T88, T78) → TIMESG_IN_GGA(T79, T76, T88)
TIMESG_IN_GGA(s(T100), T101, X154) → U6_GGA(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
TIMESG_IN_GGA(s(T100), T101, X154) → PH_IN_GAGA(T100, X153, T101, X154)
PH_IN_GAGA(T100, T102, T101, X154) → U24_GAGA(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
PH_IN_GAGA(T100, T102, T101, X154) → EVENE_IN_GA(s(T100), T102)
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_GAGA(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101, X154)
IFQ_IN_GGGA(true, T113, T114, X186) → U13_GGGA(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
IFQ_IN_GGGA(true, T113, T114, X186) → PR_IN_GAGAA(T113, X184, T114, X185, X186)
PR_IN_GAGAA(T113, T115, T114, X185, X186) → U26_GAGAA(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
PR_IN_GAGAA(T113, T115, T114, X185, X186) → HALFF_IN_GA(s(T113), T115)
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_GAGAA(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114, X185, X186)
PV_IN_GGAA(T115, T114, T118, X186) → U28_GGAA(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
PV_IN_GGAA(T115, T114, T118, X186) → TIMESG_IN_GGA(T115, T114, T118)
U28_GGAA(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_GGAA(T115, T114, T118, X186, plusT_in_ga(T118, X186))
U28_GGAA(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → PLUST_IN_GA(T118, X186)
PLUST_IN_GA(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_GA(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
PLUST_IN_GA(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → PLUSI_IN_GGA(T144, s(s(s(s(s(s(s(T144))))))), X342)
PLUSI_IN_GGA(s(T157), T158, s(X363)) → U7_GGA(T157, T158, X363, plusI_in_gga(T157, T158, X363))
PLUSI_IN_GGA(s(T157), T158, s(X363)) → PLUSI_IN_GGA(T157, T158, X363)
IFQ_IN_GGGA(false, T165, T166, X379) → U14_GGGA(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
IFQ_IN_GGGA(false, T165, T166, X379) → PS_IN_GGAA(T165, T166, X378, X379)
PS_IN_GGAA(T165, T166, T169, X379) → U30_GGAA(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
PS_IN_GGAA(T165, T166, T169, X379) → TIMESG_IN_GGA(T165, T166, T169)
U30_GGAA(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_GGAA(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
U30_GGAA(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → PLUSJ_IN_GGA(T166, T169, X379)
PLUSJ_IN_GGA(s(T183), T184, s(X402)) → U8_GGA(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
PLUSJ_IN_GGA(s(T183), T184, s(X402)) → PLUSJ_IN_GGA(T183, T184, X402)
U22_GGAA(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_GGAA(T79, T76, T88, T78, plusP_in_ga(T88, T78))
U22_GGAA(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → PLUSP_IN_GA(T88, T78)
PLUSP_IN_GA(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_GA(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
PLUSP_IN_GA(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → PLUSD_IN_GGA(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)
IFL_IN_GGGA(false, T252, T253, T255) → U10_GGGA(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
IFL_IN_GGGA(false, T252, T253, T255) → PN_IN_GGAA(T252, T253, X547, T255)
PN_IN_GGAA(T252, T253, T256, T255) → U32_GGAA(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
PN_IN_GGAA(T252, T253, T256, T255) → TIMESG_IN_GGA(s(T252), T253, T256)
U32_GGAA(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_GGAA(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U32_GGAA(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → PLUSD_IN_GGA(T253, T256, T255)

The TRS R consists of the following rules:

timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
timesK_in_ga(x1, x2)  =  timesK_in_ga(x1)
timesK_out_ga(x1, x2)  =  timesK_out_ga(x1, x2)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
plusD_in_gga(x1, x2, x3)  =  plusD_in_gga(x1, x2)
plusD_out_gga(x1, x2, x3)  =  plusD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U18_gaga(x1, x2, x3, x4, x5)  =  U18_gaga(x1, x3, x5)
evenE_in_ga(x1, x2)  =  evenE_in_ga(x1)
evenE_out_ga(x1, x2)  =  evenE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x2, x3, x5)
ifL_in_ggga(x1, x2, x3, x4)  =  ifL_in_ggga(x1, x2, x3)
true  =  true
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
pM_in_gagaa(x1, x2, x3, x4, x5)  =  pM_in_gagaa(x1, x3)
U20_gagaa(x1, x2, x3, x4, x5, x6)  =  U20_gagaa(x1, x3, x6)
halfO_in_ga(x1, x2)  =  halfO_in_ga(x1)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
halfF_in_ga(x1, x2)  =  halfF_in_ga(x1)
halfF_out_ga(x1, x2)  =  halfF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
halfO_out_ga(x1, x2)  =  halfO_out_ga(x1, x2)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x2, x3, x6)
pU_in_ggaa(x1, x2, x3, x4)  =  pU_in_ggaa(x1, x2)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U24_gaga(x1, x2, x3, x4, x5)  =  U24_gaga(x1, x3, x5)
U25_gaga(x1, x2, x3, x4, x5)  =  U25_gaga(x1, x2, x3, x5)
ifQ_in_ggga(x1, x2, x3, x4)  =  ifQ_in_ggga(x1, x2, x3)
U13_ggga(x1, x2, x3, x4)  =  U13_ggga(x1, x2, x4)
pR_in_gagaa(x1, x2, x3, x4, x5)  =  pR_in_gagaa(x1, x3)
U26_gagaa(x1, x2, x3, x4, x5, x6)  =  U26_gagaa(x1, x3, x6)
U27_gagaa(x1, x2, x3, x4, x5, x6)  =  U27_gagaa(x1, x2, x3, x6)
pV_in_ggaa(x1, x2, x3, x4)  =  pV_in_ggaa(x1, x2)
U28_ggaa(x1, x2, x3, x4, x5)  =  U28_ggaa(x1, x2, x5)
U29_ggaa(x1, x2, x3, x4, x5)  =  U29_ggaa(x1, x2, x3, x5)
plusT_in_ga(x1, x2)  =  plusT_in_ga(x1)
plusT_out_ga(x1, x2)  =  plusT_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pV_out_ggaa(x1, x2, x3, x4)  =  pV_out_ggaa(x1, x2, x3, x4)
pR_out_gagaa(x1, x2, x3, x4, x5)  =  pR_out_gagaa(x1, x2, x3, x4, x5)
ifQ_out_ggga(x1, x2, x3, x4)  =  ifQ_out_ggga(x1, x2, x3, x4)
false  =  false
U14_ggga(x1, x2, x3, x4)  =  U14_ggga(x1, x2, x4)
pS_in_ggaa(x1, x2, x3, x4)  =  pS_in_ggaa(x1, x2)
U30_ggaa(x1, x2, x3, x4, x5)  =  U30_ggaa(x1, x2, x5)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pS_out_ggaa(x1, x2, x3, x4)  =  pS_out_ggaa(x1, x2, x3, x4)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x3, x5)
plusP_in_ga(x1, x2)  =  plusP_in_ga(x1)
plusP_out_ga(x1, x2)  =  plusP_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
pU_out_ggaa(x1, x2, x3, x4)  =  pU_out_ggaa(x1, x2, x3, x4)
pM_out_gagaa(x1, x2, x3, x4, x5)  =  pM_out_gagaa(x1, x2, x3, x4, x5)
ifL_out_ggga(x1, x2, x3, x4)  =  ifL_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
pN_in_ggaa(x1, x2, x3, x4)  =  pN_in_ggaa(x1, x2)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x5)
U33_ggaa(x1, x2, x3, x4, x5)  =  U33_ggaa(x1, x2, x3, x5)
pN_out_ggaa(x1, x2, x3, x4)  =  pN_out_ggaa(x1, x2, x3, x4)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x1, x2, x3, x4)
TIMESA_IN_GGA(x1, x2, x3)  =  TIMESA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3)  =  U1_GGA(x1, x3)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U16_GAA(x1, x2, x3, x4)  =  U16_GAA(x1, x4)
TIMESK_IN_GA(x1, x2)  =  TIMESK_IN_GA(x1)
U17_GAA(x1, x2, x3, x4)  =  U17_GAA(x1, x2, x4)
PLUSD_IN_GGA(x1, x2, x3)  =  PLUSD_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
PC_IN_GAGA(x1, x2, x3, x4)  =  PC_IN_GAGA(x1, x3)
U18_GAGA(x1, x2, x3, x4, x5)  =  U18_GAGA(x1, x3, x5)
EVENE_IN_GA(x1, x2)  =  EVENE_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U19_GAGA(x1, x2, x3, x4, x5)  =  U19_GAGA(x1, x2, x3, x5)
IFL_IN_GGGA(x1, x2, x3, x4)  =  IFL_IN_GGGA(x1, x2, x3)
U9_GGGA(x1, x2, x3, x4)  =  U9_GGGA(x1, x2, x4)
PM_IN_GAGAA(x1, x2, x3, x4, x5)  =  PM_IN_GAGAA(x1, x3)
U20_GAGAA(x1, x2, x3, x4, x5, x6)  =  U20_GAGAA(x1, x3, x6)
HALFO_IN_GA(x1, x2)  =  HALFO_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
HALFF_IN_GA(x1, x2)  =  HALFF_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U21_GAGAA(x1, x2, x3, x4, x5, x6)  =  U21_GAGAA(x1, x2, x3, x6)
PU_IN_GGAA(x1, x2, x3, x4)  =  PU_IN_GGAA(x1, x2)
U22_GGAA(x1, x2, x3, x4, x5)  =  U22_GGAA(x1, x2, x5)
TIMESG_IN_GGA(x1, x2, x3)  =  TIMESG_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U24_GAGA(x1, x2, x3, x4, x5)  =  U24_GAGA(x1, x3, x5)
U25_GAGA(x1, x2, x3, x4, x5)  =  U25_GAGA(x1, x2, x3, x5)
IFQ_IN_GGGA(x1, x2, x3, x4)  =  IFQ_IN_GGGA(x1, x2, x3)
U13_GGGA(x1, x2, x3, x4)  =  U13_GGGA(x1, x2, x4)
PR_IN_GAGAA(x1, x2, x3, x4, x5)  =  PR_IN_GAGAA(x1, x3)
U26_GAGAA(x1, x2, x3, x4, x5, x6)  =  U26_GAGAA(x1, x3, x6)
U27_GAGAA(x1, x2, x3, x4, x5, x6)  =  U27_GAGAA(x1, x2, x3, x6)
PV_IN_GGAA(x1, x2, x3, x4)  =  PV_IN_GGAA(x1, x2)
U28_GGAA(x1, x2, x3, x4, x5)  =  U28_GGAA(x1, x2, x5)
U29_GGAA(x1, x2, x3, x4, x5)  =  U29_GGAA(x1, x2, x3, x5)
PLUST_IN_GA(x1, x2)  =  PLUST_IN_GA(x1)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
PLUSI_IN_GGA(x1, x2, x3)  =  PLUSI_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U14_GGGA(x1, x2, x3, x4)  =  U14_GGGA(x1, x2, x4)
PS_IN_GGAA(x1, x2, x3, x4)  =  PS_IN_GGAA(x1, x2)
U30_GGAA(x1, x2, x3, x4, x5)  =  U30_GGAA(x1, x2, x5)
U31_GGAA(x1, x2, x3, x4, x5)  =  U31_GGAA(x1, x2, x3, x5)
PLUSJ_IN_GGA(x1, x2, x3)  =  PLUSJ_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U23_GGAA(x1, x2, x3, x4, x5)  =  U23_GGAA(x1, x2, x3, x5)
PLUSP_IN_GA(x1, x2)  =  PLUSP_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U10_GGGA(x1, x2, x3, x4)  =  U10_GGGA(x1, x2, x4)
PN_IN_GGAA(x1, x2, x3, x4)  =  PN_IN_GGAA(x1, x2)
U32_GGAA(x1, x2, x3, x4, x5)  =  U32_GGAA(x1, x2, x5)
U33_GGAA(x1, x2, x3, x4, x5)  =  U33_GGAA(x1, x2, x3, x5)

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

(4) Obligation:

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

TIMESA_IN_GGA(s(0), T21, T23) → U1_GGA(T21, T23, pB_in_gaa(T21, X37, T23))
TIMESA_IN_GGA(s(0), T21, T23) → PB_IN_GAA(T21, X37, T23)
PB_IN_GAA(T21, T27, T23) → U16_GAA(T21, T27, T23, timesK_in_ga(T21, T27))
PB_IN_GAA(T21, T27, T23) → TIMESK_IN_GA(T21, T27)
U16_GAA(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_GAA(T21, T27, T23, plusD_in_gga(T21, T27, T23))
U16_GAA(T21, T27, T23, timesK_out_ga(T21, T27)) → PLUSD_IN_GGA(T21, T27, T23)
PLUSD_IN_GGA(s(T47), T48, s(T50)) → U3_GGA(T47, T48, T50, plusD_in_gga(T47, T48, T50))
PLUSD_IN_GGA(s(T47), T48, s(T50)) → PLUSD_IN_GGA(T47, T48, T50)
TIMESA_IN_GGA(s(s(T55)), T10, T12) → U2_GGA(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
TIMESA_IN_GGA(s(s(T55)), T10, T12) → PC_IN_GAGA(T55, X78, T10, T12)
PC_IN_GAGA(T55, T56, T10, T12) → U18_GAGA(T55, T56, T10, T12, evenE_in_ga(T55, T56))
PC_IN_GAGA(T55, T56, T10, T12) → EVENE_IN_GA(T55, T56)
EVENE_IN_GA(s(s(T59)), X87) → U4_GA(T59, X87, evenE_in_ga(T59, X87))
EVENE_IN_GA(s(s(T59)), X87) → EVENE_IN_GA(T59, X87)
U18_GAGA(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_GAGA(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
U18_GAGA(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → IFL_IN_GGGA(T56, T55, T10, T12)
IFL_IN_GGGA(true, T75, T76, T78) → U9_GGGA(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
IFL_IN_GGGA(true, T75, T76, T78) → PM_IN_GAGAA(T75, X112, T76, X113, T78)
PM_IN_GAGAA(T75, T79, T76, X113, T78) → U20_GAGAA(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
PM_IN_GAGAA(T75, T79, T76, X113, T78) → HALFO_IN_GA(T75, T79)
HALFO_IN_GA(T82, s(X122)) → U11_GA(T82, X122, halfF_in_ga(T82, X122))
HALFO_IN_GA(T82, s(X122)) → HALFF_IN_GA(T82, X122)
HALFF_IN_GA(s(s(T85)), s(X131)) → U5_GA(T85, X131, halfF_in_ga(T85, X131))
HALFF_IN_GA(s(s(T85)), s(X131)) → HALFF_IN_GA(T85, X131)
U20_GAGAA(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_GAGAA(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
U20_GAGAA(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → PU_IN_GGAA(T79, T76, X113, T78)
PU_IN_GGAA(T79, T76, T88, T78) → U22_GGAA(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
PU_IN_GGAA(T79, T76, T88, T78) → TIMESG_IN_GGA(T79, T76, T88)
TIMESG_IN_GGA(s(T100), T101, X154) → U6_GGA(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
TIMESG_IN_GGA(s(T100), T101, X154) → PH_IN_GAGA(T100, X153, T101, X154)
PH_IN_GAGA(T100, T102, T101, X154) → U24_GAGA(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
PH_IN_GAGA(T100, T102, T101, X154) → EVENE_IN_GA(s(T100), T102)
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_GAGA(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101, X154)
IFQ_IN_GGGA(true, T113, T114, X186) → U13_GGGA(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
IFQ_IN_GGGA(true, T113, T114, X186) → PR_IN_GAGAA(T113, X184, T114, X185, X186)
PR_IN_GAGAA(T113, T115, T114, X185, X186) → U26_GAGAA(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
PR_IN_GAGAA(T113, T115, T114, X185, X186) → HALFF_IN_GA(s(T113), T115)
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_GAGAA(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114, X185, X186)
PV_IN_GGAA(T115, T114, T118, X186) → U28_GGAA(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
PV_IN_GGAA(T115, T114, T118, X186) → TIMESG_IN_GGA(T115, T114, T118)
U28_GGAA(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_GGAA(T115, T114, T118, X186, plusT_in_ga(T118, X186))
U28_GGAA(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → PLUST_IN_GA(T118, X186)
PLUST_IN_GA(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_GA(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
PLUST_IN_GA(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → PLUSI_IN_GGA(T144, s(s(s(s(s(s(s(T144))))))), X342)
PLUSI_IN_GGA(s(T157), T158, s(X363)) → U7_GGA(T157, T158, X363, plusI_in_gga(T157, T158, X363))
PLUSI_IN_GGA(s(T157), T158, s(X363)) → PLUSI_IN_GGA(T157, T158, X363)
IFQ_IN_GGGA(false, T165, T166, X379) → U14_GGGA(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
IFQ_IN_GGGA(false, T165, T166, X379) → PS_IN_GGAA(T165, T166, X378, X379)
PS_IN_GGAA(T165, T166, T169, X379) → U30_GGAA(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
PS_IN_GGAA(T165, T166, T169, X379) → TIMESG_IN_GGA(T165, T166, T169)
U30_GGAA(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_GGAA(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
U30_GGAA(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → PLUSJ_IN_GGA(T166, T169, X379)
PLUSJ_IN_GGA(s(T183), T184, s(X402)) → U8_GGA(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
PLUSJ_IN_GGA(s(T183), T184, s(X402)) → PLUSJ_IN_GGA(T183, T184, X402)
U22_GGAA(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_GGAA(T79, T76, T88, T78, plusP_in_ga(T88, T78))
U22_GGAA(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → PLUSP_IN_GA(T88, T78)
PLUSP_IN_GA(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_GA(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
PLUSP_IN_GA(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → PLUSD_IN_GGA(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)
IFL_IN_GGGA(false, T252, T253, T255) → U10_GGGA(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
IFL_IN_GGGA(false, T252, T253, T255) → PN_IN_GGAA(T252, T253, X547, T255)
PN_IN_GGAA(T252, T253, T256, T255) → U32_GGAA(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
PN_IN_GGAA(T252, T253, T256, T255) → TIMESG_IN_GGA(s(T252), T253, T256)
U32_GGAA(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_GGAA(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U32_GGAA(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → PLUSD_IN_GGA(T253, T256, T255)

The TRS R consists of the following rules:

timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
timesK_in_ga(x1, x2)  =  timesK_in_ga(x1)
timesK_out_ga(x1, x2)  =  timesK_out_ga(x1, x2)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
plusD_in_gga(x1, x2, x3)  =  plusD_in_gga(x1, x2)
plusD_out_gga(x1, x2, x3)  =  plusD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U18_gaga(x1, x2, x3, x4, x5)  =  U18_gaga(x1, x3, x5)
evenE_in_ga(x1, x2)  =  evenE_in_ga(x1)
evenE_out_ga(x1, x2)  =  evenE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x2, x3, x5)
ifL_in_ggga(x1, x2, x3, x4)  =  ifL_in_ggga(x1, x2, x3)
true  =  true
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
pM_in_gagaa(x1, x2, x3, x4, x5)  =  pM_in_gagaa(x1, x3)
U20_gagaa(x1, x2, x3, x4, x5, x6)  =  U20_gagaa(x1, x3, x6)
halfO_in_ga(x1, x2)  =  halfO_in_ga(x1)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
halfF_in_ga(x1, x2)  =  halfF_in_ga(x1)
halfF_out_ga(x1, x2)  =  halfF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
halfO_out_ga(x1, x2)  =  halfO_out_ga(x1, x2)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x2, x3, x6)
pU_in_ggaa(x1, x2, x3, x4)  =  pU_in_ggaa(x1, x2)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U24_gaga(x1, x2, x3, x4, x5)  =  U24_gaga(x1, x3, x5)
U25_gaga(x1, x2, x3, x4, x5)  =  U25_gaga(x1, x2, x3, x5)
ifQ_in_ggga(x1, x2, x3, x4)  =  ifQ_in_ggga(x1, x2, x3)
U13_ggga(x1, x2, x3, x4)  =  U13_ggga(x1, x2, x4)
pR_in_gagaa(x1, x2, x3, x4, x5)  =  pR_in_gagaa(x1, x3)
U26_gagaa(x1, x2, x3, x4, x5, x6)  =  U26_gagaa(x1, x3, x6)
U27_gagaa(x1, x2, x3, x4, x5, x6)  =  U27_gagaa(x1, x2, x3, x6)
pV_in_ggaa(x1, x2, x3, x4)  =  pV_in_ggaa(x1, x2)
U28_ggaa(x1, x2, x3, x4, x5)  =  U28_ggaa(x1, x2, x5)
U29_ggaa(x1, x2, x3, x4, x5)  =  U29_ggaa(x1, x2, x3, x5)
plusT_in_ga(x1, x2)  =  plusT_in_ga(x1)
plusT_out_ga(x1, x2)  =  plusT_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pV_out_ggaa(x1, x2, x3, x4)  =  pV_out_ggaa(x1, x2, x3, x4)
pR_out_gagaa(x1, x2, x3, x4, x5)  =  pR_out_gagaa(x1, x2, x3, x4, x5)
ifQ_out_ggga(x1, x2, x3, x4)  =  ifQ_out_ggga(x1, x2, x3, x4)
false  =  false
U14_ggga(x1, x2, x3, x4)  =  U14_ggga(x1, x2, x4)
pS_in_ggaa(x1, x2, x3, x4)  =  pS_in_ggaa(x1, x2)
U30_ggaa(x1, x2, x3, x4, x5)  =  U30_ggaa(x1, x2, x5)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pS_out_ggaa(x1, x2, x3, x4)  =  pS_out_ggaa(x1, x2, x3, x4)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x3, x5)
plusP_in_ga(x1, x2)  =  plusP_in_ga(x1)
plusP_out_ga(x1, x2)  =  plusP_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
pU_out_ggaa(x1, x2, x3, x4)  =  pU_out_ggaa(x1, x2, x3, x4)
pM_out_gagaa(x1, x2, x3, x4, x5)  =  pM_out_gagaa(x1, x2, x3, x4, x5)
ifL_out_ggga(x1, x2, x3, x4)  =  ifL_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
pN_in_ggaa(x1, x2, x3, x4)  =  pN_in_ggaa(x1, x2)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x5)
U33_ggaa(x1, x2, x3, x4, x5)  =  U33_ggaa(x1, x2, x3, x5)
pN_out_ggaa(x1, x2, x3, x4)  =  pN_out_ggaa(x1, x2, x3, x4)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x1, x2, x3, x4)
TIMESA_IN_GGA(x1, x2, x3)  =  TIMESA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3)  =  U1_GGA(x1, x3)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U16_GAA(x1, x2, x3, x4)  =  U16_GAA(x1, x4)
TIMESK_IN_GA(x1, x2)  =  TIMESK_IN_GA(x1)
U17_GAA(x1, x2, x3, x4)  =  U17_GAA(x1, x2, x4)
PLUSD_IN_GGA(x1, x2, x3)  =  PLUSD_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
PC_IN_GAGA(x1, x2, x3, x4)  =  PC_IN_GAGA(x1, x3)
U18_GAGA(x1, x2, x3, x4, x5)  =  U18_GAGA(x1, x3, x5)
EVENE_IN_GA(x1, x2)  =  EVENE_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U19_GAGA(x1, x2, x3, x4, x5)  =  U19_GAGA(x1, x2, x3, x5)
IFL_IN_GGGA(x1, x2, x3, x4)  =  IFL_IN_GGGA(x1, x2, x3)
U9_GGGA(x1, x2, x3, x4)  =  U9_GGGA(x1, x2, x4)
PM_IN_GAGAA(x1, x2, x3, x4, x5)  =  PM_IN_GAGAA(x1, x3)
U20_GAGAA(x1, x2, x3, x4, x5, x6)  =  U20_GAGAA(x1, x3, x6)
HALFO_IN_GA(x1, x2)  =  HALFO_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
HALFF_IN_GA(x1, x2)  =  HALFF_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U21_GAGAA(x1, x2, x3, x4, x5, x6)  =  U21_GAGAA(x1, x2, x3, x6)
PU_IN_GGAA(x1, x2, x3, x4)  =  PU_IN_GGAA(x1, x2)
U22_GGAA(x1, x2, x3, x4, x5)  =  U22_GGAA(x1, x2, x5)
TIMESG_IN_GGA(x1, x2, x3)  =  TIMESG_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U24_GAGA(x1, x2, x3, x4, x5)  =  U24_GAGA(x1, x3, x5)
U25_GAGA(x1, x2, x3, x4, x5)  =  U25_GAGA(x1, x2, x3, x5)
IFQ_IN_GGGA(x1, x2, x3, x4)  =  IFQ_IN_GGGA(x1, x2, x3)
U13_GGGA(x1, x2, x3, x4)  =  U13_GGGA(x1, x2, x4)
PR_IN_GAGAA(x1, x2, x3, x4, x5)  =  PR_IN_GAGAA(x1, x3)
U26_GAGAA(x1, x2, x3, x4, x5, x6)  =  U26_GAGAA(x1, x3, x6)
U27_GAGAA(x1, x2, x3, x4, x5, x6)  =  U27_GAGAA(x1, x2, x3, x6)
PV_IN_GGAA(x1, x2, x3, x4)  =  PV_IN_GGAA(x1, x2)
U28_GGAA(x1, x2, x3, x4, x5)  =  U28_GGAA(x1, x2, x5)
U29_GGAA(x1, x2, x3, x4, x5)  =  U29_GGAA(x1, x2, x3, x5)
PLUST_IN_GA(x1, x2)  =  PLUST_IN_GA(x1)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
PLUSI_IN_GGA(x1, x2, x3)  =  PLUSI_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U14_GGGA(x1, x2, x3, x4)  =  U14_GGGA(x1, x2, x4)
PS_IN_GGAA(x1, x2, x3, x4)  =  PS_IN_GGAA(x1, x2)
U30_GGAA(x1, x2, x3, x4, x5)  =  U30_GGAA(x1, x2, x5)
U31_GGAA(x1, x2, x3, x4, x5)  =  U31_GGAA(x1, x2, x3, x5)
PLUSJ_IN_GGA(x1, x2, x3)  =  PLUSJ_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U23_GGAA(x1, x2, x3, x4, x5)  =  U23_GGAA(x1, x2, x3, x5)
PLUSP_IN_GA(x1, x2)  =  PLUSP_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U10_GGGA(x1, x2, x3, x4)  =  U10_GGGA(x1, x2, x4)
PN_IN_GGAA(x1, x2, x3, x4)  =  PN_IN_GGAA(x1, x2)
U32_GGAA(x1, x2, x3, x4, x5)  =  U32_GGAA(x1, x2, x5)
U33_GGAA(x1, x2, x3, x4, x5)  =  U33_GGAA(x1, x2, x3, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

PLUSJ_IN_GGA(s(T183), T184, s(X402)) → PLUSJ_IN_GGA(T183, T184, X402)

The TRS R consists of the following rules:

timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
timesK_in_ga(x1, x2)  =  timesK_in_ga(x1)
timesK_out_ga(x1, x2)  =  timesK_out_ga(x1, x2)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
plusD_in_gga(x1, x2, x3)  =  plusD_in_gga(x1, x2)
plusD_out_gga(x1, x2, x3)  =  plusD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U18_gaga(x1, x2, x3, x4, x5)  =  U18_gaga(x1, x3, x5)
evenE_in_ga(x1, x2)  =  evenE_in_ga(x1)
evenE_out_ga(x1, x2)  =  evenE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x2, x3, x5)
ifL_in_ggga(x1, x2, x3, x4)  =  ifL_in_ggga(x1, x2, x3)
true  =  true
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
pM_in_gagaa(x1, x2, x3, x4, x5)  =  pM_in_gagaa(x1, x3)
U20_gagaa(x1, x2, x3, x4, x5, x6)  =  U20_gagaa(x1, x3, x6)
halfO_in_ga(x1, x2)  =  halfO_in_ga(x1)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
halfF_in_ga(x1, x2)  =  halfF_in_ga(x1)
halfF_out_ga(x1, x2)  =  halfF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
halfO_out_ga(x1, x2)  =  halfO_out_ga(x1, x2)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x2, x3, x6)
pU_in_ggaa(x1, x2, x3, x4)  =  pU_in_ggaa(x1, x2)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U24_gaga(x1, x2, x3, x4, x5)  =  U24_gaga(x1, x3, x5)
U25_gaga(x1, x2, x3, x4, x5)  =  U25_gaga(x1, x2, x3, x5)
ifQ_in_ggga(x1, x2, x3, x4)  =  ifQ_in_ggga(x1, x2, x3)
U13_ggga(x1, x2, x3, x4)  =  U13_ggga(x1, x2, x4)
pR_in_gagaa(x1, x2, x3, x4, x5)  =  pR_in_gagaa(x1, x3)
U26_gagaa(x1, x2, x3, x4, x5, x6)  =  U26_gagaa(x1, x3, x6)
U27_gagaa(x1, x2, x3, x4, x5, x6)  =  U27_gagaa(x1, x2, x3, x6)
pV_in_ggaa(x1, x2, x3, x4)  =  pV_in_ggaa(x1, x2)
U28_ggaa(x1, x2, x3, x4, x5)  =  U28_ggaa(x1, x2, x5)
U29_ggaa(x1, x2, x3, x4, x5)  =  U29_ggaa(x1, x2, x3, x5)
plusT_in_ga(x1, x2)  =  plusT_in_ga(x1)
plusT_out_ga(x1, x2)  =  plusT_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pV_out_ggaa(x1, x2, x3, x4)  =  pV_out_ggaa(x1, x2, x3, x4)
pR_out_gagaa(x1, x2, x3, x4, x5)  =  pR_out_gagaa(x1, x2, x3, x4, x5)
ifQ_out_ggga(x1, x2, x3, x4)  =  ifQ_out_ggga(x1, x2, x3, x4)
false  =  false
U14_ggga(x1, x2, x3, x4)  =  U14_ggga(x1, x2, x4)
pS_in_ggaa(x1, x2, x3, x4)  =  pS_in_ggaa(x1, x2)
U30_ggaa(x1, x2, x3, x4, x5)  =  U30_ggaa(x1, x2, x5)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pS_out_ggaa(x1, x2, x3, x4)  =  pS_out_ggaa(x1, x2, x3, x4)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x3, x5)
plusP_in_ga(x1, x2)  =  plusP_in_ga(x1)
plusP_out_ga(x1, x2)  =  plusP_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
pU_out_ggaa(x1, x2, x3, x4)  =  pU_out_ggaa(x1, x2, x3, x4)
pM_out_gagaa(x1, x2, x3, x4, x5)  =  pM_out_gagaa(x1, x2, x3, x4, x5)
ifL_out_ggga(x1, x2, x3, x4)  =  ifL_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
pN_in_ggaa(x1, x2, x3, x4)  =  pN_in_ggaa(x1, x2)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x5)
U33_ggaa(x1, x2, x3, x4, x5)  =  U33_ggaa(x1, x2, x3, x5)
pN_out_ggaa(x1, x2, x3, x4)  =  pN_out_ggaa(x1, x2, x3, x4)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x1, x2, x3, x4)
PLUSJ_IN_GGA(x1, x2, x3)  =  PLUSJ_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:

PLUSJ_IN_GGA(s(T183), T184, s(X402)) → PLUSJ_IN_GGA(T183, T184, X402)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PLUSJ_IN_GGA(x1, x2, x3)  =  PLUSJ_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:

PLUSJ_IN_GGA(s(T183), T184) → PLUSJ_IN_GGA(T183, T184)

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:

  • PLUSJ_IN_GGA(s(T183), T184) → PLUSJ_IN_GGA(T183, T184)
    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:

PLUSI_IN_GGA(s(T157), T158, s(X363)) → PLUSI_IN_GGA(T157, T158, X363)

The TRS R consists of the following rules:

timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
timesK_in_ga(x1, x2)  =  timesK_in_ga(x1)
timesK_out_ga(x1, x2)  =  timesK_out_ga(x1, x2)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
plusD_in_gga(x1, x2, x3)  =  plusD_in_gga(x1, x2)
plusD_out_gga(x1, x2, x3)  =  plusD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U18_gaga(x1, x2, x3, x4, x5)  =  U18_gaga(x1, x3, x5)
evenE_in_ga(x1, x2)  =  evenE_in_ga(x1)
evenE_out_ga(x1, x2)  =  evenE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x2, x3, x5)
ifL_in_ggga(x1, x2, x3, x4)  =  ifL_in_ggga(x1, x2, x3)
true  =  true
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
pM_in_gagaa(x1, x2, x3, x4, x5)  =  pM_in_gagaa(x1, x3)
U20_gagaa(x1, x2, x3, x4, x5, x6)  =  U20_gagaa(x1, x3, x6)
halfO_in_ga(x1, x2)  =  halfO_in_ga(x1)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
halfF_in_ga(x1, x2)  =  halfF_in_ga(x1)
halfF_out_ga(x1, x2)  =  halfF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
halfO_out_ga(x1, x2)  =  halfO_out_ga(x1, x2)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x2, x3, x6)
pU_in_ggaa(x1, x2, x3, x4)  =  pU_in_ggaa(x1, x2)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U24_gaga(x1, x2, x3, x4, x5)  =  U24_gaga(x1, x3, x5)
U25_gaga(x1, x2, x3, x4, x5)  =  U25_gaga(x1, x2, x3, x5)
ifQ_in_ggga(x1, x2, x3, x4)  =  ifQ_in_ggga(x1, x2, x3)
U13_ggga(x1, x2, x3, x4)  =  U13_ggga(x1, x2, x4)
pR_in_gagaa(x1, x2, x3, x4, x5)  =  pR_in_gagaa(x1, x3)
U26_gagaa(x1, x2, x3, x4, x5, x6)  =  U26_gagaa(x1, x3, x6)
U27_gagaa(x1, x2, x3, x4, x5, x6)  =  U27_gagaa(x1, x2, x3, x6)
pV_in_ggaa(x1, x2, x3, x4)  =  pV_in_ggaa(x1, x2)
U28_ggaa(x1, x2, x3, x4, x5)  =  U28_ggaa(x1, x2, x5)
U29_ggaa(x1, x2, x3, x4, x5)  =  U29_ggaa(x1, x2, x3, x5)
plusT_in_ga(x1, x2)  =  plusT_in_ga(x1)
plusT_out_ga(x1, x2)  =  plusT_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pV_out_ggaa(x1, x2, x3, x4)  =  pV_out_ggaa(x1, x2, x3, x4)
pR_out_gagaa(x1, x2, x3, x4, x5)  =  pR_out_gagaa(x1, x2, x3, x4, x5)
ifQ_out_ggga(x1, x2, x3, x4)  =  ifQ_out_ggga(x1, x2, x3, x4)
false  =  false
U14_ggga(x1, x2, x3, x4)  =  U14_ggga(x1, x2, x4)
pS_in_ggaa(x1, x2, x3, x4)  =  pS_in_ggaa(x1, x2)
U30_ggaa(x1, x2, x3, x4, x5)  =  U30_ggaa(x1, x2, x5)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pS_out_ggaa(x1, x2, x3, x4)  =  pS_out_ggaa(x1, x2, x3, x4)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x3, x5)
plusP_in_ga(x1, x2)  =  plusP_in_ga(x1)
plusP_out_ga(x1, x2)  =  plusP_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
pU_out_ggaa(x1, x2, x3, x4)  =  pU_out_ggaa(x1, x2, x3, x4)
pM_out_gagaa(x1, x2, x3, x4, x5)  =  pM_out_gagaa(x1, x2, x3, x4, x5)
ifL_out_ggga(x1, x2, x3, x4)  =  ifL_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
pN_in_ggaa(x1, x2, x3, x4)  =  pN_in_ggaa(x1, x2)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x5)
U33_ggaa(x1, x2, x3, x4, x5)  =  U33_ggaa(x1, x2, x3, x5)
pN_out_ggaa(x1, x2, x3, x4)  =  pN_out_ggaa(x1, x2, x3, x4)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x1, x2, x3, x4)
PLUSI_IN_GGA(x1, x2, x3)  =  PLUSI_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:

PLUSI_IN_GGA(s(T157), T158, s(X363)) → PLUSI_IN_GGA(T157, T158, X363)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PLUSI_IN_GGA(x1, x2, x3)  =  PLUSI_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:

PLUSI_IN_GGA(s(T157), T158) → PLUSI_IN_GGA(T157, T158)

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:

  • PLUSI_IN_GGA(s(T157), T158) → PLUSI_IN_GGA(T157, T158)
    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:

HALFF_IN_GA(s(s(T85)), s(X131)) → HALFF_IN_GA(T85, X131)

The TRS R consists of the following rules:

timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
timesK_in_ga(x1, x2)  =  timesK_in_ga(x1)
timesK_out_ga(x1, x2)  =  timesK_out_ga(x1, x2)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
plusD_in_gga(x1, x2, x3)  =  plusD_in_gga(x1, x2)
plusD_out_gga(x1, x2, x3)  =  plusD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U18_gaga(x1, x2, x3, x4, x5)  =  U18_gaga(x1, x3, x5)
evenE_in_ga(x1, x2)  =  evenE_in_ga(x1)
evenE_out_ga(x1, x2)  =  evenE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x2, x3, x5)
ifL_in_ggga(x1, x2, x3, x4)  =  ifL_in_ggga(x1, x2, x3)
true  =  true
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
pM_in_gagaa(x1, x2, x3, x4, x5)  =  pM_in_gagaa(x1, x3)
U20_gagaa(x1, x2, x3, x4, x5, x6)  =  U20_gagaa(x1, x3, x6)
halfO_in_ga(x1, x2)  =  halfO_in_ga(x1)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
halfF_in_ga(x1, x2)  =  halfF_in_ga(x1)
halfF_out_ga(x1, x2)  =  halfF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
halfO_out_ga(x1, x2)  =  halfO_out_ga(x1, x2)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x2, x3, x6)
pU_in_ggaa(x1, x2, x3, x4)  =  pU_in_ggaa(x1, x2)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U24_gaga(x1, x2, x3, x4, x5)  =  U24_gaga(x1, x3, x5)
U25_gaga(x1, x2, x3, x4, x5)  =  U25_gaga(x1, x2, x3, x5)
ifQ_in_ggga(x1, x2, x3, x4)  =  ifQ_in_ggga(x1, x2, x3)
U13_ggga(x1, x2, x3, x4)  =  U13_ggga(x1, x2, x4)
pR_in_gagaa(x1, x2, x3, x4, x5)  =  pR_in_gagaa(x1, x3)
U26_gagaa(x1, x2, x3, x4, x5, x6)  =  U26_gagaa(x1, x3, x6)
U27_gagaa(x1, x2, x3, x4, x5, x6)  =  U27_gagaa(x1, x2, x3, x6)
pV_in_ggaa(x1, x2, x3, x4)  =  pV_in_ggaa(x1, x2)
U28_ggaa(x1, x2, x3, x4, x5)  =  U28_ggaa(x1, x2, x5)
U29_ggaa(x1, x2, x3, x4, x5)  =  U29_ggaa(x1, x2, x3, x5)
plusT_in_ga(x1, x2)  =  plusT_in_ga(x1)
plusT_out_ga(x1, x2)  =  plusT_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pV_out_ggaa(x1, x2, x3, x4)  =  pV_out_ggaa(x1, x2, x3, x4)
pR_out_gagaa(x1, x2, x3, x4, x5)  =  pR_out_gagaa(x1, x2, x3, x4, x5)
ifQ_out_ggga(x1, x2, x3, x4)  =  ifQ_out_ggga(x1, x2, x3, x4)
false  =  false
U14_ggga(x1, x2, x3, x4)  =  U14_ggga(x1, x2, x4)
pS_in_ggaa(x1, x2, x3, x4)  =  pS_in_ggaa(x1, x2)
U30_ggaa(x1, x2, x3, x4, x5)  =  U30_ggaa(x1, x2, x5)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pS_out_ggaa(x1, x2, x3, x4)  =  pS_out_ggaa(x1, x2, x3, x4)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x3, x5)
plusP_in_ga(x1, x2)  =  plusP_in_ga(x1)
plusP_out_ga(x1, x2)  =  plusP_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
pU_out_ggaa(x1, x2, x3, x4)  =  pU_out_ggaa(x1, x2, x3, x4)
pM_out_gagaa(x1, x2, x3, x4, x5)  =  pM_out_gagaa(x1, x2, x3, x4, x5)
ifL_out_ggga(x1, x2, x3, x4)  =  ifL_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
pN_in_ggaa(x1, x2, x3, x4)  =  pN_in_ggaa(x1, x2)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x5)
U33_ggaa(x1, x2, x3, x4, x5)  =  U33_ggaa(x1, x2, x3, x5)
pN_out_ggaa(x1, x2, x3, x4)  =  pN_out_ggaa(x1, x2, x3, x4)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x1, x2, x3, x4)
HALFF_IN_GA(x1, x2)  =  HALFF_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:

HALFF_IN_GA(s(s(T85)), s(X131)) → HALFF_IN_GA(T85, X131)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
HALFF_IN_GA(x1, x2)  =  HALFF_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:

HALFF_IN_GA(s(s(T85))) → HALFF_IN_GA(T85)

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:

  • HALFF_IN_GA(s(s(T85))) → HALFF_IN_GA(T85)
    The graph contains the following edges 1 > 1

(27) YES

(28) Obligation:

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

EVENE_IN_GA(s(s(T59)), X87) → EVENE_IN_GA(T59, X87)

The TRS R consists of the following rules:

timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
timesK_in_ga(x1, x2)  =  timesK_in_ga(x1)
timesK_out_ga(x1, x2)  =  timesK_out_ga(x1, x2)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
plusD_in_gga(x1, x2, x3)  =  plusD_in_gga(x1, x2)
plusD_out_gga(x1, x2, x3)  =  plusD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U18_gaga(x1, x2, x3, x4, x5)  =  U18_gaga(x1, x3, x5)
evenE_in_ga(x1, x2)  =  evenE_in_ga(x1)
evenE_out_ga(x1, x2)  =  evenE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x2, x3, x5)
ifL_in_ggga(x1, x2, x3, x4)  =  ifL_in_ggga(x1, x2, x3)
true  =  true
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
pM_in_gagaa(x1, x2, x3, x4, x5)  =  pM_in_gagaa(x1, x3)
U20_gagaa(x1, x2, x3, x4, x5, x6)  =  U20_gagaa(x1, x3, x6)
halfO_in_ga(x1, x2)  =  halfO_in_ga(x1)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
halfF_in_ga(x1, x2)  =  halfF_in_ga(x1)
halfF_out_ga(x1, x2)  =  halfF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
halfO_out_ga(x1, x2)  =  halfO_out_ga(x1, x2)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x2, x3, x6)
pU_in_ggaa(x1, x2, x3, x4)  =  pU_in_ggaa(x1, x2)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U24_gaga(x1, x2, x3, x4, x5)  =  U24_gaga(x1, x3, x5)
U25_gaga(x1, x2, x3, x4, x5)  =  U25_gaga(x1, x2, x3, x5)
ifQ_in_ggga(x1, x2, x3, x4)  =  ifQ_in_ggga(x1, x2, x3)
U13_ggga(x1, x2, x3, x4)  =  U13_ggga(x1, x2, x4)
pR_in_gagaa(x1, x2, x3, x4, x5)  =  pR_in_gagaa(x1, x3)
U26_gagaa(x1, x2, x3, x4, x5, x6)  =  U26_gagaa(x1, x3, x6)
U27_gagaa(x1, x2, x3, x4, x5, x6)  =  U27_gagaa(x1, x2, x3, x6)
pV_in_ggaa(x1, x2, x3, x4)  =  pV_in_ggaa(x1, x2)
U28_ggaa(x1, x2, x3, x4, x5)  =  U28_ggaa(x1, x2, x5)
U29_ggaa(x1, x2, x3, x4, x5)  =  U29_ggaa(x1, x2, x3, x5)
plusT_in_ga(x1, x2)  =  plusT_in_ga(x1)
plusT_out_ga(x1, x2)  =  plusT_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pV_out_ggaa(x1, x2, x3, x4)  =  pV_out_ggaa(x1, x2, x3, x4)
pR_out_gagaa(x1, x2, x3, x4, x5)  =  pR_out_gagaa(x1, x2, x3, x4, x5)
ifQ_out_ggga(x1, x2, x3, x4)  =  ifQ_out_ggga(x1, x2, x3, x4)
false  =  false
U14_ggga(x1, x2, x3, x4)  =  U14_ggga(x1, x2, x4)
pS_in_ggaa(x1, x2, x3, x4)  =  pS_in_ggaa(x1, x2)
U30_ggaa(x1, x2, x3, x4, x5)  =  U30_ggaa(x1, x2, x5)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pS_out_ggaa(x1, x2, x3, x4)  =  pS_out_ggaa(x1, x2, x3, x4)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x3, x5)
plusP_in_ga(x1, x2)  =  plusP_in_ga(x1)
plusP_out_ga(x1, x2)  =  plusP_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
pU_out_ggaa(x1, x2, x3, x4)  =  pU_out_ggaa(x1, x2, x3, x4)
pM_out_gagaa(x1, x2, x3, x4, x5)  =  pM_out_gagaa(x1, x2, x3, x4, x5)
ifL_out_ggga(x1, x2, x3, x4)  =  ifL_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
pN_in_ggaa(x1, x2, x3, x4)  =  pN_in_ggaa(x1, x2)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x5)
U33_ggaa(x1, x2, x3, x4, x5)  =  U33_ggaa(x1, x2, x3, x5)
pN_out_ggaa(x1, x2, x3, x4)  =  pN_out_ggaa(x1, x2, x3, x4)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x1, x2, x3, x4)
EVENE_IN_GA(x1, x2)  =  EVENE_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:

EVENE_IN_GA(s(s(T59)), X87) → EVENE_IN_GA(T59, X87)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
EVENE_IN_GA(x1, x2)  =  EVENE_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:

EVENE_IN_GA(s(s(T59))) → EVENE_IN_GA(T59)

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:

  • EVENE_IN_GA(s(s(T59))) → EVENE_IN_GA(T59)
    The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

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

PH_IN_GAGA(T100, T102, T101, X154) → U24_GAGA(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101, X154)
IFQ_IN_GGGA(true, T113, T114, X186) → PR_IN_GAGAA(T113, X184, T114, X185, X186)
PR_IN_GAGAA(T113, T115, T114, X185, X186) → U26_GAGAA(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114, X185, X186)
PV_IN_GGAA(T115, T114, T118, X186) → TIMESG_IN_GGA(T115, T114, T118)
TIMESG_IN_GGA(s(T100), T101, X154) → PH_IN_GAGA(T100, X153, T101, X154)
IFQ_IN_GGGA(false, T165, T166, X379) → PS_IN_GGAA(T165, T166, X378, X379)
PS_IN_GGAA(T165, T166, T169, X379) → TIMESG_IN_GGA(T165, T166, T169)

The TRS R consists of the following rules:

timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
timesK_in_ga(x1, x2)  =  timesK_in_ga(x1)
timesK_out_ga(x1, x2)  =  timesK_out_ga(x1, x2)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
plusD_in_gga(x1, x2, x3)  =  plusD_in_gga(x1, x2)
plusD_out_gga(x1, x2, x3)  =  plusD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U18_gaga(x1, x2, x3, x4, x5)  =  U18_gaga(x1, x3, x5)
evenE_in_ga(x1, x2)  =  evenE_in_ga(x1)
evenE_out_ga(x1, x2)  =  evenE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x2, x3, x5)
ifL_in_ggga(x1, x2, x3, x4)  =  ifL_in_ggga(x1, x2, x3)
true  =  true
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
pM_in_gagaa(x1, x2, x3, x4, x5)  =  pM_in_gagaa(x1, x3)
U20_gagaa(x1, x2, x3, x4, x5, x6)  =  U20_gagaa(x1, x3, x6)
halfO_in_ga(x1, x2)  =  halfO_in_ga(x1)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
halfF_in_ga(x1, x2)  =  halfF_in_ga(x1)
halfF_out_ga(x1, x2)  =  halfF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
halfO_out_ga(x1, x2)  =  halfO_out_ga(x1, x2)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x2, x3, x6)
pU_in_ggaa(x1, x2, x3, x4)  =  pU_in_ggaa(x1, x2)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U24_gaga(x1, x2, x3, x4, x5)  =  U24_gaga(x1, x3, x5)
U25_gaga(x1, x2, x3, x4, x5)  =  U25_gaga(x1, x2, x3, x5)
ifQ_in_ggga(x1, x2, x3, x4)  =  ifQ_in_ggga(x1, x2, x3)
U13_ggga(x1, x2, x3, x4)  =  U13_ggga(x1, x2, x4)
pR_in_gagaa(x1, x2, x3, x4, x5)  =  pR_in_gagaa(x1, x3)
U26_gagaa(x1, x2, x3, x4, x5, x6)  =  U26_gagaa(x1, x3, x6)
U27_gagaa(x1, x2, x3, x4, x5, x6)  =  U27_gagaa(x1, x2, x3, x6)
pV_in_ggaa(x1, x2, x3, x4)  =  pV_in_ggaa(x1, x2)
U28_ggaa(x1, x2, x3, x4, x5)  =  U28_ggaa(x1, x2, x5)
U29_ggaa(x1, x2, x3, x4, x5)  =  U29_ggaa(x1, x2, x3, x5)
plusT_in_ga(x1, x2)  =  plusT_in_ga(x1)
plusT_out_ga(x1, x2)  =  plusT_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pV_out_ggaa(x1, x2, x3, x4)  =  pV_out_ggaa(x1, x2, x3, x4)
pR_out_gagaa(x1, x2, x3, x4, x5)  =  pR_out_gagaa(x1, x2, x3, x4, x5)
ifQ_out_ggga(x1, x2, x3, x4)  =  ifQ_out_ggga(x1, x2, x3, x4)
false  =  false
U14_ggga(x1, x2, x3, x4)  =  U14_ggga(x1, x2, x4)
pS_in_ggaa(x1, x2, x3, x4)  =  pS_in_ggaa(x1, x2)
U30_ggaa(x1, x2, x3, x4, x5)  =  U30_ggaa(x1, x2, x5)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pS_out_ggaa(x1, x2, x3, x4)  =  pS_out_ggaa(x1, x2, x3, x4)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x3, x5)
plusP_in_ga(x1, x2)  =  plusP_in_ga(x1)
plusP_out_ga(x1, x2)  =  plusP_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
pU_out_ggaa(x1, x2, x3, x4)  =  pU_out_ggaa(x1, x2, x3, x4)
pM_out_gagaa(x1, x2, x3, x4, x5)  =  pM_out_gagaa(x1, x2, x3, x4, x5)
ifL_out_ggga(x1, x2, x3, x4)  =  ifL_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
pN_in_ggaa(x1, x2, x3, x4)  =  pN_in_ggaa(x1, x2)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x5)
U33_ggaa(x1, x2, x3, x4, x5)  =  U33_ggaa(x1, x2, x3, x5)
pN_out_ggaa(x1, x2, x3, x4)  =  pN_out_ggaa(x1, x2, x3, x4)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x1, x2, x3, x4)
TIMESG_IN_GGA(x1, x2, x3)  =  TIMESG_IN_GGA(x1, x2)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U24_GAGA(x1, x2, x3, x4, x5)  =  U24_GAGA(x1, x3, x5)
IFQ_IN_GGGA(x1, x2, x3, x4)  =  IFQ_IN_GGGA(x1, x2, x3)
PR_IN_GAGAA(x1, x2, x3, x4, x5)  =  PR_IN_GAGAA(x1, x3)
U26_GAGAA(x1, x2, x3, x4, x5, x6)  =  U26_GAGAA(x1, x3, x6)
PV_IN_GGAA(x1, x2, x3, x4)  =  PV_IN_GGAA(x1, x2)
PS_IN_GGAA(x1, x2, x3, x4)  =  PS_IN_GGAA(x1, x2)

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:

PH_IN_GAGA(T100, T102, T101, X154) → U24_GAGA(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_GAGA(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101, X154)
IFQ_IN_GGGA(true, T113, T114, X186) → PR_IN_GAGAA(T113, X184, T114, X185, X186)
PR_IN_GAGAA(T113, T115, T114, X185, X186) → U26_GAGAA(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_GAGAA(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114, X185, X186)
PV_IN_GGAA(T115, T114, T118, X186) → TIMESG_IN_GGA(T115, T114, T118)
TIMESG_IN_GGA(s(T100), T101, X154) → PH_IN_GAGA(T100, X153, T101, X154)
IFQ_IN_GGGA(false, T165, T166, X379) → PS_IN_GGAA(T165, T166, X378, X379)
PS_IN_GGAA(T165, T166, T169, X379) → TIMESG_IN_GGA(T165, T166, T169)

The TRS R consists of the following rules:

evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
evenE_in_ga(x1, x2)  =  evenE_in_ga(x1)
evenE_out_ga(x1, x2)  =  evenE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
true  =  true
halfF_in_ga(x1, x2)  =  halfF_in_ga(x1)
halfF_out_ga(x1, x2)  =  halfF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
false  =  false
TIMESG_IN_GGA(x1, x2, x3)  =  TIMESG_IN_GGA(x1, x2)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U24_GAGA(x1, x2, x3, x4, x5)  =  U24_GAGA(x1, x3, x5)
IFQ_IN_GGGA(x1, x2, x3, x4)  =  IFQ_IN_GGGA(x1, x2, x3)
PR_IN_GAGAA(x1, x2, x3, x4, x5)  =  PR_IN_GAGAA(x1, x3)
U26_GAGAA(x1, x2, x3, x4, x5, x6)  =  U26_GAGAA(x1, x3, x6)
PV_IN_GGAA(x1, x2, x3, x4)  =  PV_IN_GGAA(x1, x2)
PS_IN_GGAA(x1, x2, x3, x4)  =  PS_IN_GGAA(x1, x2)

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:

PH_IN_GAGA(T100, T101) → U24_GAGA(T100, T101, evenE_in_ga(s(T100)))
U24_GAGA(T100, T101, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101)
IFQ_IN_GGGA(true, T113, T114) → PR_IN_GAGAA(T113, T114)
PR_IN_GAGAA(T113, T114) → U26_GAGAA(T113, T114, halfF_in_ga(s(T113)))
U26_GAGAA(T113, T114, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114)
PV_IN_GGAA(T115, T114) → TIMESG_IN_GGA(T115, T114)
TIMESG_IN_GGA(s(T100), T101) → PH_IN_GAGA(T100, T101)
IFQ_IN_GGGA(false, T165, T166) → PS_IN_GGAA(T165, T166)
PS_IN_GGAA(T165, T166) → TIMESG_IN_GGA(T165, T166)

The TRS R consists of the following rules:

evenE_in_ga(s(0)) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59))) → U4_ga(T59, evenE_in_ga(T59))
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
U4_ga(T59, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0) → evenE_out_ga(0, true)
halfF_in_ga(0) → halfF_out_ga(0, 0)

The set Q consists of the following terms:

evenE_in_ga(x0)
halfF_in_ga(x0)
U4_ga(x0, x1)
U5_ga(x0, x1)

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

(40) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PS_IN_GGAA(T165, T166) → TIMESG_IN_GGA(T165, T166)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(IFQ_IN_GGGA(x1, x2, x3)) = 1 + x2   
POL(PH_IN_GAGA(x1, x2)) = 1 + x1   
POL(PR_IN_GAGAA(x1, x2)) = 1 + x1   
POL(PS_IN_GGAA(x1, x2)) = 1 + x1   
POL(PV_IN_GGAA(x1, x2)) = x1   
POL(TIMESG_IN_GGA(x1, x2)) = x1   
POL(U24_GAGA(x1, x2, x3)) = 1 + x1   
POL(U26_GAGAA(x1, x2, x3)) = x3   
POL(U4_ga(x1, x2)) = 0   
POL(U5_ga(x1, x2)) = 1 + x2   
POL(evenE_in_ga(x1)) = 0   
POL(evenE_out_ga(x1, x2)) = 0   
POL(false) = 0   
POL(halfF_in_ga(x1)) = x1   
POL(halfF_out_ga(x1, x2)) = x2   
POL(s(x1)) = 1 + x1   
POL(true) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
halfF_in_ga(0) → halfF_out_ga(0, 0)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))

(41) Obligation:

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

PH_IN_GAGA(T100, T101) → U24_GAGA(T100, T101, evenE_in_ga(s(T100)))
U24_GAGA(T100, T101, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101)
IFQ_IN_GGGA(true, T113, T114) → PR_IN_GAGAA(T113, T114)
PR_IN_GAGAA(T113, T114) → U26_GAGAA(T113, T114, halfF_in_ga(s(T113)))
U26_GAGAA(T113, T114, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114)
PV_IN_GGAA(T115, T114) → TIMESG_IN_GGA(T115, T114)
TIMESG_IN_GGA(s(T100), T101) → PH_IN_GAGA(T100, T101)
IFQ_IN_GGGA(false, T165, T166) → PS_IN_GGAA(T165, T166)

The TRS R consists of the following rules:

evenE_in_ga(s(0)) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59))) → U4_ga(T59, evenE_in_ga(T59))
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
U4_ga(T59, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0) → evenE_out_ga(0, true)
halfF_in_ga(0) → halfF_out_ga(0, 0)

The set Q consists of the following terms:

evenE_in_ga(x0)
halfF_in_ga(x0)
U4_ga(x0, x1)
U5_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:

U24_GAGA(T100, T101, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101)
IFQ_IN_GGGA(true, T113, T114) → PR_IN_GAGAA(T113, T114)
PR_IN_GAGAA(T113, T114) → U26_GAGAA(T113, T114, halfF_in_ga(s(T113)))
U26_GAGAA(T113, T114, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114)
PV_IN_GGAA(T115, T114) → TIMESG_IN_GGA(T115, T114)
TIMESG_IN_GGA(s(T100), T101) → PH_IN_GAGA(T100, T101)
PH_IN_GAGA(T100, T101) → U24_GAGA(T100, T101, evenE_in_ga(s(T100)))

The TRS R consists of the following rules:

evenE_in_ga(s(0)) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59))) → U4_ga(T59, evenE_in_ga(T59))
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
U4_ga(T59, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0) → evenE_out_ga(0, true)
halfF_in_ga(0) → halfF_out_ga(0, 0)

The set Q consists of the following terms:

evenE_in_ga(x0)
halfF_in_ga(x0)
U4_ga(x0, x1)
U5_ga(x0, x1)

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

(44) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

evenE_in_ga(s(0)) → evenE_out_ga(s(0), false)

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(IFQ_IN_GGGA(x1, x2, x3)) = x1   
POL(PH_IN_GAGA(x1, x2)) = 1   
POL(PR_IN_GAGAA(x1, x2)) = 1   
POL(PV_IN_GGAA(x1, x2)) = 1   
POL(TIMESG_IN_GGA(x1, x2)) = 1   
POL(U24_GAGA(x1, x2, x3)) = x3   
POL(U26_GAGAA(x1, x2, x3)) = 1   
POL(U4_ga(x1, x2)) = x2   
POL(U5_ga(x1, x2)) = 0   
POL(evenE_in_ga(x1)) = 1   
POL(evenE_out_ga(x1, x2)) = x2   
POL(false) = 0   
POL(halfF_in_ga(x1)) = 0   
POL(halfF_out_ga(x1, x2)) = 0   
POL(s(x1)) = 0   
POL(true) = 1   

(45) Obligation:

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

U24_GAGA(T100, T101, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101)
IFQ_IN_GGGA(true, T113, T114) → PR_IN_GAGAA(T113, T114)
PR_IN_GAGAA(T113, T114) → U26_GAGAA(T113, T114, halfF_in_ga(s(T113)))
U26_GAGAA(T113, T114, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114)
PV_IN_GGAA(T115, T114) → TIMESG_IN_GGA(T115, T114)
TIMESG_IN_GGA(s(T100), T101) → PH_IN_GAGA(T100, T101)
PH_IN_GAGA(T100, T101) → U24_GAGA(T100, T101, evenE_in_ga(s(T100)))

The TRS R consists of the following rules:

evenE_in_ga(s(s(T59))) → U4_ga(T59, evenE_in_ga(T59))
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
U4_ga(T59, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0) → evenE_out_ga(0, true)
halfF_in_ga(0) → halfF_out_ga(0, 0)

The set Q consists of the following terms:

evenE_in_ga(x0)
halfF_in_ga(x0)
U4_ga(x0, x1)
U5_ga(x0, x1)

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

(46) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


U24_GAGA(T100, T101, evenE_out_ga(s(T100), T102)) → IFQ_IN_GGGA(T102, T100, T101)
TIMESG_IN_GGA(s(T100), T101) → PH_IN_GAGA(T100, T101)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U26_GAGAA(x1, ..., x3) ) = x2 + x3


POL( halfF_in_ga(x1) ) = max{0, x1 - 2}


POL( s(x1) ) = 2x1 + 2


POL( U5_ga(x1, x2) ) = 2x1 + 2x2 + 2


POL( U24_GAGA(x1, ..., x3) ) = 2x1 + x2 + 1


POL( evenE_in_ga(x1) ) = 1


POL( U4_ga(x1, x2) ) = x1 + 2


POL( 0 ) = 0


POL( evenE_out_ga(x1, x2) ) = 2x1 + 2


POL( true ) = 0


POL( halfF_out_ga(x1, x2) ) = x2


POL( IFQ_IN_GGGA(x1, ..., x3) ) = 2x2 + x3


POL( PR_IN_GAGAA(x1, x2) ) = 2x1 + x2


POL( PV_IN_GGAA(x1, x2) ) = x1 + x2


POL( TIMESG_IN_GGA(x1, x2) ) = x1 + x2


POL( PH_IN_GAGA(x1, x2) ) = 2x1 + x2 + 1



The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
halfF_in_ga(0) → halfF_out_ga(0, 0)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))

(47) Obligation:

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

IFQ_IN_GGGA(true, T113, T114) → PR_IN_GAGAA(T113, T114)
PR_IN_GAGAA(T113, T114) → U26_GAGAA(T113, T114, halfF_in_ga(s(T113)))
U26_GAGAA(T113, T114, halfF_out_ga(s(T113), T115)) → PV_IN_GGAA(T115, T114)
PV_IN_GGAA(T115, T114) → TIMESG_IN_GGA(T115, T114)
PH_IN_GAGA(T100, T101) → U24_GAGA(T100, T101, evenE_in_ga(s(T100)))

The TRS R consists of the following rules:

evenE_in_ga(s(s(T59))) → U4_ga(T59, evenE_in_ga(T59))
halfF_in_ga(s(s(T85))) → U5_ga(T85, halfF_in_ga(T85))
U4_ga(T59, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U5_ga(T85, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
evenE_in_ga(0) → evenE_out_ga(0, true)
halfF_in_ga(0) → halfF_out_ga(0, 0)

The set Q consists of the following terms:

evenE_in_ga(x0)
halfF_in_ga(x0)
U4_ga(x0, x1)
U5_ga(x0, x1)

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

(48) DependencyGraphProof (EQUIVALENT transformation)

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

(49) TRUE

(50) Obligation:

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

PLUSD_IN_GGA(s(T47), T48, s(T50)) → PLUSD_IN_GGA(T47, T48, T50)

The TRS R consists of the following rules:

timesA_in_gga(0, T5, 0) → timesA_out_gga(0, T5, 0)
timesA_in_gga(s(0), T21, T23) → U1_gga(T21, T23, pB_in_gaa(T21, X37, T23))
pB_in_gaa(T21, T27, T23) → U16_gaa(T21, T27, T23, timesK_in_ga(T21, T27))
timesK_in_ga(T33, 0) → timesK_out_ga(T33, 0)
U16_gaa(T21, T27, T23, timesK_out_ga(T21, T27)) → U17_gaa(T21, T27, T23, plusD_in_gga(T21, T27, T23))
plusD_in_gga(0, T40, T40) → plusD_out_gga(0, T40, T40)
plusD_in_gga(s(T47), T48, s(T50)) → U3_gga(T47, T48, T50, plusD_in_gga(T47, T48, T50))
U3_gga(T47, T48, T50, plusD_out_gga(T47, T48, T50)) → plusD_out_gga(s(T47), T48, s(T50))
U17_gaa(T21, T27, T23, plusD_out_gga(T21, T27, T23)) → pB_out_gaa(T21, T27, T23)
U1_gga(T21, T23, pB_out_gaa(T21, X37, T23)) → timesA_out_gga(s(0), T21, T23)
timesA_in_gga(s(s(T55)), T10, T12) → U2_gga(T55, T10, T12, pC_in_gaga(T55, X78, T10, T12))
pC_in_gaga(T55, T56, T10, T12) → U18_gaga(T55, T56, T10, T12, evenE_in_ga(T55, T56))
evenE_in_ga(0, true) → evenE_out_ga(0, true)
evenE_in_ga(s(0), false) → evenE_out_ga(s(0), false)
evenE_in_ga(s(s(T59)), X87) → U4_ga(T59, X87, evenE_in_ga(T59, X87))
U4_ga(T59, X87, evenE_out_ga(T59, X87)) → evenE_out_ga(s(s(T59)), X87)
U18_gaga(T55, T56, T10, T12, evenE_out_ga(T55, T56)) → U19_gaga(T55, T56, T10, T12, ifL_in_ggga(T56, T55, T10, T12))
ifL_in_ggga(true, T75, T76, T78) → U9_ggga(T75, T76, T78, pM_in_gagaa(T75, X112, T76, X113, T78))
pM_in_gagaa(T75, T79, T76, X113, T78) → U20_gagaa(T75, T79, T76, X113, T78, halfO_in_ga(T75, T79))
halfO_in_ga(T82, s(X122)) → U11_ga(T82, X122, halfF_in_ga(T82, X122))
halfF_in_ga(0, 0) → halfF_out_ga(0, 0)
halfF_in_ga(s(s(T85)), s(X131)) → U5_ga(T85, X131, halfF_in_ga(T85, X131))
U5_ga(T85, X131, halfF_out_ga(T85, X131)) → halfF_out_ga(s(s(T85)), s(X131))
U11_ga(T82, X122, halfF_out_ga(T82, X122)) → halfO_out_ga(T82, s(X122))
U20_gagaa(T75, T79, T76, X113, T78, halfO_out_ga(T75, T79)) → U21_gagaa(T75, T79, T76, X113, T78, pU_in_ggaa(T79, T76, X113, T78))
pU_in_ggaa(T79, T76, T88, T78) → U22_ggaa(T79, T76, T88, T78, timesG_in_gga(T79, T76, T88))
timesG_in_gga(0, T95, 0) → timesG_out_gga(0, T95, 0)
timesG_in_gga(s(T100), T101, X154) → U6_gga(T100, T101, X154, pH_in_gaga(T100, X153, T101, X154))
pH_in_gaga(T100, T102, T101, X154) → U24_gaga(T100, T102, T101, X154, evenE_in_ga(s(T100), T102))
U24_gaga(T100, T102, T101, X154, evenE_out_ga(s(T100), T102)) → U25_gaga(T100, T102, T101, X154, ifQ_in_ggga(T102, T100, T101, X154))
ifQ_in_ggga(true, T113, T114, X186) → U13_ggga(T113, T114, X186, pR_in_gagaa(T113, X184, T114, X185, X186))
pR_in_gagaa(T113, T115, T114, X185, X186) → U26_gagaa(T113, T115, T114, X185, X186, halfF_in_ga(s(T113), T115))
U26_gagaa(T113, T115, T114, X185, X186, halfF_out_ga(s(T113), T115)) → U27_gagaa(T113, T115, T114, X185, X186, pV_in_ggaa(T115, T114, X185, X186))
pV_in_ggaa(T115, T114, T118, X186) → U28_ggaa(T115, T114, T118, X186, timesG_in_gga(T115, T114, T118))
U28_ggaa(T115, T114, T118, X186, timesG_out_gga(T115, T114, T118)) → U29_ggaa(T115, T114, T118, X186, plusT_in_ga(T118, X186))
plusT_in_ga(0, 0) → plusT_out_ga(0, 0)
plusT_in_ga(s(0), s(s(0))) → plusT_out_ga(s(0), s(s(0)))
plusT_in_ga(s(s(0)), s(s(s(s(0))))) → plusT_out_ga(s(s(0)), s(s(s(s(0)))))
plusT_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusT_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusT_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusT_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusT_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusT_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusT_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusT_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusT_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusT_in_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342))))))))) → U15_ga(T144, X342, plusI_in_gga(T144, s(s(s(s(s(s(s(T144))))))), X342))
plusI_in_gga(0, T152, s(T152)) → plusI_out_gga(0, T152, s(T152))
plusI_in_gga(s(T157), T158, s(X363)) → U7_gga(T157, T158, X363, plusI_in_gga(T157, T158, X363))
U7_gga(T157, T158, X363, plusI_out_gga(T157, T158, X363)) → plusI_out_gga(s(T157), T158, s(X363))
U15_ga(T144, X342, plusI_out_gga(T144, s(s(s(s(s(s(s(T144))))))), X342)) → plusT_out_ga(s(s(s(s(s(s(s(s(T144)))))))), s(s(s(s(s(s(s(s(X342)))))))))
U29_ggaa(T115, T114, T118, X186, plusT_out_ga(T118, X186)) → pV_out_ggaa(T115, T114, T118, X186)
U27_gagaa(T113, T115, T114, X185, X186, pV_out_ggaa(T115, T114, X185, X186)) → pR_out_gagaa(T113, T115, T114, X185, X186)
U13_ggga(T113, T114, X186, pR_out_gagaa(T113, X184, T114, X185, X186)) → ifQ_out_ggga(true, T113, T114, X186)
ifQ_in_ggga(false, T165, T166, X379) → U14_ggga(T165, T166, X379, pS_in_ggaa(T165, T166, X378, X379))
pS_in_ggaa(T165, T166, T169, X379) → U30_ggaa(T165, T166, T169, X379, timesG_in_gga(T165, T166, T169))
U30_ggaa(T165, T166, T169, X379, timesG_out_gga(T165, T166, T169)) → U31_ggaa(T165, T166, T169, X379, plusJ_in_gga(T166, T169, X379))
plusJ_in_gga(0, T178, T178) → plusJ_out_gga(0, T178, T178)
plusJ_in_gga(s(T183), T184, s(X402)) → U8_gga(T183, T184, X402, plusJ_in_gga(T183, T184, X402))
U8_gga(T183, T184, X402, plusJ_out_gga(T183, T184, X402)) → plusJ_out_gga(s(T183), T184, s(X402))
U31_ggaa(T165, T166, T169, X379, plusJ_out_gga(T166, T169, X379)) → pS_out_ggaa(T165, T166, T169, X379)
U14_ggga(T165, T166, X379, pS_out_ggaa(T165, T166, X378, X379)) → ifQ_out_ggga(false, T165, T166, X379)
U25_gaga(T100, T102, T101, X154, ifQ_out_ggga(T102, T100, T101, X154)) → pH_out_gaga(T100, T102, T101, X154)
U6_gga(T100, T101, X154, pH_out_gaga(T100, X153, T101, X154)) → timesG_out_gga(s(T100), T101, X154)
U22_ggaa(T79, T76, T88, T78, timesG_out_gga(T79, T76, T88)) → U23_ggaa(T79, T76, T88, T78, plusP_in_ga(T88, T78))
plusP_in_ga(0, 0) → plusP_out_ga(0, 0)
plusP_in_ga(s(0), s(s(0))) → plusP_out_ga(s(0), s(s(0)))
plusP_in_ga(s(s(0)), s(s(s(s(0))))) → plusP_out_ga(s(s(0)), s(s(s(s(0)))))
plusP_in_ga(s(s(s(0))), s(s(s(s(s(s(0))))))) → plusP_out_ga(s(s(s(0))), s(s(s(s(s(s(0)))))))
plusP_in_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0))))))))) → plusP_out_ga(s(s(s(s(0)))), s(s(s(s(s(s(s(s(0)))))))))
plusP_in_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0))))))))))) → plusP_out_ga(s(s(s(s(s(0))))), s(s(s(s(s(s(s(s(s(s(0)))))))))))
plusP_in_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) → plusP_out_ga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) → plusP_out_ga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))
plusP_in_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242))))))))) → U12_ga(T240, T242, plusD_in_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242))
U12_ga(T240, T242, plusD_out_gga(T240, s(s(s(s(s(s(s(s(T240)))))))), T242)) → plusP_out_ga(s(s(s(s(s(s(s(s(T240)))))))), s(s(s(s(s(s(s(s(T242)))))))))
U23_ggaa(T79, T76, T88, T78, plusP_out_ga(T88, T78)) → pU_out_ggaa(T79, T76, T88, T78)
U21_gagaa(T75, T79, T76, X113, T78, pU_out_ggaa(T79, T76, X113, T78)) → pM_out_gagaa(T75, T79, T76, X113, T78)
U9_ggga(T75, T76, T78, pM_out_gagaa(T75, X112, T76, X113, T78)) → ifL_out_ggga(true, T75, T76, T78)
ifL_in_ggga(false, T252, T253, T255) → U10_ggga(T252, T253, T255, pN_in_ggaa(T252, T253, X547, T255))
pN_in_ggaa(T252, T253, T256, T255) → U32_ggaa(T252, T253, T256, T255, timesG_in_gga(s(T252), T253, T256))
U32_ggaa(T252, T253, T256, T255, timesG_out_gga(s(T252), T253, T256)) → U33_ggaa(T252, T253, T256, T255, plusD_in_gga(T253, T256, T255))
U33_ggaa(T252, T253, T256, T255, plusD_out_gga(T253, T256, T255)) → pN_out_ggaa(T252, T253, T256, T255)
U10_ggga(T252, T253, T255, pN_out_ggaa(T252, T253, X547, T255)) → ifL_out_ggga(false, T252, T253, T255)
U19_gaga(T55, T56, T10, T12, ifL_out_ggga(T56, T55, T10, T12)) → pC_out_gaga(T55, T56, T10, T12)
U2_gga(T55, T10, T12, pC_out_gaga(T55, X78, T10, T12)) → timesA_out_gga(s(s(T55)), T10, T12)

The argument filtering Pi contains the following mapping:
timesA_in_gga(x1, x2, x3)  =  timesA_in_gga(x1, x2)
0  =  0
timesA_out_gga(x1, x2, x3)  =  timesA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
timesK_in_ga(x1, x2)  =  timesK_in_ga(x1)
timesK_out_ga(x1, x2)  =  timesK_out_ga(x1, x2)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
plusD_in_gga(x1, x2, x3)  =  plusD_in_gga(x1, x2)
plusD_out_gga(x1, x2, x3)  =  plusD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_gaga(x1, x2, x3, x4)  =  pC_in_gaga(x1, x3)
U18_gaga(x1, x2, x3, x4, x5)  =  U18_gaga(x1, x3, x5)
evenE_in_ga(x1, x2)  =  evenE_in_ga(x1)
evenE_out_ga(x1, x2)  =  evenE_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x2, x3, x5)
ifL_in_ggga(x1, x2, x3, x4)  =  ifL_in_ggga(x1, x2, x3)
true  =  true
U9_ggga(x1, x2, x3, x4)  =  U9_ggga(x1, x2, x4)
pM_in_gagaa(x1, x2, x3, x4, x5)  =  pM_in_gagaa(x1, x3)
U20_gagaa(x1, x2, x3, x4, x5, x6)  =  U20_gagaa(x1, x3, x6)
halfO_in_ga(x1, x2)  =  halfO_in_ga(x1)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
halfF_in_ga(x1, x2)  =  halfF_in_ga(x1)
halfF_out_ga(x1, x2)  =  halfF_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
halfO_out_ga(x1, x2)  =  halfO_out_ga(x1, x2)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x2, x3, x6)
pU_in_ggaa(x1, x2, x3, x4)  =  pU_in_ggaa(x1, x2)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
U24_gaga(x1, x2, x3, x4, x5)  =  U24_gaga(x1, x3, x5)
U25_gaga(x1, x2, x3, x4, x5)  =  U25_gaga(x1, x2, x3, x5)
ifQ_in_ggga(x1, x2, x3, x4)  =  ifQ_in_ggga(x1, x2, x3)
U13_ggga(x1, x2, x3, x4)  =  U13_ggga(x1, x2, x4)
pR_in_gagaa(x1, x2, x3, x4, x5)  =  pR_in_gagaa(x1, x3)
U26_gagaa(x1, x2, x3, x4, x5, x6)  =  U26_gagaa(x1, x3, x6)
U27_gagaa(x1, x2, x3, x4, x5, x6)  =  U27_gagaa(x1, x2, x3, x6)
pV_in_ggaa(x1, x2, x3, x4)  =  pV_in_ggaa(x1, x2)
U28_ggaa(x1, x2, x3, x4, x5)  =  U28_ggaa(x1, x2, x5)
U29_ggaa(x1, x2, x3, x4, x5)  =  U29_ggaa(x1, x2, x3, x5)
plusT_in_ga(x1, x2)  =  plusT_in_ga(x1)
plusT_out_ga(x1, x2)  =  plusT_out_ga(x1, x2)
U15_ga(x1, x2, x3)  =  U15_ga(x1, x3)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pV_out_ggaa(x1, x2, x3, x4)  =  pV_out_ggaa(x1, x2, x3, x4)
pR_out_gagaa(x1, x2, x3, x4, x5)  =  pR_out_gagaa(x1, x2, x3, x4, x5)
ifQ_out_ggga(x1, x2, x3, x4)  =  ifQ_out_ggga(x1, x2, x3, x4)
false  =  false
U14_ggga(x1, x2, x3, x4)  =  U14_ggga(x1, x2, x4)
pS_in_ggaa(x1, x2, x3, x4)  =  pS_in_ggaa(x1, x2)
U30_ggaa(x1, x2, x3, x4, x5)  =  U30_ggaa(x1, x2, x5)
U31_ggaa(x1, x2, x3, x4, x5)  =  U31_ggaa(x1, x2, x3, x5)
plusJ_in_gga(x1, x2, x3)  =  plusJ_in_gga(x1, x2)
plusJ_out_gga(x1, x2, x3)  =  plusJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pS_out_ggaa(x1, x2, x3, x4)  =  pS_out_ggaa(x1, x2, x3, x4)
pH_out_gaga(x1, x2, x3, x4)  =  pH_out_gaga(x1, x2, x3, x4)
U23_ggaa(x1, x2, x3, x4, x5)  =  U23_ggaa(x1, x2, x3, x5)
plusP_in_ga(x1, x2)  =  plusP_in_ga(x1)
plusP_out_ga(x1, x2)  =  plusP_out_ga(x1, x2)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
pU_out_ggaa(x1, x2, x3, x4)  =  pU_out_ggaa(x1, x2, x3, x4)
pM_out_gagaa(x1, x2, x3, x4, x5)  =  pM_out_gagaa(x1, x2, x3, x4, x5)
ifL_out_ggga(x1, x2, x3, x4)  =  ifL_out_ggga(x1, x2, x3, x4)
U10_ggga(x1, x2, x3, x4)  =  U10_ggga(x1, x2, x4)
pN_in_ggaa(x1, x2, x3, x4)  =  pN_in_ggaa(x1, x2)
U32_ggaa(x1, x2, x3, x4, x5)  =  U32_ggaa(x1, x2, x5)
U33_ggaa(x1, x2, x3, x4, x5)  =  U33_ggaa(x1, x2, x3, x5)
pN_out_ggaa(x1, x2, x3, x4)  =  pN_out_ggaa(x1, x2, x3, x4)
pC_out_gaga(x1, x2, x3, x4)  =  pC_out_gaga(x1, x2, x3, x4)
PLUSD_IN_GGA(x1, x2, x3)  =  PLUSD_IN_GGA(x1, x2)

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

(51) UsableRulesProof (EQUIVALENT transformation)

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

(52) Obligation:

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

PLUSD_IN_GGA(s(T47), T48, s(T50)) → PLUSD_IN_GGA(T47, T48, T50)

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

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

(53) PiDPToQDPProof (SOUND transformation)

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

(54) Obligation:

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

PLUSD_IN_GGA(s(T47), T48) → PLUSD_IN_GGA(T47, T48)

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

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

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

(56) YES